diff options
Diffstat (limited to 'pretyping')
30 files changed, 519 insertions, 384 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e7b17991e3..c3f392980a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -32,7 +32,6 @@ open Evardefine open Evarsolve open Evarconv open Evd -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -70,7 +69,7 @@ let error_wrong_numarg_inductive ?loc env c n = let list_try_compile f l = let rec aux errors = function - | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors) + | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors) | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> @@ -162,9 +161,9 @@ let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) | Continuation (n, _, _) -> - anomaly (str "Bad number of expected remaining patterns: " ++ int n) + anomaly (str "Bad number of expected remaining patterns: " ++ int n ++ str ".") | Result _ -> - anomaly (Pp.str "Exhausted pattern history") + anomaly (Pp.str "Exhausted pattern history.") (* This is for non exhaustive error message *) @@ -190,7 +189,7 @@ let pop_history_pattern = function | Continuation (0, l, MakeConstructor (pci, rh)) -> feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> - anomaly (Pp.str "Constructor not yet filled with its arguments") + anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = feed_history (CAst.make @@ PatVar Anonymous) h @@ -425,7 +424,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1 let current_pattern eqn = match eqn.patterns with | pat::_ -> pat - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let alias_of_pat = CAst.with_val (function | PatVar name -> name @@ -438,7 +437,7 @@ let remove_current_pattern eqn = { eqn with patterns = pats; alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") let push_current_pattern (cur,ty) eqn = match eqn.patterns with @@ -447,7 +446,7 @@ let push_current_pattern (cur,ty) eqn = { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } - | [] -> anomaly (Pp.str "Empty list of patterns") + | [] -> anomaly (Pp.str "Empty list of patterns.") (* spiwack: like [push_current_pattern] but does not introduce an alias in rhs_env. Aliasing binders are only useful for variables at @@ -457,7 +456,7 @@ let push_noalias_current_pattern eqn = match eqn.patterns with | _::pats -> { eqn with patterns = pats } - | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns") + | [] -> anomaly (Pp.str "push_noalias_current_pattern: Empty list of patterns.") @@ -641,7 +640,7 @@ let replace_tomatch sigma n c = | Pushed (initial,((b,tm),l,na)) :: rest -> let b = replace_term sigma n c depth b in let tm = map_tomatch_type (replace_term sigma n c depth) tm in - List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l; + List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch.")) l; Pushed (initial,((b,tm),l,na)) :: replrec depth rest | Alias (initial,(na,b,d)) :: rest -> (* [b] is out of replacement scope *) @@ -731,7 +730,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(out_name na)::avoid)) + (na::l,(Name.get_id na)::avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -882,7 +881,7 @@ let specialize_predicate_var (cur,typ,dep) env tms ccl = (*****************************************************************************) let generalize_predicate sigma (names,na) ny d tms ccl = let () = match na with - | Anonymous -> anomaly (Pp.str "Undetected dependency") + | Anonymous -> anomaly (Pp.str "Undetected dependency.") | _ -> () in let p = List.length names + 1 in let ccl = lift_predicate 1 ccl tms in @@ -961,7 +960,6 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in (p+k,liftn_predicate (k-1) (p+1) ccl tms) - let use_unit_judge evd = let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in @@ -1709,7 +1707,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in - if not b then anomaly (Pp.str "Build_tycon: should be a type"); + if not b then anomaly (Pp.str "Build_tycon: should be a type."); { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -1873,7 +1871,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = if not (eq_ind ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then - anomaly (Pp.str "Ill-formed 'in' clause in cases"); + anomaly (Pp.str "Ill-formed 'in' clause in cases."); List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in LocalAssum (na, EConstr.of_constr (build_dependent_inductive env0 indf')) @@ -2001,10 +1999,8 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let sigma,t = match tycon with | Some t -> refresh_tycon sigma t | None -> - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((t, _), sigma, _) = + let (sigma, (t, _)) = new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in - let sigma = Sigma.to_evar_map sigma in sigma, t in (* First strategy: we build an "inversion" predicate *) @@ -2065,8 +2061,8 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = CAst.make @@ - GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false), +let hole na = CAst.make @@ + GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = @@ -2169,7 +2165,7 @@ let vars_of_ctx sigma ctx = prev, (CAst.make @@ GApp ( (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole; CAst.make @@ GVar prev])) :: vars + [hole na; CAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" @@ -2224,14 +2220,14 @@ let build_ineqs evdref prevpatterns pats liftsign = (Some ([], 0, 0, [])) eqnpats pats in match acc with None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c')) - (lift_rel_context liftsign sign) - in - conj :: c) + | Some (sign, len, _, c') -> + let sigma, conj = mk_coq_and !evdref c' in + let sigma, neg = mk_coq_not sigma conj in + let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in + evdref := sigma; conj :: c) [] prevpatterns in match diffs with [] -> None - | _ -> Some (mk_coq_and diffs) + | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj) let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let i = ref 0 in @@ -2302,7 +2298,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = | l -> CAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> CAst.make @@ GApp (branch, [ hole ]) + Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 782552583d..6c2086f3e0 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -132,6 +132,7 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) +type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map } (* Change: zeta reduction cannot be avoided in CBV *) @@ -189,6 +190,43 @@ let pr_key = function | VarKey id -> Names.Id.print id | RelKey n -> Pp.(str "REL_" ++ int n) +let rec reify_stack t = function + | TOP -> t + | APP (args,st) -> + reify_stack (mkApp(t,Array.map reify_value args)) st + | CASE (ty,br,ci,env,st) -> + reify_stack + (mkCase (ci, ty, t,br)) + st + | PROJ (p, pinfo, st) -> + reify_stack (mkProj (p, t)) st + +and reify_value = function (* reduction under binders *) + | VAL (n,t) -> lift n t + | STACK (0,v,stk) -> + reify_stack (reify_value v) stk + | STACK (n,v,stk) -> + lift n (reify_stack (reify_value v) stk) + | CBN(t,env) -> + t + (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) + | LAM (n,ctxt,b,env) -> + List.fold_left (fun c (n,t) -> Term.mkLambda (n, t, c)) b ctxt + | FIXP ((lij,(names,lty,bds)),env,args) -> + mkApp + (mkFix (lij, + (names, + lty, + bds)), + Array.map reify_value args) + | COFIXP ((j,(names,lty,bds)),env,args) -> + mkApp + (mkCoFix (j, + (names,lty,bds)), + Array.map reify_value args) + | CONSTR (c,args) -> + mkApp(mkConstructU c, Array.map reify_value args) + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -213,12 +251,12 @@ let rec norm_head info env t stack = | Proj (p, c) -> let p' = - if red_set (info_flags info) (fCONST (Projection.constant p)) - && red_set (info_flags info) fBETA + if red_set (info_flags info.infos) (fCONST (Projection.constant p)) + && red_set (info_flags info.infos) fBETA then Projection.unfold p else p in - let pinfo = Environ.lookup_projection p (info_env info) in + let pinfo = Environ.lookup_projection p (info_env info.infos) in norm_head info env c (PROJ (p', pinfo, stack)) (* constants, axioms @@ -233,14 +271,16 @@ let rec norm_head info env t stack = | Var id -> norm_head_ref 0 info env stack (VarKey id) - | Const sp -> norm_head_ref 0 info env stack (ConstKey sp) + | Const sp -> + Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma t (lazy (reify_stack t stack)); + norm_head_ref 0 info env stack (ConstKey sp) | LetIn (_, b, _, c) -> (* zeta means letin are contracted; delta without zeta means we *) (* allow bindings but leave let's in place *) - if red_set (info_flags info) fZETA then + if red_set (info_flags info.infos) fZETA then (* New rule: for Cbv, Delta does not apply to locally bound variables - or red_set (info_flags info) fDELTA + or red_set (info_flags info.infos) fDELTA *) let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack @@ -248,7 +288,7 @@ let rec norm_head info env t stack = (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info.i_cache ev with + (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack | None -> (VAL(0, t), stack)) @@ -265,8 +305,8 @@ let rec norm_head info env t stack = | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt = - if red_set_ref (info_flags info) normt then - match ref_value_cache info normt with + if red_set_ref (info_flags info.infos) normt then + match ref_value_cache info.infos normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); strip_appl (shift_value k body) stack @@ -291,7 +331,7 @@ and cbv_stack_term info stack env t = and cbv_stack_value info env = function (* a lambda meets an application -> BETA *) | (LAM (nlams,ctxt,b,env), APP (args, stk)) - when red_set (info_flags info) fBETA -> + when red_set (info_flags info.infos) fBETA -> let nargs = Array.length args in if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b @@ -305,31 +345,31 @@ and cbv_stack_value info env = function (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) - when fixp_reducible (info_flags info) fix stk -> + when fixp_reducible (info_flags info.infos) fix stk -> let (envf,redfix) = contract_fixp env fix in cbv_stack_term info stk envf redfix (* constructor guard satisfied or Cofix in a Case -> IOTA *) | (COFIXP(cofix,env,[||]), stk) - when cofixp_reducible (info_flags info) cofix stk-> + when cofixp_reducible (info_flags info.infos) cofix stk-> let (envf,redfix) = contract_cofixp env cofix in cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info) fMATCH -> + when red_set (info_flags info.infos) fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info) fMATCH -> + when red_set (info_flags info.infos) fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk))) - when red_set (info_flags info) fMATCH && Projection.unfolded p -> + when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in cbv_stack_value info env (strip_appl arg stk) @@ -337,7 +377,7 @@ and cbv_stack_value info env = function | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl) | (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl) | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl) - + (* definitely a value *) | (head,stk) -> mkSTACK(head, stk) @@ -400,12 +440,11 @@ let cbv_norm infos constr = let constr = EConstr.Unsafe.to_constr constr in EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))) -type cbv_infos = cbv_value infos - (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = - create - (fun old_info c -> cbv_stack_term old_info TOP (subs_id 0) c) + let infos = create + (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c) flgs env - (Reductionops.safe_evar_value sigma) + (Reductionops.safe_evar_value sigma) in + { infos; sigma } diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3ef17912f7..1282e3cb86 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -67,7 +67,7 @@ let apply_coercion_args env evd check isproj argl funj = if check && not (e_cumul env evdref (Retyping.get_type_of env !evdref h) c1) then raise NoCoercion; apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly (Pp.str "apply_coercion_args") + | _ -> anomaly (Pp.str "apply_coercion_args.") in let res = apply_rec [] funj.uj_type argl in !evdref, res @@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 = open Program -let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c = - let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c = + let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = @@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc env evdref eq in + let evar = make_existential ?loc n env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) Some (fun x -> let cx = app_opt env evdref c x in - let evar = make_existential ?loc env evdref (mkApp (p, [| cx |])) + let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |])) in (papp evdref sig_intro [| u; p; cx; evar |])) | None -> @@ -368,7 +368,7 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion") + | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index edcfa99c86..2cb837ba03 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -220,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PSoApp (n,args),m -> let fold (ans, seen) = function | PRel n -> - let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in (n :: ans, Int.Set.add n seen) - | _ -> error "Only bound indices allowed in second order pattern matching." + | _ -> user_err (str "Only bound indices allowed in second order pattern matching.") in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in let frels = free_rels sigma cT in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 752819aa39..c93b1e568c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -425,7 +425,7 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) +let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = @@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs = let nal,c = it_destRLambda_or_LetIn_names n b in let mkPatVar na = CAst.make @@ PatVar na in let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in - let map name = try Some (Nameops.out_name name) with Failure _ -> None in - let ids = List.map_filter map nal in + let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 42aaf3a227..3757ba7e6d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -23,7 +23,6 @@ open Evardefine open Evarsolve open Evd open Pretype_errors -open Sigma.Notations open Context.Named.Declaration module RelDecl = Context.Rel.Declaration @@ -42,6 +41,31 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(*******************************************) +(* Functions to deal with impossible cases *) +(*******************************************) +(* XXX: we would like to search for this with late binding + "data.id.type" etc... *) +let impossible_default_case () = + let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let (_, u) = Term.destConst c in + Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + +let coq_unit_judge = + let open Environ in + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in + fun () -> + match impossible_default_case () with + | Some (id, type_of_id, ctx) -> + make_judge id type_of_id, ctx + | None -> + (* In case the constants id/ID are not defined *) + Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -351,7 +375,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = match ground_test with | Some result -> result | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not + (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta (fst ts) env evd term1 in let term2 = apprec_nohdbeta (fst ts) env evd term2 in @@ -613,7 +637,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -730,7 +754,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -791,7 +815,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in + let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> @@ -888,9 +912,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (i,t2::ks, m-1, test) else let dloc = Loc.tag Evar_kinds.InternalHole in - let i = Sigma.Unsafe.of_evar_map i in - let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in - let i' = Sigma.to_evar_map i' in + let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in @@ -1051,7 +1073,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> - error "Cannot force abstraction on identity instance." + user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end @@ -1063,20 +1085,19 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with | Some Locus.AllOccurrences -> mkVar id - | Some _ -> error "Selection of specific occurrences not supported" + | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in - let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in - let evd = Sigma.to_evar_map evd in + let evd = !evdref in + let (evd, ev) = new_evar_instance sign evd evty ~filter instance in evdref := evd; evsref := (fst (destEvar !evdref ev),evty)::!evsref; ev in @@ -1108,10 +1129,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* This is an arbitrary choice *) let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else @@ -1245,7 +1266,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | None -> evd | Some (evk,ev_info,l) -> let rec aux = function - | [] -> error "Unsolvable existential variables." + | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 7cee1e8a7e..45857df2ae 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index a116198465..2d86daadb6 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -17,15 +17,9 @@ open Namegen open Evd open Evarutil open Pretype_errors -open Sigma.Notations module RelDecl = Context.Rel.Declaration -let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in - (Sigma.to_evar_map evd, evk) - let env_nf_evar sigma env = let nf_evar c = nf_evar sigma c in process_rel_context @@ -82,9 +76,7 @@ let define_pure_evar_as_product evd evk = let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in let s = destSort evd concl in let evd1,(dom,u1) = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in - (Sigma.to_evar_map evd1, e) + new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (LocalAssum (id, dom)) evenv in @@ -92,13 +84,11 @@ let define_pure_evar_as_product evd evk = let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) - new_evar_unsafe newenv evd1 concl ~src ~filter + new_evar newenv evd1 concl ~src ~filter else let status = univ_flexible_alg in let evd3, (rng, srng) = - let evd1 = Sigma.Unsafe.of_evar_map evd1 in - let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in - (Sigma.to_evar_map evd3, e) + new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in @@ -143,7 +133,7 @@ let define_pure_evar_as_lambda env evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in - let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in + let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4ada91eb59..ff0aeff75d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -20,7 +20,6 @@ open Retyping open Reductionops open Evarutil open Pretype_errors -open Sigma.Notations let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with @@ -203,9 +202,7 @@ let restrict_evar_key evd evk filter candidates = let candidates = match candidates with | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates | UpdateWith c -> Some c in - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in - (Sigma.to_evar_map sigma, evk) + restrict_evar evd evk filter candidates end (* Restrict an applied evar and returns its restriction in the same context *) @@ -634,7 +631,7 @@ let make_projectable_subst aliases sigma evi args = cstrs) | _ -> (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) - | _ -> anomaly (Pp.str "Instance does not match its signature")) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -649,9 +646,7 @@ let make_projectable_subst aliases sigma evi args = *) let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evar_in_env, evd, _) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in - let evd = Sigma.to_evar_map evd in + let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in let t_in_env = whd_evar evd t_in_env in let (evk, _) = destEvar evd evar_in_env in let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in @@ -721,10 +716,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = ~status:univ_flexible (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd src ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (ev2_in_sign, evd, _) = + let (evd, ev2_in_sign) = new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in - let evd = Sigma.to_evar_map evd in let ev2_in_env = (fst (destEvar evd ev2_in_sign), Array.of_list inst2_in_env) in (evd, ev2_in_sign, ev2_in_env) @@ -828,7 +821,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> subst' end | [] -> subst' - | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance") + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") else subst' in Id.Map.fold is_projectable subst [] @@ -1050,7 +1043,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with - | UpdateWith [], _ -> error "Not solvable." + | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) @@ -1230,7 +1223,7 @@ let check_evar_instance evd evk1 body conv_algo = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> error "Ill-typed evar instance" + with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 923d7d9388..62ff9ac708 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -12,6 +12,7 @@ open Nameops open Globnames open Misctypes open Glob_term +open Evar_kinds (* Untyped intermediate terms, after ASTs and before constr. *) @@ -33,109 +34,108 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) = (na,k,comp1,comp2) let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Decl_kinds.Explicit, Decl_kinds.Explicit -> true -| Decl_kinds.Implicit, Decl_kinds.Implicit -> true -| _ -> false + | Decl_kinds.Explicit, Decl_kinds.Explicit -> true + | Decl_kinds.Implicit, Decl_kinds.Implicit -> true + | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false let case_style_eq s1 s2 = match s1, s2 with -| LetStyle, LetStyle -> true -| IfStyle, IfStyle -> true -| LetPatternStyle, LetPatternStyle -> true -| MatchStyle, MatchStyle -> true -| RegularStyle, RegularStyle -> true -| _ -> false + | LetStyle, LetStyle -> true + | IfStyle, IfStyle -> true + | LetPatternStyle, LetPatternStyle -> true + | MatchStyle, MatchStyle -> true + | RegularStyle, RegularStyle -> true + | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with -| PatVar na1, PatVar na2 -> Name.equal na1 na2 -| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && - Name.equal na1 na2 -| _ -> false + | PatVar na1, PatVar na2 -> Name.equal na1 na2 + | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> + eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Name.equal na1 na2 + | (PatVar _ | PatCstr _), _ -> false let cast_type_eq eq t1 t2 = match t1, t2 with -| CastConv t1, CastConv t2 -> eq t1 t2 -| CastVM t1, CastVM t2 -> eq t1 t2 -| CastCoerce, CastCoerce -> true -| CastNative t1, CastNative t2 -> eq t1 t2 -| _ -> false - -let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with -| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 -| GVar id1, GVar id2 -> Id.equal id1 id2 -| GEvar (id1, arg1), GEvar (id2, arg2) -> - Id.equal id1 id2 && - List.equal instance_eq arg1 arg2 -| GPatVar (b1, pat1), GPatVar (b2, pat2) -> - (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (f1, arg1), GApp (f2, arg2) -> - glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 -| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> - Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> - case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && - List.equal tomatch_tuple_eq tp1 tp2 && - List.equal cases_clause_eq cl1 cl2 -| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> - List.equal Name.equal na1 na2 && Name.equal n1 n2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> - glob_constr_eq m1 m2 && Name.equal pat1 pat2 && - Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 -| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> - fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && - Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 && - Array.equal glob_constr_eq c1 c2 && - Array.equal glob_constr_eq t1 t2 -| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 -| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) && - Miscops.intro_pattern_naming_eq nam1 nam2 -| GCast (c1, t1), GCast (c2, t2) -> - glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 -| _ -> false - -and tomatch_tuple_eq (c1, p1) (c2, p2) = + | CastConv t1, CastConv t2 -> eq t1 t2 + | CastVM t1, CastVM t2 -> eq t1 t2 + | CastCoerce, CastCoerce -> true + | CastNative t1, CastNative t2 -> eq t1 t2 + | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> false + +let matching_var_kind_eq k1 k2 = match k1, k2 with +| FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2 +| SecondOrderPatVar id1, SecondOrderPatVar id2 -> Id.equal id1 id2 +| (FirstOrderPatVar _ | SecondOrderPatVar _), _ -> false + +let tomatch_tuple_eq f (c1, p1) (c2, p2) = let eqp (_, (i1, na1)) (_, (i2, na2)) = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in - glob_constr_eq c1 c2 && eq_pred p1 p2 + f c1 c2 && eq_pred p1 p2 -and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) = - List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && - glob_constr_eq c1 c2 +and cases_clause_eq f (_, (id1, p1, c1)) (_, (id2, p2, c2)) = + List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && f c1 c2 -and glob_decl_eq (na1, bk1, c1, t1) (na2, bk2, c2, t2) = +let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && - Option.equal glob_constr_eq c1 c2 && - glob_constr_eq t1 t2 - -and fix_kind_eq k1 k2 = match k1, k2 with -| GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a1 -| GCoFix i1, GCoFix i2 -> Int.equal i1 i2 -| _ -> false - -and fix_recursion_order_eq o1 o2 = match o1, o2 with -| GStructRec, GStructRec -> true -| GWfRec c1, GWfRec c2 -> glob_constr_eq c1 c2 -| GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - glob_constr_eq c1 c2 && Option.equal glob_constr_eq o1 o2 -| _ -> false - -and instance_eq (x1,c1) (x2,c2) = - Id.equal x1 x2 && glob_constr_eq c1 c2 + Option.equal f c1 c2 && f t1 t2 + +let fix_recursion_order_eq f o1 o2 = match o1, o2 with + | GStructRec, GStructRec -> true + | GWfRec c1, GWfRec c2 -> f c1 c2 + | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> + f c1 c2 && Option.equal f o1 o2 + | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false + +let fix_kind_eq f k1 k2 = match k1, k2 with + | GFix (a1, i1), GFix (a2, i2) -> + let eq (i1, o1) (i2, o2) = + Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 + in + Int.equal i1 i2 && Array.equal eq a1 a1 + | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 + | (GFix _ | GCoFix _), _ -> false + +let instance_eq f (x1,c1) (x2,c2) = + Id.equal x1 x2 && f c1 c2 + +let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with + | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 + | GVar id1, GVar id2 -> Id.equal id1 id2 + | GEvar (id1, arg1), GEvar (id2, arg2) -> + Id.equal id1 id2 && List.equal (instance_eq f) arg1 arg2 + | GPatVar k1, GPatVar k2 -> matching_var_kind_eq k1 k2 + | GApp (f1, arg1), GApp (f2, arg2) -> + f f1 f2 && List.equal f arg1 arg2 + | GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> + Name.equal na1 na2 && binding_kind_eq bk1 bk2 && f t1 t2 && f c1 c2 + | GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> + Name.equal na1 na2 && f b1 b2 && Option.equal f t1 t2 && f c1 c2 + | GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> + case_style_eq st1 st2 && Option.equal f c1 c2 && + List.equal (tomatch_tuple_eq f) tp1 tp2 && + List.equal (cases_clause_eq f) cl1 cl2 + | GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> + List.equal Name.equal na1 na2 && Name.equal n1 n2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> + f m1 m2 && Name.equal pat1 pat2 && + Option.equal f p1 p2 && f c1 c2 && f t1 t2 + | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> + fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && + Array.equal f c1 c2 && Array.equal f t1 t2 + | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 + | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 + | GCast (c1, t1), GCast (c2, t2) -> + f c1 c2 && cast_type_eq f t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + +let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c let map_glob_constr_left_to_right f = CAst.map (function | GApp (g,args) -> @@ -215,20 +215,20 @@ let fold_glob_constr f acc = CAst.with_val (function ) let fold_return_type_with_binders f g v acc (na,tyopt) = - Option.fold_left (f (name_fold g na v)) acc tyopt + Option.fold_left (f (Name.fold_right g na v)) acc tyopt let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left (f v) (f v acc c) args | GLambda (na,_,b,c) | GProd (na,_,b,c) -> - f (name_fold g na v) (f v acc b) c + f (Name.fold_right g na v) (f v acc b) c | GLetIn (na,b,t,c) -> - f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c | GCases (_,rtntypopt,tml,pl) -> let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'') - (name_fold g na v') onal, + (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal, f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in let acc = Option.fold_left (f v') acc rtntypopt in @@ -242,7 +242,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let v,acc = List.fold_left (fun (v,acc) (na,k,bbd,bty) -> - (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) (v,acc) bll.(i) in f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in @@ -371,12 +371,12 @@ let loc_of_glob_constr c = c.CAst.loc let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l let test_id l id = if collide_id l id then raise Not_found -let test_na l na = name_iter (test_id l) na +let test_na l na = Name.iter (test_id l) na let update_subst na l = let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in - let l' = name_fold Id.List.remove_assoc na l in - name_fold + let l' = Name.fold_right Id.List.remove_assoc na l in + Name.fold_right (fun id _ -> if in_range id l' then let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in @@ -457,11 +457,44 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function | _ -> raise Not_found ) +open Declarations +open Term +open Context + +(* Keep only patterns which are not bound to a local definitions *) +let drop_local_defs typi args = + let (decls,_) = decompose_prod_assum typi in + let rec aux decls args = + match decls, args with + | [], [] -> [] + | Rel.Declaration.LocalDef _ :: decls, pat :: args -> + begin + match pat.CAst.v with + | PatVar Anonymous -> aux decls args + | _ -> raise Not_found (* The pattern is used, one cannot drop it *) + end + | Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args + | _ -> assert false in + aux (List.rev decls) args + +let add_patterns_for_params_remove_local_defs (ind,j) l = + let (mib,mip) = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + let l = + if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then + (* Optimisation *) l + else + let typi = mip.mind_nf_lc.(j-1) in + let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in + drop_local_defs typi l in + Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l + (* Turn a closed cases pattern into a glob_constr *) let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) | PatCstr (cstr,l,Anonymous) -> let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in + let l = add_patterns_for_params_remove_local_defs cstr l in GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found ) x diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index aa48516aff..75db04f77f 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -36,6 +36,9 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit +val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> + glob_constr -> glob_constr -> bool + val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit @@ -78,3 +81,5 @@ val map_pattern : (glob_constr -> glob_constr) -> val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr + +val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index c4a74d990b..97aec1814f 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -27,7 +27,6 @@ open Inductiveops open Environ open Reductionops open Nametab -open Sigma.Notations open Context.Rel.Declaration type dep_flag = bool @@ -130,19 +129,19 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = it_mkLambda_or_LetIn_name env' obj deparsign else let cs = lift_constructor (k+1) constrs.(k) in - let t = build_branch_type env (Sigma.to_evar_map sigma) dep (mkRel (k+1)) cs in + let t = build_branch_type env sigma dep (mkRel (k+1)) cs in mkLambda_string "f" t (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) in - let Sigma (s, sigma, p) = Sigma.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in - let typP = make_arity env' (Sigma.to_evar_map sigma) dep indf s in + let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in + let typP = make_arity env' sigma dep indf s in let typP = EConstr.Unsafe.to_constr typP in let c = it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar in - Sigma (c, sigma, p) + (sigma, c) (* check if the type depends recursively on one of the inductive scheme *) @@ -296,7 +295,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f - | _,[] | [],_ -> anomaly (Pp.str "process_constr") + | _,[] | [],_ -> anomaly (Pp.str "process_constr.") in process_constr env 0 f (List.rev cstr.cs_args, recargs) @@ -475,10 +474,9 @@ let mis_make_indrec env sigma listdepkind mib u = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (c, sigma, _) = mis_make_case_com dep env sigma (indi,u) (mibi,mipi) kind in - let evd' = Sigma.to_evar_map sigma in - evdref := evd'; c + let evd = !evdref in + let (evd, c) = mis_make_case_com dep env evd (indi,u) (mibi,mipi) kind in + evdref := evd; c in (* Body of mis_make_indrec *) !evdref, List.init nrec make_one_rec @@ -533,7 +531,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') - | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") in let ty, term = drec npars ty in !evdref, ty, term @@ -577,7 +575,7 @@ let build_mutual_induction_scheme env sigma = function in let _ = check_arities env listdepkind in mis_make_indrec env sigma listdepkind mib u - | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") + | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 192b64a5ed..a22470ae8c 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -26,14 +26,14 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) -val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> - dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma +val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive -> + dep_flag -> sorts_family -> evar_map * Constr.t (** Build a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections. *) -val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> - sorts_family -> (constr, 'r) Sigma.sigma +val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> + sorts_family -> evar_map * Constr.t (** Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 429e5005ec..d8252ea9bb 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and ntypes = mib.mind_ntypes and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in - if j > nconstr then error "Not enough constructors in the type."; + if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) (* Number of constructors *) @@ -538,7 +538,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = | Name _ -> true end - | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate") + | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate.") in srec env (EConstr.of_constr pred) arsign diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e4fbf8d542..e555742bca 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - CErrors.error "This tactic does not support occurrences selection" in + CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in let error_body_selection () = - CErrors.error "This tactic does not support body selection" in + CErrors.user_err Pp.(str "This tactic does not support body selection") in let hyps = match cl.onhyps with | None -> @@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl = (** Miscellaneous functions *) let out_arg = function - | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.") | Misctypes.ArgArg x -> x let occurrences_of_hyp id cls = diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0228f63cdc..61118cf777 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -139,7 +139,7 @@ let type_of_var env id = let open Context.Named.Declaration in try env |> lookup_named id |> get_type with Not_found -> - anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound") + anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.") let sort_of_product env domsort rangsort = match (domsort, rangsort) with @@ -383,7 +383,7 @@ let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in if Coq_config.no_native_compiler then - error "Native_compute reduction has been disabled at configure time." + user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in (* @@ -405,7 +405,7 @@ let native_norm env sigma c ty = let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); EConstr.of_constr res - | _ -> anomaly (Pp.str "Compilation failure") + | _ -> anomaly (Pp.str "Compilation failure.") let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a8012d35f8..c36542aebc 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -112,14 +112,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type.") let head_of_constr_reference sigma c = match EConstr.kind sigma c with | Const (sp,_) -> ConstRef sp | Construct (sp,_) -> ConstructRef sp | Ind (sp,_) -> IndRef sp | Var id -> VarRef id - | _ -> anomaly (Pp.str "Not a rigid reference") + | _ -> anomaly (Pp.str "Not a rigid reference.") let pattern_of_constr env sigma t = let rec pattern_of_constr env t = @@ -143,7 +143,7 @@ let pattern_of_constr env sigma t = match kind_of_term f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with - Evar_kinds.MatchingVar (true,id) -> Some id + Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id | _ -> None) | _ -> None with @@ -156,13 +156,14 @@ let pattern_of_constr env sigma t = pattern_of_constr env (EConstr.Unsafe.to_constr (Retyping.expand_projection env sigma p (EConstr.of_constr c) [])) | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with - | Evar_kinds.MatchingVar (b,id) -> - assert (not b); PMeta (Some id) + | Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) -> + PMeta (Some id) | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -230,7 +231,7 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") + | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c @@ -329,26 +330,26 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (false,n) -> + | GPatVar (Evar_kinds.FirstOrderPatVar n) -> metas := n::!metas; PMeta (Some n) | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> + | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | GLambda (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GProd (na,bk,c1,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | GLetIn (na,c1,t,c2) -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) @@ -363,9 +364,9 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = CAst.make ?loc @@ + let mkGLambda na c = CAst.make ?loc @@ GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; @@ -411,7 +412,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function | { CAst.v = PatVar na } -> - name_iter (fun n -> metas := n::!metas) na; + Name.iter (fun n -> metas := n::!metas) na; na | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e72394fa28..92e728683d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -44,8 +44,6 @@ open Glob_ops open Evarconv open Pattern open Misctypes -open Tactypes -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -111,9 +109,9 @@ let e_new_evar env evdref ?src ?naming typ = let typ' = subst2 subst vsubst typ in let instance = inst_rels @ inst_vars in let sign = val_of_named_context nc in - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in - evdref := Sigma.to_evar_map sigma; + let sigma = !evdref in + let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in + evdref := sigma; e let push_rec_types sigma (lna,typarray,_) env = @@ -199,7 +197,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = let names, _ = Global.global_universe_names () in if CString.string_contains ~where:s ~what:"." then match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) + | [] -> anomaly (str"Invalid universe name " ++ str s ++ str".") | n :: dp -> let num = int_of_string n in let dp = DirPath.make (List.map Id.of_string dp) in @@ -383,6 +381,20 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c +let adjust_evar_source evdref na c = + match na, kind !evdref c with + | Name id, Evar (evk,args) -> + let evi = Evd.find !evdref evk in + begin match evi.evar_source with + | loc, Evar_kinds.QuestionMark (b,Anonymous) -> + let src = (loc,Evar_kinds.QuestionMark (b,na)) in + let (evd, evk') = restrict_evar !evdref evk (evar_filter evi) ~src None in + evdref := evd; + mkEvar (evk',args) + | _ -> c + end + | _, _ -> c + (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false @@ -556,12 +568,12 @@ let pretype_sort ?loc evdref = function | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s let new_type_evar env evdref loc = - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma ((e, _), sigma, _) = + let sigma = !evdref in + let (sigma, (e, _)) = Evarutil.new_type_evar env.ExtraEnv.env sigma univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in - evdref := Sigma.to_evar_map sigma; + evdref := sigma; e module ConstrInterpObj = @@ -610,13 +622,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (someta,n) -> + | GPatVar kind -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - let k = Evar_kinds.MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar kind in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> @@ -785,6 +797,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre args, nf_evar !evdref (j_val hj) else [], j_val hj in + let ujval = adjust_evar_source evdref na ujval in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in let j = { uj_val = value; uj_type = typ } in apply_rec env (n+1) j candargs rest @@ -1133,7 +1146,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | Sort s -> ESorts.kind sigma s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev - | _ -> anomaly (Pp.str "Found a type constraint which is not a type") + | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in { utj_val = v; utj_type = s } @@ -1251,7 +1264,7 @@ let constr_flags = { (* Fully evaluate an untyped constr *) let type_uconstr ?(flags = constr_flags) ?(expected_type = WithoutTypeConstraint) ist c = - { delayed = begin fun env sigma -> + begin fun env sigma -> let { closure; term } = c in let vars = { ltac_constrs = closure.typed; @@ -1259,10 +1272,8 @@ let type_uconstr ?(flags = constr_flags) ltac_idents = closure.idents; ltac_genargs = Id.Map.empty; } in - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - Sigma.Unsafe.of_pair (c, sigma) - end } + understand_ltac flags env sigma vars expected_type term + end let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/program.ml b/pretyping/program.ml index de485dbe84..f9be82024a 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,26 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Util -open Names -let make_dir l = DirPath.make (List.rev_map Id.of_string l) - -let find_reference locstr dir s = - let dp = make_dir dir in - let sp = Libnames.make_path dp (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - user_err (str "Library " ++ Libnames.pr_dirpath dp ++ - str " has to be required first.") - -let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) - -let init_constant dir s () = coq_constant "Program" dir s -let init_reference dir s () = coq_reference "Program" dir s +let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in @@ -54,20 +38,20 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" -let coq_not = init_constant ["Init";"Logic"] "not" -let coq_and = init_constant ["Init";"Logic"] "and" - -let delayed_force c = EConstr.of_constr (c ()) +let coq_not = init_reference ["Init";"Logic"] "not" +let coq_and = init_reference ["Init";"Logic"] "and" -let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |]) +let mk_coq_not sigma x = + let sigma, notc = Evarutil.new_global sigma (coq_not ()) in + sigma, EConstr.mkApp (notc, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" -let mk_coq_and l = - let and_typ = delayed_force coq_and in - unsafe_fold_right +let mk_coq_and sigma l = + let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in + sigma, unsafe_fold_right (fun c conj -> EConstr.mkApp (and_typ, [| c ; conj |])) l diff --git a/pretyping/program.mli b/pretyping/program.mli index 94a7bdcb6d..8439b9528c 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference val coq_JMeq_ind : unit -> global_reference val coq_JMeq_refl : unit -> global_reference -val mk_coq_and : constr list -> constr -val mk_coq_not : constr -> constr +val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr +val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 7d65925e57..8e190f40b9 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -20,13 +20,13 @@ let make_red_flag l = | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 117ed338ee..c2a6483012 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -40,6 +40,54 @@ let _ = Goptions.declare_bool_option { let get_refolding_in_reduction () = !refolding_in_reduction let set_refolding_in_reduction = (:=) refolding_in_reduction +(** Support for reduction effects *) + +open Mod_subst +open Libobject + +type effect_name = string + +(** create a persistent set to store effect functions *) +module ConstrMap = Map.Make (Constr) + +(* Table bindings a constant to an effect *) +let constant_effect_table = Summary.ref ~name:"reduction-side-effect" ConstrMap.empty + +(* Table bindings function key to effective functions *) +let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty + +(** a test to know whether a constant is actually the effect function *) +let reduction_effect_hook env sigma termkey c = + try + let funkey = ConstrMap.find termkey !constant_effect_table in + let effect = String.Map.find funkey !effect_table in + effect env sigma (Lazy.force c) + with Not_found -> () + +let cache_reduction_effect (_,(termkey,funkey)) = + constant_effect_table := ConstrMap.add termkey funkey !constant_effect_table + +let subst_reduction_effect (subst,(termkey,funkey)) = + (subst_mps subst termkey,funkey) + +let inReductionEffect : Constr.constr * string -> obj = + declare_object {(default_object "REDUCTION-EFFECT") with + cache_function = cache_reduction_effect; + open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o); + subst_function = subst_reduction_effect; + classify_function = (fun o -> Substitute o) } + +let declare_reduction_effect funkey f = + if String.Map.mem funkey !effect_table then + CErrors.anomaly Pp.(str "Cannot redeclare effect function " ++ qstring funkey ++ str "."); + effect_table := String.Map.add funkey f !effect_table + +(** A function to set the value of the print function *) +let set_reduction_effect x funkey = + let termkey = Universes.constr_of_global x in + Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) + + (** Machinery to custom the behavior of the reduction *) module ReductionBehaviour = struct open Globnames @@ -595,7 +643,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -777,7 +825,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies context" in contract_fix *) let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = let raw_answer = - let env = if refold then None else Some env in + let env = if refold then Some env else None in contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> @@ -859,9 +907,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (match safe_meta_value sigma ev with | Some body -> whrec cst_l (EConstr.of_constr body, stack) | None -> fold ()) - | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> - let u' = EInstance.kind sigma u in - (match constant_opt_value_in env (fst const, u') with + | Const (c,u as const) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma x) + (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); + if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then + let u' = EInstance.kind sigma u in + (match constant_opt_value_in env (c, u') with | None -> fold () | Some body -> let body = EConstr.of_constr body in @@ -901,7 +952,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some (bef,arg,s') -> whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') - ) + ) else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in let kn = Projection.constant p in @@ -1035,7 +1086,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |_ -> fold () else fold () - | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () + | Rel _ | Var _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in fun xs -> @@ -1219,7 +1270,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1227,7 +1278,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) @@ -1317,19 +1368,23 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) + let open Universes in let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in try - let fold cstr sigma = - try Some (Evd.add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None - in + let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + in + let ans = match ans with + | None -> None + | Some cstr -> + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with | None -> false, sigma @@ -1441,7 +1496,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl @@ -1452,7 +1507,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.") let hnf_lam_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl @@ -1689,5 +1744,5 @@ let betazetaevar_applist sigma n c l = | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar _, _ -> applist (substl env t, stack) - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in stacklam n [] c l diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af80481569..af4ea3ac53 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -34,6 +34,22 @@ end val get_refolding_in_reduction : unit -> bool val set_refolding_in_reduction : bool -> unit +(** {6 Support for reduction effects } *) + +type effect_name = string + +(* [declare_reduction_effect name f] declares [f] under key [name]; + [name] must be a unique in "world". *) +val declare_reduction_effect : effect_name -> + (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit + +(* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *) +val set_reduction_effect : Globnames.global_reference -> effect_name -> unit + +(* [effect_hook env sigma key term] apply effect associated to [key] on [term] *) +val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr -> + Constr.constr Lazy.t -> unit + (** {6 Machinery about a stack of unfolded constant } cst applied to params must convertible to term of the state applied to args @@ -117,7 +133,7 @@ type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 496c706ec6..a1d0977f5a 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -48,7 +48,7 @@ let retype_error re = raise (RetypeError re) let anomaly_on_error f x = try f x - with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) + with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".") let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67221046bd..62737b65e0 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -24,7 +24,6 @@ open Reductionops open Cbv open Patternops open Locus -open Sigma.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -107,7 +106,7 @@ let destEvalRefU sigma c = match EConstr.kind sigma c with | Var id -> (EvalVar id, EInstance.empty) | Rel n -> (EvalRel n, EInstance.empty) | Evar ev -> (EvalEvar ev, EInstance.empty) - | _ -> anomaly (Pp.str "Not an unfoldable reference") + | _ -> anomaly (Pp.str "Not an unfoldable reference.") let unsafe_reference_opt_value env sigma eval = match eval with @@ -307,7 +306,7 @@ let compute_consteval_mutual_fix env sigma ref = (* Forget all \'s and args and do as if we had started with c' *) let ref,_ = destEvalRefU sigma c' in (match unsafe_reference_opt_value env sigma ref with - | None -> anomaly (Pp.str "Should have been trapped by compute_direct") + | None -> anomaly (Pp.str "Should have been trapped by compute_direct.") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in @@ -399,9 +398,8 @@ let substl_with_function subst sigma constr = if i <= k + Array.length v then match v.(i-k-1) with | (fx, Some (min, ref)) -> - let sigma = Sigma.Unsafe.of_evar_map !evd in - let Sigma (evk, sigma, _) = Evarutil.new_pure_evar venv sigma dummy in - let sigma = Sigma.to_evar_map sigma in + let sigma = !evd in + let (sigma, evk) = Evarutil.new_pure_evar venv sigma dummy in evd := sigma; minargs := Evar.Map.add evk min !minargs; Vars.lift k (mkEvar (evk, [|fx;ref|])) @@ -538,20 +536,27 @@ let reduce_mind_case_use_function func env sigma mia = | _ -> assert false -let match_eval_ref env sigma constr = +let match_eval_ref env sigma constr stack = match EConstr.kind sigma constr with - | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> - Some (EvalConst sp, u) + | Const (sp, u) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty) | Rel i -> Some (EvalRel i, EInstance.empty) | Evar ev -> Some (EvalEvar ev, EInstance.empty) | _ -> None -let match_eval_ref_value env sigma constr = +let match_eval_ref_value env sigma constr stack = match EConstr.kind sigma constr with - | Const (sp, u) when is_evaluable env (EvalConstRef sp) -> - let u = EInstance.kind sigma u in - Some (EConstr.of_constr (constant_value_in env (sp, u))) + | Const (sp, u) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + (lazy (EConstr.to_constr sigma (applist (constr,stack)))); + if is_evaluable env (EvalConstRef sp) then + let u = EInstance.kind sigma u in + Some (EConstr.of_constr (constant_value_in env (sp, u))) + else + None | Var id when is_evaluable env (EvalVarRef id) -> env |> lookup_named id |> NamedDecl.get_value | Rel n -> @@ -561,7 +566,7 @@ let match_eval_ref_value env sigma constr = let special_red_case env sigma whfun (ci, p, c, lf) = let rec redrec s = let (constr, cargs) = whfun s in - match match_eval_ref env sigma constr with + match match_eval_ref env sigma constr cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with | None -> raise Redelimination @@ -776,7 +781,7 @@ and whd_simpl_stack env sigma = with Redelimination -> s') | _ -> - match match_eval_ref env sigma x with + match match_eval_ref env sigma x stack with | Some (ref, u) -> (try let sapp, nocase = red_elim_const env sigma ref u stack in @@ -798,7 +803,7 @@ and whd_simpl_stack env sigma = and whd_construct_stack env sigma s = let (constr, cargs as s') = whd_simpl_stack env sigma s in if reducible_mind_case sigma constr then s' - else match match_eval_ref env sigma constr with + else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> (match reference_opt_value env sigma ref u with | None -> raise Redelimination @@ -846,7 +851,7 @@ let try_red_product env sigma c = | Reduced s -> simpfun (applist s) | NotReducible -> raise Redelimination) | _ -> - (match match_eval_ref env sigma x with + (match match_eval_ref env sigma x [] with | Some (ref, u) -> (* TO DO: re-fold fixpoints after expansion *) (* to get true one-step reductions *) @@ -858,7 +863,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "No head constant to reduce." + with Redelimination -> user_err (str "No head constant to reduce.") (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -927,7 +932,7 @@ let whd_simpl_stack = let whd_simpl_orelse_delta_but_fix env sigma c = let rec redrec s = let (constr, stack as s') = whd_simpl_stack env sigma s in - match match_eval_ref_value env sigma constr with + match match_eval_ref_value env sigma constr stack with | Some c -> (match EConstr.kind sigma (snd (decompose_lam sigma c)) with | CoFix _ | Fix _ -> s' @@ -983,11 +988,10 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = | _ -> mkApp (app', [| a' |])) | _ -> map_constr_with_binders_left_to_right sigma g f acc c -let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> +let e_contextually byhead (occs,c) f = begin fun env sigma t -> let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref 1 in - let sigma = Sigma.to_evar_map sigma in (** FIXME: we do suspicious things with this evarmap *) let evd = ref sigma in let rec traverse nested (env,c as envc) t = @@ -1007,8 +1011,8 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> (* Skip inner occurrences for stable counting of occurrences *) if locs != [] then ignore (traverse_below (Some (!pos-1)) envc t); - let Sigma (t, evm, _) = (f subst).e_redfun env (Sigma.Unsafe.of_evar_map !evd) t in - (evd := Sigma.to_evar_map evm; t) + let (evm, t) = (f subst) env !evd t in + (evd := evm; t) end else traverse_below nested envc t @@ -1027,15 +1031,12 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t -> in let t' = traverse None (env,c) t in if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs; - Sigma.Unsafe.of_pair (t', !evd) - end } + (!evd, t') + end let contextually byhead occs f env sigma t = - let f' subst = { e_redfun = begin fun env sigma t -> - Sigma.here (f subst env (Sigma.to_evar_map sigma) t) sigma - end } in - let Sigma (c, _, _) = (e_contextually byhead occs f').e_redfun env (Sigma.Unsafe.of_evar_map sigma) t in - c + let f' subst env sigma t = sigma, f subst env sigma t in + snd (e_contextually byhead occs f' env sigma t) (* linear bindings (following pretty-printer) of the value of name in c. * n is the number of the next occurrence of name. @@ -1080,7 +1081,7 @@ let unfold env sigma name c = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma c else - error (string_of_evaluable_ref env name^" is opaque.") + user_err Pp.(str (string_of_evaluable_ref env name^" is opaque.")) (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -1090,7 +1091,7 @@ let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in if Int.equal nbocc 1 then - error ((string_of_evaluable_ref env name)^" does not occur."); + user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); let rest = List.filter (fun o -> o >= nbocc) locs in let () = match rest with | [] -> () @@ -1112,7 +1113,7 @@ let unfoldn loccname env sigma c = let fold_one_com com env sigma c = let rcom = try red_product env sigma com - with Redelimination -> error "Not reducible." in + with Redelimination -> user_err Pp.(str "Not reducible.") in (* Reason first on the beta-iota-zeta normal form of the constant as unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) @@ -1147,22 +1148,21 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in - if occur_meta sigma ta then error "Cannot find a type for the generalisation."; + if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma else let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in mkLambda (na,ta,c'), sigma' -let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> - let sigma = Sigma.to_evar_map sigma in +let pattern_occs loccs_trm = begin fun env sigma c -> let abstr_trm, sigma = List.fold_right (abstract_scheme env sigma) loccs_trm (c,sigma) in try let _ = Typing.unsafe_type_of env sigma abstr_trm in - Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma) + (sigma, applist(abstr_trm, List.map snd loccs_trm)) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) - end } + end (* Used in several tactics. *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 919e95a8ee..d7b4842810 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -422,7 +422,7 @@ let add_class cl = match inst with | Some (Backward, info) -> (match body with - | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 757e12451e..7ad988ad0b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -31,7 +31,7 @@ let push_rec_types pfix env = let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty @@ -121,11 +121,11 @@ let lambda_applist_assum sigma n c l = let rec app n subst t l = if Int.equal n 0 then if l == [] then substl subst t - else anomaly (Pp.str "Not enough arguments") + else anomaly (Pp.str "Not enough arguments.") else match EConstr.kind sigma t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in app n [] c l let e_type_case_branches env evdref (ind,largs) pj c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cac6c50572..0fb48ed8cf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -31,7 +31,6 @@ open Recordops open Locus open Locusops open Find_subterm -open Sigma.Notations type metabinding = (metavariable * EConstr.constr * (instance_constraint * instance_typing_status)) @@ -145,9 +144,7 @@ let set_occurrences_of_last_arg args = Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) let abstract_list_all_with_dependencies env evd typ c l = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (ev, evd, _) = new_evar env evd typ in - let evd = Sigma.to_evar_map evd in + let (evd, ev) = new_evar env evd typ in let evd,ev' = evar_absorb_arguments env evd (destEvar evd ev) l in let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in @@ -1239,20 +1236,19 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * close it off. But this might not always work, * since other metavars might also need to be resolved. *) -let applyHead env (type r) (evd : r Sigma.t) n c = - let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma = - fun n c cty p evd -> +let applyHead env evd n c = + let rec apprec n c cty evd = if Int.equal n 0 then - Sigma (c, evd, p) + (evd, c) else - let sigma = Sigma.to_evar_map evd in - match EConstr.kind sigma (whd_all env sigma cty) with + match EConstr.kind evd (whd_all env evd cty) with | Prod (_,c1,c2) -> - let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' - | _ -> error "Apply_Head_Then" + let (evd',evar) = + Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + | _ -> user_err Pp.(str "Apply_Head_Then") in - apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd + apprec n c (Typing.unsafe_type_of env evd c) evd let is_mimick_head sigma ts f = match EConstr.kind sigma f with @@ -1416,9 +1412,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = and mimick_undefined_evar evd flags hdc nargs sp = let ev = Evd.find_undefined evd sp in let sp_env = Global.env_of_context ev.evar_hyps in - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, evd', _) = applyHead sp_env evd nargs hdc in - let evd' = Sigma.to_evar_map evd' in + let (evd', c) = applyHead sp_env evd nargs hdc in let (evd'',mc,ec) = unify_0 sp_env evd' CUMUL flags (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in @@ -1516,7 +1510,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let iter_fail f a = let n = Array.length a in let rec ffail i = - if Int.equal i n then error "iter_fail" + if Int.equal i n then user_err Pp.(str "iter_fail") else try f a.(i) with ex when precatchable_exception ex -> ffail (i+1) @@ -1534,10 +1528,9 @@ let indirectly_dependent sigma c d decls = List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = - let current_sigma = Sigma.to_evar_map current_sigma in let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - Sigma.Unsafe.of_pair (EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))), sigma) + (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1684,7 +1677,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in let res = match out test with | None -> None - | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma)) + | Some (sigma, c) -> Some (sigma,c) in (id,sign,depdecls,lastlhyp,ccl,res) with @@ -1711,10 +1704,9 @@ type abstraction_request = type 'r abstraction_result = Names.Id.t * named_context_val * named_declaration list * Names.Id.t option * - types * (constr, 'r) Sigma.sigma option + types * (evar_map * constr) option let make_abstraction env evd ccl abs = - let evd = Sigma.to_evar_map evd in match abs with | AbstractPattern (from_prefix,check,name,c,occs,check_occs) -> make_abstraction_core name @@ -1754,8 +1746,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> - bestexn := Some ex; error "Unsat") - else error "Bound 1" + bestexn := Some ex; user_err Pp.(str "Unsat")) + else user_err Pp.(str "Bound 1") with ex when precatchable_exception ex -> (match EConstr.kind evd cl with | App (f,args) -> @@ -1804,7 +1796,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> error "Match_subterm")) + | _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1820,7 +1812,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let (evd,c as a) = a () in if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b in - let fail str _ = error str in + let fail str _ = user_err (Pp.str str) in let bind f g a = let a1 = try f a with ex @@ -1956,7 +1948,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = | _, Meta p2 -> (* Find the predicate *) secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) - | _ -> error "w_unify2" + | _ -> user_err Pp.(str "w_unify2") (* The unique unification algorithm works like this: If the pattern is flexible, and the goal has a lambda-abstraction at the head, then diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 8d7e3521d6..0d90ab1584 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -76,14 +76,14 @@ type abstraction_request = | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> 'r Sigma.t -> (evar_map * constr) -> (constr, 'r) Sigma.sigma + env -> evar_map -> (evar_map * constr) -> evar_map * constr type 'r abstraction_result = Names.Id.t * named_context_val * named_declaration list * Names.Id.t option * - types * (constr, 'r) Sigma.sigma option + types * (evar_map * constr) option -val make_abstraction : env -> 'r Sigma.t -> constr -> +val make_abstraction : env -> evar_map -> constr -> abstraction_request -> 'r abstraction_result val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 74998349be..b08666483e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -355,7 +355,7 @@ and nf_cofix env sigma cf = let cbv_vm env sigma c t = if Termops.occur_meta_or_existential sigma c then - CErrors.error "vm_compute does not support existential variables."; + CErrors.user_err Pp.(str "vm_compute does not support existential variables."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in |