From 3f586b01da59fe16b3d7f37da28bdd71f2225131 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 29 Dec 2006 11:28:13 +0000 Subject: [PATCH] - tactics: rename tactic enabled, rewrite and rewrite_simpl now take optional names for the rewrited premises - procedural script reconstruction now starts directly from acic bypassing the content level, the script for the use case proof in matita/contribs/prova.ma is reconstructed completely now and is correctly parsed and typechecked --- components/content_pres/.depend | 20 +- components/content_pres/Makefile | 4 +- components/content_pres/acic2Procedural.ml | 229 +++++++++++++++ ...ent2Procedural.mli => acic2Procedural.mli} | 9 +- components/content_pres/cicClassify.ml | 145 ++++++++++ components/content_pres/cicClassify.mli | 36 +++ components/content_pres/content2Procedural.ml | 262 ------------------ components/content_pres/objPp.ml | 5 +- components/content_pres/proceduralTypes.ml | 185 +++++++++++++ components/content_pres/proceduralTypes.mli | 62 +++++ components/grafite/grafiteAst.ml | 3 +- components/grafite/grafiteAstPp.ml | 19 +- components/grafite_engine/grafiteEngine.ml | 5 +- .../grafite_parser/grafiteDisambiguate.ml | 6 +- components/grafite_parser/grafiteParser.ml | 8 +- components/tactics/auto.ml | 2 +- components/tactics/discriminationTactics.ml | 4 +- components/tactics/equalityTactics.ml | 52 ++-- components/tactics/equalityTactics.mli | 6 +- components/tactics/fourierR.ml | 2 +- .../tactics/proofEngineStructuralRules.ml | 86 +++--- .../tactics/proofEngineStructuralRules.mli | 2 +- components/tactics/tactics.ml | 1 + components/tactics/tactics.mli | 7 +- matita/contribs/prova.ma | 41 ++- matita/matita.lang | 1 + 26 files changed, 822 insertions(+), 380 deletions(-) create mode 100644 components/content_pres/acic2Procedural.ml rename components/content_pres/{content2Procedural.mli => acic2Procedural.mli} (83%) create mode 100644 components/content_pres/cicClassify.ml create mode 100644 components/content_pres/cicClassify.mli delete mode 100644 components/content_pres/content2Procedural.ml create mode 100644 components/content_pres/proceduralTypes.ml create mode 100644 components/content_pres/proceduralTypes.mli diff --git a/components/content_pres/.depend b/components/content_pres/.depend index 5a5fbce64..d2bd17f19 100644 --- a/components/content_pres/.depend +++ b/components/content_pres/.depend @@ -30,12 +30,20 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -content2Procedural.cmo: content2Procedural.cmi -content2Procedural.cmx: content2Procedural.cmi -objPp.cmo: termContentPres.cmi content2pres.cmi content2Procedural.cmi \ - cicNotationPres.cmi boxPp.cmi objPp.cmi -objPp.cmx: termContentPres.cmx content2pres.cmx content2Procedural.cmx \ - cicNotationPres.cmx boxPp.cmx objPp.cmi +cicClassify.cmo: cicClassify.cmi +cicClassify.cmx: cicClassify.cmi +proceduralTypes.cmo: proceduralTypes.cmi +proceduralTypes.cmx: proceduralTypes.cmi +content2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi \ + content2Procedural.cmi +content2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx \ + content2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi cicClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx cicClassify.cmx acic2Procedural.cmi +objPp.cmo: termContentPres.cmi content2pres.cmi cicNotationPres.cmi boxPp.cmi \ + acic2Procedural.cmi objPp.cmi +objPp.cmx: termContentPres.cmx content2pres.cmx cicNotationPres.cmx boxPp.cmx \ + acic2Procedural.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index 497afc8d2..a3b153029 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -12,7 +12,9 @@ INTERFACE_FILES = \ cicNotationPres.mli \ boxPp.mli \ content2pres.mli \ - content2Procedural.mli \ + cicClassify.mli \ + proceduralTypes.mli \ + acic2Procedural.mli \ objPp.mli \ sequent2pres.mli \ $(NULL) diff --git a/components/content_pres/acic2Procedural.ml b/components/content_pres/acic2Procedural.ml new file mode 100644 index 000000000..f568ac7c5 --- /dev/null +++ b/components/content_pres/acic2Procedural.ml @@ -0,0 +1,229 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module L = CicClassify +module P = ProceduralTypes +module D = Deannotate +module DTI = DoubleTypeInference +module TC = CicTypeChecker +module U = CicUniv +module UM = UriManager +module Obj = LibraryObjects +module HObj = HelmLibraryObjects +module A = Cic2acic +module T = CicUtil + +type status = { + sorts : (Cic.id, Cic2acic.sort_kind) Hashtbl.t; + types : (C.id, A.anntypes) Hashtbl.t; + prefix: string; + max_depth: int option; + depth: int; + entries: C.context; + intros: string list +} + +(* helpers ******************************************************************) + +let cic = D.deannotate_term + +let split2_last l1 l2 = + let n = pred (List.length l1) in + let before1, after1 = P.list_split n l1 in + let before2, after2 = P.list_split n l2 in + before1, before2, List.hd after1, List.hd after2 + +let string_of_head = function + | C.ASort _ -> "sort" + | C.AConst _ -> "const" + | C.AMutInd _ -> "mutind" + | C.AMutConstruct _ -> "mutconstruct" + | C.AVar _ -> "var" + | C.ARel _ -> "rel" + | C.AProd _ -> "prod" + | C.ALambda _ -> "lambda" + | C.ALetIn _ -> "letin" + | C.AFix _ -> "fix" + | C.ACoFix _ -> "cofix" + | C.AAppl _ -> "appl" + | C.ACast _ -> "cast" + | C.AMutCase _ -> "mutcase" + | C.AMeta _ -> "meta" + | C.AImplicit _ -> "implict" + +let next st = {st with depth = succ st.depth; intros = []} + +let add st entry intro = + {st with entries = entry :: st.entries; intros = intro :: st.intros} + +let test_depth st = + let msg = Printf.sprintf "Depth %u: " st.depth in + match st.max_depth with + | None -> true, "" + | Some d -> + if st.depth < d then true, msg else false, "DEPTH EXCEDED" + +let get_itype st v = + let id = T.id_of_annterm v in + try Some ((Hashtbl.find st.types id).A.annsynthesized) + with Not_found -> None + +(* proof construction *******************************************************) + +let unused_premise = "UNUSED" + +let get_intro name t = match name with + | C.Anonymous -> unused_premise + | C.Name s -> + if DTI.does_not_occur 1 (cic t) then unused_premise else s + +let mk_intros st script = + if st.intros = [] then script else + let count = List.length st.intros in + P.Intros (Some count, List.rev st.intros, "") :: script + +let is_rewrite_right = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_r_URI || Obj.is_eq_ind_r_URI uri + | _ -> false + +let is_rewrite_left = function + | C.AConst (_, uri, []) -> + UM.eq uri HObj.Logic.eq_ind_URI || Obj.is_eq_ind_URI uri + | _ -> false + +let mk_premise = function + | C.ARel (_, _, _, binder) -> binder + | _ -> assert false + +let rec mk_fwd_proof st dtext name = function + | C.AAppl (_, hd :: tl) as v -> + if is_rewrite_right hd then + let what, where = List.nth tl 5, List.nth tl 3 in + let premise = mk_premise where in + [P.Rewrite (true, what, Some (premise, name), dtext)] + else if is_rewrite_left hd then + let what, where = List.nth tl 5, List.nth tl 3 in + let premise = mk_premise where in + [P.Rewrite (false, what, Some (premise, name), dtext)] + else begin match get_itype st v with + | Some ty -> + let qs = [[P.Id ""]; mk_proof (next st) v] in + [P.Branch (qs, ""); P.Cut (name, ty, dtext)] + | None -> + let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in + let (classes, rc) as h = L.classify ty in + let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in + [P.LetIn (name, v, dtext ^ text)] + end + | v -> + [P.LetIn (name, v, dtext)] + +and mk_proof st = function + | C.ALambda (_, name, v, t) -> + let entry = Some (name, C.Decl (cic v)) in + let intro = get_intro name t in + mk_proof (add st entry intro) t + | C.ALetIn (_, name, v, t) as what -> + let proceed, dtext = test_depth st in + let script = if proceed then + let intro = get_intro name t in + let q = mk_proof (next st) t in + List.rev_append (mk_fwd_proof st dtext intro v) q + else + [P.Apply (what, dtext)] + in + mk_intros st script + | C.ARel _ as what -> + let _, dtext = test_depth st in + let script = [P.Apply (what, dtext)] in + mk_intros st script + | C.AAppl (_, hd :: tl) as t -> + let proceed, dtext = test_depth st in + let script = if proceed then + let ty, _ = TC.type_of_aux' [] st.entries (cic hd) U.empty_ugraph in + let (classes, rc) as h = L.classify ty in + let synth = L.S.singleton 0 in + let text = Printf.sprintf "%u %s" (List.length classes) (L.to_string h) in + match rc with + | Some (i, j) when i > 1 -> + let classes, tl, _, what = split2_last classes tl in + let synth = L.S.add 1 synth in + let qs = mk_bkd_proofs (next st) synth classes tl in + if is_rewrite_right hd then + [P.Rewrite (false, what, None, dtext); P.Branch (qs, "")] + else if is_rewrite_left hd then + [P.Rewrite (true, what, None, dtext); P.Branch (qs, "")] + else + let using = Some hd in + [P.Elim (what, using, dtext ^ text); P.Branch (qs, "")] + | _ -> + let qs = mk_bkd_proofs (next st) synth classes tl in + [P.Apply (hd, dtext ^ text); P.Branch (qs, "")] + else + [P.Apply (t, dtext)] + in + mk_intros st script + | t -> + let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in + let script = [P.Note text] in + mk_intros st script + +and mk_bkd_proofs st synth classes ts = + let _, dtext = test_depth st in + let aux inv v = + if L.overlaps synth inv then None else + if L.S.is_empty inv then Some (mk_proof st v) else + Some [P.Apply (v, dtext ^ "dependent")] + in + P.list_map2_filter aux classes ts + +(* object costruction *******************************************************) + +let mk_obj st = function + | C.AConstant (_, _, s, Some v, t, [], _) -> + let ast = mk_proof st v in + let count = P.count_steps 0 ast in + let text = Printf.sprintf "tactics: %u" count in + P.Theorem (s, t, text) :: ast @ [P.Qed ""] + | _ -> assert false + +(* interface functions ******************************************************) + +let acic2procedural ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj = + let st = { + sorts = ids_to_inner_sorts; + types = ids_to_inner_types; + prefix = prefix; + max_depth = None; + depth = 0; + entries = []; + intros = [] + } in + prerr_endline "Level 2 transformation"; + let steps = mk_obj st aobj in + prerr_endline "grafite rendering"; + List.rev (P.render_steps [] steps) diff --git a/components/content_pres/content2Procedural.mli b/components/content_pres/acic2Procedural.mli similarity index 83% rename from components/content_pres/content2Procedural.mli rename to components/content_pres/acic2Procedural.mli index 938d4dd6b..50fb60898 100644 --- a/components/content_pres/content2Procedural.mli +++ b/components/content_pres/acic2Procedural.mli @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2003-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,9 +23,10 @@ * http://cs.unibo.it/helm/. *) -val content2procedural: - ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> string -> - Cic.annterm Content.cobj -> +val acic2procedural: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> + ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t -> + string -> Cic.annobj -> (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list diff --git a/components/content_pres/cicClassify.ml b/components/content_pres/cicClassify.ml new file mode 100644 index 000000000..155ab98f3 --- /dev/null +++ b/components/content_pres/cicClassify.ml @@ -0,0 +1,145 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module C = Cic +module CS = CicSubstitution +module D = Deannotate +module Int = struct + type t = int + let compare = compare +end +module S = Set.Make (Int) + +type conclusion = (int * int) option + +(* debugging ****************************************************************) + +let string_of_entry inverse = + if S.mem 0 inverse then "C" else + if S.is_empty inverse then "I" else "P" + +let to_string (classes, rc) = + let linearize = String.concat " " (List.map string_of_entry classes) in + match rc with + | None -> linearize + | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j + +let out_table b = + let map i (_, inverse) = + let map i tl = Printf.sprintf "%2u" i :: tl in + let iset = String.concat " " (S.fold map inverse []) in + Printf.eprintf "%2u|%s\n" i iset + in + Array.iteri map b; + prerr_newline () + +(****************************************************************************) + +let rec list_fold_left g map = function + | [] -> g + | hd :: tl -> map (list_fold_left g map tl) hd + +let get_rels h t = + let rec aux d g = function + | C.Sort _ + | C.Implicit _ -> g + | C.Rel i -> + if i < d then g else fun a -> g (S.add (i - d + h + 1) a) + | C.Appl ss -> list_fold_left g (aux d) ss + | C.Const (_, ss) + | C.MutInd (_, _, ss) + | C.MutConstruct (_, _, _, ss) + | C.Var (_, ss) -> + let map g (_, t) = aux d g t in + list_fold_left g map ss + | C.Meta (_, ss) -> + let map g = function + | None -> g + | Some t -> aux d g t + in + list_fold_left g map ss + | C.Cast (t1, t2) -> aux d (aux d g t2) t1 + | C.LetIn (_, t1, t2) + | C.Lambda (_, t1, t2) + | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1 + | C.MutCase (_, _, t1, t2, ss) -> + aux d (aux d (list_fold_left g (aux d) ss) t2) t1 + | C.Fix (_, ss) -> + let k = List.length ss in + let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in + list_fold_left g map ss + | C.CoFix (_, ss) -> + let k = List.length ss in + let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in + list_fold_left g map ss + in + let g a = a in + aux 1 g t S.empty + +let split t = + let rec aux a n = function + | C.Prod (_, v, t) -> aux (v :: a) (succ n) t + | C.Cast (t, v) -> aux a n t + | C.LetIn (_, v, t) -> aux a n (CS.subst v t) + | v -> v :: a, n + in + aux [] 0 t + +let classify_conclusion = function + | C.Rel i -> Some (i, 0) + | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) + | _ -> None + +let classify t = + let vs, h = split t in + let rc = classify_conclusion (List.hd vs) in + let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in + let l, h = List.fold_left map ([], 0) vs in + let b = Array.of_list (List.rev l) in + let mk_closure b h = + let map j = S.union (fst b.(j)) in + for i = pred h downto 0 do + let direct, unused = b.(i) in + b.(i) <- S.fold map direct direct, unused + done; b + in + let b = mk_closure b h in + let rec mk_inverse i direct = + if S.is_empty direct then () else + let j = S.choose direct in + let unused, inverse = b.(j) in + b.(j) <- unused, S.add i inverse; + mk_inverse i (S.remove j direct) + in + let map i (direct, _) = mk_inverse i direct in + Array.iteri map b; + out_table b; + List.rev_map snd (List.tl (Array.to_list b)), rc + +let aclassify t = classify (D.deannotate_term t) + +let overlaps s1 s2 = + let predicate x = S.mem x s1 in + S.exists predicate s2 diff --git a/components/content_pres/cicClassify.mli b/components/content_pres/cicClassify.mli new file mode 100644 index 000000000..c35ba1b5c --- /dev/null +++ b/components/content_pres/cicClassify.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module S : Set.S with type elt = int + +type conclusion = (int * int) option + +val classify: Cic.term -> S.t list * conclusion + +val aclassify: Cic.annterm -> S.t list * conclusion + +val to_string: S.t list * conclusion -> string + +val overlaps: S.t -> S.t -> bool diff --git a/components/content_pres/content2Procedural.ml b/components/content_pres/content2Procedural.ml deleted file mode 100644 index 5c1ca4c15..000000000 --- a/components/content_pres/content2Procedural.ml +++ /dev/null @@ -1,262 +0,0 @@ -(* Copyright (C) 2003-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -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 - -let mk_note str = G.Comment (floc, G.Note (floc, str)) - -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 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) - diff --git a/components/content_pres/objPp.ml b/components/content_pres/objPp.ml index aa2e3a6b8..68badf324 100644 --- a/components/content_pres/objPp.ml +++ b/components/content_pres/objPp.ml @@ -42,9 +42,9 @@ let term2pres n ids_to_inner_sorts annterm = let obj_to_string n style prefix obj = let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in - let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in match style with | GrafiteAst.Declarative -> + let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in remove_closed_substs ("\n\n" ^ BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) @@ -54,5 +54,6 @@ let obj_to_string n style prefix obj = let lazy_term_pp = term_pp in let obj_pp = CicNotationPp.pp_obj term_pp in let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in - let script = Content2Procedural.content2procedural ~ids_to_inner_sorts prefix cobj in + let script = Acic2Procedural.acic2procedural + ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj in "\n\n" ^ String.concat "" (List.map aux script) diff --git a/components/content_pres/proceduralTypes.ml b/components/content_pres/proceduralTypes.ml new file mode 100644 index 000000000..700fed082 --- /dev/null +++ b/components/content_pres/proceduralTypes.ml @@ -0,0 +1,185 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +module H = HExtlib +module C = Cic +module G = GrafiteAst +module N = CicNotationPt + +(* functions to be moved ****************************************************) + +let list_map2_filter map l1 l2 = + let rec filter l = function + | [] -> l + | None :: tl -> filter l tl + | Some a :: tl -> filter (a :: l) tl + in + filter [] (List.rev_map2 map l1 l2) + +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 how = bool +type using = Cic.annterm +type count = int +type note = string +type where = (name * name) option + +type step = Note of note + | Theorem of name * what * note + | Qed of note + | Id of note + | Intros of count option * name list * note + | Cut of name * what * note + | LetIn of name * what * note + | Rewrite of how * what * where * note + | Elim of what * using option * note + | Apply of what * note + | Branch of step list list * note + +(* annterm constructors *****************************************************) + +let mk_arel i b = Cic.ARel ("", "", i, b) + +(* grafite ast constructors *************************************************) + +let floc = H.dummy_floc + +let mk_note str = G.Comment (floc, G.Note (floc, str)) + +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_id = + let tactic = G.IdTac floc in + mk_tactic tactic + +let mk_intros xi ids = + let tactic = G.Intros (floc, xi, ids) in + mk_tactic tactic + +let mk_cut name what = + let tactic = G.Cut (floc, Some name, what) in + mk_tactic tactic + +let mk_letin name what = + let tactic = G.LetIn (floc, what, name) in + mk_tactic tactic + +let mk_rewrite direction what where = + let hole = C.AImplicit ("", Some `Hole) in + let direction = if direction then `RightToLeft else `LeftToRight in + let pattern, rename = match where with + | None -> (None, [], Some hole), [] + | Some (premise, name) -> (None, [premise, hole], None), [name] + in + let tactic = G.Rewrite (floc, direction, what, pattern, rename) in + mk_tactic tactic + +let mk_elim what using = + let tactic = G.Elim (floc, what, using, Some 0, []) in + mk_tactic tactic + +let mk_apply t = + let tactic = G.Apply (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 + | Id s -> mk_note s :: cont sep (mk_id :: a) + | Intros (c, ns, s) -> mk_note s :: cont sep (mk_intros c ns :: a) + | Cut (n, t, s) -> mk_note s :: cont sep (mk_cut n t :: a) + | LetIn (n, t, s) -> mk_note s :: cont sep (mk_letin n t :: a) + | Rewrite (b, t, w, s) -> mk_note s :: cont sep (mk_rewrite b t w :: a) + | Elim (t, xu, s) -> mk_note s :: cont sep (mk_elim t xu :: a) + | Apply (t, s) -> mk_note s :: cont sep (mk_apply 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 + +(* counting *****************************************************************) + +let rec count_step a = function + | Note _ + | Theorem _ + | Qed _ -> a + | Branch (pps, _) -> List.fold_left count_steps a pps + | _ -> succ a + +and count_steps a = List.fold_left count_step a diff --git a/components/content_pres/proceduralTypes.mli b/components/content_pres/proceduralTypes.mli new file mode 100644 index 000000000..ebadd9da8 --- /dev/null +++ b/components/content_pres/proceduralTypes.mli @@ -0,0 +1,62 @@ +(* Copyright (C) 2003-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* functions to be moved ****************************************************) + +val list_map2_filter: ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list + +val list_split: int -> 'a list -> 'a list * 'a list + +val mk_arel: int -> string -> Cic.annterm + +(****************************************************************************) + +type name = string +type what = Cic.annterm +type how = bool +type using = Cic.annterm +type count = int +type note = string +type where = (name * name) option + +type step = Note of note + | Theorem of name * what * note + | Qed of note + | Id of note + | Intros of count option * name list * note + | Cut of name * what * note + | LetIn of name * what * note + | Rewrite of how * what * where * note + | Elim of what * using option * note + | Apply of what * note + | Branch of step list list * note + +val render_steps: + (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> + step list -> + (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list + +val count_steps: + int -> step list -> int diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index d6dfa53a6..e75e53867 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -77,9 +77,10 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | LetIn of loc * 'term * 'ident | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern | Reflexivity of loc + | Rename of loc * 'ident list * 'ident list | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Rewrite of loc * direction * 'term * - ('term, 'lazy_term, 'ident) pattern + ('term, 'lazy_term, 'ident) pattern * 'ident list | Right of loc | Ring of loc | Split of loc diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index d775a77dc..f38dbf859 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -44,6 +44,7 @@ let pp_reduction_kind ~term_pp = function | `Whd -> "whd" let pp_tactic_pattern ~term_pp ~lazy_term_pp (what, hyp, goal) = + if what = None && hyp = [] && goal = None then "" else let what_text = match what with | None -> "" @@ -74,7 +75,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in function | Absurd (_, term) -> "absurd" ^ term_pp term - | Apply (_, term) -> "apply " ^ term_pp term + | Apply (_, term) -> "apply (" ^ term_pp term ^ ")" (* FG: rm parentheses *) | ApplyS (_, term, params) -> "applyS " ^ term_pp term ^ String.concat " " @@ -92,7 +93,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> - "cut " ^ term_pp term ^ + "cut (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *) (match ident with None -> "" | Some id -> " as " ^ id) | Decompose (_, [], what, names) -> sprintf "decompose %s%s" (opt_string_pp what) (pp_intros_specs (None, names)) @@ -106,7 +107,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Demodulate _ -> "demodulate" | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, term, using, num, idents) -> - sprintf "elim " ^ term_pp term ^ + sprintf "elim (" ^ term_pp term ^ ")" ^ (* FG: rm parentheses *) (match using with None -> "" | Some term -> " using " ^ term_pp term) ^ pp_intros_specs (num, idents) | ElimType (_, term, using, num, idents) -> @@ -142,17 +143,21 @@ 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 "letin %s \\def %s" ident (term_pp term) + | LetIn (_, term, ident) -> + sprintf "letin %s \\def %s" ident ("(" ^ term_pp term ^ ")") (* FG: rm parentheses *) | Reduce (_, kind, pat) -> sprintf "%s %s" (pp_reduction_kind kind) (pp_tactic_pattern pat) | Reflexivity _ -> "reflexivity" + | Rename (_, froms, tos) -> + sprintf "rename %s as %s" (pp_idents froms) (pp_idents tos) | Replace (_, pattern, t) -> sprintf "replace %s with %s" (pp_tactic_pattern pattern) (lazy_term_pp t) - | Rewrite (_, pos, t, pattern) -> - sprintf "rewrite %s %s %s" + | Rewrite (_, pos, t, pattern, names) -> + sprintf "rewrite %s %s %s%s" (if pos = `LeftToRight then ">" else "<") - (term_pp t) + ("(" ^ term_pp t ^ ")") (* FG: rm parentheses *) (pp_tactic_pattern pattern) + (if names = [] then "" else " as " ^ pp_idents names) | Right _ -> "right" | Ring _ -> "ring" | Split _ -> "split" diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index a125d23be..30aa982d8 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -151,10 +151,11 @@ let tactic_of_ast status ast = | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) | GrafiteAst.Reflexivity _ -> Tactics.reflexivity + | GrafiteAst.Rename (_, froms, tos) -> Tactics.rename ~froms ~tos | GrafiteAst.Replace (_, pattern, with_what) -> Tactics.replace ~pattern ~with_what - | GrafiteAst.Rewrite (_, direction, t, pattern) -> - EqualityTactics.rewrite_tac ~direction ~pattern t + | GrafiteAst.Rewrite (_, direction, t, pattern, names) -> + EqualityTactics.rewrite_tac ~direction ~pattern t names | GrafiteAst.Right _ -> Tactics.right | GrafiteAst.Ring _ -> Tactics.ring | GrafiteAst.Split _ -> Tactics.split diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 2d06942e3..e7f5eb1fd 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -232,14 +232,16 @@ let disambiguate_tactic metasenv,GrafiteAst.Reduce(loc, red_kind, pattern) | GrafiteAst.Reflexivity loc -> metasenv,GrafiteAst.Reflexivity loc + | GrafiteAst.Rename (loc, froms, tos) -> + metasenv,GrafiteAst.Rename (loc, froms, tos) | GrafiteAst.Replace (loc, pattern, with_what) -> let pattern = disambiguate_pattern pattern in let with_what = disambiguate_lazy_term with_what in metasenv,GrafiteAst.Replace (loc, pattern, with_what) - | GrafiteAst.Rewrite (loc, dir, t, pattern) -> + | GrafiteAst.Rewrite (loc, dir, t, pattern, names) -> let metasenv,term = disambiguate_term context metasenv t in let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern) + metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names) | GrafiteAst.Right loc -> metasenv,GrafiteAst.Right loc | GrafiteAst.Ring loc -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 054bff621..586cca004 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -218,9 +218,12 @@ EXTEND GrafiteAst.Reduce (loc, kind, p) | IDENT "reflexivity" -> GrafiteAst.Reflexivity loc + | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 -> + GrafiteAst.Rename (loc, froms, tos) | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec; + xnames = OPT [ "as"; n = ident_list0 -> n ] -> let (pt,_,_) = p in if pt <> None then raise @@ -228,7 +231,8 @@ EXTEND (CicNotationParser.Parse_error "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) else - GrafiteAst.Rewrite (loc, d, t, p) + let n = match xnames with None -> [] | Some names -> names in + GrafiteAst.Rewrite (loc, d, t, p, n) | IDENT "right" -> GrafiteAst.Right loc | IDENT "ring" -> diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 5f110bc4c..65087f8cb 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -452,7 +452,7 @@ let new_metasenv_and_unify_and_t ProofEngineTypes.apply_tactic (EqualityTactics.rewrite_tac ~direction:`RightToLeft ~pattern:(ProofEngineTypes.conclusion_pattern None) - (Cic.Meta(newmeta,irl))) + (Cic.Meta(newmeta,irl)) []) (proof'',goal) in let goal = match goals with [g] -> g | _ -> assert false in diff --git a/components/tactics/discriminationTactics.ml b/components/tactics/discriminationTactics.ml index 9c5d002ca..ebf772844 100644 --- a/components/tactics/discriminationTactics.ml +++ b/components/tactics/discriminationTactics.ml @@ -186,7 +186,7 @@ let discriminate_tac ~term = (EqualityTactics.rewrite_simpl_tac ~direction:`RightToLeft ~pattern:(ProofEngineTypes.conclusion_pattern None) - term) + term []) ~continuation: (IntroductionTactics.constructor_tac ~n:1)))) status | _ -> fail "not an equality" @@ -459,7 +459,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = (EqualityTactics.rewrite_simpl_tac ~direction:`LeftToRight ~pattern:(ProofEngineTypes.conclusion_pattern None) - term) + term []) ~continuation:EqualityTactics.reflexivity_tac) ]) status diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index e81f54076..89da5c9fd 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -40,9 +40,8 @@ module LO = LibraryObjects module DTI = DoubleTypeInference module HEL = HExtlib -let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equality = - let _rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality status - = +let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = + let _rewrite_tac status = assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in let curi, metasenv, pbo, pty = proof in @@ -50,7 +49,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit match hyps_pat with he::(_::_ as tl) -> PET.apply_tactic - (Tacticals.then_ + (T.then_ (rewrite_tac ~direction ~pattern:(None,[he],None) equality) (rewrite_tac ~direction ~pattern:(None,tl,concl_pat) @@ -58,7 +57,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit ) status | [_] as hyps_pat when concl_pat <> None -> PET.apply_tactic - (Tacticals.then_ + (T.then_ (rewrite_tac ~direction ~pattern:(None,hyps_pat,None) equality) (rewrite_tac ~direction ~pattern:(None,[],concl_pat) @@ -81,17 +80,17 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit let dummy = "dummy" in Some arg,false, (fun ~term typ -> - Tacticals.seq + T.seq ~tactics: - [ProofEngineStructuralRules.rename name dummy; + [PESR.rename [name] [dummy]; P.letin_tac ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name name) term; - ProofEngineStructuralRules.clearbody name; + PESR.clearbody name; ReductionTactics.change_tac ~pattern: (None,[name,Cic.Implicit (Some `Hole)], None) (ProofEngineTypes.const_lazy_term typ); - ProofEngineStructuralRules.clear [dummy] + PESR.clear [dummy] ]), Some pat,gty | _::_ -> assert false @@ -196,22 +195,23 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit TC.TypeCheckerFailure _ -> let msg = lazy "rewrite: nothing to rewrite" in raise (PET.Fail msg) - in - ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality) - - -let rewrite_simpl_tac ~direction ~pattern equality = - let rewrite_simpl_tac ~direction ~pattern equality status = - ProofEngineTypes.apply_tactic - (Tacticals.then_ - ~start:(rewrite_tac ~direction ~pattern equality) + in + PET.mk_tactic _rewrite_tac + +let rewrite_tac ~direction ~pattern equality names = + let _, hyps_pat, _ = pattern in + let froms = List.map fst hyps_pat in + let start = rewrite_tac ~direction ~pattern equality in + let continuation = PESR.rename ~froms ~tos:names in + if names = [] then start else T.then_ ~start ~continuation + +let rewrite_simpl_tac ~direction ~pattern equality names = + T.then_ + ~start:(rewrite_tac ~direction ~pattern equality names) ~continuation: (ReductionTactics.simpl_tac - ~pattern:(ProofEngineTypes.conclusion_pattern None))) - status - in - ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~direction ~pattern equality) -;; + ~pattern:(ProofEngineTypes.conclusion_pattern None)) + let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status = @@ -295,7 +295,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~continuations:[ T.then_ ~start:( - rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1)) + rewrite_tac ~direction:`LeftToRight ~pattern:lazy_pattern (C.Rel 1) []) ~continuation:( T.then_ ~start:( @@ -311,7 +311,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = with (Failure "hd") -> assert false in ProofEngineTypes.apply_tactic - (ProofEngineStructuralRules.clear ~hyps) status)) + (PESR.clear ~hyps) status)) ~continuation:(aux_tac (n + 1) tl)); T.id_tac]) status @@ -383,7 +383,7 @@ let rec lift_rewrite_tac ~context ~direction ~pattern equality = let _, new_context, _ = CicUtil.lookup_meta goal metasenv in let n = List.length new_context - List.length context in let equality = if n > 0 then S.lift n equality else equality in - PET.apply_tactic (rewrite_tac ~direction ~pattern equality) status + PET.apply_tactic (rewrite_tac ~direction ~pattern equality []) status in PET.mk_tactic lift_rewrite_tac diff --git a/components/tactics/equalityTactics.mli b/components/tactics/equalityTactics.mli index 4edb5747a..52f2f2043 100644 --- a/components/tactics/equalityTactics.mli +++ b/components/tactics/equalityTactics.mli @@ -25,11 +25,13 @@ val rewrite_tac: direction:[`LeftToRight | `RightToLeft] -> - pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list -> + ProofEngineTypes.tactic val rewrite_simpl_tac: direction:[`LeftToRight | `RightToLeft] -> - pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic + pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> string list -> + ProofEngineTypes.tactic val replace_tac: pattern:ProofEngineTypes.lazy_pattern -> diff --git a/components/tactics/fourierR.ml b/components/tactics/fourierR.ml index 8b910bded..1123b506f 100644 --- a/components/tactics/fourierR.ml +++ b/components/tactics/fourierR.ml @@ -885,7 +885,7 @@ let equality_replace a b = (EqualityTactics.rewrite_simpl_tac ~direction:`LeftToRight ~pattern:(ProofEngineTypes.conclusion_pattern None) - (C.Meta (fresh_meta,irl))) + (C.Meta (fresh_meta,irl)) []) ((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in diff --git a/components/tactics/proofEngineStructuralRules.ml b/components/tactics/proofEngineStructuralRules.ml index b1e23751f..acc4bb164 100644 --- a/components/tactics/proofEngineStructuralRules.ml +++ b/components/tactics/proofEngineStructuralRules.ml @@ -25,11 +25,11 @@ (* $Id$ *) -open ProofEngineTypes +module PET = ProofEngineTypes +module C = Cic let clearbody ~hyp = - let clearbody ~hyp (proof, goal) = - let module C = Cic in + let clearbody (proof, goal) = let curi,metasenv,pbo,pty = proof in let metano,_,_ = CicUtil.lookup_meta goal metasenv in let string_of_name = @@ -68,7 +68,7 @@ let clearbody ~hyp = with _ -> raise - (Fail + (PET.Fail (lazy ("The correctness of hypothesis " ^ string_of_name n ^ " relies on the body of " ^ hyp) @@ -85,7 +85,7 @@ let clearbody ~hyp = with _ -> raise - (Fail + (PET.Fail (lazy ("The correctness of the goal relies on the body of " ^ hyp))) in @@ -95,11 +95,10 @@ let clearbody ~hyp = in (curi,metasenv',pbo,pty), [goal] in - mk_tactic (clearbody ~hyp) + PET.mk_tactic clearbody let clear_one ~hyp = - let clear_one ~hyp (proof, goal) = - let module C = Cic in + let clear_one (proof, goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv @@ -130,7 +129,7 @@ let clear_one ~hyp = CicUniv.empty_ugraph with _ -> raise - (Fail + (PET.Fail (lazy ("Hypothesis " ^ string_of_name n ^ " uses hypothesis " ^ hyp))) in @@ -140,13 +139,13 @@ let clear_one ~hyp = ) canonical_context (false, []) in if not context_changed then - raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); + raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty CicUniv.empty_ugraph with _ -> - raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) + raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) in m,canonical_context',ty | t -> t @@ -154,54 +153,53 @@ let clear_one ~hyp = in (curi,metasenv',pbo,pty), [goal] in - mk_tactic (clear_one ~hyp) + PET.mk_tactic clear_one let clear ~hyps = - let clear hyps status = + let clear status = let aux status hyp = - match apply_tactic (clear_one ~hyp) status with + match PET.apply_tactic (clear_one ~hyp) status with | proof, [g] -> proof, g - | _ -> raise (Fail (lazy "clear: internal error")) + | _ -> raise (PET.Fail (lazy "clear: internal error")) in let proof, g = List.fold_left aux status hyps in proof, [g] in - mk_tactic (clear hyps) + PET.mk_tactic clear (* Warning: this tactic has no effect on the proof term. It just changes the name of an hypothesis in the current sequent *) -let rename ~from ~to_ = - let rename ~from ~to_ (proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - CicUtil.lookup_meta goal metasenv - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.map - (function - Some (Cic.Name hyp,decl_or_def) when hyp = from -> - Some (Cic.Name to_,decl_or_def) - | item -> item - ) canonical_context - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] - in - mk_tactic (rename ~from ~to_) +let rename ~froms ~tos = + let rename (proof, goal) = + let error = "rename: lists of different length" in + let assocs = + try List.combine froms tos + with Invalid_argument _ -> raise (PET.Fail (lazy error)) + in + let curi, metasenv, pbo, pty = proof in + let metano, _, _ = CicUtil.lookup_meta goal metasenv in + let rename_map = function + | Some (Cic.Name hyp, decl_or_def) as entry -> + begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def) + with Not_found -> entry end + | entry -> entry + in + let map = function + | m, canonical_context, ty when m = metano -> + let canonical_context = List.map rename_map canonical_context in + m, canonical_context, ty + | conjecture -> conjecture + in + let metasenv = List.map map metasenv in + (curi, metasenv, pbo, pty), [goal] + in + PET.mk_tactic rename let set_goal n = - ProofEngineTypes.mk_tactic + PET.mk_tactic (fun (proof, goal) -> let (_, metasenv, _, _) = proof in if CicUtil.exists_meta n metasenv then (proof, [n]) else - raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n)))) + raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n)))) diff --git a/components/tactics/proofEngineStructuralRules.mli b/components/tactics/proofEngineStructuralRules.mli index 7eb8fcc6b..f87a48325 100644 --- a/components/tactics/proofEngineStructuralRules.mli +++ b/components/tactics/proofEngineStructuralRules.mli @@ -28,7 +28,7 @@ val clear: hyps:string list -> ProofEngineTypes.tactic (* Warning: this tactic has no effect on the proof term. It just changes the name of an hypothesis in the current sequent *) -val rename: from:string -> to_:string -> ProofEngineTypes.tactic +val rename: froms:string list -> tos:string list -> ProofEngineTypes.tactic (* change the current goal to those referred by the given meta number *) val set_goal: int -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 82c343085..130ad7100 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -59,6 +59,7 @@ let letin = PrimitiveTactics.letin_tac let normalize = ReductionTactics.normalize_tac let reduce = ReductionTactics.reduce_tac let reflexivity = Setoids.setoid_reflexivity_tac +let rename = ProofEngineStructuralRules.rename let replace = EqualityTactics.replace_tac let rewrite = EqualityTactics.rewrite_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index b0ec098e0..6d842a797 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Dec 21 00:41:09 CET 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 00:00:27 CET 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -72,17 +72,18 @@ val normalize : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic +val rename : froms:string list -> tos:string list -> ProofEngineTypes.tactic val replace : pattern:ProofEngineTypes.lazy_pattern -> with_what:Cic.lazy_term -> ProofEngineTypes.tactic val rewrite : direction:[ `LeftToRight | `RightToLeft ] -> pattern:ProofEngineTypes.lazy_pattern -> - Cic.term -> ProofEngineTypes.tactic + Cic.term -> string list -> ProofEngineTypes.tactic val rewrite_simpl : direction:[ `LeftToRight | `RightToLeft ] -> pattern:ProofEngineTypes.lazy_pattern -> - Cic.term -> ProofEngineTypes.tactic + Cic.term -> string list -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic val set_goal : int -> ProofEngineTypes.tactic diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma index fc6c62b56..7751a0d1f 100644 --- a/matita/contribs/prova.ma +++ b/matita/contribs/prova.ma @@ -14,21 +14,40 @@ set "baseuri" "cic:/matita/tests". -alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)". +include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma". + +alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)". +alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)". +alias id "Appl" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/1)". +alias id "Bind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/1)". +alias id "Cast" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/F.ind#xpointer(1/1/2)". +alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con". +alias id "ex3_2_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/ex3_2_ind.con". +alias id "Flat" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/K.ind#xpointer(1/1/2)". +alias id "lift" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs/lift.con". +alias id "or3_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/defs/or3_ind.con". +alias id "pr0_beta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/3)". 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)". +alias id "pr0_comp" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/2)". +alias id "pr0_delta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/5)". +alias id "pr0_epsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/7)". alias id "pr0_ind" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0_ind.con". +alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con". +alias id "pr0_upsilon" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/4)". +alias id "pr0_zeta" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs/pr0.ind#xpointer(1/1/6)". +alias id "s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs/s.con". +alias id "subst0_both" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/4)". +alias id "subst0" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1)". +alias id "subst0_confluence_neq" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_confluence_neq.con". +alias id "subst0_fst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/2)". 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". -alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)". -alias id "pr0_subst0_fwd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0_fwd.con". -alias id "ex2_sym" = "cic:/matita/LAMBDA-TYPES/Level-1/Base/types/props/ex2_sym.con". +alias id "subst0_lift_ge_s" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/props/subst0_lift_ge_s.con". +alias id "subst0_snd" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs/subst0.ind#xpointer(1/1/3)". +alias id "subst0_subst0_back" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_subst0_back.con". +alias id "subst0_trans" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0/subst0_trans.con". +alias id "T" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1)". +alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xpointer(1/1/3)". inline procedural "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con". diff --git a/matita/matita.lang b/matita/matita.lang index fbb21d6d1..0ba60d173 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -115,6 +115,7 @@ normalize reduce reflexivity + rename replace rewrite ring -- 2.39.2