Merge remote-tracking branch 'origin/sail_new_tc' into experiments

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) ->