diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_lem.ml | 1 | ||||
| -rw-r--r-- | src/spec_analysis.ml | 9 |
2 files changed, 9 insertions, 1 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 169bd824..7d2cc479 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1444,6 +1444,7 @@ let rec doc_def_lem type_env def = | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings" | DEF_pragma _ -> empty + | DEF_measure _ -> empty (* we might use these in future *) let find_exc_typ defs = let is_exc_typ_def = function diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml index 634b34b6..907a2f10 100644 --- a/src/spec_analysis.ml +++ b/src/spec_analysis.ml @@ -502,7 +502,14 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef | DEF_reg_dec rdec -> fv_of_rd consider_var rdec | DEF_pragma _ -> mt,mt - | DEF_measure _ -> mt,mt (* currently removed beforehand *) + (* removed beforehand for Coq, but may still be present otherwise *) + | DEF_measure(id,pat,exp) -> + let i = string_of_id id in + let used = Nameset.of_list [i; "val:"^i] in + ((fun (_,u,_) -> Nameset.singleton ("measure:"^i),u) + (fv_of_pes consider_var mt used mt + [Pat_aux(Pat_exp (pat,exp),(Unknown,Type_check.empty_tannot))])) + let group_defs consider_scatter_as_one (Ast.Defs defs) = List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs |