Typecheck patch

abstract_syntax.py

@@ -1105,7 +1105,7 @@ def do_function_call(loc, name, type_params, type_args,
       ret = intToNat(loc, x ** y, sname=sname, zname=zname, ty=ty)
     if ret: 
       if get_verbose():
-        print(f"Doing fast arithmetic on call {self}.")
+        print(f"Doing fast arithmetic on call {x} {op} {y}.")
       ret.typeof = return_type
       fast_call = True
 
@@ -1377,8 +1377,7 @@ def reduce_associative(self, loc, name, fun, type_params, type_args,
       return explicit_term_inst(flat_results[0])
     else:
       return Call(self.location, self.typeof,
-                  Var(loc, FunctionType(loc, [], params, returns),
-                      name, [name]),
+                  fun,
                   flat_results)
 
   def substitute(self, sub):
@@ -2209,7 +2208,7 @@ class PTLetNew(Proof):
   body: Proof
 
   def copy(self):
-      return PLetNew(self.location, self.var, self.rhs.copy(), self.body.copy())
+      return PTLetNew(self.location, self.var, self.rhs.copy(), self.body.copy())
 
   def pretty_print(self, indent):
       return indent*' ' + 'define ' + base_name(self.var) + ' = ' + str(self.rhs) + '\n' \
@@ -2294,7 +2293,7 @@ class Cases(Proof):
   cases: List[Tuple[str,Formula,Proof]]
 
   def copy(self):
-      return Cases(self.location, self.subject.copy(), [(l, f.copy(), p.copy()) for (l,f,p) in cases])
+      return Cases(self.location, self.subject.copy(), [(l, f.copy(), p.copy()) for (l,f,p) in self.cases])
 
   def pretty_print(self, indent):
       cases_str = ''
@@ -2487,7 +2486,7 @@ class SomeIntro(Proof):
   body: Proof
 
   def copy(self):
-      return SomeIntro(self.location, [w.copy() for w in witnesses], self.body.copy())
+      return SomeIntro(self.location, [w.copy() for w in self.witnesses], self.body.copy())
 
   def pretty_print(self, indent):
     return indent*' ' + 'choose ' + ",".join([str(t) for t in self.witnesses]) + '\n' \
@@ -2913,7 +2912,7 @@ def copy(self):
                            self.subject.copy())
 
   def __str__(self):
-      return 'definition ' + ' | '.join([str(d) for d in self.definitions]) \
+      return 'expand ' + ' | '.join([str(d) for d in self.definitions]) \
         + ' in ' + str(self.subject)
 
   def uniquify(self, env):
@@ -2945,7 +2944,7 @@ class RewriteFact(Proof):
   equations: List[Proof]
 
   def copy(self):
-      return RewriteFast(self.location,
+      return RewriteFact(self.location,
                          self.subject.copy(),
                          [p.copy() for p in self.equations])
 
@@ -4627,7 +4626,8 @@ def rewrite_aux(loc, formula, equation, env, depth = -1):
       if get_verbose():
           print('is_assoc? ' + str(is_assoc))
       if is_assoc:
-          args = sum([flatten_assoc(rator_name(rator), arg) for arg in args], [])
+          # args = sum([flatten_assoc(rator_name(rator), arg) for arg in args], [])
+          args = flatten_assoc_list(rator_name(rator), args)
       new_rator = rewrite_aux(loc, rator, equation, env, depth - 1)
       new_args = [rewrite_aux(loc, arg, equation, env, depth - 1) for arg in args]
       if get_verbose():

proof_checker.py

@@ -1504,25 +1504,19 @@ def type_check_call_funty(loc, new_rator, args, env, recfun, subterms, ret_ty,
     error(loc, 'incorrect number of arguments in call:\n\t' + str(call) \
           + '\n\texpected ' + str(len(param_types)) \
           + ' arguments, not ' + str(len(args)))
+  # We force associative operators to have the same param type
+  if is_assoc:
+    param_types = [param_types[0]] * len(args)
+
   if len(typarams) == 0:
     #print('type check call to regular: ' + str(call))
-    if is_assoc:
-      new_args = []
-      param_type = param_types[0]
-      for arg in args:
-        new_args.append(type_check_term(arg, param_type, env, recfun, subterms))
-      if ret_ty != None and ret_ty != return_type:
-        error(loc, 'expected ' + str(ret_ty) \
-              + ' but the call returns ' + str(return_type))
-      return Call(loc, return_type, new_rator, new_args)
-    else:
-      new_args = []
-      for (param_type, arg) in zip(param_types, args):
-        new_args.append(type_check_term(arg, param_type, env, recfun, subterms))
-      if ret_ty != None and ret_ty != return_type:
-        error(loc, 'expected ' + str(ret_ty) \
-              + ' but the call returns ' + str(return_type))
-      return Call(loc, return_type, new_rator, new_args)
+    new_args = []
+    for (param_type, arg) in zip(param_types, args):
+      new_args.append(type_check_term(arg, param_type, env, recfun, subterms))
+    if ret_ty != None and ret_ty != return_type:
+      error(loc, 'expected ' + str(ret_ty) \
+            + ' but the call returns ' + str(return_type))
+    return Call(loc, return_type, new_rator, new_args)
   else:
     #print('type check call to generic: ' + str(call))
     matching = {}

test/should-validate/replace_inst_assoc.pf

@@ -0,0 +1,25 @@
+import UInt
+import List
+
+lemma rev_rev_lemma2: all U:type. all xs : List<U>, ys :List<U>.
+    reverse(reverse(xs) ++ ys) = reverse(ys) ++ reverse(reverse(xs))
+proof
+    arbitrary U:type
+    induction List<U>
+    case [] {
+        arbitrary ys:List<U>
+        expand reverse
+        expand operator ++
+        replace append_empty
+        .
+    }
+    case node(x, xs') assume IH : all ys : List<U>. reverse(reverse(xs') ++ ys) = reverse(ys) ++ reverse(reverse(xs')) {
+        arbitrary ys:List<U>
+        expand reverse
+        expand 2* operator ++
+        replace IH[node(x, ys)]
+        expand reverse
+        replace IH[[x]]
+        evaluate
+    }
+end