Merge branch 'protz_comments' of github.com:FStarLang/karamel into pr…

…otz_comments

lib/Ast.ml

@@ -120,12 +120,18 @@ and branch_t =
 and fields_t =
   (ident * (typ * bool)) list
 
+type node_meta =
+  | CommentBefore of string
+  | CommentAfter of string
+
+and node_meta' = node_meta [@visitors.opaque] [@@deriving show]
 
 (* This type, by virtue of being separated from the recursive definition of expr
  * and pattern, generates no implementation. We provide our own below. *)
 type 'a with_type = {
   node: 'a;
-  mutable typ: typ
+  mutable typ: typ;
+  meta: node_meta' list;
     (** Filled in by [Checker] *)
 }
   [@@deriving show]
@@ -163,7 +169,7 @@ class ['self] map_typ_adapter = object (self: 'self)
     fun f (env, _) x ->
       let typ = self#visit_typ env x.typ in
       let node = f (env, typ) x.node in
-      { node; typ }
+      { node; typ; meta = x.meta }
 end
 
 class ['self] iter_typ_adapter = object (self: 'self)
@@ -283,7 +289,6 @@ type expr' =
      * ]}
      * The scope of the binder is the second, third and fourth expressions. *)
   | ECast of expr * typ_wo
-  | EComment of string * expr * string
   | EStandaloneComment of string
   | EAddrOf of expr
 
@@ -381,7 +386,7 @@ class ['self] map_expr_adapter = object (self: 'self)
     fun f env x ->
       let typ = self#visit_typ env x.typ in
       let node = f (env, typ) x.node in
-      { node; typ }
+      { node; typ; meta = x.meta }
 
   method visit_expr_w env e =
     self#visit_expr (env, e.typ) e
@@ -679,7 +684,7 @@ let map_decls f files =
   List.map (fun (file, decls) -> file, List.map f decls) files
 
 let with_type typ node =
-  { typ; node }
+  { typ; node; meta = [] }
 
 let flatten_tapp t =
   let rec flatten_tapp cgs t =

lib/AstToCFlat.ml

@@ -893,9 +893,6 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr =
   | ETuple _ | EMatch _ | ECons _ ->
       invalid_arg "should've been desugared before"
 
-  | EComment (_, e, _) ->
-      mk_expr env locals e
-
   | ESequence es ->
       let locals, es = fold (mk_expr env) locals es in
       locals, CF.Sequence es

lib/AstToCStar.ml

@@ -349,6 +349,16 @@ and return_type_not_needed e =
   | _ -> false
 
 and mk_expr env in_stmt e =
+  (* Wrap in comment node if need be. *)
+  let meta = match e.node with ELet (b, _, _) -> b.meta @ e.meta | _ -> e.meta in
+  begin match List.filter_map (function CommentBefore s -> Some s | _ -> None) meta,
+    List.filter_map (function CommentAfter s -> Some s | _ -> None) meta
+  with
+  | [], [] -> fun e -> e
+  | s, s' -> fun e -> CStar.InlineComment (String.concat "\n" s, e, String.concat "\n" s')
+  end @@
+
+  (* Actual translation. *)
   let mk_expr env e = mk_expr env false e in
   match e.node with
   | EBound var ->
@@ -430,9 +440,6 @@ and mk_expr env in_stmt e =
   | EField (expr, field) ->
       CStar.Field (mk_expr env expr, field)
 
