From: Ferruccio Guidi Date: Wed, 14 Feb 2007 17:10:16 +0000 (+0000) Subject: Procedural : some improvements X-Git-Tag: make_still_working~6455 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=977e819edc19f6c25d9f05c2fafe72c63ad301fd;p=helm.git Procedural : some improvements PrimitiveTactics : tentative implementation of using clause in elim CicNotationParser: noe declarations of the form (_:t) are parsable --- diff --git a/helm/software/components/METAS/meta.helm-acic_procedural.src b/helm/software/components/METAS/meta.helm-acic_procedural.src index e91f1f7d8..f696baea6 100644 --- a/helm/software/components/METAS/meta.helm-acic_procedural.src +++ b/helm/software/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/helm/software/components/Makefile b/helm/software/components/Makefile index 9f42d0dad..1b38db7e7 100644 --- a/helm/software/components/Makefile +++ b/helm/software/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/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index 5f1cd6590..61c8bfef8 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/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/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index 5f1cd6590..61c8bfef8 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/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/helm/software/components/acic_procedural/Makefile b/helm/software/components/acic_procedural/Makefile index 3435f01d0..ae52b5a20 100644 --- a/helm/software/components/acic_procedural/Makefile +++ b/helm/software/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/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index e26dd68a2..b1cbc74ab 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/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/helm/software/components/acic_procedural/cicClassify.ml b/helm/software/components/acic_procedural/cicClassify.ml deleted file mode 100644 index 4cfd47e5a..000000000 --- a/helm/software/components/acic_procedural/cicClassify.ml +++ /dev/null @@ -1,149 +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 C = Cic -module R = CicReduction -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 id x = x - -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 c t = - let add s v c = Some (s, C.Decl v) :: c in - let rec aux whd a n c = function - | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t - | v when whd -> v :: a, n - | v -> aux true a n c (R.whd ~delta:true c v) - in - aux false [] 0 c 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 c t = -try - let vs, h = split c 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 = if j < h then S.union (fst b.(j)) else id 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 - if j < h then - let unused, inverse = b.(j) in - b.(j) <- unused, S.add i inverse - else (); - 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 -with Invalid_argument _ -> failwith "Classify.classify" - -let overlaps s1 s2 = - let predicate x = S.mem x s1 in - S.exists predicate s2 diff --git a/helm/software/components/acic_procedural/cicClassify.mli b/helm/software/components/acic_procedural/cicClassify.mli deleted file mode 100644 index 3d92134df..000000000 --- a/helm/software/components/acic_procedural/cicClassify.mli +++ /dev/null @@ -1,34 +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 S : Set.S with type elt = int - -type conclusion = (int * int) option - -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 diff --git a/helm/software/components/acic_procedural/proceduralClassify.ml b/helm/software/components/acic_procedural/proceduralClassify.ml new file mode 100644 index 000000000..4cfd47e5a --- /dev/null +++ b/helm/software/components/acic_procedural/proceduralClassify.ml @@ -0,0 +1,149 @@ +(* 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 R = CicReduction +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 id x = x + +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 c t = + let add s v c = Some (s, C.Decl v) :: c in + let rec aux whd a n c = function + | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t + | v when whd -> v :: a, n + | v -> aux true a n c (R.whd ~delta:true c v) + in + aux false [] 0 c 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 c t = +try + let vs, h = split c 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 = if j < h then S.union (fst b.(j)) else id 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 + if j < h then + let unused, inverse = b.(j) in + b.(j) <- unused, S.add i inverse + else (); + 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 +with Invalid_argument _ -> failwith "Classify.classify" + +let overlaps s1 s2 = + let predicate x = S.mem x s1 in + S.exists predicate s2 diff --git a/helm/software/components/acic_procedural/proceduralClassify.mli b/helm/software/components/acic_procedural/proceduralClassify.mli new file mode 100644 index 000000000..79a8f4d9f --- /dev/null +++ b/helm/software/components/acic_procedural/proceduralClassify.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.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/helm/software/components/acic_procedural/proceduralMode.ml b/helm/software/components/acic_procedural/proceduralMode.ml new file mode 100644 index 000000000..bd2c3a438 --- /dev/null +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralMode.mli b/helm/software/components/acic_procedural/proceduralMode.mli new file mode 100644 index 000000000..dc382693f --- /dev/null +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 53605271d..1d8bbbc21 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/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/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index dfd82df12..9fb7f3035 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/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/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 69ae68aee..d110bda9a 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/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/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 3ef39d0c5..1012fc935 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/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 ())