diff options
| author | Thomas Bauereiss | 2020-04-04 17:20:06 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-04-21 02:20:11 +0100 |
| commit | e1a2b0d2a88e4797d714ad0cb941c3cbf019720b (patch) | |
| tree | d4b70e68765ac6cb7c2795fdd313047185cafab0 /src | |
| parent | 264ab693afa90a1e9fa842f5972f64dc7e06c492 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 |