use named axioms

kframework · Feb 11, 2020 · 74f3c0b · 74f3c0b
1 parent 8585a5d
commit 74f3c0b
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 10 deletions.
diff --git a/prover/drivers/coq-driver.md b/prover/drivers/coq-driver.md
@@ -43,9 +43,9 @@ module DRIVER-COQ
        </k>
        <declarations> ( .Bag
                      => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : StringToSort("Term") </declaration>
-                        <declaration> axiom \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
                       ) ...
-       </declarations>       
+       </declarations>
 
 // Translate inductive cases
   rule <k> Inductive ID BINDERs : TERM := .CoqIndCases .
@@ -63,7 +63,7 @@ module DRIVER-COQ
        </k>
        <declarations> ( .Bag
                      => <declaration> symbol CoqIdentToSymbol(IDC)(.Sorts) : StringToSort("Term") </declaration>
-                        <declaration> axiom \type(CoqIdentToSymbol(IDC)(.Patterns), CoqTermToPattern(TERMC))  </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \type(CoqIdentToSymbol(IDC)(.Patterns), CoqTermToPattern(TERMC))  </declaration>
                       ) ...
        </declarations>
 

diff --git a/prover/lang/coq-lang.md b/prover/lang/coq-lang.md
@@ -38,11 +38,6 @@ module COQ
   syntax VariableName ::= CoqNameToVariableName(CoqName) [function]
   rule CoqNameToVariableName(NAME) => StringToVariableName(CoqNameToString(NAME))
 
-  syntax Sorts ::= CoqBindersToSorts(CoqBinders) [function]
-  rule CoqBindersToSorts(.CoqBinders) => .Sorts
-  rule CoqBindersToSorts(NAME:CoqName BINDERs) => StringToSort("Term"), CoqBindersToSorts(BINDERs)
-  rule CoqBindersToSorts((NAMES : TYPE) BINDERs) => CoqNamesToSorts(NAMES) ++Sorts CoqBindersToSorts(BINDERs)
-
   syntax Sorts ::= CoqNamesToSorts(CoqNames) [function]
   rule CoqNamesToSorts(.CoqNames) => .Sorts
   rule CoqNamesToSorts(NAME:CoqName NAMEs) => StringToSort("Term"), CoqNamesToSorts(NAMEs)

diff --git a/prover/t/coq-tests/Logic.v b/prover/t/coq-tests/Logic.v
@@ -5,7 +5,7 @@ Inductive False : Prop := .
 
 Inductive nat : Prop :=
     Z : nat
-  | S : nat -> nat .
+  | S : (forall (x : nat), nat) .
 
 Definition not := fun (A: Prop) => (forall (x : A), False) .
 

diff --git a/prover/t/coq-tests/nat_ind.v b/prover/t/coq-tests/nat_ind.v
@@ -7,7 +7,7 @@ Inductive nat : Type :=  Z : nat | S : forall (x : nat), nat .
 // axiom \type(Z(), nat())
 
 Definition nat_ind := 
-fun (P : nat -> Prop) (f : P 0) (f0 : forall (n : nat), P n -> P (S n)) =>
+fun (P : (forall (n : nat), Prop)) (f : P 0) (f0 : forall (n : nat), (forall (x : P n), P (S n))) =>
 fix F (n : nat) := match n with
                            Z => f
                          | S n0 => f0 n0 (F n0)