Merge branch 'main' of https://github.com/jsiek/deduce

Deduce.lark

@@ -88,9 +88,9 @@ ident: IDENT              -> ident
     | "fun" var_list "{" term "}"                  -> lambda
     | "generic" ident_list "{" term "}"            -> generic
     | "switch" term "{" switch_list "}"            -> switch
-    | "all" var_list "." term                      -> all_formula
-    | "<" ident_list ">" term                       -> alltype_formula
-    | "some" var_list "." term                     -> some_formula
+    | "all" type_annot_list "." term               -> all_formula
+    | "<" ident_list ">" term                      -> alltype_formula
+    | "some" type_annot_list "." term              -> some_formula
     | "define" IDENT "=" term ";" term             -> define_term
     | "?"                                          -> hole_term
     | "─"                                          -> omitted_term
@@ -107,6 +107,10 @@ ident: IDENT              -> ident
     | ident                                        -> single
     | ident "," ident_list                         -> push
 
+?type_annot_list:                                  -> empty_binding
+    | ident ":" type                               -> single_binding
+    | ident ":" type "," type_annot_list           -> push_binding
+
 ?var_list:                                         -> empty_binding
     | ident ":" type                               -> single_binding
     | ident ":" type "," var_list                  -> push_binding
@@ -184,7 +188,7 @@ ident: IDENT              -> ident
     | "sorry"                                            -> sorry_proof
     | "{" proof "}"
 
-?proof_stmt: "arbitrary" var_list                   -> all_intro
+?proof_stmt: "arbitrary" type_annot_list                   -> all_intro
     | "assume" IDENT                                -> imp_intro
     | "assume" IDENT ":" term                       -> imp_intro_explicit
     | "assume" ":" term                             -> imp_intro_anon

rec_desc_parser.py

@@ -119,7 +119,7 @@ def parse_term_hi():
 
   if token.type == 'ALL':
     advance()
-    vars = parse_var_list()
+    vars = parse_type_annot_list()
     if current_token().type != 'DOT':
       error(meta_from_tokens(current_token(), current_token()),
             'expected "." after parameters of "all", not\n\t' \
@@ -288,7 +288,7 @@ def parse_term_hi():
 
   elif token.type == 'SOME':
     advance()
-    vars = parse_var_list()
+    vars = parse_type_annot_list()
     if current_token().type != 'DOT':
       error(meta_from_tokens(token, current_token()),
             'expected "." after parameters of "some", not\n\t' \
@@ -903,7 +903,7 @@ def parse_proof_statement():
 
   elif token.type == 'ARBITRARY':
     advance()
-    vars = parse_var_list()
+    vars = parse_type_annot_list()
     meta = meta_from_tokens(token, previous_token())
     result = None
     for j, var in enumerate(reversed(vars)):
@@ -1154,7 +1154,7 @@ def parse_equation_list():
 
 def parse_theorem():
   while_parsing = 'while parsing\n' \
-      + '\tproof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"'
+      + '\tproof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"'
   try:    
     start_token = current_token()
     advance()
@@ -1510,6 +1510,33 @@ def parse_ident_list():
     ident_list.append(ident)
   return ident_list
 
+def parse_type_annot_list():
+  start_tok = current_token()
+  ident = parse_identifier()
+  if current_token().type == 'COLON':
+    advance()
+    ty = parse_type()
+  else:
+    error(meta_from_tokens(current_token(), current_token()), "Missing type annotation. Expected ':' followed by a type.\n" \
+          + error_header(meta_from_tokens(start_tok, current_token())) \
+          + 'while parsing\n\ttype_annot_list ::= identifier ":" type' \
+          + '\n\ttype_annot_list ::= identifier ":" type "," type_annot_list')
+  type_annot_list = [(ident,ty)]
+
+  while current_token().type == 'COMMA':
+    advance()
+    ident = parse_identifier()
+    if current_token().type == 'COLON':
+      advance()
+      ty = parse_type()
+    else:
+      error(meta_from_tokens(current_token(), current_token()), "Missing type annotation. Expected ':' followed by a type.\n" \
+          + error_header(meta_from_tokens(start_tok, current_token())) \
+          + 'while parsing\n\ttype_annot_list ::= identifier ":" type' \
+          + '\n\ttype_annot_list ::= identifier ":" type "," type_annot_list')
+    type_annot_list.append((ident, ty))
+  return type_annot_list
+
 def parse_var_list():
   ident = parse_identifier()
   if current_token().type == 'COLON':

test/should-error/all5.pf.err

@@ -3,4 +3,4 @@
 while parsing
 	term ::= "all" var_list "." term
 ./test/should-error/all5.pf:1.1-1.24: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/define_proof_missing_term.pf.err

@@ -4,4 +4,4 @@
 	proof_stmt ::= "define" identifier "=" term
 
 ./test/should-error/define_proof_missing_term.pf:1.1-3.13: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/induction_case.pf.err

@@ -7,4 +7,4 @@
 	conclusion ::= "induction" type ind_case*
 
 ./test/should-error/induction_case.pf:16.1-20.14: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/inst-term-angle-bracket.pf.err

@@ -3,4 +3,4 @@
 while trying to parse type arguments for instantiation of an "all" formula:
 	proof ::= proof "<" type_list ">"
 ./test/should-error/inst-term-angle-bracket.pf:4.1-8.17: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/missing-colon-in-have.pf.err

@@ -5,4 +5,4 @@
 	proof_stmt ::= "have" ":" formula "by" proof
 
 ./test/should-error/missing-colon-in-have.pf:1.1-3.7: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/missing-conclusion.pf.err

@@ -1,4 +1,4 @@
 ./test/should-error/missing-conclusion.pf:5.1-5.4: missing conclusion after
 	have Y: true by .
 ./test/should-error/missing-conclusion.pf:1.1-4.20: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/suffices_misspell.pf.err

@@ -1,3 +1,3 @@
 ./test/should-error/suffices_misspell.pf:5.3-5.10: did you mean "suffices" instead of "sufices"?
 ./test/should-error/suffices_misspell.pf:1.1-4.15: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"

test/should-error/theorem_implies8.pf.err

@@ -3,4 +3,4 @@
 while parsing
 	formula ::= "if" formula "then" formula
 ./test/should-error/theorem_implies8.pf:1.1-1.20: while parsing
-	proof_stmt ::= "theorem" identfier ":" formula "proof" proof "end"
+	proof_stmt ::= "theorem" identifier ":" formula "proof" proof "end"