diff options
Diffstat (limited to 'pretyping')
39 files changed, 266 insertions, 4634 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3d6fa38d0..2cbf3a265 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Vars -open Context open Termops open Namegen open Declarations @@ -131,7 +130,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool*(Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * rel_declaration + | Abstract of int * Context.Rel.Declaration.t type tomatch_stack = tomatch_status list @@ -602,7 +601,7 @@ let relocate_index_tomatch n1 n2 = NonDepAlias :: genrec depth rest | Abstract (i,d) :: rest -> let i = relocate_rel n1 n2 depth i in - Abstract (i,map_rel_declaration (relocate_index n1 n2 depth) d) + Abstract (i, Context.Rel.Declaration.map (relocate_index n1 n2 depth) d) :: genrec (depth+1) rest in genrec 0 @@ -635,7 +634,7 @@ let replace_tomatch n c = | NonDepAlias :: rest -> NonDepAlias :: replrec depth rest | Abstract (i,d) :: rest -> - Abstract (i,map_rel_declaration (replace_term n c depth) d) + Abstract (i, Context.Rel.Declaration.map (replace_term n c depth) d) :: replrec (depth+1) rest in replrec 0 @@ -660,7 +659,7 @@ let rec liftn_tomatch_stack n depth = function NonDepAlias :: liftn_tomatch_stack n depth rest | Abstract (i,d)::rest -> let i = if i<depth then i else i+n in - Abstract (i,map_rel_declaration (liftn n depth) d) + Abstract (i, Context.Rel.Declaration.map (liftn n depth) d) ::(liftn_tomatch_stack n (depth+1) rest) let lift_tomatch_stack n = liftn_tomatch_stack n 1 @@ -837,10 +836,10 @@ let regeneralize_index_predicate n = map_predicate (relocate_index n 1) 0 let substnl_predicate sigma = map_predicate (substnl sigma) (* This is parallel bindings *) -let subst_predicate (args,copt) ccl tms = +let subst_predicate (subst,copt) ccl tms = let sigma = match copt with - | None -> List.rev args - | Some c -> c::(List.rev args) in + | None -> subst + | Some c -> c::subst in substnl_predicate sigma 0 ccl tms let specialize_predicate_var (cur,typ,dep) tms ccl = @@ -921,7 +920,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl = let tms = List.fold_right2 (fun par arg tomatch -> match kind_of_term par with | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch - | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign) + | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list 0 sign) (lift_tomatch_stack n tms) in (* Pred is already dependent in the current term to match (if *) (* (na<>Anonymous) and its realargs; we just need to adjust it to *) @@ -1018,7 +1017,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl = (* We prepare the substitution of X and x:I(X) *) let realargsi = if not (Int.equal nrealargs 0) then - adjust_subst_to_rel_context arsign (Array.to_list cs.cs_concl_realargs) + subst_of_rel_context_instance arsign (Array.to_list cs.cs_concl_realargs) else [] in let copti = match depna with @@ -1118,7 +1117,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with | [], _ -> brs,tomatch,pred,[] | n::deps, Abstract (i,d) :: tomatch -> - let d = map_rel_declaration (nf_evar evd) d in + let d = Context.Rel.Declaration.map (nf_evar evd) d in let is_d = match d with (_, None, _) -> false | _ -> true in if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck && Array.exists (is_dependent_branch k) brs then @@ -1187,7 +1186,7 @@ let group_equations pb ind current cstrs mat = let rec generalize_problem names pb = function | [] -> pb, [] | i::l -> - let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in + let (na,b,t as d) = Context.Rel.Declaration.map (lift i) (Environ.lookup_rel i pb.env) in let pb',deps = generalize_problem names pb l in begin match (na, b) with | Anonymous, Some _ -> pb', deps @@ -1230,7 +1229,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* We adjust the terms to match in the context they will be once the *) (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *) let typs' = - List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in + List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 typs in let extenv = push_rel_context typs pb.env in @@ -1560,8 +1559,8 @@ let matx_of_eqns env eqns = *) let adjust_to_extended_env_and_remove_deps env extenv subst t = - let n = rel_context_length (rel_context env) in - let n' = rel_context_length (rel_context extenv) in + let n = Context.Rel.length (rel_context env) in + let n' = Context.Rel.length (rel_context extenv) in (* We first remove the bindings that are dependently typed (they are difficult to manage and it is not sure these are so useful in practice); Notes: @@ -1673,8 +1672,8 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = | None -> (* This is the situation we are building a return predicate and we are in an impossible branch *) - let n = rel_context_length (rel_context env) in - let n' = rel_context_length (rel_context tycon_env) in + let n = Context.Rel.length (rel_context env) in + let n' = Context.Rel.length (rel_context tycon_env) in let impossible_case_type, u = e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in (lift (n'-n) impossible_case_type, mkSort u) @@ -1744,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t = let n = List.length sign in let decls = - List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in + List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 sign in let pb_env = push_rel_context sign env in let decls = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ab00aa165..257d1e578 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Inductiveops @@ -45,11 +44,11 @@ val compile_cases : val constr_of_pat : Environ.env -> Evd.evar_map ref -> - rel_declaration list -> + Context.Rel.Declaration.t list -> Glob_term.cases_pattern -> Names.Id.t list -> Glob_term.cases_pattern * - (rel_declaration list * Term.constr * + (Context.Rel.Declaration.t list * Term.constr * (Term.types * Term.constr list) * Glob_term.cases_pattern) * Names.Id.t list @@ -83,7 +82,7 @@ type tomatch_status = | Pushed of (bool*((constr * tomatch_type) * int list * Name.t)) | Alias of (bool * (Name.t * constr * (constr * types))) | NonDepAlias - | Abstract of int * rel_declaration + | Abstract of int * Context.Rel.Declaration.t type tomatch_stack = tomatch_status list @@ -117,7 +116,7 @@ val prepare_predicate : Loc.t -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> - Context.rel_context list -> + Context.Rel.t list -> Constr.constr option -> 'a option -> (Evd.evar_map * Names.name list * Term.constr) list diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ee3c43d8d..69c1dfb47 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -17,7 +17,6 @@ open Termops open Reductionops open Term open Vars -open Context open Pattern open Patternops open Misctypes @@ -269,8 +268,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in - let n = rel_context_length ctx_b2 in - let n' = rel_context_length ctx_b2' in + let n = Context.Rel.length ctx_b2 in + let n' = Context.Rel.length ctx_b2' in if noccur_between 1 n b2 && noccur_between 1 n' b2' then let f l (na,_,t) = (Anonymous,na,t)::l in let ctx_br = List.fold_left f ctx ctx_b2 in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c3877c56e..c8ecf91d3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Vars -open Context open Inductiveops open Environ open Glob_term @@ -199,7 +198,7 @@ let computable p k = engendrera un prédicat non dépendant) *) let sign,ccl = decompose_lam_assum p in - Int.equal (rel_context_length sign) (k + 1) + Int.equal (Context.Rel.length sign) (k + 1) && noccur_between 1 (k+1) ccl @@ -315,7 +314,7 @@ let is_nondep_branch c l = try (* FIXME: do better using tags from l *) let sign,ccl = decompose_lam_n_decls (List.length l) c in - noccur_between 1 (rel_context_length sign) ccl + noccur_between 1 (Context.Rel.length sign) ccl with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *) false @@ -673,7 +672,13 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = match bk with | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r) | BLambda -> GLambda (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r) - | BLetIn -> GLetIn (dl, na',detype (lax,false) avoid env sigma (Option.get body), r) + | BLetIn -> + let c = detype (lax,false) avoid env sigma (Option.get body) in + (* Heuristic: we display the type if in Prop *) + let s = Retyping.get_sort_family_of (snd env) sigma ty in + let c = if s != InProp then c else + GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in + GLetIn (dl, na', c, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 838588dc4..c51cb0f44 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Glob_term open Termops @@ -46,7 +45,7 @@ val detype_case : val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list + evar_map -> Context.Rel.t -> glob_decl list val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 637a9e50e..99e51330e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -22,6 +22,7 @@ open Evarsolve open Globnames open Evd open Pretype_errors +open Sigma.Notations type unify_fun = transparent_state -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -830,7 +831,9 @@ 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.ghost,Evar_kinds.InternalHole) in - let (i',ev) = new_evar env i ~src:dloc (substl ks b) 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 (i', ev :: ks, m - 1,test)) (evd,[],List.length bs,fun i -> Success i) bs in @@ -1096,7 +1099,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in + let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 3bf6f3764..0dd0ad2e0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -11,7 +11,6 @@ open Errors open Names open Term open Vars -open Context open Environ open Termops open Evd @@ -501,7 +500,7 @@ let solve_pattern_eqn env l c = match kind_of_term a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> - let d = map_rel_declaration (lift n) (lookup_rel n env) in + let d = Context.Rel.Declaration.map (lift n) (lookup_rel n env) in mkLambda_or_LetIn d c' | Var id -> let d = lookup_named id env in mkNamedLambda_or_LetIn d c' @@ -1007,21 +1006,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let are_canonical_instances args1 args2 env = - let n1 = Array.length args1 in - let n2 = Array.length args2 in - let rec aux n = function - | (id,_,c)::sign - when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) -> - aux (n+1) sign - | [] -> - let rec aux2 n = - Int.equal n n1 || - (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1)) - in aux2 n - | _ -> false in - Int.equal n1 n2 && aux 0 (named_context env) - let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index e23e5a53a..8c210e283 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -12,7 +12,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Namegen open Pre_env @@ -78,12 +77,12 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = let env_nf_evar sigma env = process_rel_context - (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env + (fun d e -> push_rel (Context.Rel.Declaration.map (nf_evar sigma) d) e) env let env_nf_betaiotaevar sigma env = process_rel_context (fun d e -> - push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env + push_rel (Context.Rel.Declaration.map (Reductionops.nf_betaiota sigma) d) e) env let nf_evars_universes evm = Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) @@ -106,10 +105,10 @@ let nf_evar_map_universes evm = Evd.raw_map (fun _ -> map_evar_info f) evm, f let nf_named_context_evar sigma ctx = - Context.map_named_context (nf_evar sigma) ctx + Context.Named.map (nf_evar sigma) ctx let nf_rel_context_evar sigma ctx = - Context.map_rel_context (nf_evar sigma) ctx + Context.Rel.map (nf_evar sigma) ctx let nf_env_evar sigma env = let nc' = nf_named_context_evar sigma (Environ.named_context env) in @@ -239,17 +238,6 @@ let make_pure_subst evi args = | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) -(**********************) -(* Creating new evars *) -(**********************) - -let evar_counter_summary_name = "evar counter" - -(* Generator of existential names *) -let new_untyped_evar = - let evar_ctr = Summary.ref 0 ~name:evar_counter_summary_name in - fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr - (*------------------------------------* * functional operations on evar sets * *------------------------------------*) @@ -314,7 +302,7 @@ let push_rel_context_to_named_context env typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, vsubst, _, env) = - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,c,t) (subst, vsubst, avoid, env) -> let id = (* ppedrot: we want to infer nicer names for the refine tactic, but @@ -354,17 +342,15 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) let restrict_evar evd evk filter candidates = - let evk' = new_untyped_evar () in - let evd = Evd.restrict evk evk' filter ?candidates evd in + let evd, evk' = Evd.restrict evk filter ?candidates evd in Evd.declare_future_goal evk' evd, evk' let new_pure_evar_full evd evi = - let evk = new_untyped_evar () in - let evd = Evd.add evd evk evi in + let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ = +let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = let default_naming = if principal then (* waiting for a more principled approach @@ -374,8 +360,16 @@ let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?nam Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in - let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in + let evi = { + evar_hyps = sign; + evar_concl = typ; + evar_body = Evar_empty; + evar_filter = filter; + evar_source = src; + evar_candidates = candidates; + evar_extra = store; } + in + let (evd, newevk) = Evd.new_evar evd ~naming evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd @@ -390,7 +384,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in let instance = @@ -399,9 +393,14 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let evd = Sigma.to_evar_map evd in + let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in + Sigma.Unsafe.of_pair (c, sigma) + let new_type_evar env evd ?src ?filter ?naming ?principal rigid = let evd', s = new_sort_variable rigid evd in - let evd', e = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in + let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in evd', (e, s) let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = @@ -419,7 +418,7 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = (* The same using side-effect *) let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in + let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in evdref := evd'; ev @@ -723,7 +722,7 @@ let define_pure_evar_as_product evd evk = let filter = Filter.extend 1 (evar_filter evi) in if is_prop_sort s then (* Impredicative product, conclusion must fall in [Prop]. *) - new_evar newenv evd1 concl ~src ~filter + new_evar_unsafe newenv evd1 concl ~src ~filter else let status = univ_flexible_alg in let evd3, (rng, srng) = @@ -770,7 +769,7 @@ let define_pure_evar_as_lambda env evd evk = let newenv = push_named (id, None, dom) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = evar_source evk evd1 in - let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in + let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in let lam = mkLambda (Name id, dom, subst_var id body) in Evd.define evk lam evd2, lam @@ -860,13 +859,14 @@ let kind_of_term_upto sigma t = let eq_constr_univs_test sigma1 sigma2 t u = (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) let open Evd in - let b, c = + let fold cstr sigma = + try Some (add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | UniversesDiffer -> None + in + let ans = Universes.eq_constr_univs_infer_with (fun t -> kind_of_term_upto sigma1 t) (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) t u + (universes sigma2) fold t u sigma2 in - if b then - try let _ = add_universe_constraints sigma2 c in true - with Univ.UniverseInconsistency _ | UniversesDiffer -> false - else false + match ans with None -> false | Some _ -> true diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f68651a74..d87c7ef8d 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ @@ -22,10 +21,10 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : - env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * constr + ?principal:bool -> types -> (constr, 'r) Sigma.sigma val new_pure_evar : named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> @@ -129,7 +128,7 @@ val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.M [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t (** [occur_evar_upto sigma k c] returns [true] if [k] appears in @@ -170,8 +169,8 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> named_context -> named_context -val nf_rel_context_evar : evar_map -> rel_context -> rel_context +val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t val nf_env_evar : evar_map -> env -> env val nf_evar_info : evar_map -> evar_info -> evar_info @@ -252,4 +251,3 @@ val subterm_source : existential_key -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located val meta_counter_summary_name : string -val evar_counter_summary_name : string diff --git a/pretyping/evd.ml b/pretyping/evd.ml deleted file mode 100644 index 544114518..000000000 --- a/pretyping/evd.ml +++ /dev/null @@ -1,1912 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Errors -open Util -open Names -open Nameops -open Term -open Vars -open Termops -open Environ -open Globnames - -(** Generic filters *) -module Filter : -sig - type t - val equal : t -> t -> bool - val identity : t - val filter_list : t -> 'a list -> 'a list - val filter_array : t -> 'a array -> 'a array - val extend : int -> t -> t - val compose : t -> t -> t - val apply_subfilter : t -> bool list -> t - val restrict_upon : t -> int -> (int -> bool) -> t option - val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t - val make : bool list -> t - val repr : t -> bool list option -end = -struct - type t = bool list option - (** We guarantee through the interface that if a filter is [Some _] then it - contains at least one [false] somewhere. *) - - let identity = None - - let rec equal l1 l2 = match l1, l2 with - | [], [] -> true - | h1 :: l1, h2 :: l2 -> - (if h1 then h2 else not h2) && equal l1 l2 - | _ -> false - - let equal l1 l2 = match l1, l2 with - | None, None -> true - | Some _, None | None, Some _ -> false - | Some l1, Some l2 -> equal l1 l2 - - let rec is_identity = function - | [] -> true - | true :: l -> is_identity l - | false :: _ -> false - - let normalize f = if is_identity f then None else Some f - - let filter_list f l = match f with - | None -> l - | Some f -> CList.filter_with f l - - let filter_array f v = match f with - | None -> v - | Some f -> CArray.filter_with f v - - let rec extend n l = - if n = 0 then l - else extend (pred n) (true :: l) - - let extend n = function - | None -> None - | Some f -> Some (extend n f) - - let compose f1 f2 = match f1 with - | None -> f2 - | Some f1 -> - match f2 with - | None -> None - | Some f2 -> normalize (CList.filter_with f1 f2) - - let apply_subfilter_array filter subfilter = - (** In both cases we statically know that the argument will contain at - least one [false] *) - match filter with - | None -> Some (Array.to_list subfilter) - | Some f -> - let len = Array.length subfilter in - let fold b (i, ans) = - if b then - let () = assert (0 <= i) in - (pred i, Array.unsafe_get subfilter i :: ans) - else - (i, false :: ans) - in - Some (snd (List.fold_right fold f (pred len, []))) - - let apply_subfilter filter subfilter = - apply_subfilter_array filter (Array.of_list subfilter) - - let restrict_upon f len p = - let newfilter = Array.init len p in - if Array.for_all (fun id -> id) newfilter then None - else - Some (apply_subfilter_array f newfilter) - - let map_along f flt l = - let ans = match flt with - | None -> List.map (fun x -> f true x) l - | Some flt -> List.map2 f flt l - in - normalize ans - - let make l = normalize l - - let repr f = f - -end - -(* The kinds of existential variables are now defined in [Evar_kinds] *) - -(* The type of mappings for existential variables *) - -module Dummy = struct end -module Store = Store.Make(Dummy) - -type evar = Term.existential_key - -let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) - -type evar_body = - | Evar_empty - | Evar_defined of constr - -type evar_info = { - evar_concl : constr; - evar_hyps : named_context_val; - evar_body : evar_body; - evar_filter : Filter.t; - evar_source : Evar_kinds.t Loc.located; - evar_candidates : constr list option; (* if not None, list of allowed instances *) - evar_extra : Store.t } - -let make_evar hyps ccl = { - evar_concl = ccl; - evar_hyps = hyps; - evar_body = Evar_empty; - evar_filter = Filter.identity; - evar_source = (Loc.ghost,Evar_kinds.InternalHole); - evar_candidates = None; - evar_extra = Store.empty -} - -let instance_mismatch () = - anomaly (Pp.str "Signature and its instance do not match") - -let evar_concl evi = evi.evar_concl - -let evar_filter evi = evi.evar_filter - -let evar_body evi = evi.evar_body - -let evar_context evi = named_context_of_val evi.evar_hyps - -let evar_filtered_context evi = - Filter.filter_list (evar_filter evi) (evar_context evi) - -let evar_hyps evi = evi.evar_hyps - -let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with -| None -> evar_hyps evi -| Some filter -> - let rec make_hyps filter ctxt = match filter, ctxt with - | [], [] -> empty_named_context_val - | false :: filter, _ :: ctxt -> make_hyps filter ctxt - | true :: filter, decl :: ctxt -> - let hyps = make_hyps filter ctxt in - push_named_context_val decl hyps - | _ -> instance_mismatch () - in - make_hyps filter (evar_context evi) - -let evar_env evi = Global.env_of_context evi.evar_hyps - -let evar_filtered_env evi = match Filter.repr (evar_filter evi) with -| None -> evar_env evi -| Some filter -> - let rec make_env filter ctxt = match filter, ctxt with - | [], [] -> reset_context (Global.env ()) - | false :: filter, _ :: ctxt -> make_env filter ctxt - | true :: filter, decl :: ctxt -> - let env = make_env filter ctxt in - push_named decl env - | _ -> instance_mismatch () - in - make_env filter (evar_context evi) - -let map_evar_body f = function - | Evar_empty -> Evar_empty - | Evar_defined d -> Evar_defined (f d) - -let map_evar_info f evi = - {evi with - evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; - evar_concl = f evi.evar_concl; - evar_candidates = Option.map (List.map f) evi.evar_candidates } - -let evar_ident_info evi = - match evi.evar_source with - | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id - | _,Evar_kinds.VarInstance id -> id - | _,Evar_kinds.GoalEvar -> Id.of_string "Goal" - | _ -> - let env = reset_with_named_context evi.evar_hyps (Global.env()) in - Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous - -(* This exception is raised by *.existential_value *) -exception NotInstantiatedEvar - -(* Note: let-in contributes to the instance *) - -let evar_instance_array test_id info args = - let len = Array.length args in - let rec instrec filter ctxt i = match filter, ctxt with - | [], [] -> - if Int.equal i len then [] - else instance_mismatch () - | false :: filter, _ :: ctxt -> - instrec filter ctxt i - | true :: filter, (id,_,_ as d) :: ctxt -> - if i < len then - let c = Array.unsafe_get args i in - if test_id d c then instrec filter ctxt (succ i) - else (id, c) :: instrec filter ctxt (succ i) - else instance_mismatch () - | _ -> instance_mismatch () - in - match Filter.repr (evar_filter info) with - | None -> - let map i (id,_,_ as d) = - if (i < len) then - let c = Array.unsafe_get args i in - if test_id d c then None else Some (id,c) - else instance_mismatch () - in - List.map_filter_i map (evar_context info) - | Some filter -> - instrec filter (evar_context info) 0 - -let make_evar_instance_array info args = - evar_instance_array (fun (id,_,_) -> isVarId id) info args - -let instantiate_evar_array info c args = - let inst = make_evar_instance_array info args in - match inst with - | [] -> c - | _ -> replace_vars inst c - -module StringOrd = struct type t = string let compare = String.compare end -module UNameMap = struct - - include Map.Make(StringOrd) - - let union s t = - if s == t then s - else - merge (fun k l r -> - match l, r with - | Some _, _ -> l - | _, _ -> r) s t -end - -(* 2nd part used to check consistency on the fly. *) -type evar_universe_context = - { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; - uctx_local : Univ.universe_context_set; (** The local context of variables *) - uctx_univ_variables : Universes.universe_opt_subst; - (** The local universes that are unification variables *) - uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that can be instantiated with - algebraic universes as they appear in inferred types only. *) - uctx_universes : Univ.universes; (** The current graph extended with the local constraints *) - uctx_initial_universes : Univ.universes; (** The graph at the creation of the evar_map *) - } - -let empty_evar_universe_context = - { uctx_names = UNameMap.empty, Univ.LMap.empty; - uctx_local = Univ.ContextSet.empty; - uctx_univ_variables = Univ.LMap.empty; - uctx_univ_algebraic = Univ.LSet.empty; - uctx_universes = Univ.initial_universes; - uctx_initial_universes = Univ.initial_universes } - -let evar_universe_context_from e = - let u = universes e in - {empty_evar_universe_context with - uctx_universes = u; uctx_initial_universes = u} - -let is_empty_evar_universe_context ctx = - Univ.ContextSet.is_empty ctx.uctx_local && - Univ.LMap.is_empty ctx.uctx_univ_variables - -let union_evar_universe_context ctx ctx' = - if ctx == ctx' then ctx - else if is_empty_evar_universe_context ctx' then ctx - else - let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in - let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) - (Univ.ContextSet.levels ctx.uctx_local) in - let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in - let declarenew g = - Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g - in - let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in - { uctx_names = (names, names_rev); - uctx_local = local; - uctx_univ_variables = - Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables; - uctx_univ_algebraic = - Univ.LSet.union ctx.uctx_univ_algebraic ctx'.uctx_univ_algebraic; - uctx_initial_universes = declarenew ctx.uctx_initial_universes; - uctx_universes = - if local == ctx.uctx_local then ctx.uctx_universes - else - let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - Univ.merge_constraints cstrsr (declarenew ctx.uctx_universes) } - -(* let union_evar_universe_context_key = Profile.declare_profile "union_evar_universe_context";; *) -(* let union_evar_universe_context = *) -(* Profile.profile2 union_evar_universe_context_key union_evar_universe_context;; *) - -type 'a in_evar_universe_context = 'a * evar_universe_context - -let evar_universe_context_set diff ctx = - let initctx = ctx.uctx_local in - let cstrs = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty - in - Univ.ContextSet.add_constraints cstrs initctx - -let evar_universe_context_constraints ctx = snd ctx.uctx_local -let evar_context_universe_context ctx = Univ.ContextSet.to_context ctx.uctx_local - -let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local = ctx } -let evar_universe_context_subst ctx = ctx.uctx_univ_variables - -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) - -let evar_universe_context_of_binders b = - let ctx = empty_evar_universe_context in - let names = - List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) - ctx.uctx_names b - in { ctx with uctx_names = names } - -let instantiate_variable l b v = - v := Univ.LMap.add l (Some b) !v - -exception UniversesDiffer - -let process_universe_constraints univs vars alg cstrs = - let vars = ref vars in - let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo l d r local = - let l = normalize l and r = normalize r in - if Univ.Universe.equal l r then local - else - let varinfo x = - match Univ.Universe.level x with - | None -> Inl x - | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l alg) - in - if d == Universes.ULe then - if Univ.check_leq univs l r then - (** Keep Prop/Set <= var around if var might be instantiated by prop or set - later. *) - if Univ.Universe.is_level l then - match Univ.Universe.level r with - | Some r -> - Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local - | _ -> local - else local - else - match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl then - let levels = Univ.Universe.levels l in - Univ.LSet.fold (fun l local -> - if Univ.Level.is_small l || Univ.LMap.mem l !vars then - unify_universes fo (Univ.Universe.make l) Universes.UEq r local - else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) - levels local - else - Univ.enforce_leq l r local - else if d == Universes.ULub then - match varinfo l, varinfo r with - | (Inr (l, true, _), Inr (r, _, _)) - | (Inr (r, _, _), Inr (l, true, _)) -> - instantiate_variable l (Univ.Universe.make r) vars; - Univ.enforce_eq_level l r local - | Inr (_, _, _), Inr (_, _, _) -> - unify_universes true l Universes.UEq r local - | _, _ -> assert false - else (* d = Universes.UEq *) - match varinfo l, varinfo r with - | Inr (l', lloc, _), Inr (r', rloc, _) -> - let () = - if lloc then - instantiate_variable l' r vars - else if rloc then - instantiate_variable r' l vars - else if not (Univ.check_eq univs l r) then - (* Two rigid/global levels, none of them being local, - one of them being Prop/Set, disallow *) - if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) - else - if fo then - raise UniversesDiffer - in - Univ.enforce_eq_level l' r' local - | Inr (l, loc, alg), Inl r - | Inl r, Inr (l, loc, alg) -> - let inst = Univ.univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) - else - let lu = Univ.Universe.make l in - if Univ.univ_level_mem l r then - Univ.enforce_leq inst lu local - else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) - | _, _ (* One of the two is algebraic or global *) -> - if Univ.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) - in - let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty - in - !vars, local - -let add_constraints_context ctx cstrs = - let univs, local = ctx.uctx_local in - let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> - let l = Univ.Universe.make l and r = Univ.Universe.make r in - let cstr' = - if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r) - else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r) - in Universes.Constraints.add cstr' acc) - cstrs Universes.Constraints.empty - in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs' - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } - -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) - -let add_universe_constraints_context ctx cstrs = - let univs, local = ctx.uctx_local in - let vars, local' = - process_universe_constraints ctx.uctx_universes - ctx.uctx_univ_variables ctx.uctx_univ_algebraic - cstrs - in - { ctx with uctx_local = (univs, Univ.Constraint.union local local'); - uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } - -(* let addunivconstrkey = Profile.declare_profile "add_universe_constraints_context";; *) -(* let add_universe_constraints_context = *) -(* Profile.profile2 addunivconstrkey add_universe_constraints_context;; *) -(*******************************************************************) -(* Metamaps *) - -(*******************************************************************) -(* Constraints for existential variables *) -(*******************************************************************) - -type 'a freelisted = { - rebus : 'a; - freemetas : Int.Set.t } - -(* Collects all metavars appearing in a constr *) -let metavars_of c = - let rec collrec acc c = - match kind_of_term c with - | Meta mv -> Int.Set.add mv acc - | _ -> fold_constr collrec acc c - in - collrec Int.Set.empty c - -let mk_freelisted c = - { rebus = c; freemetas = metavars_of c } - -let map_fl f cfl = { cfl with rebus=f cfl.rebus } - -(* Status of an instance found by unification wrt to the meta it solves: - - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - - a term that can be eta-expanded n times while still being a solution - (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) -*) - -type instance_constraint = IsSuperType | IsSubType | Conv - -let eq_instance_constraint c1 c2 = c1 == c2 - -(* Status of the unification of the type of an instance against the type of - the meta it instantiates: - - CoerceToType means that the unification of types has not been done - and that a coercion can still be inserted: the meta should not be - substituted freely (this happens for instance given via the - "with" binding clause). - - TypeProcessed means that the information obtainable from the - unification of types has been extracted. - - TypeNotProcessed means that the unification of types has not been - done but it is known that no coercion may be inserted: the meta - can be substituted freely. -*) - -type instance_typing_status = - CoerceToType | TypeNotProcessed | TypeProcessed - -(* Status of an instance together with the status of its type unification *) - -type instance_status = instance_constraint * instance_typing_status - -(* Clausal environments *) - -type clbinding = - | Cltyp of Name.t * constr freelisted - | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted - -let map_clb f = function - | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl) - | Clval (na,(cfl1,pb),cfl2) -> Clval (na,(map_fl f cfl1,pb),map_fl f cfl2) - -(* name of defined is erased (but it is pretty-printed) *) -let clb_name = function - Cltyp(na,_) -> (na,false) - | Clval (na,_,_) -> (na,true) - -(***********************) - -module Metaset = Int.Set - -module Metamap = Int.Map - -let metamap_to_list m = - Metamap.fold (fun n v l -> (n,v)::l) m [] - -(*************************) -(* Unification state *) - -type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * Environ.env * constr * constr - -module EvMap = Evar.Map - -type evar_map = { - (** Existential variables *) - defn_evars : evar_info EvMap.t; - undf_evars : evar_info EvMap.t; - evar_names : Id.t EvMap.t * existential_key Idmap.t; - (** Universes *) - universes : evar_universe_context; - (** Conversion problems *) - conv_pbs : evar_constraint list; - last_mods : Evar.Set.t; - (** Metas *) - metas : clbinding Metamap.t; - (** Interactive proofs *) - effects : Safe_typing.private_constants; - future_goals : Evar.t list; (** list of newly created evars, to be - eventually turned into goals if not solved.*) - principal_future_goal : Evar.t option; (** if [Some e], [e] must be - contained - [future_goals]. The evar - [e] will inherit - properties (now: the - name) of the evar which - will be instantiated with - a term containing [e]. *) - extras : Store.t; -} - -(*** Lifting primitive from Evar.Map. ***) - -let add_name_newly_undefined naming evk evi (evtoid,idtoev) = - let id = match naming with - | Misctypes.IntroAnonymous -> - let id = evar_ident_info evi in - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) - | Misctypes.IntroIdentifier id -> - let id' = - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - if not (Names.Id.equal id id') then - user_err_loc - (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); - id' - | Misctypes.IntroFresh id -> - Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) - -let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = - if EvMap.mem evk evtoid then - evar_names - else - add_name_newly_undefined naming evk evi evar_names - -let remove_name_defined evk (evtoid,idtoev) = - let id = EvMap.find evk evtoid in - (EvMap.remove evk evtoid, Idmap.remove id idtoev) - -let remove_name_possibly_already_defined evk evar_names = - try remove_name_defined evk evar_names - with Not_found -> evar_names - -let rename evk id evd = - let (evtoid,idtoev) = evd.evar_names in - let id' = EvMap.find evk evtoid in - if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); - { evd with evar_names = - (EvMap.add evk id evtoid (* overwrite old name *), - Idmap.add id evk (Idmap.remove id' idtoev)) } - -let reassign_name_defined evk evk' (evtoid,idtoev) = - let id = EvMap.find evk evtoid in - (EvMap.add evk' id (EvMap.remove evk evtoid), - Idmap.add id evk' (Idmap.remove id idtoev)) - -let add d e i = match i.evar_body with -| Evar_empty -> - let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in - { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } -| Evar_defined _ -> - let evar_names = remove_name_possibly_already_defined e d.evar_names in - { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } - -let remove d e = - let undf_evars = EvMap.remove e d.undf_evars in - let defn_evars = EvMap.remove e d.defn_evars in - let principal_future_goal = match d.principal_future_goal with - | None -> None - | Some e' -> if Evar.equal e e' then None else d.principal_future_goal - in - let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in - { d with undf_evars; defn_evars; principal_future_goal; future_goals } - -let find d e = - try EvMap.find e d.undf_evars - with Not_found -> EvMap.find e d.defn_evars - -let find_undefined d e = EvMap.find e d.undf_evars - -let mem d e = EvMap.mem e d.undf_evars || EvMap.mem e d.defn_evars - -(* spiwack: this function loses information from the original evar_map - it might be an idea not to export it. *) -let to_list d = - (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) - let l = ref [] in - EvMap.iter (fun evk x -> l := (evk,x)::!l) d.defn_evars; - EvMap.iter (fun evk x -> l := (evk,x)::!l) d.undf_evars; - !l - -let undefined_map d = d.undf_evars - -let drop_all_defined d = { d with defn_evars = EvMap.empty } - -(* spiwack: not clear what folding over an evar_map, for now we shall - simply fold over the inner evar_map. *) -let fold f d a = - EvMap.fold f d.defn_evars (EvMap.fold f d.undf_evars a) - -let fold_undefined f d a = EvMap.fold f d.undf_evars a - -let raw_map f d = - let f evk info = - let ans = f evk info in - let () = match info.evar_body, ans.evar_body with - | Evar_defined _, Evar_empty - | Evar_empty, Evar_defined _ -> - anomaly (str "Unrespectful mapping function.") - | _ -> () - in - ans - in - let defn_evars = EvMap.smartmapi f d.defn_evars in - let undf_evars = EvMap.smartmapi f d.undf_evars in - { d with defn_evars; undf_evars; } - -let raw_map_undefined f d = - let f evk info = - let ans = f evk info in - let () = match ans.evar_body with - | Evar_defined _ -> - anomaly (str "Unrespectful mapping function.") - | _ -> () - in - ans - in - { d with undf_evars = EvMap.smartmapi f d.undf_evars; } - -let is_evar = mem - -let is_defined d e = EvMap.mem e d.defn_evars - -let is_undefined d e = EvMap.mem e d.undf_evars - -let existential_value d (n, args) = - let info = find d n in - match evar_body info with - | Evar_defined c -> - instantiate_evar_array info c args - | Evar_empty -> - raise NotInstantiatedEvar - -let existential_opt_value d ev = - try Some (existential_value d ev) - with NotInstantiatedEvar -> None - -let existential_type d (n, args) = - let info = - try find d n - with Not_found -> - anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in - instantiate_evar_array info info.evar_concl args - -let add_constraints d c = - { d with universes = add_constraints_context d.universes c } - -let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } - -(*** /Lifting... ***) - -(* evar_map are considered empty disregarding histories *) -let is_empty d = - EvMap.is_empty d.defn_evars && - EvMap.is_empty d.undf_evars && - List.is_empty d.conv_pbs && - Metamap.is_empty d.metas - -let cmap f evd = - { evd with - metas = Metamap.map (map_clb f) evd.metas; - defn_evars = EvMap.map (map_evar_info f) evd.defn_evars; - undf_evars = EvMap.map (map_evar_info f) evd.undf_evars - } - -(* spiwack: deprecated *) -let create_evar_defs sigma = { sigma with - conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } -(* spiwack: tentatively deprecated *) -let create_goal_evar_defs sigma = { sigma with - (* conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } *) - metas=Metamap.empty } - -let empty = { - defn_evars = EvMap.empty; - undf_evars = EvMap.empty; - universes = empty_evar_universe_context; - conv_pbs = []; - last_mods = Evar.Set.empty; - metas = Metamap.empty; - effects = Safe_typing.empty_private_constants; - evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) - future_goals = []; - principal_future_goal = None; - extras = Store.empty; -} - -let from_env e = - { empty with universes = evar_universe_context_from e } - -let from_ctx ctx = { empty with universes = ctx } - -let has_undefined evd = not (EvMap.is_empty evd.undf_evars) - -let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = - let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in - let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in - let universes = - if not with_univs then evd.universes - else union_evar_universe_context evd.universes d.universes - in - { evd with - metas = d.metas; - last_mods; conv_pbs; universes } - -let merge_universe_context evd uctx' = - { evd with universes = union_evar_universe_context evd.universes uctx' } - -let set_universe_context evd uctx' = - { evd with universes = uctx' } - -let add_conv_pb ?(tail=false) pb d = - if tail then {d with conv_pbs = d.conv_pbs @ [pb]} - else {d with conv_pbs = pb::d.conv_pbs} - -let evar_source evk d = (find d evk).evar_source - -let evar_ident evk evd = - try EvMap.find evk (fst evd.evar_names) - with Not_found -> - (* Unnamed (non-dependent) evar *) - add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk)) - -let evar_key id evd = - Idmap.find id (snd evd.evar_names) - -let define_aux def undef evk body = - let oldinfo = - try EvMap.find evk undef - with Not_found -> - if EvMap.mem evk def then - anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") - else - anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") - in - let () = assert (oldinfo.evar_body == Evar_empty) in - let newinfo = { oldinfo with evar_body = Evar_defined body } in - EvMap.add evk newinfo def, EvMap.remove evk undef - -(* define the existential of section path sp as the constr body *) -let define evk body evd = - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in - let last_mods = match evd.conv_pbs with - | [] -> evd.last_mods - | _ -> Evar.Set.add evk evd.last_mods - in - let evar_names = remove_name_defined evk evd.evar_names in - { evd with defn_evars; undf_evars; last_mods; evar_names } - -let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) - ?(filter=Filter.identity) ?candidates ?(store=Store.empty) - ?(naming=Misctypes.IntroAnonymous) evd = - let () = match Filter.repr filter with - | None -> () - | Some filter -> - assert (Int.equal (List.length filter) (List.length (named_context_of_val hyps))) - in - let evar_info = { - evar_hyps = hyps; - evar_concl = ty; - evar_body = Evar_empty; - evar_filter = filter; - evar_source = src; - evar_candidates = candidates; - evar_extra = store; } - in - let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in - { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } - -let restrict evk evk' filter ?candidates evd = - let evar_info = EvMap.find evk evd.undf_evars in - let evar_info' = - { evar_info with evar_filter = filter; - evar_candidates = candidates; - evar_extra = Store.empty } in - let evar_names = reassign_name_defined evk evk' evd.evar_names in - let ctxt = Filter.filter_list filter (evar_context evar_info) in - let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in - let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in - { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; evar_names } - -let downcast evk ccl evd = - let evar_info = EvMap.find evk evd.undf_evars in - let evar_info' = { evar_info with evar_concl = ccl } in - { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars } - -(* extracts conversion problems that satisfy predicate p *) -(* Note: conv_pbs not satisying p are stored back in reverse order *) -let extract_conv_pbs evd p = - let (pbs,pbs1) = - List.fold_left - (fun (pbs,pbs1) pb -> - if p pb then - (pb::pbs,pbs1) - else - (pbs,pb::pbs1)) - ([],[]) - evd.conv_pbs - in - {evd with conv_pbs = pbs1; last_mods = Evar.Set.empty}, - pbs - -let extract_changed_conv_pbs evd p = - extract_conv_pbs evd (fun pb -> p evd.last_mods pb) - -let extract_all_conv_pbs evd = - extract_conv_pbs evd (fun _ -> true) - -let loc_of_conv_pb evd (pbty,env,t1,t2) = - match kind_of_term (fst (decompose_app t1)) with - | Evar (evk1,_) -> fst (evar_source evk1 evd) - | _ -> - match kind_of_term (fst (decompose_app t2)) with - | Evar (evk2,_) -> fst (evar_source evk2 evd) - | _ -> Loc.ghost - -(** The following functions return the set of evars immediately - contained in the object *) - -(* excluding defined evars *) - -let evar_list c = - let rec evrec acc c = - match kind_of_term c with - | Evar (evk, _ as ev) -> ev :: acc - | _ -> fold_constr evrec acc c in - evrec [] c - -let evars_of_term c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> fold_constr evrec acc c - in - evrec Evar.Set.empty c - -let evars_of_named_context nc = - List.fold_right (fun (_, b, t) s -> - Option.fold_left (fun s t -> - Evar.Set.union s (evars_of_term t)) - (Evar.Set.union s (evars_of_term t)) b) - nc Evar.Set.empty - -let evars_of_filtered_evar_info evi = - Evar.Set.union (evars_of_term evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b) - (evars_of_named_context (evar_filtered_context evi))) - -(**********************************************************) -(* Sort variables *) - -type rigid = - | UnivRigid - | UnivFlexible of bool (** Is substitution by an algebraic ok? *) - -let univ_rigid = UnivRigid -let univ_flexible = UnivFlexible false -let univ_flexible_alg = UnivFlexible true - -let evar_universe_context d = d.universes - -let universe_context_set d = d.universes.uctx_local - -let pr_uctx_level uctx = - let map, map_rev = uctx.uctx_names in - fun l -> - try str(Univ.LMap.find l map_rev) - with Not_found -> - Universes.pr_with_global_universes l - -let universe_context ?names evd = - match names with - | None -> [], Univ.ContextSet.to_context evd.universes.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels evd.universes.uctx_local in - let newinst, map, left = - List.fold_right - (fun (loc,id) (newinst, map, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst evd.universes.uctx_names) - with Not_found -> - user_err_loc (loc, "universe_context", - str"Universe " ++ pr_id id ++ str" is not bound anymore.") - in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) - pl ([], [], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - errorlabstrm "universe_context" - (str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level evd.universes) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") - else - let inst = Univ.Instance.of_array (Array.of_list newinst) in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints evd.universes.uctx_local) - in map, ctx - -let restrict_universe_context evd vars = - let uctx = evd.universes in - let uctx' = Universes.restrict_universe_context uctx.uctx_local vars in - { evd with universes = { uctx with uctx_local = uctx' } } - -let universe_subst evd = - evd.universes.uctx_univ_variables - -let merge_uctx sideff rigid uctx ctx' = - let open Univ in - let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else - match rigid with - | UnivRigid -> uctx - | UnivFlexible b -> - let fold u accu = - if LMap.mem u accu then accu - else LMap.add u None accu - in - let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in - if b then - { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } - else { uctx with uctx_univ_variables = uvars' } - in - let uctx_local = - if sideff then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local - in - let declare g = - LSet.fold (fun u g -> - try Univ.add_universe u false g - with Univ.AlreadyDeclared when sideff -> g) - levels g - in - let initial = declare uctx.uctx_initial_universes in - let univs = declare uctx.uctx_universes in - let uctx_universes = merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } - -let merge_context_set ?(sideff=false) rigid evd ctx' = - {evd with universes = merge_uctx sideff rigid evd.universes ctx'} - -let merge_uctx_subst uctx s = - { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } - -let merge_universe_subst evd subst = - {evd with universes = merge_uctx_subst evd.universes subst } - -let with_context_set rigid d (a, ctx) = - (merge_context_set rigid d ctx, a) - -let emit_universe_side_effects eff u = - let uctxs = Safe_typing.universes_of_private eff in - List.fold_left (merge_uctx true univ_rigid) u uctxs - -let uctx_new_univ_variable rigid name predicative - ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = Universes.new_univ_level (Global.current_dirpath ()) in - let ctx' = Univ.ContextSet.add_universe u ctx in - let uctx', pred = - match rigid with - | UnivRigid -> uctx, true - | UnivFlexible b -> - let uvars' = Univ.LMap.add u None uvars in - if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars}, false - else {uctx with uctx_univ_variables = uvars'}, false - in - let names = - match name with - | Some n -> add_uctx_names n u uctx.uctx_names - | None -> uctx.uctx_names - in - let initial = - Univ.add_universe u false uctx.uctx_initial_universes - in - let uctx' = - {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u false uctx.uctx_universes; - uctx_initial_universes = initial} - in uctx', u - -let new_univ_level_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in - ({evd with universes = uctx'}, u) - -let new_univ_variable ?name ?(predicative=true) rigid evd = - let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in - ({evd with universes = uctx'}, Univ.Universe.make u) - -let new_sort_variable ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable rigid ?name ~predicative d in - (d', Type u) - -let add_global_univ d u = - let uctx = d.universes in - let initial = - Univ.add_universe u true uctx.uctx_initial_universes - in - let univs = - Univ.add_universe u true uctx.uctx_universes - in - { d with universes = { uctx with uctx_local = Univ.ContextSet.add_universe u uctx.uctx_local; - uctx_initial_universes = initial; - uctx_universes = univs } } - -let make_flexible_variable evd b u = - let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as ctx = evd.universes in - let uvars' = Univ.LMap.add u None uvars in - let avars' = - if b then - let uu = Univ.Universe.make u in - let substu_not_alg u' v = - Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v - in - if not (Univ.LMap.exists substu_not_alg uvars) - then Univ.LSet.add u avars else avars - else avars - in - {evd with universes = {ctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = avars'}} - -let make_evar_universe_context e l = - let uctx = evar_universe_context_from e in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx (loc,id) -> - fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx)) - uctx us - -(****************************************) -(* Operations on constants *) -(****************************************) - -let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = - with_context_set rigid evd (Universes.fresh_sort_in_family env s) - -let fresh_constant_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constant_instance env c) - -let fresh_inductive_instance env evd i = - with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i) - -let fresh_constructor_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c) - -let fresh_global ?(rigid=univ_flexible) ?names env evd gr = - with_context_set rigid evd (Universes.fresh_global_instance ?names env gr) - -let whd_sort_variable evd t = t - -let is_sort_variable evd s = - match s with - | Type u -> - (match Univ.universe_level u with - | Some l as x -> - let uctx = evd.universes in - if Univ.LSet.mem l (Univ.ContextSet.levels uctx.uctx_local) then x - else None - | None -> None) - | _ -> None - -let is_flexible_level evd l = - let uctx = evd.universes in - Univ.LMap.mem l uctx.uctx_univ_variables - -let is_eq_sort s1 s2 = - if Sorts.equal s1 s2 then None - else - let u1 = univ_of_sort s1 - and u2 = univ_of_sort s2 in - if Univ.Universe.equal u1 u2 then None - else Some (u1, u2) - -let normalize_universe evd = - let vars = ref evd.universes.uctx_univ_variables in - let normalize = Universes.normalize_universe_opt_subst vars in - normalize - -let normalize_universe_instance evd l = - let vars = ref evd.universes.uctx_univ_variables in - let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in - Univ.Instance.subst_fn normalize l - -let normalize_sort evars s = - match s with - | Prop _ -> s - | Type u -> - let u' = normalize_universe evars u in - if u' == u then s else Type u' - -(* FIXME inefficient *) -let set_eq_sort env d s1 s2 = - let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in - match is_eq_sort s1 s2 with - | None -> d - | Some (u1, u2) -> - if not (type_in_type env) then - add_universe_constraints d - (Universes.Constraints.singleton (u1,Universes.UEq,u2)) - else - d - -let has_lub evd u1 u2 = - (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *) - (* (\* let dref, norm = memo_normalize_universe d in *\) *) - (* let u1 = normalize u1 and u2 = normalize u2 in *) - if Univ.Universe.equal u1 u2 then evd - else add_universe_constraints evd - (Universes.Constraints.singleton (u1,Universes.ULub,u2)) - -let set_eq_level d u1 u2 = - add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty) - -let set_leq_level d u1 u2 = - add_constraints d (Univ.enforce_leq_level u1 u2 Univ.Constraint.empty) - -let set_eq_instances ?(flex=false) d u1 u2 = - add_universe_constraints d - (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) - -let set_leq_sort env evd s1 s2 = - let s1 = normalize_sort evd s1 - and s2 = normalize_sort evd s2 in - match is_eq_sort s1 s2 with - | None -> evd - | Some (u1, u2) -> - (* if Univ.is_type0_univ u2 then *) - (* if Univ.is_small_univ u1 then evd *) - (* else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) - (* else if Univ.is_type0m_univ u2 then *) - (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) - (* else *) - if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) - else evd - -let check_eq evd s s' = - Univ.check_eq evd.universes.uctx_universes s s' - -let check_leq evd s s' = - Univ.check_leq evd.universes.uctx_universes s s' - -let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst) - -let normalize_evar_universe_context_variables uctx = - let normalized_variables, undef, def, subst = - Universes.normalize_univ_variables uctx.uctx_univ_variables - in - let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in - let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in - subst, { uctx with uctx_local = ctx_local'; - uctx_univ_variables = normalized_variables; - uctx_universes = univs } - -(* let normvarsconstrkey = Profile.declare_profile "normalize_evar_universe_context_variables";; *) -(* let normalize_evar_universe_context_variables = *) -(* Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *) - -let abstract_undefined_variables uctx = - let vars' = - Univ.LMap.fold (fun u v acc -> - if v == None then Univ.LSet.remove u acc - else acc) - uctx.uctx_univ_variables uctx.uctx_univ_algebraic - in { uctx with uctx_local = Univ.ContextSet.empty; - uctx_univ_algebraic = vars' } - -let fix_undefined_variables ({ universes = uctx } as evm) = - let algs', vars' = - Univ.LMap.fold (fun u v (algs, vars as acc) -> - if v == None then (Univ.LSet.remove u algs, Univ.LMap.remove u vars) - else acc) - uctx.uctx_univ_variables - (uctx.uctx_univ_algebraic, uctx.uctx_univ_variables) - in - {evm with universes = - { uctx with uctx_univ_variables = vars'; - uctx_univ_algebraic = algs' } } - - -let refresh_undefined_univ_variables uctx = - let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in - let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (Univ.subst_univs_level_level subst u) acc) - uctx.uctx_univ_algebraic Univ.LSet.empty - in - let vars = - Univ.LMap.fold - (fun u v acc -> - Univ.LMap.add (Univ.subst_univs_level_level subst u) - (Option.map (Univ.subst_univs_level_universe subst) v) acc) - uctx.uctx_univ_variables Univ.LMap.empty - in - let declare g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) - (Univ.ContextSet.levels ctx') g in - let initial = declare uctx.uctx_initial_universes in - let univs = declare Univ.initial_universes in - let uctx' = {uctx_names = uctx.uctx_names; - uctx_local = ctx'; - uctx_univ_variables = vars; uctx_univ_algebraic = alg; - uctx_universes = univs; - uctx_initial_universes = initial } in - uctx', subst - -let refresh_undefined_universes evd = - let uctx', subst = refresh_undefined_univ_variables evd.universes in - let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in - evd', subst - -let normalize_evar_universe_context uctx = - let rec fixpoint uctx = - let ((vars',algs'), us') = - Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables - uctx.uctx_univ_algebraic - in - if Univ.ContextSet.equal us' uctx.uctx_local then uctx - else - let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in - let uctx' = - { uctx_names = uctx.uctx_names; - uctx_local = us'; - uctx_univ_variables = vars'; - uctx_univ_algebraic = algs'; - uctx_universes = universes; - uctx_initial_universes = uctx.uctx_initial_universes } - in fixpoint uctx' - in fixpoint uctx - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let evd' = {evd with universes = uctx'} in - evd', subst - -let nf_constraints evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let uctx' = normalize_evar_universe_context uctx' in - {evd with universes = uctx'} - -let nf_constraints = - if Flags.profile then - let nfconstrkey = Profile.declare_profile "nf_constraints" in - Profile.profile1 nfconstrkey nf_constraints - else nf_constraints - -let universe_of_name evd s = - UNameMap.find s (fst evd.universes.uctx_names) - -let add_universe_name evd s l = - let names' = add_uctx_names s l evd.universes.uctx_names in - {evd with universes = {evd.universes with uctx_names = names'}} - -let universes evd = evd.universes.uctx_universes - -let update_sigma_env evd env = - let univs = Environ.universes env in - let eunivs = - { evd.universes with uctx_initial_universes = univs; - uctx_universes = univs } - in - let eunivs = merge_uctx true univ_rigid eunivs eunivs.uctx_local in - { evd with universes = eunivs } - -(* Conversion w.r.t. an evar map and its local universes. *) - -let test_conversion_gen env evd pb t u = - match pb with - | Reduction.CONV -> - Reduction.trans_conv_universes - full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes - full_transparent_state ~evars:(existential_opt_value evd) env - evd.universes.uctx_universes t u - -let test_conversion env d pb t u = - try test_conversion_gen env d pb t u; true - with _ -> false - -let eq_constr_univs evd t u = - let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in - if b then - try let evd' = add_universe_constraints evd c in evd', b - with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false - else evd, b - -let e_eq_constr_univs evdref t u = - let evd, b = eq_constr_univs !evdref t u in - evdref := evd; b - -(**********************************************************) -(* Side effects *) - -let emit_side_effects eff evd = - { evd with effects = Safe_typing.concat_private eff evd.effects; - universes = emit_universe_side_effects eff evd.universes } - -let drop_side_effects evd = - { evd with effects = Safe_typing.empty_private_constants; } - -let eval_side_effects evd = evd.effects - -(* Future goals *) -let declare_future_goal evk evd = - { evd with future_goals = evk::evd.future_goals } - -let declare_principal_goal evk evd = - match evd.principal_future_goal with - | None -> { evd with - future_goals = evk::evd.future_goals; - principal_future_goal=Some evk; } - | Some _ -> Errors.error "Only one main subgoal per instantiation." - -let future_goals evd = evd.future_goals - -let principal_future_goal evd = evd.principal_future_goal - -let reset_future_goals evd = - { evd with future_goals = [] ; principal_future_goal=None } - -let restore_future_goals evd gls pgl = - { evd with future_goals = gls ; principal_future_goal = pgl } - -(**********************************************************) -(* Accessing metas *) - -(** We use this function to overcome OCaml compiler limitations and to prevent - the use of costly in-place modifications. *) -let set_metas evd metas = { - defn_evars = evd.defn_evars; - undf_evars = evd.undf_evars; - universes = evd.universes; - conv_pbs = evd.conv_pbs; - last_mods = evd.last_mods; - metas; - effects = evd.effects; - evar_names = evd.evar_names; - future_goals = evd.future_goals; - principal_future_goal = evd.principal_future_goal; - extras = evd.extras; -} - -let meta_list evd = metamap_to_list evd.metas - -let undefined_metas evd = - let filter = function - | (n,Clval(_,_,typ)) -> None - | (n,Cltyp (_,typ)) -> Some n - in - let m = List.map_filter filter (meta_list evd) in - List.sort Int.compare m - -let map_metas_fvalue f evd = - let map = function - | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ) - | x -> x - in - set_metas evd (Metamap.smartmap map evd.metas) - -let map_metas f evd = - let map cl = map_clb f cl in - set_metas evd (Metamap.smartmap map evd.metas) - -let meta_opt_fvalue evd mv = - match Metamap.find mv evd.metas with - | Clval(_,b,_) -> Some b - | Cltyp _ -> None - -let meta_defined evd mv = - match Metamap.find mv evd.metas with - | Clval _ -> true - | Cltyp _ -> false - -let try_meta_fvalue evd mv = - match Metamap.find mv evd.metas with - | Clval(_,b,_) -> b - | Cltyp _ -> raise Not_found - -let meta_fvalue evd mv = - try try_meta_fvalue evd mv - with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value") - -let meta_value evd mv = - (fst (try_meta_fvalue evd mv)).rebus - -let meta_ftype evd mv = - match Metamap.find mv evd.metas with - | Cltyp (_,b) -> b - | Clval(_,_,b) -> b - -let meta_type evd mv = (meta_ftype evd mv).rebus - -let meta_declare mv v ?(name=Anonymous) evd = - let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in - set_metas evd metas - -let meta_assign mv (v, pb) evd = - let modify _ = function - | Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined") - in - let metas = Metamap.modify mv modify evd.metas in - set_metas evd metas - -let meta_reassign mv (v, pb) evd = - let modify _ = function - | Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty) - | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined") - in - let metas = Metamap.modify mv modify evd.metas in - set_metas evd metas - -(* If the meta is defined then forget its name *) -let meta_name evd mv = - try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous - -let explain_no_such_bound_variable evd id = - let mvl = - List.rev (Metamap.fold (fun n clb l -> - let na = fst (clb_name clb) in - if na != Anonymous then out_name na :: l else l) - evd.metas []) in - errorlabstrm "Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ - (if mvl == [] then str " (no bound variables at all in the expression)." - else - (str" (possible name" ++ - str (if List.length mvl == 1 then " is: " else "s are: ") ++ - pr_enum pr_id mvl ++ str")."))) - -let meta_with_name evd id = - let na = Name id in - let (mvl,mvnodef) = - Metamap.fold - (fun n clb (l1,l2 as l) -> - let (na',def) = clb_name clb in - if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) - else l) - evd.metas ([],[]) in - match mvnodef, mvl with - | _,[] -> - explain_no_such_bound_variable evd id - | ([n],_|_,[n]) -> - n - | _ -> - errorlabstrm "Evd.meta_with_name" - (str "Binder name \"" ++ pr_id id ++ - strbrk "\" occurs more than once in clause.") - -let clear_metas evd = {evd with metas = Metamap.empty} - -let meta_merge ?(with_univs = true) evd1 evd2 = - let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in - let universes = - if with_univs then union_evar_universe_context evd2.universes evd1.universes - else evd2.universes - in - {evd2 with universes; metas; } - -type metabinding = metavariable * constr * instance_status - -let retract_coercible_metas evd = - let mc = ref [] in - let map n v = match v with - | Clval (na, (b, (Conv, CoerceToType as s)), typ) -> - let () = mc := (n, b.rebus, s) :: !mc in - Cltyp (na, typ) - | v -> v - in - let metas = Metamap.smartmapi map evd.metas in - !mc, set_metas evd metas - -let subst_defined_metas_evars (bl,el) c = - let rec substrec c = match kind_of_term c with - | Meta i -> - let select (j,_,_) = Int.equal i j in - substrec (pi2 (List.find select bl)) - | Evar (evk,args) -> - let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in - (try substrec (pi3 (List.find select el)) - with Not_found -> map_constr substrec c) - | _ -> map_constr substrec c - in try Some (substrec c) with Not_found -> None - -let evar_source_of_meta mv evd = - match meta_name evd mv with - | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) - | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) - -let dependent_evar_ident ev evd = - let evi = find evd ev in - match evi.evar_source with - | (_,Evar_kinds.VarInstance id) -> id - | _ -> anomaly (str "Not an evar resulting of a dependent binding") - -(**********************************************************) -(* Extra data *) - -let get_extra_data evd = evd.extras -let set_extra_data extras evd = { evd with extras } - -(*******************************************************************) - -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - -type open_constr = evar_map * constr - -(*******************************************************************) -(* The type constructor ['a sigma] adds an evar map to an object of - type ['a] *) -type 'a sigma = { - it : 'a ; - sigma : evar_map -} - -let sig_it x = x.it -let sig_sig x = x.sigma -let on_sig s f = - let sigma', v = f s.sigma in - { s with sigma = sigma' }, v - -(*******************************************************************) -(* The state monad with state an evar map. *) - -module MonadR = - Monad.Make (struct - - type +'a t = evar_map -> evar_map * 'a - - let return a = fun s -> (s,a) - - let (>>=) x f = fun s -> - let (s',a) = x s in - f a s' - - let (>>) x y = fun s -> - let (s',()) = x s in - y s' - - let map f x = fun s -> - on_snd f (x s) - - end) - -module Monad = - Monad.Make (struct - - type +'a t = evar_map -> 'a * evar_map - - let return a = fun s -> (a,s) - - let (>>=) x f = fun s -> - let (a,s') = x s in - f a s' - - let (>>) x y = fun s -> - let ((),s') = x s in - y s' - - let map f x = fun s -> - on_fst f (x s) - - end) - -(**********************************************************) -(* Failure explanation *) - -type unsolvability_explanation = SeveralInstancesFound of int - -(**********************************************************) -(* Pretty-printing *) - -let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma) - -let pr_instance_status (sc,typ) = - begin match sc with - | IsSubType -> str " [or a subtype of it]" - | IsSuperType -> str " [or a supertype of it]" - | Conv -> mt () - end ++ - begin match typ with - | CoerceToType -> str " [up to coercion]" - | TypeNotProcessed -> mt () - | TypeProcessed -> str " [type is checked]" - end - -let pr_meta_map mmap = - let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" - | _ -> mt() in - let pr_meta_binding = function - | (mv,Cltyp (na,b)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " : " ++ - print_constr b.rebus ++ fnl ()) - | (mv,Clval(na,(b,s),t)) -> - hov 0 - (pr_meta mv ++ pr_name na ++ str " := " ++ - print_constr b.rebus ++ - str " : " ++ print_constr t.rebus ++ - spc () ++ pr_instance_status s ++ fnl ()) - in - prlist pr_meta_binding (metamap_to_list mmap) - -let pr_decl ((id,b,_),ok) = - match b with - | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ - print_constr c ++ str (if ok then ")" else "}") - -let rec pr_evar_source = function - | Evar_kinds.QuestionMark _ -> str "underscore" - | Evar_kinds.CasesType false -> str "pattern-matching return predicate" - | Evar_kinds.CasesType true -> - str "subterm of pattern-matching return predicate" - | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id - | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" - | Evar_kinds.ImplicitArg (c,(n,ido),b) -> - let id = Option.get ido in - str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ - spc () ++ print_constr (printable_constr_of_global c) - | Evar_kinds.InternalHole -> str "internal placeholder" - | Evar_kinds.TomatchTypeParameter (ind,n) -> - pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind) - | Evar_kinds.GoalEvar -> str "goal evar" - | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" - | Evar_kinds.MatchingVar _ -> str "matching variable" - | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id - | Evar_kinds.SubEvar evk -> - str "subterm of " ++ str (string_of_existential evk) - -let pr_evar_info evi = - let phyps = - try - let decls = match Filter.repr (evar_filter evi) with - | None -> List.map (fun c -> (c, true)) (evar_context evi) - | Some filter -> List.combine (evar_context evi) filter - in - prlist_with_sep spc pr_decl (List.rev decls) - with Invalid_argument _ -> str "Ill-formed filtered context" in - let pty = print_constr evi.evar_concl in - let pb = - match evi.evar_body with - | Evar_empty -> mt () - | Evar_defined c -> spc() ++ str"=> " ++ print_constr c - in - let candidates = - match evi.evar_body, evi.evar_candidates with - | Evar_empty, Some l -> - spc () ++ str "{" ++ - prlist_with_sep (fun () -> str "|") print_constr l ++ str "}" - | _ -> - mt () - in - let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in - hov 2 - (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++ - candidates ++ spc() ++ src) - -let compute_evar_dependency_graph (sigma : evar_map) = - (* Compute the map binding ev to the evars whose body depends on ev *) - let fold evk evi acc = - let fold_ev evk' acc = - let tab = - try EvMap.find evk' acc - with Not_found -> Evar.Set.empty - in - EvMap.add evk' (Evar.Set.add evk tab) acc - in - match evar_body evi with - | Evar_empty -> assert false - | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc - in - EvMap.fold fold sigma.defn_evars EvMap.empty - -let evar_dependency_closure n sigma = - (** Create the DAG of depth [n] representing the recursive dependencies of - undefined evars. *) - let graph = compute_evar_dependency_graph sigma in - let rec aux n curr accu = - if Int.equal n 0 then Evar.Set.union curr accu - else - let fold evk accu = - try - let deps = EvMap.find evk graph in - Evar.Set.union deps accu - with Not_found -> accu - in - (** Consider only the newly added evars *) - let ncurr = Evar.Set.fold fold curr Evar.Set.empty in - (** Merge the others *) - let accu = Evar.Set.union curr accu in - aux (n - 1) ncurr accu - in - let undef = EvMap.domain (undefined_map sigma) in - aux n undef Evar.Set.empty - -let evar_dependency_closure n sigma = - let deps = evar_dependency_closure n sigma in - let map = EvMap.bind (fun ev -> find sigma ev) deps in - EvMap.bindings map - -let has_no_evar sigma = - EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars - -let pr_evd_level evd = pr_uctx_level evd.universes - -let pr_evar_universe_context ctx = - let prl = pr_uctx_level ctx in - if is_empty_evar_universe_context ctx then mt () - else - (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++ - str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++ - str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) - -let print_env_short env = - let pr_body n = function - | None -> pr_name n - | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in - let pr_named_decl (n, b, _) = pr_body (Name n) b in - let pr_rel_decl (n, b, _) = pr_body n b in - let nc = List.rev (named_context env) in - let rc = List.rev (rel_context env) in - str "[" ++ pr_sequence pr_named_decl nc ++ str "]" ++ spc () ++ - str "[" ++ pr_sequence pr_rel_decl rc ++ str "]" - -let pr_evar_constraints pbs = - let pr_evconstr (pbty, env, t1, t2) = - print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env t1 ++ spc () ++ - str (match pbty with - | Reduction.CONV -> "==" - | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env t2 - in - prlist_with_sep fnl pr_evconstr pbs - -let pr_evar_map_gen with_univs pr_evars sigma = - let { universes = uvs } = sigma in - let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl () - and svs = if with_univs then pr_evar_universe_context uvs else mt () - and cstrs = - if List.is_empty sigma.conv_pbs then mt () - else - str "CONSTRAINTS:" ++ brk (0, 1) ++ - pr_evar_constraints sigma.conv_pbs ++ fnl () - and metas = - if Metamap.is_empty sigma.metas then mt () - else - str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma.metas - in - evs ++ svs ++ cstrs ++ metas - -let pr_evar_list sigma l = - let pr (ev, evi) = - h 0 (str (string_of_existential ev) ++ - str "==" ++ pr_evar_info evi ++ - (if evi.evar_body == Evar_empty - then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}" - else mt ())) - in - h 0 (prlist_with_sep fnl pr l) - -let pr_evar_by_depth depth sigma = match depth with -| None -> - (* Print all evars *) - str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl() -| Some n -> - (* Print all evars *) - str"UNDEFINED EVARS:"++ - (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ - brk(0,1)++ - pr_evar_list sigma (evar_dependency_closure n sigma)++fnl() - -let pr_evar_by_filter filter sigma = - let defined = Evar.Map.filter filter sigma.defn_evars in - let undefined = Evar.Map.filter filter sigma.undf_evars in - let prdef = - if Evar.Map.is_empty defined then mt () - else str "DEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma (Evar.Map.bindings defined) - in - let prundef = - if Evar.Map.is_empty undefined then mt () - else str "UNDEFINED EVARS:" ++ brk (0, 1) ++ - pr_evar_list sigma (Evar.Map.bindings undefined) - in - prdef ++ prundef - -let pr_evar_map ?(with_univs=true) depth sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma - -let pr_evar_map_filter ?(with_univs=true) filter sigma = - pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma - -let pr_metaset metas = - str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]" diff --git a/pretyping/evd.mli b/pretyping/evd.mli deleted file mode 100644 index 9cfca02ed..000000000 --- a/pretyping/evd.mli +++ /dev/null @@ -1,622 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Loc -open Names -open Term -open Context -open Environ - -(** {5 Existential variables and unification states} - - A unification state (of type [evar_map]) is primarily a finite mapping - from existential variables to records containing the type of the evar - ([evar_concl]), the context under which it was introduced ([evar_hyps]) - and its definition ([evar_body]). [evar_extra] is used to add any other - kind of information. - - It also contains conversion constraints, debugging information and - information about meta variables. *) - -(** {6 Evars} *) - -type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) - -val string_of_existential : evar -> string - -(** {6 Evar filters} *) - -module Filter : -sig - type t - (** Evar filters, seen as bitmasks. *) - - val equal : t -> t -> bool - (** Equality over filters *) - - val identity : t - (** The identity filter. *) - - val filter_list : t -> 'a list -> 'a list - (** Filter a list. Sizes must coincide. *) - - val filter_array : t -> 'a array -> 'a array - (** Filter an array. Sizes must coincide. *) - - val extend : int -> t -> t - (** [extend n f] extends [f] on the left with [n]-th times [true]. *) - - val compose : t -> t -> t - (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where - [f1] is set. In particular, [f1] and [f2] must have the same length. *) - - val apply_subfilter : t -> bool list -> t - (** [apply_subfilter f1 f2] applies filter [f2] where [f1] is [true]. In - particular, the length of [f2] is the number of times [f1] is [true] *) - - val restrict_upon : t -> int -> (int -> bool) -> t option - (** Ad-hoc primitive. *) - - val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t - (** Apply the function on the filter and the list. Sizes must coincide. *) - - val make : bool list -> t - (** Create out of a list *) - - val repr : t -> bool list option - (** Observe as a bool list. *) - -end - -(** {6 Evar infos} *) - -type evar_body = - | Evar_empty - | Evar_defined of constr - - -module Store : Store.S -(** Datatype used to store additional information in evar maps. *) - -type evar_info = { - evar_concl : constr; - (** Type of the evar. *) - evar_hyps : named_context_val; - (** Context of the evar. *) - evar_body : evar_body; - (** Optional content of the evar. *) - evar_filter : Filter.t; - (** Boolean mask over {!evar_hyps}. Should have the same length. - TODO: document me more. *) - evar_source : Evar_kinds.t located; - (** Information about the evar. *) - evar_candidates : constr list option; - (** TODO: document this *) - evar_extra : Store.t - (** Extra store, used for clever hacks. *) -} - -val make_evar : named_context_val -> types -> evar_info -val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context -val evar_hyps : evar_info -> named_context_val -val evar_filtered_hyps : evar_info -> named_context_val -val evar_body : evar_info -> evar_body -val evar_filter : evar_info -> Filter.t -val evar_env : evar_info -> env -val evar_filtered_env : evar_info -> env - -val map_evar_body : (constr -> constr) -> evar_body -> evar_body -val map_evar_info : (constr -> constr) -> evar_info -> evar_info - -(** {6 Unification state} **) - -type evar_universe_context -(** The universe context associated to an evar map *) - -type evar_map -(** Type of unification state. Essentially a bunch of state-passing data needed - to handle incremental term construction. *) - -val empty : evar_map -(** The empty evar map. *) - -val from_env : env -> evar_map -(** The empty evar map with given universe context, taking its initial - universes from env. *) - -val from_ctx : evar_universe_context -> evar_map -(** The empty evar map with given universe context *) - -val is_empty : evar_map -> bool -(** Whether an evarmap is empty. *) - -val has_undefined : evar_map -> bool -(** [has_undefined sigma] is [true] if and only if - there are uninstantiated evars in [sigma]. *) - -val add : evar_map -> evar -> evar_info -> evar_map -(** [add sigma ev info] adds [ev] with evar info [info] in sigma. - Precondition: ev must not preexist in [sigma]. *) - -val find : evar_map -> evar -> evar_info -(** Recover the data associated to an evar. *) - -val find_undefined : evar_map -> evar -> evar_info -(** Same as {!find} but restricted to undefined evars. For efficiency - reasons. *) - -val remove : evar_map -> evar -> evar_map -(** Remove an evar from an evar map. Use with caution. *) - -val mem : evar_map -> evar -> bool -(** Whether an evar is present in an evarmap. *) - -val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a -(** Apply a function to all evars and their associated info in an evarmap. *) - -val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a -(** Same as {!fold}, but restricted to undefined evars. For efficiency - reasons. *) - -val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map -(** Apply the given function to all evars in the map. Beware: this function - expects the argument function to preserve the kind of [evar_body], i.e. it - must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some - [Evar_defined c']. *) - -val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map -(** Same as {!raw_map}, but restricted to undefined evars. For efficiency - reasons. *) - -val define : evar -> constr -> evar_map -> evar_map -(** Set the body of an evar to the given constr. It is expected that: - {ul - {- The evar is already present in the evarmap.} - {- The evar is not defined in the evarmap yet.} - {- All the evars present in the constr should be present in the evar map.} - } *) - -val cmap : (constr -> constr) -> evar_map -> evar_map -(** Map the function on all terms in the evar map. *) - -val is_evar : evar_map -> evar -> bool -(** Alias for {!mem}. *) - -val is_defined : evar_map -> evar -> bool -(** Whether an evar is defined in an evarmap. *) - -val is_undefined : evar_map -> evar -> bool -(** Whether an evar is not defined in an evarmap. *) - -val add_constraints : evar_map -> Univ.constraints -> evar_map -(** Add universe constraints in an evar map. *) - -val undefined_map : evar_map -> evar_info Evar.Map.t -(** Access the undefined evar mapping directly. *) - -val drop_all_defined : evar_map -> evar_map - -(** {6 Instantiating partial terms} *) - -exception NotInstantiatedEvar - -val existential_value : evar_map -> existential -> constr -(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has - no body and [Not_found] if it does not exist in [sigma] *) - -val existential_type : evar_map -> existential -> types - -val existential_opt_value : evar_map -> existential -> constr option -(** Same as {!existential_value} but returns an option instead of raising an - exception. *) - -val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> - 'a array -> (Id.t * 'a) list - -val instantiate_evar_array : evar_info -> constr -> constr array -> constr - -val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> - evar_map -> evar_map -> evar_map -(** spiwack: this function seems to somewhat break the abstraction. *) - -(** {6 Misc} *) - -val evar_declare : - named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map -(** Convenience function. Just a wrapper around {!add}. *) - -val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map -(** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) - -val downcast : evar -> types -> evar_map -> evar_map -(** Change the type of an undefined evar to a new type assumed to be a - subtype of its current type; subtyping must be ensured by caller *) - -val evar_source : existential_key -> evar_map -> Evar_kinds.t located -(** Convenience function. Wrapper around {!find} to recover the source of an - evar in a given evar map. *) - -val evar_ident : existential_key -> evar_map -> Id.t - -val rename : existential_key -> Id.t -> evar_map -> evar_map - -val evar_key : Id.t -> evar_map -> existential_key - -val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located - -val dependent_evar_ident : existential_key -> evar_map -> Id.t - -(** {5 Side-effects} *) - -val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map -(** Push a side-effect into the evar map. *) - -val eval_side_effects : evar_map -> Safe_typing.private_constants -(** Return the effects contained in the evar map. *) - -val drop_side_effects : evar_map -> evar_map -(** This should not be used. For hacking purposes. *) - -(** {5 Future goals} *) - -val declare_future_goal : Evar.t -> evar_map -> evar_map -(** Adds an existential variable to the list of future goals. For - internal uses only. *) - -val declare_principal_goal : Evar.t -> evar_map -> evar_map -(** Adds an existential variable to the list of future goals and make - it principal. Only one existential variable can be made principal, an - error is raised otherwise. For internal uses only. *) - -val future_goals : evar_map -> Evar.t list -(** Retrieves the list of future goals. Used by the [refine] primitive - of the tactic engine. *) - -val principal_future_goal : evar_map -> Evar.t option -(** Retrieves the name of the principal existential variable if there - is one. Used by the [refine] primitive of the tactic engine. *) - -val reset_future_goals : evar_map -> evar_map -(** Clears the list of future goals (as well as the principal future - goal). Used by the [refine] primitive of the tactic engine. *) - -val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map -(** Sets the future goals (including the principal future goal) to a - previous value. Intended to be used after a local list of future - goals has been consumed. Used by the [refine] primitive of the - tactic engine. *) - -(** {5 Sort variables} - - Evar maps also keep track of the universe constraints defined at a given - point. This section defines the relevant manipulation functions. *) - -val whd_sort_variable : evar_map -> constr -> constr - -exception UniversesDiffer - -val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map -(** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency -*) - -(** {5 Extra data} - - Evar maps can contain arbitrary data, allowing to use an extensible state. - As evar maps are theoretically used in a strict state-passing style, such - additional data should be passed along transparently. Some old and bug-prone - code tends to drop them nonetheless, so you should keep cautious. - -*) - -val get_extra_data : evar_map -> Store.t -val set_extra_data : Store.t -> evar_map -> evar_map - -(** {5 Enriching with evar maps} *) - -type 'a sigma = { - it : 'a ; - (** The base object. *) - sigma : evar_map - (** The added unification state. *) -} -(** The type constructor ['a sigma] adds an evar map to an object of type - ['a]. *) - -val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> evar_map -val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b - -(** {5 The state monad with state an evar map} *) - -module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a -module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map - - -(** {5 Meta machinery} - - These functions are almost deprecated. They were used before the - introduction of the full-fledged evar calculus. In an ideal world, they - should be removed. Alas, some parts of the code still use them. Do not use - in newly-written code. *) - -module Metaset : Set.S with type elt = metavariable -module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - -val metavars_of : constr -> Metaset.t -val mk_freelisted : constr -> constr freelisted -val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted - -(** Status of an instance found by unification wrt to the meta it solves: - - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - - a term that can be eta-expanded n times while still being a solution - (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) -*) - -type instance_constraint = IsSuperType | IsSubType | Conv - -val eq_instance_constraint : - instance_constraint -> instance_constraint -> bool - -(** Status of the unification of the type of an instance against the type of - the meta it instantiates: - - CoerceToType means that the unification of types has not been done - and that a coercion can still be inserted: the meta should not be - substituted freely (this happens for instance given via the - "with" binding clause). - - TypeProcessed means that the information obtainable from the - unification of types has been extracted. - - TypeNotProcessed means that the unification of types has not been - done but it is known that no coercion may be inserted: the meta - can be substituted freely. -*) - -type instance_typing_status = - CoerceToType | TypeNotProcessed | TypeProcessed - -(** Status of an instance together with the status of its type unification *) - -type instance_status = instance_constraint * instance_typing_status - -(** Clausal environments *) - -type clbinding = - | Cltyp of Name.t * constr freelisted - | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted - -(** Unification constraints *) -type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map - -val extract_changed_conv_pbs : evar_map -> - (Evar.Set.t -> evar_constraint -> bool) -> - evar_map * evar_constraint list -val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list -val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t - -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) - -val evar_list : constr -> existential list - (** excluding evars in instances of evars and collected with - redundancies from right to left (used by tactic "instantiate") *) - -val evars_of_term : constr -> Evar.Set.t - (** including evars in instances of evars *) - -val evars_of_named_context : named_context -> Evar.Set.t - -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t - -(** Metas *) -val meta_list : evar_map -> (metavariable * clbinding) list -val meta_defined : evar_map -> metavariable -> bool - -val meta_value : evar_map -> metavariable -> constr -(** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if - meta has no value *) - -val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status -val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option -val meta_type : evar_map -> metavariable -> types -val meta_ftype : evar_map -> metavariable -> types freelisted -val meta_name : evar_map -> metavariable -> Name.t -val meta_with_name : evar_map -> Id.t -> metavariable -val meta_declare : - metavariable -> types -> ?name:Name.t -> evar_map -> evar_map -val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map -val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map - -val clear_metas : evar_map -> evar_map - -(** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map - -val undefined_metas : evar_map -> metavariable list -val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map -val map_metas : (constr -> constr) -> evar_map -> evar_map - -type metabinding = metavariable * constr * instance_status - -val retract_coercible_metas : evar_map -> metabinding list * evar_map -val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option - -(** {5 FIXME: Nothing to do here} *) - -(********************************************************* - Sort/universe variables *) - -(** Rigid or flexible universe variables *) - -type rigid = - | UnivRigid - | UnivFlexible of bool (** Is substitution by an algebraic ok? *) - -val univ_rigid : rigid -val univ_flexible : rigid -val univ_flexible_alg : rigid - -type 'a in_evar_universe_context = 'a * evar_universe_context - -val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set -val evar_universe_context_constraints : evar_universe_context -> Univ.constraints -val evar_context_universe_context : evar_universe_context -> Univ.universe_context -val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context -val empty_evar_universe_context : evar_universe_context -val union_evar_universe_context : evar_universe_context -> evar_universe_context -> - evar_universe_context -val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst - -val evar_universe_context_of_binders : - Universes.universe_binders -> evar_universe_context - -val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context -val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map -(** Raises Not_found if not a name for a universe in this map. *) -val universe_of_name : evar_map -> string -> Univ.universe_level -val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map - -val universes : evar_map -> Univ.universes - -val add_constraints_context : evar_universe_context -> - Univ.constraints -> evar_universe_context - - -val normalize_evar_universe_context_variables : evar_universe_context -> - Univ.universe_subst in_evar_universe_context - -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context - -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts -val add_global_univ : evar_map -> Univ.Level.t -> evar_map - -val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map -val is_sort_variable : evar_map -> sorts -> Univ.universe_level option -(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is - not a local sort variable declared in [evm] *) -val is_flexible_level : evar_map -> Univ.Level.t -> bool - -val whd_sort_variable : evar_map -> constr -> constr -(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) -val normalize_universe : evar_map -> Univ.universe -> Univ.universe -val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance - -val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map -val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_eq_instances : ?flex:bool -> - evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map - -val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool -val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool - -val evar_universe_context : evar_map -> evar_universe_context -val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> - (Id.t * Univ.Level.t) list * Univ.universe_context -val universe_subst : evar_map -> Universes.universe_opt_subst -val universes : evar_map -> Univ.universes - - -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> evar_map - -val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map -val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map - -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a - -val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst -val abstract_undefined_variables : evar_universe_context -> evar_universe_context - -val fix_undefined_variables : evar_map -> evar_map - -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - -val nf_constraints : evar_map -> evar_map - -val update_sigma_env : evar_map -> env -> evar_map - -(** Polymorphic universes *) - -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor - -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> - Globnames.global_reference -> evar_map * constr - -(******************************************************************** - Conversion w.r.t. an evar map, not unifying universes. See - [Reductionops.infer_conv] for conversion up-to universes. *) - -val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** WARNING: This does not allow unification of universes *) - -val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool -(** Syntactic equality up to universes, recording the associated constraints *) - -val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool -(** Syntactic equality up to universes. *) - -(********************************************************************) -(* constr with holes and pending resolution of classes, conversion *) -(* problems, candidates, etc. *) - -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - -type open_constr = evar_map * constr (* Special case when before is empty *) - -(** Partially constructed constrs. *) - -type unsolvability_explanation = SeveralInstancesFound of int -(** Failure explanation. *) - -val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds - -(** {5 Debug pretty-printers} *) - -val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds -val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.std_ppcmds -val pr_metaset : Metaset.t -> Pp.std_ppcmds -val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds -val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds - -(** {5 Deprecated functions} *) - -val create_evar_defs : evar_map -> evar_map -(** Create an [evar_map] with empty meta map: *) - -val create_goal_evar_defs : evar_map -> evar_map diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index 28108f8ca..c741ab048 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -7,7 +7,6 @@ (************************************************************************) open Locus -open Context open Term open Evd open Pretype_errors @@ -50,7 +49,7 @@ val replace_term_occ_modulo : occurrences or_like_first -> val replace_term_occ_decl_modulo : (occurrences * hyp_location_flag) or_like_first -> 'a testing_function -> (unit -> constr) -> - named_declaration -> named_declaration + Context.Named.Declaration.t -> Context.Named.Declaration.t (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), @@ -62,7 +61,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> - constr -> named_declaration -> named_declaration * evar_map + constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map (** Miscellaneous *) val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0588dcc87..fb45be663 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -19,7 +19,6 @@ open Globnames open Nameops open Term open Vars -open Context open Namegen open Declarations open Declareops @@ -28,6 +27,7 @@ open Inductiveops open Environ open Reductionops open Nametab +open Sigma.Notations type dep_flag = bool @@ -60,7 +60,7 @@ let check_privacy_block mib = let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in - let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in + let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in let constrs = get_constructors env indf in let projs = get_projections env indf in @@ -91,8 +91,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let pbody = appvect (mkRel (ndepar + nbprod), - if dep then Termops.extended_rel_vect 0 deparsign - else Termops.extended_rel_vect 1 arsign) in + if dep then Context.Rel.to_extended_vect 0 deparsign + else Context.Rel.to_extended_vect 1 arsign) in let p = it_mkLambda_or_LetIn_name env' ((if dep then mkLambda_name env' else mkLambda) @@ -120,13 +120,14 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = mkLambda_string "f" t (add_branch (push_rel (Anonymous, None, t) env) (k+1)) in - let sigma, s = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind 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' dep indf s in let c = it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar - in sigma, c + in + Sigma (c, sigma, p) (* check if the type depends recursively on one of the inductive scheme *) @@ -163,7 +164,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let base = applist (lift i pk,realargs) in if depK then Reduction.beta_appvect - base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|] + base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|] else base | _ -> @@ -238,7 +239,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs - and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in + and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in applist(lift i fk,realargs@[arg]) | _ -> let t' = whd_betadeltaiota env sigma p in @@ -281,24 +282,13 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = in process_constr env 0 f (List.rev cstr.cs_args, recargs) - -(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k - variables *) -let context_chop k ctx = - let rec chop_aux acc = function - | (0, l2) -> (List.rev acc, l2) - | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) - | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) - | (_, []) -> failwith "context_chop" - in chop_aux [] (k,ctx) - (* Main function *) let mis_make_indrec env sigma listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in let lnonparrec,lnamesparrec = - context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in + Termops.context_chop (nparams-nparrec) (Vars.subst_instance_context u mib.mind_params_ctxt) in let nrec = List.length listdepkind in let depPvec = Array.make mib.mind_ntypes (None : (bool * constr) option) in @@ -327,29 +317,29 @@ let mis_make_indrec env sigma listdepkind mib u = (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) - let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in + let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in let indf = make_ind_family((indi,u),args) in let arsign,_ = get_arity env indf in let depind = build_dependent_inductive env indf in let deparsign = (Anonymous,None,depind)::arsign in - let nonrecpar = rel_context_length lnonparrec in - let larsign = rel_context_length deparsign in + let nonrecpar = Context.Rel.length lnonparrec in + let larsign = Context.Rel.length deparsign in let ndepar = larsign - nonrecpar in let dect = larsign+nrec+nbconstruct in (* constructors in context of the Cases expr, i.e. P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) - let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in - let args'' = Termops.extended_rel_list ndepar lnonparrec in + let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in + let args'' = Context.Rel.to_extended_list ndepar lnonparrec in let indf' = make_ind_family((indi,u),args'@args'') in let branches = let constrs = get_constructors env indf' in let fi = Termops.rel_vect (dect-i-nctyi) nctyi in let vecfi = Array.map - (fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec)) + (fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec)) fi in Array.map3 @@ -370,9 +360,9 @@ let mis_make_indrec env sigma listdepkind mib u = let deparsign' = (Anonymous,None,depind')::arsign' in let pargs = - let nrpar = Termops.extended_rel_list (2*ndepar) lnonparrec - and nrar = if dep then Termops.extended_rel_list 0 deparsign' - else Termops.extended_rel_list 1 arsign' + let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec + and nrar = if dep then Context.Rel.to_extended_list 0 deparsign' + else Context.Rel.to_extended_list 1 arsign' in nrpar@nrar in @@ -415,14 +405,14 @@ let mis_make_indrec env sigma listdepkind mib u = let typtyi = let concl = - let pargs = if dep then Termops.extended_rel_vect 0 deparsign - else Termops.extended_rel_vect 1 arsign + let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign + else Context.Rel.to_extended_vect 1 arsign in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs) in it_mkProd_or_LetIn_name env concl deparsign in - mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) + mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp) (deftyi::ldef) rest | [] -> let fixn = Array.of_list (List.rev ln) in @@ -443,7 +433,7 @@ let mis_make_indrec env sigma listdepkind mib u = else let recarg = (dest_subterms recargsvec.(tyi)).(j) in let recarg = recargpar@recarg in - let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in + let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in let p_0 = type_rec_branch @@ -457,7 +447,7 @@ let mis_make_indrec env sigma listdepkind mib u = in let rec put_arity env i = function | ((indi,u),_,_,dep,kinds)::rest -> - let indf = make_ind_family ((indi,u), Termops.extended_rel_list i lnamesparrec) in + let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list i lnamesparrec) in let s = Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) evdref kinds @@ -480,7 +470,9 @@ let mis_make_indrec env sigma listdepkind mib u = it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamesparrec else - let evd', c = mis_make_case_com dep env !evdref (indi,u) (mibi,mipi) kind in + 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 in (* Body of mis_make_indrec *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 4d81a59ef..f0736d2dd 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -25,13 +25,13 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) -val build_case_analysis_scheme : env -> evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * constr +val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> + dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma (** Build a dependent case elimination predicate unless type is in Prop *) -val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> - sorts_family -> evar_map * constr +val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> + sorts_family -> (constr, 'r) Sigma.sigma (** 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 fb180b8b7..bb38c72f2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Termops open Declarations open Declareops @@ -142,12 +141,12 @@ let constructor_nallargs_env env ((kn,i),j) = let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *) let (mib,mip) = Global.lookup_inductive indsp in - mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *) let mib = Environ.lookup_mind kn env in let mip = mib.mind_packets.(i) in - mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) (* Arity of constructors excluding params, excluding local defs *) @@ -213,21 +212,21 @@ let inductive_nparams_env env ind = let inductive_nparamdecls ind = let (mib,mip) = Global.lookup_inductive ind in - rel_context_length mib.mind_params_ctxt + Context.Rel.length mib.mind_params_ctxt let inductive_nparamdecls_env env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - rel_context_length mib.mind_params_ctxt + Context.Rel.length mib.mind_params_ctxt (* Full length of arity (with local defs) *) let inductive_nalldecls ind = let (mib,mip) = Global.lookup_inductive ind in - rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls + Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls let inductive_nalldecls_env env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in - rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls + Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls (* Others *) @@ -249,13 +248,13 @@ let inductive_alldecls_env env (ind,u) = let constructor_has_local_defs (indsp,j) = let (mib,mip) = Global.lookup_inductive indsp in - let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in + let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in not (Int.equal l1 l2) let inductive_has_local_defs ind = let (mib,mip) = Global.lookup_inductive ind in - let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in + let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) @@ -273,11 +272,11 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = - rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in + Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in let cstr_tags = Array.map2 (fun c n -> let d,_ = decompose_prod_assum c in - rel_context_tags (List.firstn n d)) + Context.Rel.to_tags (List.firstn n d)) mip.mind_nf_lc mip.mind_consnrealdecls in let print_info = { ind_tags; cstr_tags; style } in { ci_ind = ind; @@ -292,7 +291,7 @@ type constructor_summary = { cs_cstr : pconstructor; cs_params : constr list; cs_nargs : int; - cs_args : rel_context; + cs_args : Context.Rel.t; cs_concl_realargs : constr array } @@ -303,21 +302,15 @@ let lift_constructor n cs = { cs_args = lift_rel_context n cs.cs_args; cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs } -(* Accept less parameters than in the signature *) - -let instantiate_params t args sign = - let rec inst s t = function - | ((_,None,_)::ctxt,a::args) -> - (match kind_of_term t with - | Prod(_,_,t) -> inst (a::s) t (ctxt,args) - | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")) - | ((_,(Some b),_)::ctxt,args) -> - (match kind_of_term t with - | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args) - | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")) - | _, [] -> substl s t - | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") - in inst [] t (List.rev sign,args) + +(* Accept either all parameters or only recursively uniform ones *) +let instantiate_params t params sign = + let nnonrecpar = Context.Rel.nhyps sign - List.length params in + (* Adjust the signature if recursively non-uniform parameters are not here *) + let _,sign = context_chop nnonrecpar sign in + let _,t = decompose_prod_n_assum (Context.Rel.length sign) t in + let subst = subst_of_rel_context_instance sign params in + substl subst t let get_constructor ((ind,u as indu),mib,mip,params) j = assert (j <= Array.length mip.mind_consnames); @@ -329,7 +322,7 @@ let get_constructor ((ind,u as indu),mib,mip,params) j = let vargs = List.skipn (List.length params) allargs in { cs_cstr = (ith_constructor_of_inductive ind j,u); cs_params = params; - cs_nargs = rel_context_length args; + cs_nargs = Context.Rel.length args; cs_args = args; cs_concl_realargs = Array.of_list vargs } @@ -354,14 +347,6 @@ let substnl_rel_context subst n sign = let substl_rel_context subst = substnl_rel_context subst 0 -let instantiate_context sign args = - let rec aux subst = function - | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args) - | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args) - | [], [] -> subst - | _ -> anomaly (Pp.str "Signature/instance mismatch in inductive family") - in aux [] (List.rev sign,args) - let get_arity env ((ind,u),params) = let (mib,mip) = Inductive.lookup_mind_specif env ind in let parsign = @@ -379,7 +364,7 @@ let get_arity env ((ind,u),params) = let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in - let subst = instantiate_context parsign params in + let subst = subst_of_rel_context_instance parsign params in let arsign = Vars.subst_instance_context u arsign in (substl_rel_context subst arsign, Inductive.inductive_sort_family mip) @@ -388,14 +373,14 @@ let build_dependent_constructor cs = applist (mkConstructU cs.cs_cstr, (List.map (lift cs.cs_nargs) cs.cs_params) - @(extended_rel_list 0 cs.cs_args)) + @(Context.Rel.to_extended_list 0 cs.cs_args)) let build_dependent_inductive env ((ind, params) as indf) = let arsign,_ = get_arity env indf in let nrealargs = List.length arsign in applist (mkIndU ind, - (List.map (lift nrealargs) params)@(extended_rel_list 0 arsign)) + (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign)) (* builds the arity of an elimination predicate in sort [s] *) @@ -430,12 +415,15 @@ let extract_mrectype t = | Ind ind -> (ind, l) | _ -> raise Not_found -let find_mrectype env sigma c = - let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in +let find_mrectype_vect env sigma c = + let (t, l) = decompose_appvect (whd_betadeltaiota env sigma c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found +let find_mrectype env sigma c = + let (ind, v) = find_mrectype_vect env sigma c in (ind, Array.to_list v) + let find_rectype env sigma c = let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in match kind_of_term t with @@ -517,7 +505,7 @@ let set_pattern_names env ind brv = let arities = Array.map (fun c -> - rel_context_length ((prod_assum c)) - + Context.Rel.length ((prod_assum c)) - mib.mind_nparams) mip.mind_nf_lc in Array.map2 (set_names env) arities brv @@ -529,7 +517,7 @@ let type_case_branches_with_names env indspec p c = let (params,realargs) = List.chop nparams args in let lbrty = Inductive.build_branches_type ind specif params p in (* Build case type *) - let conclty = Reduction.betazeta_appvect (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in + let conclty = lambda_appvect_assum (mip.mind_nrealdecls+1) p (Array.of_list (realargs@[c])) in (* Adjust names *) if is_elim_predicate_explicitly_dependent env p (ind,params) then (set_pattern_names env (fst ind) lbrty, conclty) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7cd2ff2af..d25f8a837 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Environ open Evd @@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> rel_context -val inductive_paramdecls_env : env -> pinductive -> rel_context +val inductive_paramdecls : pinductive -> Context.Rel.t +val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> rel_context -val inductive_alldecls_env : env -> pinductive -> rel_context +val inductive_alldecls : pinductive -> Context.Rel.t +val inductive_alldecls_env : env -> pinductive -> Context.Rel.t (** {7 Extract information from a constructor name} *) @@ -133,9 +132,9 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) - cs_params : constr list; (* parameters of the constructor in current ctx *) - cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : rel_context; (* signature of the arguments (letin included) *) + cs_params : constr list; (* parameters of the constructor in current ctx *) + cs_nargs : int; (* length of arguments signature (letin included) *) + cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -148,17 +147,18 @@ val get_projections : env -> inductive_family -> constant array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> rel_context * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> rel_context +val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : constr -> pinductive * constr list val find_mrectype : env -> evar_map -> types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array val find_rectype : env -> evar_map -> types -> inductive_type val find_inductive : env -> evar_map -> types -> pinductive * constr list val find_coinductive : env -> evar_map -> types -> pinductive * constr list diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml deleted file mode 100644 index fc3f0cc75..000000000 --- a/pretyping/namegen.ml +++ /dev/null @@ -1,395 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Created from contents that was formerly in termops.ml and - nameops.ml, Nov 2009 *) - -(* This file is about generating new or fresh names and dealing with - alpha-renaming *) - -open Util -open Names -open Term -open Vars -open Nametab -open Nameops -open Libnames -open Globnames -open Environ -open Termops - -(**********************************************************************) -(* Conventional names *) - -let default_prop_string = "H" -let default_prop_ident = Id.of_string default_prop_string - -let default_small_string = "H" -let default_small_ident = Id.of_string default_small_string - -let default_type_string = "X" -let default_type_ident = Id.of_string default_type_string - -let default_non_dependent_string = "H" -let default_non_dependent_ident = Id.of_string default_non_dependent_string - -let default_dependent_ident = Id.of_string "x" - -(**********************************************************************) -(* Globality of identifiers *) - -let is_imported_modpath = function - | MPfile dp -> - let rec find_prefix = function - |MPfile dp1 -> not (DirPath.equal dp1 dp) - |MPdot(mp,_) -> find_prefix mp - |MPbound(_) -> false - in find_prefix (Lib.current_mp ()) - | _ -> false - -let is_imported_ref = function - | VarRef _ -> false - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> - let (mp,_,_) = repr_mind kn in is_imported_modpath mp - | ConstRef kn -> - let (mp,_,_) = repr_con kn in is_imported_modpath mp - -let is_global id = - try - let ref = locate (qualid_of_ident id) in - not (is_imported_ref ref) - with Not_found -> - false - -let is_constructor id = - try - match locate (qualid_of_ident id) with - | ConstructRef _ -> true - | _ -> false - with Not_found -> - false - -(**********************************************************************) -(* Generating "intuitive" names from its type *) - -let head_name c = (* Find the head constant of a constr if any *) - let rec hdrec c = - match kind_of_term c with - | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) - | Cast (c,_,_) | App (c,_) -> hdrec c - | Proj (kn,_) -> Some (Label.to_id (con_label (Projection.constant kn))) - | Const _ | Ind _ | Construct _ | Var _ -> - Some (basename_of_global (global_of_constr c)) - | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> - Some (match lna.(i) with Name id -> id | _ -> assert false) - | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None - in - hdrec c - -let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) - -let sort_hdchar = function - | Prop(_) -> "P" - | Type(_) -> "T" - -let hdchar env c = - let rec hdrec k c = - match kind_of_term c with - | Prod (_,_,c) | Lambda (_,_,c) | LetIn (_,_,_,c) -> hdrec (k+1) c - | Cast (c,_,_) | App (c,_) -> hdrec k c - | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) - | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) - | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) - | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) - | Var id -> lowercase_first_char id - | Sort s -> sort_hdchar s - | Rel n -> - (if n<=k then "p" (* the initial term is flexible product/function *) - else - try match Environ.lookup_rel (n-k) env with - | (Name id,_,_) -> lowercase_first_char id - | (Anonymous,_,t) -> hdrec 0 (lift (n-k) t) - with Not_found -> "y") - | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> - let id = match lna.(i) with Name id -> id | _ -> assert false in - lowercase_first_char id - | Evar _ (* We could do better... *) - | Meta _ | Case (_, _, _, _) -> "y" - in - hdrec 0 c - -let id_of_name_using_hdchar env a = function - | Anonymous -> Id.of_string (hdchar env a) - | Name id -> id - -let named_hd env a = function - | Anonymous -> Name (Id.of_string (hdchar env a)) - | x -> x - -let mkProd_name env (n,a,b) = mkProd (named_hd env a n, a, b) -let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b) - -let lambda_name = mkLambda_name -let prod_name = mkProd_name - -let prod_create env (a,b) = mkProd (named_hd env a Anonymous, a, b) -let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous, a, b) - -let name_assumption env (na,c,t) = - match c with - | None -> (named_hd env t na, None, t) - | Some body -> (named_hd env body na, c, t) - -let name_context env hyps = - snd - (List.fold_left - (fun (env,hyps) d -> - let d' = name_assumption env d in (push_rel d' env, d' :: hyps)) - (env,[]) (List.rev hyps)) - -let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b -let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b - -let it_mkProd_or_LetIn_name env b hyps = - it_mkProd_or_LetIn b (name_context env hyps) -let it_mkLambda_or_LetIn_name env b hyps = - it_mkLambda_or_LetIn b (name_context env hyps) - -(**********************************************************************) -(* Fresh names *) - -(* Looks for next "good" name by lifting subscript *) - -let next_ident_away_from id bad = - let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in - name_rec id - -(* Restart subscript from x0 if name starts with xN, or x00 if name - starts with x0N, etc *) - -let restart_subscript id = - if not (has_subscript id) then id else - (* It would probably be better with something in the spirit of - *** make_ident id (Some 0) *** but compatibility would be lost... *) - forget_subscript id - -let rec to_avoid id = function -| [] -> false -| id' :: avoid -> Id.equal id id' || to_avoid id avoid - -let occur_rel p env id = - try - let name = lookup_name_of_rel p env in - begin match name with - | Name id' -> Id.equal id' id - | Anonymous -> false - end - with Not_found -> false (* Unbound indice : may happen in debug *) - -let visibly_occur_id id (nenv,c) = - let rec occur n c = match kind_of_term c with - | Const _ | Ind _ | Construct _ | Var _ - when - let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in - qualid_eq short (qualid_of_ident id) -> - raise Occur - | Rel p when p>n && occur_rel (p-n) nenv id -> raise Occur - | _ -> iter_constr_with_binders succ occur n c - in - try occur 1 c; false - with Occur -> true - | Not_found -> false (* Happens when a global is not in the env *) - -(* Now, there are different renaming strategies... *) - -(* 1- Looks for a fresh name for printing in cases pattern *) - -let next_name_away_in_cases_pattern env_t na avoid = - let id = match na with Name id -> id | Anonymous -> default_dependent_ident in - let bad id = to_avoid id avoid || is_constructor id - || visibly_occur_id id env_t in - next_ident_away_from id bad - -(* 2- Looks for a fresh name for introduction in goal *) - -(* The legacy strategy for renaming introduction variables is not very uniform: - - if the name to use is fresh in the context but used as a global - name, then a fresh name is taken by finding a free subscript - starting from the current subscript; - - but if the name to use is not fresh in the current context, the fresh - name is taken by finding a free subscript starting from 0 *) - -let next_ident_away_in_goal id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || (is_global id && not (is_section_variable id)) in - next_ident_away_from id bad - -let next_name_away_in_goal na avoid = - let id = match na with - | Name id -> id - | Anonymous -> default_non_dependent_ident in - next_ident_away_in_goal id avoid - -(* 3- Looks for next fresh name outside a list that is moreover valid - as a global identifier; the legacy algorithm is that if the name is - already used in the list, one looks for a name of same base with - lower available subscript; if the name is not in the list but is - used globally, one looks for a name of same base with lower subscript - beyond the current subscript *) - -let next_global_ident_away id avoid = - let id = if to_avoid id avoid then restart_subscript id else id in - let bad id = to_avoid id avoid || is_global id in - next_ident_away_from id bad - -(* 4- Looks for next fresh name outside a list; if name already used, - looks for same name with lower available subscript *) - -let next_ident_away id avoid = - if to_avoid id avoid then - next_ident_away_from (restart_subscript id) (fun id -> to_avoid id avoid) - else id - -let next_name_away_with_default default na avoid = - let id = match na with Name id -> id | Anonymous -> Id.of_string default in - next_ident_away id avoid - -let reserved_type_name = ref (fun t -> Anonymous) -let set_reserved_typed_name f = reserved_type_name := f - -let next_name_away_with_default_using_types default na avoid t = - let id = match na with - | Name id -> id - | Anonymous -> match !reserved_type_name t with - | Name id -> id - | Anonymous -> Id.of_string default in - next_ident_away id avoid - -let next_name_away = next_name_away_with_default default_non_dependent_string - -let make_all_name_different env = - let avoid = ref (ids_of_named_context (named_context env)) in - process_rel_context - (fun (na,c,t) newenv -> - let na = named_hd newenv t na in - let id = next_name_away na !avoid in - avoid := id::!avoid; - push_rel (Name id,c,t) newenv) - env - -(* 5- Looks for next fresh name outside a list; avoids also to use names that - would clash with short name of global references; if name is already used, - looks for name of same base with lower available subscript beyond current - subscript *) - -let next_ident_away_for_default_printing env_t id avoid = - let bad id = to_avoid id avoid || visibly_occur_id id env_t in - next_ident_away_from id bad - -let next_name_away_for_default_printing env_t na avoid = - let id = match na with - | Name id -> id - | Anonymous -> - (* In principle, an anonymous name is not dependent and will not be *) - (* taken into account by the function compute_displayed_name_in; *) - (* just in case, invent a valid name *) - default_non_dependent_ident in - next_ident_away_for_default_printing env_t id avoid - -(**********************************************************************) -(* Displaying terms avoiding bound variables clashes *) - -(* Renaming strategy introduced in December 1998: - - - Rule number 1: all names, even if unbound and not displayed, contribute - to the list of names to avoid - - Rule number 2: only the dependency status is used for deciding if - a name is displayed or not - - Example: - bool_ind: "forall (P:bool->Prop)(f:(P true))(f:(P false))(b:bool), P b" is - displayed "forall P:bool->Prop, P true -> P false -> forall b:bool, P b" - but f and f0 contribute to the list of variables to avoid (knowing - that f and f0 are how the f's would be named if introduced, assuming - no other f and f0 are already used). -*) - -type renaming_flags = - | RenamingForCasesPattern of (Name.t list * constr) - | RenamingForGoal - | RenamingElsewhereFor of (Name.t list * constr) - -let next_name_for_display flags = - match flags with - | RenamingForCasesPattern env_t -> next_name_away_in_cases_pattern env_t - | RenamingForGoal -> next_name_away_in_goal - | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t - -(* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in flags avoid na c = - match na with - | Anonymous when noccurn 1 c -> - (Anonymous,avoid) - | _ -> - let fresh_id = next_name_for_display flags na avoid in - let idopt = if noccurn 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::avoid) - -let compute_and_force_displayed_name_in flags avoid na c = - match na with - | Anonymous when noccurn 1 c -> - (Anonymous,avoid) - | _ -> - let fresh_id = next_name_for_display flags na avoid in - (Name fresh_id, fresh_id::avoid) - -let compute_displayed_let_name_in flags avoid na c = - let fresh_id = next_name_for_display flags na avoid in - (Name fresh_id, fresh_id::avoid) - -let rename_bound_vars_as_displayed avoid env c = - let rec rename avoid env c = - match kind_of_term c with - | Prod (na,c1,c2) -> - let na',avoid' = - compute_displayed_name_in - (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkProd (na', c1, rename avoid' (add_name na' env) c2) - | LetIn (na,c1,t,c2) -> - let na',avoid' = - compute_displayed_let_name_in - (RenamingElsewhereFor (env,c2)) avoid na c2 in - mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2) - | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) - | _ -> c - in - rename avoid env c - -(**********************************************************************) -(* "H"-based naming strategy introduced June 2014 for hypotheses in - Prop produced by case/elim/destruct/induction, in place of the - strategy that was using the first letter of the type, leading to - inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar - types *) - -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = - !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 - -open Goptions - -let _ = declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli deleted file mode 100644 index 6751bd3cf..000000000 --- a/pretyping/namegen.mli +++ /dev/null @@ -1,102 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Context -open Environ - -(********************************************************************* - Conventional default names *) - -val default_prop_ident : Id.t (* "H" *) -val default_small_ident : Id.t (* "H" *) -val default_type_ident : Id.t (* "X" *) -val default_non_dependent_ident : Id.t (* "H" *) -val default_dependent_ident : Id.t (* "x" *) - -(********************************************************************* - Generating "intuitive" names from their type *) - -val lowercase_first_char : Id.t -> string -val sort_hdchar : sorts -> string -val hdchar : env -> types -> string -val id_of_name_using_hdchar : env -> types -> Name.t -> Id.t -val named_hd : env -> types -> Name.t -> Name.t -val head_name : types -> Id.t option - -val mkProd_name : env -> Name.t * types * types -> types -val mkLambda_name : env -> Name.t * types * constr -> constr - -(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) -val prod_name : env -> Name.t * types * types -> types -val lambda_name : env -> Name.t * types * constr -> constr - -val prod_create : env -> types * types -> constr -val lambda_create : env -> types * constr -> constr -val name_assumption : env -> rel_declaration -> rel_declaration -val name_context : env -> rel_context -> rel_context - -val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types -val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr -val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types -val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr - -(********************************************************************* - Fresh names *) - -(** Avoid clashing with a name satisfying some predicate *) -val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t - -(** Avoid clashing with a name of the given list *) -val next_ident_away : Id.t -> Id.t list -> Id.t - -(** Avoid clashing with a name already used in current module *) -val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t - -(** Avoid clashing with a name already used in current module - but tolerate overwriting section variables, as in goals *) -val next_global_ident_away : Id.t -> Id.t list -> Id.t - -(** Avoid clashing with a constructor name already used in current module *) -val next_name_away_in_cases_pattern : (Termops.names_context * constr) -> Name.t -> Id.t list -> Id.t - -(** Default is [default_non_dependent_ident] *) -val next_name_away : Name.t -> Id.t list -> Id.t - -val next_name_away_with_default : string -> Name.t -> Id.t list -> - Id.t - -val next_name_away_with_default_using_types : string -> Name.t -> - Id.t list -> types -> Id.t - -val set_reserved_typed_name : (types -> Name.t) -> unit - -(********************************************************************* - Making name distinct for displaying *) - -type renaming_flags = - | RenamingForCasesPattern of (Name.t list * constr) (** avoid only global constructors *) - | RenamingForGoal (** avoid all globals (as in intro) *) - | RenamingElsewhereFor of (Name.t list * constr) - -val make_all_name_different : env -> env - -val compute_displayed_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list -val compute_and_force_displayed_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list -val compute_displayed_let_name_in : - renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list -val rename_bound_vars_as_displayed : - Id.t list -> Name.t list -> types -> types - -(**********************************************************************) -(* Naming strategy for arguments in Prop when eliminating inductive types *) - -val use_h_based_elimination_names : unit -> bool diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index bbda55f48..0b1ce8e51 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -8,7 +8,6 @@ open Term open Environ open Evd -open Nativelambda (** This module implements normalization by evaluation to OCaml code *) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 5f877814d..1f63565d6 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context open Term open Globnames open Glob_term diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b33084a42..11fba7b94 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -28,7 +28,6 @@ open Names open Evd open Term open Vars -open Context open Termops open Reductionops open Environ @@ -47,7 +46,7 @@ open Misctypes 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 = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; @@ -95,10 +94,6 @@ let search_guard loc env possible_indexes fixdefs = 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,7 +129,7 @@ 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 @@ -321,7 +316,7 @@ 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 @@ -454,26 +449,12 @@ let new_type_evar env evdref loc = 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 (f_genarg_interp, genarg_interp_hook) = Hook.make () (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* 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 inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in let pretype_type = pretype_type k0 resolve_tc in @@ -539,14 +520,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ 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 + 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 + 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 -> @@ -573,7 +554,7 @@ 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 @@ -894,7 +875,7 @@ 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 = @@ -1027,7 +1008,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function let ise_pretype_gen flags env sigma lvar kind c = 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 @@ -1069,7 +1050,7 @@ let on_judgment f j = let understand_judgment env sigma c = 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 @@ -1077,7 +1058,7 @@ let understand_judgment env sigma c = in j, Evd.evar_universe_context !evdref let understand_judgment_tcc env evdref c = - 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 on_judgment (fun c -> let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index ac899a786..bfb4e7325 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.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 = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; @@ -148,12 +148,9 @@ val ise_pretype_gen : (** To embed constr in glob_constr *) -val constr_in : constr -> Dyn.t -val constr_out : Dyn.t -> constr - val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t -> + (types -> env -> evar_map -> unbound_ltac_var_map -> Genarg.glob_generic_argument -> constr * evar_map) Hook.t diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index a644e3d10..b59589bda 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,7 +1,4 @@ Locusops -Termops -Namegen -Evd Reductionops Inductiveops Vnorm diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 560beb6f1..6499ddd53 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -299,7 +299,7 @@ let check_and_decompose_canonical_structure ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in + let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 13b7fb407..5e21154a6 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -11,7 +11,6 @@ open Util open Names open Term open Vars -open Context open Termops open Univ open Evd @@ -1256,28 +1255,26 @@ let report_anomaly _ = let e = Errors.push e in iraise e -let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = +let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in - let _ = f ~evars reds env (Evd.universes sigma) x y in + let _ = f ~reds env ~evars:(evars, Evd.universes sigma) x y in true with Reduction.NotConvertible -> false | e when is_anomaly e -> report_anomaly e -let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma -let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma -let is_trans_fconv = function Reduction.CONV -> is_trans_conv | Reduction.CUMUL -> is_trans_conv_leq - -let is_conv = is_trans_conv full_transparent_state -let is_conv_leq = is_trans_conv_leq full_transparent_state -let is_fconv = function | Reduction.CONV -> is_conv | Reduction.CUMUL -> is_conv_leq +let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv reds env sigma +let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion Reduction.conv_leq reds env sigma +let is_fconv ?(reds=full_transparent_state) = function + | Reduction.CONV -> is_conv ~reds + | Reduction.CUMUL -> is_conv_leq ~reds let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = let f = match pb with - | Reduction.CONV -> Reduction.trans_conv_universes - | Reduction.CUMUL -> Reduction.trans_conv_leq_universes + | Reduction.CONV -> Reduction.conv + | Reduction.CUMUL -> Reduction.conv_leq in - try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true + try f ~reds:ts env ~evars:(safe_evar_value sigma, Evd.universes sigma) x y; true with Reduction.NotConvertible -> false | Univ.UniverseInconsistency _ -> false | e when is_anomaly e -> report_anomaly e @@ -1299,18 +1296,21 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = - try + try + let fold cstr sigma = + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None + in let b, sigma = - let b, cstrs = + let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) x y + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma else - Universes.eq_constr_univs_infer (Evd.universes sigma) x y + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma in - if b then - try true, Evd.add_universe_constraints sigma cstrs - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> false, sigma - else false, sigma + match ans with + | None -> false, sigma + | Some sigma -> true, sigma in if b then sigma, true else @@ -1465,17 +1465,17 @@ let splay_prod_assum env sigma = match kind_of_term t with | Prod (x,t,c) -> prodec_rec (push_rel (x,None,t) env) - (add_rel_decl (x, None, t) l) c + (Context.Rel.add (x, None, t) l) c | LetIn (x,b,t,c) -> prodec_rec (push_rel (x, Some b, t) env) - (add_rel_decl (x, Some b, t) l) c + (Context.Rel.add (x, Some b, t) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let t' = whd_betadeltaiota env sigma t in if Term.eq_constr t t' then l,t else prodec_rec env l t' in - prodec_rec env empty_rel_context + prodec_rec env Context.Rel.empty let splay_arity env sigma c = let l, c = splay_prod env sigma c in @@ -1490,20 +1490,20 @@ let splay_prod_n env sigma n = match kind_of_term (whd_betadeltaiota env sigma c) with | Prod (n,a,c0) -> decrec (push_rel (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + (m-1) (Context.Rel.add (n,None,a) ln) c0 | _ -> invalid_arg "splay_prod_n" in - decrec env n empty_rel_context + decrec env n Context.Rel.empty let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match kind_of_term (whd_betadeltaiota env sigma c) with | Lambda (n,a,c0) -> decrec (push_rel (n,None,a) env) - (m-1) (add_rel_decl (n,None,a) ln) c0 + (m-1) (Context.Rel.add (n,None,a) ln) c0 | _ -> invalid_arg "splay_lam_n" in - decrec env n empty_rel_context + decrec env n Context.Rel.empty let is_sort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index aea0a9ae2..e65ab83b2 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Univ open Evd open Environ @@ -218,11 +217,10 @@ val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts -val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr +val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr -val is_sort : env -> evar_map -> types -> bool + env -> evar_map -> constr -> Context.Rel.t * constr type 'a miota_args = { mP : constr; (** the result type *) @@ -251,13 +249,9 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val is_conv : env -> evar_map -> constr -> constr -> bool -val is_conv_leq : env -> evar_map -> constr -> constr -> bool -val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool - -val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool -val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool +val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool (** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 37cec0c63..e4cca2679 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -8,7 +8,6 @@ open Term open Evd -open Context open Environ (** This family of functions assumes its constr argument is known to be @@ -44,6 +43,6 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> rel_context -> sorts list +val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7c4f28cac..bd46911c9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -940,8 +940,6 @@ let matches_head env sigma c t = | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p)) | _ -> raise Constr_matching.PatternMatchingFailure -let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false - (** FIXME: Specific function to handle projections: it ignores what happens on the parameters. This is a temporary fix while rewrite etc... are not up to equivalence of the projection and its eta expanded form. @@ -1055,10 +1053,6 @@ let unfold env sigma name = else error (string_of_evaluable_ref env name^" is opaque.") -let is_projection env = function - | EvalVarRef _ -> false - | EvalConstRef c -> Environ.is_projection c env - (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences. diff --git a/pretyping/termops.ml b/pretyping/termops.ml deleted file mode 100644 index 9d469cb71..000000000 --- a/pretyping/termops.ml +++ /dev/null @@ -1,1026 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Errors -open Util -open Names -open Nameops -open Term -open Vars -open Context -open Environ - -(* Sorts and sort family *) - -let print_sort = function - | Prop Pos -> (str "Set") - | Prop Null -> (str "Prop") - | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") - -let pr_sort_family = function - | InSet -> (str "Set") - | InProp -> (str "Prop") - | InType -> (str "Type") - -let pr_name = function - | Name id -> pr_id id - | Anonymous -> str "_" - -let pr_con sp = str(string_of_con sp) - -let pr_fix pr_constr ((t,i),(lna,tl,bl)) = - let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in - hov 1 - (str"fix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -let pr_puniverses p u = - if Univ.Instance.is_empty u then p - else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)" - -let rec pr_constr c = match kind_of_term c with - | Rel n -> str "#"++int n - | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> pr_id id - | Sort s -> print_sort s - | Cast (c,_, t) -> hov 1 - (str"(" ++ pr_constr c ++ cut() ++ - str":" ++ pr_constr t ++ str")") - | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++ - spc() ++ pr_constr c) - | Prod (Anonymous,t,c) -> hov 0 - (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ - pr_constr c ++ str")") - | Lambda (na,t,c) -> hov 1 - (str"fun " ++ pr_name na ++ str":" ++ - pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) - | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ - str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ - pr_constr c) - | App (c,l) -> hov 1 - (str"(" ++ pr_constr c ++ spc() ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") - | Evar (e,l) -> hov 1 - (str"Evar#" ++ int (Evar.repr e) ++ str"{" ++ - prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") - | Const (c,u) -> str"Cst(" ++ pr_puniverses (pr_con c) u ++ str")" - | Ind ((sp,i),u) -> str"Ind(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i) u ++ str")" - | Construct (((sp,i),j),u) -> - str"Constr(" ++ pr_puniverses (pr_mind sp ++ str"," ++ int i ++ str"," ++ int j) u ++ str")" - | Proj (p,c) -> str"Proj(" ++ pr_con (Projection.constant p) ++ str"," ++ bool (Projection.unfolded p) ++ pr_constr c ++ str")" - | Case (ci,p,c,bl) -> v 0 - (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ - pr_constr c ++ str"of") ++ cut() ++ - prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++ - cut() ++ str"end") - | Fix f -> pr_fix pr_constr f - | CoFix(i,(lna,tl,bl)) -> - let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in - hov 1 - (str"cofix " ++ int i ++ spc() ++ str"{" ++ - v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ pr_constr ty ++ - cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ - str"}") - -let term_printer = ref (fun _ -> pr_constr) -let print_constr_env t = !term_printer t -let print_constr t = !term_printer (Global.env()) t -let set_print_constr f = term_printer := f - -let pr_var_decl env (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> - (* Force evaluation *) - let pb = print_constr_env env c in - (str" := " ++ pb ++ cut () ) in - let pt = print_constr_env env typ in - let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) - -let pr_rel_decl env (na,c,typ) = - let pbody = match c with - | None -> mt () - | Some c -> - (* Force evaluation *) - let pb = print_constr_env env c in - (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = print_constr_env env typ in - match na with - | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - -let print_named_context env = - hv 0 (fold_named_context - (fun env d pps -> - pps ++ ws 2 ++ pr_var_decl env d) - env ~init:(mt ())) - -let print_rel_context env = - hv 0 (fold_rel_context - (fun env d pps -> pps ++ ws 2 ++ pr_rel_decl env d) - env ~init:(mt ())) - -let print_env env = - let sign_env = - fold_named_context - (fun env d pps -> - let pidt = pr_var_decl env d in - (pps ++ fnl () ++ pidt)) - env ~init:(mt ()) - in - let db_env = - fold_rel_context - (fun env d pps -> - let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) - env ~init:(mt ()) - in - (sign_env ++ db_env) - -(* [Rel (n+m);...;Rel(n+1)] *) -let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) - -let rel_list n m = - let rec reln l p = - if p>m then l else reln (mkRel(n+p)::l) (p+1) - in - reln [] 1 - -(* Same as [rel_list] but takes a context as argument and skips let-ins *) -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - -let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps) - - - -let push_rel_assum (x,t) env = push_rel (x,None,t) env - -let push_rels_assum assums = - push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums) - -let push_named_rec_types (lna,typarray,_) env = - let ctxt = - Array.map2_i - (fun i na t -> - match na with - | Name id -> (id, None, lift i t) - | Anonymous -> anomaly (Pp.str "Fix declarations must be named")) - lna typarray in - Array.fold_left - (fun e assum -> push_named assum e) env ctxt - -let lookup_rel_id id sign = - let rec lookrec n = function - | [] -> raise Not_found - | (Anonymous, _, _) :: l -> lookrec (n + 1) l - | (Name id', b, t) :: l -> - if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l - in - lookrec 1 sign - -(* Constructs either [forall x:t, c] or [let x:=b:t in c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> mkLetIn (na, b, t, c) - -(* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *) -let mkProd_wo_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c - -let it_mkProd init = List.fold_left (fun c (n,t) -> mkProd (n, t, c)) init -let it_mkLambda init = List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) init - -let it_named_context_quantifier f ~init = - List.fold_left (fun c d -> f d c) init - -let it_mkProd_or_LetIn init = it_named_context_quantifier mkProd_or_LetIn ~init -let it_mkProd_wo_LetIn init = it_named_context_quantifier mkProd_wo_LetIn ~init -let it_mkLambda_or_LetIn init = it_named_context_quantifier mkLambda_or_LetIn ~init -let it_mkNamedProd_or_LetIn init = it_named_context_quantifier mkNamedProd_or_LetIn ~init -let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_LetIn ~init -let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init - -let it_mkLambda_or_LetIn_from_no_LetIn c decls = - let rec aux k decls c = match decls with - | [] -> c - | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c)) - | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c) - in aux (List.length decls) (List.rev decls) c - -(* *) - -(* strips head casts and flattens head applications *) -let rec strip_head_cast c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2) - in - collapse_rec f cl - | Cast (c,_,_) -> strip_head_cast c - | _ -> c - -let rec drop_extra_implicit_args c = match kind_of_term c with - (* Removed trailing extra implicit arguments, what improves compatibility - for constants with recently added maximal implicit arguments *) - | App (f,args) when isEvar (Array.last args) -> - drop_extra_implicit_args - (mkApp (f,fst (Array.chop (Array.length args - 1) args))) - | _ -> c - -(* Get the last arg of an application *) -let last_arg c = match kind_of_term c with - | App (f,cl) -> Array.last cl - | _ -> anomaly (Pp.str "last_arg") - -(* Get the last arg of an application *) -let decompose_app_vect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) - -let adjust_app_list_size f1 l1 f2 l2 = - let len1 = List.length l1 and len2 = List.length l2 in - if Int.equal len1 len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = List.chop (len2-len1) l2 in - (f1, l1, applist (f2,extras), restl2) - else - let extras,restl1 = List.chop (len1-len2) l1 in - (applist (f1,extras), restl1, f2, l2) - -let adjust_app_array_size f1 l1 f2 l2 = - let len1 = Array.length l1 and len2 = Array.length l2 in - if Int.equal len1 len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = Array.chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) - else - let extras,restl1 = Array.chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) - -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) - -let map_constr_with_named_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (c,k,t) -> mkCast (f l c, k, f l t) - | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c) - | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) - | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) - | App (c,al) -> mkApp (f l c, Array.map (f l) al) - | Proj (p,c) -> mkProj (p, f l c) - | Evar (e,al) -> mkEvar (e, Array.map (f l) al) - | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl) - | Fix (ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - | CoFix(ln,(lna,tl,bl)) -> - let l' = Array.fold_left (fun l na -> g na l) l lna in - mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl)) - -(* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the - immediate subterms of [c]; it carries an extra data [n] (typically - a lift index) which is processed by [g] (which typically add 1 to - [n]) at each binder traversal; the subterms are processed from left - to right according to the usual representation of the constructions - (this may matter if [f] does a side-effect); it is not recursive; - in fact, the usual representation of the constructions is at the - time being almost those of the ML representation (except for - (co-)fixpoint) *) - -let fold_rec_types g (lna,typarray,_) e = - let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in - Array.fold_left (fun e assum -> g assum e) e ctxt - -let map_left2 f a g b = - let l = Array.length a in - if Int.equal l 0 then [||], [||] else begin - let r = Array.make l (f a.(0)) in - let s = Array.make l (g b.(0)) in - for i = 1 to l - 1 do - r.(i) <- f a.(i); - s.(i) <- g b.(i) - done; - r, s - end - -let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> c - | Cast (b,k,t) -> - let b' = f l b in - let t' = f l t in - if b' == b && t' == t then c - else mkCast (b',k,t') - | Prod (na,t,b) -> - let t' = f l t in - let b' = f (g (na,None,t) l) b in - if t' == t && b' == b then c - else mkProd (na, t', b') - | Lambda (na,t,b) -> - let t' = f l t in - let b' = f (g (na,None,t) l) b in - if t' == t && b' == b then c - else mkLambda (na, t', b') - | LetIn (na,bo,t,b) -> - let bo' = f l bo in - let t' = f l t in - let b' = f (g (na,Some bo,t) l) b in - if bo' == bo && t' == t && b' == b then c - else mkLetIn (na, bo', t', b') - | App (c,[||]) -> assert false - | App (t,al) -> - (*Special treatment to be able to recognize partially applied subterms*) - let a = al.(Array.length al - 1) in - let app = (mkApp (t, Array.sub al 0 (Array.length al - 1))) in - let app' = f l app in - let a' = f l a in - if app' == app && a' == a then c - else mkApp (app', [| a' |]) - | Proj (p,b) -> - let b' = f l b in - if b' == b then c - else mkProj (p, b') - | Evar (e,al) -> - let al' = Array.map_left (f l) al in - if Array.for_all2 (==) al' al then c - else mkEvar (e, al') - | Case (ci,p,b,bl) -> - (* In v8 concrete syntax, predicate is after the term to match! *) - let b' = f l b in - let p' = f l p in - let bl' = Array.map_left (f l) bl in - if b' == b && p' == p && bl' == bl then c - else mkCase (ci, p', b', bl') - | Fix (ln,(lna,tl,bl as fx)) -> - let l' = fold_rec_types g fx l in - let (tl', bl') = map_left2 (f l) tl (f l') bl in - if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' - then c - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl as fx)) -> - let l' = fold_rec_types g fx l in - let (tl', bl') = map_left2 (f l) tl (f l') bl in - if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' - then c - else mkCoFix (ln,(lna,tl',bl')) - -(* strong *) -let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> cstr - | Cast (c,k, t) -> - let c' = f l c in - let t' = f l t in - if c==c' && t==t' then cstr else mkCast (c', k, t') - | Prod (na,t,c) -> - let t' = f l t in - let c' = f (g (na,None,t) l) c in - if t==t' && c==c' then cstr else mkProd (na, t', c') - | Lambda (na,t,c) -> - let t' = f l t in - let c' = f (g (na,None,t) l) c in - if t==t' && c==c' then cstr else mkLambda (na, t', c') - | LetIn (na,b,t,c) -> - let b' = f l b in - let t' = f l t in - let c' = f (g (na,Some b,t) l) c in - if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c') - | App (c,al) -> - let c' = f l c in - let al' = Array.map (f l) al in - if c==c' && Array.for_all2 (==) al al' then cstr else mkApp (c', al') - | Proj (p,c) -> - let c' = f l c in - if c' == c then cstr else mkProj (p, c') - | Evar (e,al) -> - let al' = Array.map (f l) al in - if Array.for_all2 (==) al al' then cstr else mkEvar (e, al') - | Case (ci,p,c,bl) -> - let p' = f l p in - let c' = f l c in - let bl' = Array.map (f l) bl in - if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else - mkCase (ci, p', c', bl') - | Fix (ln,(lna,tl,bl)) -> - let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in - let bl' = Array.map (f l') bl in - if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' - then cstr - else mkFix (ln,(lna,tl',bl')) - | CoFix(ln,(lna,tl,bl)) -> - let tl' = Array.map (f l) tl in - let l' = - Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in - let bl' = Array.map (f l') bl in - if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' - then cstr - else mkCoFix (ln,(lna,tl',bl')) - -(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate - subterms of [c] starting from [acc] and proceeding from left to - right according to the usual representation of the constructions as - [fold_constr] but it carries an extra data [n] (typically a lift - index) which is processed by [g] (which typically add 1 to [n]) at - each binder traversal; it is not recursive *) - -let fold_constr_with_full_binders g f n acc c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (na,None,t) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (na,Some b,t) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (n,None,t) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - -let fold_constr_with_binders g f n acc c = - fold_constr_with_full_binders (fun _ x -> g x) f n acc c - -(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate - subterms of [c]; it carries an extra data [acc] which is processed by [g] at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) - -let iter_constr_with_full_binders g f l c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> () - | Cast (c,_, t) -> f l c; f l t - | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c - | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c - | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c - | App (c,args) -> f l c; Array.iter (f l) args - | Proj (p,c) -> f l c - | Evar (_,args) -> Array.iter (f l) args - | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl - | Fix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl - | CoFix (_,(lna,tl,bl)) -> - let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in - Array.iter (f l) tl; - Array.iter (f l') bl - -(***************************) -(* occurs check functions *) -(***************************) - -exception Occur - -let occur_meta c = - let rec occrec c = match kind_of_term c with - | Meta _ -> raise Occur - | _ -> iter_constr occrec c - in try occrec c; false with Occur -> true - -let occur_existential c = - let rec occrec c = match kind_of_term c with - | Evar _ -> raise Occur - | _ -> iter_constr occrec c - in try occrec c; false with Occur -> true - -let occur_meta_or_existential c = - let rec occrec c = match kind_of_term c with - | Evar _ -> raise Occur - | Meta _ -> raise Occur - | _ -> iter_constr occrec c - in try occrec c; false with Occur -> true - -let occur_evar n c = - let rec occur_rec c = match kind_of_term c with - | Evar (sp,_) when Evar.equal sp n -> raise Occur - | _ -> iter_constr occur_rec c - in - try occur_rec c; false with Occur -> true - -let occur_in_global env id constr = - let vars = vars_of_global env constr in - if Id.Set.mem id vars then raise Occur - -let occur_var env id c = - let rec occur_rec c = - match kind_of_term c with - | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c - | _ -> iter_constr occur_rec c - in - try occur_rec c; false with Occur -> true - -let occur_var_in_decl env hyp (_,c,typ) = - match c with - | None -> occur_var env hyp typ - | Some body -> - occur_var env hyp typ || - occur_var env hyp body - -(* returns the list of free debruijn indices in a term *) - -let free_rels m = - let rec frec depth acc c = match kind_of_term c with - | Rel n -> if n >= depth then Int.Set.add (n-depth+1) acc else acc - | _ -> fold_constr_with_binders succ frec depth acc c - in - frec 1 Int.Set.empty m - -(* collects all metavar occurrences, in left-to-right order, preserving - * repetitions and all. *) - -let collect_metas c = - let rec collrec acc c = - match kind_of_term c with - | Meta mv -> List.add_set Int.equal mv acc - | _ -> fold_constr collrec acc c - in - List.rev (collrec [] c) - -(* collects all vars; warning: this is only visible vars, not dependencies in - all section variables; for the latter, use global_vars_set *) -let collect_vars c = - let rec aux vars c = match kind_of_term c with - | Var id -> Id.Set.add id vars - | _ -> fold_constr aux vars c in - aux Id.Set.empty c - -(* Tests whether [m] is a subterm of [t]: - [m] is appropriately lifted through abstractions of [t] *) - -let dependent_main noevar univs m t = - let eqc x y = if univs then fst (Universes.eq_constr_universes x y) else eq_constr_nounivs x y in - let rec deprec m t = - if eqc m t then - raise Occur - else - match kind_of_term m, kind_of_term t with - | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); - CArray.Fun1.iter deprec m - (Array.sub lt - (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when noevar && isMeta c -> () - | _, Evar _ when noevar -> () - | _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t - in - try deprec m t; false with Occur -> true - -let dependent = dependent_main false false -let dependent_no_evar = dependent_main true false - -let dependent_univs = dependent_main false true -let dependent_univs_no_evar = dependent_main true true - -let dependent_in_decl a (_,c,t) = - match c with - | None -> dependent a t - | Some body -> dependent a body || dependent a t - -let count_occurrences m t = - let n = ref 0 in - let rec countrec m t = - if eq_constr m t then - incr n - else - match kind_of_term m, kind_of_term t with - | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); - Array.iter (countrec m) - (Array.sub lt - (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when isMeta c -> () - | _, Evar _ -> () - | _ -> iter_constr_with_binders (lift 1) countrec m t - in - countrec m t; - !n - -(* Synonymous *) -let occur_term = dependent - -let pop t = lift (-1) t - -(***************************) -(* bindings functions *) -(***************************) - -type meta_type_map = (metavariable * types) list - -type meta_value_map = (metavariable * constr) list - -let rec subst_meta bl c = - match kind_of_term c with - | Meta i -> (try Int.List.assoc i bl with Not_found -> c) - | _ -> map_constr (subst_meta bl) c - -(* First utilities for avoiding telescope computation for subst_term *) - -let prefix_application eq_fun (k,c) (t : constr) = - let c' = collapse_appl c and t' = collapse_appl t in - match kind_of_term c', kind_of_term t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in - if l1 <= l2 - && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) - else - None - | _ -> None - -let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = - let c' = collapse_appl c and t' = collapse_appl t in - match kind_of_term c', kind_of_term t' with - | App (f1,cl1), App (f2,cl2) -> - let l1 = Array.length cl1 - and l2 = Array.length cl2 in - if l1 <= l2 - && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1))) - else - None - | _ -> None - -(* Recognizing occurrences of a given subterm in a term: [subst_term c t] - substitutes [(Rel 1)] for all occurrences of term [c] in a term [t]; - works if [c] has rels *) - -let subst_term_gen eq_fun c t = - let rec substrec (k,c as kc) t = - match prefix_application eq_fun kc t with - | Some x -> x - | None -> - if eq_fun c t then mkRel k - else - map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t - in - substrec (1,c) t - -let subst_term = subst_term_gen eq_constr - -(* Recognizing occurrences of a given subterm in a term : - [replace_term c1 c2 t] substitutes [c2] for all occurrences of - term [c1] in a term [t]; works if [c1] and [c2] have rels *) - -let replace_term_gen eq_fun c by_c in_t = - let rec substrec (k,c as kc) t = - match my_prefix_application eq_fun kc by_c t with - | Some x -> x - | None -> - (if eq_fun c t then (lift k by_c) else - map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) - substrec kc t) - in - substrec (0,c) in_t - -let replace_term = replace_term_gen eq_constr - -let vars_of_env env = - let s = - Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) - (named_context env) ~init:Id.Set.empty in - Context.fold_rel_context - (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s) - (rel_context env) ~init:s - -let add_vname vars = function - Name id -> Id.Set.add id vars - | _ -> vars - -(*************************) -(* Names environments *) -(*************************) -type names_context = Name.t list -let add_name n nl = n::nl -let lookup_name_of_rel p names = - try List.nth names (p-1) - with Invalid_argument _ | Failure _ -> raise Not_found -let lookup_rel_of_name id names = - let rec lookrec n = function - | Anonymous :: l -> lookrec (n+1) l - | (Name id') :: l -> if Id.equal id' id then n else lookrec (n+1) l - | [] -> raise Not_found - in - lookrec 1 names -let empty_names_context = [] - -let ids_of_rel_context sign = - Context.fold_rel_context - (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l) - sign ~init:[] - -let ids_of_named_context sign = - Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[] - -let ids_of_context env = - (ids_of_rel_context (rel_context env)) - @ (ids_of_named_context (named_context env)) - - -let names_of_rel_context env = - List.map (fun (na,_,_) -> na) (rel_context env) - -let is_section_variable id = - try let _ = Global.lookup_named id in true - with Not_found -> false - -let isGlobalRef c = - match kind_of_term c with - | Const _ | Ind _ | Construct _ | Var _ -> true - | _ -> false - -let is_template_polymorphic env f = - match kind_of_term f with - | Ind ind -> Environ.template_polymorphic_pind ind env - | Const c -> Environ.template_polymorphic_pconstant c env - | _ -> false - -let base_sort_cmp pb s0 s1 = - match (s0,s1) with - | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb == Reduction.CUMUL - | (Type u1, Type u2) -> true - | _ -> false - -(* eq_constr extended with universe erasure *) -let compare_constr_univ f cv_pb t1 t2 = - match kind_of_term t1, kind_of_term t2 with - Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2 - | Prod (_,t1,c1), Prod (_,t2,c2) -> - f Reduction.CONV t1 t2 && f cv_pb c1 c2 - | _ -> compare_constr (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 - -let rec constr_cmp cv_pb t1 t2 = compare_constr_univ constr_cmp cv_pb t1 t2 - -let eq_constr t1 t2 = constr_cmp Reduction.CONV t1 t2 - -(* App(c,[t1,...tn]) -> ([c,t1,...,tn-1],tn) - App(c,[||]) -> ([],c) *) -let split_app c = match kind_of_term c with - App(c,l) -> - let len = Array.length l in - if Int.equal len 0 then ([],c) else - let last = Array.get l (len-1) in - let prev = Array.sub l 0 (len-1) in - c::(Array.to_list prev), last - | _ -> assert false - -type subst = (rel_context*constr) Evar.Map.t - -exception CannotFilter - -let filtering env cv_pb c1 c2 = - let evm = ref Evar.Map.empty in - let define cv_pb e1 ev c1 = - try let (e2,c2) = Evar.Map.find ev !evm in - let shift = List.length e1 - List.length e2 in - if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter - with Not_found -> - evm := Evar.Map.add ev (e1,c1) !evm - in - let rec aux env cv_pb c1 c2 = - match kind_of_term c1, kind_of_term c2 with - | App _, App _ -> - let ((p1,l1),(p2,l2)) = (split_app c1),(split_app c2) in - let () = aux env cv_pb l1 l2 in - begin match p1, p2 with - | [], [] -> () - | (h1 :: p1), (h2 :: p2) -> - aux env cv_pb (applistc h1 p1) (applistc h2 p2) - | _ -> assert false - end - | Prod (n,t1,c1), Prod (_,t2,c2) -> - aux env cv_pb t1 t2; - aux ((n,None,t1)::env) cv_pb c1 c2 - | _, Evar (ev,_) -> define cv_pb env ev c1 - | Evar (ev,_), _ -> define cv_pb env ev c2 - | _ -> - if compare_constr_univ - (fun pb c1 c2 -> aux env pb c1 c2; true) cv_pb c1 c2 then () - else raise CannotFilter - (* TODO: le reste des binders *) - in - aux env cv_pb c1 c2; !evm - -let decompose_prod_letin : constr -> int * rel_context * constr = - let rec prodec_rec i l c = match kind_of_term c with - | Prod (n,t,c) -> prodec_rec (succ i) ((n,None,t)::l) c - | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c - | Cast (c,_,_) -> prodec_rec i l c - | _ -> i,l,c in - prodec_rec 0 [] - -let align_prod_letin c a : rel_context * constr = - let (lc,_,_) = decompose_prod_letin c in - let (la,l,a) = decompose_prod_letin a in - if not (la >= lc) then invalid_arg "align_prod_letin"; - let (l1,l2) = Util.List.chop lc l in - l2,it_mkProd_or_LetIn a l1 - -(* We reduce a series of head eta-redex or nothing at all *) -(* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) -(* Remplace 2 earlier buggish versions *) - -let rec eta_reduce_head c = - match kind_of_term c with - | Lambda (_,c1,c') -> - (match kind_of_term (eta_reduce_head c') with - | App (f,cl) -> - let lastn = (Array.length cl) - 1 in - if lastn < 0 then anomaly (Pp.str "application without arguments") - else - (match kind_of_term cl.(lastn) with - | Rel 1 -> - let c' = - if Int.equal lastn 0 then f - else mkApp (f, Array.sub cl 0 lastn) - in - if noccurn 1 c' - then lift (-1) c' - else c - | _ -> c) - | _ -> c) - | _ -> c - - -(* iterator on rel context *) -let process_rel_context f env = - let sign = named_context_val env in - let rels = rel_context env in - let env0 = reset_with_named_context sign env in - Context.fold_rel_context f rels ~init:env0 - -let assums_of_rel_context sign = - Context.fold_rel_context - (fun (na,c,t) l -> - match c with - Some _ -> l - | None -> (na, t)::l) - sign ~init:[] - -let map_rel_context_in_env f env sign = - let rec aux env acc = function - | d::sign -> - aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign - | [] -> - acc - in - aux env [] (List.rev sign) - -let map_rel_context_with_binders f sign = - let rec aux k = function - | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign - | [] -> [] - in - aux (rel_context_length sign) sign - -let substl_rel_context l = - map_rel_context_with_binders (fun k -> substnl l (k-1)) - -let lift_rel_context n = - map_rel_context_with_binders (liftn n) - -let smash_rel_context sign = - let rec aux acc = function - | [] -> acc - | (_,None,_ as d) :: l -> aux (d::acc) l - | (_,Some b,_) :: l -> - (* Quadratic in the number of let but there are probably a few of them *) - aux (List.rev (substl_rel_context [b] (List.rev acc))) l - in List.rev (aux [] sign) - -let adjust_subst_to_rel_context sign l = - let rec aux subst sign l = - match sign, l with - | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' - | (_,Some c,_)::sign', args' -> - aux (substl subst c :: subst) sign' args' - | [], [] -> List.rev subst - | _ -> anomaly (Pp.str "Instance and signature do not match") - in aux [] (List.rev sign) l - -let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init - -let rec mem_named_context id = function - | (id',_,_) :: _ when Id.equal id id' -> true - | _ :: sign -> mem_named_context id sign - | [] -> false - -let compact_named_context_reverse sign = - let compact l (i1,c1,t1) = - match l with - | [] -> [[i1],c1,t1] - | (l2,c2,t2)::q -> - if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2 - then (i1::l2,c2,t2)::q - else ([i1],c1,t1)::l - in Context.fold_named_context_reverse compact ~init:[] sign - -let compact_named_context sign = List.rev (compact_named_context_reverse sign) - -let clear_named_body id env = - let aux _ = function - | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t) - | d -> push_named d in - fold_named_context aux env ~init:(reset_context env) - -let global_vars env ids = Id.Set.elements (global_vars_set env ids) - -let global_vars_set_of_decl env = function - | (_,None,t) -> global_vars_set env t - | (_,Some c,t) -> - Id.Set.union (global_vars_set env t) - (global_vars_set env c) - -let dependency_closure env sign hyps = - if Id.Set.is_empty hyps then [] else - let (_,lh) = - Context.fold_named_context_reverse - (fun (hs,hl) (x,_,_ as d) -> - if Id.Set.mem x hs then - (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), - x::hl) - else (hs,hl)) - ~init:(hyps,[]) - sign in - List.rev lh - -(* Combinators on judgments *) - -let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } -let on_judgment_value f j = { j with uj_val = f j.uj_val } -let on_judgment_type f j = { j with uj_type = f j.uj_type } - -(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k - variables; skips let-in's *) -let context_chop k ctx = - let rec chop_aux acc = function - | (0, l2) -> (List.rev acc, l2) - | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) - | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) - | (_, []) -> anomaly (Pp.str "context_chop") - in chop_aux [] (k,ctx) - -(* Do not skip let-in's *) -let env_rel_context_chop k env = - let rels = rel_context env in - let ctx1,ctx2 = List.chop k rels in - push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), - ctx1 - -(*******************************************) -(* Functions to deal with impossible cases *) -(*******************************************) -let impossible_default_case = ref None - -let set_impossible_default_clause c = impossible_default_case := Some c - -let coq_unit_judge = - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in - fun () -> - match !impossible_default_case with - | Some fn -> - let (id,type_of_id), ctx = fn () in - make_judge id type_of_id, ctx - | None -> - (* In case the constants id/ID are not defined *) - make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), - Univ.ContextSet.empty diff --git a/pretyping/termops.mli b/pretyping/termops.mli deleted file mode 100644 index ca98f8d73..000000000 --- a/pretyping/termops.mli +++ /dev/null @@ -1,248 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Names -open Term -open Context -open Environ - -(** printers *) -val print_sort : sorts -> std_ppcmds -val pr_sort_family : sorts_family -> std_ppcmds -val pr_fix : (constr -> std_ppcmds) -> fixpoint -> std_ppcmds - -(** debug printer: do not use to display terms to the casual user... *) -val set_print_constr : (env -> constr -> std_ppcmds) -> unit -val print_constr : constr -> std_ppcmds -val print_constr_env : env -> constr -> std_ppcmds -val print_named_context : env -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds -val print_rel_context : env -> std_ppcmds -val print_env : env -> std_ppcmds - -(** about contexts *) -val push_rel_assum : Name.t * types -> env -> env -val push_rels_assum : (Name.t * types) list -> env -> env -val push_named_rec_types : Name.t array * types array * 'a -> env -> env - -val lookup_rel_id : Id.t -> rel_context -> int * constr option * types -(** Associates the contents of an identifier in a [rel_context]. Raise - [Not_found] if there is no such identifier. *) - -(** Functions that build argument lists matching a block of binders or a context. - [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|] - [extended_rel_vect n ctx] extends the [ctx] context of length [m] - with [n] elements. -*) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> constr list -val extended_rel_list : int -> rel_context -> constr list -val extended_rel_vect : int -> rel_context -> constr array - -(** iterators/destructors on terms *) -val mkProd_or_LetIn : rel_declaration -> types -> types -val mkProd_wo_LetIn : rel_declaration -> types -> types -val it_mkProd : types -> (Name.t * types) list -> types -val it_mkLambda : constr -> (Name.t * types) list -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types -val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : types -> named_context -> types -val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr - -(* Ad hoc version reinserting letin, assuming the body is defined in - the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr - -(** {6 Generic iterators on constr} *) - -val map_constr_with_named_binders : - (Name.t -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr -val map_constr_with_binders_left_to_right : - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> constr) -> - 'a -> constr -> constr -val map_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr - -(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate - subterms of [c] starting from [acc] and proceeding from left to - right according to the usual representation of the constructions as - [fold_constr] but it carries an extra data [n] (typically a lift - index) which is processed by [g] (which typically add 1 to [n]) at - each binder traversal; it is not recursive *) - -val fold_constr_with_binders : - ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b - -val fold_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b - -val iter_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> - constr -> unit - -(**********************************************************************) - -val strip_head_cast : constr -> constr -val drop_extra_implicit_args : constr -> constr - -(** occur checks *) -exception Occur -val occur_meta : types -> bool -val occur_existential : types -> bool -val occur_meta_or_existential : types -> bool -val occur_evar : existential_key -> types -> bool -val occur_var : env -> Id.t -> types -> bool -val occur_var_in_decl : - env -> - Id.t -> 'a * types option * types -> bool -val free_rels : constr -> Int.Set.t - -(** [dependent m t] tests whether [m] is a subterm of [t] *) -val dependent : constr -> constr -> bool -val dependent_no_evar : constr -> constr -> bool -val dependent_univs : constr -> constr -> bool -val dependent_univs_no_evar : constr -> constr -> bool -val dependent_in_decl : constr -> named_declaration -> bool -val count_occurrences : constr -> constr -> int -val collect_metas : constr -> int list -val collect_vars : constr -> Id.Set.t (** for visible vars only *) -val occur_term : constr -> constr -> bool (** Synonymous - of dependent - Substitution of metavariables *) -type meta_value_map = (metavariable * constr) list -val subst_meta : meta_value_map -> constr -> constr - -(** Type assignment for metavariables *) -type meta_type_map = (metavariable * types) list - -(** [pop c] lifts by -1 the positive indexes in [c] *) -val pop : constr -> constr - -(** {6 ... } *) -(** Substitution of an arbitrary large term. Uses equality modulo - reduction of let *) - -(** [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq] - as equality *) -val subst_term_gen : - (constr -> constr -> bool) -> constr -> constr -> constr - -(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] - as equality *) -val replace_term_gen : - (constr -> constr -> bool) -> - constr -> constr -> constr -> constr - -(** [subst_term d c] replaces [Rel 1] by [d] in [c] *) -val subst_term : constr -> constr -> constr - -(** [replace_term d e c] replaces [d] by [e] in [c] *) -val replace_term : constr -> constr -> constr -> constr - -(** Alternative term equalities *) -val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool -val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> - Reduction.conv_pb -> constr -> constr -> bool -val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool -val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) - -val eta_reduce_head : constr -> constr - -exception CannotFilter - -(** Lightweight first-order filtering procedure. Unification - variables ar represented by (untyped) Evars. - [filtering c1 c2] returns the substitution n'th evar -> - (context,term), or raises [CannotFilter]. - Warning: Outer-kernel sort subtyping are taken into account: c1 has - to be smaller than c2 wrt. sorts. *) -type subst = (rel_context*constr) Evar.Map.t -val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst - -val decompose_prod_letin : constr -> int * rel_context * constr -val align_prod_letin : constr -> constr -> rel_context * constr - -(** Get the last arg of a constr intended to be an application *) -val last_arg : constr -> constr - -(** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : constr -> constr * constr array - -val adjust_app_list_size : constr -> constr list -> constr -> constr list -> - (constr * constr list * constr * constr list) -val adjust_app_array_size : constr -> constr array -> constr -> constr array -> - (constr * constr array * constr * constr array) - -(** name contexts *) -type names_context = Name.t list -val add_name : Name.t -> names_context -> names_context -val lookup_name_of_rel : int -> names_context -> Name.t -val lookup_rel_of_name : Id.t -> names_context -> int -val empty_names_context : names_context -val ids_of_rel_context : rel_context -> Id.t list -val ids_of_named_context : named_context -> Id.t list -val ids_of_context : env -> Id.t list -val names_of_rel_context : env -> names_context - -val context_chop : int -> rel_context -> rel_context * rel_context -val env_rel_context_chop : int -> env -> env * rel_context - -(** Set of local names *) -val vars_of_env: env -> Id.Set.t -val add_vname : Id.Set.t -> Name.t -> Id.Set.t - -(** other signature iterators *) -val process_rel_context : (rel_declaration -> env -> env) -> env -> env -val assums_of_rel_context : rel_context -> (Name.t * constr) list -val lift_rel_context : int -> rel_context -> rel_context -val substl_rel_context : constr list -> rel_context -> rel_context -val smash_rel_context : rel_context -> rel_context (** expand lets in context *) -val adjust_subst_to_rel_context : rel_context -> constr list -> constr list -val map_rel_context_in_env : - (env -> constr -> constr) -> env -> rel_context -> rel_context -val map_rel_context_with_binders : - (int -> constr -> constr) -> rel_context -> rel_context -val fold_named_context_both_sides : - ('a -> named_declaration -> named_declaration list -> 'a) -> - named_context -> init:'a -> 'a -val mem_named_context : Id.t -> named_context -> bool -val compact_named_context : named_context -> named_list_context -val compact_named_context_reverse : named_context -> named_list_context - -val clear_named_body : Id.t -> env -> env - -val global_vars : env -> constr -> Id.t list -val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t - -(** Gives an ordered list of hypotheses, closed by dependencies, - containing a given set *) -val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list - -(** Test if an identifier is the basename of a global reference *) -val is_section_variable : Id.t -> bool - -val isGlobalRef : constr -> bool - -val is_template_polymorphic : env -> constr -> bool - -(** Combinators on judgments *) - -val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment - -(** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3be98a1ae..3d6196c35 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -12,7 +12,6 @@ open Globnames open Decl_kinds open Term open Vars -open Context open Evd open Util open Typeclasses_errors @@ -59,10 +58,10 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) - cl_props : rel_context; + cl_props : Context.Rel.t; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * int option) option * constant option) list; @@ -127,7 +126,7 @@ let typeclass_univ_instance (cl,u') = in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') in - let subst_ctx = Context.map_rel_context (subst_univs_level_constr subst) in + let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); cl_props = subst_ctx cl.cl_props}, u' @@ -204,7 +203,7 @@ let discharge_class (_,cl) = (decl :: ctx', n :: subst) ) ctx ([], []) in let discharge_rel_context subst n rel = - let rel = map_rel_context (Cooking.expmod_constr repl) rel in + let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in let ctx, _ = List.fold_right (fun (id, b, t) (ctx, k) -> @@ -287,7 +286,7 @@ let build_subclasses ~check env sigma glob pri = | None -> [] | Some (rels, ((tc,u), args)) -> let instapp = - Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) + Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels)) in let projargs = Array.of_list (args @ [instapp]) in let projs = List.map_filter @@ -436,7 +435,7 @@ let instance_constructor (cl,u) args = | None -> true | Some _ -> false in - let lenpars = List.length (List.filter filter (snd cl.cl_context)) in + let lenpars = List.count filter (snd cl.cl_context) in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 9e018f616..7bb0ef3ab 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -9,7 +9,6 @@ open Names open Globnames open Term -open Context open Evd open Environ @@ -24,10 +23,10 @@ type typeclass = { (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass and the global reference gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * rel_context; + cl_context : (global_reference * bool) option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) - cl_props : rel_context; + cl_props : Context.Rel.t; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if @@ -68,7 +67,7 @@ val dest_class_app : env -> constr -> typeclass puniverses * constr list val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses (** Just return None if not a class *) -val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option +val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option val instance_impl : instance -> global_reference diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index a0f631984..b1dfb19a0 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -9,7 +9,6 @@ (*i*) open Names open Term -open Context open Environ open Constrexpr open Globnames @@ -20,7 +19,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) + | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 7facb06f0..ee76f6383 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -9,7 +9,6 @@ open Loc open Names open Term -open Context open Environ open Constrexpr open Globnames @@ -19,7 +18,7 @@ type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * Id.t located (** Class name, method *) - | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *) + | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *) exception TypeClassError of env * typeclass_error @@ -27,5 +26,5 @@ val not_a_class : env -> constr -> 'a val unbound_method : env -> global_reference -> Id.t located -> 'a -val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a +val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a diff --git a/pretyping/typing.ml b/pretyping/typing.ml index eb16628b1..fb0c49320 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -111,9 +111,8 @@ let e_type_case_branches env evdref (ind,largs) pj c = let p = pj.uj_val in let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in - let n = (snd specif).Declarations.mind_nrealargs in - let ty = - whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in + let n = (snd specif).Declarations.mind_nrealdecls in + let ty = whd_betaiota !evdref (lambda_applist_assum (n+1) p (realargs@[c])) in (lc, ty, univ) let e_judge_of_case env evdref ci pj cj lfj = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f97f6fbc5..b5e882bc4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -27,6 +27,7 @@ open Recordops open Locus open Locusops open Find_subterm +open Sigma.Notations let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { @@ -107,7 +108,9 @@ 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,ev = new_evar env evd typ in + 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' = evar_absorb_arguments env evd (destEvar ev) l in let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in @@ -556,6 +559,19 @@ let isAllowedEvar flags c = match kind_of_term c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false + +let subst_defined_metas_evars (bl,el) c = + let rec substrec c = match kind_of_term c with + | Meta i -> + let select (j,_,_) = Int.equal i j in + substrec (pi2 (List.find select bl)) + | Evar (evk,args) -> + let select (_,(evk',args'),_) = Evar.equal evk evk' && Array.equal Constr.equal args args' in + (try substrec (pi3 (List.find select el)) + with Not_found -> map_constr substrec c) + | _ -> map_constr substrec c + in try Some (substrec c) with Not_found -> None + let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = match subst_defined_metas_evars (metasubst,[]) tyM with | None -> sigma @@ -1154,20 +1170,20 @@ 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 evd n c = - let rec apprec n c cty evd = +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 -> if Int.equal n 0 then - (evd, c) + Sigma (c, evd, p) else - match kind_of_term (whd_betadeltaiota env evd cty) with + match kind_of_term (whd_betadeltaiota env (Sigma.to_evar_map evd) cty) with | Prod (_,c1,c2) -> - let (evd',evar) = - Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in - apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.unsafe_type_of env evd c) evd - + apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd + let is_mimick_head ts f = match kind_of_term f with | Const (c,u) -> not (Closure.is_transparent_constant ts c) @@ -1327,7 +1343,9 @@ let w_merge env with_types flags (evd,metas,evars) = 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', c) = applyHead sp_env evd nargs hdc 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'',mc,ec) = unify_0 sp_env evd' CUMUL flags (get_type_of sp_env evd' c) ev.evar_concl in @@ -1436,9 +1454,10 @@ let indirect_dependency d decls = pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) 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, subst_univs_constr subst (nf_evar sigma c) + Sigma.Unsafe.of_pair (subst_univs_constr subst (nf_evar sigma c), sigma) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1565,7 +1584,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in - if Context.eq_named_declaration d newdecl + if Context.Named.Declaration.equal d newdecl && not (indirectly_dependent c d depdecls) then if check_occs && not (in_every_hyp occs) @@ -1589,7 +1608,11 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in - (id,sign,depdecls,lastlhyp,ccl,out test) + let res = match out test with + | None -> None + | Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma)) + in + (id,sign,depdecls,lastlhyp,ccl,res) with SubtermUnificationError e -> raise (PretypeError (env,sigma,CannotUnifyOccurrences e)) @@ -1611,12 +1634,13 @@ type abstraction_request = | AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool -type abstraction_result = +type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * - types * (Evd.evar_map * constr) option + Context.Named.Declaration.t list * Names.Id.t option * + types * (constr, 'r) Sigma.sigma 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 diff --git a/pretyping/unification.mli b/pretyping/unification.mli index d5d5caf9e..0ad882a9f 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -75,15 +75,15 @@ type abstraction_request = | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> Evd.evar_map -> pending_constr -> Evd.evar_map * constr + env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma -type abstraction_result = +type 'r abstraction_result = Names.Id.t * named_context_val * - Context.named_declaration list * Names.Id.t option * - types * (Evd.evar_map * constr) option + Context.Named.Declaration.t list * Names.Id.t option * + types * (constr, 'r) Sigma.sigma option -val make_abstraction : env -> Evd.evar_map -> constr -> - abstraction_request -> abstraction_result +val make_abstraction : env -> 'r Sigma.t -> 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 7d86fad92..8b9c2d6c9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -45,13 +45,7 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) (* Argggg, ces constructeurs de ... qui commencent a 1*) -let find_rectype_a env c = - let (t, l) = - let t = whd_betadeltaiota env c in - try destApp t with DestKO -> (t,[||]) in - match kind_of_term t with - | Ind ind -> (ind, l) - | _ -> raise Not_found +let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c (* Instantiate inductives and parameters in constructor type *) @@ -59,11 +53,11 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let ndecls = Context.rel_context_length mib.mind_params_ctxt in + let ndecls = Context.Rel.length mib.mind_params_ctxt in if Int.equal ndecls 0 then ctyp else let _,ctyp = decompose_prod_n_assum ndecls ctyp in - substl (List.rev (Termops.adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) ctyp diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index bdc6c1db6..58f5b14e1 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -8,7 +8,6 @@ open Term open Environ -open Evd (** {6 Reduction functions } *) val cbv_vm : env -> constr -> types -> constr |