More tidbits

FStarLang · Nov 29, 2023 · 6f0b5f1 · 6f0b5f1
1 parent aa31ad6
commit 6f0b5f1
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 8 deletions.
diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml
@@ -803,7 +803,7 @@ and mk_return_type env = function
   | TAnonymous t ->
       mk_type_def env t
   | TBottom ->
-      failwith "impossible: TBottom not eliminated"
+      CStar.Void
 
 
 and mk_type env = function

diff --git a/lib/Checker.ml b/lib/Checker.ml
@@ -201,7 +201,7 @@ and check_decl env d =
   if Options.debug "checker" then
     KPrint.bprintf "%schecking %a\n" !indent plid (lid_of_decl d);
   indent := "  ";
-  match d with
+  begin match d with
   | DFunction (_, _, n, t, name, binders, body) ->
       assert (!Options.allow_tapps || n = 0);
       let env = List.fold_left push env binders in
@@ -216,7 +216,8 @@ and check_decl env d =
   | DType _ ->
       (* Barring any parameterized types, there's is nothing to check here
        * really. *)
-      (); ;
+      ()
+  end;
   decr ()
 
 and check_or_infer env _ e =

diff --git a/lib/Helpers.ml b/lib/Helpers.ml
@@ -723,16 +723,19 @@ let rec nest_in_return_pos i typ f e =
 
 let nest_in_return_pos = nest_in_return_pos 0
 
-let push_ignore = nest_in_return_pos TUnit (fun _ e ->
+let push_ignore_ f = nest_in_return_pos TUnit (fun _ e ->
   with_type TUnit (EApp (
-    with_type (TArrow (e.typ, TUnit)) (
+    with_type (TArrow (f e.typ, TUnit)) (
       ETApp (
         with_type (TArrow (TBound 0, TUnit))
           (EQualified (["LowStar"; "Ignore"], "ignore")),
-        [ e.typ ]
+        [ f e.typ ]
       )),
     [ e ])))
 
+let push_ignore = push_ignore_ (fun x -> x)
+let push_ignore_with_type t = push_ignore_ (fun _ -> t)
+
 (* Big AST nodes *************************************************************)
 
 let mk_bufblit src_buf src_ofs dst_buf dst_ofs len =

diff --git a/lib/Simplify.ml b/lib/Simplify.ml
@@ -145,6 +145,7 @@ let optimize_lets ?ifdefs files =
   let _ = (build_usage_map_and_mark ifdefs)#visit_files [] files in
   let files = (use_mark_to_remove_or_ignore (not (ifdefs = None)))#visit_files () files in
   let files = use_mark_to_inline_temporaries#visit_files () files in
+PPrint.(Print.(print (PrintAst.print_files files ^^ hardline)));
   files
 
 (* Unused parameter elimination ***********************************************)

diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml
@@ -189,14 +189,14 @@ let use_mark_to_remove_or_ignore final = object (self)
          but that's ok. *)
       if is_readonly then
         self#remove_trivial_let (snd (open_binder b e2)).node
-      else if e1.typ = TUnit then
+      else if b.typ = TUnit then
         self#remove_trivial_let (ELet ({ b with node = { b.node with meta = Some MetaSequence }}, e1, e2))
       (* Definitely unused, except we can't generate let _ = ignore (bufcreate
          ...) -- this is a bad idea, as it'll force the hoisting phase to hoist
          the bufcreate back into a let-binding, which will then be named "buf". *)
       else if not (is_bufcreate e1) then
         ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit},
-          push_ignore e1,
+          push_ignore_with_type b.typ e1,
           e2)
       (* Definitely unused, push an ignore at depth *)
       else