From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- proofs/logic.ml | 187 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 94 insertions(+), 93 deletions(-) (limited to 'proofs/logic.ml') diff --git a/proofs/logic.ml b/proofs/logic.ml index c019d45f..9cab6a05 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -28,7 +28,7 @@ open Type_errors open Retyping open Evarutil open Tacexpr - + type refiner_error = (* Errors raised by the refiner *) @@ -50,15 +50,17 @@ open Pretype_errors let rec catchable_exception = function | Stdpp.Exc_located(_,e) -> catchable_exception e | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ + | Util.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + (* reduction errors *) + | Tacred.ReductionTacticError _ (* unification errors *) | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true - | Typeclasses_errors.TypeClassError + | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false @@ -73,19 +75,19 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = - try apply_to_hyp sign id f - with Hyp_not_found -> + try apply_to_hyp sign id f + with Hyp_not_found -> if !check then error "No such assumption." else sign let apply_to_hyp_and_dependent_on sign id f g = - try apply_to_hyp_and_dependent_on sign id f g - with Hyp_not_found -> + try apply_to_hyp_and_dependent_on sign id f g + with Hyp_not_found -> if !check then error "No such assumption." else sign let check_typability env sigma c = - if !check then let _ = type_of env sigma c in () + if !check then let _ = type_of env sigma c in () (************************************************************************) (************************************************************************) @@ -99,7 +101,7 @@ let check_typability env sigma c = let clear_hyps sigma ids sign cl = let evdref = ref (Evd.create_goal_evar_defs sigma) in let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in - (hyps,concl,evars_of !evdref) + (hyps,concl, !evdref) (* The ClearBody tactic *) @@ -111,7 +113,7 @@ let recheck_typability (what,id) env sigma t = | Some id -> "hypothesis "^(string_of_id id) in error ("The correctness of "^s^" relies on the body of "^(string_of_id id)) - + let remove_hyp_body env sigma id = let sign = apply_to_hyp_and_dependent_on (named_context_val env) id @@ -121,7 +123,7 @@ let remove_hyp_body env sigma id = | Some c ->(id,None,t)) (fun (id',c,t as d) sign -> (if !check then - begin + begin let env = reset_with_named_context sign env in match c with | None -> recheck_typability (Some id',id) env sigma t @@ -130,7 +132,7 @@ let remove_hyp_body env sigma id = recheck_typability (Some id',id) env sigma b' end;d)) in - reset_with_named_context sign env + reset_with_named_context sign env (* Reordering of the context *) @@ -138,7 +140,7 @@ let remove_hyp_body env sigma id = (* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *) (* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *) (* reculees par rapport aux autres (faire le contraire!) *) - + let mt_q = (Idmap.empty,[]) let push_val y = function (_,[] as q) -> q @@ -211,8 +213,8 @@ let check_decl_position env sign (x,_,_ as d) = (* Auxiliary functions for primitive MOVE tactic * * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves - * hyp [hfrom] at location [hto] which belongs to the hyps on the - * left side [left] of the full signature if [toleft=true] or to the hyps + * hyp [hfrom] at location [hto] which belongs to the hyps on the + * left side [left] of the full signature if [toleft=true] or to the hyps * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) @@ -228,17 +230,17 @@ let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom | (hyp,c,typ) as d :: right -> - if hyp = hfrom then + if hyp = hfrom then (left,right,d, toleft or hto = MoveToEnd true) else - splitrec (d::left) + splitrec (d::left) (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) right - in + in splitrec [] false l let hyp_of_move_location = function - | MoveAfter id -> id + | MoveAfter id -> id | MoveBefore id -> id | _ -> assert false @@ -258,12 +260,12 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = List.rev first @ List.rev middle @ right | (hyp,_,_) as d :: right -> let (first',middle') = - if List.exists (test_dep d) middle then - if with_dep & hto <> MoveAfter hyp then + if List.exists (test_dep d) middle then + if with_dep & hto <> MoveAfter hyp then (first, d::middle) - else - errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++ - pr_move_location pr_id hto ++ + else + errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ + pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") else @@ -271,16 +273,16 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = in if hto = MoveAfter hyp then List.rev first' @ List.rev middle' @ right - else + else moverec first' middle' right in - if toleft then - let right = + if toleft then + let right = List.fold_right push_named_context_val right empty_named_context_val in List.fold_left (fun sign d -> push_named_context_val d sign) - right (moverec [] [declfrom] left) - else - let right = + right (moverec [] [declfrom] left) + else + let right = List.fold_right push_named_context_val (moverec [] [declfrom] right) empty_named_context_val in List.fold_left (fun sign d -> push_named_context_val d sign) @@ -295,7 +297,7 @@ let rename_hyp id1 id2 sign = (************************************************************************) (* Implementation of the logical rules *) -(* Will only be used on terms given to the Refine rule which have meta +(* Will only be used on terms given to the Refine rule which have meta variables only in Application and Case *) let error_unsupported_deep_meta c = @@ -303,7 +305,7 @@ let error_unsupported_deep_meta c = strbrk "form contains metavariables deep inside the term is not " ++ strbrk "supported; try \"refine\" instead.") -let collect_meta_variables c = +let collect_meta_variables c = let rec collrec deep acc c = match kind_of_term c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c @@ -312,16 +314,16 @@ let collect_meta_variables c = in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables c = if not (list_distinct (collect_meta_variables c)) then raise (RefinerError (NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = - if !check & not (is_conv_leq env sigma ty conclty) then + if !check & not (is_conv_leq env sigma ty conclty) then raise (RefinerError (BadType (arg,ty,conclty))) let goal_type_of env sigma c = - (if !check then type_of else Retyping.get_type_of) env sigma c + (if !check then type_of 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 @@ -329,7 +331,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = 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 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 @@ -352,9 +354,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Ind _ | Const _ when (isInd f or has_polymorphic_type (destConst f)) -> (* Sort-polymorphism of definition and inductive types *) - goalacc, + goalacc, type_of_global_reference_knowing_conclusion env sigma f conclty - | _ -> + | _ -> mk_hdgoals sigma goal goalacc f in let (acc'',conclty') = @@ -365,14 +367,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (_,p,c,lf) -> let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in check_conv_leq_goal env sigma trm conclty' conclty; - let acc'' = + let acc'' = array_fold_left2 (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + acc' lbrty lf in (acc'',conclty') - | _ -> + | _ -> if occur_meta trm then anomaly "refiner called with a meta in non app/case subterm"; @@ -397,8 +399,8 @@ and mk_hdgoals sigma goal goalacc trm = mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty) = - if isInd f or isConst f + let (acc',hdty) = + 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) @@ -408,16 +410,16 @@ and mk_hdgoals sigma goal goalacc trm = | Case (_,p,c,lf) -> let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in - let acc'' = + let acc'' = array_fold_left2 (fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi)) - acc' lbrty lf + acc' lbrty lf in (acc'',conclty') | _ -> if !check && occur_meta trm then - anomaly "refined called with a dependent meta"; + anomaly "refine called with a dependent meta"; goalacc, goal_type_of env sigma trm and mk_arggoals sigma goal goalacc funty = function @@ -434,14 +436,13 @@ and mk_arggoals sigma goal goalacc funty = function 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',ct) = mk_hdgoals sigma goal goalacc c in let (acc'',pt) = mk_hdgoals sigma goal acc' p in - let pj = {uj_val=p; uj_type=pt} in let indspec = - try find_mrectype env sigma (nf_evar sigma ct) + try find_mrectype env sigma ct with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = - type_case_branches_with_names env indspec pj c in + type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty) @@ -467,7 +468,7 @@ 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 + { 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 @@ -487,7 +488,7 @@ let prim_refiner r sigma goal = (* Logical rules *) | Intro id -> if !check && mem_named_context id (named_context_of_val sign) then - error "New variable is already declared"; + 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) @@ -500,7 +501,7 @@ let prim_refiner r sigma goal = ([sg], sigma) | _ -> raise (RefinerError IntroNeedsProduct)) - + | Cut (b,replace,id,t) -> let sg1 = mk_goal sign (nf_betaiota sigma t) in let sign,cl,sigma = @@ -512,58 +513,58 @@ let prim_refiner r sigma goal = cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - error "New variable is already declared"; + 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 if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) | FixRule (f,n,rest,j) -> - let rec check_ind env k cl = - match kind_of_term (strip_outer_cast cl) with - | Prod (na,c1,b) -> - if k = 1 then - try + let rec check_ind env k cl = + match kind_of_term (strip_outer_cast cl) with + | Prod (na,c1,b) -> + if k = 1 then + try fst (find_inductive env sigma c1) - with Not_found -> + with Not_found -> error "Cannot do a fixpoint on a non inductive type." - else + else check_ind (push_rel (na,None,c1) env) (k-1) b | _ -> error "Not enough products." in let (sp,_) = check_ind env n cl in let firsts,lasts = list_chop j rest in let all = firsts@(f,n,cl)::lasts in - let rec mk_sign sign = function + let rec mk_sign sign = function | (f,n,ar)::oth -> - let (sp',_) = check_ind env n ar in - if not (sp=sp') then - error ("Fixpoints should be on the same " ^ + let (sp',_) = check_ind env n ar in + if not (sp=sp') then + error ("Fixpoints should be on the same " ^ "mutual inductive declaration."); if !check && mem_named_context f (named_context_of_val sign) then error ("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 - in + in (mk_sign sign all, sigma) - + | Cofix (f,others,j) -> - let rec check_is_coind env cl = + let rec check_is_coind env cl = let b = whd_betadeltaiota env sigma cl in match kind_of_term b with | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b - | _ -> - try + | _ -> + try let _ = find_coinductive env sigma b in () - with Not_found -> + with Not_found -> error ("All methods must construct elements " ^ "in coinductive types.") in let firsts,lasts = list_chop j others in let all = firsts@(f,cl)::lasts in List.iter (fun (_,c) -> check_is_coind env c) all; - let rec mk_sign sign = function + let rec mk_sign sign = function | (f,ar)::oth -> (try (let _ = lookup_named_val f sign in @@ -572,7 +573,7 @@ let prim_refiner r sigma goal = | Not_found -> mk_sign (push_named_context_val (f,None,ar) sign) oth) | [] -> List.map (fun (_,c) -> mk_goal sign c) all - in + in (mk_sign sign all, sigma) | Refine c -> @@ -587,17 +588,17 @@ let prim_refiner r sigma goal = if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in ([sg], sigma) - else + 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) (* And now the structural rules *) - | Thin ids -> + | Thin ids -> let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in ([mk_goal hyps concl], nsigma) - + | ThinBody ids -> let clear_aux env id = let env' = remove_hyp_body env sigma id in @@ -609,9 +610,9 @@ let prim_refiner r sigma goal = ([sg], sigma) | Move (withdep, hfrom, hto) -> - let (left,right,declfrom,toleft) = + let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in - let hyps' = + let hyps' = move_hyp withdep toleft (left,declfrom,right) hto in ([mk_goal hyps' cl], sigma) @@ -642,7 +643,7 @@ type variable_proof_status = ProofVar | SectionVar of identifier type proof_variable = name * variable_proof_status -let subst_proof_vars = +let subst_proof_vars = let rec aux p vars = let _,subst = List.fold_left (fun (n,l) var -> @@ -653,22 +654,22 @@ let subst_proof_vars = (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 -> + | (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 proof_variable_index x = let rec aux n = function | (Name id,ProofVar)::l when x = id -> n | _::l -> aux (n+1) l | [] -> raise Not_found - in + in aux 1 let prim_extractor subfun vl pft = @@ -684,7 +685,7 @@ let prim_extractor subfun vl pft = 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, @@ -699,7 +700,7 @@ let prim_extractor subfun vl pft = 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)) + mkFix ((vn,j),(names,lcty,lfix)) | Some (Prim (Cofix (f,others,j)),spfl) -> let firsts,lasts = list_chop j others in @@ -707,14 +708,14 @@ let prim_extractor subfun vl pft = 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 + (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 + let cc = subst_proof_vars vl c in plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) @@ -727,10 +728,10 @@ let prim_extractor subfun vl pft = | 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 @@ -743,4 +744,4 @@ let prim_extractor subfun vl pft = | Some _ -> anomaly "prim_extractor" | None-> error "prim_extractor handed incomplete proof" - + -- cgit v1.2.3