Huge commit:

[helm.git] / components / content_pres / content2Procedural.ml

diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index e09ca0b03a3ce124d467061d2db83b4fabd6f19d..66a4370f36eca1e79ff702e17a3bb59b3b456e32 100644 (file)
--- a/components/content_pres/content2Procedural.ml
+++ b/components/content_pres/content2Procedural.ml
@@ -23,4 +23,38 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let content2procedural ~ids_to_inner_sorts prefix annterm = []
+module H = HExtlib
+module C = Content
+module G = GrafiteAst
+module N = CicNotationPt
+
+(* grafite ast constructors *************************************************)
+
+let floc = H.dummy_floc
+
+let mk_note str = G.Comment (floc, G.Note (floc, str))
+
+let mk_theorem name t = 
+   let obj = N.Theorem (`Theorem, name, t, None) in
+   G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+
+let mk_tactic tactic =
+   G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))
+
+let mk_exact t =
+   let tactic = G.Exact (floc, t) in
+   mk_tactic tactic
+
+(* interface functions ******************************************************)
+
+let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = 
+   if List.length params > 0 || xmenv <> None then assert false;
+   match obj with
+      | `Def (C.Const, t, `Proof {
+           C.proof_name = Some name; C.proof_context = []; 
+          C.proof_apply_context = []; C.proof_conclude = {
+             C.conclude_conclusion = Some b
+          }
+        }) ->  
+       [mk_theorem name t; mk_exact b]
+      | _ -> assert false