Skip to content

Commit

Permalink
Merge pull request #498 from FStarLang/protz_debug
Browse files Browse the repository at this point in the history 
Print locally bound variable names in debug
  • Loading branch information
@msprotz
msprotz authored Nov 21, 2024
2 parents 0784079 + 9f99d2c commit 8233a90
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 55 deletions.
4 changes: 2 additions & 2 deletions lib/Monomorphization.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ module NameGen = struct

let print_extra = function
| Cg cgs -> separate_map underscore print_cg cgs
| Expr (n_cgs, cgs, _) -> separate_map underscore print_expr (fst (KList.split n_cgs cgs))
| Expr (n_cgs, cgs, _) -> separate_map underscore (print_expr empty_env) (fst (KList.split n_cgs cgs))

(* An informative comment in case the short name option is chosen. *)
let gen_comment original_name ts extra =
Expand Down Expand Up @@ -139,7 +139,7 @@ module NameGen = struct
match extra with
| Expr (n_cgs, es, _bs) ->
string "(expr)" ^/^ string (string_of_int n_cgs) ^/^ string "const generics, followed by trait method impl arguments" ^^ hardline ^^
separate_map hardline print_expr es
separate_map hardline (print_expr empty_env) es
| Cg cgs ->
string "(type) const generics" ^^ hardline ^^ separate_map hardline print_cg cgs
));
Expand Down
117 changes: 64 additions & 53 deletions lib/PrintAst.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,14 @@ let print_app_ empty f head g arguments =
let print_app x = print_app_ "😱" x
let print_cg_app x = print_app_ "□" x

type env = string list
let push env x = x.node.name :: env
let push_n = List.fold_left push
let lookup env n =
(* Need to print open terms for debug *)
Option.value ~default:"" (List.nth_opt env n)
let empty_env = []

let rec print_decl = function
| DFunction (cc, flags, n_cg, n, typ, name, binders, body) ->
let cc = match cc with Some cc -> print_cc cc ^^ break1 | None -> empty in
Expand All @@ -36,7 +44,7 @@ let rec print_decl = function
parens_with_nesting (
separate_map (comma ^^ break 1) print_binder binders
) ^^ colon ^/^ print_typ typ) ^/^ braces_with_nesting (
print_expr body
print_expr empty_env body
)

| DExternal (cc, flags, n_cg, n, name, typ, _) ->
Expand All @@ -49,7 +57,9 @@ let rec print_decl = function

| DGlobal (flags, name, n, typ, expr) ->
print_comment flags ^^
print_flags flags ^^ langle ^^ int n ^^ rangle ^^ print_typ typ ^^ space ^^ string (string_of_lident name) ^^ space ^^ equals ^/^ nest 2 (print_expr expr)
print_flags flags ^^ langle ^^ int n ^^ rangle ^^ print_typ typ ^^ space
^^ string (string_of_lident name) ^^ space ^^ equals ^/^ nest 2
(print_expr empty_env expr)

| DType (name, flags, n_cg, n, def) ->
let args = List.init n (fun i -> string ("t" ^ string_of_int i)) in
Expand Down Expand Up @@ -211,9 +221,9 @@ and print_lifetime = function
| Eternal -> string "eternal"
| Heap -> string "heap"

and print_let_binding (binder, e1) =
and print_let_binding env (binder, e1) =
group (group (string "let" ^/^ print_binder binder ^/^ equals) ^^
jump (print_expr e1))
jump (print_expr env e1))

and print_node_meta meta =
begin match List.filter_map (function CommentBefore s -> Some s | _ -> None) meta,
Expand All @@ -223,7 +233,7 @@ and print_node_meta meta =
| s, s' -> fun doc -> surround 2 1 (string (String.concat "\n" s)) doc (string (String.concat "\n" s'))
end

