we parametrized CicNotationPt.obj on 'term

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

diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index e09ca0b03a3ce124d467061d2db83b4fabd6f19d..8306ea286ed59d8442885814f924dd2a8cdc99b2 100644 (file)
--- a/components/content_pres/content2Procedural.ml
+++ b/components/content_pres/content2Procedural.ml
@@ -23,4 +23,40 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let content2procedural ~ids_to_inner_sorts prefix annterm = []
+module H = HExtlib
+module C = Content
+module G = GrafiteAst
+
+(* grafite ast constructors *************************************************)
+
+let floc = H.dummy_floc
+
+let mk_note str = G.Comment (floc, G.Note (floc, str))
+   
+(* interface functions ******************************************************)
+
+let out_arg = function
+   | C.Aux _       -> "aux"
+   | C.Premise _   -> "premise"
+   | C.Lemma _     -> "lemma"
+   | C.Term _      -> "term"
+   | C.ArgProof _  -> "proof"
+   | C.ArgMethod _ -> "method"
+
+let out_args args = String.concat " " (List.map out_arg args) 
+
+let out_name = function
+   | None     -> ""
+   | Some str -> str
+
+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_note (Printf.sprintf "%s" name)]
+      | _ -> assert false