From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/logic.ml | 515 +++++++++++++++++++++++++------------------------------- 1 file changed, 231 insertions(+), 284 deletions(-) (limited to 'proofs/logic.ml') diff --git a/proofs/logic.ml b/proofs/logic.ml index 52ca0e00..53f8093e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,37 +1,34 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* catchable_exception e - | LtacLocated(_,e) -> catchable_exception e - | Util.UserError _ | TypeError _ | PretypeError (_,_,TypingError _) +(** FIXME: this is quite brittle. Why not accept any PretypeError? *) +let is_typing_error = function +| UnexpectedType (_, _) | NotProduct _ +| VarNotFound _ | TypingError _ -> true +| _ -> false + +let is_unification_error = function +| CannotUnify _ | CannotUnifyLocal _| CannotGeneralize _ +| NoOccurrenceFound _ | CannotUnifyBindingType _ +| ActualTypeNotCoercible _ | UnifOccurCheck _ +| CannotFindWellTypedAbstraction _ | WrongAbstractionType _ +| UnsolvableImplicit _| AbstractionOverMeta _ +| UnsatisfiableConstraints _ -> true +| _ -> false + +let catchable_exception = function + | Errors.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ - | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) + | Nametab.GlobalizationError _ (* reduction errors *) - | Tacred.ReductionTacticError _ - (* unification errors *) - | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ - |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ - |CannotFindWellTypedAbstraction _|OccurCheck _ - |UnsolvableImplicit _|AbstractionOverMeta _)) -> true - | Typeclasses_errors.TypeClassError - (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true + | Tacred.ReductionTacticError _ -> true + (* unification and typing errors *) + | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = - error ("No such hypothesis: " ^ string_of_id id ^ ".") +let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -75,13 +80,13 @@ let with_check = Flags.with_option check let apply_to_hyp sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error "No such assumption." + if !check then error_no_such_hypothesis id 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 -> - if !check then error "No such assumption." + if !check then error_no_such_hypothesis id else sign let check_typability env sigma c = @@ -96,41 +101,17 @@ let check_typability env sigma c = (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) -let clear_hyps sigma ids sign cl = +let clear_hyps env 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, !evdref) + let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in + (hyps, cl, !evdref) -(* The ClearBody tactic *) +let clear_hyps2 env sigma ids sign t cl = + let evdref = ref (Evd.create_goal_evar_defs sigma) in + let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in + (hyps, t, cl, !evdref) -let recheck_typability (what,id) env sigma t = - try check_typability env sigma t - with e when Errors.noncritical e -> - let s = match what with - | None -> "the conclusion" - | 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 - (fun (_,c,t) _ -> - match c with - | None -> error ((string_of_id id)^" is not a local definition.") - | Some c ->(id,None,t)) - (fun (id',c,t as d) sign -> - (if !check then - begin - let env = reset_with_named_context sign env in - match c with - | None -> recheck_typability (Some id',id) env sigma t - | Some b -> - let b' = mkCast (b,DEFAULTcast, t) in - recheck_typability (Some id',id) env sigma b' - end;d)) - in - reset_with_named_context sign env +(* The ClearBody tactic *) (* Reordering of the context *) @@ -139,36 +120,36 @@ let remove_hyp_body env sigma id = (* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *) (* reculees par rapport aux autres (faire le contraire!) *) -let mt_q = (Idmap.empty,[]) +let mt_q = (Id.Map.empty,[]) let push_val y = function (_,[] as q) -> q - | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q) + | (m, (x,l)::q) -> (m, (x,Id.Set.add y l)::q) let push_item x v (m,l) = - (Idmap.add x v m, (x,Idset.empty)::l) -let mem_q x (m,_) = Idmap.mem x m -let rec find_q x (m,q) = - let v = Idmap.find x m in - let m' = Idmap.remove x m in + (Id.Map.add x v m, (x,Id.Set.empty)::l) +let mem_q x (m,_) = Id.Map.mem x m +let find_q x (m,q) = + let v = Id.Map.find x m in + let m' = Id.Map.remove x m in let rec find accs acc = function [] -> raise Not_found | [(x',l)] -> - if x=x' then ((v,Idset.union accs l),(m',List.rev acc)) + if Id.equal x x' then ((v,Id.Set.union accs l),(m',List.rev acc)) else raise Not_found | (x',l as i)::((x'',l'')::q as itl) -> - if x=x' then - ((v,Idset.union accs l), - (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q)) - else find (Idset.union l accs) (i::acc) itl in - find Idset.empty [] q + if Id.equal x x' then + ((v,Id.Set.union accs l), + (m',List.rev acc@(x'',Id.Set.add x (Id.Set.union l l''))::q)) + else find (Id.Set.union l accs) (i::acc) itl in + find Id.Set.empty [] q let occur_vars_in_decl env hyps d = - if Idset.is_empty hyps then false else + if Id.Set.is_empty hyps then false else let ohyps = global_vars_set_of_decl env d in - Idset.exists (fun h -> Idset.mem h ohyps) hyps + Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps let reorder_context env sign ord = - let ords = List.fold_right Idset.add ord Idset.empty in - if List.length ord <> Idset.cardinal ords then + let ords = List.fold_right Id.Set.add ord Id.Set.empty in + if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then error "Order list has duplicates"; let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with @@ -179,16 +160,16 @@ let reorder_context env sign ord = errorlabstrm "reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ - prlist_with_sep pr_spc pr_id - (Idset.elements (Idset.inter h + pr_sequence pr_id + (Id.Set.elements (Id.Set.inter h (global_vars_set_of_decl env d)))); step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with | [] -> error_no_such_hypothesis (List.hd ord) | (x,_,_ as d) :: ctxt -> - if Idset.mem x expected then - step ord (Idset.remove x expected) + if Id.Set.mem x expected then + step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail else step ord expected @@ -204,8 +185,8 @@ let reorder_val_context env sign ord = let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in - if List.mem x deps then - error ("Cannot create self-referring hypothesis "^string_of_id x); + if Id.List.mem x deps then + error ("Cannot create self-referring hypothesis "^Id.to_string x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -216,11 +197,18 @@ let check_decl_position env sign (x,_,_ as d) = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +let move_location_eq m1 m2 = match m1, m2 with +| MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 +| MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 +| MoveLast, MoveLast -> true +| MoveFirst, MoveFirst -> true +| _ -> false + let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | (hyp,_,_) :: right -> - if hyp = h then - match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false + if Id.equal hyp h then + match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst else get_hyp_after h right @@ -228,11 +216,14 @@ 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 - (left,right,d, toleft or hto = MoveToEnd true) + if Id.equal hyp hfrom then + (left,right,d, toleft || move_location_eq hto MoveLast) else - splitrec (d::left) - (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) + let is_toleft = match hto with + | MoveAfter h' | MoveBefore h' -> Id.equal hyp h' + | _ -> false + in + splitrec (d::left) (toleft || is_toleft) right in splitrec [] false l @@ -242,7 +233,7 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = +let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = let env = Global.env() in let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = if toleft @@ -251,25 +242,25 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = in let rec moverec first middle = function | [] -> - if match hto with MoveToEnd _ -> false | _ -> true then + if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | (hyp,_,_) :: _ as right when hto = MoveBefore hyp -> + | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) -> 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 not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ - pr_move_location pr_id hto ++ + Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") else (d::first, middle) in - if hto = MoveAfter hyp then + if move_location_eq hto (MoveAfter hyp) then List.rev first' @ List.rev middle' @ right else moverec first' middle' right @@ -291,6 +282,9 @@ let rename_hyp id1 id2 sign = (fun (_,b,t) _ -> (id2,b,t)) (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) +(**********************************************************************) + + (************************************************************************) (************************************************************************) (* Implementation of the logical rules *) @@ -308,21 +302,34 @@ let collect_meta_variables c = | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c | (App _| Case _) -> fold_constr (collrec deep) acc c + | Proj (_, c) -> collrec deep acc c | _ -> fold_constr (collrec true) acc c in List.rev (collrec false [] c) let check_meta_variables c = - if not (list_distinct (collect_meta_variables c)) then + if not (List.distinct_f Int.compare (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 - raise (RefinerError (BadType (arg,ty,conclty))) + if !check then + let evm, b = Reductionops.infer_conv env sigma ty conclty in + if b then evm + else raise (RefinerError (BadType (arg,ty,conclty))) + else sigma + +exception Stop of constr list +let meta_free_prefix a = + try + let _ = Array.fold_left (fun acc a -> + if occur_meta a then raise (Stop acc) + else a :: acc) [] a + in a + with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = if !check then type_of env sigma c - else Retyping.get_type_of ~refresh:true env sigma c + else Retyping.get_type_of env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -330,62 +337,77 @@ let rec mk_refgoals sigma goal goalacc conclty trm = 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 _ -> + if (not !check) && not (occur_meta trm) then + let t'ty = Retyping.get_type_of env sigma trm in + let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + (goalacc,t'ty,sigma,trm) + else + match kind_of_term trm with + | Meta _ -> let conclty = nf_betaiota sigma conclty in if !check && occur_meta conclty then raise (RefinerError (MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in gl::goalacc, conclty, sigma, ev - | Cast (t,k, ty) -> + | Cast (t,k, ty) -> check_typability env sigma ty; - check_conv_leq_goal env sigma trm ty conclty; + let sigma = check_conv_leq_goal env sigma trm ty conclty in let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast) except + (** we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin - assert (k <> VMcast); + assert (k != VMcast && k != NATIVEcast); res end else - let (gls,cty,sigma,trm) = res in - (gls,cty,sigma,mkCast(trm,k,ty)) + let (gls,cty,sigma,ans) = res in + let ans = if ans == t then trm else mkCast(ans,k,ty) in + (gls,cty,sigma,ans) - | App (f,l) -> + | App (f,l) -> 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, - sigma, f - | _ -> - mk_hdgoals sigma goal goalacc f + if is_template_polymorphic env f then + let sigma, ty = + (* Template sort-polymorphism of definition and inductive types *) + type_of_global_reference_knowing_conclusion env sigma f conclty + in + goalacc, ty, sigma, f + else + mk_hdgoals sigma goal goalacc f in - 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',sigma, Term.mkApp (applicand, Array.of_list args)) - - | Case (ci,p,c,lf) -> + let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let sigma = check_conv_leq_goal env sigma trm conclty' conclty in + let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in + (acc'',conclty',sigma, ans) + + | Proj (p,c) -> + let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let c = mkProj (p, c') in + let ty = get_type_of env sigma c in + (acc',ty,sigma,c) + + | 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 sigma = check_conv_leq_goal env sigma trm conclty' conclty in let (acc'',sigma, rbranches) = - array_fold_left2 + Array.fold_left2 (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',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches))) + let lf' = Array.rev_of_list rbranches in + let ans = + if p' == p && c' == c && Array.equal (==) lf' lf then trm + else Term.mkCase (ci,p',c',lf') + in + (acc'',conclty',sigma, ans) - | _ -> + | _ -> if occur_meta trm then - anomaly "refiner called with a meta in non app/case subterm"; - - let t'ty = goal_type_of env sigma trm in - check_conv_leq_goal env sigma trm t'ty conclty; - (goalacc,t'ty,sigma, trm) + anomaly (Pp.str "refiner called with a meta in non app/case subterm"); + let t'ty = goal_type_of env sigma trm in + let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + (goalacc,t'ty,sigma, trm) (* Same as mkREFGOALS but without knowing the type of the term. Therefore, * Metas should be casted. *) @@ -407,44 +429,57 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if isInd f or isConst f - & not (array_exists occur_meta l) (* we could be finer *) + if is_template_polymorphic env f then - (goalacc,type_of_global_reference_knowing_parameters env sigma f l,sigma,f) + let l' = meta_free_prefix l in + (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in - 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)) + let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let ans = if applicand == f && args == l then trm else Term.mkApp (applicand, args) in + (acc'',conclty',sigma, ans) | 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 + Array.fold_left2 (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',sigma, Term.mkCase (ci,p',c',Array.of_list (List.rev rbranches))) + let lf' = Array.rev_of_list rbranches in + let ans = + if p' == p && c' == c && Array.equal (==) lf' lf then trm + else Term.mkCase (ci,p',c',lf') + in + (acc'',conclty',sigma, ans) + + | Proj (p,c) -> + let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let c = mkProj (p, c') in + let ty = get_type_of env sigma c in + (acc',ty,sigma,c) | _ -> if !check && occur_meta trm then - anomaly "refine called with a dependent meta"; + anomaly (Pp.str "refine called with a dependent meta"); goalacc, goal_type_of env sigma trm, sigma, trm -and mk_arggoals sigma goal goalacc funty = function - | [] -> goalacc,funty,sigma, [] - | harg::tlargs as allargs -> - let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in - match kind_of_term t with - | Prod (_,c1,b) -> - 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_arggoals sigma goal goalacc funty allargs = + let foldmap (goalacc, funty, sigma) harg = + let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in + let rec collapse t = match kind_of_term t with + | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) + | _ -> t + in + let t = collapse t in + match kind_of_term t with + | Prod (_, c1, b) -> + let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in + (acc, subst1 harg b, sigma), arg + | _ -> raise (RefinerError (CannotApply (t, harg))) + in + Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in @@ -452,24 +487,23 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = 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 + with Not_found -> anomaly (Pp.str "mk_casegoals") in + let (lbrty,conclty) = type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty,sigma,p',c') -let convert_hyp sign sigma (id,b,bt as d) = +let convert_hyp check sign sigma (id,b,bt as d) = let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp sign id (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(string_of_id id)^"."); - if !check && not (Option.Misc.compare (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(string_of_id id)^"."); - if !check then reorder := check_decl_position env sign d; + if check && not (is_conv env sigma bt ct) then + error ("Incorrect change of the type of "^(Id.to_string id)^"."); + if check && not (Option.equal (is_conv env sigma) b c) then + error ("Incorrect change of the body of "^(Id.to_string id)^"."); + if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -488,50 +522,31 @@ let prim_refiner r sigma goal = in match r with (* Logical rules *) - | Intro id -> - if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ string_of_id id ^ " is already declared."); - (match kind_of_term (strip_outer_cast cl) with - | Prod (_,c1,b) -> - 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,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) -> +(* if !check && not (Retyping.get_sort_of env sigma t) then*) let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in - let sign,cl,sigma = + let sign,t,cl,sigma = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in - let sign,cl,sigma = clear_hyps sigma [id] sign cl in - move_hyp true false ([],(id,None,t),named_context_of_val sign) + let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in + move_hyp false ([],(id,None,t),named_context_of_val sign) nexthyp, - cl,sigma + t,cl,sigma else (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 + error ("Variable " ^ Id.to_string id ^ " is already declared."); + push_named_context_val (id,None,t) sign,t,cl,sigma) 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 + let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in + let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm 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 + if Int.equal k 1 then try fst (find_inductive env sigma c1) with Not_found -> @@ -540,31 +555,30 @@ let prim_refiner r sigma goal = 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 ((sp,_),u) = 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 | (f,n,ar)::oth -> - let (sp',_) = check_ind env n ar in - if not (sp=sp') then + let ((sp',_),u') = check_ind env n ar in + if not (eq_mind 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"); + ("Name "^Id.to_string f^" already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> - 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 + Evd.Monad.List.map (fun (_,_,c) sigma -> + let gl,ev,sig' = + Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in + (gl,ev),sig') + all sigma in 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 evs = List.map (Vars.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 @@ -585,7 +599,7 @@ let prim_refiner r sigma goal = error ("All methods must construct elements " ^ "in coinductive types.") in - let firsts,lasts = list_chop j others 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 @@ -596,18 +610,17 @@ let prim_refiner r sigma goal = with | Not_found -> mk_sign (push_named_context_val (f,None,ar) sign) oth) - | [] -> 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 + | [] -> + Evd.Monad.List.map (fun (_,c) sigma -> + let gl,ev,sigma = + Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in + (gl,ev),sigma) + all sigma in 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 evs = List.map (Vars.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 @@ -622,87 +635,21 @@ let prim_refiner r sigma goal = let sigma = Goal.V82.partial_solution sigma goal oterm in (sgl, sigma) - (* Conversion rules *) - | Convert_concl (cl',k) -> - check_typability env sigma cl'; - if (not !check) || is_conv_leq env sigma cl' cl then - 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) -> - 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 + let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in + let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in 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 + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) - | ThinBody ids -> - let clear_aux env id = - let env' = remove_hyp_body env sigma id in - if !check then recheck_typability (None,id) env' sigma cl; - env' - in - let sign' = named_context_val (List.fold_left clear_aux env ids) 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) -> + | Move (hfrom, hto) -> let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in let hyps' = - move_hyp withdep toleft (left,declfrom,right) hto in + move_hyp toleft (left,declfrom,right) hto in let (gl,ev,sigma) = mk_goal hyps' cl in - let sigma = Goal.V82.partial_solution sigma goal ev in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) - - | Order ord -> - let hyps' = reorder_val_context env sign ord in - 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 && - List.mem id2 (ids_of_named_context (named_context_of_val sign)) then - 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 - 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 -> - (* Normalises evars in goals. Used by instantiate. *) - let (goal,sigma) = Goal.V82.nf_evar sigma goal in - ([goal],sigma) - -(************************************************************************) -(************************************************************************) -(* Extracting a proof term from the proof tree *) - -(* Util *) - -type variable_proof_status = ProofVar | SectionVar of identifier - -type proof_variable = name * variable_proof_status - -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 - aux 1 -- cgit v1.2.3