From 957f4b277b7efabf200e81a1c60cbe8c42af12fd Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 7 Dec 2020 17:31:29 -0800
Subject: [PATCH 1/3] modify LFSC 1.5 grammar to what rlfsc's "sugar" branch
 currently implements

---
 doc/lfsc1_5.g4 | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/doc/lfsc1_5.g4 b/doc/lfsc1_5.g4
index 3452c4a..97e0f7c 100644
--- a/doc/lfsc1_5.g4
+++ b/doc/lfsc1_5.g4
@@ -78,7 +78,7 @@ ntype
 // (^ c t)
 
 // Extension /////////////////////
-vtype : '(' 'var' iden ntype ')' ;
+vtype : '(' 'id' iden ntype ')' ;
 //////////////////////////////////
 
 type 
@@ -89,7 +89,7 @@ type
   | '(' '!' iden ntype type ')' 
 // Extension ///////////////////////////////
   | '(' 'Forall' iden ntype type ')' 
-  | '(' '->' ( ntype | vtype )+ type ')'  
+  | '(' '->' '(' ( ntype | vtype )+ ')' type ')'  
 ////////////////////////////////////////////
   ;
 // (Forall ξ τ₁ τ₂)
@@ -117,14 +117,16 @@ term
   | rat_const
   | '(' term term+ ')'
   | '(' '\\' iden term ')'
-  | '(' '@' iden term ')'
+  | '(' '@' iden term term ')'
   | '(' ':' type term ')'
   | '(' '%' iden type term ')'
 // Extensions ///////////////////
   | '(' 'lam' iden term ')'
   | '(' 'let' iden term term ')'
   | '(' 'proved-by' type term ')'
-  | '(' 'assuming' vtype+ term ')'
+  | '(' 'assuming' iden type term ')'
+// TODO
+//  | '(' 'assuming' '(' vtype+ ')' term ')'
   ;
 //////////////////////////////////
 // (lam ξ t)
@@ -167,4 +169,4 @@ code
 INT : [0-9]+ ;
 RAT : ('0' | [1-9][0-9]*) '/' [1-9][0-9]* ;
 ID : [a-zA-Z~!@$%^&*_\-+=<>.?/][a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ;
-KW : ':'[a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ; 
\ No newline at end of file
+KW : ':'[a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ; 

From a834b337cff8436df5d6114b324b7a04a548d9fb Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Tue, 8 Dec 2020 17:08:12 -0800
Subject: [PATCH 2/3] Update 'assuming' form

---
 doc/lfsc1_5.g4 | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/doc/lfsc1_5.g4 b/doc/lfsc1_5.g4
index 97e0f7c..e62d607 100644
--- a/doc/lfsc1_5.g4
+++ b/doc/lfsc1_5.g4
@@ -124,9 +124,7 @@ term
   | '(' 'lam' iden term ')'
   | '(' 'let' iden term term ')'
   | '(' 'proved-by' type term ')'
-  | '(' 'assuming' iden type term ')'
-// TODO
-//  | '(' 'assuming' '(' vtype+ ')' term ')'
+  | '(' 'assuming' '(' (ntype | vtype)+ ')' term ')'
   ;
 //////////////////////////////////
 // (lam ξ t)

From eeae3865dbceb22892dee44dcade4a7230953bba Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 14 Dec 2020 13:03:56 -0800
Subject: [PATCH 3/3] Post-discussion changes:

* (: instead of (id in declaration lists
* check-assuming
* define-const
---
 doc/lfsc1_5.g4 | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

diff --git a/doc/lfsc1_5.g4 b/doc/lfsc1_5.g4
index e62d607..fef8e3e 100644
--- a/doc/lfsc1_5.g4
+++ b/doc/lfsc1_5.g4
@@ -17,8 +17,10 @@ command
   | '(' 'run' code ')'
   | '(' 'program' iden '(' typed_par+ ')' type code ')'
 // Extension /////////////////////////////////
-  | '(' 'declare-type' iden '(' type* ')' ')'
-  | '(' 'declare-rule' iden ( ntype | vtype )+ type ')' ')'
+  | '(' 'declare-type' iden decl_list ')'
+  | '(' 'declare-rule' iden decl_list type ')'
+  | '(' 'define-const' iden decl_list term ')'
+  | '(' 'check-assuming' decl_list type term ')'
 //////////////////////////////////////////////
   ;
 // (declare-type c (τ₁ ⋯ τᵢ)) with i > 0
@@ -33,6 +35,8 @@ command
 // is equivalent to
 // (declare r (-> r ν₁ ⋯ νᵢ τ))
 
+decl_list : '(' (ntype | vtype)* ')';
+
 iden : ID ;
 
 kind 
@@ -78,7 +82,7 @@ ntype
 // (^ c t)
 
 // Extension /////////////////////
-vtype : '(' 'id' iden ntype ')' ;
+vtype : '(' ':' iden ntype ')' ;
 //////////////////////////////////
 
 type 
@@ -89,7 +93,7 @@ type
   | '(' '!' iden ntype type ')' 
 // Extension ///////////////////////////////
   | '(' 'Forall' iden ntype type ')' 
-  | '(' '->' '(' ( ntype | vtype )+ ')' type ')'  
+  | '(' '->' decl_list type ')'  
 ////////////////////////////////////////////
   ;
 // (Forall ξ τ₁ τ₂)
@@ -119,12 +123,11 @@ term
   | '(' '\\' iden term ')'
   | '(' '@' iden term term ')'
   | '(' ':' type term ')'
+  // Deprecated
   | '(' '%' iden type term ')'
 // Extensions ///////////////////
   | '(' 'lam' iden term ')'
   | '(' 'let' iden term term ')'
-  | '(' 'proved-by' type term ')'
-  | '(' 'assuming' '(' (ntype | vtype)+ ')' term ')'
   ;
 //////////////////////////////////
 // (lam ξ t)