X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FprimitiveTactics.ml;h=9f9da081830c94da80fdba1bde8df4d3e30e9333;hb=6a25db65c9a787daf7344e3b166b2d798b1ff1a5;hp=5fb8d4ae1eb56f88522cb14133c1a7c846a60e69;hpb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;p=helm.git diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 5fb8d4ae1..9f9da0818 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -25,7 +25,6 @@ (* $Id$ *) -open ProofEngineHelpers open ProofEngineTypes exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple @@ -232,7 +231,8 @@ let let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - saturate_term newmeta' metasenv' context termty goal_arity in + TermUtil.saturate_term newmeta' metasenv' context termty + goal_arity in let subst,newmetasenv',_ = CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph in @@ -246,14 +246,14 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_tac_verbose_with_subst ~term (proof, goal) = +let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof in + let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with C.Var (uri,exp_named_subst) -> @@ -318,27 +318,28 @@ let apply_tac_verbose_with_subst ~term (proof, goal) = CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst) in let (newproof, newmetasenv''') = - subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv'' + ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in + newmetasenv'' in - (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *) - (newproof, - List.map (function (i,_,_) -> i) new_uninstantiatedmetas)) + let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in + subst, + (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas), + max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst) (* ALB *) -let apply_tac_verbose_with_subst ~term status = +let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status = try (* apply_tac_verbose ~term status *) - apply_tac_verbose_with_subst ~term status + apply_with_subst ~term ~subst ~maxmeta status (* TODO cacciare anche altre eccezioni? *) with | CicUnification.UnificationFailure msg - | CicTypeChecker.TypeCheckerFailure msg -> - raise (Fail msg) + | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg) (* ALB *) let apply_tac_verbose ~term status = - let subst, status = apply_tac_verbose_with_subst ~term status in + let subst, status, _ = apply_with_subst ~term status in (CicMetaSubst.apply_subst subst), status let apply_tac ~term status = snd (apply_tac_verbose ~term status) @@ -366,12 +367,13 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_ let module R = CicReduction in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof in + let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let (context',ty',bo') = lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback in let (newproof, _) = - subst_meta_in_proof proof metano bo' [newmeta,context',ty'] + ProofEngineHelpers.subst_meta_in_proof proof metano bo' + [newmeta,context',ty'] in (newproof, [newmeta]) in @@ -385,7 +387,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: let module C = Cic in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta1 = new_meta_of_proof ~proof in + let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in @@ -405,7 +407,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: C.Meta (newmeta2,irl2)] in let (newproof, _) = - subst_meta_in_proof proof metano bo' + ProofEngineHelpers.subst_meta_in_proof proof metano bo' [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty]; in (newproof, [newmeta1 ; newmeta2]) @@ -419,10 +421,19 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: = let module C = Cic in let curi,metasenv,pbo,pty = proof in + (* occur check *) + let occur i t = + let m = CicUtil.metas_of_term t in + List.exists (fun (j,_) -> i=j) m + in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let _,_ = (* TASSI: FIXME *) + if occur metano term then + raise + (ProofEngineTypes.Fail (lazy + "You can't letin a term containing the current goal")); + let _,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let newmeta = new_meta_of_proof ~proof 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 = @@ -434,7 +445,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let newmetaty = CicSubstitution.lift 1 ty in let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in let (newproof, _) = - subst_meta_in_proof + ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in (newproof, [newmeta]) @@ -454,7 +465,7 @@ let exact_tac ~term = if b then begin let (newproof, metasenv') = - subst_meta_in_proof proof metano term [] in + ProofEngineHelpers.subst_meta_in_proof proof metano term [] in (newproof, []) end else @@ -474,7 +485,7 @@ let elim_tac ~term = let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = - ProofEngineHelpers.saturate_term + 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 let uri,exp_named_subst,typeno,args = @@ -549,6 +560,100 @@ let elim_tac ~term = mk_tactic (elim_tac ~term) ;; +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 U = UriManager in + let module R = CicReduction in + let module C = Cic in + let (curi,metasenv,proofbo,proofty) = 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 = CicReduction.whd context termty in + 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 + let uri,exp_named_subst,typeno,args = + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> + (uri,exp_named_subst,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate + in + let paramsno,patterns = + match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + C.InductiveDefinition (tys,_,paramsno,_),_ -> + let _,_,_,cl = List.nth tys typeno in + let rec aux n context t = + match n,CicReduction.whd context t with + 0,C.Prod (name,source,target) -> + let fresh_name = + mk_fresh_name_callback metasenv' context name + (*CSC: WRONG TYPE HERE: I can get a "bad" name*) + ~typ:source + in + C.Lambda (fresh_name,C.Implicit None, + aux 0 (Some (fresh_name,C.Decl source)::context) target) + | n,C.Prod (name,source,target) -> + let fresh_name = + mk_fresh_name_callback metasenv' context name + (*CSC: WRONG TYPE HERE: I can get a "bad" name*) + ~typ:source + in + aux (n-1) (Some (fresh_name,C.Decl source)::context) target + | 0,_ -> C.Implicit None + | _,_ -> assert false + in + paramsno, + List.map (function (_,cty) -> aux paramsno context cty) cl + | _ -> assert false + in + let outtype = + let target = + C.Lambda (C.Name "fixme",C.Implicit None, + ProofEngineReduction.replace_lifting + ~equality:(ProofEngineReduction.alpha_equivalence) + ~what:[CicSubstitution.lift (paramsno+1) term] + ~with_what:[C.Rel (paramsno+1)] + ~where:(CicSubstitution.lift (paramsno+1) ty)) + in + let rec add_lambdas = + function + 0 -> target + | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1)) + in + add_lambdas paramsno + in + let term_to_refine = + C.MutCase (uri,typeno,outtype,term,patterns) + in +prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context); + let refined_term,_,metasenv'',_ = + CicRefine.type_of_aux' metasenv' context term_to_refine + CicUniv.empty_ugraph + in + let new_goals = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + let proof' = curi,metasenv'',proofbo,proofty in + let proof'', new_goals' = + 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 = + let (_,metasenv''',_,_) = proof'' in + List.filter + (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' + ) new_goals @ new_goals' + in + proof'', patched_new_goals + in + mk_tactic (cases_tac ~term) +;; + + let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ?depth ?using what = Tacticals.then_ ~start:(elim_tac ~term:what) @@ -571,19 +676,19 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres module C = Cic -let letout_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, pbo, pty = proof in let metano, context, ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof 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, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in + let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in newproof, [newmeta] in mk_tactic letout_tac