X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FprimitiveTactics.ml;h=e7632ebf4bf40c4bad2678b5ea23916b9e899796;hb=35e102fec6bad146fee425f299a93520e657e7c2;hp=70502d1b28030650e0540348f5582b9b9ba06369;hpb=eeed0d603ddadba6b5ee5041e87794051b9283dd;p=helm.git diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 70502d1b2..e7632ebf4 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -62,11 +62,11 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = collect_context ctx (howmany - 1) do_whd t in (context',ty,C.Lambda(n',s,bo)) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,sty,t) -> let (context',ty,bo) = - collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t + collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t in - (context',ty,C.LetIn(n,s,bo)) + (context',ty,C.LetIn(n,s,sty,bo)) | _ as t -> if howmany <= 0 then let irl = @@ -102,7 +102,7 @@ let eta_expand metasenv context t arg = | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t) | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t) - | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t) + | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t) | C.Appl l -> C.Appl (List.map (aux n) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = aux_exp_named_subst n exp_named_subst in @@ -159,15 +159,13 @@ let classify_metas newmeta in_subst_domain subst_in metasenv = match entry with Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in canonical_context' s)) - | Some (n,Cic.Def (s,None)) -> - Some (n,Cic.Def ((subst_in canonical_context' s),None)) | None -> None - | Some (n,Cic.Def (bo,Some ty)) -> + | Some (n,Cic.Def (bo,ty)) -> Some (n, Cic.Def (subst_in canonical_context' bo, - Some (subst_in canonical_context' ty))) + subst_in canonical_context' ty)) in entry'::canonical_context' ) canonical_context [] @@ -409,15 +407,8 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: CicMkImplicit.identity_relocation_list_for_metavariable context in let newmeta1ty = CicSubstitution.lift 1 ty in -(* This is the pre-letin implementation - let bo' = - C.Appl - [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ; - C.Meta (newmeta2,irl2)] - in -*) let bo' = - Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1)) + Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1)) in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo' @@ -444,19 +435,19 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: raise (ProofEngineTypes.Fail (lazy "You can't letin a term containing the current goal")); - let _,_ = + let tty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in let context_for_newmeta = - (Some (fresh_name,C.Def (term,None)))::context in + (Some (fresh_name,C.Def (term,tty)))::context in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in + let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in let (newproof, _) = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] @@ -517,12 +508,12 @@ let mk_predicate_for_elim | _ -> assert false in (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) - let rec mk_pred metasenv context' pred arg' = function + let rec mk_pred metasenv context' pred arg' cpattern' = function | [] -> metasenv, pred, arg' | arg :: tail -> (* FG: we find the predicate for the eliminator as in the rewrite tactic ****) - let argty, _ugraph = TC.type_of_aux' metasenv context' arg ugraph in - let argty = CicReduction.whd context' argty in + let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in + let argty = CicReduction.whd context argty in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context' C.Anonymous ~typ:argty @@ -532,7 +523,7 @@ let mk_predicate_for_elim let distance = List.length c - List.length context in S.lift distance arg, m, u in - let pattern = Some lazy_term, [], Some cpattern in + let pattern = Some lazy_term, [], Some cpattern' in let subst, metasenv, _ugraph, _conjecture, selected_terms = ProofEngineHelpers.select ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern @@ -545,10 +536,13 @@ let mk_predicate_for_elim let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in let pred = MS.apply_subst subst pred in let pred = C.Lambda (fresh_name, argty, pred) in - mk_pred metasenv (hyp :: context') pred arg' tail + let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in + mk_pred metasenv (hyp :: context') pred arg' cpattern' tail in - let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in - HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); + let metasenv, pred, arg = + mk_pred metasenv context goal arg cpattern (List.rev actual_args) + in + HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); metasenv, pred, arg, actual_args let beta_after_elim_tac upto predicate = @@ -599,9 +593,9 @@ let beta_after_elim_tac upto predicate = | C.Lambda (_, s, t) -> let s, t = gen_term k s, gen_term (succ k) t in if is_meta [s; t] then meta else C.Lambda (anon, s, t) - | C.LetIn (_, s, t) -> - let s, t = gen_term k s, gen_term (succ k) t in - if is_meta [s; t] then meta else C.LetIn (anon, s, t) + | C.LetIn (_, s, ty, t) -> + let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in + if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t) | C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl) | C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl) in @@ -870,22 +864,3 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres [ReductionTactics.simpl_tac ~pattern:(ProofEngineTypes.conclusion_pattern None)]) ;; - -(* FG: insetrts a "hole" in the context (derived from letin_tac) *) - -let letout_tac = - let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in - let term = C.Sort C.Set in - let letout_tac (proof, goal) = - let curi, metasenv, _subst, pbo, pty, attrs = proof in - let metano, context, ty = CicUtil.lookup_meta goal metasenv in - let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in - let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in - let context_for_newmeta = None :: context in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in - let newmetaty = CicSubstitution.lift 1 ty in - let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in - let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in - newproof, [newmeta] - in - PET.mk_tactic letout_tac