diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 512 |
1 files changed, 306 insertions, 206 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ac0104d9..4b6d10c6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -22,13 +22,12 @@ open Pp -open Errors +open CErrors open Util open Names open Evd open Term open Vars -open Context open Termops open Reductionops open Environ @@ -37,17 +36,20 @@ open Typeops open Globnames open Nameops open Evarutil +open Evardefine open Pretype_errors open Glob_term open Glob_ops open Evarconv open Pattern open Misctypes +open Sigma.Notations +open Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; @@ -56,6 +58,8 @@ type ltac_var_map = { } type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } (************************************************************************) (* This concerns Cases *) @@ -64,6 +68,61 @@ open Inductiveops (************************************************************************) +module ExtraEnv = +struct + +type t = { + env : Environ.env; + extra : Evarutil.ext_named_context Lazy.t; + (** Delay the computation of the evar extended environment *) +} + +let get_extra env = + let open Context.Named.Declaration in + let ids = List.map get_id (named_context env) in + let avoid = List.fold_right Id.Set.add ids Id.Set.empty in + Context.Rel.fold_outside push_rel_decl_to_named_context + (Environ.rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + +let make_env env = { env = env; extra = lazy (get_extra env) } +let rel_context env = rel_context env.env + +let push_rel d env = { + env = push_rel d env.env; + extra = lazy (push_rel_decl_to_named_context d (Lazy.force env.extra)); +} + +let pop_rel_context n env = make_env (pop_rel_context n env.env) + +let push_rel_context ctx env = { + env = push_rel_context ctx env.env; + extra = lazy (List.fold_right push_rel_decl_to_named_context ctx (Lazy.force env.extra)); +} + +let lookup_named id env = lookup_named id env.env + +let e_new_evar env evdref ?src ?naming typ = + let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in + let open Context.Named.Declaration in + let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) in + let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in + let (subst, vsubst, _, nc) = Lazy.force env.extra in + 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; + e + +let push_rec_types (lna,typarray,_) env = + let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt + +end + +open ExtraEnv + (* An auxiliary function for searching for fixpoint guard indexes *) exception Found of int array @@ -77,7 +136,7 @@ let search_guard loc env possible_indexes fixdefs = let fix = ((indexes, 0),fixdefs) in (try check_fix env fix with reraise -> - let (e, info) = Errors.push reraise in + let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in iraise (e, info)); indexes @@ -87,18 +146,23 @@ let search_guard loc env possible_indexes fixdefs = List.iter (fun l -> let indexes = Array.of_list l in - let fix = ((indexes, 0),fixdefs) in - try check_fix env fix; raise (Found indexes) + let fix = ((indexes, 0),fixdefs) in + (* spiwack: We search for a unspecified structural + argument under the assumption that we need to check the + guardedness condition (otherwise the first inductive argument + will be chosen). A more robust solution may be to raise an + error when totality is assumed but the strutural argument is + not specified. *) + try + let flags = { (typing_flags env) with Declarations.check_guarded = true } in + let env = Environ.set_typing_flags flags env in + check_fix env fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in user_err_loc (loc,"search_guard", Pp.str errmsg) with Found indexes -> indexes) -(* To embed constr in glob_constr *) -let ((constr_in : constr -> Dyn.t), - (constr_out : Dyn.t -> constr)) = Dyn.create "constr" - (* To force universe name declaration before use *) let strict_universe_declarations = ref true @@ -134,24 +198,24 @@ let interp_universe_level_name evd (loc,s) = let level = Univ.Level.make dp num in let evd = try Evd.add_global_univ evd level - with Univ.AlreadyDeclared -> evd + with UGraph.AlreadyDeclared -> evd in evd, level else try - let id = - try Id.of_string s with _ -> raise Not_found in - evd, Idmap.find id names + let level = Evd.universe_of_name evd s in + evd, level with Not_found -> - try let level = Evd.universe_of_name evd s in - evd, level + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, snd (Idmap.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~name:s univ_rigid evd + new_univ_level_variable ~loc ~name:s univ_rigid evd else user_err_loc (loc, "interp_universe_level_name", Pp.(str "Undeclared universe: " ++ str s)) -let interp_universe evd = function - | [] -> let evd, l = new_univ_level_variable univ_rigid evd in +let interp_universe ?loc evd = function + | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> List.fold_left (fun (evd, u) l -> @@ -159,15 +223,15 @@ let interp_universe evd = function (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l -let interp_universe_level evd = function - | None -> new_univ_level_variable univ_rigid evd +let interp_universe_level loc evd = function + | None -> new_univ_level_variable ~loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name evd (loc,s) -let interp_sort evd = function +let interp_sort ?loc evd = function | GProp -> evd, Prop Null | GSet -> evd, Prop Pos | GType n -> - let evd, u = interp_universe evd n in + let evd, u = interp_universe ?loc evd n in evd, Type u let interp_elimination_sort = function @@ -175,23 +239,31 @@ let interp_elimination_sort = function | GSet -> InSet | GType _ -> InType +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; - use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + solve_unification_constraints : bool; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } -let frozen_holes (sigma, sigma') = - let fold evk _ accu = Evar.Set.add evk accu in - Evd.fold_undefined fold sigma Evar.Set.empty - -let pending_holes (sigma, sigma') = - let fold evk _ accu = - if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu - in - Evd.fold_undefined fold sigma' Evar.Set.empty +(* Compute the set of still-undefined initial evars up to restriction + (e.g. clearing) and the set of yet-unsolved evars freshly created + in the extension [sigma'] of [sigma] (excluding the restrictions of + the undefined evars of [sigma] to be freshly created evars of + [sigma']). Otherwise said, we partition the undefined evars of + [sigma'] into those already in [sigma] or deriving from an evar in + [sigma] by restriction, and the evars properly created in [sigma'] *) + +let frozen_and_pending_holes (sigma, sigma') = + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen,pending) let apply_typeclasses env evdref frozen fail_evar = let filter_frozen evk = Evar.Set.mem evk frozen in @@ -209,7 +281,7 @@ let apply_inference_hook hook evdref pending = if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let c = hook sigma evk in + let sigma, c = hook sigma evk in Evd.define evk c sigma with Exit -> sigma @@ -218,10 +290,10 @@ let apply_inference_hook hook evdref pending = let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) - try evdref := consider_remaining_unif_problems + try evdref := solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env !evdref - with e when Errors.noncritical e -> - let e = Errors.push e in if fail_evar then iraise e + with e when CErrors.noncritical e -> + let e = CErrors.push e in if fail_evar then iraise e let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) @@ -237,6 +309,23 @@ let check_extra_evars_are_solved env current_sigma pending = | _ -> error_unsolvable_implicit loc env current_sigma evk None) pending +(* [check_evars] fails if some unresolved evar remains *) + +let check_evars env initial_sigma sigma c = + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,_ as ev) -> + (match existential_opt_value sigma ev with + | Some c -> proc_rec c + | None -> + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk sigma in + match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None) + | _ -> Constr.iter proc_rec c + in proc_rec c + let check_evars_are_solved env current_sigma frozen pending = check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; @@ -245,19 +334,17 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then apply_inference_hook (Option.get flags.use_hook env) evdref pending; - if flags.use_unif_heuristics then apply_heuristics env evdref false; + if flags.solve_unification_constraints then apply_heuristics env evdref false; if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref let check_evars_are_solved env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = @@ -268,26 +355,11 @@ let process_inference_flags flags env initial_sigma (sigma,c) = (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *) let allow_anonymous_refs = ref false -(* Utilisé pour inférer le prédicat des Cases *) -(* Semble exagérement fort *) -(* Faudra préférer une unification entre les types de toutes les clauses *) -(* et autoriser des ? à rester dans le résultat de l'unification *) - -let evar_type_fixpoint loc env evdref lna lar vdefj = - let lt = Array.length vdefj in - if Int.equal (Array.length lar) lt then - for i = 0 to lt-1 do - if not (e_cumul env evdref (vdefj.(i)).uj_type - (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env !evdref - i lna vdefj lar - done - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () @@ -321,11 +393,12 @@ let ltac_interp_name_env k0 lvar env = specification of pretype which accepts to start with a non empty rel_context) *) (* tail is the part of the env enriched by pretyping *) - let n = rel_context_length (rel_context env) - k0 in + let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in - let env = pop_rel_context n env in - let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in - push_rel_context ctxt env + let open Context.Rel.Declaration in + let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env + else push_rel_context ctxt' (pop_rel_context n env) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -336,7 +409,7 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env sigma c + try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c with Retyping.RetypeError _ -> errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ @@ -372,13 +445,15 @@ let pretype_id pretype k0 loc env evdref lvar id = with Not_found -> (* Check if [id] is a ltac variable not bound to a term *) (* and build a nice error message *) - if Id.Map.mem id lvar.ltac_genargs then + if Id.Map.mem id lvar.ltac_genargs then begin + let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in user_err_loc (loc,"", - str "Variable " ++ pr_id id ++ str " should be bound to a term."); + str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + bound to a " ++ Geninterp.Val.pr typ ++ str ".") + end; (* Check if [id] is a section or goal variable *) try - let (_,_,typ) = lookup_named id env in - { uj_val = mkVar id; uj_type = typ } + { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found_loc loc id @@ -389,11 +464,11 @@ let evar_kind_of_term sigma c = (*************************************************************************) (* Main pretyping function *) -let interp_universe_level_name evd l = +let interp_universe_level_name loc evd l = match l with | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set - | GType s -> interp_universe_level evd s + | GType s -> interp_universe_level loc evd s let pretype_global loc rigid env evd gr us = let evd, instance = @@ -408,7 +483,7 @@ let pretype_global loc rigid env evd gr us = str "Universe instance should have length " ++ int len) else let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_universe_level_name evd l in + let evd, l = interp_universe_level_name loc evd l in (evd, l :: univs)) (evd, []) l in if List.exists (fun l -> Univ.Level.is_prop l) l' then @@ -417,14 +492,13 @@ let pretype_global loc rigid env evd gr us = str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in - Evd.fresh_global ~rigid ?names:instance env evd gr + Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr let pretype_ref loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) - (try let (_,_,ty) = lookup_named id env in - make_judge (mkVar id) ty + (try make_judge (mkVar id) (get_type (lookup_named id env)) with Not_found -> (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal @@ -433,34 +507,29 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty -let judge_of_Type evd s = - let evd, s = interp_universe evd s in +let judge_of_Type loc evd s = + let evd, s = interp_universe ~loc evd s in let judge = { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in evd, judge -let pretype_sort evdref = function +let pretype_sort loc evdref = function | GProp -> judge_of_prop | GSet -> judge_of_set - | GType s -> evd_comb1 judge_of_Type evdref s + | GType s -> evd_comb1 (judge_of_Type loc) evdref s let new_type_evar env evdref loc = - let e, s = - evd_comb0 (fun evd -> Evarutil.new_type_evar env evd - univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref - in e - -let get_projection env cst = - let cb = lookup_constant cst env in - match cb.Declarations.const_proj with - | Some {Declarations.proj_ind = mind; proj_npars = n; - proj_arg = m; proj_type = ty} -> - (cst,mind,n,m,ty) - | None -> raise Not_found + let sigma = Sigma.Unsafe.of_evar_map !evdref in + let Sigma ((e, _), sigma, _) = + Evarutil.new_type_evar env.ExtraEnv.env sigma + univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) + in + evdref := Sigma.to_evar_map sigma; + e let (f_genarg_interp, genarg_interp_hook) = Hook.make () @@ -468,16 +537,11 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make () (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) -let is_GHole = function - | GHole _ -> true - | _ -> false - -let evars = ref Id.Map.empty - -let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t = +let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in + let open Context.Rel.Declaration in match t with | GRef (loc,ref,u) -> inh_conv_coerce_to_tycon loc env evdref @@ -499,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in - let j = (Retyping.get_judgment_of env !evdref c) in + let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon loc env evdref j tycon | GPatVar (loc,(someta,n)) -> @@ -528,7 +592,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env !evdref ist arg in + let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } @@ -537,16 +601,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = (na,None,ty'.utj_val) in - let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl + let dcl = LocalAssum (na, ty'.utj_val) in + let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in - let dcl = (na,Some bd'.uj_val,ty'.utj_val) in - let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in - type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in - let ctxtv = Array.map (type_bl env empty_rel_context) bl in + let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in + type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in + let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = Array.map2 (fun e ar -> @@ -562,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixi = match fixkind with | GFix (vn,i) -> i | GCoFix i -> i - in e_conv env evdref ftys.(fixi) t + in e_conv env.ExtraEnv.env evdref ftys.(fixi) t | None -> true in (* Note: bodies are not used by push_rec_types, so [||] is safe *) @@ -573,14 +637,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ (* we lift nbfix times the type in tycon, because of * the nbfix variables pushed to newenv *) let (ctxt,ty) = - decompose_prod_n_assum (rel_context_length ctxt) + decompose_prod_n_assum (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - evar_type_fixpoint loc env evdref names ftys vdefj; + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with @@ -599,13 +663,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ vn) in let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in + let indexes = + search_guard + loc env.ExtraEnv.env possible_indexes fixdecls + in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env.ExtraEnv.env cofix with reraise -> - let (e, info) = Errors.push reraise in + let (e, info) = CErrors.push reraise in let info = Loc.add_loc info loc in iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) @@ -613,7 +680,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ inh_conv_coerce_to_tycon loc env evdref fixj tycon | GSort (loc,s) -> - let j = pretype_sort evdref s in + let j = pretype_sort loc evdref s in inh_conv_coerce_to_tycon loc env evdref j tycon | GApp (loc,f,args) -> @@ -633,7 +700,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if Int.equal npars 0 then [] else try - let IndType (indf, args) = find_rectype env !evdref ty in + let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in let ((ind',u'),pars) = dest_ind_family indf in if eq_ind ind ind' then pars else (* Let the usual code throw an error *) [] @@ -642,9 +709,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ in let app_f = match kind_of_term fj.uj_val with - | Const (p, u) when Environ.is_projection p env -> + | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in - let pb = Environ.lookup_projection p env in + let pb = Environ.lookup_projection p env.ExtraEnv.env in let npars = pb.Declarations.proj_npars in fun n -> if n == npars + 1 then fun _ v -> mkProj (p, v) @@ -655,8 +722,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in - let resty = whd_betadeltaiota env !evdref resj.uj_type in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> let tycon = Some c1 in @@ -665,7 +732,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match candargs with | [] -> [], j_val hj | arg :: args -> - if e_conv env evdref (j_val hj) arg then + if e_conv env.ExtraEnv.env evdref (j_val hj) arg then args, nf_evar !evdref (j_val hj) else [], j_val hj in @@ -676,7 +743,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env !evdref + (Loc.merge floc argloc) env.ExtraEnv.env !evdref resj [hj] in let resj = apply_rec env 1 fj candargs args in @@ -684,13 +751,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env f then + if is_template_polymorphic env.ExtraEnv.env f then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in - let t = Retyping.get_type_of env !evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in + let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj | _ -> resj @@ -703,20 +770,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = (name,None,j.utj_val) in + let var = LocalAssum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - let resj = judge_of_abstraction env (orelse_name name name') j j' in + let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in inh_conv_coerce_to_tycon loc env evdref resj tycon | GProd(loc,name,bk,c1,c2) -> @@ -729,16 +796,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = (name,j.utj_val) in - let env' = push_rel_assum var env in + let var = LocalAssum (name, j.utj_val) in + let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = try - judge_of_product env name j j' + judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> - let (e, info) = Errors.push e in + let (e, info) = CErrors.push e in let info = Loc.add_loc info loc in iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -752,12 +819,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes - ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = (name,Some j.uj_val,t) in + let var = LocalDef (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in @@ -767,12 +834,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in - let cstrs = get_constructors env indf in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ str " with one constructor."); @@ -781,18 +848,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = - match get_projections env indf with - | None -> List.map2 (fun na (_,c,t) -> (na,c,t)) - (List.rev nal) cs.cs_args, false + match get_projections env.ExtraEnv.env indf with + | None -> + List.map2 set_name (List.rev nal) cs.cs_args, false | Some ps -> let rec aux n k names l = match names, l with - | na :: names, ((_, None, t) :: l) -> + | na :: names, (LocalAssum (_,t) :: l) -> let proj = Projection.make ps.(cs.cs_nargs - k) true in - (na, Some (lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val))), t) + LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l - | na :: names, ((_, c, t) :: l) -> - (na, c, t) :: aux (n+1) k names l + | na :: names, (decl :: l) -> + set_name na decl :: aux (n+1) k names l | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in @@ -800,38 +867,38 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in let nal = List.rev nal in - let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in + let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info env (fst ind) LetStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in (* Make dependencies from arity signature impossible *) let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + List.map (set_name Anonymous) arsgn else arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let nar = List.length arsgn in (match po with | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in let ccl = nf_evar !evdref pj.utj_val in - let psign = make_arity_signature env true indf in (* with names *) + let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = (Array.to_list cs.cs_concl_realargs) @[build_dependent_constructor cs] in let lp = lift cs.cs_nargs p in - let fty = hnf_lam_applist env !evdref lp inst in + let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -844,37 +911,37 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env !evdref + error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env !evdref cj.uj_type + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env !evdref cj in - let cstrs = get_constructors env indf in + error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then user_err_loc (loc,"", str "If is only for inductive types with two constructors."); let arsgn = - let arsgn,_ = get_arity env indf in + let arsgn,_ = get_arity env.ExtraEnv.env indf in if not !allow_anonymous_refs then (* Make dependencies from arity signature impossible *) - List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn + List.map (set_name Anonymous) arsgn else arsgn in let nar = List.length arsgn in - let psign = (na,None,build_dependent_inductive env indf)::arsgn in + let psign = LocalAssum (na, build_dependent_inductive env.ExtraEnv.env indf) :: arsgn in let pred,p = match po with | Some p -> let env_p = push_rel_context psign env in @@ -894,19 +961,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let pred = nf_evar !evdref pred in let p = nf_evar !evdref p in let f cs b = - let n = rel_context_length cs.cs_args in + let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist (pi, [build_dependent_constructor cs]) in let csgn = if not !allow_anonymous_refs then - List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args + List.map (set_name Anonymous) cs.cs_args else - List.map - (fun (n, b, t) -> - match n with - Name _ -> (n, b, t) - | Anonymous -> (Name Namegen.default_non_dependent_ident, b, t)) - cs.cs_args + List.map (map_name (function Name _ as n -> n + | Anonymous -> Name Namegen.default_non_dependent_ident)) + cs.cs_args in let env_c = push_rel_context csgn env in let bj = pretype (mk_tycon pi) env_c evdref lvar b in @@ -915,9 +979,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info env (fst ind) IfStyle in + let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in @@ -925,51 +989,55 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | GCases (loc,sty,po,tml,eqns) -> Cases.compile_cases loc sty - ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref) - tycon env (* loc *) (po,tml,eqns) + ((fun vtyc env evdref -> pretype vtyc (make_env env) evdref lvar),evdref) + tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) | GCast (loc,c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with + let tval = evd_comb1 (Evarsolve.refresh_universes + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) + evdref tj.utj_val in + let tval = nf_evar !evdref tval in + let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then - let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin - let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in + if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env !evdref cj tval - (ConversionFailed (env,cty,tval)) + error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c + pretype (mk_tycon tval) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = - let f (id,_,t) (subst,update) = - let t = replace_vars subst t in + let f decl (subst,update) = + let id = get_id decl in + let t = replace_vars subst (get_type decl) in let c, update = try let c = List.assoc id update in @@ -978,11 +1046,11 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in - if is_conv env !evdref t t' then mkRel n, update else raise Not_found + if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found with Not_found -> try - let (_,_,t') = lookup_named id env in - if is_conv env !evdref t t' then mkVar id, update else raise Not_found + let t' = lookup_named id env |> get_type in + if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> user_err_loc (loc,"",str "Cannot interpret " ++ pr_existential_key !evdref evk ++ @@ -993,17 +1061,17 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = Array.map_of_list snd subst (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) -and pretype_type k0 resolve_tc valcon env evdref lvar = function +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = let sigma = !evdref in - let t = Retyping.get_type_of env sigma v in - match kind_of_term (whd_betadeltaiota env sigma t) with + let t = Retyping.get_type_of env.ExtraEnv.env sigma v in + match kind_of_term (whd_all env.ExtraEnv.env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort env) evdref ev + evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; @@ -1016,18 +1084,19 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> - if e_cumul env evdref v tj.utj_val then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type_loc - (loc_of_glob_constr c) env !evdref tj.utj_val v + (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = + let env = make_env env in let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let c' = match kind with | WithoutTypeConstraint -> (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val @@ -1036,18 +1105,18 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = fail; expand_evars = true } let no_classes_no_fail_inference_flags = { use_typeclasses = false; - use_unif_heuristics = true; + solve_unification_constraints = true; use_hook = None; fail_evar = false; expand_evars = true } @@ -1068,19 +1137,21 @@ let on_judgment f j = {uj_val = c; uj_type = t} let understand_judgment env sigma c = + let env = make_env env in let evdref = ref sigma in - let k0 = rel_context_length (rel_context env) in + let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in let j = on_judgment (fun c -> - let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in + let evd, c = process_inference_flags all_and_fail_flags env.ExtraEnv.env sigma (!evdref,c) in evdref := evd; c) j in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - let k0 = rel_context_length (rel_context env) in + let env = make_env env in + let k0 = Context.Rel.length (rel_context env) in let j = pretype k0 true empty_tycon env evdref empty_lvar c in on_judgment (fun c -> - let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in + let (evd,c) = process_inference_flags all_no_fail_flags env.ExtraEnv.env Evd.empty (!evdref,c) in evdref := evd; c) j let ise_pretype_gen_ctx flags env sigma lvar kind c = @@ -1106,3 +1177,32 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W let understand_ltac flags env sigma lvar kind c = ise_pretype_gen flags env sigma lvar kind c + +let constr_flags = { + use_typeclasses = true; + solve_unification_constraints = true; + use_hook = None; + fail_evar = true; + expand_evars = true } + +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = constr_flags) + ?(expected_type = WithoutTypeConstraint) ist c = + { delayed = begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + 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 } + +let pretype k0 resolve_tc typcon env evdref lvar t = + pretype k0 resolve_tc typcon (make_env env) evdref lvar t + +let pretype_type k0 resolve_tc valcon env evdref lvar t = + pretype_type k0 resolve_tc valcon (make_env env) evdref lvar t |