From 8d04559d1b190e74e1d560000b01a648d086f484 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 18 Dec 2006 21:10:52 +0000 Subject: [PATCH] Procedural: some improvements --- components/content_pres/content2Procedural.ml | 170 +++++++++++++++--- components/grafite/grafiteAstPp.ml | 1 + components/grafite_parser/grafiteParser.ml | 4 +- matita/contribs/prova.ma | 1 + matita/matitaScript.ml | 4 +- 5 files changed, 152 insertions(+), 28 deletions(-) diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml index 99fe8d0b2..6d64a0ef8 100644 --- a/components/content_pres/content2Procedural.ml +++ b/components/content_pres/content2Procedural.ml @@ -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) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 0704863f5..fea47d15b 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -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) diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 14802a629..1321f613b 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -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 ] diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma index 93b195990..84331106d 100644 --- a/matita/contribs/prova.ma +++ b/matita/contribs/prova.ma @@ -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". diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index 1a128fb1c..7a978bbde 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -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 -- 2.39.2