From: Ferruccio Guidi Date: Fri, 16 Mar 2007 18:39:27 +0000 (+0000) Subject: elim tactic: it needs two arguments, a term as well as a pattern X-Git-Tag: 0.4.95@7852~562 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2a39b3fe15889f379932c642f4775a5f8e756022;p=helm.git elim tactic: it needs two arguments, a term as well as a pattern CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce Procedural: refactoring --- diff --git a/components/acic_procedural/.depend b/components/acic_procedural/.depend index 8cb9645ae..3bb617fbd 100644 --- a/components/acic_procedural/.depend +++ b/components/acic_procedural/.depend @@ -2,12 +2,10 @@ proceduralPreprocess.cmo: proceduralPreprocess.cmi proceduralPreprocess.cmx: proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi -proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi -proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \ - proceduralMode.cmi -proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \ - proceduralMode.cmi +proceduralClassify.cmo: proceduralClassify.cmi +proceduralClassify.cmx: proceduralClassify.cmi +proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi +proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ proceduralMode.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ diff --git a/components/acic_procedural/.depend.opt b/components/acic_procedural/.depend.opt index 8cb9645ae..3bb617fbd 100644 --- a/components/acic_procedural/.depend.opt +++ b/components/acic_procedural/.depend.opt @@ -2,12 +2,10 @@ proceduralPreprocess.cmo: proceduralPreprocess.cmi proceduralPreprocess.cmx: proceduralPreprocess.cmi proceduralTypes.cmo: proceduralTypes.cmi proceduralTypes.cmx: proceduralTypes.cmi -proceduralClassify.cmo: proceduralPreprocess.cmi proceduralClassify.cmi -proceduralClassify.cmx: proceduralPreprocess.cmx proceduralClassify.cmi -proceduralMode.cmo: proceduralPreprocess.cmi proceduralClassify.cmi \ - proceduralMode.cmi -proceduralMode.cmx: proceduralPreprocess.cmx proceduralClassify.cmx \ - proceduralMode.cmi +proceduralClassify.cmo: proceduralClassify.cmi +proceduralClassify.cmx: proceduralClassify.cmi +proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi +proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralTypes.cmi proceduralPreprocess.cmi \ proceduralMode.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralTypes.cmx proceduralPreprocess.cmx \ diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index dbdfb9792..d6638b3f0 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -35,6 +35,7 @@ module HObj = HelmLibraryObjects module A = Cic2acic module Ut = CicUtil module E = CicEnvironment +module PEH = ProofEngineHelpers module PER = ProofEngineReduction module P = ProceduralPreprocess @@ -275,7 +276,7 @@ and mk_proof st = function let script = if proceed then let ty = get_type "TC2" st hd in let (classes, rc) as h = Cl.classify st.context ty in - let premises, _ = P.split st.context ty in + let premises, _ = PEH.split_with_whd (st.context, ty) in assert (List.length classes - List.length tl = 0); let synth = I.S.singleton 0 in let text = Printf.sprintf "%u %s" (List.length classes) (Cl.to_string h) in diff --git a/components/acic_procedural/proceduralClassify.ml b/components/acic_procedural/proceduralClassify.ml index 2fd2d979d..d21c14601 100644 --- a/components/acic_procedural/proceduralClassify.ml +++ b/components/acic_procedural/proceduralClassify.ml @@ -23,11 +23,10 @@ * http://cs.unibo.it/helm/. *) -module C = Cic -module D = Deannotate -module I = CicInspect - -module P = ProceduralPreprocess +module C = Cic +module D = Deannotate +module I = CicInspect +module PEH = ProofEngineHelpers type conclusion = (int * int) option @@ -57,15 +56,15 @@ let out_table b = let id x = x let classify_conclusion = function - | C.Rel i -> Some (i, 0) - | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl) - | _ -> None + | _, 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 = P.split c t in + let vs, h = PEH.split_with_whd (c, t) in let rc = classify_conclusion (List.hd vs) in - let map (b, h) v = (I.get_rels_from_premise h v, I.S.empty) :: b, succ h in + let map (b, h) (_, v) = (I.get_rels_from_premise h v, I.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 = diff --git a/components/acic_procedural/proceduralMode.ml b/components/acic_procedural/proceduralMode.ml index 2b233a4bf..d2ddc6c98 100644 --- a/components/acic_procedural/proceduralMode.ml +++ b/components/acic_procedural/proceduralMode.ml @@ -23,15 +23,15 @@ * http://cs.unibo.it/helm/. *) -module C = Cic +module C = Cic +module PEH = ProofEngineHelpers -module P = ProceduralPreprocess module Cl = ProceduralClassify let is_eliminator = function - | _ :: C.MutInd _ :: _ -> true - | _ :: C.Appl (C.MutInd _ :: _) :: _ -> true - | _ -> false + | _ :: (_, C.MutInd _) :: _ -> true + | _ :: (_, C.Appl (C.MutInd _ :: _)) :: _ -> true + | _ -> false let is_const = function | C.Sort _ @@ -49,9 +49,9 @@ let rec is_appl b = function let bkd c t = let classes, rc = Cl.classify c t in - let premises, _ = P.split c t in + let premises, _ = PEH.split_with_whd (c, t) in match rc with | Some (i, j) when i > 1 && i <= List.length classes && is_eliminator premises -> true | _ -> - let ts, _ = P.split c t in - is_appl true (List.hd ts) + let _, conclusion = List.hd premises in + is_appl true conclusion diff --git a/components/acic_procedural/proceduralMode.mli b/components/acic_procedural/proceduralMode.mli index 2f0e7e9f4..b55188600 100644 --- a/components/acic_procedural/proceduralMode.mli +++ b/components/acic_procedural/proceduralMode.mli @@ -23,6 +23,6 @@ * http://cs.unibo.it/helm/. *) -val is_eliminator: Cic.term list -> bool +val is_eliminator: (Cic.context * Cic.term) list -> bool val bkd: Cic.context -> Cic.term -> bool diff --git a/components/acic_procedural/proceduralPreprocess.ml b/components/acic_procedural/proceduralPreprocess.ml index dcd4cb58b..d3e655da7 100644 --- a/components/acic_procedural/proceduralPreprocess.ml +++ b/components/acic_procedural/proceduralPreprocess.ml @@ -30,26 +30,17 @@ module Un = CicUniv module I = CicInspect module E = CicEnvironment module S = CicSubstitution -module Rd = CicReduction module TC = CicTypeChecker module Rf = CicRefine module DTI = DoubleTypeInference module HEL = HExtlib +module PEH = ProofEngineHelpers (* helper functions *********************************************************) let identity x = x let comp f g x = f (g x) - -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 (Rd.whd ~delta:true c v) - in - aux false [] 0 c t let get_type c t = try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty @@ -67,9 +58,9 @@ let refine c t = raise e let get_tail c t = - match split c t with - | hd :: _, _ -> hd - | _ -> assert false + match PEH.split_with_whd (c, t) with + | (_, hd) :: _, _ -> hd + | _ -> assert false let is_proof c t = match get_tail c (get_type c (get_type c t)) with @@ -159,8 +150,8 @@ let eta_expand g tys t = let lambda i ty t = C.Lambda (C.Name (name i), ty, t) in let arg i = C.Rel (succ i) in let rec aux i f a = function - | [] -> f, a - | ty :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl + | [] -> f, a + | (_, ty) :: tl -> aux (succ i) (comp f (lambda i ty)) (arg i :: a) tl in let n = List.length tys in let absts, args = aux 0 identity [] tys in @@ -174,7 +165,7 @@ let get_tys c decurry = let rec aux n = function (* | C.Appl (hd :: tl) -> aux (n + List.length tl) hd *) | t -> - let tys, _ = split c (get_type c t) in + let tys, _ = PEH.split_with_whd (c, get_type c t) in let _, tys = HEL.split_nth n (List.rev tys) in let tys, _ = HEL.split_nth decurry tys in tys @@ -251,7 +242,7 @@ and pp_appl g ht es c t = function pp_proof g ht es c x and pp_atomic g ht es c t = - let _, premsno = split c (get_type c t) in + let _, premsno = PEH.split_with_whd (c, get_type c t) in g t true premsno and pp_mutcase g ht es c uri tyno outty arg cases = @@ -265,14 +256,14 @@ and pp_mutcase g ht es c uri tyno outty arg cases = I.S.mem tyno (I.get_mutinds_of_uri uri t) in let map2 case (_, cty) = - let map (h, case, k) premise = + let map (h, case, k) (_, premise) = if h > 0 then pred h, case, k else if is_recursive premise then 0, add_abst k case, k + 2 else 0, case, succ k in - let premises, _ = split c cty in + let premises, _ = PEH.split_with_whd (c, cty) in let _, lifted_case, _ = List.fold_left map (lpsno, case, 1) (List.rev (List.tl premises)) in diff --git a/components/acic_procedural/proceduralPreprocess.mli b/components/acic_procedural/proceduralPreprocess.mli index 7bd55f4e2..6d66bf237 100644 --- a/components/acic_procedural/proceduralPreprocess.mli +++ b/components/acic_procedural/proceduralPreprocess.mli @@ -23,6 +23,4 @@ * http://cs.unibo.it/helm/. *) -val split: Cic.context -> Cic.term -> Cic.term list * int - val pp_obj: Cic.obj -> Cic.obj diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml index 3ef27ea40..b4d88169a 100644 --- a/components/acic_procedural/proceduralTypes.ml +++ b/components/acic_procedural/proceduralTypes.ml @@ -138,8 +138,8 @@ let mk_rewrite direction what where pattern = mk_tactic tactic let mk_elim what using pattern = - let pattern = Some what, [], Some pattern in - let tactic = G.Elim (floc, pattern, using, Some 0, []) in + let pattern = None, [], Some pattern in + let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in mk_tactic tactic let mk_apply t = diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml index f4880e426..6e963a274 100644 --- a/components/cic_proof_checking/cicReduction.ml +++ b/components/cic_proof_checking/cicReduction.ml @@ -1120,46 +1120,50 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce ?(delta=false) = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - let he''' = - match he'' with - Cic.Appl l -> Cic.Appl (l@tl') - | _ -> Cic.Appl (he''::tl') +let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = + HLog.warn (Printf.sprintf "inside head_beta_reduce %i %s" upto (CicPp.ppterm t)); + match upto with + 0 -> t + | n -> + match t with + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce ~delta ~upto:(upto - 1) he''' + | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te + | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition in - head_beta_reduce ~delta he''' - | Cic.Cast (te,_) -> head_beta_reduce ~delta te - | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> - let bo = - match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with - Cic.Constant (_,bo,_,_,_) -> bo - | Cic.Variable _ -> raise ReferenceToVariable - | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - in - (match bo with - None -> t - | Some bo -> - head_beta_reduce - ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) - | Cic.Const (uri,ens) as t when delta=true -> - let bo = - match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with - Cic.Constant (_,bo,_,_,_) -> bo - | Cic.Variable _ -> raise ReferenceToVariable - | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo - | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - in - (match bo with - None -> t - | Some bo -> - head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo)) - | t -> t + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~upto + ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) + | Cic.Const (uri,ens) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo)) + | t -> t (* let are_convertible ?subst ?metasenv context t1 t2 ugraph = diff --git a/components/cic_proof_checking/cicReduction.mli b/components/cic_proof_checking/cicReduction.mli index bee4607d5..82be7fd3f 100644 --- a/components/cic_proof_checking/cicReduction.mli +++ b/components/cic_proof_checking/cicReduction.mli @@ -38,6 +38,7 @@ val are_convertible : val normalize: ?delta:bool -> ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term -(* performs an head beta/cast reduction; the default is to not perform - delta reduction *) -val head_beta_reduce: ?delta:bool -> Cic.term -> Cic.term +(* performs head beta/(delta)/cast reduction; the default is to not perform + delta reduction; if provided, ~upto is the maximum number of beta redexes + reduced *) +val head_beta_reduce: ?delta:bool -> ?upto:int -> Cic.term -> Cic.term diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index b5e75712f..e88118303 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -55,8 +55,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Decompose of loc * 'ident list | Demodulate of loc | Destruct of loc * 'term - | Elim of loc * ('term, 'lazy_term, 'ident) pattern * 'term option * - int option * 'ident list + | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern * + int option * 'ident list | ElimType of loc * 'term * 'term option * int option * 'ident list | Exact of loc * 'term | Exists of loc diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index e8fd2fe02..d7ed16efd 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -99,10 +99,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = sprintf "decompose%s" (pp_intros_specs (None, names)) | Demodulate _ -> "demodulate" | Destruct (_, term) -> "destruct " ^ term_pp term - | Elim (_, pattern, using, num, idents) -> - sprintf "elim %s%s%s" - (pp_tactic_pattern pattern) + | Elim (_, what, using, pattern, num, idents) -> + sprintf "elim %s%s %s%s" + (term_pp what) (match using with None -> "" | Some term -> " using " ^ term_pp term) + (pp_tactic_pattern pattern) (pp_intros_specs (num, idents)) | ElimType (_, term, using, num, idents) -> sprintf "elim type " ^ term_pp term ^ diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 4c177fee7..51b86fa5e 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -87,9 +87,9 @@ let tactic_of_ast status ast = Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe | GrafiteAst.Destruct (_,term) -> Tactics.destruct term - | GrafiteAst.Elim (_, pattern, using, depth, names) -> + | GrafiteAst.Elim (_, what, using, pattern, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) - pattern + ~pattern what | GrafiteAst.ElimType (_, what, using, depth, names) -> Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 97f0d5e85..5748f0bbb 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -158,13 +158,15 @@ let disambiguate_tactic | GrafiteAst.Exact (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Exact (loc, cic) - | GrafiteAst.Elim (loc, pattern, Some using, depth, idents) -> - let pattern = disambiguate_pattern pattern in + | GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents) -> + let metasenv,what = disambiguate_term context metasenv what in let metasenv,using = disambiguate_term context metasenv using in - metasenv,GrafiteAst.Elim (loc, pattern, Some using, depth, idents) - | GrafiteAst.Elim (loc, pattern, None, depth, idents) -> let pattern = disambiguate_pattern pattern in - metasenv,GrafiteAst.Elim (loc, pattern, None, depth, idents) + metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents) + | GrafiteAst.Elim (loc, what, None, pattern, depth, idents) -> + let metasenv,what = disambiguate_term context metasenv what in + let pattern = disambiguate_pattern pattern in + metasenv,GrafiteAst.Elim (loc, what, None, pattern, depth, idents) | GrafiteAst.ElimType (loc, what, Some using, depth, idents) -> let metasenv,what = disambiguate_term context metasenv what in let metasenv,using = disambiguate_term context metasenv using in diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index dac05d7bd..3eb64d458 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -163,13 +163,14 @@ EXTEND | IDENT "demodulate" -> GrafiteAst.Demodulate loc | IDENT "destruct"; t = tactic_term -> GrafiteAst.Destruct (loc, t) - | IDENT "elim"; what = tactic_term; using = using; + | IDENT "elim"; what = tactic_term; using = using; + pattern = OPT pattern_spec; (num, idents) = intros_spec -> - let pattern = Some what, [], Some Ast.UserInput in - GrafiteAst.Elim (loc, pattern, using, num, idents) - | IDENT "elim"; pattern = pattern_spec; using = using; - (num, idents) = intros_spec -> - GrafiteAst.Elim (loc, pattern, using, num, idents) + let pattern = match pattern with + | None -> None, [], Some Ast.UserInput + | Some pattern -> pattern + in + GrafiteAst.Elim (loc, what, using, pattern, num, idents) | IDENT "elimType"; what = tactic_term; using = using; (num, idents) = intros_spec -> GrafiteAst.ElimType (loc, what, using, num, idents) diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 189cd9079..6c37acaa4 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -127,12 +127,11 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 = let metano,context,_ = CicUtil.lookup_meta goal metasenv in let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in let proof' = (n,metasenv,bo,ty,attrs) in - let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in ProofEngineTypes.apply_tactic ( Tacticals.thens ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)])) ~continuations: - [ Tactics.elim_intros pattern + [ Tactics.elim_intros (Cic.Rel 1) ~mk_fresh_name_callback: (let i = ref 0 in fun _ _ _ ~typ -> @@ -147,7 +146,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 = ;; let andelim t id1 t1 id2 t2 = - Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t)) + Tactics.elim_intros t ~mk_fresh_name_callback: (let i = ref 0 in fun _ _ _ ~typ -> @@ -251,8 +250,8 @@ let we_proceed_by_cases_on t pat = ;; let we_proceed_by_induction_on t pat = - let pattern = Some (fun c m u -> t, m, u), [], Some pat in - Tactics.elim_intros ~depth:0 pattern + let pattern = None, [], Some pat in + Tactics.elim_intros ~depth:0 ~pattern t ;; let case id ~params = diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml index 85eade2d0..f18d2b333 100644 --- a/components/tactics/eliminationTactics.ml +++ b/components/tactics/eliminationTactics.ml @@ -34,24 +34,11 @@ module T = Tacticals module PESR = ProofEngineStructuralRules module F = FreshNamesGenerator module PET = ProofEngineTypes -module H = ProofEngineHelpers module RT = ReductionTactics module E = CicEnvironment module R = CicReduction module Un = CicUniv - -(* from ProceduralClasify ***************************************************) - -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 - -(****************************************************************************) +module PEH = ProofEngineHelpers let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None @@ -64,9 +51,9 @@ let get_inductive_def uri = let is_not_recursive uri tyno tys = let map mutinds (_, ty) = (* FG: we can do much better here *) - let map mutinds t = I.S.union mutinds (I.get_mutinds_of_uri uri t) in + let map mutinds (_, t) = I.S.union mutinds (I.get_mutinds_of_uri uri t) in (**********************************) - let premises, _ = split [] ty in + let premises, _ = PEH.split_with_whd ([], ty) in List.fold_left map mutinds (List.tl premises) in let msg = "recursiveness check non implemented for mutually inductive types" in @@ -80,14 +67,14 @@ let rec check_type sorts metasenv context t = | C.MutInd (uri, tyno, _) as t -> let lpsno, tys = get_inductive_def uri in let _, inductive, arity, _ = List.nth tys tyno in - let _, psno = split [] arity in + let _, psno = PEH.split_with_whd ([], arity) in let not_relation = (lpsno = psno) in let not_recursive = is_not_recursive uri tyno tys in let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in - let sort = match split context ty_ty with - | C.Sort sort ::_ , _ -> CicPp.ppsort sort - | C.Meta _ :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ())) - | _ -> assert false + let sort = match PEH.split_with_whd (context, ty_ty) with + | (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort + | (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ())) + | _ -> assert false in let right_sort = List.mem sort sorts in if not_relation && inductive && not_recursive && right_sort then @@ -108,7 +95,7 @@ let rec scan_tac ~old_context_length ~index ~tactic = let _, context, _ = CicUtil.lookup_meta goal metasenv in let context_length = List.length context in let rec aux index = - match H.get_name context index with + match PEH.get_name context index with | _ when index <= 0 -> (proof, [goal]) | None -> aux (pred index) | Some what -> @@ -126,11 +113,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what = let (proof, goal) = status in let _, metasenv, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - let index, ty = H.lookup_type metasenv context what in - let pattern = PET.conclusion_pattern (Some (C.Rel index)) in + let index, ty = PEH.lookup_type metasenv context what in let tac = if check_type sorts metasenv context (S.lift index ty) then - T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern) + T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) ~continuation:(PESR.clear [what]) else let msg = "unexported elim_clear: not an decomposable type" in @@ -149,9 +135,8 @@ let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback in let elim_type_tac status = - let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in let tac = - T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac] + T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] in PET.apply_tactic tac status in diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 2c22aa5ec..664615724 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -30,6 +30,7 @@ open ProofEngineTypes exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple exception NotAnInductiveTypeToEliminate exception WrongUriToVariable of string +exception NotAnEliminator (* lambda_abstract newmeta ty *) (* returns a triple [bo],[context],[ty'] where *) @@ -477,21 +478,33 @@ let exact_tac ~term = mk_tactic (exact_tac ~term) (* not really "primitive" tactics .... *) -let elim_tac ?using pattern = + +module TC = CicTypeChecker +module U = UriManager +module R = CicReduction +module C = Cic +module PET = ProofEngineTypes +module PEH = ProofEngineHelpers +module PER = ProofEngineReduction +module MS = CicMetaSubst +module S = CicSubstitution +module T = Tacticals +module RT = ReductionTactics + +let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = let elim_tac (proof, goal) = - let module T = CicTypeChecker in - let module U = UriManager in - let module R = CicReduction in - let module C = Cic in - let (curi,metasenv,proofbo,proofty, attrs) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let term, metasenv, _ = match pattern with - | Some f, [], Some _ -> f context metasenv CicUniv.empty_ugraph - | _ -> assert false + let ugraph = CicUniv.empty_ugraph in + let curi, metasenv, proofbo, proofty, attrs = proof in + let conjecture = CicUtil.lookup_meta goal metasenv in + let metano, context, ty = conjecture in +(* let (term, metasenv, _ugraph), cpatt = match pattern with + | Some f, [], Some cpatt -> f context metasenv ugraph, cpatt + | _ -> assert false in - let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in +*) + let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in let termty = CicReduction.whd context termty in - let (termty,metasenv',arguments,fresh_meta) = + let (termty,metasenv',arguments,_fresh_meta) = TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in let term = if arguments = [] then term else Cic.Appl (term::arguments) in @@ -505,14 +518,14 @@ let elim_tac ?using pattern = let eliminator_uri = let buri = U.buri_of_uri uri in let name = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let o,_ugraph = CicEnvironment.get_obj ugraph uri in match o with C.InductiveDefinition (tys,_,_,_) -> let (name,_,_,_) = List.nth tys typeno in name | _ -> assert false in - let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in + let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in let ext = match ty_ty with C.Sort C.Prop -> "_ind" @@ -528,47 +541,75 @@ let elim_tac ?using pattern = | 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 = - function - C.Prod (_,_,t) -> 1 + find_args_no t - | C.Cast (s,_) -> find_args_no s - | C.LetIn (_,_,t) -> 0 + find_args_no t - | _ -> 0 - in - let args_no = find_args_no ety in -(* we find the predicate for the eliminator as in the rewrite tactic ********) + let ety,_ugraph = + TC.type_of_aux' metasenv' context eliminator_ref ugraph in +(* FG: ADDED PART ***********************************************************) +(* FG: we can not assume eliminator is the default eliminator ***************) + let add_lambdas n t = + let rec aux n t = + if n <= 0 then t + else C.Lambda (C.Anonymous, C.Implicit None, aux (pred n) t) + in + aux n (S.lift n t) + in + let rec args_init n f = + if n <= 0 then [] else f n :: args_init (pred n) f + in + let splits, args_no = PEH.split_with_whd (context, ety) in + let pred_pos = match List.hd splits with + | _, C.Rel i when i > 1 && i <= args_no -> i + | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i + | _ -> raise NotAnEliminator + in + let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in + let termty_ty = + let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in + CicReduction.whd context termty_ty + in (* - let fresh_name = - FreshNamesGenerator.mk_fresh_name - ~subst:[] metasenv' context C.Anonymous ~typ:termty in - let lifted_gty = S.lift 1 ty in - let lifted_conjecture = - metano, (Some (fresh_name, Cic.Decl ty)) :: context, lifted_gty in - let lifted_t1 = S.lift 1 t1x in - let lifted_pattern = - let lifted_concl_pat = - match concl_pat with - | None -> None - | Some term -> Some (S.lift 1 term) in - Some (fun c m u -> - let distance = pred (List.length c - List.length context) in - S.lift distance lifted_t1, m, u),[],lifted_concl_pat - in + let metasenv', term, pred, upto = match cpatt, termty_ty with + | C.Implicit (Some `Hole), _ + | _, C.Sort C.Prop when lambdas = 0 -> metasenv', term, C.Implicit None, 0 + | _ -> +(* FG: we find the predicate for the eliminator as in the rewrite tactic ****) + let fresh_name = + FreshNamesGenerator.mk_fresh_name + ~subst:[] metasenv' context C.Anonymous ~typ:termty + in + let lazy_term c m u = + let distance = List.length c - List.length context in + S.lift distance term, m, u + in + let pattern = Some lazy_term, [], Some cpatt in + let subst, metasenv', _ugraph, _conjecture, selected_terms = + ProofEngineHelpers.select + ~metasenv:metasenv' ~ugraph ~conjecture ~pattern + in + let metasenv' = MS.apply_subst_metasenv subst metasenv' in + let map (_context_of_t, t) l = t :: l in + let what = List.fold_right map selected_terms [] in + let ty = MS.apply_subst subst ty in + let term = MS.apply_subst subst term in + let termty = MS.apply_subst subst termty in + let abstr_ty = PER.replace_with_rel_1_from ~equality:(==) ~what 1 ty in + let abstr_ty = MS.apply_subst subst abstr_ty in + let pred_body = C.Lambda (fresh_name, termty, abstr_ty) in + metasenv', term, add_lambdas (pred lambdas) pred_body, lambdas + in +(* FG: END OF ADDED PART ****************************************************) *) -(****************************************************************************) + let pred, upto = C.Implicit None, 0 in + let term_to_refine = - let rec make_tl base_case = - function - 0 -> [base_case] - | n -> (C.Implicit None)::(make_tl base_case (n - 1)) - in - C.Appl (eliminator_ref :: make_tl term (args_no - 1)) + let f n = + if n = pred_pos then pred else + if n = 1 then term else C.Implicit None + in + C.Appl (eliminator_ref :: args_init args_no f) in - let refined_term,_,metasenv'',_ = + let refined_term,_refined_termty,metasenv'',_ugraph = CicRefine.type_of_aux' metasenv' context term_to_refine - CicUniv.empty_ugraph + ugraph in let new_goals = ProofEngineHelpers.compare_metasenvs @@ -576,7 +617,7 @@ let elim_tac ?using pattern = in let proof' = curi,metasenv'',proofbo,proofty, attrs in let proof'', new_goals' = - apply_tactic (apply_tac ~term:refined_term) (proof',goal) + apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = @@ -585,20 +626,30 @@ let elim_tac ?using pattern = (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' ) new_goals @ new_goals' in - proof'', patched_new_goals + let res = proof'', patched_new_goals in + if upto = 0 then res else + let pattern = PET.conclusion_pattern None in + let continuation = + RT.simpl_tac ~pattern + (* RT.head_beta_reduce_tac ~delta:false ~upto ~pattern *) + in + let dummy_status = proof,goal in + PET.apply_tactic + (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation) + dummy_status in mk_tactic elim_tac ;; let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term = let cases_tac ~term (proof, goal) = - let module T = CicTypeChecker in + let module TC = CicTypeChecker in let module U = UriManager in let module R = CicReduction in let module C = Cic in let (curi,metasenv,proofbo,proofty, attrs) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = TermUtil.saturate_term @@ -684,15 +735,15 @@ 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 pattern = - Tacticals.then_ ~start:(elim_tac ?using pattern) + ?depth ?using ?pattern what = + Tacticals.then_ ~start:(elim_tac ?using ?pattern 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 pattern = - Tacticals.then_ ~start:(elim_tac ?using pattern) + ?depth ?using ?pattern what = + Tacticals.then_ ~start:(elim_tac ?using ?pattern what) ~continuation: (Tacticals.thens ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ()) @@ -703,8 +754,6 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres (* FG: insetrts a "hole" in the context (derived from letin_tac) *) -module C = Cic - let letout_tac = let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in let term = C.Sort C.Set in diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli index 2700fc27f..863df5eee 100644 --- a/components/tactics/primitiveTactics.mli +++ b/components/tactics/primitiveTactics.mli @@ -73,12 +73,12 @@ val letin_tac: val elim_intros_simpl_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> ?using:Cic.term -> - ProofEngineTypes.lazy_pattern -> + ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic val elim_intros_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> ?using:Cic.term -> - ProofEngineTypes.lazy_pattern -> + ?pattern:ProofEngineTypes.lazy_pattern -> Cic.term -> ProofEngineTypes.tactic val cases_intros_tac: diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index c2d0d15e1..177471c74 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/components/tactics/proofEngineHelpers.ml @@ -639,3 +639,12 @@ let get_rel context name = | _ :: tl -> aux (succ i) tl in aux 1 context + +let split_with_whd (c, t) = + let add s v c = Some (s, Cic.Decl v) :: c in + let rec aux whd a n c = function + | Cic.Prod (s, v, t) -> aux false ((c, v) :: a) (succ n) (add s v c) t + | v when whd -> (c, v) :: a, n + | v -> aux true a n c (CicReduction.whd c v) + in + aux false [] 0 c t diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli index f0b2c87f1..1ac3ee707 100644 --- a/components/tactics/proofEngineHelpers.mli +++ b/components/tactics/proofEngineHelpers.mli @@ -111,3 +111,12 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term val get_name: Cic.context -> int -> string option val get_rel: Cic.context -> string -> Cic.term option + +(* split_with_whd (c, t) takes a type t typed in the context c and returns + [(c_0, t_0); (c_1, t_1); ...; (c_n, t_n)], n where t_0 is the conclusion of + t and t_i is the premise of t accessed by Rel i in t_0. + Performes a whd on the conclusion before giving up. + Each t_i is returned with a context c_i in wich it is typed +*) +val split_with_whd: Cic.context * Cic.term -> + (Cic.context * Cic.term) list * int diff --git a/components/tactics/proofEngineReduction.ml b/components/tactics/proofEngineReduction.ml index dbc98f722..1b5922d1d 100644 --- a/components/tactics/proofEngineReduction.ml +++ b/components/tactics/proofEngineReduction.ml @@ -383,8 +383,9 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where = substaux 1 where ;; -(* This is the inverse of the subst function. *) -let subst_inv ~equality ~what = +(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" + up to the fact that the index to start from can be specified *) +let replace_with_rel_1_from ~equality ~what = let rec find_image t = function | [] -> false | hd :: tl -> equality t hd || find_image t tl @@ -392,7 +393,7 @@ let subst_inv ~equality ~what = let rec subst_term k t = if find_image t what then C.Rel k else inspect_term k t and inspect_term k = function - | C.Rel n -> if n < k then C.Rel n else C.Rel (succ n) + | C.Rel i -> if i < k then C.Rel i else C.Rel (succ i) | C.Sort _ as t -> t | C.Implicit _ as t -> t | C.Var (uri, enss) -> diff --git a/components/tactics/proofEngineReduction.mli b/components/tactics/proofEngineReduction.mli index 39beb84aa..78f4b7f4c 100644 --- a/components/tactics/proofEngineReduction.mli +++ b/components/tactics/proofEngineReduction.mli @@ -65,7 +65,9 @@ val replace_lifting_csc : int -> equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> with_what:Cic.term list -> where:Cic.term -> Cic.term -val subst_inv : +(* This is like "replace_lifting_csc 1 ~with_what:[Rel 1; ... ; Rel 1]" + up to the fact that the index to start from can be specified *) +val replace_with_rel_1_from : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> int -> Cic.term -> Cic.term val reduce : Cic.context -> Cic.term -> Cic.term diff --git a/components/tactics/reductionTactics.ml b/components/tactics/reductionTactics.ml index 754b2c0c5..5afc67269 100644 --- a/components/tactics/reductionTactics.ml +++ b/components/tactics/reductionTactics.ml @@ -118,6 +118,17 @@ let normalize_tac ~pattern = mk_tactic (reduction_tac ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern) +let head_beta_reduce_tac ?delta ?upto ~pattern = + begin match upto with + | Some upto -> + HLog.warn (Printf.sprintf "inside head_beta_reduce_tac %i" upto) + | None -> HLog.warn (Printf.sprintf "inside head_beta_reduce_tac none") + end; + mk_tactic (reduction_tac + ~reduction: + (const_lazy_reduction + (fun _context -> CicReduction.head_beta_reduce ?delta ?upto)) ~pattern) + exception NotConvertible (* Note: this code is almost identical to reduction_tac and diff --git a/components/tactics/reductionTactics.mli b/components/tactics/reductionTactics.mli index 16e2bc23c..62200df69 100644 --- a/components/tactics/reductionTactics.mli +++ b/components/tactics/reductionTactics.mli @@ -27,6 +27,7 @@ val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic +val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic (* The default of term is the thesis of the goal to be prooved *) val unfold_tac: diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 8cca5aee0..4f2908706 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Mar 12 13:47:11 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Mar 16 19:03:48 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -33,11 +33,15 @@ val destruct : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> - ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic + ?using:Cic.term -> + ?pattern:ProofEngineTypes.lazy_pattern -> + Cic.term -> ProofEngineTypes.tactic val elim_intros_simpl : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> - ?using:Cic.term -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic + ?using:Cic.term -> + ?pattern:ProofEngineTypes.lazy_pattern -> + Cic.term -> ProofEngineTypes.tactic val elim_type : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml index 83fee2e15..684e1fa2f 100644 --- a/matita/matitaGui.ml +++ b/matita/matitaGui.ml @@ -990,7 +990,8 @@ class gui () = connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); connect_button tbar#elimButton (tac_w_term - (A.Elim (loc, (Some hole, [], Some CicNotationPt.UserInput), None, None, []))); + (let pattern = None, [], Some CicNotationPt.UserInput in + A.Elim (loc, hole, None, pattern, None, []))); connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, []))); connect_button tbar#splitButton (tac (A.Split loc));