X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcontent_pres%2Fcontent2Procedural.ml;h=5c1ca4c157fdaeb459d9dd2e1f47e450e81c7221;hb=6968ba1ad67ba19e9d794260dc21ba2246d31dac;hp=66a4370f36eca1e79ff702e17a3bb59b3b456e32;hpb=2951babfd31047ac057714130157da2bc36e906e;p=helm.git

diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml
index 66a4370f3..5c1ca4c15 100644
--- a/components/content_pres/content2Procedural.ml
+++ b/components/content_pres/content2Procedural.ml
@@ -24,10 +24,158 @@
  *)
 
 module H = HExtlib
+module U = UriManager
 module C = Content
 module G = GrafiteAst
 module N = CicNotationPt
 
+(* functions to be moved ****************************************************)
+
+let rec list_split n l =
+   if n = 0 then [],l else 
+   let l1, l2 = list_split (pred n) (List.tl l) in
+   List.hd l :: l1, l2
+
+let cont sep a = match sep with 
+   | None     -> a
+   | Some sep -> sep :: a
+
+let list_rev_map_concat map sep a l =
+   let rec aux a = function
+      | []          -> a
+      | [x]         -> map a x
+      | x :: y :: l -> aux (sep :: map a x) (y :: l)  
+   in
+   aux a l
+
+(****************************************************************************)
+
+type name  = string
+type what  = Cic.annterm
+type using = Cic.annterm
+type count = int
+type note  = string
+
+type step = Note of note 
+          | Theorem of name * what * note
+          | Qed of note
+	  | Intros of count option * name list * note
+	  | Elim of what * using option * note
+	  | LetIn of name * what * note
+	  | Apply of what * note
+	  | Exact of what * note
+	  | Branch of step list list * note
+
+(* annterm constructors *****************************************************)
+
+let mk_arel i b = Cic.ARel ("", "", i, b)
+
+(* level 2 transformation ***************************************************)
+
+let mk_name = function
+   | Some name -> name
+   | None      -> "UNUSED" (**)
+
+let mk_intros_arg = function
+   | `Declaration {C.dec_name = name}
+   | `Hypothesis {C.dec_name = name}
+   | `Definition {C.def_name = name}  -> mk_name name 
+   | `Joint _                         -> assert false
+   | `Proof _                         -> assert false
+
+let mk_intros_args pc = List.map mk_intros_arg pc
+
+let split_inductive n tl =
+   let l1, l2 = list_split (int_of_string n) tl in
+   List.hd (List.rev l2), l1
+
+let rec mk_apply_term aref ac ds cargs =
+   let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in
+   let ac, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in
+   ac, ds, Cic.AAppl (aref, List.rev row) 
+
+and mk_delta ac ds = match ac with
+   | p :: ac ->
+      let cmethod = p.C.proof_conclude.C.conclude_method in
+      let cargs = p.C.proof_conclude.C.conclude_args in
+      let capply = p.C.proof_apply_context in
+      let ccont = p.C.proof_context in
+      let caref = p.C.proof_conclude.C.conclude_aref in
+      begin match cmethod with
+         | "Exact"
+         | "Apply" when ccont = [] && capply = [] ->
+	    let ac, ds, what = mk_apply_term caref ac ds cargs in
+	    let name = "PREVIOUS" in
+	    ac, mk_arel 1 name, LetIn (name, what, "") :: ds
+         | _ -> ac, mk_arel 1 "COMPOUND", ds
+      end
+   | _ -> assert false
+
+and mk_arg first (ac, row, ds) = function
+   | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} ->
+      let t = match CicUtil.term_of_uri (U.uri_of_string uri) with
+         | Cic.Const (uri, _) -> Cic.AConst (aref, uri, [])
+	 | Cic.MutConstruct (uri, tno, cno, _) -> 
+	    Cic.AMutConstruct (aref, uri, tno, cno, [])
+         | _ -> assert false
+      in
+      ac, t :: row, ds 
+   | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} -> 
+      ac, mk_arel i b :: row, ds
+   | C.Premise {C.premise_n = None; C.premise_binder = None} -> 
+      let ac, arg, ds = mk_delta ac ds in
+      ac, arg :: row, ds
+   | C.Term t when first -> ac, t :: row, ds
+   | C.Term _            -> ac, Cic.AImplicit ("", None) :: row, ds
+   | C.Premise _         -> assert false
+   | C.ArgMethod _       -> assert false
+   | C.ArgProof _        -> assert false
+   | C.Aux _             -> assert false
+
+let rec mk_proof p =
+   let names = mk_intros_args p.C.proof_context in
+   let count = List.length names in
+   if count > 0 then Intros (Some count, names, "") :: mk_proof_body p
+   else mk_proof_body p
+   
+and mk_proof_body p = 
+   let cmethod = p.C.proof_conclude.C.conclude_method in
+   let cargs = p.C.proof_conclude.C.conclude_args in
+   let capply = p.C.proof_apply_context in
+   let caref = p.C.proof_conclude.C.conclude_aref in
+   match cmethod, cargs with
+      | "Intros+LetTac", [C.ArgProof p] -> mk_proof p 
+      | "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
+	 let whatm, ms = split_inductive n tl in (* actual rx params here *)
+         let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in
+	 let what, qs = List.hd row, mk_subproofs ms in
+	 List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")] 
+      | "Apply", _ -> 
+	 let ac, ds, what = mk_apply_term caref (List.rev capply) [] cargs in
+         let qs = List.map mk_proof ac in
+	 List.rev ds @ [Apply (what, ""); Branch (qs, "")]
+      | _ ->  
+	 let text = 
+	    Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs)
+	 in [Note text] 
+
+and mk_subproofs cargs =
+   let mk_subproof proofs = function
+      | C.ArgProof ({C.proof_name = Some n} as p) -> 
+         (Note n :: mk_proof p) :: proofs
+      | C.ArgProof ({C.proof_name = None} as p)   -> 
+         (Note "" :: mk_proof p) :: proofs
+      | _                                         -> proofs
+   in
+   List.rev (List.fold_left mk_subproof [] cargs)
+
+let mk_obj 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} as p)) ->
+           Theorem (name, t, "") :: mk_proof p @ [Qed ""]
+      | _ -> assert false 
+
 (* grafite ast constructors *************************************************)
 
 let floc = H.dummy_floc
@@ -38,23 +186,77 @@ 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_qed =
+   G.Executable (floc, G.Command (floc, G.Qed floc))
+
 let mk_tactic tactic =
    G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), None))
 
+let mk_intros xi ids =
+   let tactic = G.Intros (floc, xi, ids) in
+   mk_tactic tactic
+
+let mk_elim what using =
+   let tactic = G.Elim (floc, what, using, Some 0, []) in
+   mk_tactic tactic
+
+let mk_letin name what =
+   let tactic = G.LetIn (floc, what, name) in
+   mk_tactic tactic
+
+let mk_apply t =
+   let tactic = G.Apply (floc, t) in
+   mk_tactic tactic
+
 let mk_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
 
+let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
+
+let mk_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
+
+let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None))
+
+let mk_cb = G.Executable (floc, G.Tactical (floc, G.Merge floc, None))
+
+let mk_vb = G.Executable (floc, G.Tactical (floc, G.Shift floc, None))
+
+(* rendering ****************************************************************)
+
+let rec render_step sep a = function
+   | Note s            -> mk_note s :: a
+   | Theorem (n, t, s) -> mk_note s :: mk_theorem n t :: a 
+   | Qed s             -> mk_note s :: mk_qed :: a
+   | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a)
+   | Elim (t, xu, s)   -> mk_note s :: cont sep (mk_elim t xu :: a)
+   | LetIn (n, t, s)   -> mk_note s :: cont sep (mk_letin n t :: a)
+   | Apply (t, s)      -> mk_note s :: cont sep (mk_apply t :: a)
+   | Exact (t, s)      -> mk_note s :: cont sep (mk_exact t :: a)
+   | Branch ([], s)    -> a
+   | Branch ([ps], s)  -> render_steps a ps
+   | Branch (pss, s)   ->
+      let a =  mk_ob :: a in
+      let body = mk_cb :: list_rev_map_concat render_steps mk_vb a pss in
+      mk_note s :: cont sep body
+
+and render_steps a = function
+   | []                                          -> a
+   | [p]                                         -> render_step None a p
+   | (Note _ | Theorem _ | Qed _ as p) :: ps     ->
+      render_steps (render_step None a p) ps 
+   | p :: ((Branch ([], _) :: _) as ps) ->
+      render_steps (render_step None a p) ps
+   | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) ->
+      render_steps (render_step (Some mk_sc) a p) ps
+   | p :: ps                                     ->
+      render_steps (render_step (Some mk_dot) a p) ps
+
 (* 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 
+let content2procedural ~ids_to_inner_sorts prefix cobj = 
+   prerr_endline "Level 2 transformation";
+   let steps = mk_obj ids_to_inner_sorts prefix cobj in
+   prerr_endline "grafite rendering";
+   List.rev (render_steps [] steps)
+