X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FprimitiveTactics.ml;h=1012fc9355b931ae19a770a9abc90b9f1a54f430;hb=cfbcef4637ff26ac4dfefe41bf2df29222e80138;hp=9baf829ea940d2bad3c61d71ebfdea8781043f34;hpb=45d71beffd253ffd767a9afbfcec5c4f44afd8a8;p=helm.git diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 9baf829ea..1012fc935 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 (_,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) @@ -364,14 +365,15 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_ = let module C = Cic in let module R = CicReduction in - let (_,metasenv,_,_) = proof 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 @@ -383,9 +385,9 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,pbo,pty, attrs = 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]) @@ -418,11 +420,20 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty = proof in + let curi,metasenv,pbo,pty, attrs = 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]) @@ -445,7 +456,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let exact_tac ~term = let exact_tac ~term (proof, goal) = (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_) = proof in + let (_,metasenv,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let module T = CicTypeChecker in let module R = CicReduction in @@ -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 @@ -463,18 +474,18 @@ 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 let module C = Cic in - let (curi,metasenv,proofbo,proofty) = proof 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 = 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 = @@ -506,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 = @@ -533,32 +547,125 @@ let elim_tac ~term = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty in + let proof' = curi,metasenv'',proofbo,proofty, attrs 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 + 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 (elim_tac ~term) + 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 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 = 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,itty,patterns = + match CicEnvironment.get_obj CicUniv.empty_ugraph uri with + C.InductiveDefinition (tys,_,paramsno,_),_ -> + let _,_,itty,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,itty, + 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 (count_prods context itty - paramsno) + in + let term_to_refine = + C.MutCase (uri,typeno,outtype,term,patterns) + in + 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, attrs 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) + 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 ()) @@ -575,15 +682,15 @@ 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 curi, metasenv, pbo, pty, attrs = 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