From e1a2b0d2a88e4797d714ad0cb941c3cbf019720b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sat, 4 Apr 2020 17:20:06 +0100
Subject: Tweak types of loop combinators for prover combinators

Split the variable (tuple) type into an input and output type.  They are
meant to be the same, but due to the way function types are
instantiated, unification can fail in the case of existential types, as
in the added test case (when trying to generate Lem definitions from
it).  The output of the loop will be checked against the expected type,
though, due to a type annotation outside the loop added by the rewrite
pass for variable updates.
---
 src/rewrites.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index ffa790f5..abb3e4ed 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3785,11 +3785,11 @@ let rewrite_defs_remove_superfluous_returns env =
 
 let rewrite_defs_remove_e_assign env (Defs defs) =
   let (Defs loop_specs) = fst (Type_error.check initial_env (Defs (List.map gen_vs
-    [("foreach#", "forall ('vars : Type). (int, int, int, bool, 'vars, 'vars) -> 'vars");
-     ("while#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("until#", "forall ('vars : Type). (bool, 'vars, 'vars) -> 'vars");
-     ("while#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars");
-     ("until#t", "forall ('vars : Type). (bool, 'vars, 'vars, int) -> 'vars")]))) in
+    [("foreach#", "forall ('vars_in 'vars_out : Type). (int, int, int, bool, 'vars_in, 'vars_out) -> 'vars_out");
+     ("while#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out");
+     ("until#", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out) -> 'vars_out");
+     ("while#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out");
+     ("until#t", "forall ('vars_in 'vars_out : Type). (bool, 'vars_in, 'vars_out, int) -> 'vars_out")]))) in
  let rewrite_exp _ e =
     replace_memwrite_e_assign (remove_reference_types (rewrite_var_updates e)) in
   rewrite_defs_base
-- 
cgit v1.2.3