diff options
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 95ddc580..7adccfdf 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -239,7 +239,8 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a = | Typ_id (Id_aux (Id "string", _)) -> "\"\"" | _ -> "(failwith \"undefined value of unsupported type\")") | _ -> "(failwith \"undefined value of unsupported type\")") - | L_string s -> "\"" ^ s ^ "\"") + | L_string s -> "\"" ^ s ^ "\"" + | L_real s -> s (* TODO What's the Lem syntax for reals? *)) (* typ_doc is the doc for the type being quantified *) @@ -257,16 +258,10 @@ let is_ctor env id = match Env.lookup_id id env with *) let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_app(id, ((_ :: _) as pats)) -> - (match annot with - | Some (env, _, _) when (is_ctor env id) -> - let ppp = doc_unop (doc_id_lem_ctor id) - (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in - if apat_needed then parens ppp else ppp - | _ -> empty) - | P_app(id,[]) -> - (match annot with - | Some (env, _, _) when (is_ctor env id) -> doc_id_lem_ctor id - | _ -> empty) + let ppp = doc_unop (doc_id_lem_ctor id) + (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in + if apat_needed then parens ppp else ppp + | P_app(id,[]) -> doc_id_lem_ctor id | P_lit lit -> doc_lit_lem true lit annot | P_wild -> underscore | P_id id -> @@ -281,15 +276,14 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in if apat_needed then parens ppp else ppp | P_vector_concat pats -> - let ppp = - (separate space) - [string "Vector";parens (separate_map (string "::") (doc_pat_lem regtypes true) pats);underscore;underscore] in - if apat_needed then parens ppp else ppp + raise (Reporting_basic.err_unreachable l + "vector concatenation patterns should have been removed before pretty-printing") | P_tup pats -> (match pats with | [p] -> doc_pat_lem regtypes apat_needed p | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats)) - | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*) + | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*) + | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem regtypes true p) (doc_pat_lem regtypes true p') | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *) let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with @@ -926,7 +920,7 @@ let doc_exp_lem, doc_let_lem = | E_return _ -> raise (Reporting_basic.err_todo l "pretty-printing early return statements to Lem not yet supported") - | E_comment _ | E_comment_struc _ -> empty + | E_constraint _ | E_comment _ | E_comment_struc _ -> empty | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable l "unsupported internal expression encountered while pretty-printing") @@ -944,9 +938,13 @@ let doc_exp_lem, doc_let_lem = else doc_id_lem id in group (doc_op equals fname (top_exp regtypes true e)) - and doc_case regtypes (Pat_aux(Pat_exp(pat,e),_)) = + and doc_case regtypes = function + | Pat_aux(Pat_exp(pat,e),_) -> group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow]) (group (top_exp regtypes false e))) + | Pat_aux(Pat_when(_,_,_),(l,_)) -> + raise (Reporting_basic.err_unreachable l + "guarded pattern expression should have been rewritten before pretty-printing") and doc_lexp_deref_lem regtypes ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_field (le,id) -> |