From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- proofs/logic.ml | 340 +++++++++++++++++++++++++------------------------------- 1 file changed, 152 insertions(+), 188 deletions(-) (limited to 'proofs/logic.ml') diff --git a/proofs/logic.ml b/proofs/logic.ml index d837dca5..a363c6bb 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* catchable_exception e + | Loc.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ + | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) | RefinerError _ | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* reduction errors *) | Tacred.ReductionTacticError _ (* unification errors *) - | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ + | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _|OccurCheck _ - |UnsolvableImplicit _)) -> true + |UnsolvableImplicit _|AbstractionOverMeta _)) -> true | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false @@ -327,53 +325,59 @@ let goal_type_of env sigma c = else Retyping.get_type_of ~refresh:true env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = - let env = evar_env goal in - let hyps = goal.evar_hyps in - let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in -(* - if not (occur_meta trm) then - let t'ty = (unsafe_machine env sigma trm).uj_type in - let _ = conv_leq_goal env sigma trm t'ty conclty in - (goalacc,t'ty) - else -*) + let env = Goal.V82.env sigma goal in + let hyps = Goal.V82.hyps sigma goal in + let mk_goal hyps concl = + Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) + in match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma conclty in if !check && occur_meta conclty then raise (RefinerError (MetaInType conclty)); - (mk_goal hyps conclty)::goalacc, conclty + let (gl,ev,sigma) = mk_goal hyps conclty in + gl::goalacc, conclty, sigma, ev - | Cast (t,_, ty) -> + | Cast (t,k, ty) -> check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; - mk_refgoals sigma goal goalacc ty t + let res = mk_refgoals sigma goal goalacc ty t in + (** we keep the casts (in particular VMcast) except + when they are annotating metas *) + if isMeta t then begin + assert (k <> VMcast); + res + end else + let (gls,cty,sigma,trm) = res in + (gls,cty,sigma,mkCast(trm,k,ty)) | App (f,l) -> - let (acc',hdty) = + let (acc',hdty,sigma,applicand) = match kind_of_term f with | Ind _ | Const _ when (isInd f or has_polymorphic_type (destConst f)) -> (* Sort-polymorphism of definition and inductive types *) goalacc, - type_of_global_reference_knowing_conclusion env sigma f conclty + type_of_global_reference_knowing_conclusion env sigma f conclty, + sigma, f | _ -> mk_hdgoals sigma goal goalacc f in - let (acc'',conclty') = + let (acc'',conclty',sigma, args) = mk_arggoals sigma goal acc' hdty (Array.to_list l) in check_conv_leq_goal env sigma trm conclty' conclty; - (acc'',conclty') + (acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args)) - | Case (_,p,c,lf) -> - let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in + | Case (ci,p,c,lf) -> + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in check_conv_leq_goal env sigma trm conclty' conclty; - let acc'' = + let (acc'',sigma, rbranches) = array_fold_left2 - (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + (fun (lacc,sigma,bacc) ty fi -> + let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) + (acc',sigma,[]) lbrty lf in - (acc'',conclty') + (acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches))) | _ -> if occur_meta trm then @@ -381,70 +385,77 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let t'ty = goal_type_of env sigma trm in check_conv_leq_goal env sigma trm t'ty conclty; - (goalacc,t'ty) + (goalacc,t'ty,sigma, trm) -(* Same as mkREFGOALS but without knowing te type of the term. Therefore, +(* Same as mkREFGOALS but without knowing the type of the term. Therefore, * Metas should be casted. *) and mk_hdgoals sigma goal goalacc trm = - let env = evar_env goal in - let hyps = goal.evar_hyps in - let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in + let env = Goal.V82.env sigma goal in + let hyps = Goal.V82.hyps sigma goal in + let mk_goal hyps concl = + Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - (mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in + gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> check_typability env sigma ty; mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty) = + let (acc',hdty,sigma,applicand) = if isInd f or isConst f & not (array_exists occur_meta l) (* we could be finer *) then - (goalacc,type_of_global_reference_knowing_parameters env sigma f l) + (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) else mk_hdgoals sigma goal goalacc f in - mk_arggoals sigma goal acc' hdty (Array.to_list l) + let (acc'',conclty',sigma, args) = + mk_arggoals sigma goal acc' hdty (Array.to_list l) in + (acc'',conclty',sigma, Term.mkApp (applicand, Array.of_list args)) - | Case (_,p,c,lf) -> - let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in - let acc'' = + | Case (ci,p,c,lf) -> + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in + let (acc'',sigma,rbranches) = array_fold_left2 - (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + (fun (lacc,sigma,bacc) ty fi -> + let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) + (acc',sigma,[]) lbrty lf in - (acc'',conclty') + (acc'',conclty',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches))) | _ -> if !check && occur_meta trm then anomaly "refine called with a dependent meta"; - goalacc, goal_type_of env sigma trm + goalacc, goal_type_of env sigma trm, sigma, trm and mk_arggoals sigma goal goalacc funty = function - | [] -> goalacc,funty + | [] -> goalacc,funty,sigma, [] | harg::tlargs as allargs -> - let t = whd_betadeltaiota (evar_env goal) sigma funty in + let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in match kind_of_term t with | Prod (_,c1,b) -> - let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in - mk_arggoals sigma goal acc' (subst1 harg b) tlargs + let (acc',hargty,sigma,arg') = mk_refgoals sigma goal goalacc c1 harg in + let (acc'',fty, sigma', args) = + mk_arggoals sigma goal acc' (subst1 harg b) tlargs in + (acc'',fty,sigma',arg'::args) | LetIn (_,c1,_,b) -> mk_arggoals sigma goal goalacc (subst1 c1 b) allargs | _ -> raise (RefinerError (CannotApply (t,harg))) and mk_casegoals sigma goal goalacc p c = - let env = evar_env goal in - let (acc',ct) = mk_hdgoals sigma goal goalacc c in - let (acc'',pt) = mk_hdgoals sigma goal acc' p in + let env = Goal.V82.env sigma goal in + let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = - try find_mrectype env sigma ct + try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec p c in - (acc'',lbrty,conclty) + (acc'',lbrty,conclty,sigma,p',c') let convert_hyp sign sigma (id,b,bt as d) = @@ -462,18 +473,6 @@ let convert_hyp sign sigma (id,b,bt as d) = d) in reorder_val_context env sign' !reorder -(* Normalizing evars in a goal. Called by tactic Local_constraints - (i.e. when the sigma of the proof tree changes). Detect if the - goal is unchanged *) -let norm_goal sigma gl = - let red_fun = Evarutil.nf_evar sigma in - let ncl = red_fun gl.evar_concl in - let ngl = - { gl with - evar_concl = ncl; - evar_hyps = map_named_val red_fun gl.evar_hyps } in - if Evd.eq_evar_info ngl gl then None else Some ngl - (************************************************************************) @@ -481,10 +480,12 @@ let norm_goal sigma gl = (* Primitive tactics are handled here *) let prim_refiner r sigma goal = - let env = evar_env goal in - let sign = goal.evar_hyps in - let cl = goal.evar_concl in - let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in + let env = Goal.V82.env sigma goal in + let sign = Goal.V82.hyps sigma goal in + let cl = Goal.V82.concl sigma goal in + let mk_goal hyps concl = + Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) + in match r with (* Logical rules *) | Intro id -> @@ -492,19 +493,23 @@ let prim_refiner r sigma goal = error ("Variable " ^ string_of_id id ^ " is already declared."); (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> - let sg = mk_goal (push_named_context_val (id,None,c1) sign) + let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in + let sigma = + Goal.V82.partial_solution sigma goal (mkNamedLambda id c1 ev) in ([sg], sigma) | LetIn (_,c1,t1,b) -> - let sg = + let (sg,ev,sigma) = mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in + let sigma = + Goal.V82.partial_solution sigma goal (mkNamedLetIn id c1 t1 ev) in ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) | Cut (b,replace,id,t) -> - let sg1 = mk_goal sign (nf_betaiota sigma t) in + let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in let sign,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in @@ -516,7 +521,10 @@ let prim_refiner r sigma goal = (if !check && mem_named_context id (named_context_of_val sign) then error ("Variable " ^ string_of_id id ^ " is already declared."); push_named_context_val (id,None,t) sign,cl,sigma) in - let sg2 = mk_goal sign cl in + let (sg2,ev2,sigma) = + Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in + let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in + let sigma = Goal.V82.partial_solution sigma goal oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | FixRule (f,n,rest,j) -> @@ -546,9 +554,24 @@ let prim_refiner r sigma goal = ("Name "^string_of_id f^" already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> - List.map (fun (_,_,c) -> mk_goal sign c) all + Goal.list_map (fun sigma (_,_,c) -> + let (gl,ev,sig')= + Goal.V82.mk_goal sigma sign c + (Goal.V82.extra sigma goal) + in ((gl,ev),sig')) + all sigma in - (mk_sign sign all, sigma) + let (gls_evs,sigma) = mk_sign sign all in + let (gls,evs) = List.split gls_evs in + let ids = List.map pi1 all in + let evs = List.map (Term.subst_vars (List.rev ids)) evs in + let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in + let funnames = Array.of_list (List.map (fun i -> Name i) ids) in + let typarray = Array.of_list (List.map pi3 all) in + let bodies = Array.of_list evs in + let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in + let sigma = Goal.V82.partial_solution sigma goal oterm in + (gls,sigma) | Cofix (f,others,j) -> let rec check_is_coind env cl = @@ -573,32 +596,56 @@ let prim_refiner r sigma goal = with | Not_found -> mk_sign (push_named_context_val (f,None,ar) sign) oth) - | [] -> List.map (fun (_,c) -> mk_goal sign c) all + | [] -> Goal.list_map (fun sigma(_,c) -> + let (gl,ev,sigma) = + Goal.V82.mk_goal sigma sign c + (Goal.V82.extra sigma goal) + in + ((gl,ev),sigma)) + all sigma in - (mk_sign sign all, sigma) + let (gls_evs,sigma) = mk_sign sign all in + let (gls,evs) = List.split gls_evs in + let (ids,types) = List.split all in + let evs = List.map (Term.subst_vars (List.rev ids)) evs in + let funnames = Array.of_list (List.map (fun i -> Name i) ids) in + let typarray = Array.of_list types in + let bodies = Array.of_list evs in + let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in + let sigma = Goal.V82.partial_solution sigma goal oterm in + (gls,sigma) | Refine c -> check_meta_variables c; - let (sgl,cl') = mk_refgoals sigma goal [] cl c in + let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in + let sigma = Goal.V82.partial_solution sigma goal oterm in (sgl, sigma) (* Conversion rules *) - | Convert_concl (cl',_) -> + | Convert_concl (cl',k) -> check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then - let sg = mk_goal sign cl' in + let (sg,ev,sigma) = mk_goal sign cl' in + let ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev in + let sigma = Goal.V82.partial_solution sigma goal ev in ([sg], sigma) else error "convert-concl rule passed non-converting term" | Convert_hyp (id,copt,ty) -> - ([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma) + let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([gl], sigma) (* And now the structural rules *) | Thin ids -> let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in - ([mk_goal hyps concl], nsigma) + let (gl,ev,sigma) = + Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal) + in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([gl], sigma) | ThinBody ids -> let clear_aux env id = @@ -607,7 +654,8 @@ let prim_refiner r sigma goal = env' in let sign' = named_context_val (List.fold_left clear_aux env ids) in - let sg = mk_goal sign' cl in + let (sg,ev,sigma) = mk_goal sign' cl in + let sigma = Goal.V82.partial_solution sigma goal ev in ([sg], sigma) | Move (withdep, hfrom, hto) -> @@ -615,11 +663,15 @@ let prim_refiner r sigma goal = split_sign hfrom hto (named_context_of_val sign) in let hyps' = move_hyp withdep toleft (left,declfrom,right) hto in - ([mk_goal hyps' cl], sigma) + let (gl,ev,sigma) = mk_goal hyps' cl in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([gl], sigma) | Order ord -> let hyps' = reorder_val_context env sign ord in - ([mk_goal hyps' cl], sigma) + let (gl,ev,sigma) = mk_goal hyps' cl in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([gl], sigma) | Rename (id1,id2) -> if !check & id1 <> id2 && @@ -627,12 +679,19 @@ let prim_refiner r sigma goal = error ((string_of_id id2)^" is already used."); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in - ([mk_goal sign' cl'], sigma) + let (gl,ev,sigma) = mk_goal sign' cl' in + let ev = Term.replace_vars [(id2,mkVar id1)] ev in + let sigma = Goal.V82.partial_solution sigma goal ev in + ([gl], sigma) | Change_evars -> - match norm_goal sigma goal with - Some ngl -> ([ngl],sigma) - | None -> ([goal], sigma) + (* spiwack: a priori [Change_evars] is now devoid of operational content. + The new proof engine keeping the evar_map up to date at all time. + As a compatibility mesure I leave the rule. + It is possible that my assumption is wrong and some uses of + [Change_evars] are not subsumed by the new engine. In which + case something has to be done here. (Feb. 2010) *) + ([goal],sigma) (************************************************************************) (************************************************************************) @@ -644,27 +703,6 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = - let rec aux p vars = - let _,subst = - List.fold_left (fun (n,l) var -> - let t = match var with - | Anonymous,_ -> l - | Name id, ProofVar -> (id,mkRel n)::l - | Name id, SectionVar id' -> (id,mkVar id')::l in - (n+1,t)) (p,[]) vars - in replace_vars (List.rev subst) - in aux 1 - -let rec rebind id1 id2 = function - | [] -> [Name id2,SectionVar id1] - | (na,k as x)::l -> - if na = Name id1 then (Name id2,k)::l else - let l' = rebind id1 id2 l in - if na = Name id2 then (Anonymous,k)::l' else x::l' - -let add_proof_var id vl = (Name id,ProofVar)::vl - let proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n @@ -672,77 +710,3 @@ let proof_variable_index x = | [] -> raise Not_found in aux 1 - -let prim_extractor subfun vl pft = - let cl = pft.goal.evar_concl in - match pft.ref with - | Some (Prim (Intro id), [spf]) -> - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,ty,_) -> - let cty = subst_proof_vars vl ty in - mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) - | LetIn (_,b,ty,_) -> - let cb = subst_proof_vars vl b in - let cty = subst_proof_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) - | _ -> error "Incomplete proof!") - - | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) -> - let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in - mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t, - subfun (add_proof_var id vl) spf2) - - | Some (Prim (FixRule (f,n,others,j)),spfl) -> - let firsts,lasts = list_chop j others in - let all = Array.of_list (firsts@(f,n,cl)::lasts) in - let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in - let names = Array.map (fun (f,_,_) -> Name f) all in - let vn = Array.map (fun (_,n,_) -> n-1) all in - let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl) - (add_proof_var f vl) others in - let lfix = Array.map (subfun newvl) (Array.of_list spfl) in - mkFix ((vn,j),(names,lcty,lfix)) - - | Some (Prim (Cofix (f,others,j)),spfl) -> - let firsts,lasts = list_chop j others in - let all = Array.of_list (firsts@(f,cl)::lasts) in - let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in - let names = Array.map (fun (f,_) -> Name f) all in - let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl) - (add_proof_var f vl) others in - let lfix = Array.map (subfun newvl) (Array.of_list spfl) in - mkCoFix (j,(names,lcty,lfix)) - - | Some (Prim (Refine c),spfl) -> - let mvl = collect_meta_variables c in - let metamap = List.combine mvl (List.map (subfun vl) spfl) in - let cc = subst_proof_vars vl c in - plain_instance metamap cc - - (* Structural and conversion rules do not produce any proof *) - | Some (Prim (Convert_concl (t,k)),[pf]) -> - if k = DEFAULTcast then subfun vl pf - else mkCast (subfun vl pf,k,subst_proof_vars vl cl) - | Some (Prim (Convert_hyp _),[pf]) -> - subfun vl pf - - | Some (Prim (Thin _),[pf]) -> - (* No need to make ids Anon in vl: subst_proof_vars take the most recent*) - subfun vl pf - - | Some (Prim (ThinBody _),[pf]) -> - subfun vl pf - - | Some (Prim (Move _|Order _),[pf]) -> - subfun vl pf - - | Some (Prim (Rename (id1,id2)),[pf]) -> - subfun (rebind id1 id2 vl) pf - - | Some (Prim Change_evars, [pf]) -> - subfun vl pf - - | Some _ -> anomaly "prim_extractor" - - | None-> error "prim_extractor handed incomplete proof" - -- cgit v1.2.3