and print_expr { node; typ; meta } =
and print_expr env { node; typ; meta } =
(* print_typ typ ^^ colon ^^ space ^^ parens @@ *)
print_node_meta meta @@
match node with
Expand All @@ -236,9 +246,9 @@ and print_expr { node; typ; meta } =
string "$abort<" ^^ t ^^ string ">" ^^
(match s with None -> empty | Some s -> string " (" ^^ string s ^^ string ")")
| EIgnore e ->
print_app string "ignore" print_expr [ e ]
print_app string "ignore" (print_expr env) [ e ]
| EBound v ->
at ^^ int v
string (lookup env v) ^^ at ^^ int v
| EOpen (name, _) ->
bang ^^ string name
| EQualified lident ->
Expand All @@ -250,48 +260,48 @@ and print_expr { node; typ; meta } =
| EString s ->
dquote ^^ string s ^^ dquote
| EApp (e, es) ->
print_app print_expr e print_expr es
print_app (print_expr env) e (print_expr env) es
| ETApp (e, es, es', ts) ->
print_cg_app (fun (e, ts) ->
print_app print_expr e (fun t -> group (langle ^/^ print_typ t ^/^ rangle)) ts
) (e, ts) (fun e -> brackets (brackets (print_expr e))) (es @ es')
print_app (print_expr env) e (fun t -> group (langle ^/^ print_typ t ^/^ rangle)) ts
) (e, ts) (fun e -> brackets (brackets (print_expr env e))) (es @ es')
| ELet (binder, e1, e2) ->
group (print_let_binding (binder, e1) ^/^ string "in") ^^ hardline ^^
group (print_expr e2)
group (print_let_binding env (binder, e1) ^/^ string "in") ^^ hardline ^^
group (print_expr (push env binder) e2)
| EIfThenElse (e1, e2, e3) ->
string "if" ^/^ print_expr e1 ^/^ string "then" ^^
jump (print_expr e2) ^/^ string "else" ^^
jump (print_expr e3)
string "if" ^/^ print_expr env e1 ^/^ string "then" ^^
jump (print_expr env e2) ^/^ string "else" ^^
jump (print_expr env e3)
| ESequence es ->
separate_map (semi ^^ hardline) (fun e -> group (print_expr e)) es
separate_map (semi ^^ hardline) (fun e -> group (print_expr env e)) es
| EAssign (e1, e2) ->
group (print_expr e1 ^/^ string ":=") ^^ (jump (print_expr e2))
group (print_expr env e1 ^/^ string ":=") ^^ (jump (print_expr env e2))
| EBufCreate (l, e1, e2) ->
print_lifetime l ^^ space ^^
print_app string "newbuf" print_expr [e1; e2]
print_app string "newbuf" (print_expr env) [e1; e2]
| EBufRead (e1, e2) ->
parens (print_expr e1 ^^ colon ^^ print_typ e1.typ) ^^ lbracket ^^ print_expr e2 ^^ rbracket
parens (print_expr env e1 ^^ colon ^^ print_typ e1.typ) ^^ lbracket ^^ print_expr env e2 ^^ rbracket
| EBufWrite (e1, e2, e3) ->
print_expr e1 ^^ (*colon ^^ print_typ e1.typ ^^*) lbracket ^^ print_expr e2 ^^ rbracket ^/^
string "<-" ^/^ print_expr e3
print_expr env e1 ^^ (*colon ^^ print_typ e1.typ ^^*) lbracket ^^ print_expr env e2 ^^ rbracket ^/^
string "<-" ^/^ print_expr env e3
| EBufSub (e1, e2) ->
print_app string "subbuf" print_expr [e1; e2]
print_app string "subbuf" (print_expr env) [e1; e2]
| EBufDiff (e1, e2) ->
print_app string "diffbuf" print_expr [e1; e2]
print_app string "diffbuf" (print_expr env) [e1; e2]
| EBufBlit (e1, e2, e3, e4, e5) ->
print_app string "blitbuf" print_expr [e1; e2; e3; e4; e5]
print_app string "blitbuf" (print_expr env) [e1; e2; e3; e4; e5]
| EBufFill (e1, e2, e3) ->
print_app string "fillbuf" print_expr [e1; e2; e3 ]
print_app string "fillbuf" (print_expr env) [e1; e2; e3 ]
| EBufFree e ->
print_app string "freebuf" print_expr [ e ]
print_app string "freebuf" (print_expr env) [ e ]
| EMatch (c, e, branches) ->
let c = if c = Unchecked then string "UNCHECKED " else empty in
group (c ^^ string "match" ^/^ print_expr e ^/^ string "with") ^^
jump ~indent:0 (print_branches branches)
group (c ^^ string "match" ^/^ print_expr env e ^/^ string "with") ^^
jump ~indent:0 (print_branches env branches)
| EOp (o, w) ->
string "(" ^^ print_op o ^^ string "," ^^ print_width w ^^ string ")"
| ECast (e, t) ->
parens_with_nesting (print_expr e ^^ langle ^^ colon ^/^ print_typ t)
parens_with_nesting (print_expr env e ^^ langle ^^ colon ^/^ print_typ t)
| EPopFrame ->
string "pop_frame"
| EPushFrame ->
Expand All @@ -301,50 +311,51 @@ and print_expr { node; typ; meta } =
| EBreak ->
string "break"
| EReturn e ->
string "return" ^/^ (nest 2 (print_expr e))
string "return" ^/^ (nest 2 (print_expr env e))
| EFlat fields ->
braces_with_nesting (separate_map break1 (fun (name, expr) ->
let name = match name with Some name -> string name | None -> empty in
group (name ^/^ equals ^/^ print_expr expr ^^ semi)
group (name ^/^ equals ^/^ print_expr env expr ^^ semi)
) fields) ^^ colon ^/^ group (print_typ typ)
| EField (expr, field) ->
parens_with_nesting (print_expr expr) ^^ dot ^^ string field
parens_with_nesting (print_expr env expr) ^^ dot ^^ string field
| EWhile (e1, e2) ->
string "while" ^^ langle ^^ print_typ typ ^^ rangle ^/^ parens_with_nesting (print_expr e1) ^/^
braces_with_nesting (print_expr e2)
string "while" ^^ langle ^^ print_typ typ ^^ rangle ^/^ parens_with_nesting (print_expr env e1) ^/^
braces_with_nesting (print_expr env e2)
| EFor (binder, e1, e2, e3, e4) ->
let env1 = push env binder in
string "for" ^/^ parens_with_nesting (
print_let_binding (binder, e1) ^^
print_let_binding env (binder, e1) ^^
semi ^/^
separate_map (semi ^^ break1) print_expr [ e2; e3 ]) ^/^
braces_with_nesting (print_expr e4)
separate_map (semi ^^ break1) (print_expr env1) [ e2; e3 ]) ^/^
braces_with_nesting (print_expr env1 e4)
| EBufCreateL (l, es) ->
print_lifetime l ^/^
string "newbuf" ^/^ braces_with_nesting (flow (comma ^^ break1) (List.map print_expr es))
string "newbuf" ^/^ braces_with_nesting (flow (comma ^^ break1) (List.map (print_expr env)es))
| ECons (ident, es) ->
string ident ^/^
if List.length es > 0 then
parens_with_nesting (separate_map (comma ^^ break1) print_expr es) ^^ colon ^/^ print_typ typ
parens_with_nesting (separate_map (comma ^^ break1) (print_expr env) es) ^^ colon ^/^ print_typ typ
else
empty ^^ colon ^/^ print_typ typ
| ETuple es ->
parens_with_nesting (separate_map (comma ^^ break1) print_expr es)
parens_with_nesting (separate_map (comma ^^ break1) (print_expr env) es)
| EEnum lid ->
string (string_of_lident lid)
| ESwitch (e, branches) ->
string "switch" ^^ space ^^ print_expr e ^/^ braces_with_nesting (
string "switch" ^^ space ^^ print_expr env e ^/^ braces_with_nesting (
separate_map hardline (fun (lid, e) ->
string "case" ^^ space ^^ print_case lid ^^ colon ^^
nest 2 (hardline ^^ print_expr e)
nest 2 (hardline ^^ print_expr env e)
) branches)
| EFun (binders, body, t) ->
string "fun" ^/^ parens_with_nesting (
separate_map (comma ^^ break 1) print_binder binders
) ^/^ colon ^^ group (print_typ t) ^/^ braces_with_nesting (
print_expr body
print_expr (push_n env binders) body
)
| EAddrOf e ->
ampersand ^^ parens_with_nesting (print_expr e)
ampersand ^^ parens_with_nesting (print_expr env e)
| EPolyComp (c, t) ->
parens_with_nesting (print_poly_comp c ^^ comma ^^ space ^^ print_typ t)
| EBufNull ->
Expand All @@ -365,16 +376,16 @@ and print_case = function
underscore


and print_branches branches =
separate_map (break 1) (fun b -> group (print_branch b)) branches
and print_branches env branches =
separate_map (break 1) (fun b -> group (print_branch env b)) branches

and print_branch (binders, pat, expr) =
and print_branch env (binders, pat, expr) =
group (bar ^^ space ^^
lambda ^/^
group (separate_map (comma ^^ break 1) print_binder binders) ^^
dot ^^ space ^/^
group (print_pat pat ^^ space ^^ arrow)
) ^/^ jump ~indent:4 (print_expr expr)
) ^/^ jump ~indent:4 (print_expr (push_n env binders) expr)

and print_pat p =
(* print_typ p.typ ^^ colon ^^ space ^^ *)
Expand Down Expand Up @@ -409,7 +420,7 @@ let print_files = print_files print_decl
module Ops = struct
let print_cgs = separate_map (comma ^^ space) print_cg
let print_typs = separate_map (comma ^^ space) print_typ
let print_exprs = separate_map (comma ^^ space) print_expr
let print_exprs = separate_map (comma ^^ space) (print_expr empty_env)
let print_lidents = separate_map (comma ^^ space) print_lident

let ploc = printf_of_pprint Loc.print_location
Expand All @@ -420,10 +431,10 @@ module Ops = struct
let pcg = printf_of_pprint print_cg
let pcgs = printf_of_pprint print_cgs
let pptyp = printf_of_pprint_pretty print_typ
let pexpr = printf_of_pprint print_expr
let pexpr = printf_of_pprint (print_expr empty_env)
let pbind = printf_of_pprint print_binder
let pexprs = printf_of_pprint print_exprs
let ppexpr = printf_of_pprint_pretty print_expr
let ppexpr = printf_of_pprint_pretty (print_expr empty_env)
let plid = printf_of_pprint print_lident
let plids = printf_of_pprint print_lidents
let pplid = printf_of_pprint_pretty print_lident
Expand All @@ -435,8 +446,8 @@ module Ops = struct
let ppop = printf_of_pprint_pretty print_op
let ppat = printf_of_pprint print_pat
let pppat = printf_of_pprint_pretty print_pat
let plb = printf_of_pprint print_let_binding
let pplb = printf_of_pprint_pretty print_let_binding
let plb = printf_of_pprint (print_let_binding empty_env)
let pplb = printf_of_pprint_pretty (print_let_binding empty_env)
let plbs buf lbs = List.iter (fun lb -> plb buf lb; Buffer.add_string buf " ") lbs
let pplbs buf lbs = List.iter (fun lb -> pplb buf lb; Buffer.add_string buf "\n") lbs
end
Expand Down

0 comments on commit 8233a90

Please sign in to comment.