(* $Id$ *)
-open ProofEngineHelpers
open ProofEngineTypes
exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
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
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) ->
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)
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
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
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])
=
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 =
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])
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
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 =
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)
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
projects / helm.git / blobdiff