]> matita.cs.unibo.it Git - helm.git/commitdiff
Procedural: some improvements
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 18 Dec 2006 21:10:52 +0000 (21:10 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 18 Dec 2006 21:10:52 +0000 (21:10 +0000)
components/content_pres/content2Procedural.ml
components/grafite/grafiteAstPp.ml
components/grafite_parser/grafiteParser.ml
matita/contribs/prova.ma
matita/matitaScript.ml

index 99fe8d0b250b9e647fe46f260b6b5b023e63eeb6..6d64a0ef80e10ecc1940dc3774d0233d568d07c2 100644 (file)
@@ -28,6 +28,92 @@ 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
+
+(****************************************************************************)
+
+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
+         | Exact of what * note
+         | Branch of step list list * note
+
+(* level 2 transformation ***************************************************)
+
+let mk_name = function
+   | Some name -> name
+   | None      -> "_"
+
+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 mk_what rpac = function
+   | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} -> 
+      Cic.ARel ("", "", i, b)
+   | C.Premise {C.premise_n = None; C.premise_binder = None} -> 
+      Cic.ARel ("", "", 1, "COMPOUND")
+   | C.Term t -> t
+   | C.Premise _   -> assert false
+   | C.ArgMethod _ -> assert false
+   | C.ArgProof _  -> assert false
+   | C.Lemma _     -> 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
+   match cmethod, cargs with
+      | "Intros+LetTac", [C.ArgProof p] -> mk_proof p 
+      | "ByInduction", C.Aux n :: C.Term (Cic.AAppl (_, using :: _)) :: tl ->
+        let rpac = List.rev capply in
+        let whatm, ms = split_inductive n tl in (* actual rx params here *)
+         let what, qs = mk_what rpac whatm, List.map mk_subproof ms in
+        [Elim (what, Some using, ""); Branch (qs, "")] 
+      | _ ->  
+        [Note (Printf.sprintf "%s %u" cmethod (List.length cargs))] 
+
+and mk_subproof = function
+   | C.ArgProof ({C.proof_name = Some n} as p) -> Note n :: mk_proof p
+   | C.ArgProof ({C.proof_name = None} as p)   -> Note "" :: mk_proof p
+   | _                                         -> assert false
+
+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,44 +124,76 @@ 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 =
-   let sep = G.Dot floc in
-   G.Executable (floc, G.Tactical (floc, G.Tactic (floc, tactic), Some sep))
+   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_exact t =
    let tactic = G.Exact (floc, t) in
    mk_tactic tactic
 
-(* internal functions *******************************************************)
+let mk_dot = G.Executable (floc, G.Tactical (floc, G.Dot floc, None))
 
-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_sc = G.Executable (floc, G.Tactical (floc, G.Semicolon floc, None))
 
-let mk_intros_args pc = List.map mk_intros_arg pc
+let mk_ob = G.Executable (floc, G.Tactical (floc, G.Branch floc, None))
 
-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))] 
+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 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
+
+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)
+   | Exact (t, s)      -> mk_note s :: cont sep (mk_exact t :: a)
+(*   | Branch ([], s)    -> mk_note s :: cont sep a
+   | Branch ([ps], s)  -> mk_note s :: cont sep (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 (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} as p)) ->
-           mk_theorem name t :: mk_proof p
-      | _ -> assert false 
+let content2procedural ~ids_to_inner_sorts prefix cobj = 
+   prerr_endline "Phase 2 transformation";
+   let steps = mk_obj ids_to_inner_sorts prefix cobj in
+   prerr_endline "grafite rendering";
+   List.rev (render_steps [] steps)
index 0704863f5a779ee28282863c16b38741221ee6a6..fea47d15ba12df4e956c2ce291b778c0e2393ca7 100644 (file)
@@ -298,6 +298,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
                       
 let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
   function
+  | Note (_,"") -> sprintf "\n"
   | Note (_,str) -> sprintf "(* %s *)\n" str
   | Code (_,code) ->
       sprintf "(** %s. **)\n" (pp_executable ~term_pp ~lazy_term_pp ~obj_pp code)
index 14802a629e8cd32360a33c33d1550f506fc50b84..1321f613b82e91a5acc8e793d14c76d49f687624 100644 (file)
@@ -117,7 +117,9 @@ EXTEND
   ];
   int: [ [ num = NUMBER -> int_of_string num ] ];
   intros_spec: [
-    [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 ->
+    [ OPT [ IDENT "names" ]; 
+      num = OPT [ num = int -> num ]; 
+      idents = OPT ident_list0 ->
         let idents = match idents with None -> [] | Some idents -> idents in
         num, idents
     ]
index 93b1959905a2740f5552faa94441f123616fcc68..84331106d1f5587ef774bc80db7359115f5e160a 100644 (file)
@@ -20,6 +20,7 @@ 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)".
+alias id "pr0_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0_ind.con".
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
index 1a128fb1c753bfa58cd30c1631997e0742614b41..7a978bbde3bb19fdd2d0b6eb7d1de28fa17b0831 100644 (file)
@@ -331,7 +331,9 @@ prerr_endline ("Stampo " ^ UriManager.string_of_uri uri);
              ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *)
               (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
             with
-             _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri
+            | e (* BRRRRRRRRR *) -> 
+               Printf.sprintf "\nERRORE IN STAMPA DI %s\n%s\n" 
+               (UriManager.string_of_uri uri) (Printexc.to_string e)
           ) sorted_uris_without_xpointer)
       in
        [],declarative,String.length parsed_text