-  | EComment (s, e, s') ->
-      CStar.InlineComment (s, mk_expr env e, s')
-
   | EAddrOf e ->
       CStar.AddrOf (mk_expr env e)
 
@@ -661,10 +668,6 @@ and mk_stmts env e ret_type =
     | EReturn e ->
         mk_as_return env e acc Must
 
-    | EComment (s, e, s') ->
-        let env, stmts = collect (env, CStar.Comment s :: acc) return_pos e in
-        env, CStar.Comment s' :: stmts
-
     | EStandaloneComment s ->
         env, maybe_return (CStar.Comment s :: acc)
 

lib/AstToMiniRust.ml

@@ -582,7 +582,7 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
 (* However, generally, we will have a type provided by the context that may
    necessitate the insertion of conversions *)
 and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr =
-  (* KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e; *)
+  KPrint.bprintf "translate_expr_with_type: %a @@ %a\n" PrintMiniRust.ptyp t_ret PrintAst.Ops.pexpr e;
 
   let erase_lifetime_info = (object(self)
     inherit [_] MiniRust.DeBruijn.map
@@ -737,7 +737,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       assert (cgs @ cgs' = []);
       let es =
         match es with
-        | [ { typ = TUnit; node } ] -> assert (node = EUnit); []
+        | [ { typ = TUnit; node; _ } ] -> assert (node = EUnit); []
         | _ -> es
       in
       let env, e = translate_expr env e in
@@ -755,7 +755,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
   | EApp (e0, es) ->
       let es =
         match es with
-        | [ { typ = TUnit; node } ] -> assert (node = EUnit); []
+        | [ { typ = TUnit; node; _ } ] -> assert (node = EUnit); []
         | _ -> es
       in
       let env, e0 = translate_expr env e0 in
@@ -1074,8 +1074,6 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
   | ECast (e, t) ->
       let env, e = translate_expr env e in
       env, As (e, translate_type env t)
-  | EComment _ ->
-      failwith "TODO: EComment"
   | EStandaloneComment _ ->
       failwith "TODO: EStandaloneComment"
   | EAddrOf _e1 ->

lib/Checker.ml

@@ -339,9 +339,6 @@ and check' env t e =
         Warn.maybe_fatal_error ("", NotLowStarCast e);
       c (infer env e)
 
-  | EComment (_, e, _) ->
-      check env t e
-
   | ELet (binder, body, cont) ->
       let t' = check_or_infer (locate env (In binder.node.name)) binder.typ body in
       binder.typ <- t';
@@ -833,9 +830,6 @@ and infer' env e =
       ) branches in
       t
 
-  | EComment (_, e, _) ->
-      infer env e
-
   | EFun (binders, e, t_ret) ->
       let env = List.fold_left push env binders in
       check env t_ret e;

lib/DataTypes.ml

@@ -137,7 +137,7 @@ let remove_unused_type_arguments files =
             chop (kept + 1) (i + 1) (def, binders, ret)
           else
             let def = DeBruijn.subst_te TAny (n - i - 1) def in
-            let binders = List.map (fun { node; typ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ }) binders in
+            let binders = List.map (fun { node; typ; _ } -> { node; typ = DeBruijn.subst_t TAny (n - i - 1) typ; meta = [] }) binders in
             let ret = DeBruijn.subst_t TAny (n - i - 1) ret in
             chop kept (i + 1) (def, binders, ret)
       in
@@ -511,17 +511,17 @@ let compile_simple_matches (map, enums) = object(self)
   method! visit_expr_w env x =
     let node = self#visit_expr' (env, x.typ) x.node in
     let typ = self#visit_typ env x.typ in
-    { node; typ }
+    { node; typ; meta = [] }
 
   method! visit_pattern_w env x =
     let node = self#visit_pattern' (env, x.typ) x.node in
     let typ = self#visit_typ env x.typ in
-    { node; typ }
+    { node; typ; meta = [] }
 
   method! visit_with_type f (env, _) x =
       let node = f (env, x.typ) x.node in
       let typ = self#visit_typ env x.typ in
-      { node; typ }
+      { node; typ; meta = [] }
 
   method! visit_TQualified _ lid =
     match Hashtbl.find map lid with

lib/DeBruijn.ml

@@ -234,7 +234,7 @@ let close_branch bs p e =
 let opening_binder b =
   let a = Atom.fresh () in
   let b = { b with node = { b.node with atom = a } } in
-  b, subst { node = EOpen (b.node.name, a); typ = b.typ } 0
+  b, subst { node = EOpen (b.node.name, a); typ = b.typ; meta = [] } 0
 
 let open_binder b e1 =
   let b, f = opening_binder b in
@@ -254,7 +254,7 @@ let open_branch bs pat expr =
   List.fold_right (fun binder (bs, pat, expr) ->
     let b, expr = open_binder binder expr in
     let pat =
-      subst_p { node = POpen (b.node.name, b.node.atom); typ = b.typ } 0 pat
+      subst_p { node = POpen (b.node.name, b.node.atom); typ = b.typ; meta = [] } 0 pat
     in
     b :: bs, pat, expr
   ) bs ([], pat, expr)

lib/Helpers.ml

@@ -71,7 +71,7 @@ let pwild = with_type TAny PWild
 
 let mk_op op w =
   { node = EOp (op, w);
-    typ = type_of_op op w }
+    typ = type_of_op op w; meta = [] }
 
 (* @0 < <finish> *)
 let mk_lt w finish =
@@ -160,13 +160,13 @@ let unused_binding = sequence_binding
 let mk_binding ?(mut=false) name t =
   let b = fresh_binder name t in
   { b with node = { b.node with mut } },
-  { node = EOpen (b.node.name, b.node.atom); typ = t }
+  { node = EOpen (b.node.name, b.node.atom); typ = t; meta = [] }
 
 (** Generates "let [[name]]: [[t]] = [[e]] in [[name]]" *)
 let mk_named_binding name t e =
   let b, ref = mk_binding name t in
   b,
-  { node = e; typ = t },
+  { node = e; typ = t; meta = [] },
   ref
 
 
@@ -411,7 +411,7 @@ let rec is_initializer_constant e =
   match e with
   | { node = EAddrOf { node = EQualified _; _ }; _ } ->
       true
-  | { node = EQualified _; typ = t } ->
+  | { node = EQualified _; typ = t; _ } ->
       is_address t
   | { node = EEnum _; _ } ->
       true
@@ -688,7 +688,7 @@ let rec strip_cast e =
 let rec nest bs t e2 =
   match bs with
   | (b, e1) :: bs ->
-      { node = ELet (b, e1, close_binder b (nest bs t e2)); typ = t }
+      { node = ELet (b, e1, close_binder b (nest bs t e2)); typ = t; meta = [] }
   | [] ->
       e2
 
@@ -715,30 +715,30 @@ let rec nest_in_return_pos i typ f e =
   match e.node with
   | ELet (b, e1, e2) ->
       let e2 = nest_in_return_pos (i + 1) typ f e2 in
-      { node = ELet (b, e1, e2); typ }
+      { node = ELet (b, e1, e2); typ; meta = [] }
   | EIfThenElse (e1, e2, e3) ->
       let e2 = nest_in_return_pos i typ f e2 in
       let e3 = nest_in_return_pos i typ f e3 in
-      { node = EIfThenElse (e1, e2, e3); typ }
+      { node = EIfThenElse (e1, e2, e3); typ; meta = [] }
   | ESwitch (e, branches) ->
       let branches = List.map (fun (t, e) ->
         t, nest_in_return_pos i typ f e
       ) branches in
-      { node = ESwitch (e, branches); typ }
+      { node = ESwitch (e, branches); typ; meta = [] }
   | EMatch (c, e, branches) ->
       { node =
         EMatch (c, e, List.map (fun (bs, p, e) ->
           bs, p, nest_in_return_pos (i + List.length bs) typ f e
         ) branches);
-        typ }
+        typ; meta = [] }
   | ESequence es ->
       let l = List.length es in
       { node = ESequence (List.mapi (fun j e ->
           if j = l - 1 then
             nest_in_return_pos i typ f e
           else
             e
-        ) es); typ }
+        ) es); typ; meta = [] }
   | _ ->
       f i e
 

