Various fixes for Hexapod

- Support tuples in lexps
- Rewrite trivial sizeofs
- Rewrite early returns more aggressively
- Support let bindings with ticked variables (binding both a type-level and
  term-level variable at the same time)

1 files changed, 22 insertions, 18 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 4e6b6615..5e0d39a0 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -58,7 +58,11 @@ let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
 
-let fix_id name = match name with
+let is_number_char c =
+  c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
+  c = '6' || c = '7' || c = '8' || c = '9'
+
+let fix_id remove_tick name = match name with
   | "assert"
   | "lsl"
   | "lsr"
@@ -76,22 +80,17 @@ let fix_id name = match name with
   | "EQ"
   | "integer"
     -> name ^ "'"
-  | _ -> name
-
-let is_number char =
-  char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' ||
-  char = '6' || char = '7' || char = '8' || char = '9'
+  | _ ->
+     if name.[0] = '\'' then
+       let var = String.sub name 1 (String.length name - 1) in
+       if remove_tick then var else (var ^ "'")
+     else if is_number_char(name.[0]) then
+       ("v" ^ name ^ "'")
+     else name
 
 let doc_id_lem (Id_aux(i,_)) =
   match i with
-  | Id i ->
-     (* this not the right place to do this, just a workaround *)
-     if i.[0] = '\'' then
-       string ((String.sub i 1 (String.length i - 1)) ^ "'")
-     else if is_number(i.[0]) then
-       string ("v" ^ i ^ "'")
-     else
-       string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -102,7 +101,7 @@ let doc_id_lem_type (Id_aux(i,_)) =
   | Id("int") -> string "ii"
   | Id("nat") -> string "ii"
   | Id("option") -> string "maybe"
-  | Id i -> string (fix_id i)
+  | Id i -> string (fix_id false i)
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
@@ -115,12 +114,14 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
-  | Id i -> string (fix_id (String.capitalize i))
+  | Id i -> string (fix_id false (String.capitalize i))
   | DeIid x ->
      (* add an extra space through empty to avoid a closing-comment
       * token in case of x ending with star. *)
      separate space [colon; string (String.capitalize x); empty]
 
+let doc_var_lem kid = string (fix_id true (string_of_kid kid))
+
 let effectful_set =
   List.exists
     (fun (BE_aux (eff,_)) ->
@@ -230,6 +231,7 @@ let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
   | Typ_wild -> true
   | Typ_id _ -> false
   | Typ_var _ -> true
+  | Typ_exist _ -> true
   | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
   | Typ_tup ts -> List.exists contains_t_pp_var ts
   | Typ_app (c,targs) ->
@@ -321,6 +323,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
+  | P_var kid -> doc_var_lem kid
   | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem sequential mwords true p in
@@ -697,7 +700,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match annot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
@@ -707,7 +710,7 @@ let doc_exp_lem, doc_let_lem =
        let recordtyp = match eannot with
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
-         | _ ->  raise (report l "cannot get record type") in
+         | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
@@ -1011,6 +1014,7 @@ let doc_exp_lem, doc_let_lem =
                                  top_exp sequential mwords early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
+    | LEXP_tup lexps -> parens (separate_map comma_sp (doc_lexp_deref_lem sequential mwords early_ret) lexps)
     | _ ->
        raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen"))
              (* expose doc_exp_lem and doc_let *)