diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 294 |
1 files changed, 137 insertions, 157 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 65497c80..e5294715 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -11,7 +13,7 @@ open CErrors open Util open Names open Nameops -open Term +open Constr open Vars open Termops open Environ @@ -22,7 +24,8 @@ open Proof_type open Type_errors open Retyping open Misctypes -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration type refiner_error = @@ -32,14 +35,14 @@ type refiner_error = | CannotApply of constr * constr | NotWellTyped of constr | NonLinearProof of constr - | MetaInType of constr + | MetaInType of EConstr.constr (* Errors raised by the tactics *) | IntroNeedsProduct | DoesNotOccurIn of constr * Id.t | NoSuchHyp of Id.t -exception RefinerError of refiner_error +exception RefinerError of Environ.env * Evd.evar_map * refiner_error open Pretype_errors @@ -68,7 +71,7 @@ let catchable_exception = function | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false -let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) +let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -77,34 +80,20 @@ 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 check sign id f = +let apply_to_hyp env sigma check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if check then error_no_such_hypothesis id + if check then error_no_such_hypothesis env sigma id else sign let check_typability env sigma c = - if !check then let _ = unsafe_type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () (************************************************************************) (************************************************************************) (* Implementation of the structural rules (moving and deleting hypotheses around) *) -(* The Clear tactic: it scans the context for hypotheses to be removed - (instead of iterating on the list of identifier to be removed, which - forces the user to give them in order). *) - -let clear_hyps env sigma ids sign cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in - (hyps, cl, !evdref) - -let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - (* The ClearBody tactic *) (* Reordering of the context *) @@ -136,33 +125,33 @@ let find_q x (m,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 = +let occur_vars_in_decl env sigma hyps d = if Id.Set.is_empty hyps then false else - let ohyps = global_vars_set_of_decl env d in + let ohyps = global_vars_set_of_decl env sigma d in Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps -let reorder_context env sign ord = +let reorder_context env sigma sign ord = 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"; + user_err Pp.(str "Order list has duplicates"); let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with | [] -> List.rev ctxt_tail @ ctxt_head | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in - if occur_vars_in_decl env h d then - errorlabstrm "reorder_context" - (str "Cannot move declaration " ++ pr_id top ++ spc() ++ + if occur_vars_in_decl env sigma h d then + user_err ~hdr:"reorder_context" + (str "Cannot move declaration " ++ Id.print top ++ spc() ++ str "before " ++ - pr_sequence pr_id + pr_sequence Id.print (Id.Set.elements (Id.Set.inter h - (global_vars_set_of_decl env d)))); + (global_vars_set_of_decl env sigma d)))); step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with - | [] -> error_no_such_hypothesis (List.hd ord) + | [] -> error_no_such_hypothesis env sigma (List.hd ord) | d :: ctxt -> - let x = get_id d in + let x = NamedDecl.get_id d in if Id.Set.mem x expected then step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail @@ -171,19 +160,21 @@ let reorder_context env sign ord = ctxt (push_val x moved_hyps) (d::ctxt_tail)) in step ord ords sign mt_q [] -let reorder_val_context env sign ord = - val_of_named_context (reorder_context env (named_context_of_val sign) ord) +let reorder_val_context env sigma sign ord = + let open EConstr in + val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) -let check_decl_position env sign d = - let x = get_id d in - let needed = global_vars_set_of_decl env d in - let deps = dependency_closure env (named_context_of_val sign) needed in +let check_decl_position env sigma sign d = + let open EConstr in + let x = NamedDecl.get_id d in + let needed = global_vars_set_of_decl env sigma d in + let deps = dependency_closure env sigma (named_context_of_val sign) needed in if Id.List.mem x deps then - errorlabstrm "Logic.check_decl_position" - (str "Cannot create self-referring hypothesis " ++ pr_id x); + user_err ~hdr:"Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ Id.print x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -201,19 +192,11 @@ let move_location_eq m1 m2 = match m1, m2 with | MoveFirst, MoveFirst -> true | _ -> false -let rec get_hyp_after h = function - | [] -> error_no_such_hypothesis h - | d :: right -> - if Id.equal (get_id d) h then - match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst - else - get_hyp_after h right - -let split_sign hfrom hto l = +let split_sign env sigma hfrom hto l = let rec splitrec left toleft = function - | [] -> error_no_such_hypothesis hfrom + | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> - let hyp,_,typ = to_tuple d in + let hyp = NamedDecl.get_id d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -231,31 +214,31 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,declfrom,right) hto = +let move_hyp sigma toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (get_id d2) d - else occur_var_in_decl env (get_id d) d2 + then occur_var_in_decl env sigma (NamedDecl.get_id d2) d + else occur_var_in_decl env sigma (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then - error_no_such_hypothesis (hyp_of_move_location hto); + error_no_such_hypothesis env sigma (hyp_of_move_location hto); List.rev first @ List.rev middle - | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) -> + | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> List.rev first @ List.rev middle @ right | d :: right -> - let hyp = get_id d in + let hyp = NamedDecl.get_id d in let (first',middle') = if List.exists (test_dep d) middle then if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ - Miscprint.pr_move_location pr_id hto ++ - str (if toleft then ": it occurs in " else ": it depends on ") - ++ pr_id hyp ++ str ".") + user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ + Miscprint.pr_move_location Id.print hto ++ + str (if toleft then ": it occurs in the type of " else ": it depends on ") + ++ Id.print hyp ++ str ".") else (d::first, middle) in @@ -264,6 +247,7 @@ let move_hyp toleft (left,declfrom,right) hto = else moverec first' middle' right in + let open EConstr in if toleft then let right = List.fold_right push_named_context_val right empty_named_context_val in @@ -276,10 +260,15 @@ let move_hyp toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context hfrom hto sign = +let move_hyp_in_named_context env sigma hfrom hto sign = + let open EConstr in let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in - move_hyp toleft (left,declfrom,right) hto + split_sign env sigma hfrom hto (named_context_of_val sign) in + move_hyp sigma toleft (left,declfrom,right) hto + +let insert_decl_in_named_context sigma decl hto sign = + let open EConstr in + move_hyp sigma false ([],decl,named_context_of_val sign) hto (**********************************************************************) @@ -292,43 +281,46 @@ let move_hyp_in_named_context hfrom hto sign = variables only in Application and Case *) let error_unsupported_deep_meta c = - errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++ + user_err (strbrk "Application of lemmas whose beta-iota normal " ++ strbrk "form contains metavariables deep inside the term is not " ++ strbrk "supported; try \"refine\" instead.") let collect_meta_variables c = - let rec collrec deep acc c = match kind_of_term c with + let rec collrec deep acc c = match kind c with | 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 + | (App _| Case _) -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c - | _ -> fold_constr (collrec true) acc c + | _ -> Constr.fold (collrec true) acc c in List.rev (collrec false [] c) -let check_meta_variables c = +let check_meta_variables env sigma c = if not (List.distinct_f Int.compare (collect_meta_variables c)) then - raise (RefinerError (NonLinearProof c)) + raise (RefinerError (env, sigma, NonLinearProof c)) let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma ty conclty in + let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in if b then evm - else raise (RefinerError (BadType (arg,ty,conclty))) + else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma -exception Stop of constr list -let meta_free_prefix a = +exception Stop of EConstr.t list +let meta_free_prefix sigma a = try + let a = Array.map EConstr.of_constr a in let _ = Array.fold_left (fun acc a -> - if occur_meta a then raise (Stop acc) + if occur_meta sigma 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 unsafe_type_of env sigma c - else Retyping.get_type_of env sigma c + if !check then + let (sigma,t) = type_of env sigma (EConstr.of_constr c) in + (sigma, EConstr.Unsafe.to_constr t) + else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -336,17 +328,20 @@ 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 - if (not !check) && not (occur_meta trm) then - let t'ty = Retyping.get_type_of env sigma trm in + if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then + let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in + let t'ty = EConstr.Unsafe.to_constr t'ty 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 + match kind trm with | Meta _ -> - let conclty = nf_betaiota sigma conclty in - if !check && occur_meta conclty then - raise (RefinerError (MetaInType conclty)); + let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in + if !check && occur_meta sigma conclty then + raise (RefinerError (env, sigma, MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in + let ev = EConstr.Unsafe.to_constr ev in + let conclty = EConstr.Unsafe.to_constr conclty in gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> @@ -365,26 +360,28 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f then + if is_template_polymorphic env sigma (EConstr.of_constr f) then let ty = - (* Template sort-polymorphism of definition and inductive types *) - let firstmeta = Array.findi (fun i x -> occur_meta x) l in + (* Template polymorphism of definitions and inductive types *) + let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in - type_of_global_reference_knowing_parameters env sigma f args + type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in + let ty = EConstr.Unsafe.to_constr ty in goalacc, ty, sigma, f else mk_hdgoals sigma goal goalacc f in 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 + let ans = if applicand == f && args == l then trm else 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 + let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -399,14 +396,14 @@ let rec mk_refgoals sigma goal goalacc conclty trm = 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') + else mkCase (ci,p',c',lf') in (acc'',conclty',sigma, ans) | _ -> - if occur_meta trm then - anomaly (Pp.str "refiner called with a meta in non app/case subterm"); - let t'ty = goal_type_of env sigma trm in + if occur_meta sigma (EConstr.of_constr trm) then + anomaly (Pp.str "refiner called with a meta in non app/case subterm."); + let (sigma, 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) @@ -418,10 +415,11 @@ and mk_hdgoals sigma goal goalacc trm = 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 + match kind trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; - let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma ty) in + let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in + let ev = EConstr.Unsafe.to_constr ev in gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> @@ -430,14 +428,14 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f + if is_template_polymorphic env sigma (EConstr.of_constr f) then - let l' = meta_free_prefix l in - (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) + let l' = meta_free_prefix sigma l in + (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) else mk_hdgoals sigma goal goalacc f in 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 + let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Case (ci,p,c,lf) -> @@ -451,68 +449,74 @@ and mk_hdgoals sigma goal goalacc trm = 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') + else 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 + let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in (acc',ty,sigma,c) | _ -> - if !check && occur_meta trm then - anomaly (Pp.str "refine called with a dependent meta"); - goalacc, goal_type_of env sigma trm, sigma, trm + if !check && occur_meta sigma (EConstr.of_constr trm) then + anomaly (Pp.str "refine called with a dependent meta."); + let (sigma, ty) = goal_type_of env sigma trm in + goalacc, ty, sigma, trm and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_all (Goal.V82.env sigma goal) sigma funty in - let rec collapse t = match kind_of_term t with + let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = EConstr.Unsafe.to_constr t in + let rec collapse t = match kind t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t in let t = collapse t in - match kind_of_term t with + match kind 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))) + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,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 let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in - let indspec = + let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct - with Not_found -> anomaly (Pp.str "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 indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in + let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') let convert_hyp check sign sigma d = - let id,b,bt = to_tuple d in - let env = Global.env() in + let id = NamedDecl.get_id d in + let b = NamedDecl.get_value d in + let env = Global.env () in let reorder = ref [] in let sign' = - apply_to_hyp check sign id + apply_to_hyp env sigma check sign id (fun _ d' _ -> - let _,c,ct = to_tuple d' in + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in let env = Global.env_of_context sign in - if check && not (is_conv env sigma bt ct) then - errorlabstrm "Logic.convert_hyp" - (str "Incorrect change of the type of " ++ pr_id id ++ str "."); + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - errorlabstrm "Logic.convert_hyp" - (str "Incorrect change of the body of "++ pr_id id ++ str "."); - if check then reorder := check_decl_position env sign d; - d) in - reorder_val_context env sign' !reorder - - + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the body of "++ Id.print id ++ str "."); + if check then reorder := check_decl_position env sigma sign d; + map_named_decl EConstr.Unsafe.to_constr d) in + reorder_val_context env sigma sign' !reorder (************************************************************************) (************************************************************************) @@ -520,37 +524,13 @@ let convert_hyp check sign sigma d = let prim_refiner r sigma goal = 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 *) - | 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,t,cl,sigma = - if replace then - let nexthyp = get_hyp_after id (named_context_of_val sign) in - let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) - nexthyp, - t,cl,sigma - else - (if !check && mem_named_context_val id sign then - errorlabstrm "Logic.prim_refiner" - (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (LocalAssum (id,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.mkNamedLetIn id ev1 t ev2 in - let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in - if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | Refine c -> - check_meta_variables c; + let cl = EConstr.Unsafe.to_constr cl in + check_meta_variables env sigma c; 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 + let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in (sgl, sigma) |