lib/Inlining.ml

@@ -91,17 +91,6 @@ let rec memoize_inline map visit lid =
  * boolean, return a function from an [lid] to its body where inlining has been
  * performed. *)
 let mk_inliner files criterion =
-  let debug_inline = Options.debug "inline" in
-  let wrap_comment lid term =
-    if debug_inline then
-      EComment (
-        KPrint.bsprintf "start inlining %a" plid lid,
-        term,
-        KPrint.bsprintf "end inlining %a" plid lid)
-    else
-      term.node
-  in
-
   (* Build a map suitable for the [memoize_inline] combinator. *)
   let map = Helpers.build_map files (fun map -> function
     | DGlobal (_, name, _, _, body)
@@ -121,7 +110,7 @@ let mk_inliner files criterion =
            * meaning we may pass more arguments to safe_substitution than the
            * function definition takes. Safe_substitution just drops them and
            * this results in typing errors later on. *)
-          wrap_comment lid (Helpers.safe_substitution es (recurse lid) t)
+          (Helpers.safe_substitution es (recurse lid) t).node
       | _ ->
           EApp (self#visit_expr_w () e, es)
     method! visit_EQualified (_, t) lid =

lib/InputAstToAst.ml

@@ -9,7 +9,7 @@ open Common
 module I = InputAst
 
 let mk (type a) (node: a): a with_type =
-  { node; typ = TAny }
+  { node; typ = TAny; meta = [] }
 
 let rec binders_of_pat p =
   let open I in
@@ -147,13 +147,13 @@ and mk_expr = function
   | I.EApp (I.ETApp (I.EQualified ([ "Steel"; "Reference" ], "null"), [ t ]), [ I.EUnit ])
   | I.EApp (I.ETApp (I.EQualified ([ "C"; "Nullity" ], "null"), [ t ]), [ I.EUnit ])
   | I.EBufNull t ->
-      { node = EBufNull; typ = TBuf (mk_typ t, false) }
+      { node = EBufNull; typ = TBuf (mk_typ t, false); meta = [] }
 
   | I.EApp (I.ETApp (I.EQualified ( [ "LowStar"; "Monotonic"; "Buffer" ], "is_null"), [ t; _; _ ]), [ e ])
   | I.EApp (I.ETApp (I.EQualified ( [ "Steel"; "Reference" ], "is_null"), [ t ]), [ e ]) ->
       mk (EApp (mk (EPolyComp (K.PEq, TBuf (mk_typ t, false))), [
         mk_expr e;
-        { node = EBufNull; typ = TBuf (mk_typ t, false) }]))
+        { node = EBufNull; typ = TBuf (mk_typ t, false); meta = [] }]))
 
   | I.EApp (e, es) ->
       mk (EApp (mk_expr e, List.map mk_expr es))
