From 8f5b25b6091f1e240f37de5355e7a99b756e98e8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 14 Feb 2007 17:10:16 +0000 Subject: [PATCH] Procedural : some improvements PrimitiveTactics : tentative implementation of using clause in elim CicNotationParser: noe declarations of the form (_:t) are parsable --- .../METAS/meta.helm-acic_procedural.src | 2 +- components/Makefile | 2 +- components/acic_procedural/.depend | 14 +++--- components/acic_procedural/.depend.opt | 14 +++--- components/acic_procedural/Makefile | 3 +- components/acic_procedural/acic2Procedural.ml | 26 +++++++---- .../{cicClassify.ml => proceduralClassify.ml} | 0 ...cicClassify.mli => proceduralClassify.mli} | 2 + components/acic_procedural/proceduralMode.ml | 45 +++++++++++++++++++ components/acic_procedural/proceduralMode.mli | 26 +++++++++++ components/acic_procedural/proceduralTypes.ml | 22 ++++++--- .../acic_procedural/proceduralTypes.mli | 20 +++++---- components/content_pres/cicNotationParser.ml | 2 + components/tactics/primitiveTactics.ml | 15 ++++--- 14 files changed, 148 insertions(+), 45 deletions(-) rename components/acic_procedural/{cicClassify.ml => proceduralClassify.ml} (100%) rename components/acic_procedural/{cicClassify.mli => proceduralClassify.mli} (95%) create mode 100644 components/acic_procedural/proceduralMode.ml create mode 100644 components/acic_procedural/proceduralMode.mli diff --git a/components/METAS/meta.helm-acic_procedural.src b/components/METAS/meta.helm-acic_procedural.src index e91f1f7d8..f696baea6 100644 --- a/components/METAS/meta.helm-acic_procedural.src +++ b/components/METAS/meta.helm-acic_procedural.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking helm-acic_content helm-grafite" +requires="helm-acic_content helm-grafite helm-tactics" version="0.0.1" archive(byte)="acic_procedural.cma" archive(native)="acic_procedural.cmxa" diff --git a/components/Makefile b/components/Makefile index 9f42d0dad..1b38db7e7 100644 --- a/components/Makefile +++ b/components/Makefile @@ -24,11 +24,11 @@ MODULES = \ library \ acic_content \ grafite \ - acic_procedural \ content_pres \ cic_unification \ whelp \ tactics \ + acic_procedural \ cic_disambiguation \ lexicon \ grafite_engine \ diff --git a/components/acic_procedural/.depend b/components/acic_procedural/.depend index 5f1cd6590..61c8bfef8 100644 --- a/components/acic_procedural/.depend +++ b/components/acic_procedural/.depend @@ -1,10 +1,12 @@ -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi +proceduralClassify.cmo: proceduralClassify.cmi +proceduralClassify.cmx: proceduralClassify.cmi +proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi +proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralConversion.cmi proceduralConversion.cmx: proceduralConversion.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ - cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ - cicClassify.cmx acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ + proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ + proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/.depend.opt b/components/acic_procedural/.depend.opt index 5f1cd6590..61c8bfef8 100644 --- a/components/acic_procedural/.depend.opt +++ b/components/acic_procedural/.depend.opt @@ -1,10 +1,12 @@ -cicClassify.cmo: cicClassify.cmi -cicClassify.cmx: cicClassify.cmi +proceduralClassify.cmo: proceduralClassify.cmi +proceduralClassify.cmx: proceduralClassify.cmi +proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi +proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralConversion.cmi proceduralConversion.cmx: proceduralConversion.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -acic2Procedural.cmo: proceduralTypes.cmi proceduralConversion.cmi \ - cicClassify.cmi acic2Procedural.cmi -acic2Procedural.cmx: proceduralTypes.cmx proceduralConversion.cmx \ - cicClassify.cmx acic2Procedural.cmi +acic2Procedural.cmo: proceduralTypes.cmi proceduralMode.cmi \ + proceduralConversion.cmi proceduralClassify.cmi acic2Procedural.cmi +acic2Procedural.cmx: proceduralTypes.cmx proceduralMode.cmx \ + proceduralConversion.cmx proceduralClassify.cmx acic2Procedural.cmi diff --git a/components/acic_procedural/Makefile b/components/acic_procedural/Makefile index 3435f01d0..ae52b5a20 100644 --- a/components/acic_procedural/Makefile +++ b/components/acic_procedural/Makefile @@ -2,7 +2,8 @@ PACKAGE = acic_procedural PREDICATES = INTERFACE_FILES = \ - cicClassify.mli \ + proceduralClassify.mli \ + proceduralMode.mli \ proceduralConversion.mli \ proceduralTypes.mli \ acic2Procedural.mli \ diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index e26dd68a2..b1cbc74ab 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -34,8 +34,10 @@ module HObj = HelmLibraryObjects module A = Cic2acic module Ut = CicUtil module E = CicEnvironment +module PER = ProofEngineReduction -module Cl = CicClassify +module Cl = ProceduralClassify +module M = ProceduralMode module T = ProceduralTypes module Cn = ProceduralConversion @@ -153,6 +155,14 @@ let assumed_premise = "ASSUMED" let expanded_premise = "EXPANDED" +let convert st v = + match get_inner_types st v with + | Some (st, et) -> + let cst, cet = cic st, cic et in + if PER.alpha_equivalence cst cet then [] else + [T.Change (st, et, "")] + | None -> [] + let eta_expand n t = let ty = C.AImplicit ("", None) in let name i = Printf.sprintf "%s%u" expanded_premise i in @@ -221,12 +231,12 @@ and mk_fwd_proof st dtext name = function | C.AAppl (_, hd :: tl) as v -> if is_rewrite_right hd then mk_fwd_rewrite st dtext name tl true else if is_rewrite_left hd then mk_fwd_rewrite st dtext name tl false else + let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in begin match get_inner_types st v with - | Some (ity, _) -> + | Some (ity, _) when M.bkd st.context ty -> let qs = [[T.Id ""]; mk_proof (next st) v] in [T.Branch (qs, ""); T.Cut (name, ity, dtext)] - | None -> - let ty, _ = TC.type_of_aux' [] st.context (cic hd) Un.empty_ugraph in + | _ -> let (classes, rc) as h = Cl.classify st.context ty in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in [T.LetIn (name, v, dtext ^ text)] @@ -280,19 +290,19 @@ and mk_proof st = function let synth = Cl.S.add 1 synth in let qs = mk_bkd_proofs (next st) synth classes tl in if is_rewrite_right hd then - List.rev script @ + List.rev script @ convert st t @ [T.Rewrite (false, what, None, dtext); T.Branch (qs, "")] else if is_rewrite_left hd then - List.rev script @ + List.rev script @ convert st t @ [T.Rewrite (true, what, None, dtext); T.Branch (qs, "")] else let using = Some hd in - List.rev script @ + List.rev script @ convert st t @ [T.Elim (what, using, dtext ^ text); T.Branch (qs, "")] | _ -> let qs = mk_bkd_proofs (next st) synth classes tl in let script, hd = mk_atomic st dtext hd in - List.rev script @ + List.rev script @ convert st t @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else [T.Apply (t, dtext)] diff --git a/components/acic_procedural/cicClassify.ml b/components/acic_procedural/proceduralClassify.ml similarity index 100% rename from components/acic_procedural/cicClassify.ml rename to components/acic_procedural/proceduralClassify.ml diff --git a/components/acic_procedural/cicClassify.mli b/components/acic_procedural/proceduralClassify.mli similarity index 95% rename from components/acic_procedural/cicClassify.mli rename to components/acic_procedural/proceduralClassify.mli index 3d92134df..79a8f4d9f 100644 --- a/components/acic_procedural/cicClassify.mli +++ b/components/acic_procedural/proceduralClassify.mli @@ -32,3 +32,5 @@ val classify: Cic.context -> Cic.term -> S.t list * conclusion val to_string: S.t list * conclusion -> string val overlaps: S.t -> S.t -> bool + +val split: Cic.context -> Cic.term -> Cic.term list * int diff --git a/components/acic_procedural/proceduralMode.ml b/components/acic_procedural/proceduralMode.ml new file mode 100644 index 000000000..bd2c3a438 --- /dev/null +++ b/components/acic_procedural/proceduralMode.ml @@ -0,0 +1,45 @@ +(* 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 Cl = ProceduralClassify + +let is_const = function + | C.Sort _ + | C.Const _ + | C.Var _ + | C.MutInd _ + | C.MutConstruct _ -> true + | _ -> false + +let rec is_appl b = function + | C.Appl (hd :: tl) -> List.fold_left is_appl (is_const hd) tl + | t when is_const t -> b + | C.Rel _ -> b + | _ -> false + +let bkd c t = + let ts, _ = Cl.split c t in + is_appl true (List.hd ts) diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli new file mode 100644 index 000000000..dc382693f --- /dev/null +++ b/components/acic_procedural/proceduralMode.mli @@ -0,0 +1,26 @@ +(* 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/. + *) + +val bkd: Cic.context -> Cic.term -> bool diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index 53605271d..1d8bbbc21 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -68,13 +68,14 @@ let is_atomic = function (****************************************************************************) -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 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 inferred = Cic.annterm type step = Note of note | Theorem of name * what * note @@ -87,6 +88,7 @@ type step = Note of note | Elim of what * using option * note | Apply of what * note | Whd of count * note + | Change of inferred * what * note | Branch of step list list * note (* annterm constructors *****************************************************) @@ -149,6 +151,11 @@ let mk_whd i = let tactic = G.Reduce (floc, `Whd, pattern) in mk_tactic tactic +let mk_change t = + let pattern = None, [], Some hole in + let tactic = G.Change (floc, pattern, 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)) @@ -173,6 +180,7 @@ let rec render_step sep a = function | 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) | Whd (c, s) -> mk_note s :: cont sep (mk_whd c :: a) + | Change (t, _, s) -> mk_note s :: cont sep (mk_change t :: a) | Branch ([], s) -> a | Branch ([ps], s) -> render_steps sep a ps | Branch (pss, s) -> diff --git a/components/acic_procedural/proceduralTypes.mli b/components/acic_procedural/proceduralTypes.mli index dfd82df12..9fb7f3035 100644 --- a/components/acic_procedural/proceduralTypes.mli +++ b/components/acic_procedural/proceduralTypes.mli @@ -35,13 +35,14 @@ val is_atomic:Cic.annterm -> bool (****************************************************************************) -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 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 inferred = Cic.annterm type step = Note of note | Theorem of name * what * note @@ -54,12 +55,13 @@ type step = Note of note | Elim of what * using option * note | Apply of what * note | Whd of count * note + | Change of inferred * what * note | Branch of step list list * note val render_steps: - (what, 'a, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> + (what, inferred, [> `Whd] as 'b, what CicNotationPt.obj, name) GrafiteAst.statement list -> step list -> - (what, 'a, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list + (what, inferred, 'b, what CicNotationPt.obj, name) GrafiteAst.statement list val count_steps: int -> step list -> int diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml index 69ae68aee..d110bda9a 100644 --- a/components/content_pres/cicNotationParser.ml +++ b/components/content_pres/cicNotationParser.ml @@ -452,6 +452,8 @@ EXTEND id, Some typ | arg = single_arg -> arg, None | SYMBOL "_" -> Ast.Ident ("_", None), None + | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN -> + Ast.Ident ("_", None), Some typ ] ]; match_pattern: [ diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 3ef39d0c5..1012fc935 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -474,8 +474,8 @@ let exact_tac ~term = mk_tactic (exact_tac ~term) (* not really "primitive" tactics .... *) -let elim_tac ~term = - let elim_tac ~term (proof, goal) = +let elim_tac ?using ~term = + let elim_tac (proof, goal) = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in @@ -517,7 +517,10 @@ let elim_tac ~term = in U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in - let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in + let eliminator_ref = match using with + | None -> C.Const (eliminator_uri,exp_named_subst) + | Some t -> t + in let ety,_ = T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in let rec find_args_no = @@ -557,7 +560,7 @@ let elim_tac ~term = in proof'', patched_new_goals in - mk_tactic (elim_tac ~term) + mk_tactic elim_tac ;; let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = @@ -655,14 +658,14 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?depth ?using what = - Tacticals.then_ ~start:(elim_tac ~term:what) + Tacticals.then_ ~start:(elim_tac ?using ~term:what) ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ()) ;; (* The simplification is performed only on the conclusion *) let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?depth ?using what = - Tacticals.then_ ~start:(elim_tac ~term:what) + Tacticals.then_ ~start:(elim_tac ?using ~term:what) ~continuation: (Tacticals.thens ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ()) -- 2.39.2