diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml index 95f598ec56eb2f67323d05174dad1bf835be7407..b8c5854a739645e686cf7a00456dcb174a65088e 100644 --- a/src/plugins/wp/ProofEngine.ml +++ b/src/plugins/wp/ProofEngine.ml @@ -198,6 +198,7 @@ let head t = match t.head with | Some n -> n.goal let tree n = proof ~main:n.tree let goal n = n.goal + let stats n = n.stats let tree_context t = Wpo.get_context t.main let node_context n = Wpo.get_context n.goal diff --git a/src/plugins/wp/wpApi.mli b/src/plugins/wp/wpApi.mli index c39609bc14ce88c74ac7f991a8bb28a04f21f981..0a81123b9756c04070aef31722516a844e5f4ead 100644 --- a/src/plugins/wp/wpApi.mli +++ b/src/plugins/wp/wpApi.mli @@ -26,4 +26,7 @@ val package : Server.Package.package +module Goal : Server.Data.S with type t = Wpo.t +module Node : Server.Data.S with type t = ProofEngine.node + (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml index 1afc661e52dacaffc9f85476cdaf2b763de35880..77cdd5338eadd06161bdc0fd374c5bc6bfbfa1cb 100644 --- a/src/plugins/wp/wpTipApi.ml +++ b/src/plugins/wp/wpTipApi.ml @@ -31,7 +31,6 @@ module S = Server.States module Md = Markdown module AST = Server.Kernel_ast -let () = ignore WpApi.package let package = P.package ~plugin:"wp" ~name:"tip" ~title:"WP Interactive Prover" () @@ -120,16 +119,59 @@ let () = Wpo.add_cleared_hook let registry = PRINTER.get () in Hashtbl.clear registry) -let printer (node : ProofEngine.node) : printer = +let printer (wpo : Wpo.t) : printer = let registry = PRINTER.get () in - let wpo = ProofEngine.goal node in try Hashtbl.find registry wpo.po_gid with Not_found -> let pp = new printer () in Hashtbl.add registry wpo.po_gid pp ; pp (* -------------------------------------------------------------------------- *) +(* --- Printer Requests --- *) +(* -------------------------------------------------------------------------- *) -let () = (*TODO*) ignore package -let () = (*TODO*) ignore printer +let signal = R.signal ~package ~name:"sequent" ~descr:(Md.plain "Updated TIP") + +let flags (type a) tags : a R.input = + (module struct + type t = a + let jtype = P.Junion (List.map (fun (tg,_) -> P.Jtag tg) tags) + let of_json js = List.assoc (Json.string js) tags + end) + +let iformat : Plang.iformat R.input = + flags [ "dec", `Dec ; "hex", `Hex ; "bin", `Bin ] + +let rformat : Plang.rformat R.input = + flags [ "ratio", `Ratio ; "float", `Float ; "double", `Double ] + +let () = + let printSequent = R.signature ~output:(module D.Jtext) () in + let get_node = R.param printSequent ~name:"node" + ~descr:(Md.plain "Proof Node") (module WpApi.Node) in + let get_indent = R.param_opt printSequent ~name:"indent" + ~descr:(Md.plain "Number of identation spaces") (module D.Jint) in + let get_margin = R.param_opt printSequent ~name:"margin" + ~descr:(Md.plain "Maximial text width") (module D.Jint) in + let get_iformat = R.param_opt printSequent ~name:"iformat" + ~descr:(Md.plain "Integer constants format") iformat in + let get_rformat = R.param_opt printSequent ~name:"rformat" + ~descr:(Md.plain "Real constants format") rformat in + R.register_sig ~package + ~kind:`EXEC + ~name:"printSequent" + ~descr:(Md.plain "Pretty-print the associated node in its current state") + ~signals:[signal] printSequent + begin fun rq () -> + let node = get_node rq in + let indent = get_indent rq in + let margin = get_margin rq in + let tree = ProofEngine.tree node in + let main = ProofEngine.main tree in + let goal = ProofEngine.goal node in + let pp = printer main in + Option.iter pp#set_iformat (get_iformat rq) ; + Option.iter pp#set_rformat (get_rformat rq) ; + D.jpretty ?indent ?margin pp#pp_goal goal + end (* -------------------------------------------------------------------------- *)