@@ -211,22 +211,22 @@ and mk_expr = function
   | I.EAbortS s ->
       mk (EAbort (None, Some s))
   | I.EAbortT (s, t) ->
-      { node = EAbort (Some (mk_typ t), Some s); typ = mk_typ t }
+      { node = EAbort (Some (mk_typ t), Some s); typ = mk_typ t; meta = [] }
   | I.EReturn e ->
       mk (EReturn (mk_expr e))
   | I.EFlat (tname, fields) ->
-      { node = EFlat (mk_fields fields); typ = mk_typ tname }
+      { node = EFlat (mk_fields fields); typ = mk_typ tname; meta = [] }
   | I.EField (tname, e, field) ->
       let e = { (mk_expr e) with typ = mk_typ tname } in
       mk (EField (e, field))
   | I.ETuple es ->
       mk (ETuple (List.map mk_expr es))
   | I.ECons (lid, id, es) ->
-      { node = ECons (id, List.map mk_expr es); typ = mk_typ lid }
+      { node = ECons (id, List.map mk_expr es); typ = mk_typ lid; meta = [] }
   | I.EFun (bs, e, t) ->
       mk (EFun (mk_binders bs, mk_expr e, mk_typ t))
   | I.EComment (before, e, after) ->
-      mk (EComment (before, mk_expr e, after))
+      { (mk_expr e) with meta = [ CommentBefore before; CommentAfter after ] }
   | I.EStandaloneComment s ->
       mk (EStandaloneComment s)
   | I.EAddrOf e ->

lib/Monomorphization.ml

@@ -612,8 +612,8 @@ let functions files =
                     (* binders are the remaining binders after the cg-binders have been eliminated *)
                     let diff = List.length binders - List.length cgs in
                     let _cg_binders, binders = KList.split (List.length cgs + List.length cgs') binders in
-                    let binders = List.map (fun { node; typ } ->
-                      { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)) }
+                    let binders = List.map (fun { node; typ; _ } ->
+                      { node; typ = DeBruijn.(subst_ctn diff cgs (subst_tn ts typ)); meta = [] }
                     ) binders in
                     (* KPrint.bprintf "about to substitute:\n  e=%a\n  cgs=%a\n cgs'=%a\n  ts=%a\n  head type=%a\n%a\n" *)
                     (*   pexpr e *)