diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 111 |
1 files changed, 88 insertions, 23 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1605ef7cf..908e59227 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -21,6 +21,27 @@ open Evd open Reductionops open Pretype_errors +let evd_comb0 f evdref = + let (evd',x) = f !evdref in + evdref := evd'; + x + +let evd_comb1 f evdref x = + let (evd',y) = f !evdref x in + evdref := evd'; + y + +let evd_comb2 f evdref x y = + let (evd',z) = f !evdref x y in + evdref := evd'; + z + +let e_new_global evdref x = + evd_comb1 (Evd.fresh_global (Global.env())) evdref x + +let new_global evd x = + Evd.fresh_global (Global.env()) evd x + (****************************************************) (* Expanding/testing/exposing existential variables *) (****************************************************) @@ -37,6 +58,8 @@ let rec flush_and_check_evars sigma c = | Some c -> flush_and_check_evars sigma c) | _ -> map_constr (flush_and_check_evars sigma) c +(* let nf_evar_key = Profile.declare_profile "nf_evar" *) +(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *) let nf_evar = Reductionops.nf_evar let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; @@ -60,24 +83,38 @@ let env_nf_betaiotaevar sigma env = (fun d e -> push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env +let nf_evars_universes evm = + Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) + (Evd.universe_subst evm) + +let nf_evars_and_universes evm = + let evm = Evd.nf_constraints evm in + evm, nf_evars_universes evm + +let e_nf_evars_and_universes evdref = + evdref := Evd.nf_constraints !evdref; + nf_evars_universes !evdref, Evd.universe_subst !evdref + +let nf_evar_map_universes evm = + let evm = Evd.nf_constraints evm in + let subst = Evd.universe_subst evm in + if Univ.LMap.is_empty subst then evm, nf_evar evm + else + let f = nf_evars_universes evm in + Evd.raw_map (fun _ -> map_evar_info f) evm, f + let nf_named_context_evar sigma ctx = - Context.map_named_context (Reductionops.nf_evar sigma) ctx + Context.map_named_context (nf_evar sigma) ctx let nf_rel_context_evar sigma ctx = - Context.map_rel_context (Reductionops.nf_evar sigma) ctx + Context.map_rel_context (nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) -let nf_evar_info evc info = - { info with - evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; - evar_body = match info.evar_body with - | Evar_empty -> Evar_empty - | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } +let nf_evar_info evc info = map_evar_info (nf_evar evc) info let nf_evar_map evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm @@ -89,7 +126,7 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) -let has_undefined_evars_or_sorts evd t = +let has_undefined_evars or_sorts evd t = let rec has_ev t = match kind_of_term t with | Evar (ev,args) -> @@ -98,13 +135,16 @@ let has_undefined_evars_or_sorts evd t = has_ev c; Array.iter has_ev args | Evar_empty -> raise NotInstantiatedEvar) - | Sort s when is_sort_variable evd s -> raise Not_found + | Sort (Type _) (*FIXME could be finer, excluding Prop and Set universes *) when or_sorts -> + raise Not_found + | Ind (_,l) | Const (_,l) | Construct (_,l) + when l <> Univ.Instance.empty && or_sorts -> raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true let is_ground_term evd t = - not (has_undefined_evars_or_sorts evd t) + not (has_undefined_evars true evd t) let is_ground_env evd env = let is_ground_decl = function @@ -333,9 +373,21 @@ let new_evar evd env ?src ?filter ?candidates typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates instance -let new_type_evar ?src ?filter evd env = - let evd', s = new_sort_variable evd in - new_evar evd' env ?src ?filter (mkSort s) +let new_type_evar ?src ?filter rigid evd env = + let evd', s = new_sort_variable rigid evd in + let evd', e = new_evar evd' env ?src ?filter (mkSort s) in + evd', (e, s) + + (* The same using side-effect *) +let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty = + let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in + evdref := evd'; + ev + +let e_new_type_evar evdref ?src ?filter rigid env = + let evd', c = new_type_evar ?src ?filter rigid !evdref env in + evdref := evd'; + c (* The same using side-effect *) let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ty = @@ -470,7 +522,6 @@ let clear_hyps_in_evi evdref hyps concl ids = in (nhyps,nconcl) - (** The following functions return the set of evars immediately contained in the object, including defined evars *) @@ -597,6 +648,7 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c + (****************************************) (* Operations on value/type constraints *) (****************************************) @@ -639,15 +691,25 @@ let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in + let s = destSort evi.evar_concl in + let evd1,(dom,u1) = new_type_evar univ_flexible_alg evd evenv ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - new_type_evar evd1 newenv ~src ~filter in + if is_prop_sort s then + (* Impredicative product, conclusion must fall in [Prop]. *) + new_evar evd1 newenv evi.evar_concl ~src ~filter + else + let evd3, (rng, srng) = + new_type_evar univ_flexible_alg evd1 newenv ~src ~filter in + let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in + let evd3 = Evd.set_leq_sort evd3 (Type prods) s in + evd3, rng + in let prod = mkProd (Name id, dom, subst_var id rng) in let evd3 = Evd.define evk prod evd2 in - evd3,prod + evd3,prod (* Refine an applied evar to a product and returns its instantiation *) @@ -707,15 +769,18 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function (* Refining an evar to a sort *) let define_evar_as_sort evd (ev,args) = - let evd, s = new_sort_variable evd in - Evd.define ev (mkSort s) evd, s + let evd, u = new_univ_variable univ_rigid evd in + let evi = Evd.find_undefined evd ev in + let s = Type u in + let evd' = Evd.define ev (mkSort s) evd in + Evd.set_leq_sort evd' (Type (Univ.super u)) (destSort evi.evar_concl), s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) let judge_of_new_Type evd = - let evd', s = new_univ_variable evd in - evd', Typeops.judge_of_type s + let evd', s = new_univ_variable univ_rigid evd in + evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type |