move closer to power.sail -> power.ml output

3 files changed, 22 insertions, 10 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 24c978fd..b85b31da 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1287,7 +1287,7 @@ let doc_lit_ocaml in_pat (L_aux(l,_)) =
   | L_one   -> "Vone"
   | L_true  -> "Vone"
   | L_false -> "Vzero"
-  | L_num i -> if in_pat then string_of_int i else "(big_int_of_int " ^ string_of_int i ^ ")"
+  | L_num i -> string_of_int i
   | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)
   | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)
   | L_undef -> "Vundef"
@@ -1407,11 +1407,19 @@ let doc_exp_ocaml, doc_let_ocaml =
          *)*)
     | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
     | E_app(f,args) ->
-      let call = match annot with
-        | Base(_,External (Some n),_,_,_,_) -> string n
-        | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i f
-        | _ -> doc_id_ocaml f in
-      parens (doc_unop call (parens (separate_map comma exp args)))
+      let call,ctor = match annot with
+        | Base(_,External (Some n),_,_,_,_) -> string n,false
+        | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i f,true
+        | _ -> doc_id_ocaml f,false in
+      let base_print () = parens (doc_unop call (parens (separate_map comma exp args))) in
+      if not(ctor)
+      then base_print ()
+      else (match args with
+        | [] -> call
+        | [arg] -> (match arg with
+            | E_aux(E_lit (L_aux(L_unit,_)),_) -> call
+            | _ -> base_print())
+        | args ->  base_print())
     | E_vector_access(v,e) ->
       let call = (match annot with
           | Base((_,t),_,_,_,_,_) ->
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 3d211d82..f3120833 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -89,8 +89,9 @@ let rec format_loc_aux ff l =
   let (l_org, mod_s) = dest_loc l in
   let _ = match l_org with
     | Parse_ast.Unknown -> Format.fprintf ff "no location information available"
+    | Parse_ast.Generated l -> Format.fprintf ff "Code generated: original nearby source is "; (format_loc_aux ff l)
     | Parse_ast.Range(p1,p2) -> format_pos2 ff p1 p2
-    | Parse_ast.Int(s,_) -> Format.fprintf ff "code generated by: %s" s
+    | Parse_ast.Int(s,_) -> Format.fprintf ff "code in lib from: %s" s
   in
   ()
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 18994458..d957ee6c 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1151,8 +1151,9 @@ let rewrite_exp_separate_ints rewriters nmap ((E_aux (exp,(l,annot))) as full_ex
   match exp with
   | E_lit (L_aux (((L_num _) as lit),_)) ->
     (match (is_within_machine64 t nexps) with
-     | Yes | Maybe -> rewrite_base full_exp
-     | No -> E_aux(E_app(Id_aux (Id "integer_of_int",l),[rewrite_base full_exp]),
+     | Yes -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int yes\n" in rewrite_base full_exp
+     | Maybe -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int maybe\n" in rewrite_base full_exp
+     | No -> let _ = Printf.eprintf "Rewriter of num_const, within 64bit int no\n" in E_aux(E_app(Id_aux (Id "integer_of_int",l),[rewrite_base full_exp]),
                    (l, Base((tparms,t),External(None),nexps,eff,cum_eff,bounds))))
   | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite_rec exp))
   | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite_rec exps))
@@ -1172,7 +1173,9 @@ let rewrite_exp_separate_ints rewriters nmap ((E_aux (exp,(l,annot))) as full_ex
                        (fun (Pat_aux (Pat_exp(p,e),pannot)) -> 
                           Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite_rec e),pannot)) pexps)))
   | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite_rec body))
-  | _ -> rewrite_rec full_exp
+  | E_internal_let (lexp,exp,body) ->
+    rewrap (E_internal_let (rewriters.rewrite_lexp rewriters nmap lexp, rewrite_rec exp, rewrite_rec body))
+  | _ -> rewrite_base full_exp
 
 let rewrite_defs_separate_numbs defs = rewrite_defs_base
     {rewrite_exp = rewrite_exp_separate_ints;