Skip to content

Commit

Permalink
remove ecomment
Browse files Browse the repository at this point in the history
  • Loading branch information
msprotz committed Sep 13, 2024
1 parent b9aae02 commit 686aa74
Show file tree
Hide file tree
Showing 11 changed files with 27 additions and 46 deletions.
4 changes: 2 additions & 2 deletions lib/Ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,8 @@ and fields_t =
(ident * (typ * bool)) list

type node_meta =
| NodeComment of string
| CommentBefore of string
| CommentAfter of string

and node_meta' = node_meta [@visitors.opaque] [@@deriving show]

Expand Down Expand Up @@ -288,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

Expand Down
3 changes: 0 additions & 3 deletions lib/AstToCFlat.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
17 changes: 10 additions & 7 deletions lib/AstToCStar.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -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)

Expand Down
2 changes: 0 additions & 2 deletions lib/AstToMiniRust.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1041,8 +1041,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 ->
Expand Down
6 changes: 0 additions & 6 deletions lib/Checker.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down Expand Up @@ -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;
Expand Down
13 changes: 1 addition & 12 deletions lib/Inlining.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion lib/InputAstToAst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -226,7 +226,7 @@ and mk_expr = function
| 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 ->
Expand Down
12 changes: 6 additions & 6 deletions lib/PrintAst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -214,13 +214,13 @@ and print_let_binding (binder, e1) =

and print_expr { node; typ; meta } =
(* print_typ typ ^^ colon ^^ space ^^ parens @@ *)
begin match List.filter_map (function NodeComment s -> Some s (* | _ -> None*) ) meta with
| [] -> empty
| s -> string (String.concat "\n" s) ^^ break1
end ^^
begin match List.filter_map (function CommentBefore s -> Some s | _ -> None) meta,
List.filter_map (function CommentAfter s -> Some s | _ -> None) meta
with
| [], [] -> fun doc -> doc
| s, s' -> fun doc -> surround 2 1 (string (String.concat "\n" s)) doc (string (String.concat "\n" s'))
end @@
match node with
| EComment (s, e, s') ->
surround 2 1 (string s) (print_expr e) (string s')
| EStandaloneComment s ->
surround 2 1 (string "/*") (string s) (string "*/")
| EAny ->
Expand Down
7 changes: 7 additions & 0 deletions lib/Simplify.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1109,6 +1109,9 @@ and hoist_stmt loc e =
| EMatch _ ->
failwith "[hoist_t]: EMatch not properly desugared"

| EComment (s, e, s') ->
mk (EComment (s, hoist_stmt loc e, s'))

| ETuple _ ->
failwith "[hoist_t]: ETuple not properly desugared"

Expand Down Expand Up @@ -1153,6 +1156,10 @@ and hoist_expr loc pos e =
let lhs, e = hoist_expr loc Unspecified e in
lhs, mk (EComment (s, e, s'))

| EComment (s, e, s') ->
let lhs, e = hoist_expr loc Unspecified e in
lhs, mk (EComment (s, e, s'))

| EIgnore e ->
let lhs, e = hoist_expr loc Unspecified e in
lhs, mk (EIgnore e)
Expand Down
4 changes: 0 additions & 4 deletions lib/SimplifyMerge.ml
Original file line number Diff line number Diff line change
Expand Up @@ -304,10 +304,6 @@ let rec merge' (env: env) (u: S.t) (e: expr): S.t * S.t * expr =
let s = closing_binder binder in
KList.reduce S.inter [ d1; d2; d3; d4 ], u, w (EFor (b, e1, s e2, s e3, s e4))

| EComment (s1, e, s2) ->
let d, u, e = merge env u e in
d, u, w (EComment (s1, e, s2))

| EAddrOf e ->
let d, u, e = merge env u e in
d, u, w (EAddrOf e)
Expand Down
3 changes: 0 additions & 3 deletions lib/Structs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -741,9 +741,6 @@ let to_addr is_struct =
| ECast (e, t) ->
w (ECast (to_addr false e, t))

| EComment (s, e, s') ->
w (EComment (s, to_addr false e, s'))

| ESequence _
| ETuple _
| EMatch _
Expand Down

0 comments on commit 686aa74

Please sign in to comment.