diff --git a/spectec/src/backend-interpreter/manual.ml b/spectec/src/backend-interpreter/manual.ml index cf6c0d59df..87f6bfb214 100644 --- a/spectec/src/backend-interpreter/manual.ml +++ b/spectec/src/backend-interpreter/manual.ml @@ -95,10 +95,10 @@ let call_ref = (accE (fi, dotP ("MODULE", "module"))) )); letI (ff, frameE (Some m, f)); - enterI (ff, listE ([caseE (("FRAME_", ""), [])]), + enterI (ff, listE ([caseE (("FRAME_", "admininstr"), [])]), [ letI (ll, labelE (m, listE [])); - enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (("LABEL_", ""), [])])), []); + enterI (ll, catE (iterE (instr, ["instr"], List), listE ([caseE (("LABEL_", "admininstr"), [])])), []); ] ); ], []); @@ -211,7 +211,7 @@ let return_instrs_of_instantiate config = [ enterI ( frameE (Some (numE 0L), frame), - listE ([ caseE (("FRAME_", ""), []) ]), rhs + listE ([ caseE (("FRAME_", "admininstr"), []) ]), rhs ); returnI (Some (tupE [ store; varE "mm" ])) ] @@ -221,7 +221,7 @@ let return_instrs_of_invoke config = letI (varE "k", lenE (iterE (varE "t_2", ["t_2"], List))); enterI ( frameE (Some (varE "k"), frame), - listE ([caseE (("FRAME_", ""), [])]), rhs + listE ([caseE (("FRAME_", "admininstr"), [])]), rhs ); popI (iterE (varE "val", ["val"], ListN (varE "k", None))); returnI (Some (iterE (varE "val", ["val"], ListN (varE "k", None)))) diff --git a/spectec/src/backend-latex/render.mli b/spectec/src/backend-latex/render.mli index b1387f7749..752c39b83a 100644 --- a/spectec/src/backend-latex/render.mli +++ b/spectec/src/backend-latex/render.mli @@ -11,12 +11,6 @@ val with_syntax_decoration : bool -> env -> env val with_rule_decoration : bool -> env -> env -(* Utilities *) - -(* TODO: this should not be public *) -val expand_exp : arg list -> int ref -> exp -> exp - - (* Generators *) val render_atom : env -> atom -> string diff --git a/spectec/src/backend-prose/dune b/spectec/src/backend-prose/dune index 11be215b16..4bcb8bbc21 100644 --- a/spectec/src/backend-prose/dune +++ b/spectec/src/backend-prose/dune @@ -8,6 +8,5 @@ gen render macro - hint symbol) ) diff --git a/spectec/src/backend-prose/gen.mli b/spectec/src/backend-prose/gen.mli new file mode 100644 index 0000000000..1284c07ac0 --- /dev/null +++ b/spectec/src/backend-prose/gen.mli @@ -0,0 +1,2 @@ +val gen_string : Il.Ast.script -> Al.Ast.algorithm list -> string +val gen_prose : Il.Ast.script -> Al.Ast.algorithm list -> Prose.prose diff --git a/spectec/src/backend-prose/hint.ml b/spectec/src/backend-prose/hint.ml deleted file mode 100644 index 827b02e9ac..0000000000 --- a/spectec/src/backend-prose/hint.ml +++ /dev/null @@ -1,105 +0,0 @@ -open Util.Source - -module KMap = Map.Make(struct - type t = string * string - let compare (a1, a2) (b1, b2) = - let c1 = String.compare a1 b1 in - let c2 = String.compare a2 b2 in - if c1 = 0 then c2 else c1 -end) -module FMap = Map.Make(String) - -(* Environment *) - -type env = - { - render_latex: Backend_latex.Render.env; - show_kwds: El.Ast.exp KMap.t ref; - show_funcs: El.Ast.exp FMap.t ref; - } - -(* Extracting Hint from DSL *) -(* Assume each syntax variant / function have at most one "show" hint. *) - -let extract_show_hint (hint: El.Ast.hint) = - if hint.hintid.it = "show" then [ hint.hintexp ] else [] - -let extract_typcase_hint = function - | El.Ast.Nl -> None - | El.Ast.Elem (atom, _, hints) -> (match atom.it with - | El.Ast.Atom id -> - let show_hints = List.concat_map extract_show_hint hints in - (match show_hints with - | hint :: _ -> Some (id, hint) - | [] -> None) - | _ -> None) - -let extract_typ_hints typ = - match typ.it with - | El.Ast.CaseT (_, _, typcases, _) -> List.filter_map extract_typcase_hint typcases - | _ -> [] - -let extract_syntax_hints show_kwds def = - match def.it with - | El.Ast.SynD (id, subid, _, typ, _) -> - let id = - if subid.it = "" then id.it - else id.it ^ "-" ^ subid.it - in - let show_hints = extract_typ_hints typ in - List.fold_left - (fun acc (variant, hint) -> - KMap.add (variant, id) hint acc) - show_kwds show_hints - | _ -> show_kwds - -let extract_func_hints show_funcs def = - match def.it with - | El.Ast.DecD (id, _, _, hints) -> - let show_hints = List.concat_map extract_show_hint hints in - (match show_hints with - | hint :: _ -> FMap.add id.it hint show_funcs - | [] -> show_funcs) - | _ -> show_funcs - -(* Environment Construction *) - -let env render_latex el = - let show_kwds = List.fold_left extract_syntax_hints KMap.empty el in - let show_funcs = List.fold_left extract_func_hints FMap.empty el in - { - render_latex; - show_kwds = ref show_kwds; - show_funcs = ref show_funcs - } - -(* Hint Application *) - -let apply_hint env args hint = - (* TODO Placeholder El args with "!!!", to be expanded into the El hint exp. *) - let placeholder = - let text = (El.Ast.TextE "!!!") $ no_region in - let arg = El.Ast.ExpA text in - (ref arg) $ no_region - in - let placeholders = List.init (List.length args) (fun _ -> placeholder) in - (* Expand hint exp with placeholder args, then manipulate the rendered hint exp by string replacements. *) - try - let hint_expanded = Backend_latex.Render.expand_exp placeholders (ref 0) hint in - let hint_rendered = Backend_latex.Render.render_exp env.render_latex hint_expanded in - let hint_replaced = - let placeholder = Str.regexp (Backend_latex.Render.render_arg env.render_latex placeholder) in - List.fold_left - (fun hint_rendered arg -> Str.replace_first placeholder arg hint_rendered) - hint_rendered args - in - Some hint_replaced - with _ -> None - -let apply_kwd_hint env kwd args = - let hint = KMap.find_opt kwd !(env.show_kwds) in - Option.bind hint (apply_hint env args) - -let apply_func_hint env fname args = - let hint = FMap.find_opt fname !(env.show_funcs) in - Option.bind hint (apply_hint env args) diff --git a/spectec/src/backend-prose/macro.ml b/spectec/src/backend-prose/macro.ml index 5ae023242c..cf836e1f35 100644 --- a/spectec/src/backend-prose/macro.ml +++ b/spectec/src/backend-prose/macro.ml @@ -31,6 +31,10 @@ type env = sections: string Map.t ref; } +(* Environment Lookup *) + +let find_section env s = Map.mem s !(env.sections) + (* Macro Generation *) let macro_template = {| @@ -84,10 +88,10 @@ let gen_macro_kwd env syntax kwd = gen_macro_rule ~note:syntax env header font kwd let gen_macro_kwds env kwds = - Map.fold + Symbol.Map.fold (fun syntax variants skwd -> let terminals, _ = variants in - let svariants = Set.fold + let svariants = Symbol.Set.fold (fun kwd svariants -> let svariant = gen_macro_kwd env syntax kwd in svariants ^ svariant ^ "\n") @@ -106,15 +110,17 @@ let gen_macro_func env fname = gen_macro_rule env header font fname let gen_macro_funcs env funcs = - Set.fold + Symbol.Set.fold (fun fname sfunc -> let sword = gen_macro_func env fname in sfunc ^ sword ^ "\n") funcs "" let gen_macro' env (symbol: Symbol.env) = - let skwd = gen_macro_kwds env !(symbol.kwds) in - let sfunc = gen_macro_funcs env !(symbol.funcs) in + let kwds = Symbol.kwds symbol in + let skwd = gen_macro_kwds env kwds in + let funcs = Symbol.funcs symbol in + let sfunc = gen_macro_funcs env funcs in macro_template ^ ".. syntax\n.. ------\n\n" ^ skwd @@ -168,9 +174,8 @@ let env inputs outputs = let sections = if check_rst outputs then parse_section inputs outputs else Map.empty in { sections = ref sections; } -(* Environment Lookup *) -let find_section env s = Map.mem s !(env.sections) +(* Macro generation *) let macro_kwd env kwd = let variant, syntax = kwd in diff --git a/spectec/src/backend-prose/macro.mli b/spectec/src/backend-prose/macro.mli new file mode 100644 index 0000000000..1ec06333cc --- /dev/null +++ b/spectec/src/backend-prose/macro.mli @@ -0,0 +1,19 @@ +open Al.Ast + +(* Environment *) + +type env + +val env : string list -> string list -> env + + +(* Lookups *) + +val find_section : env -> string -> bool + + +(* Macro Generation *) + +val macro_kwd : env -> kwd -> string * string +val macro_func : env -> id -> string * string +val gen_macro : env -> Symbol.env -> unit diff --git a/spectec/src/backend-prose/print.ml b/spectec/src/backend-prose/print.ml index 561d67bd7b..1f0db0bafb 100644 --- a/spectec/src/backend-prose/print.ml +++ b/spectec/src/backend-prose/print.ml @@ -3,6 +3,7 @@ open Prose open Printf (* Helpers *) + let string_of_opt prefix stringifier suffix = function | None -> "" | Some x -> prefix ^ stringifier x ^ suffix @@ -81,30 +82,3 @@ let string_of_def = function | Algo algo -> string_of_algorithm algo let string_of_prose prose = List.map string_of_def prose |> String.concat "\n" - -(* Structured string *) - -let string_of_structured_instr = function - | LetI _ -> "LetI(...)" - | CmpI _ -> "CmpI(...)" - | MustValidI (e1, e2, eo) -> - "MustValidI (" - ^ structured_string_of_expr e1 - ^ ", " - ^ structured_string_of_expr e2 - ^ ", " - ^ "(" ^ string_of_opt "" structured_string_of_expr "" eo ^ ")" - ^ ")" - | MustMatchI (e1, e2) -> - "MustMatchI (" - ^ structured_string_of_expr e1 - ^ ", " - ^ structured_string_of_expr e2 - ^ ")" - | IsValidI e_opt -> - "IsValidI" ^ string_of_opt " (" structured_string_of_expr ")" e_opt - | IfI _ -> "IfI(...)" - | ForallI _ -> "ForallI(...)" - | EquivI _ -> "EquivI ..." - | YetI s -> "YetI (" ^ s ^ ")" - diff --git a/spectec/src/backend-prose/print.mli b/spectec/src/backend-prose/print.mli new file mode 100644 index 0000000000..40066b4789 --- /dev/null +++ b/spectec/src/backend-prose/print.mli @@ -0,0 +1,5 @@ +open Prose + +val string_of_instr : instr -> string +val string_of_def : def -> string +val string_of_prose : prose -> string diff --git a/spectec/src/backend-prose/render.ml b/spectec/src/backend-prose/render.ml index d3bab957dc..ddb69945bc 100644 --- a/spectec/src/backend-prose/render.ml +++ b/spectec/src/backend-prose/render.ml @@ -12,9 +12,9 @@ type env = { config: config; prose: prose; + render_latex: Backend_latex.Render.env; symbol: Symbol.env; macro: Macro.env; - hint: Hint.env; } let gen_macro env = @@ -24,10 +24,179 @@ let gen_macro env = let env config inputs outputs render_latex el prose : env = let symbol = Symbol.env el in let macro = Macro.env inputs outputs in - let hint = Hint.env render_latex el in - let env = { config; prose; symbol; macro; hint; } in + let env = { config; prose; render_latex; symbol; macro; } in env +(* Translation from Al exp to El exp *) + +let (let*) = Option.bind + +let al_to_el_unop = function + | Al.Ast.MinusOp -> Some El.Ast.MinusOp + | _ -> None + +let al_to_el_binop = function + | Al.Ast.AddOp -> Some El.Ast.AddOp + | Al.Ast.SubOp -> Some El.Ast.SubOp + | Al.Ast.MulOp -> Some El.Ast.MulOp + | Al.Ast.DivOp -> Some El.Ast.DivOp + | Al.Ast.ExpOp -> Some El.Ast.ExpOp + | _ -> None + +(* TODO hardcoded types for infixop atom, + *) +let al_to_el_infixop op = + let elatom, typ = match op with + | "->" -> Some El.Ast.Arrow, "" + | "X" -> Some (El.Ast.Atom "X"), "shape" + | _ -> None, "" + in + Option.map + (fun elatom -> elatom $$ no_region % ref typ) + elatom + +let al_to_el_kwd (id, typ) = + let elatom = El.Ast.Atom id in + elatom $$ no_region % (ref typ) + +let rec al_to_el_iter iter = match iter with + | Al.Ast.Opt -> Some El.Ast.Opt + | Al.Ast.List -> Some El.Ast.List + | Al.Ast.List1 -> Some El.Ast.List1 + | Al.Ast.ListN (e, id) -> + let* ele = al_to_el_expr e in + let elid = Option.map (fun id -> id $ no_region) id in + Some (El.Ast.ListN (ele, elid)) + +and al_to_el_path pl = + let fold_path p elp = + let elp' = (match p.it with + | Al.Ast.IdxP ei -> + let* elei = al_to_el_expr ei in + Some (El.Ast.IdxP (elp, elei)) + | Al.Ast.SliceP (el, eh) -> + let* elel = al_to_el_expr el in + let* eleh = al_to_el_expr eh in + Some (El.Ast.SliceP (elp, elel, eleh)) + | Al.Ast.DotP kwd -> + let elatom = al_to_el_kwd kwd in + Some (El.Ast.DotP (elp, elatom))) + in + Option.map (fun elp' -> elp' $ no_region) elp' + in + List.fold_left + (fun elp p -> Option.bind elp (fold_path p)) + (Some (El.Ast.RootP $ no_region)) pl + +and al_to_el_expr expr = + let exp' = + match expr.it with + | Al.Ast.NumE i -> + let ei = Int64.to_int i in + let eli = El.Ast.NatE (El.Ast.DecOp, ei) in + Some eli + | Al.Ast.UnE (op, e) -> + let* elop = al_to_el_unop op in + let* ele = al_to_el_expr e in + Some (El.Ast.UnE (elop, ele)) + | Al.Ast.BinE (op, e1, e2) -> + let* elop = al_to_el_binop op in + let* ele1 = al_to_el_expr e1 in + let* ele2 = al_to_el_expr e2 in + Some (El.Ast.BinE (ele1, elop, ele2)) + | Al.Ast.TupE el -> + let* elel = al_to_el_exprs el in + Some (El.Ast.TupE elel) + | Al.Ast.CallE (id, el) -> + let elid = id $ no_region in + let* elel = al_to_el_exprs el in + let elel = List.map + (fun ele -> + let elarg = El.Ast.ExpA ele in + (ref elarg) $ no_region) + elel + in + Some (El.Ast.CallE (elid, elel)) + | Al.Ast.CatE (e1, e2) -> + let* ele1 = al_to_el_expr e1 in + let* ele2 = al_to_el_expr e2 in + Some (El.Ast.SeqE [ ele1; ele2 ]) + | Al.Ast.LenE e -> + let* ele = al_to_el_expr e in + Some (El.Ast.LenE ele) + | Al.Ast.ListE el -> + let* elel = al_to_el_exprs el in + if (List.length elel > 0) then Some (El.Ast.SeqE elel) + else Some (El.Ast.EpsE) + | Al.Ast.AccE (e, p) -> + let* ele = al_to_el_expr e in + (match p.it with + | Al.Ast.IdxP ei -> + let* elei = al_to_el_expr ei in + Some (El.Ast.IdxE (ele, elei)) + | Al.Ast.SliceP (el, eh) -> + let* elel = al_to_el_expr el in + let* eleh = al_to_el_expr eh in + Some (El.Ast.SliceE (ele, elel, eleh)) + | DotP kwd -> + let elatom = al_to_el_kwd kwd in + Some (El.Ast.DotE (ele, elatom))) + | Al.Ast.UpdE (e1, pl, e2) -> + let* ele1 = al_to_el_expr e1 in + let* elp = al_to_el_path pl in + let* ele2 = al_to_el_expr e2 in + Some (El.Ast.UpdE (ele1, elp, ele2)) + | Al.Ast.ExtE (e1, pl, e2, _) -> + let* ele1 = al_to_el_expr e1 in + let* elp = al_to_el_path pl in + let* ele2 = al_to_el_expr e2 in + Some (El.Ast.ExtE (ele1, elp, ele2)) + | Al.Ast.StrE r -> + let* elexpfield = al_to_el_record r in + Some (El.Ast.StrE elexpfield) + | Al.Ast.VarE id | Al.Ast.SubE (id, _) -> + let elid = id $ no_region in + Some (El.Ast.VarE (elid, [])) + | Al.Ast.IterE (e, _, iter) -> + let* ele = al_to_el_expr e in + let* eliter = al_to_el_iter iter in + Some (El.Ast.IterE (ele, eliter)) + | Al.Ast.InfixE (e1, op, e2) -> + let* ele1 = al_to_el_expr e1 in + let* elop = al_to_el_infixop op in + let* ele2 = al_to_el_expr e2 in + Some (El.Ast.InfixE (ele1, elop, ele2)) + | Al.Ast.CaseE (kwd, el) -> + let elatom = al_to_el_kwd kwd in + let ekwd = (El.Ast.AtomE elatom) $ no_region in + let* elel = al_to_el_exprs el in + Some (El.Ast.SeqE ([ ekwd ] @ elel)) + | Al.Ast.OptE (Some e) -> + let* ele = al_to_el_expr e in + Some (ele.it) + | Al.Ast.OptE None -> Some (El.Ast.EpsE) + | _ -> None + in + Option.map (fun exp' -> exp' $ no_region) exp' + +and al_to_el_exprs exprs = + List.fold_left + (fun exps e -> + let* exps = exps in + let* exp = al_to_el_expr e in + Some (exps @ [ exp ])) + (Some []) exprs + +and al_to_el_record record = + Util.Record.fold + (fun kwd e expfield -> + let* expfield = expfield in + let elatom = al_to_el_kwd kwd in + let* ele = al_to_el_expr e in + let elelem = El.Ast.Elem (elatom, ele) in + Some (expfield @ [ elelem ])) + record (Some []) + (* Helpers *) let indent = " " @@ -39,9 +208,9 @@ let rec repeat str num = let math = ":math:" -let render_math s = math ^ sprintf "`%s`" s - -let force_math in_math s = if in_math then s else render_math s +let render_math s = + if (String.length s > 0) then math ^ sprintf "`%s`" s + else s let render_opt prefix stringifier suffix = function | None -> "" @@ -60,18 +229,6 @@ let render_order index depth = | 3 -> alp_idx ^ ")" | _ -> failwith "unreachable" -let render_list stringifier left sep right = function - | [] -> left ^ right - | h :: t -> - let limit = 16 in - let is_long = List.length t > limit in - left - ^ List.fold_left - (fun acc elem -> acc ^ sep ^ stringifier elem) - (stringifier h) (List.filteri (fun i _ -> i <= limit) t) - ^ (if is_long then (sep ^ "...") else "") - ^ right - (* Operators *) let render_prose_cmpop = function @@ -84,18 +241,18 @@ let render_prose_cmpop = function let render_al_unop = function | Al.Ast.NotOp -> "not" - | Al.Ast.MinusOp -> "-" + | Al.Ast.MinusOp -> "minus" let render_al_binop = function | Al.Ast.AndOp -> "and" | Al.Ast.OrOp -> "or" | Al.Ast.ImplOp -> "implies" | Al.Ast.EquivOp -> "is equivanlent to" - | Al.Ast.AddOp -> "+" - | Al.Ast.SubOp -> "-" - | Al.Ast.MulOp -> "\\cdot" - | Al.Ast.DivOp -> "/" - | Al.Ast.ExpOp -> "^" + | Al.Ast.AddOp -> "plus" + | Al.Ast.SubOp -> "minus" + | Al.Ast.MulOp -> "multiplied by" + | Al.Ast.DivOp -> "divided by" + | Al.Ast.ExpOp -> "to the power of" | Al.Ast.EqOp -> "is" | Al.Ast.NeOp -> "is not" | Al.Ast.LtOp -> "is less than" @@ -103,316 +260,184 @@ let render_al_binop = function | Al.Ast.LeOp -> "is less than or equal to" | Al.Ast.GeOp -> "is greater than or equal to" -(* Names and Iters *) - -(* assume Names and Iters are always embedded in math blocks *) - -let rec render_name name = match String.index_opt name '_' with - | Some idx -> - let base = String.sub name 0 idx in - let subscript = String.sub name (idx + 1) ((String.length name) - idx - 1) in - base ^ "_{" ^ subscript ^ "}" - | _ -> name - -and render_kwd env kwd = match Symbol.narrow_kwd env.symbol kwd with - | Some kwd -> - let lhs, rhs = Macro.macro_kwd env.macro kwd in - if env.config.macros then lhs else rhs - | None -> render_name (Al.Print.string_of_kwd kwd) - -and render_funcname env fname = - if Symbol.find_func env.symbol fname - then ( - let lhs, rhs = Macro.macro_func env.macro fname in - if env.config.macros then lhs else rhs - ) - else ( - let escape acc c = - if c = '.' then acc ^ "{.}" - else if c = '_' then acc ^ "\\_" - else acc ^ (String.make 1 c) - in - String.fold_left escape "" fname - ) +(* Names *) -let rec render_iter env = function - | Al.Ast.Opt -> "^?" - | Al.Ast.List -> "^\\ast" - | Al.Ast.List1 -> "^{+}" - | Al.Ast.ListN (expr, None) -> "^{" ^ render_expr env true expr ^ "}" - | Al.Ast.ListN (expr, Some name) -> - "^{(" ^ render_name name ^ "<" ^ render_expr env true expr ^ ")}" +let render_kwd env kwd = + let elatom = al_to_el_kwd kwd in + let satom = Backend_latex.Render.render_atom env.render_latex elatom in + render_math satom -and render_iters env iters = List.map (render_iter env) iters |> List.fold_left (^) "" (* Expressions and Paths *) -and render_expr env in_math expr = +(* Invariant: All AL expressions fall into one of the three categories: + 1. EL-like expression, only containing EL subexpressions + 2. AL-only expression, possibly containing EL subexpressions + 3. pseudo-EL-like expression, containing at least one AL-only subexpression *) + +(* Category 1 is translated to EL then rendered by the Latex backend *) + +let rec render_expr env expr = match al_to_el_expr expr with + | Some exp -> + (* embedded math blocks cannot have line-breaks *) + let newline = Str.regexp "\n" in + let sexp = Backend_latex.Render.render_exp env.render_latex exp in + let sexp = Str.global_replace newline "" sexp in + render_math sexp + | None -> render_expr' env expr + +(* Categories 2 and 3 are rendered by the prose backend, + yet EL subexpressions are still rendered by the Latex backend *) + +and render_expr' env expr = match expr.it with - | Al.Ast.NumE i -> - let si = Int64.to_string i in - if in_math then si else render_math si - | Al.Ast.BoolE b -> - string_of_bool b - | Al.Ast.UnE (MinusOp, e) -> - let se = render_expr env in_math e in - let s = sprintf "-%s" se in - force_math in_math s - | Al.Ast.UnE (NotOp, { it = Al.Ast.IsCaseOfE (e, c); _ }) -> - sprintf "%s is not of the case %s" - (render_expr env in_math e) - (render_math (render_kwd env c)) + | Al.Ast.BoolE b -> string_of_bool b + | Al.Ast.UnE (NotOp, { it = Al.Ast.IsCaseOfE (e, kwd); _ }) -> + let se = render_expr env e in + let skwd = render_math (render_kwd env kwd) in + sprintf "%s is not of the case %s" se skwd | Al.Ast.UnE (NotOp, { it = Al.Ast.IsDefinedE e; _ }) -> - sprintf "%s is not defined" (render_expr env in_math e) + let se = render_expr env e in + sprintf "%s is not defined" se | Al.Ast.UnE (NotOp, { it = Al.Ast.IsValidE e; _ }) -> - sprintf "%s is not valid" (render_expr env in_math e) + let se = render_expr env e in + sprintf "%s is not valid" se | Al.Ast.UnE (op, e) -> - sprintf "%s %s" (render_al_unop op) (render_expr env in_math e) + let sop = render_al_unop op in + let se = render_expr env e in + sprintf "%s %s" sop se | Al.Ast.BinE (op, e1, e2) -> let sop = render_al_binop op in - let se1 = render_expr env true e1 in - let se2 = render_expr env true e2 in - let s = - (match op with - | AddOp | SubOp | MulOp | DivOp | ExpOp -> - sprintf "{%s} %s {%s}" se1 sop se2 - | _ -> - sprintf "%s \\textrm{ %s } %s" se1 sop se2) - in - force_math in_math s - | Al.Ast.TupE el -> - let sel = render_list (render_expr env true) "(" "~" ")" el in - if in_math then sel else render_math sel - | Al.Ast.CallE (fn, es) -> - let sfn = render_funcname env fn in - let ses = List.map (render_expr env true) es in - let sdefault = sprintf "%s(%s)" sfn (String.concat ", " ses) in - let shint = - if Symbol.find_func env.symbol fn - then Hint.apply_func_hint env.hint fn ses - else None - in - let s = Option.value shint ~default:sdefault in - force_math in_math s - (* TODO a better way to flatten single-element list? *) - | Al.Ast.CatE ({ it = Al.Ast.ListE e1; _ }, { it = Al.Ast.ListE e2; _ }) when List.length e1 = 1 && List.length e2 = 1 -> - let se1 = render_expr env true (List.hd e1) in - let se2 = render_expr env true (List.hd e2) in - let s = sprintf "%s~%s" se1 se2 in - force_math in_math s - | Al.Ast.CatE ({ it = Al.Ast.ListE e1; _ }, e2) when List.length e1 = 1 -> - let se1 = render_expr env true (List.hd e1) in - let se2 = render_expr env true e2 in - let s = sprintf "%s~%s" se1 se2 in - force_math in_math s - | Al.Ast.CatE (e1, { it = Al.Ast.ListE e2; _ }) when List.length e2 = 1 -> - let se1 = render_expr env true e1 in - let se2 = render_expr env true (List.hd e2) in - let s = sprintf "%s~%s" se1 se2 in - force_math in_math s - | Al.Ast.CatE (e1, e2) -> - let se1 = render_expr env true e1 in - let se2 = render_expr env true e2 in - let s = sprintf "%s~%s" se1 se2 in - force_math in_math s - | Al.Ast.LenE e -> - let se = render_expr env true e in - if in_math then "|" ^ se ^ "|" else "the length of " ^ render_math se - | Al.Ast.ArityE e -> sprintf "the arity of %s" (render_expr env in_math e) + let se1 = render_expr env e1 in + let se2 = render_expr env e2 in + sprintf "%s %s %s" se1 sop se2 + | Al.Ast.UpdE (e1, ps, e2) -> + let se1 = render_expr env e1 in + let sps = render_paths env ps in + let se2 = render_expr env e2 in + sprintf "%s with %s replaced by %s" se1 sps se2 + | Al.Ast.ExtE (e1, ps, e2, dir) -> + let se1 = render_expr env e1 in + let sps = render_paths env ps in + let se2 = render_expr env e2 in + (match dir with + | Al.Ast.Front -> sprintf "%s with %s prepended by %s" se1 sps se2 + | Al.Ast.Back -> sprintf "%s with %s appended by %s" se1 sps se2) + | Al.Ast.IterE (e, ids, iter) when al_to_el_expr e = None -> + let se = render_expr env e in + let ids = Al.Al_util.tupE (List.map Al.Al_util.varE ids) in + let loop = Al.Al_util.iterE (ids, [], iter) in + let sloop = render_expr env loop in + sprintf "for all %s, %s" sloop se + | Al.Ast.ArityE e -> + let se = render_expr env e in + sprintf "the arity of %s" se | Al.Ast.GetCurLabelE -> "the current label" | Al.Ast.GetCurFrameE -> "the current frame" | Al.Ast.GetCurContextE -> "the current context" | Al.Ast.FrameE (None, e2) -> - sprintf "the activation of %s" (render_expr env in_math e2) + let se2 = render_expr env e2 in + sprintf "the activation of %s" se2 | Al.Ast.FrameE (Some e1, e2) -> - sprintf "the activation of %s with arity %s" (render_expr env in_math e2) - (render_expr env in_math e1) - | Al.Ast.ListE el -> - let sel = - if List.length el > 0 then - render_list (render_expr env true) "" "~" "" el - else - "\\epsilon" - in - if in_math then sel else render_math sel - | Al.Ast.AccE (e, p) -> - let se = render_expr env true e in - let sp = render_path env p in - let s = sprintf "%s%s" se sp in - force_math in_math s - | Al.Ast.ExtE (e1, ps, e2, dir) -> - let se1 = render_expr env in_math e1 in - let sps = render_paths env in_math ps in - let se2 = render_expr env in_math e2 in - if in_math then - (match dir with - | Al.Ast.Front -> sprintf "\\{%s~%s\\}~\\bigoplus~%s" sps se2 se1 - | Al.Ast.Back -> sprintf "%s~\\bigoplus~\\{%s~%s\\}" se1 sps se2) - else - (match dir with - | Al.Ast.Front -> sprintf "%s with %s prepended by %s" se1 sps se2 - | Al.Ast.Back -> sprintf "%s with %s appended by %s" se1 sps se2) - | Al.Ast.UpdE (e1, ps, e2) -> - sprintf "%s with %s replaced by %s" - (render_expr env in_math e1) - (render_paths env in_math ps) - (render_expr env in_math e2) - | Al.Ast.StrE r -> - let sr = - Util.Record.fold - (fun k v acc -> acc @ [ render_kwd env k ^ "~" ^ render_expr env true v ]) - r [] - in - let sr = render_list Fun.id "\\{" ", " "\\}" sr in - if in_math then sr else render_math sr - | Al.Ast.ContE e -> sprintf "the continuation of %s" (render_expr env in_math e) + let se1 = render_expr env e1 in + let se2 = render_expr env e2 in + sprintf "the activation of %s with arity %s" se2 se1 + | Al.Ast.ContE e -> + let se = render_expr env e in + sprintf "the continuation of %s" se | Al.Ast.LabelE (e1, e2) -> - sprintf "the label whose arity is %s and whose continuation is %s" (render_expr env in_math e1) (render_expr env in_math e2) - | Al.Ast.VarE n | Al.Ast.SubE (n, _) -> - let sn = render_name n in - if in_math then sn else render_math sn - | Al.Ast.IterE ({ it = Al.Ast.VarE n; _ }, _, iter) -> - let sn = render_name n in - let siter = render_iter env iter in - let s = sprintf "{%s}{%s}" sn siter in - force_math in_math s - | Al.Ast.IterE (e, _, iter) -> - let se = render_expr env true e in - let siter = render_iter env iter in - let s = sprintf "{(%s)}{%s}" se siter in - force_math in_math s - | Al.Ast.InfixE (e1, infix, e2) -> - let se1 = render_expr env true e1 in - (* Hardcoded rendering of infix *) - let sinfix = - match infix with - | "->" -> "\\to" - | "X" -> "\\times" - | _ -> infix - in - let se2 = render_expr env true e2 in - let s = sprintf "%s %s %s" se1 sinfix se2 in - force_math in_math s - | Al.Ast.CaseE (kwd, es) -> - let skwd = render_kwd env kwd in - let ses = List.map (render_expr env true) es in - let sdefault = - if List.length ses = 0 then skwd - else sprintf "%s~%s" skwd (String.concat "~" ses) - in - let shint = - Option.map - (fun kwd_narrow -> Hint.apply_kwd_hint env.hint kwd_narrow ses) - (Symbol.narrow_kwd env.symbol kwd) - in - let shint = Option.join shint in - let s = Option.value shint ~default:sdefault in - force_math in_math s - | Al.Ast.OptE (Some e) -> - let se = render_expr env true e in - let s = sprintf "{%s}^?" se in - force_math in_math s - | Al.Ast.OptE None -> - let s = "\\epsilon" in - force_math in_math s - (* Assume conditional expressions are always embedded in math blocks. *) + let se1 = render_expr env e1 in + let se2 = render_expr env e2 in + sprintf "the label whose arity is %s and whose continuation is %s" se1 se2 | Al.Ast.ContextKindE (kwd, e) -> - let skwd = render_kwd env kwd in - let se = render_expr env true e in - let s = sprintf "%s\\textrm{ is }%s" se skwd in - force_math in_math s + let skwd = render_math (render_kwd env kwd) in + let se = render_expr env e in + sprintf "%s is %s" se skwd | Al.Ast.IsDefinedE e -> - let se = render_expr env true e in - let s = sprintf "%s\\textrm{ is defined}" se in - force_math in_math s + let se = render_expr env e in + sprintf "%s is defined" se | Al.Ast.IsCaseOfE (e, kwd) -> - let se = render_expr env true e in - let skwd = render_kwd env kwd in - let s = sprintf "%s\\textrm{ is of the case }%s" se skwd in - force_math in_math s + let se = render_expr env e in + let skwd = render_math (render_kwd env kwd) in + sprintf "%s is of the case %s" se skwd | Al.Ast.HasTypeE (e, t) -> - let se = render_expr env true e in - let s = sprintf "\\textrm{the type of }%s\\textrm{ is }%s" se t in - force_math in_math s + let se = render_expr env e in + sprintf "the type of %s is %s" se t | Al.Ast.IsValidE e -> - let se = render_expr env true e in - let s = sprintf "%s\\textrm{ is valid}" se in - force_math in_math s - | Al.Ast.TopLabelE -> - let s = "\\textrm{a label is now on the top of the stack}" in - force_math in_math s - | Al.Ast.TopFrameE -> - let s = "\\textrm{a frame is now on the top of the stack}" in - force_math in_math s + let se = render_expr env e in + sprintf "%s is valid" se + | Al.Ast.TopLabelE -> "a label is now on the top of the stack" + | Al.Ast.TopFrameE -> "a frame is now on the top of the stack" | Al.Ast.TopValueE (Some e) -> - let se = render_expr env true e in - let s = sprintf "\\textrm{a value of value type }%s\\textrm{ is on the top of the stack}" se in - force_math in_math s - | Al.Ast.TopValueE None -> - let s = "\\textrm{a value is on the top of the stack}" in - force_math in_math s + let se = render_expr env e in + sprintf "a value of value type %s is on the top of the stack" se + | Al.Ast.TopValueE None -> "a value is on the top of the stack" | Al.Ast.TopValuesE e -> - let se = render_expr env true e in - let s = sprintf "\\textrm{there are at least }%s\\textrm{ values on the top of the stack}" se in - force_math in_math s + let se = render_expr env e in + sprintf "there are at least %s values on the top of the stack" se | Al.Ast.MatchE (e1, e2) -> - let se1 = render_expr env true e1 in - let se2 = render_expr env true e2 in - let s = sprintf "%s\\textrm{ matches }%s" se1 se2 in - force_math in_math s - | Al.Ast.YetE s -> sprintf "YetE (%s)" s - -(* assume Paths are always embedded in math blocks *) + let se1 = render_expr env e1 in + let se2 = render_expr env e2 in + sprintf "%s matches %s" se1 se2 + | _ -> + let se = Al.Print.string_of_expr expr in + let msg = sprintf "%s was not properly handled\n" se in + Util.Source.error expr.at "prose backend error: " msg and render_path env path = match path.it with - | Al.Ast.IdxP e -> sprintf "[%s]" (render_expr env true e) + | Al.Ast.IdxP e -> + let se = render_expr env e in + let space = if (String.starts_with ~prefix:math se) then " " else "" in + sprintf "the %s%s-th element" (render_expr env e) space | Al.Ast.SliceP (e1, e2) -> - sprintf "[%s : %s]" (render_expr env true e1) (render_expr env true e2) - | Al.Ast.DotP s -> sprintf ".%s" (render_kwd env s) - -and render_paths env in_math paths = - let spaths = List.map (render_path env) paths |> List.fold_left (^) "" in - if in_math then spaths else render_math spaths + let se1 = render_expr env e1 in + let se2 = render_expr env e2 in + sprintf "the slice from %s to %s" se1 se2 + | Al.Ast.DotP kwd -> + sprintf "the field %s" (render_math (render_kwd env kwd)) +and render_paths env paths = + let spaths = List.map (render_path env) paths in + String.concat " of " spaths (* Instructions *) let rec render_prose_instr env depth = function | LetI (e1, e2) -> sprintf "* Let %s be %s." - (render_expr env false e1) - (render_expr env false e2) + (render_expr env e1) + (render_expr env e2) | CmpI (e1, cmpop, e2) -> sprintf "* %s must be %s %s." - (String.capitalize_ascii (render_expr env false e1)) + (String.capitalize_ascii (render_expr env e1)) (render_prose_cmpop cmpop) - (render_expr env false e2) + (render_expr env e2) | MustValidI (e1, e2, e3) -> sprintf "* Under the context %s, %s must be valid%s." - (render_expr env false e1) - (render_expr env false e2) - (render_opt " with type " (render_expr env false) "" e3) + (render_expr env e1) + (render_expr env e2) + (render_opt " with type " (render_expr env) "" e3) | MustMatchI (e1, e2) -> sprintf "* %s must match %s." - (String.capitalize_ascii (render_expr env false e1)) - (render_expr env false e2) + (String.capitalize_ascii (render_expr env e1)) + (render_expr env e2) | IsValidI e -> sprintf "* The instruction is valid%s." - (render_opt " with type " (render_expr env false) "" e) + (render_opt " with type " (render_expr env) "" e) | IfI (c, is) -> sprintf "* If %s,%s" - (render_expr env false c) + (render_expr env c) (render_prose_instrs env (depth + 1) is) | ForallI (e1, e2, is) -> sprintf "* For all %s in %s,%s" - (render_expr env false e1) - (render_expr env false e2) + (render_expr env e1) + (render_expr env e2) (render_prose_instrs env (depth + 1) is) | EquivI (c1, c2) -> sprintf "* %s and %s are equivalent." - (String.capitalize_ascii (render_expr env false c1)) - (render_expr env false c2) + (String.capitalize_ascii (render_expr env c1)) + (render_expr env c2) | YetI s -> sprintf "* YetI: %s." s @@ -425,17 +450,17 @@ and render_prose_instrs env depth instrs = let rec render_al_instr env algoname index depth instr = match instr.it with | Al.Ast.IfI (c, il, []) -> - sprintf "%s If %s, then:%s" (render_order index depth) (render_expr env false c) - (render_al_instrs env algoname (depth + 1) il) + sprintf "%s If %s, then:%s" (render_order index depth) + (render_expr env c) (render_al_instrs env algoname (depth + 1) il) | Al.Ast.IfI (c, il1, [ { it = IfI (inner_c, inner_il1, []); _ } ]) -> let if_index = render_order index depth in let else_if_index = render_order index depth in sprintf "%s If %s, then:%s\n\n%s Else if %s, then:%s" if_index - (render_expr env false c) + (render_expr env c) (render_al_instrs env algoname (depth + 1) il1) (repeat indent depth ^ else_if_index) - (render_expr env false inner_c) + (render_expr env inner_c) (render_al_instrs env algoname (depth + 1) inner_il1) | Al.Ast.IfI (c, il1, [ { it = IfI (inner_c, inner_il1, inner_il2); _ } ]) -> let if_index = render_order index depth in @@ -443,17 +468,19 @@ let rec render_al_instr env algoname index depth instr = let else_index = render_order index depth in sprintf "%s If %s, then:%s\n\n%s Else if %s, then:%s\n\n%s Else:%s" if_index - (render_expr env false c) + (render_expr env c) (render_al_instrs env algoname (depth + 1) il1) (repeat indent depth ^ else_if_index) - (render_expr env false inner_c) + (render_expr env inner_c) (render_al_instrs env algoname (depth + 1) inner_il1) (repeat indent depth ^ else_index) (render_al_instrs env algoname (depth + 1) inner_il2) | Al.Ast.IfI (c, il1, il2) -> let if_index = render_order index depth in let else_index = render_order index depth in - sprintf "%s If %s, then:%s\n\n%s Else:%s" if_index (render_expr env false c) + sprintf "%s If %s, then:%s\n\n%s Else:%s" + if_index + (render_expr env c) (render_al_instrs env algoname (depth + 1) il1) (repeat indent depth ^ else_index) (render_al_instrs env algoname (depth + 1) il2) @@ -463,50 +490,57 @@ let rec render_al_instr env algoname index depth instr = | Al.Ast.EitherI (il1, il2) -> let either_index = render_order index depth in let or_index = render_order index depth in - sprintf "%s Either:%s\n\n%s Or:%s" either_index + sprintf "%s Either:%s\n\n%s Or:%s" + either_index (render_al_instrs env algoname (depth + 1) il1) (repeat indent depth ^ or_index) (render_al_instrs env algoname (depth + 1) il2) | Al.Ast.AssertI c -> - let vref = if Macro.find_section env.macro ("valid-" ^ algoname) then ":ref:`validation `" else "validation" in - sprintf "%s Assert: Due to %s, %s." (render_order index depth) vref (render_expr env false c) + let vref = + if Macro.find_section env.macro ("valid-" ^ algoname) then + ":ref:`validation `" + else + "validation" + in + sprintf "%s Assert: Due to %s, %s." (render_order index depth) + vref (render_expr env c) | Al.Ast.PushI e -> sprintf "%s Push %s to the stack." (render_order index depth) - (render_expr env false e) + (render_expr env e) (* TODO hardcoded for PopI on label or frame by raw string *) | Al.Ast.PopI ({ it = Al.Ast.VarE s; _ }) when s = "the label" || s = "the frame" -> sprintf "%s Pop %s from the stack." (render_order index depth) s | Al.Ast.PopI e -> sprintf "%s Pop %s from the stack." (render_order index depth) - (render_expr env false e) + (render_expr env e) | Al.Ast.PopAllI e -> sprintf "%s Pop all values %s from the stack." (render_order index depth) - (render_expr env false e) + (render_expr env e) | Al.Ast.LetI (n, e) -> - sprintf "%s Let %s be %s." (render_order index depth) (render_expr env false n) - (render_expr env false e) + sprintf "%s Let %s be %s." (render_order index depth) (render_expr env n) + (render_expr env e) | Al.Ast.TrapI -> sprintf "%s Trap." (render_order index depth) | Al.Ast.NopI -> sprintf "%s Do nothing." (render_order index depth) | Al.Ast.ReturnI e_opt -> sprintf "%s Return%s." (render_order index depth) - (render_opt " " (render_expr env false) "" e_opt) + (render_opt " " (render_expr env) "" e_opt) | Al.Ast.EnterI (e1, e2, il) -> sprintf "%s Enter %s with label %s:%s" (render_order index depth) - (render_expr env false e1) (render_expr env false e2) + (render_expr env e1) (render_expr env e2) (render_al_instrs env algoname (depth + 1) il) | Al.Ast.ExecuteI e -> - sprintf "%s Execute %s." (render_order index depth) (render_expr env false e) + sprintf "%s Execute %s." (render_order index depth) (render_expr env e) | Al.Ast.ExecuteSeqI e -> - sprintf "%s Execute the sequence %s." (render_order index depth) (render_expr env false e) + sprintf "%s Execute the sequence %s." (render_order index depth) (render_expr env e) | Al.Ast.PerformI (n, es) -> - sprintf "%s Perform %s." (render_order index depth) (render_expr env false (Al.Ast.CallE (n, es) $ instr.at)) + sprintf "%s Perform %s." (render_order index depth) (render_expr env (Al.Ast.CallE (n, es) $ no_region)) | Al.Ast.ExitI -> render_order index depth ^ " Exit current context." | Al.Ast.ReplaceI (e1, p, e2) -> sprintf "%s Replace %s with %s." (render_order index depth) - (render_expr env false (Al.Ast.AccE (e1, p) $ e1.at)) (render_expr env false e2) + (render_expr env (Al.Ast.AccE (e1, p) $ no_region)) (render_expr env e2) | Al.Ast.AppendI (e1, e2) -> sprintf "%s Append %s to the %s." (render_order index depth) - (render_expr env false e2) (render_expr env false e1) + (render_expr env e2) (render_expr env e1) | Al.Ast.YetI s -> sprintf "%s YetI: %s." (render_order index depth) s and render_al_instrs env algoname depth instrs = @@ -527,10 +561,10 @@ let render_kwd_title env kwd params = else if name = "FRAME" then ("FRAME_", syntax) else kwd in - render_expr env false (Al.Ast.CaseE (kwd, params) $ no_region) + render_expr env (Al.Ast.CaseE (kwd, params) $ no_region) let render_funcname_title env fname params = - render_expr env false (Al.Ast.CallE (fname, params) $ no_region) + render_expr env (Al.Ast.CallE (fname, params) $ no_region) let render_pred env name params instrs = let (pname, syntax) = name in diff --git a/spectec/src/backend-prose/render.mli b/spectec/src/backend-prose/render.mli new file mode 100644 index 0000000000..4e0a870633 --- /dev/null +++ b/spectec/src/backend-prose/render.mli @@ -0,0 +1,19 @@ +open Al.Ast + + +(* Environment *) + +type env + +val env : Config.t -> string list -> string list -> Backend_latex.Render.env -> El.Ast.script -> Prose.prose -> env + + +(* Generators *) + +val gen_macro : env -> unit + +val render_expr : env -> expr -> string +val render_al_instr : env -> id -> int ref -> int -> instr -> string +val render_prose_instr : env -> int -> Prose.instr -> string +val render_def : env -> Prose.def -> string +val render_prose : env -> Prose.prose -> string diff --git a/spectec/src/backend-prose/symbol.ml b/spectec/src/backend-prose/symbol.ml index 212de5478b..c333fa1f1f 100644 --- a/spectec/src/backend-prose/symbol.ml +++ b/spectec/src/backend-prose/symbol.ml @@ -99,6 +99,11 @@ let env el = let funcs = extract_func_kwds el in { kwds = ref kwds; funcs = ref funcs; } +(* Environment Getters *) + +let kwds env = !(env.kwds) +let funcs env = !(env.funcs) + (* Environment Lookup *) let rec narrow_kwd' env nonterminals variant = match nonterminals with diff --git a/spectec/src/backend-prose/symbol.mli b/spectec/src/backend-prose/symbol.mli new file mode 100644 index 0000000000..718775f31b --- /dev/null +++ b/spectec/src/backend-prose/symbol.mli @@ -0,0 +1,26 @@ +open Al.Ast + +(* Set module with string elements *) + +module Set : Set.S with type elt = String.t + +(* Map module with string keys *) + +module Map : Map.S with type key = String.t + + +(* Environment *) + +type env + +val env : El.Ast.script -> env + +val kwds : env -> (Set.t * Set.t) Map.t +val funcs : env -> Set.t + + +(* Lookups *) + +val narrow_kwd : env -> kwd -> (string * string) option + +val find_func : env -> id -> bool diff --git a/spectec/src/il2al/translate.ml b/spectec/src/il2al/translate.ml index 66931e4c3c..f84b393941 100644 --- a/spectec/src/il2al/translate.ml +++ b/spectec/src/il2al/translate.ml @@ -408,7 +408,7 @@ let rec rhs2instrs exp = }) -> [ letI (varE "F", frameE (Some (varE arity.it), varE fname.it)) ~at:at; - enterI (varE "F", listE ([caseE (("FRAME_", ""), [])]), rhs2instrs labelexp) ~at:at; + enterI (varE "F", listE ([caseE (("FRAME_", "admininstr"), [])]), rhs2instrs labelexp) ~at:at; ] (* TODO: Label *) | Ast.CaseE @@ -427,12 +427,12 @@ let rec rhs2instrs exp = | Ast.CatE (valexp, instrsexp) -> [ letI (varE "L", label_expr) ~at:at; - enterI (varE "L", catE (exp2expr instrsexp, listE ([caseE (("LABEL_", ""), [])])), [pushI (exp2expr valexp)]) ~at:at; + enterI (varE "L", catE (exp2expr instrsexp, listE ([caseE (("LABEL_", "admininstr"), [])])), [pushI (exp2expr valexp)]) ~at:at; ] | _ -> [ letI (varE "L", label_expr) ~at:at; - enterI (varE "L", catE(exp2expr instrs_exp2, listE ([caseE (("LABEL_", ""), [])])), []) ~at:at; + enterI (varE "L", catE(exp2expr instrs_exp2, listE ([caseE (("LABEL_", "admininstr"), [])])), []) ~at:at; ]) (* Execute instr *) | Ast.CaseE (Atom atomid, argexp) -> @@ -632,13 +632,13 @@ let rulepr2instrs id exp = (* TODO: Name of f..? *) enterI ( frameE (None, varE "z"), - listE [caseE (("FRAME_", ""), [])], + listE [caseE (("FRAME_", "admininstr"), [])], [ letI (rhs, callE ("eval_expr", [ lhs ])) ] ) ~at:at | "Step_read", [ { it = TupE [ { it = TupE [ _s; f ]; _ }; lhs ]; _ }; rhs] -> enterI ( frameE (None, f), - listE [caseE (("FRAME_", ""), [])], + listE [caseE (("FRAME_", "admininstr"), [])], [ letI (rhs, callE ("eval_expr", [ lhs ])) ] ) ~at:at | "Ref_ok", [_s; ref; rt] ->