diff --git a/src/backend/prep.ml b/src/backend/prep.ml index 35688813..f95b28e7 100644 --- a/src/backend/prep.ml +++ b/src/backend/prep.ml @@ -897,6 +897,21 @@ let expand_enabled_cdot ob print_obl_and_msg ob ( "Proof obligation before `Expr.Action.expand_action_operators`:\n"); let expr = expr_from_obl ob in + (* Print syntax tree if requested. *) + if !Params.dumps_json_ast then begin + let visitor = + object (self: 'self) + inherit [unit] Expr.Visit.json_map + end in + let cx = ((), Deque.empty) in + let json_str = visitor#expr cx expr in + print_string ( + "------------\n\ + JSON output:\n\n" ^ + json_str ^ + "\n\n========\n\n") + end; + (* expand action operators *) let expr: Expr.T.expr = begin if expand_enabled || expand_cdot then begin let cx = Deque.empty in diff --git a/src/expr.mli b/src/expr.mli index 39f9a25f..506eead7 100644 --- a/src/expr.mli +++ b/src/expr.mli @@ -308,6 +308,42 @@ module Visit : sig method rename : ctx -> hyp -> Util.hint -> hyp * Util.hint method renames : ctx -> hyp list -> Util.hint list -> hyp list * Util.hint list end + + val hyps_of_bounds: bounds -> hyp list + + class virtual ['s] json_map: object + method expr: + 's scx -> expr -> string + method sel: + 's scx -> sel -> string + method sequent: + 's scx -> sequent -> string + method defn: + 's scx -> defn -> string + method defns: + 's scx -> defn list -> + 's scx * string + method bounds: 's scx -> bounds -> + 's scx * string + method bound: 's scx -> bound -> + 's scx * string + method exspec: + 's scx -> exspec -> string + method instance: + 's scx -> instance -> string + method hyp: + 's scx -> hyp -> 's scx * string + method hyps: + 's scx -> hyp Deque.dq -> + 's scx * string + method adj: + 's scx -> hyp -> 's scx + method adjs: + 's scx -> hyp list -> 's scx + end + val format_parameter: + Util.hint * shape -> string + val json_of_ast: ctx -> expr -> string end;; module Eq : sig diff --git a/src/expr/e_visit.ml b/src/expr/e_visit.ml index 3817816f..f5e80cb4 100644 --- a/src/expr/e_visit.ml +++ b/src/expr/e_visit.ml @@ -688,3 +688,573 @@ class virtual ['s] map_rename = object (self : 'self) method rename cx hyp name = (hyp, name) end + + +let hyps_of_bounds bounds = + let make_fresh (name, kind, dom) = + Fresh ( + name, Shape_expr, + kind, Unbounded) + @@ name in + List.map make_fresh bounds + + +let arity_of_shape shape = + match shape with + | Shape_expr -> 0 + | Shape_op arity -> + assert (arity > 0); + arity + + +let format_parameter (name, shape) = + let arity = shape + |> arity_of_shape + |> string_of_int in + ("{" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Arity\": " ^ arity ^ + "}") + + +let format_modal_op modal_op = + match modal_op with + | Box -> "[]" + | Dia -> "<>" + + +class virtual ['s] json_map = + object (self: 'self) + + method expr (scx: 's scx) oe = + match oe.core with + | Ix n -> + (* Ix n @@ oe *) + let cx = snd scx in + let hyp = E_t.get_val_from_id cx n in + let opaque = begin match hyp.core with + | Flex name -> name.core + | Fresh (name, _, _, _) -> name.core + | Defn (defn, _, _, _) -> + begin match defn.core with + | Recursive (name, _) + | Operator (name, _) + | Instance (name, _) + | Bpragma (name, _, _) -> + name.core + end + | Fact (expr, _, _) -> + assert false + end in + "{\"OpRef\": \"" ^ opaque ^ "\"}" + | Internal Conj -> + "{\"OpRef\": \"/\\\\\"}" + | Internal Disj -> + "{\"OpRef\": \"\\\\/\"}" + | Internal builtin -> + (* Internal b @@ oe *) + let form = Optable.standard_form builtin in + let opname = form.name in + "{\"OpRef\": \"" ^ opname ^ "\"}" + | Opaque name -> + "{\"OpRef\": \"" ^ name ^ "\"}" + | Bang (expr, sels) -> + let expr = self#expr scx expr in + let sels = List.map (self#sel scx) sels in + let sels = Fmtutil.comma sels in + ("{\"!\": {" ^ + "\"Expr\": " ^ expr ^ + ", " ^ + "\"Selectors\": [" ^ sels ^ + "]}}") + | Lambda (names, expr) -> + let scx = self#adjs scx + (List.map + (fun (v, shp) -> + Fresh ( + v, shp, Unknown, + Unbounded) @@ v) + names) in + let expr = self#expr scx expr in + let names = names + |> List.map format_parameter + |> Fmtutil.comma in + ("{\"Lambda\": " ^ + "\"Parameters\": [" ^ names ^ + "], " ^ + "\"Expr\": " ^ expr ^ + "}}") + | String value -> + "{\"String\": \"" ^ value ^ "\"}" + | Num (m, n) -> + "{\"Number\": [\"" ^ m ^ "\", \"" ^ n ^ "\"]}" + | Apply (op, exprs) -> + let operator = self#expr scx op in + let args = exprs + |> List.map (self#expr scx) + |> Fmtutil.comma + in + ("{\"Apply\": {" ^ + "\"Operator\": " ^ operator ^ + ", " ^ + "\"Operands\": [" ^ args ^ + "]}}") + | Sequent sq -> + let sq = self#sequent scx sq in + "{\"Sequent\": " ^ sq ^ "}" + | With (expr, meth) -> + let expr = self#expr scx expr in + (* TODO: convert `meth` to string *) + "{\"WithMethod\": " ^ expr ^ "}" + | Let (defs, expr) -> + let (scx, defs) = self#defns scx defs in + let expr = self#expr scx expr in + ("{\"LET\": {" ^ + "\"Definitions\": " ^ defs ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | If (e, f, g) -> + let if_ = self#expr scx e in + let then_ = self#expr scx f in + let else_ = self#expr scx g in + ("{\"IF\": {" ^ + "\"If\": " ^ if_ ^ + ", " ^ + "\"THEN\": " ^ then_ ^ + ", " ^ + "\"ELSE\": " ^ else_ ^ + "}}") + | List (op, exprs) -> + let operator = match op with + | And -> "And" + | Or -> "Or" + | Refs -> "Refs" in + let exprs = List.map (self#expr scx) exprs in + let exprs = Fmtutil.comma exprs in + ("{\"Junction\": {" ^ + "\"Operator\": \"" ^ operator ^ + "\", " ^ + "\"Expressions\": [" ^ exprs ^ + "]}}") + | Quant (qtf, bounds, expr) -> + let (scx, bounds) = self#bounds scx bounds in + let expr = self#expr scx expr in + let quantifier = match qtf with + | Forall -> "\\A" + | Exists -> "\\E" in + ("{\"" ^ quantifier ^ "\": {" ^ + "\"Bounds\": " ^ bounds ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Tquant (qtf, vars, expr) -> + let mapper v = Flex v @@ v in + let hyps = List.map mapper vars in + let scx = self#adjs scx hyps in + let expr = self#expr scx expr in + let vars = List.map + (fun nm -> nm.core) vars in + let vars = Fmtutil.comma vars in + let quantifier = match qtf with + | Forall -> "\\AA" + | Exists -> "\\EE" in + ("{\"" ^ quantifier ^ "\": {" ^ + "\"Variables\": " ^ vars ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Choose (name, optdom, expr) -> + let optdom = Option.map + (self#expr scx) optdom in + (* no need for the domain to be + in the context *) + let hyp = Fresh ( + name, Shape_expr, + Constant, Unbounded) @@ name in + let dom = match optdom with + | None -> "" + | Some dom -> dom in + let scx = self#adj scx hyp in + let expr = self#expr scx expr in + ("{\"CHOOSE\": {" ^ + "\"Name\": " ^ name.core ^ + ", " ^ + "\"Domain\": " ^ dom ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | SetSt (name, dom, expr) -> + let dom = self#expr scx dom in + (* no need for the domain to be + in the context *) + let fresh = Fresh ( + name, Shape_expr, + Constant, Unbounded) @@ name in + let scx = self#adj scx fresh in + let expr = self#expr scx expr in + ("{\"SetSt\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Domain\": " ^ dom ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | SetOf (expr, bounds) -> + let (scx, bounds) = self#bounds scx bounds in + let expr = self#expr scx expr in + ("{\"SetOf\": {" ^ + "\"Bounds\": " ^ bounds ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | SetEnum exprs -> + let exprs = exprs + |> List.map (self#expr scx) + |> Fmtutil.comma in + "{\"SetEnum\": [" ^ exprs ^ "]}" + | Fcn (bounds, expr) -> + let (scx, bounds) = self#bounds scx bounds in + let expr = self#expr scx expr in + ("{\"Function\": {" ^ + "\"Bounds\": " ^ bounds ^ + ", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | FcnApp (fcn, exprs) -> + let fcn = self#expr scx fcn in + let exprs = exprs + |> List.map (self#expr scx) + |> Fmtutil.comma in + ("{\"FunctionApplication\": {" ^ + "\"Function\": " ^ fcn ^ + ", " ^ + "\"Expressions\": [" ^ exprs ^ + "]}}") + | Arrow (a, b) -> + let a = self#expr scx a in + let b = self#expr scx b in + ("{\"->\": {" ^ + "\"Domain\": " ^ a ^ + ", " ^ + "\"Codomain\": " ^ b ^ + "}}") + | Product exprs -> + let exprs = exprs + |> List.map (self#expr scx) + |> Fmtutil.comma in + "{\"\\X\": [" ^ exprs ^ "]}" + | Tuple exprs -> + let exprs = exprs + |> List.map (self#expr scx) + |> Fmtutil.comma in + "{\"<<\": [" ^ exprs ^ "]}" + | Rect fields -> + let mapper (s, e) = (s, self#expr scx e) in + let fields = fields + |> List.map mapper + |> List.map (fun (a, b) -> a ^ b) + |> Fmtutil.comma + in + "{\"SetOfRecords\": [" ^ fields ^ "]}" + | Record fields -> + let mapper (s, e) = (s, self#expr scx e) in + let fields = fields + |> List.map mapper + |> List.map (fun (a, b) -> a ^ b) + |> Fmtutil.comma + in + "{\"Record\": [" ^ fields ^ "]}" + | Except (expr, xs) -> + let expr = self#expr scx expr in + let xs = xs + |> List.map (self#exspec scx) + |> Fmtutil.comma in + ("{\"EXCEPT\": {" ^ + "\"Expr\": " ^ expr ^ + ", " ^ + "\"Changes\": " ^ xs ^ + "}}") + | Dot (expr, field) -> + let expr = self#expr scx expr in + ("{\"Dot\": {" ^ + "\"Expr\": " ^ expr ^ + ", " ^ + "\"Field\": \"" ^ field ^ + "\"}}") + | Sub (modal_op, action, subscript) -> + let operator = format_modal_op modal_op in + let action = self#expr scx action in + let subscript = self#expr scx subscript in + ("{\"Subscripted\": {" ^ + "\"Operator\": \"" ^ operator ^ + "\", " ^ + "\"Action\": " ^ action ^ + ", " ^ + "\"Subscript\": " ^ subscript ^ + "}}") + | Tsub (modal_op, action, subscript) -> + let operator = format_modal_op modal_op in + let action = self#expr scx action in + let subscript = self#expr scx subscript in + ("{\"TemporalSubscripted\": {" ^ + "\"Operator\": \"" ^ operator ^ + "\", " ^ + "\"Action\": " ^ action ^ + ", " ^ + "\"Subscript\": " ^ subscript ^ + "}}") + | Fair (fop, expr, subscript) -> + let operator = match fop with + | Weak -> "WF_" + | Strong -> "SF_" in + let expr = self#expr scx expr in + let subscript = self#expr scx subscript in + ("{\"Fairness\": {" ^ + "\"Operator\": \"" ^ operator ^ + "\", " ^ + "\"Action\": " ^ expr ^ + ", " ^ + "\"Subscript\": " ^ subscript ^ + "}}") + | Case (arms, other) -> + let mapper (e, f) = ( + self#expr scx e, self#expr scx f) in + let arms = arms + |> List.map mapper + |> List.map (fun (a, b) -> a ^ b) + |> Fmtutil.comma + in + let other = Option.map + (self#expr scx) other in + let other = match other with + | Some other -> other + | None -> "" in + ("{\"CASE\": {" ^ + "\"Arms\": [" ^ arms ^ + "], " ^ + "\"Other\": " ^ other ^ + "}}") + | At b -> + "\"@\"" + | Parens (expr, pf) -> + let expr = self#expr scx expr in + begin match pf.core with + | Syntax -> + "{\"(\": " ^ expr ^ "}" + | Nlabel (name, args) -> + let args = args + |> List.map (fun x -> x.core) + |> Fmtutil.comma + in + ("{\"::\": " ^ + "\"Expr\": " ^ expr ^ + ", " ^ + "\"Label\": " ^ name ^ + ", " ^ + "\"Args\": " ^ args ^ + "}") + | Xlabel (name, []) -> + ("{\"::\": " ^ + "\"Expr\": " ^ expr ^ + "\"Label\": " ^ name ^ + "}") + | Xlabel _ -> + failwith "the parser does not \ + give this case as output" + end + + method sel scx selector = + match selector with + | Sel_inst args -> + let args = List.map + (self#expr scx) args in + "[" ^ Fmtutil.comma args ^ "]" + | Sel_lab (label, args) -> + let args = List.map + (self#expr scx) args in + ("{\"Label\": \"" ^ + label ^ "\", " ^ + "\"Arguments\": [" ^ + (Fmtutil.comma args) ^ + "]}") + | _ -> failwith "unimplemented" + + method sequent scx sq = + let (scx, hyps) = self#hyps + scx sq.context in + let active = self#expr + scx sq.active in + ("{\"Sequent\": {" ^ + "\"Hypotheses\": [" ^ hyps ^ + "], " ^ + "\"Goal\": " ^ active ^ + "}}") + + method defn scx df = + match df.core with + | Recursive (name, shape) -> + ("{\"Recursive\": \"" ^ + (format_parameter (name, shape)) ^ "}") + | Operator (name, expr) -> + let expr = self#expr scx expr in + ("{\"==\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Instance (name, inst) -> + let inst = self#instance scx inst in + ("{\"==\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ inst ^ + "}}") + | Bpragma(name, expr, pragma) -> + (* TODO: pragma info *) + let expr = self#expr scx expr in + ("{\"==\": {\"" ^ + "\"Name\": " ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}}") + + method defns scx = function + | [] -> (scx, "") + | df :: dfs -> + let def = self#defn scx df in + let defn = Defn ( + df, User, Visible, Local) @@ df in + let scx = self#adj scx defn in + let (scx, defs) = self#defns scx dfs in + let defstr = def ^ ", " ^ defs in + (scx, defstr) + + method bounds scx bounds = + let hyps = hyps_of_bounds bounds in + let scx = self#adjs scx hyps in + let mapper (name, kind, dom) = + match dom with + | Domain expr -> + let expr = self#expr scx expr in + ("{\"Bound\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Ditto -> + ("{\"Bound\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Ditto\": \"true\"}") + | No_domain -> + ("{\"Bound\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\"}}") in + let bounds = + bounds + |> List.map mapper + |> Fmtutil.comma in + (scx, bounds) + + method bound scx b = + self#bounds scx [b] + + method exspec scx (trail, res) = + let do_trail = function + | Except_dot name -> + "{\".\": \"" ^ name ^ "\"}" + | Except_apply expr -> + let expr = self#expr scx expr in + "{\"[\": " ^ expr ^ "}" + in + let trail = List.map do_trail trail in + let trail = Fmtutil.join ", " trail in + let expr = self#expr scx res in + ("{\"Change\": {" ^ + "\"Trail\": [" ^ trail ^ + "], " ^ + "\"Expr\": " ^ expr ^ + "}}") + + method instance scx inst = + let step scx name = + let fresh = Fresh ( + name, Shape_expr, + Unknown, Unbounded) @@ name in + self#adj scx fresh in + let scx = List.fold_left + step scx inst.inst_args in + let mapper (name, expr) = + let expr = self#expr scx expr in + name.core ^ " <- " ^ expr in + let inst_sub = List.map + mapper inst.inst_sub in + let inst_sub = Fmtutil.comma inst_sub in + ("{\"INSTANCE\": {" ^ + "\"ModuleName\": \"" ^ inst.inst_mod ^ + "\", " ^ + "\"WITH\": " ^ inst_sub ^ + "}}") + + method hyp scx h = + match h.core with + | Fresh (name, shape, loc, dom) -> + let dom = match dom with + | Unbounded -> "" + | Bounded (r, rvis) -> + self#expr scx r + in + let hstr = ( + "{\"Hypothesis\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Domain\": " ^ dom ^ + "}}") in + (self#adj scx h, hstr) + | Flex name -> + let hstr = ( + "{\"VARIABLE\": \"" ^ + name.core ^ "\"}") in + (self#adj scx h, hstr) + | Defn (df, wd, vis, ex) -> + let df = self#defn scx df in + let hstr = ( + "{\"Hypothesis\": " ^ + df ^ "}") in + (self#adj scx h, hstr) + | Fact (e, vis, tm) -> + let fact = self#expr scx e in + let hstr = ( + "{\"Hypothesis\": " ^ + fact ^ "}") in + (self#adj scx h, hstr) + + method hyps scx hs = + match Dq.front hs with + | None -> (scx, "") + | Some (h, hs) -> + let (scx, h) = self#hyp scx h in + let (scx, hs) = self#hyps scx hs in + match hs with + | "" -> (scx, h) + | _ -> (scx, h ^ ", " ^ hs) + + method adj (s, cx) h = + (s, Dq.snoc cx h) + + method adjs scx = function + | [] -> scx + | h :: hs -> + self#adjs (self#adj scx h) hs +end + + +let json_of_ast cx expr = + let visitor = + object (self: 'self) + inherit [unit] json_map + end in + let scx = ((), cx) in + visitor#expr scx expr diff --git a/src/expr/e_visit.mli b/src/expr/e_visit.mli index 421ac0fb..53c93e63 100644 --- a/src/expr/e_visit.mli +++ b/src/expr/e_visit.mli @@ -69,5 +69,45 @@ class virtual ['s] map_rename : object end val set_to_list: ('a, 'b) Hashtbl.t -> 'a list + val collect_unprimed_vars: ctx -> expr -> string list val collect_primed_vars: ctx -> expr -> string list + + +val hyps_of_bounds: bounds -> hyp list + + +class virtual ['s] json_map: object + method expr: + 's scx -> expr -> string + method sel: + 's scx -> sel -> string + method sequent: + 's scx -> sequent -> string + method defn: + 's scx -> defn -> string + method defns: + 's scx -> defn list -> + 's scx * string + method bounds: 's scx -> bounds -> + 's scx * string + method bound: 's scx -> bound -> + 's scx * string + method exspec: + 's scx -> exspec -> string + method instance: + 's scx -> instance -> string + method hyp: + 's scx -> hyp -> 's scx * string + method hyps: + 's scx -> hyp Deque.dq -> + 's scx * string + method adj: + 's scx -> hyp -> 's scx + method adjs: + 's scx -> hyp list -> 's scx +end + +val format_parameter: + Util.hint * shape -> string +val json_of_ast: ctx -> expr -> string diff --git a/src/module/m_visit.ml b/src/module/m_visit.ml index 25364cc0..2b4eeaa7 100644 --- a/src/module/m_visit.ml +++ b/src/module/m_visit.ml @@ -112,3 +112,188 @@ class map = (cx, mu) end + + + +let format_thm_name name_opt = + match name_opt with + | None -> "" + | Some name -> + "\"Name\": \"" ^ + name.core ^ "\", " + + +class json_map = + (* Map module to JSON string. + + The methods of this class + traverse expressions too. + *) + object (self: 'self) + inherit [unit] Proof.Visit.json_map as super + + method module_units cx tla_module = + let json = [] in + let init = (cx, json) in + let fold (cx, new_module) mu = + let (cx, mu) = self#module_unit cx mu in + let json = List.append json [mu] in + (cx, json) in + let (cx, json) = List.fold_left + fold init tla_module in + let json = Fmtutil.join "" json in + (cx, json) + + method module_unit + (cx: ctx) + (mu: M_t.modunit) = + let (cx, json) = + match mu.core with + | Constants decls -> + self#constants cx decls + | Variables names -> + self#variables cx names + | Recursives decls -> + self#recursives cx decls + | Definition (df, wd, vsbl, local) -> + self#definition cx df wd vsbl local + | Axiom (name, expr) -> + self#axiom cx name expr + | Theorem (name, sq, naxs, pf, orig_pf, summ) -> + self#theorem cx name sq naxs pf orig_pf summ + | Mutate (change, usable) -> + self#mutate cx change usable + | Submod tla_module -> + self#submod cx tla_module + | Anoninst (inst, local) -> + self#anoninst cx inst local + in + (cx, json) + + method constants cx decls = + let json = decls + |> List.map Expr.Visit.format_parameter + |> Fmtutil.comma in + let json = "{\"CONSTANT\": [" ^ json ^ "]}" in + let mu = Constants decls in + let cx = update_cx cx mu in + (cx, json) + + method variables cx names = + let mapper name = "\"" ^ name.core ^ "\"" in + let json = names + |> List.map mapper + |> Fmtutil.comma in + let json = "" ^ json ^ "]}" in + let mu = Variables names in + let cx = update_cx cx mu in + (cx, json) + + method recursives cx decls = + let json = decls + |> List.map Expr.Visit.format_parameter + |> Fmtutil.comma in + let mu = Recursives decls in + let cx = update_cx cx mu in + (cx, json) + + method definition cx df wd vsbl local = + let json = match df.core with + | Recursive (name, shape) -> + failwith "not implemented" + | Operator (name, expr) -> + let scx = ((), cx) in + let expr = self#expr scx expr in + ("{\"==\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Instance (name, inst) -> + let scx = ((), cx) in + let expr = self#instance scx inst in + ("{\"==\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}}") + | Bpragma (name, expr, args) -> + (* TODO: format backend pragmas ? *) + let scx = ((), cx) in + let expr = self#expr scx expr in + ("{\"==\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"Expr\": " ^ expr ^ + "}") in + let mu = Definition (df, wd, vsbl, local) in + let cx = update_cx cx mu in + (cx, json) + + method axiom cx name expr = + let scx = ((), cx) in + let expr_json = self#expr scx expr in + let name_json = format_thm_name name in + let json = ( + "{\"AXIOM\": {" ^ + name_json ^ + "\"Expr\": " ^ expr_json ^ + "}}") in + let mu = Axiom (name, expr) in + let cx = update_cx cx mu in + (cx, json) + + method theorem + cx name sq naxs + proof orig_pf summ = + let scx = ((), cx) in + let name_json = format_thm_name name in + let sq_json = self#sequent scx sq in + let proof_json = + let scx = Expr.Visit.adjs + scx (Deque.to_list sq.context) in + self#proof scx proof in + let json = ( + "{\"THEOREM\": {" ^ + name_json ^ + "\"Expr\": " ^ sq_json ^ + "\"PROOF\": " ^ proof_json ^ + "}}") in + let mu = Theorem ( + name, sq, naxs, proof, + orig_pf, summ) in + let cx = update_cx cx mu in + (cx, json) + + method mutate cx change usable = + (* TODO *) + (cx, "") + + method submod cx tla_module = + let name = tla_module.core.name in + let extendees = tla_module.core.extendees in + let extendees_json = extendees + |> List.map (fun s -> s.core) + |> Fmtutil.comma in + let modunits = tla_module.core.body in + let _, modunits_json = self#module_units + cx modunits in + let json = ( + "{\"MODULE\": {" ^ + "\"Name\": \"" ^ name.core ^ + "\", " ^ + "\"EXTENDS\": [" ^ extendees_json ^ + "], " ^ + "\"Units\": " ^ modunits_json ^ + "}}") in + (cx, json) + + method anoninst cx inst local = + failwith "not implemented" +end + + +let json_of_module cx (tla_module: mule) = + let visitor = new json_map in + let _, json = visitor#submod cx tla_module in + json diff --git a/src/module/m_visit.mli b/src/module/m_visit.mli index c71e98e2..1e50ea1b 100644 --- a/src/module/m_visit.mli +++ b/src/module/m_visit.mli @@ -30,3 +30,8 @@ class map : object method anoninst: ctx -> Expr.T.instance -> export -> ctx * modunit_ end + + + +val json_of_module: + Expr.T.ctx -> M_t.mule -> string diff --git a/src/params.ml b/src/params.ml index e674ebdc..8318fc28 100644 --- a/src/params.ml +++ b/src/params.ml @@ -365,6 +365,9 @@ let () = let set_tlapm_cache_dir dir = cachedir := dir +let dumps_json_ast = ref false + + let keep_going = ref false let suppress_all = ref false let check = ref false diff --git a/src/params.mli b/src/params.mli index b30cc820..90995643 100644 --- a/src/params.mli +++ b/src/params.mli @@ -91,6 +91,7 @@ val suppress_all : bool ref;; val set_smt_logic : string -> unit;; val set_smt_solver : string -> unit;; val set_tlapm_cache_dir : string -> unit;; +val dumps_json_ast: bool ref val printconfig : bool -> string;; val print_config_toolbox : bool -> string;; val check_zenon_ver : unit -> unit;; diff --git a/src/proof.mli b/src/proof.mli index e7743f85..852a0408 100644 --- a/src/proof.mli +++ b/src/proof.mli @@ -103,7 +103,20 @@ module Visit : sig method step : 's scx -> step -> 's scx method usable : 's scx -> usable -> unit end -end;; + class virtual ['s] json_map: object + inherit ['s] Expr.Visit.json_map + method proof: + 's scx -> proof -> string + method steps: + 's scx -> step list -> + 's scx * string + method step: + 's scx -> step -> + 's scx * string + method usable: + 's scx -> usable -> string + end +end module Simplify : sig open Property diff --git a/src/proof/p_visit.ml b/src/proof/p_visit.ml index c39bb3d8..ff60b371 100644 --- a/src/proof/p_visit.ml +++ b/src/proof/p_visit.ml @@ -296,3 +296,302 @@ class virtual ['hyp] iter = object (self : 'self) List.iter usdef us.defs end + + +let bump1 scx = bump scx 1 +let bump2 scx = bump scx 2 +let bump3 scx = bump scx 3 +let bump4 scx = bump scx 4 + + +let format_qed proof = + "{\"QED\": " ^ proof ^ "}" + + +class virtual ['hyp] json_map = + object (self: 'self) + inherit ['hyp] Expr.Visit.json_map + + method proof scx pf = match pf.core with + | Obvious -> + "{\"BY\": \"OBVIOUS\"}" + | Omitted _ -> + "{\"BY\": \"OMITTED\"}" + | By (usables, only) -> + let usables = self#usable + scx usables in + let only = string_of_bool only in + ("{\"BY\": {" ^ + "\"Usables\": " ^ + usables ^ ", " ^ + "\"ONLY\": " ^ only ^ + "}}") + | Steps ([], qed) -> + let qed_proof = self#proof + scx (get_qed_proof qed) in + let qed_json = format_qed + qed_proof in + ("{\"Steps\": [" ^ + qed_json ^ + "]}") + | Steps (inits, qed) -> + let scx, inits = self#steps + scx inits in + let qed_proof = self#proof + scx (get_qed_proof qed) in + let qed_json = format_qed + qed_proof in + ("{\"Steps\": [" ^ + inits ^ ", " ^ + qed_json ^ "]") + | Error _ -> + assert false + + method steps scx = function + | [] -> (scx, "") + | step :: rest -> + let scx, step = self#step + scx step in + let scx, rest = self#steps + scx rest in + let steps = + step ^ ", " ^ rest in + (scx, steps) + + method step scx step_ = + let stepnm = string_of_stepno + (Property.get step_ Props.step) in + let adj_step scx = + Expr.Visit.adj + scx ( + Defn ( + Operator ( + stepnm @@ step_, dummy) + @@ step_, + Proof + Always, + Visible, + Local) @@ step_) in + match step_.core with + | Forget k -> + let k = string_of_int k in + let json = + "{\"FORGET\": " ^ k ^ "}" in + (scx, json) + | Hide usables -> + let usables = self#usable + scx usables in + let hide = ( + "{\"HIDE\": " ^ usables ^ "}") in + (scx, hide) + | Use (usables, only) -> + let n_facts = List.length + usables.facts in + let usables = self#usable + scx usables in + let scx = bump scx n_facts in + let use = ( + "{\"USE\": " ^ usables ^ "}") in + (scx, use) + | Define defs -> + let (scx, defs) = self#defns scx defs in + (scx, defs) + | Assert (sq, proof) -> + let sq_json = self#sequent scx sq in + let proof = + let scx = scx + (* assumptions *) + |> fun scx -> + Expr.Visit.adjs + scx (Deque.to_list sq.context) + (* negation of old goal *) + |> bump1 + (* tuplified form of assertion *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + self#proof scx proof in + let assertion = ( + "{\"Assert\": {" ^ + "\"SEQUENT\": " ^ sq_json ^ ", " ^ + "\"PROOF\": " ^ proof ^ + "}}") in + let scx = scx + (* step name defn. *) + |> adj_step + (* fact that it is true *) + |> bump1 in + (scx, assertion) + | Pcase (expr, proof) -> + let expr = self#expr scx expr in + let proof = + let scx = scx + (* negation of old goal + + new assumption *) + |> bump2 + (* assertion *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + self#proof scx proof in + let pcase = ( + "{\"PROOF_CASE\": {" ^ + "\"Expr\": " ^ expr ^ ", " ^ + "\"PROOF\": " ^ proof ^ + "}}") in + (* update context *) + let scx = scx + (* step name defn *) + |> adj_step + (* fact that it is true *) + |> fun x -> bump1 x in + (scx, pcase) + | Suffices (sq, proof) -> + let sq_json = self#sequent + scx sq in + let proof = + let scx = scx + (* step name definition *) + |> adj_step + (* step name fact *) + |> bump1 in + self#proof scx proof in + let suffices = ( + "{\"SUFFICES\": {" ^ + "\"Sequent\": " ^ sq_json ^ ", " ^ + "\"PROOF\": " ^ proof ^ + "}}") in + let scx = scx + (* assumptions *) + |> fun scx -> + Expr.Visit.adjs + scx (Deque.to_list sq.context) + (* negation of old goal *) + |> bump1 + (* tuplified form of assertion *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + (scx, suffices) + | Have expr -> + let expr = self#expr scx expr in + let have = ( + "{\"HAVE\": " ^ expr ^ "}") in + let scx = scx + (* new assumption + + negation of old goal *) + |> bump2 + (* tuplified form of assertion *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + (scx, have) + | Take bounds -> + (* new declarations *) + let (scx, bounds) = self#bounds + scx bounds in + let take = ( + "{\"TAKE\": " ^ bounds ^ "}") in + let scx = + scx + (* negation of old goal *) + |> bump1 + (* tuplified form of assertion *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + (scx, take) + | Witness exprs -> + let exprs = List.map + (self#expr scx) exprs in + let exprs = Fmtutil.comma exprs in + let witness = ( + "{\"WITNESS\": " ^ exprs ^ "}") in + let scx = scx + (* no new assumptions *) + (* negation of old goal *) + |> bump1 + (* tuplified form of assumption *) + |> adj_step + (* hidden assertion that + the tuple is true *) + |> bump1 in + (scx, witness) + | Pick (bounds, expr, proof) -> + let proof = self#proof + (bump3 scx) proof in + let (bounds_json, expr) = + let (scx, bounds_json) = self#bounds + scx bounds in + let expr = self#expr scx expr in + (bounds_json, expr) in + let pick = ( + "{\"PICK\": {" ^ + "\"Bounds\": " ^ bounds_json ^ + ", " ^ + "\"Expr\": " ^ expr ^ + ", " ^ + "\"PROOF\": " ^ proof ^ + "}}") in + let hyps = Expr.Visit.hyps_of_bounds + bounds in + let scx = scx + (* equivalent existential + for subexprs *) + |> adj_step + (* fact that it is true *) + |> bump1 + (* there is a SUFFICES here + ... so add assumptions for + the new identifiers *) + |> fun scx -> + Expr.Visit.adjs scx hyps + (* + ... then add assumption about + the body of the `PICK` + ... then add the negation of + the old goal + ... then the step name definition + for the `SUFFICES` + ... then the conjunction of the + nondom facts in the `SUFFICES` + *) + |> bump4 in + (* finally, we are in the next step *) + (scx, pick) + + method usable ((_, cx) as scx) usables = + let facts = usables.facts + |> List.map (self#expr scx) + |> Fmtutil.comma in + let mapper def = + match def.core with + | Dvar v -> v + | Dx n -> + let hyp = Expr.T.get_val_from_id cx n in + begin match hyp.core with + | Flex name -> name.core + | Fresh (name, _, _, _) -> name.core + | Defn (defn, _, _, _) -> + begin match defn.core with + | Recursive (name, _) + | Operator (name, _) + | Instance (name, _) + | Bpragma (name, _, _) -> + name.core + end + | Fact (expr, _, _) -> + let scx = Expr.T.scx_front scx n in + self#expr scx expr + end in + let defs = usables.defs + |> List.map mapper + |> Fmtutil.comma in + ("{\"Facts\": [" ^ facts ^ "], " ^ + "\"DEF\": [" ^ defs ^ "]}") +end diff --git a/src/proof/p_visit.mli b/src/proof/p_visit.mli index 18340ff7..5aefd228 100644 --- a/src/proof/p_visit.mli +++ b/src/proof/p_visit.mli @@ -30,3 +30,17 @@ class virtual ['s] iter : object method step : 's scx -> step -> 's scx method usable : 's scx -> usable -> unit end + +class virtual ['s] json_map: object + inherit ['s] Expr.Visit.json_map + method proof: + 's scx -> proof -> string + method steps: + 's scx -> step list -> + 's scx * string + method step: + 's scx -> step -> + 's scx * string + method usable: + 's scx -> usable -> string +end diff --git a/src/tlapm_args.ml b/src/tlapm_args.ml index 21e50c4d..fc7e9a7b 100644 --- a/src/tlapm_args.ml +++ b/src/tlapm_args.ml @@ -222,6 +222,9 @@ let init () = parameter takes precedence over \ the environment variable. If neither \ is specified, the default value is \".tlacache\"."; + "--json-ast", Arg.Set Params.dumps_json_ast, + "Serialize the abstract syntax tree to \ + JSON, and write the output to stdout."; ] in let opts = Arg.align opts in diff --git a/src/util/fmtutil.ml b/src/util/fmtutil.ml index 832c157c..796bdd13 100644 --- a/src/util/fmtutil.ml +++ b/src/util/fmtutil.ml @@ -7,6 +7,47 @@ open Format + +let _join + (separator: string) + (items: string list): + string = + if ((List.length items) < 2) then + failwith + "expected list length >= 2"; + let step accum item = + accum ^ separator ^ item in + let accum = List.hd items in + let tail = List.tl items in + List.fold_left step accum tail + + +let join + (separator: string) + (items: string list): + string = + (* Concatenate `items`. + + Return the concatenation of `items`, + with `separator` inserted in-between. + Example: + + ```ocaml + let items = ["a"; "b"] in + let separator = "," in + let s = join separator items in + assert s = "a, b" + ``` + *) + match items with + | [] -> "" + | [item] -> item + | _ -> _join separator items + + +let comma items = join "," items + + let pp_print_commasp ff () = pp_print_string ff "," ; pp_print_space ff () diff --git a/src/util/fmtutil.mli b/src/util/fmtutil.mli index 9871e7a3..b9beebaa 100644 --- a/src/util/fmtutil.mli +++ b/src/util/fmtutil.mli @@ -9,6 +9,9 @@ open Format +val join: string -> string list -> string +val comma: string list -> string + (** [pp_print_commasp ff ()] is equivalent to [pp_print_string ff "," ; pp_print_space ff ()] *) val pp_print_commasp : formatter -> unit -> unit