From b9185037db1db1c73031ce18eb943bdd7e170cdc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 14 Dec 2006 15:38:40 +0000
Subject: [PATCH] content2Procedural.ml: "Intros+LetTac" ok

---
 .../content_pres/content2Procedural.ml        | 37 +++++++++++++++----
 .../components/grafite/grafiteAstPp.ml        |  6 +--
 helm/software/matita/contribs/prova.ma        |  7 ++++
 3 files changed, 39 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml
index 66a4370f3..99fe8d0b2 100644
--- a/helm/software/components/content_pres/content2Procedural.ml
+++ b/helm/software/components/content_pres/content2Procedural.ml
@@ -39,22 +39,43 @@ let mk_theorem name t =
    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 sep = G.Dot floc in
+   G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), Some sep))
 
+let mk_intros xi ids =
+   let tactic = G.Intros (floc, xi, ids) in
+   mk_tactic tactic
+   
 let mk_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
 
+(* internal functions *******************************************************)
+
+let mk_intros_arg = function
+   | `Declaration {C.dec_name = Some name}
+   | `Hypothesis {C.dec_name = Some name}
+   | `Definition {C.def_name = Some name} -> name 
+   | _ -> assert false
+
+let mk_intros_args pc = List.map mk_intros_arg pc
+
+let rec mk_proof p = 
+   let cmethod = p.C.proof_conclude.C.conclude_method in
+   let cargs = p.C.proof_conclude.C.conclude_args in
+   match cmethod, cargs with
+      | "Intros+LetTac", [C.ArgProof q] -> 
+         let names = mk_intros_args q.C.proof_context in
+	 let num = List.length names in
+	 let text = String.concat " " names in
+	 mk_intros (Some num) [] :: mk_note text :: mk_proof q
+      | _ -> [mk_note (Printf.sprintf "%s %u" cmethod (List.length cargs))] 
+
 (* 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]
+      | `Def (C.Const, t, `Proof ({C.proof_name = Some name} as p)) ->
+           mk_theorem name t :: mk_proof p
       | _ -> assert false 
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index efc007886..0704863f5 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -33,7 +33,7 @@ let tactical_terminator = ""
 let tactic_terminator = tactical_terminator
 let command_terminator = tactical_terminator
 
-let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
+let pp_idents idents = "(" ^ String.concat " " idents ^ ")"
 
 let pp_reduction_kind ~term_pp = function
   | `Normalize -> "normalize"
@@ -298,9 +298,9 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
-  | Note (_,str) -> sprintf "(* %s *)" str
+  | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
-      sprintf "(** %s. **)" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
+      sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
 
 let pp_statement ~term_pp ~lazy_term_pp ~obj_pp =
   function
diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 67c4b1ebf..93b195990 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -14,5 +14,12 @@
 
 set "baseuri" "cic:/matita/tests".
 
+alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)".
+alias id "pr0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1)".
+alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
+alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)".
+
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
-- 
2.39.2