From 89f4301e7fa016e462fb4a01ad4b777c8f33912f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Dec 2006 19:21:36 +0000 Subject: [PATCH] Procedural: "ByInduction" method ok GrafiteAstPp: letin tactic now works --- .../content_pres/content2Procedural.ml | 111 ++++++++++++------ .../components/grafite/grafiteAstPp.ml | 2 +- helm/software/matita/contribs/prova.ma | 5 + 3 files changed, 82 insertions(+), 36 deletions(-) diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml index 6d64a0ef8..9be504913 100644 --- a/helm/software/components/content_pres/content2Procedural.ml +++ b/helm/software/components/content_pres/content2Procedural.ml @@ -24,6 +24,7 @@ *) module H = HExtlib +module U = UriManager module C = Content module G = GrafiteAst module N = CicNotationPt @@ -35,6 +36,18 @@ let rec list_split n l = 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 @@ -48,14 +61,19 @@ type step = Note of note | Qed of note | Intros of count option * name list * note | Elim of what * using option * note + | LetIn of name * 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 -> "_" + | None -> "UNUSED" (**) let mk_intros_arg = function | `Declaration {C.dec_name = name} @@ -70,17 +88,44 @@ 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 +let rec mk_apply_term aref ac ds cargs = + let step0 = mk_arg true (ac, [], ds) (List.hd cargs) in + let _, row, ds = List.fold_left (mk_arg false) step0 (List.tl cargs) in + Cic.AAppl (aref, List.rev row), ds + +and mk_delta p ds = + 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 + match cmethod with + | "Exact" + | "Apply" when ccont = [] -> + let what, ds = mk_apply_term caref capply ds cargs in + let name = "PREVIOUS" in + mk_arel 1 name, LetIn (name, what, "") :: ds + | _ -> mk_arel 1 "COMPOUND", ds + +and mk_arg first (ac, row, ds) = function + | C.Lemma {C.lemma_id = aref; C.lemma_uri = uri} -> + ac, Cic.AConst (aref, U.uri_of_string uri, []) :: row, ds | C.Premise {C.premise_n = Some i; C.premise_binder = Some b} -> - Cic.ARel ("", "", i, b) + ac, mk_arel i b :: row, ds | 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 + begin match first, ac with + | _, hd :: tl -> + let arg, ds = mk_delta hd ds in + tl, arg :: row, ds + | false, [] -> ac, Cic.AImplicit ("", None) :: row, ds + | _ -> assert false + end + | 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 @@ -95,12 +140,14 @@ and mk_proof_body p = 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, "")] + let _, row, ds = mk_arg true (List.rev capply, [], []) whatm in + let what, qs = List.hd row, List.map mk_subproof ms in + List.rev ds @ [Elim (what, Some using, ""); Branch (qs, "")] | _ -> - [Note (Printf.sprintf "%s %u" cmethod (List.length cargs))] + let text = + Printf.sprintf "UNEXPANDED %s %u" cmethod (List.length cargs) + in [Note text] and mk_subproof = function | C.ArgProof ({C.proof_name = Some n} as p) -> Note n :: mk_proof p @@ -138,6 +185,10 @@ 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_exact t = let tactic = G.Exact (floc, t) in mk_tactic tactic @@ -154,46 +205,36 @@ 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) + | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: 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) -> + | 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 -> + | [] -> 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) -> + | p :: ((Branch (_ :: _ :: _, _) :: _) as ps) -> render_steps (render_step (Some mk_sc) a p) ps - | p :: ps -> + | p :: ps -> render_steps (render_step (Some mk_dot) a p) ps (* interface functions ******************************************************) let content2procedural ~ids_to_inner_sorts prefix cobj = - prerr_endline "Phase 2 transformation"; + 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) + diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index fea47d15b..840c16351 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -140,7 +140,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms) (match ident_opt with None -> "" | Some ident -> " as " ^ ident) | Left _ -> "left" - | LetIn (_, term, ident) -> sprintf "let %s in %s" (term_pp term) ident + | LetIn (_, term, ident) -> sprintf "letin %s \\def %s" ident (term_pp term) | Reduce (_, kind, pat) -> sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma index 84331106d..1b817c38e 100644 --- a/helm/software/matita/contribs/prova.ma +++ b/helm/software/matita/contribs/prova.ma @@ -21,6 +21,11 @@ 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". +alias id "subst0_gen_head" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_head.con". +alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con". +alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con". +alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con". +alias id "subst0_gen_lift_ge" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd/subst0_gen_lift_ge.con". inline procedural "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con". -- 2.39.2