First commit of our future proof-assistant/proof-improver (???)

[helm.git] / helm / gTopLevel / sequentPp.ml

diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml
new file mode 100644 (file)
index 0000000..8fbb78b
--- /dev/null
+++ b/helm/gTopLevel/sequentPp.ml
@@ -0,0 +1,68 @@
+module TextualPp =
+ struct
+  (* It also returns the pretty-printing context! *)
+  let print_context ctx =
+   let module P = ProofEngine in
+    let print_name =
+     function
+        Cic.Name n -> n
+      | Cic.Anonimous -> "_"
+    in
+     List.fold_right
+      (fun i env ->
+        match i with
+           (P.Declaration,n,t) ->
+             print_endline (print_name n ^ ":" ^ CicPp.pp t env) ;
+             flush stdout ;
+             n::env
+         | (P.Definition,n,t) ->
+             print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ;
+             flush stdout ;
+             n::env
+      ) ctx []
+  ;;
+
+  exception NotImplemented;;
+
+  let print_sequent (context,goal) =
+   let module P = ProofEngine in
+    print_newline () ;
+    let pretty_printer_env_of_context =
+     print_context context
+    in
+    print_endline "----------------------" ;
+    print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout
+  ;;
+ end
+;;
+
+module XmlPp =
+ struct
+  let print_sequent (context,goal) =
+   let module X = Xml in
+    X.xml_nempty "Sequent" []
+     (let final_s,final_env =
+       (List.fold_right
+         (fun (b,n,t) (s,env) ->
+           [< s ;
+              X.xml_nempty
+               (match b with
+                   ProofEngine.Definition  -> "Definition"
+                 | ProofEngine.Declaration -> "Declaration"
+               ) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
+               (Cic2Xml.print_term
+                 (UriManager.uri_of_string "cic:/dummy.con")
+                 (let (acic,_,_) = Cic2acic.acic_of_cic_env env t in acic)) ;
+           >],(n::env)
+         ) context ([<>],[])
+       )
+      in
+       [< final_s ;
+          Xml.xml_nempty "Goal" []
+           (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con")
+             (let (acic,_,_) = Cic2acic.acic_of_cic_env final_env goal in acic))
+       >]
+     )
+  ;;
+ end
+;;