diff options
| author | Alasdair | 2019-04-27 00:20:37 +0100 |
|---|---|---|
| committer | Alasdair | 2019-04-27 00:40:56 +0100 |
| commit | 0c99f19b012205f1be1d4ae18b722ecbdd80e3d4 (patch) | |
| tree | 55f796f9bdf270064bfe87bdf275b93ffcdc1fb2 /src/pretty_print_lem.ml | |
| parent | bf240119e43cb4e3b5f5746b5ef21f19a8fac2d2 (diff) | |
| parent | 094c8e254abde44d45097aca7a36203704fe2ef4 (diff) | |
Merge branch 'sail2' into smt_experiments
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 6479a028..10441ed5 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -715,11 +715,12 @@ let doc_exp_lem, doc_let_lem = | _ -> raise (Reporting.err_unreachable l __POS__ "Unexpected number of arguments for loop combinator") end - | Id_aux (Id (("while#" | "until#") as combinator), _) -> - let combinator = String.sub combinator 0 (String.length combinator - 1) in + | Id_aux (Id (("while#" | "until#" | "while#t" | "until#t") as combinator), _) -> + let combinator = String.sub combinator 0 (String.index combinator '#') in begin match args with - | [cond; varstuple; body] -> + | [cond; varstuple; body] + | [cond; varstuple; body; _] -> (* Ignore termination measures - not used in Lem *) let return (E_aux (e, a)) = E_aux (E_internal_return (E_aux (e, a)), a) in let csuffix, cond, body = match effectful (effect_of cond), effectful (effect_of body) with @@ -1408,7 +1409,7 @@ let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) = let doc_spec_lem env (VS_aux (valspec,annot)) = match valspec with - | VS_val_spec (typschm,id,ext,_) when ext "lem" = None -> + | VS_val_spec (typschm,id,exts,_) when Ast_util.extern_assoc "lem" exts = None -> (* let (TypSchm_aux (TypSchm_ts (tq, typ), _)) = typschm in if contains_t_pp_var typ then empty else *) doc_docstring_lem annot ^^ @@ -1485,6 +1486,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 *) + | DEF_loop_measures _ -> empty let find_exc_typ defs = let is_exc_typ_def = function |