diff options
Diffstat (limited to 'kernel')
80 files changed, 1680 insertions, 1323 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 7e193ef82..31ded9129 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -23,7 +23,7 @@ open CErrors open Util open Pp open Names -open Term +open Constr open Vars open Environ open Esubst @@ -85,7 +85,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind val no_red : reds val red_add : reds -> red_kind -> reds @@ -114,7 +114,7 @@ module RedFlags = (struct type red_kind = BETA | DELTA | ETA | MATCH | FIX | COFIX | ZETA - | CONST of constant | VAR of Id.t + | CONST of Constant.t | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA @@ -234,7 +234,7 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = constant puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' @@ -401,7 +401,7 @@ let update v1 no t = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -480,7 +480,8 @@ let rec lft_fconstr n ft = | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | _ -> {norm=ft.norm; term=FLIFT(n,ft)} + | FFlex _ | FAtom _ | FCast _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f let lift_fconstr_vect k v = @@ -516,7 +517,7 @@ let zupdate m s = else s let mk_lambda env t = - let (rvars,t') = decompose_lam t in + let (rvars,t') = Term.decompose_lam t in FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = @@ -530,7 +531,7 @@ let destFLambda clos_fun t = (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) let mk_clos e t = - match kind_of_term t with + match kind t with | Rel i -> clos_rel e i | Var x -> { norm = Red; term = FFlex (VarKey x) } | Const c -> { norm = Red; term = FFlex (ConstKey c) } @@ -556,7 +557,7 @@ let mk_clos_vect env v = match v with subterms. Could be used insted of mk_clos. *) let mk_clos_deep clos_fun env t = - match kind_of_term t with + match kind t with | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> mk_clos env t | Cast (a,k,b) -> @@ -655,7 +656,7 @@ let term_of_fconstr = match v.term with | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts -> - compose_lam (List.rev tys) f + Term.compose_lam (List.rev tys) f | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx | _ -> to_constr term_of_fconstr_lift lfts v in @@ -891,7 +892,7 @@ let rec knh info m stk = (* The same for pure terms *) and knht info e t stk = - match kind_of_term t with + match kind t with | App(a,b) -> knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> @@ -958,7 +959,10 @@ let rec knr info m stk = (match evar_value info.i_cache ev with Some c -> knit info env c stk | None -> (m,stk)) - | _ -> (m,stk) + | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ + | FCLOS _ -> (m, stk) + (* Computes the weak head normal form of a term *) and kni info m stk = @@ -1034,7 +1038,8 @@ and norm_head info m = mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args) | FProj (p,c) -> mkProj (p, kl info c) - | t -> term_of_fconstr m + | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _ + | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m (* Initialization and then normalization *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9e5cb48a4..119b70e30 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Esubst @@ -29,7 +29,7 @@ val all_opaque : transparent_state val all_transparent : transparent_state val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool +val is_transparent_constant : transparent_state -> Constant.t -> bool (** Sets of reduction kinds. *) module type RedFlagsSig = sig @@ -46,7 +46,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind (** No reduction at all *) @@ -92,7 +92,7 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = constant puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey type 'a infos_cache type 'a infos = { @@ -122,8 +122,8 @@ type fterm = | FAtom of constr (** Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive puniverses - | FConstruct of constructor puniverses + | FInd of inductive Univ.puniverses + | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array | FProj of projection * fconstr | FFix of fixpoint * fconstr subs @@ -145,7 +145,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 25f61c7aa..9febc6449 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -13,7 +13,7 @@ (* This file defines the type of bytecode instructions *) open Names -open Term +open Constr type tag = int @@ -32,13 +32,13 @@ let cofix_evaluated_tag = 7 let last_variant_tag = 245 type structured_constant = - | Const_sorts of sorts + | Const_sorts of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.universe_level - | Const_type of Univ.universe + | Const_univ_level of Univ.Level.t + | Const_type of Univ.Universe.t type reloc_table = (tag * int) array @@ -74,7 +74,7 @@ type instruction = | Kclosurerec of int * int * Label.t array * Label.t array | Kclosurecofix of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of int * tag | Kmakeprod @@ -186,14 +186,15 @@ open Pp open Util let pp_sort s = - match family_of_sort s with + let open Sorts in + match family s with | InSet -> str "Set" | InProp -> str "Prop" | InType -> str "Type" let rec pp_struct_const = function | Const_sorts s -> pp_sort s - | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i + | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> @@ -241,7 +242,7 @@ let rec pp_instr i = prlist_with_sep spc pp_lbl (Array.to_list lblt) ++ str " bodies = " ++ prlist_with_sep spc pp_lbl (Array.to_list lblb)) - | Kgetglobal idu -> str "getglobal " ++ pr_con idu + | Kgetglobal idu -> str "getglobal " ++ Constant.print idu | Kconst sc -> str "const " ++ pp_struct_const sc | Kmakeblock(n, m) -> diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 718917ab3..5d37a5840 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -9,7 +9,7 @@ (* $Id$ *) open Names -open Term +open Constr type tag = int @@ -26,13 +26,13 @@ val cofix_evaluated_tag : tag val last_variant_tag : tag type structured_constant = - | Const_sorts of sorts + | Const_sorts of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.universe_level - | Const_type of Univ.universe + | Const_univ_level of Univ.Level.t + | Const_type of Univ.Universe.t val pp_struct_const : structured_constant -> Pp.t @@ -69,7 +69,7 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of Constant.t | Kconst of structured_constant | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0 ** is accu, all others are popped from diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index d63fcffa2..5dab2932d 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -14,7 +14,7 @@ open Util open Names open Cbytecodes open Cemitcodes -open Term +open Constr open Declarations open Pre_env @@ -438,12 +438,12 @@ let get_strcst = function | _ -> raise Not_found let rec str_const c = - match kind_of_term c with + match kind c with | Sort s -> Bstrconst (Const_sorts s) | Cast(c,_,_) -> str_const c | App(f,args) -> begin - match kind_of_term f with + match kind f with | Construct(((kn,j),i),u) -> begin let oib = lookup_mind kn !global_env in @@ -596,7 +596,7 @@ let rec get_alias env kn = (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = set_max_stack_size sz; - match kind_of_term c with + match kind c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" | Proj (p,c) -> @@ -621,9 +621,9 @@ let rec compile_constr reloc c sz cont = (Univ.Instance.to_array u) sz cont - | Sort (Prop _) | Construct _ -> + | Sort (Sorts.Prop _) | Construct _ -> compile_str_cst reloc (str_const c) sz cont - | Sort (Type u) -> + | Sort (Sorts.Type u) -> (* We separate global and local universes in [u]. The former will be part of the structured constant, while the later (if any) will be applied as arguments. *) @@ -641,7 +641,7 @@ let rec compile_constr reloc c sz cont = LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m in if local_levels = [] then - compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont + compile_str_cst reloc (Bstrconst (Const_sorts (Sorts.Type uglob))) sz cont else let compile_get_univ reloc idx sz cont = set_max_stack_size sz; @@ -659,7 +659,7 @@ let rec compile_constr reloc c sz cont = Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in compile_constr reloc (mkLambda(id,dom,codom)) sz cont1 | Lambda _ -> - let params, body = decompose_lam c in + let params, body = Term.decompose_lam c in let arity = List.length params in let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in @@ -672,7 +672,7 @@ let rec compile_constr reloc c sz cont = | App(f,args) -> begin - match kind_of_term f with + match kind f with | Construct _ -> compile_str_cst reloc (str_const c) sz cont | Const (kn,u) -> compile_const reloc kn u args sz cont | _ -> comp_app compile_constr compile_constr reloc f args sz cont @@ -694,7 +694,7 @@ let rec compile_constr reloc c sz cont = done; (* Compiling bodies *) for i = 0 to ndef - 1 do - let params,body = decompose_lam rec_bodies.(i) in + let params,body = Term.decompose_lam rec_bodies.(i) in let arity = List.length params in let env_body = comp_env_fix ndef i arity rfv in let cont1 = @@ -726,7 +726,7 @@ let rec compile_constr reloc c sz cont = done; (* Compiling bodies *) for i = 0 to ndef - 1 do - let params,body = decompose_lam rec_bodies.(i) in + let params,body = Term.decompose_lam rec_bodies.(i) in let arity = List.length params in let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in @@ -792,7 +792,7 @@ let rec compile_constr reloc c sz cont = lbl_consts.(tag) <- lbl_b; c := code_b else - let args, body = decompose_lam branchs.(i) in + let args, body = Term.decompose_lam branchs.(i) in let nargs = List.length args in let code_b = @@ -953,9 +953,9 @@ let compile fail_on_error ?universes:(universes=0) env c = *) let reloc = empty_comp_env () in let arity , body = - match kind_of_term c with + match kind c with | Lambda _ -> - let params, body = decompose_lam c in + let params, body = Term.decompose_lam c in List.length params , body | _ -> 0 , c in @@ -995,10 +995,10 @@ let compile_constant_body fail_on_error env univs = function | Monomorphic_const _ -> 0 | Polymorphic_const univ -> Univ.AUContext.size univ in - match kind_of_term body with + match kind body with | Const (kn',u) when is_univ_copy instance_size u -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con kn') in + let con= Constant.make1 (Constant.canonical kn') in Some (BCalias (get_alias env con)) | _ -> let res = compile fail_on_error ~universes:instance_size env body in @@ -1006,7 +1006,7 @@ let compile_constant_body fail_on_error env univs = function (* Shortcut of the previous function used during module strengthening *) -let compile_alias kn = BCalias (constant_of_kn (canonical_con kn)) +let compile_alias kn = BCalias (Constant.make1 (Constant.canonical kn)) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) @@ -1024,7 +1024,7 @@ let compile_structured_int31 fc args = if not fc then raise Not_found else Const_b0 (Array.fold_left - (fun temp_i -> fun t -> match kind_of_term t with + (fun temp_i -> fun t -> match kind t with | Construct ((_,d),_) -> 2*temp_i+d-1 | _ -> raise NotClosed) 0 args diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 48c2e4533..c117d3fb5 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,6 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + open Cbytecodes open Cemitcodes -open Term +open Constr open Declarations open Pre_env @@ -14,7 +22,7 @@ val compile_constant_body : bool -> (** Shortcut of the previous function used during module strengthening *) -val compile_alias : Names.constant -> body_code +val compile_alias : Names.Constant.t -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 092bcecc3..eeea19c12 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of Names.constant + | Reloc_getglobal of Names.Constant.t type patch = reloc_info * int @@ -348,12 +348,12 @@ let subst_to_patch s (code,pl,fv) = type body_code = | BCdefined of to_patch - | BCalias of Names.constant + | BCalias of Names.Constant.t | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of Names.constant substituted +| PBCalias of Names.Constant.t substituted | PBCconstant let from_val = function diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index c80edd596..fee45aafd 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of Constant.t type patch = reloc_info * int @@ -23,7 +23,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCalias of constant + | BCalias of Constant.t | BCconstant diff --git a/kernel/constr.ml b/kernel/constr.ml index c3e609536..5930cfadc 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -75,7 +75,7 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type 'a puniverses = 'a Univ.puniverses -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array @@ -233,7 +233,6 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id - (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -250,6 +249,168 @@ let of_kind = function | Cast (c, knd, t) -> mkCast (c, knd, t) | k -> k +(**********************************************************************) +(* Non primitive term destructors *) +(**********************************************************************) + +(* Destructor operations : partial functions + Raise [DestKO] if the const has not the expected form *) + +exception DestKO + +let isMeta c = match kind c with Meta _ -> true | _ -> false + +(* Destructs a type *) +let isSort c = match kind c with + | Sort _ -> true + | _ -> false + +let rec isprop c = match kind c with + | Sort (Sorts.Prop _) -> true + | Cast (c,_,_) -> isprop c + | _ -> false + +let rec is_Prop c = match kind c with + | Sort (Sorts.Prop Sorts.Null) -> true + | Cast (c,_,_) -> is_Prop c + | _ -> false + +let rec is_Set c = match kind c with + | Sort (Sorts.Prop Sorts.Pos) -> true + | Cast (c,_,_) -> is_Set c + | _ -> false + +let rec is_Type c = match kind c with + | Sort (Sorts.Type _) -> true + | Cast (c,_,_) -> is_Type c + | _ -> false + +let is_small = Sorts.is_small +let iskind c = isprop c || is_Type c + +(* Tests if an evar *) +let isEvar c = match kind c with Evar _ -> true | _ -> false +let isEvar_or_Meta c = match kind c with + | Evar _ | Meta _ -> true + | _ -> false + +let isCast c = match kind c with Cast _ -> true | _ -> false +(* Tests if a de Bruijn index *) +let isRel c = match kind c with Rel _ -> true | _ -> false +let isRelN n c = + match kind c with Rel n' -> Int.equal n n' | _ -> false +(* Tests if a variable *) +let isVar c = match kind c with Var _ -> true | _ -> false +let isVarId id c = match kind c with Var id' -> Id.equal id id' | _ -> false +(* Tests if an inductive *) +let isInd c = match kind c with Ind _ -> true | _ -> false +let isProd c = match kind c with | Prod _ -> true | _ -> false +let isLambda c = match kind c with | Lambda _ -> true | _ -> false +let isLetIn c = match kind c with LetIn _ -> true | _ -> false +let isApp c = match kind c with App _ -> true | _ -> false +let isConst c = match kind c with Const _ -> true | _ -> false +let isConstruct c = match kind c with Construct _ -> true | _ -> false +let isCase c = match kind c with Case _ -> true | _ -> false +let isProj c = match kind c with Proj _ -> true | _ -> false +let isFix c = match kind c with Fix _ -> true | _ -> false +let isCoFix c = match kind c with CoFix _ -> true | _ -> false + +(* Destructs a de Bruijn index *) +let destRel c = match kind c with + | Rel n -> n + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destMeta c = match kind c with + | Meta n -> n + | _ -> raise DestKO + +(* Destructs a variable *) +let destVar c = match kind c with + | Var id -> id + | _ -> raise DestKO + +let destSort c = match kind c with + | Sort s -> s + | _ -> raise DestKO + +(* Destructs a casted term *) +let destCast c = match kind c with + | Cast (t1,k,t2) -> (t1,k,t2) + | _ -> raise DestKO + +(* Destructs the product (x:t1)t2 *) +let destProd c = match kind c with + | Prod (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the abstraction [x:t1]t2 *) +let destLambda c = match kind c with + | Lambda (x,t1,t2) -> (x,t1,t2) + | _ -> raise DestKO + +(* Destructs the let [x:=b:t1]t2 *) +let destLetIn c = match kind c with + | LetIn (x,b,t1,t2) -> (x,b,t1,t2) + | _ -> raise DestKO + +(* Destructs an application *) +let destApp c = match kind c with + | App (f,a) -> (f, a) + | _ -> raise DestKO + +(* Destructs a constant *) +let destConst c = match kind c with + | Const kn -> kn + | _ -> raise DestKO + +(* Destructs an existential variable *) +let destEvar c = match kind c with + | Evar (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a (co)inductive type named kn *) +let destInd c = match kind c with + | Ind (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a constructor *) +let destConstruct c = match kind c with + | Construct (kn, a as r) -> r + | _ -> raise DestKO + +(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) +let destCase c = match kind c with + | Case (ci,p,c,v) -> (ci,p,c,v) + | _ -> raise DestKO + +let destProj c = match kind c with + | Proj (p, c) -> (p, c) + | _ -> raise DestKO + +let destFix c = match kind c with + | Fix fix -> fix + | _ -> raise DestKO + +let destCoFix c = match kind c with + | CoFix cofix -> cofix + | _ -> raise DestKO + + +(******************************************************************) +(* Flattening and unflattening of embedded applications and casts *) +(******************************************************************) + +let decompose_app c = + match kind c with + | App (f,cl) -> (f, Array.to_list cl) + | _ -> (c,[]) + +let decompose_appvect c = + match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) + (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -513,6 +674,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = | Prod (_,t1,c1), Prod (_,t2,c2) -> eq t1 t2 && leq c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq t1 t2 && eq c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq b1 b2 && eq t1 t2 && leq c1 c2 + (* Why do we suddenly make a special case for Cast here? *) | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2 | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2)) | App (c1,l1), App (c2,l2) -> @@ -520,7 +682,7 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = eq c1 c2 && Array.equal_norefl eq l1 l2 | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2 | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2 - | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2 + | Const (c1,u1), Const (c2,u2) -> Constant.equal c1 c2 && eq_universes true u1 u2 | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2 | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> @@ -530,7 +692,9 @@ let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2 - | _ -> false + | (Rel _ | Meta _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | App _ + | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ | Fix _ + | CoFix _), _ -> false (* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity, @@ -650,9 +814,6 @@ let always_true _ _ = true let rec eq_constr_nounivs m n = (m == n) || compare_head_gen (fun _ -> always_true) always_true eq_constr_nounivs m n -(** We only use this function over blocks! *) -let tag t = Obj.tag (Obj.repr t) - let constr_ord_int f t1 t2 = let (=?) f g i1 i2 j1 j2= let c = f i1 i2 in @@ -664,35 +825,50 @@ let constr_ord_int f t1 t2 = ((Array.compare Int.compare) =? Int.compare) a1 a2 i1 i2 in match kind t1, kind t2 with + | Cast (c1,_,_), _ -> f c1 t2 + | _, Cast (c2,_,_) -> f t1 c2 + (* Why this special case? *) + | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 + | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) | Rel n1, Rel n2 -> Int.compare n1 n2 - | Meta m1, Meta m2 -> Int.compare m1 m2 + | Rel _, _ -> -1 | _, Rel _ -> 1 | Var id1, Var id2 -> Id.compare id1 id2 + | Var _, _ -> -1 | _, Var _ -> 1 + | Meta m1, Meta m2 -> Int.compare m1 m2 + | Meta _, _ -> -1 | _, Meta _ -> 1 + | Evar (e1,l1), Evar (e2,l2) -> + (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 + | Evar _, _ -> -1 | _, Evar _ -> 1 | Sort s1, Sort s2 -> Sorts.compare s1 s2 - | Cast (c1,_,_), _ -> f c1 t2 - | _, Cast (c2,_,_) -> f t1 c2 + | Sort _, _ -> -1 | _, Sort _ -> 1 | Prod (_,t1,c1), Prod (_,t2,c2) | Lambda (_,t1,c1), Lambda (_,t2,c2) -> (f =? f) t1 t2 c1 c2 + | Prod _, _ -> -1 | _, Prod _ -> 1 + | Lambda _, _ -> -1 | _, Lambda _ -> 1 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> ((f =? f) ==? f) b1 b2 t1 t2 c1 c2 - | App (Cast(c1,_,_),l1), _ -> f (mkApp (c1,l1)) t2 - | _, App (Cast(c2, _,_),l2) -> f t1 (mkApp (c2,l2)) + | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 - | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 - | Evar (e1,l1), Evar (e2,l2) -> - (Evar.compare =? (Array.compare f)) e1 e2 l1 l2 - | Const (c1,u1), Const (c2,u2) -> con_ord c1 c2 + | App _, _ -> -1 | _, App _ -> 1 + | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const _, _ -> -1 | _, Const _ -> 1 | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind _, _ -> -1 | _, Ind _ -> 1 | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 + | Case _, _ -> -1 | _, Case _ -> 1 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> ((fix_cmp =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 + | Fix _, _ -> -1 | _, Fix _ -> 1 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> ((Int.compare =? (Array.compare f)) ==? (Array.compare f)) ln1 ln2 tl1 tl2 bl1 bl2 - | t1, t2 -> Int.compare (tag t1) (tag t2) + | CoFix _, _ -> -1 | _, CoFix _ -> 1 + | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2 let rec compare m n= constr_ord_int compare m n @@ -776,7 +952,9 @@ let hasheq t1 t2 = && array_eqeq lna1 lna2 && array_eqeq tl1 tl2 && array_eqeq bl1 bl2 - | _ -> false + | (Rel _ | Meta _ | Var _ | Sort _ | Cast _ | Prod _ | Lambda _ | LetIn _ + | App _ | Proj _ | Evar _ | Const _ | Ind _ | Construct _ | Case _ + | Fix _ | CoFix _), _ -> false (** Note that the following Make has the side effect of creating once and for all the table we'll use for hash-consing all constr *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 76dbf5530..21c477578 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -13,20 +13,22 @@ open Names (** {6 Value under universe substitution } *) type 'a puniverses = 'a Univ.puniverses +[@@ocaml.deprecated "use Univ.puniverses"] (** {6 Simply type aliases } *) -type pconstant = constant puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses +type pconstant = Constant.t Univ.puniverses +type pinductive = inductive Univ.puniverses +type pconstructor = constructor Univ.puniverses (** {6 Existential variables } *) type existential_key = Evar.t +[@@ocaml.deprecated "use Evar.t"] (** {6 Existential variables } *) type metavariable = int (** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) @@ -80,14 +82,14 @@ val mkVar : Id.t -> constr val mkMeta : metavariable -> constr (** Constructs an existential variable *) -type existential = existential_key * constr array +type existential = Evar.t * constr array val mkEvar : existential -> constr (** Construct a sort *) val mkSort : Sorts.t -> types val mkProp : types val mkSet : types -val mkType : Univ.universe -> types +val mkType : Univ.Universe.t -> types (** This defines the strategy to use for verifiying a Cast *) @@ -111,10 +113,10 @@ val mkLetIn : Name.t * constr * types * constr -> constr {%latex:$(f~t_1\dots f_n)$%}. *) val mkApp : constr * constr array -> constr -val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses +val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -(** Constructs a constant *) -val mkConst : constant -> constr +(** Constructs a Constant.t *) +val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) @@ -180,7 +182,7 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type 'constr pexistential = Evar.t * 'constr array type ('constr, 'types) prec_declaration = Name.t array * 'types array * 'constr array type ('constr, 'types) pfixpoint = @@ -208,7 +210,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of (constant * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + | Const of (Constant.t * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) @@ -225,6 +227,110 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr +(** {6 Simple case analysis} *) +val isRel : constr -> bool +val isRelN : int -> constr -> bool +val isVar : constr -> bool +val isVarId : Id.t -> constr -> bool +val isInd : constr -> bool +val isEvar : constr -> bool +val isMeta : constr -> bool +val isEvar_or_Meta : constr -> bool +val isSort : constr -> bool +val isCast : constr -> bool +val isApp : constr -> bool +val isLambda : constr -> bool +val isLetIn : constr -> bool +val isProd : constr -> bool +val isConst : constr -> bool +val isConstruct : constr -> bool +val isFix : constr -> bool +val isCoFix : constr -> bool +val isCase : constr -> bool +val isProj : constr -> bool + +val is_Prop : constr -> bool +val is_Set : constr -> bool +val isprop : constr -> bool +val is_Type : constr -> bool +val iskind : constr -> bool +val is_small : Sorts.t -> bool + +(** {6 Term destructors } *) +(** Destructor operations are partial functions and + @raise DestKO if the term has not the expected form. *) + +exception DestKO + +(** Destructs a de Bruijn index *) +val destRel : constr -> int + +(** Destructs an existential variable *) +val destMeta : constr -> metavariable + +(** Destructs a variable *) +val destVar : constr -> Id.t + +(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether + [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) +val destSort : constr -> Sorts.t + +(** Destructs a casted term *) +val destCast : constr -> constr * cast_kind * constr + +(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) +val destProd : types -> Name.t * types * types + +(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) +val destLambda : constr -> Name.t * types * constr + +(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) +val destLetIn : constr -> Name.t * constr * types * constr + +(** Destructs an application *) +val destApp : constr -> constr * constr array + +(** Decompose any term as an applicative term; the list of args can be empty *) +val decompose_app : constr -> constr * constr list + +(** Same as [decompose_app], but returns an array. *) +val decompose_appvect : constr -> constr * constr array + +(** Destructs a constant *) +val destConst : constr -> Constant.t Univ.puniverses + +(** Destructs an existential variable *) +val destEvar : constr -> existential + +(** Destructs a (co)inductive type *) +val destInd : constr -> inductive Univ.puniverses + +(** Destructs a constructor *) +val destConstruct : constr -> constructor Univ.puniverses + +(** Destructs a [match c as x in I args return P with ... | +Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args +return P in t1], or [if c then t1 else t2]) +@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] +where [info] is pretty-printing information *) +val destCase : constr -> case_info * constr * constr * constr array + +(** Destructs a projection *) +val destProj : constr -> projection * constr + +(** Destructs the {% $ %}i{% $ %}th function of the block + [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} + with f{_ 2} ctx{_ 2} = b{_ 2} + ... + with f{_ n} ctx{_ n} = b{_ n}], + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. +*) +val destFix : constr -> fixpoint + +val destCoFix : constr -> cofixpoint + +(** {6 Equality} *) + (** [equal a b] is true if [a] equals [b] modulo alpha, casts, and application grouping *) val equal : constr -> constr -> bool @@ -302,7 +408,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances (the first boolean tells if they belong to a constant), [s] to + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) @@ -335,7 +441,7 @@ val compare_head_gen_with : (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for conversion, [fle] for cumulativity, [u] to compare universe - instances (the first boolean tells if they belong to a constant), + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) @@ -344,7 +450,7 @@ val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) (constr -> constr -> bool) -> (constr -> constr -> bool) -> constr -> constr -> bool - + (** {6 Hashconsing} *) val hash : constr -> int diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 248cd2b30..02c179ab6 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -16,7 +16,7 @@ val empty : oracle If [oracle_order kn1 kn2] is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) -val oracle_order : ('a -> constant) -> oracle -> bool -> +val oracle_order : ('a -> Constant.t) -> oracle -> bool -> 'a tableKey -> 'a tableKey -> bool (** Priority for the expansion of constant in the conversion test. @@ -30,14 +30,14 @@ val transparent : level (** Check whether a level is transparent *) val is_transparent : level -> bool -val get_strategy : oracle -> constant tableKey -> level +val get_strategy : oracle -> Constant.t tableKey -> level (** Sets the level of a constant. * Level of RelKey constant cannot be set. *) -val set_strategy : oracle -> constant tableKey -> level -> oracle +val set_strategy : oracle -> Constant.t tableKey -> level -> oracle (** Fold over the non-transparent levels of the oracle. Order unspecified. *) -val fold_strategy : (constant tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a +val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> transparent_state diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 80d41847c..7b921d35b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -17,6 +17,7 @@ open CErrors open Util open Names open Term +open Constr open Declarations open Univ @@ -29,15 +30,15 @@ let pop_dirpath p = match DirPath.repr p with | _::l -> DirPath.make l let pop_mind kn = - let (mp,dir,l) = Names.repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_con con = - let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l type my_global_reference = - | ConstRef of constant + | ConstRef of Constant.t | IndRef of inductive | ConstructRef of constructor @@ -100,42 +101,42 @@ let expmod_constr cache modlist c = let share_univs = share_univs cache in let update_case_info = update_case_info cache in let rec substrec c = - match kind_of_term c with + match kind c with | Case (ci,p,t,br) -> - map_constr substrec (mkCase (update_case_info ci modlist,p,t,br)) + Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br)) | Ind (ind,u) -> (try share_univs (IndRef ind) u modlist with - | Not_found -> map_constr substrec c) + | Not_found -> Constr.map substrec c) | Construct (cstr,u) -> (try share_univs (ConstructRef cstr) u modlist with - | Not_found -> map_constr substrec c) + | Not_found -> Constr.map substrec c) | Const (cst,u) -> (try share_univs (ConstRef cst) u modlist with - | Not_found -> map_constr substrec c) + | Not_found -> Constr.map substrec c) | Proj (p, c') -> (try let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in let make c = Projection.make c (Projection.unfolded p) in - match kind_of_term p' with + match kind p' with | Const (p',_) -> mkProj (make p', substrec c') | App (f, args) -> - (match kind_of_term f with + (match kind f with | Const (p', _) -> mkProj (make p', substrec c') | _ -> assert false) | _ -> assert false - with Not_found -> map_constr substrec c) + with Not_found -> Constr.map substrec c) - | _ -> map_constr substrec c + | _ -> Constr.map substrec c in if is_empty_modlist modlist then c @@ -203,7 +204,7 @@ let cook_constant ~hcons env { from = cb; info } = let hyps = Context.Named.map expmod abstract in let map c = let c = abstract_constant_body (expmod c) hyps in - if hcons then hcons_constr c else c + if hcons then Constr.hcons c else c in let body = on_body modlist (hyps, usubst, abs_ctx) map @@ -222,7 +223,7 @@ let cook_constant ~hcons env { from = cb; info } = let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind_of_term c' with + match kind c' with | App (f,l) -> (destInd f, Array.length l) | Ind ind -> ind, 0 | _ -> assert false @@ -249,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 6d1b776c0..7696d7545 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Declarations open Environ @@ -26,7 +26,7 @@ type result = { } val cook_constant : hcons:bool -> env -> recipe -> result -val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr +val cook_constr : Opaqueproof.cooking_info -> constr -> constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index d21ea9670..2ffe36fcf 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -14,7 +14,7 @@ open Util open Names -open Term +open Constr open Vm open Cemitcodes open Cbytecodes @@ -68,7 +68,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 | Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2 +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false | Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 | Const_type _ , _ -> false diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 633cf0abd..91bb30e7e 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -9,10 +9,10 @@ (* $Id$ *) open Names -open Term +open Constr open Pre_env val val_of_constr : env -> constr -> values -val set_opaque_const : constant -> unit -val set_transparent_const : constant -> unit +val set_opaque_const : Constant.t -> unit +val set_transparent_const : Constant.t -> unit diff --git a/kernel/declarations.ml b/kernel/declarations.ml index e17fb1c38..7f4b85fd0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr (** This module defines the internal representation of global declarations. This includes global constants/axioms, mutual @@ -28,8 +28,8 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.universe_level option list; - template_level : Univ.universe; + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; } type ('a, 'b) declaration_arity = @@ -48,7 +48,7 @@ type inline = int option always transparent. *) type projection_body = { - proj_ind : mutual_inductive; + proj_ind : MutInd.t; proj_npars : int; proj_arg : int; proj_type : types; (* Type under params *) @@ -63,8 +63,8 @@ type constant_def = | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = - | Monomorphic_const of Univ.universe_context - | Polymorphic_const of Univ.abstract_universe_context + | Monomorphic_const of Univ.ContextSet.t + | Polymorphic_const of Univ.AUContext.t (** The [typing_flags] are instructions to the type-checker which modify its behaviour. The typing flags used in the type-checking @@ -115,11 +115,11 @@ v} - The constants associated to each projection. - The checked projection bodies. *) -type record_body = (Id.t * constant array * projection_body array) option +type record_body = (Id.t * Constant.t array * projection_body array) option type regular_inductive_arity = { mind_user_arity : types; - mind_sort : sorts; + mind_sort : Sorts.t; } type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity @@ -146,7 +146,7 @@ type one_inductive_body = { mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) - mind_kelim : sorts_family list; (** List of allowed elimination sorts *) + mind_kelim : Sorts.family list; (** List of allowed elimination sorts *) mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *) @@ -168,9 +168,14 @@ type one_inductive_body = { } type abstract_inductive_universes = - | Monomorphic_ind of Univ.universe_context - | Polymorphic_ind of Univ.abstract_universe_context - | Cumulative_ind of Univ.abstract_cumulativity_info + | Monomorphic_ind of Univ.ContextSet.t + | Polymorphic_ind of Univ.AUContext.t + | Cumulative_ind of Univ.ACumulativityInfo.t + +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) type mutual_inductive_body = { @@ -178,7 +183,7 @@ type mutual_inductive_body = { mind_record : record_body option; (** The record information *) - mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) @@ -212,12 +217,12 @@ type ('ty,'a) functorize = only for short module printing and for extraction. *) type with_declaration = - | WithMod of Id.t list * module_path + | WithMod of Id.t list * ModPath.t | WithDef of Id.t list * constr Univ.in_universe_context type module_alg_expr = - | MEident of module_path - | MEapply of module_alg_expr * module_path + | MEident of ModPath.t + | MEapply of module_alg_expr * ModPath.t | MEwith of module_alg_expr * with_declaration (** A component of a module structure *) @@ -251,7 +256,7 @@ and module_implementation = | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) and 'a generic_module_body = - { mod_mp : module_path; (** absolute path of the module *) + { mod_mp : ModPath.t; (** absolute path of the module *) mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) @@ -290,5 +295,5 @@ and _ module_retroknowledge = - A module application is atomic, for instance ((M N) P) : * the head of [MEapply] can only be another [MEapply] or a [MEident] - * the argument of [MEapply] is now directly forced to be a [module_path]. + * the argument of [MEapply] is now directly forced to be a [ModPath.t]. *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 66d66c7d0..d8768a0fc 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -112,7 +112,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types + RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons let hcons_rel_context l = List.smartmap hcons_rel_decl l @@ -120,20 +120,20 @@ let hcons_const_def = function | Undef inl -> Undef inl | Def l_constr -> let constr = force_constr l_constr in - Def (from_val (Term.hcons_constr constr)) + Def (from_val (Constr.hcons constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context ctx) + Monomorphic_const (Univ.hcons_universe_context_set ctx) | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; - const_type = Term.hcons_constr cb.const_type; + const_type = Constr.hcons cb.const_type; const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -249,8 +249,8 @@ let inductive_is_cumulative mib = (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = - { mind_user_arity = Term.hcons_constr a.mind_user_arity; - mind_sort = Term.hcons_sorts a.mind_sort } + { mind_user_arity = Constr.hcons a.mind_user_arity; + mind_sort = Sorts.hcons a.mind_sort } (** Just as for constants, this hash-consing is quite partial *) @@ -260,8 +260,8 @@ let hcons_ind_arity = (** Substitution of inductive declarations *) let hcons_mind_packet oib = - let user = Array.smartmap Term.hcons_types oib.mind_user_lc in - let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in + let user = Array.smartmap Constr.hcons oib.mind_user_lc in + let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) let nf = if Array.equal (==) user nf then user else nf in { oib with @@ -274,7 +274,7 @@ let hcons_mind_packet oib = let hcons_mind_universes miu = match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) @@ -287,9 +287,9 @@ let hcons_mind mib = (** {6 Stm machinery } *) let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" (** Hashconsing of modules *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index b2d29759d..198831848 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -27,7 +27,7 @@ val subst_const_body : substitution -> constant_body -> constant_body val constant_has_body : constant_body -> bool -val constant_polymorphic_context : constant_body -> abstract_universe_context +val constant_polymorphic_context : constant_body -> AUContext.t (** Is the constant polymorphic? *) val constant_is_polymorphic : constant_body -> bool @@ -57,7 +57,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body -val inductive_polymorphic_context : mutual_inductive_body -> abstract_universe_context +val inductive_polymorphic_context : mutual_inductive_body -> AUContext.t (** Is the inductive polymorphic? *) val inductive_is_polymorphic : mutual_inductive_body -> bool diff --git a/kernel/entries.ml b/kernel/entries.ml index a1ccbdbc1..ca79de404 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr (** This module defines the entry types for global declarations. This information is entered in the environments. This includes global @@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; *) type inductive_universes = - | Monomorphic_ind_entry of Univ.universe_context - | Polymorphic_ind_entry of Univ.universe_context - | Cumulative_ind_entry of Univ.cumulativity_info + | Monomorphic_ind_entry of Univ.ContextSet.t + | Polymorphic_ind_entry of Univ.UContext.t + | Cumulative_ind_entry of Univ.CumulativityInfo.t type one_inductive_entry = { mind_entry_typename : Id.t; @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -65,8 +65,10 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = - | Monomorphic_const_entry of Univ.universe_context - | Polymorphic_const_entry of Univ.universe_context + | Monomorphic_const_entry of Univ.ContextSet.t + | Polymorphic_const_entry of Univ.UContext.t + +type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; @@ -82,10 +84,10 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.Named.t option * bool * types Univ.in_universe_context * inline + Context.Named.t option * types in_constant_universes_entry * inline type projection_entry = { - proj_entry_ind : mutual_inductive; + proj_entry_ind : MutInd.t; proj_entry_arg : int } type 'a constant_entry = @@ -112,11 +114,11 @@ type seff_env = [ `Nothing (* The proof term and its universes. Same as the constant_body's but not in an ephemeron *) - | `Opaque of Constr.t * Univ.universe_context_set ] + | `Opaque of Constr.t * Univ.ContextSet.t ] type side_eff = - | SEsubproof of constant * Declarations.constant_body * seff_env - | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + | SEsubproof of Constant.t * Declarations.constant_body * seff_env + | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string type side_effect = { from_env : Declarations.structure_body CEphemeron.key; diff --git a/kernel/environ.ml b/kernel/environ.ml index c3fd8962e..1afab453a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -23,7 +23,7 @@ open CErrors open Util open Names -open Term +open Constr open Vars open Declarations open Pre_env @@ -391,7 +391,7 @@ let lookup_constructor_variables (ind,_) env = (* Returns the list of global variables in a term *) let vars_of_global env constr = - match kind_of_term constr with + match kind constr with Var id -> Id.Set.singleton id | Const (kn, _) -> lookup_constant_variables kn env | Ind (ind, _) -> lookup_inductive_variables ind env @@ -402,12 +402,12 @@ let vars_of_global env constr = let global_vars_set env constr = let rec filtrec acc c = let acc = - match kind_of_term c with + match kind c with | Var _ | Const _ | Ind _ | Construct _ -> Id.Set.union (vars_of_global env c) acc | _ -> acc in - Term.fold_constr filtrec acc c + Constr.fold filtrec acc c in filtrec Id.Set.empty constr @@ -478,7 +478,7 @@ let j_type j = j.uj_type type 'types punsafe_type_judgment = { utj_val : 'types; - utj_type : sorts } + utj_type : Sorts.t } type unsafe_type_judgment = types punsafe_type_judgment @@ -538,7 +538,7 @@ let register_one env field entry = let register env field entry = match field with | KInt31 (grp, Int31Type) -> - let i31c = match kind_of_term entry with + let i31c = match kind entry with | Ind i31t -> mkConstructUi (i31t, 1) | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.") in @@ -584,7 +584,7 @@ let dispatch = fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = - match kind_of_term value with + match kind value with | Const kn -> int31_op n op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.") in @@ -601,13 +601,13 @@ fun rk value field -> (Pp.str "add_int31_decompilation_from_type called with an abnormal field.") in let i31bit_type = - match kind_of_term int31bit with + match kind int31bit with | Ind (i31bit_type,_) -> i31bit_type | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type.") in let int31_decompilation = - match kind_of_term value with + match kind value with | Ind (i31t,_) -> constr_of_int31 i31t i31bit_type | _ -> anomaly ~label:"Environ.register" diff --git a/kernel/environ.mli b/kernel/environ.mli index 2667ad7ca..7cc541258 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -7,9 +7,9 @@ (************************************************************************) open Names -open Term -open Declarations +open Constr open Univ +open Declarations (** Unsafe environments. We define here a datatype for environments. Since typing is not yet defined, it is not possible to check the @@ -126,19 +126,19 @@ val pop_rel_context : int -> env -> env (** {5 Global constants } {6 Add entries to global environment } *) -val add_constant : constant -> constant_body -> env -> env -val add_constant_key : constant -> constant_body -> Pre_env.link_info -> +val add_constant : Constant.t -> constant_body -> env -> env +val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info -> env -> env (** Looks up in the context of global constant names raises [Not_found] if the required path is not found *) -val lookup_constant : constant -> env -> constant_body -val evaluable_constant : constant -> env -> bool +val lookup_constant : Constant.t -> env -> constant_body +val evaluable_constant : Constant.t -> env -> bool (** New-style polymorphism *) -val polymorphic_constant : constant -> env -> bool +val polymorphic_constant : Constant.t -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool -val type_in_type_constant : constant -> env -> bool +val type_in_type_constant : Constant.t -> env -> bool (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if @@ -149,35 +149,35 @@ val type_in_type_constant : constant -> env -> bool type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> types constrained +val constant_value : env -> Constant.t puniverses -> constr constrained +val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option -val constant_value_and_type : env -> constant puniverses -> - constr option * types * Univ.constraints +val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option +val constant_value_and_type : env -> Constant.t puniverses -> + constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not polymorphic *) -val constant_context : env -> constant -> Univ.abstract_universe_context +val constant_context : env -> Constant.t -> Univ.AUContext.t (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) -val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> types -val constant_opt_value_in : env -> constant puniverses -> constr option +val constant_value_in : env -> Constant.t puniverses -> constr +val constant_type_in : env -> Constant.t puniverses -> types +val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) val lookup_projection : Names.projection -> env -> projection_body -val is_projection : constant -> env -> bool +val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) -val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env -val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env +val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env +val add_mind : MutInd.t -> mutual_inductive_body -> env -> env (** Looks up in the context of global inductive names raises [Not_found] if the required path is not found *) -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind : MutInd.t -> env -> mutual_inductive_body (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool @@ -195,20 +195,20 @@ val add_modtype : module_type_body -> env -> env (** [shallow_add_module] does not add module components *) val shallow_add_module : module_body -> env -> env -val lookup_module : module_path -> env -> module_body -val lookup_modtype : module_path -> env -> module_type_body +val lookup_module : ModPath.t -> env -> module_body +val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. @raises UniverseInconsistency *) -val add_constraints : Univ.constraints -> env -> env +val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) -val check_constraints : Univ.constraints -> env -> bool -val push_context : ?strict:bool -> Univ.universe_context -> env -> env -val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env +val check_constraints : Univ.Constraint.t -> env -> bool +val push_context : ?strict:bool -> Univ.UContext.t -> env -> env +val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env @@ -247,7 +247,7 @@ val j_type : ('constr, 'types) punsafe_judgment -> 'types type 'types punsafe_type_judgment = { utj_val : 'types; - utj_type : sorts } + utj_type : Sorts.t } type unsafe_type_judgment = types punsafe_type_judgment diff --git a/kernel/evar.ml b/kernel/evar.ml index e63665f51..dcd2e12a0 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -13,6 +13,7 @@ let unsafe_of_int x = x let compare = Int.compare let equal = Int.equal let hash = Int.hash +let print x = Pp.(str "?X" ++ int x) module Set = Int.Set module Map = Int.Map diff --git a/kernel/evar.mli b/kernel/evar.mli index eee6680fb..6a058207f 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -30,5 +30,8 @@ val compare : t -> t -> int val hash : t -> int (** Hash over existential variables. *) +val print : t -> Pp.t +(** Printing representation *) + module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e248436ec..8e9b606a5 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Declarations open Declareops @@ -130,11 +131,11 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = let t = whd_all env t in - match kind_of_term t with + match kind t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in - let max = Universe.sup max (univ_of_sort varj.utj_type) in + let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max @@ -168,7 +169,7 @@ let infer_constructor_packet env_ar_par params lc = let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) - let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in + let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in @@ -183,7 +184,7 @@ let cumulate_arity_large_levels env sign = match d with | LocalAssum (_,t) -> let tj = infer_type env t in - let u = univ_of_sort tj.utj_type in + let u = Sorts.univ_of_sort tj.utj_type in (Universe.sup u lev, push_rel d env) | LocalDef _ -> lev, push_rel d env) @@ -199,8 +200,8 @@ let is_impredicative env u = let param_ccls paramsctxt = let fold acc = function | (LocalAssum (_, p)) -> - (let c = strip_prod_assum p in - match kind_of_term c with + (let c = Term.strip_prod_assum p in + match kind c with | Sort (Type u) -> Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc @@ -208,7 +209,7 @@ let param_ccls paramsctxt = List.fold_left fold [] paramsctxt (* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity = +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = let numchecked = ref 0 in let basic_check ev tp = if !numchecked < numparams then () else conv_leq ev tp (subst tp); @@ -264,13 +265,12 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let univctx = + let env' = match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> ctx - | Polymorphic_ind_entry ctx -> ctx - | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry ctx -> push_context ctx env + | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env in - let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -288,7 +288,7 @@ let typecheck_inductive env mie = (** We have an algebraic universe as the conclusion of the arity, typecheck the dummy Î ctx, Prop and do a special case for the conclusion. *) - let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in + let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in let (cctx, _) = destArity proparity.utj_val in (* Any universe is well-formed, we don't need to check [s] here *) mkArity (cctx, s) @@ -350,7 +350,7 @@ let typecheck_inductive env mie = | None -> clev in let full_polymorphic () = - let defu = Term.univ_of_sort def_level in + let defu = Sorts.univ_of_sort def_level in let is_natural = type_in_type env || (UGraph.check_leq (universes env') infu defu) in @@ -468,7 +468,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = | LocalDef _ :: paramdecls -> check param_index (paramdecl_index+1) paramdecls | _::paramdecls -> - match kind_of_term (whd_all env params.(param_index)) with + match kind (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -495,7 +495,7 @@ if Int.equal nmr 0 then 0 else | (_,[]) -> assert false (* |paramsctxt|>=nmr *) | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) | (p::lp,_::paramsctxt) -> - ( match kind_of_term (whd_all env p) with + ( match kind (whd_all env p) with | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) in find 0 (n-1) (lpar,List.rev paramsctxt) @@ -526,7 +526,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in - match kind_of_term c' with + match kind c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b @@ -555,7 +555,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in (** If one of the inductives of the mutually inductive @@ -663,7 +663,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -746,7 +746,7 @@ let allowed_sorts is_smashed s = as well. *) all_sorts else - match family_of_sort s with + match Sorts.family s with (* Type: all elimination allowed: above and below *) | InType -> all_sorts (* Smashed Set is necessarily impredicative: forbids large elimination *) @@ -787,7 +787,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = - let mp, dp, l = repr_mind kn in + let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) @@ -915,11 +915,11 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let ar = {template_param_levels = paramlevs; template_level = lev} in TemplateArity ar, all_sorts | RegularArity (info,ar,defs) -> - let s = sort_of_univ defs in + let s = Sorts.sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in + mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index e4b7c086a..9a9380adb 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Declarations open Environ open Entries @@ -34,7 +34,7 @@ exception InductiveError of inductive_error (** The following function does checks on inductive declarations. *) -val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body +val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body (** The following enforces a system compatible with the univalent model *) @@ -44,4 +44,4 @@ val is_indices_matter : unit -> bool val compute_projections : pinductive -> Id.t -> Id.t -> int -> Context.Rel.t -> int array -> int array -> Context.Rel.t -> Context.Rel.t -> - (constant array * projection_body array) + (Constant.t array * projection_body array) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a39307368..2a629f00a 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -10,7 +10,7 @@ open CErrors open Util open Names open Univ -open Term +open Constr open Vars open Declarations open Declareops @@ -30,20 +30,20 @@ let lookup_mind_specif env (kn,tyi) = let find_rectype env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found @@ -81,7 +81,7 @@ let instantiate_params full t u args sign = let (rem_args, subs, ty) = Context.Rel.fold_outside (fun decl (largs,subs,ty) -> - match (decl, largs, kind_of_term ty) with + match (decl, largs, kind ty) with | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t) | (LocalDef (_,b,_), _, LetIn(_,_,_,t)) -> (largs, (substl subs (subst_instance_constr u b))::subs, t) @@ -94,9 +94,9 @@ let instantiate_params full t u args sign = substl subs ty let full_inductive_instantiate mib u params sign = - let dummy = prop_sort in - let t = mkArity (Vars.subst_instance_context u sign,dummy) in - fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) + let dummy = Sorts.prop in + let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in + fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = let inst_ind = constructor_instantiate mind u mib t in @@ -128,7 +128,7 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = function +let sort_as_univ = let open Sorts in function | Type u -> u | Prop Null -> Universe.type0m | Prop Pos -> Universe.type0 @@ -192,11 +192,11 @@ let instantiate_universes env ctx ar argsorts = let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) - if is_type0m_univ level then prop_sort + if is_type0m_univ level then Sorts.prop (* Non singleton type not containing types are interpretable in Set *) - else if is_type0_univ level then set_sort + else if is_type0_univ level then Sorts.set (* This is a Type with constraints *) - else Type level + else Sorts.Type level in (ctx, ty) @@ -211,9 +211,9 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) - if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s + if not polyprop && not (is_type0m_univ ar.template_level) && Sorts.is_prop s then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s) + Term.mkArity (List.rev ctx,s) let type_of_inductive env pind = type_of_inductive_gen env pind [||] @@ -233,7 +233,7 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) -let cumulate_constructor_univ u = function +let cumulate_constructor_univ u = let open Sorts in function | Prop Null -> u | Prop Pos -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' @@ -276,8 +276,8 @@ let type_of_constructors (ind,u) (mib,mip) = let inductive_sort_family mip = match mip.mind_arity with - | RegularArity s -> family_of_sort s.mind_sort - | TemplateArity _ -> InType + | RegularArity s -> Sorts.family s.mind_sort + | TemplateArity _ -> Sorts.InType let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip @@ -296,19 +296,20 @@ let is_primitive_record (mib,_) = let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in - applist + Term.applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (sorts_family * sorts_family * arity_error) option +exception LocalArity of (Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = + let open Sorts in let eq_ksort s = match ksort, s with | InProp, InProp | InSet, InSet | InType, InType -> true | _ -> false in - if not (List.exists eq_ksort (elim_sorts specif)) then + if not (CList.exists eq_ksort (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) @@ -316,7 +317,7 @@ let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = let pt' = whd_all env pt in - match kind_of_term pt', ar with + match kind pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = try conv env a1 a1' @@ -325,8 +326,8 @@ let is_correct_arity env c pj ind specif params = (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind_of_term (whd_all env' a2) with - | Sort s -> family_of_sort s + let ksort = match kind (whd_all env' a2) with + | Sort s -> Sorts.family s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in let _ = @@ -351,22 +352,22 @@ let is_correct_arity env c pj ind specif params = let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in - let (cstrsign,ccl) = decompose_prod_assum typi in + let (cstrsign,ccl) = Term.decompose_prod_assum typi in let nargs = Context.Rel.length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in + let dep_cstr = Term.applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in vargs @ [dep_cstr] in - let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in - it_mkProd_or_LetIn base cstrsign in + let base = Term.lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + Term.it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type env n p c realargs = - whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (Term.lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (pind,largs) pj c = let specif = lookup_mind_specif env (fst pind) in @@ -589,7 +590,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in - match kind_of_term c' with + match kind c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b @@ -621,7 +622,7 @@ compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> assert (List.is_empty largs); build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d @@ -680,7 +681,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -709,7 +710,7 @@ let restrict_spec env spec p = let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in let i,args = decompose_app (whd_all env s) in - match kind_of_term i with + match kind i with | Ind i -> begin match spec with | Dead_code -> spec @@ -730,7 +731,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) let f,l = decompose_app (whd_all renv.env t) in - match kind_of_term f with + match kind f with | Rel k -> subterm_var k renv | Case (ci,p,c,lbr) -> let stack' = push_stack_closures renv l stack in @@ -773,7 +774,7 @@ let rec subterm_specif renv stack t = let decrArg = recindxs.(i) in let theBody = bodies.(i) in let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in (* pushing the fix parameters *) let stack' = push_stack_closures renv l stack in let renv'' = push_ctxt_renv renv' sign in @@ -808,8 +809,11 @@ let rec subterm_specif renv stack t = | Dead_code -> Dead_code | Not_subterm -> Not_subterm) + | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ + | Construct _ | CoFix _ -> Not_subterm + + (* Other terms are not subterms *) - | _ -> Not_subterm and lazy_subterm_specif renv stack t = lazy (subterm_specif renv stack t) @@ -857,13 +861,13 @@ let filter_stack_domain env ci p stack = else let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_all env ar in - match stack, kind_of_term t with + match stack, kind t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in let ctx, a = dest_prod_assum env a in let env = push_rel_context ctx env in let ty, args = decompose_app (whd_all env a) in - let elt = match kind_of_term ty with + let elt = match kind ty with | Ind ind -> let spec' = stack_element_specif elt in (match (Lazy.force spec') with @@ -894,7 +898,7 @@ let check_one_fix renv recpos trees def = if noccur_with_meta renv.rel_min nfi t then () else let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in - match kind_of_term f with + match kind f with | Rel p -> (* Test if [p] is a fixpoint (recursive call) *) if renv.rel_min <= p && p < renv.rel_min+nfi then @@ -924,7 +928,7 @@ let check_one_fix renv recpos trees def = | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with FixGuardError _ -> - check_rec_call renv stack (applist(lift p c,l)) + check_rec_call renv stack (Term.applist(lift p c,l)) end | Case (ci,p,c_0,lrest) -> @@ -970,7 +974,7 @@ let check_one_fix renv recpos trees def = if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> - let value = (applist(constant_value_in renv.env cu, l)) in + let value = (Term.applist(constant_value_in renv.env cu, l)) in check_rec_call renv stack value else List.iter (check_rec_call renv []) l @@ -1007,7 +1011,7 @@ let check_one_fix renv recpos trees def = | LocalDef (_,c,_) -> try List.iter (check_rec_call renv []) l with (FixGuardError _) -> - check_rec_call renv stack (applist(c,l)) + check_rec_call renv stack (Term.applist(c,l)) end | Sort _ -> @@ -1022,7 +1026,7 @@ let check_one_fix renv recpos trees def = if Int.equal decr 0 then check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else - match kind_of_term body with + match kind body with | Lambda (x,a,b) -> check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in @@ -1053,7 +1057,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match kind_of_term (whd_all env def) with + match kind (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in @@ -1094,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) @@ -1108,7 +1112,7 @@ let anomaly_ill_typed () = let rec codomain_is_coind env c = let b = whd_all env c in - match kind_of_term b with + match kind b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> @@ -1120,7 +1124,7 @@ let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then let c,args = decompose_app (whd_all env t) in - match kind_of_term c with + match kind c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive call allowed *) @@ -1192,8 +1196,8 @@ let check_one_cofix env nbfix def deftype = | Meta _ -> () | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args - - | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in + | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ + | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in let vlra = lookup_subterms env mind in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 0dfa8db00..8aaeee831 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Univ open Declarations open Environ @@ -32,23 +32,23 @@ type mind_specif = mutual_inductive_body * one_inductive_body val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) -val ind_subst : mutual_inductive -> mutual_inductive_body -> universe_instance -> constr list +val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t -val instantiate_inductive_constraints : - mutual_inductive_body -> universe_instance -> constraints +val instantiate_inductive_constraints : + mutual_inductive_body -> Instance.t -> Constraint.t val constrained_type_of_inductive : env -> mind_specif puniverses -> types constrained -val constrained_type_of_inductive_knowing_parameters : +val constrained_type_of_inductive_knowing_parameters : env -> mind_specif puniverses -> types Lazy.t array -> types constrained val type_of_inductive : env -> mind_specif puniverses -> types -val type_of_inductive_knowing_parameters : +val type_of_inductive_knowing_parameters : env -> ?polyprop:bool -> mind_specif puniverses -> types Lazy.t array -> types -val elim_sorts : mind_specif -> sorts_family list +val elim_sorts : mind_specif -> Sorts.family list val is_private : mind_specif -> bool val is_primitive_record : mind_specif -> bool @@ -65,7 +65,7 @@ val arities_of_constructors : pinductive -> mind_specif -> types array val type_of_constructors : pinductive -> mind_specif -> types array (** Transforms inductive specification into types (in nf) *) -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> types array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> types array val inductive_params : mind_specif -> int @@ -85,9 +85,9 @@ val build_branches_type : constr list -> constr -> types array (** Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> Context.Rel.t * sorts_family +val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family -val inductive_sort_family : one_inductive_body -> sorts_family +val inductive_sort_family : one_inductive_body -> Sorts.family (** Check a [case_info] actually correspond to a Case expression on the given inductive type. *) @@ -111,10 +111,10 @@ val check_cofix : env -> cofixpoint -> unit exception SingletonInductiveBecomesProp of Id.t -val max_inductive_sort : sorts array -> universe +val max_inductive_sort : Sorts.t array -> Universe.t val instantiate_universes : env -> Context.Rel.t -> - template_arity -> constr Lazy.t array -> Context.Rel.t * sorts + template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t (** {6 Debug} *) @@ -135,6 +135,6 @@ type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec -val lambda_implicit_lift : int -> Constr.constr -> Term.constr +val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> Constr.constr array -> Constr.constr array +val abstract_mind_lc : int -> Int.t -> constr array -> constr array diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 7b660939b..2c8ef477f 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -16,20 +16,20 @@ open Pp open Util open Names -open Term +open Constr (* For Inline, the int is an inlining level, and the constr (if present) is the term into which we should inline. *) type delta_hint = | Inline of int * constr option - | Equiv of kernel_name + | Equiv of KerName.t -(* NB: earlier constructor Prefix_equiv of module_path +(* NB: earlier constructor Prefix_equiv of ModPath.t is now stored in a separate table, see Deltamap.t below *) module Deltamap = struct - type t = module_path MPmap.t * delta_hint KNmap.t + type t = ModPath.t MPmap.t * delta_hint KNmap.t let empty = MPmap.empty, KNmap.empty let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km @@ -45,7 +45,7 @@ module Deltamap = struct end (* Invariant: in the [delta_hint] map, an [Equiv] should only - relate [kernel_name] with the same label (and section dirpath). *) + relate [KerName.t] with the same label (and section dirpath). *) type delta_resolver = Deltamap.t @@ -65,7 +65,7 @@ module Umap = struct let join map1 map2 = fold add_mp add_mbi map1 map2 end -type substitution = (module_path * delta_resolver) Umap.t +type substitution = (ModPath.t * delta_resolver) Umap.t let empty_subst = Umap.empty @@ -76,21 +76,21 @@ let is_empty_subst = Umap.is_empty let string_of_hint = function | Inline (_,Some _) -> "inline(Some _)" | Inline _ -> "inline()" - | Equiv kn -> string_of_kn kn + | Equiv kn -> KerName.to_string kn let debug_string_of_delta resolve = let kn_to_string kn hint l = - (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l + (KerName.to_string kn ^ "=>" ^ string_of_hint hint) :: l in let mp_to_string mp mp' l = - (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l + (ModPath.to_string mp ^ "=>" ^ ModPath.to_string mp') :: l in let l = Deltamap.fold mp_to_string kn_to_string resolve [] in String.concat ", " (List.rev l) let list_contents sub = - let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in - let mp_one_pair mp0 p l = (string_of_mp mp0, one_pair p)::l in + let one_pair (mp,reso) = (ModPath.to_string mp,debug_string_of_delta reso) in + let mp_one_pair mp0 p l = (ModPath.to_string mp0, one_pair p)::l in let mbi_one_pair mbi p l = (MBId.debug_to_string mbi, one_pair p)::l in Umap.fold mp_one_pair mbi_one_pair sub [] @@ -117,7 +117,7 @@ let debug_pr_subst sub = let add_inline_delta_resolver kn (lev,oc) = Deltamap.add_kn kn (Inline (lev,oc)) let add_kn_delta_resolver kn kn' = - assert (Label.equal (label kn) (label kn')); + assert (Label.equal (KerName.label kn) (KerName.label kn')); Deltamap.add_kn kn (Equiv kn') let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2 @@ -165,12 +165,12 @@ let solve_delta_kn resolve kn = | Inline (lev, Some c) -> raise (Change_equiv_to_inline (lev,c)) | Inline (_, None) -> raise Not_found with Not_found -> - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let new_mp = find_prefix resolve mp in if mp == new_mp then kn else - make_kn new_mp dir l + KerName.make new_mp dir l let kn_of_delta resolve kn = try solve_delta_kn resolve kn @@ -242,18 +242,18 @@ let subst_mp sub mp = | Some (mp',_) -> mp' let subst_kn_delta sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',resolve) -> - solve_delta_kn resolve (make_kn mp' dir l) + solve_delta_kn resolve (KerName.make mp' dir l) | None -> kn let subst_kn sub kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in match subst_mp0 sub mp with Some (mp',_) -> - (make_kn mp' dir l) + (KerName.make mp' dir l) | None -> kn exception No_subst @@ -340,7 +340,7 @@ let subst_evaluable_reference subst = function let rec map_kn f f' c = let func = map_kn f f' in - match kind_of_term c with + match kind c with | Const kn -> (try snd (f' kn) with No_subst -> c) | Proj (p,t) -> let p' = @@ -419,7 +419,7 @@ let subst_mps sub c = let rec replace_mp_in_mp mpfrom mpto mp = match mp with - | _ when mp_eq mp mpfrom -> mpto + | _ when ModPath.equal mp mpfrom -> mpto | MPdot (mp1,l) -> let mp1' = replace_mp_in_mp mpfrom mpto mp1 in if mp1 == mp1' then mp @@ -427,14 +427,14 @@ let rec replace_mp_in_mp mpfrom mpto mp = | _ -> mp let replace_mp_in_kn mpfrom mpto kn = - let mp,dir,l = repr_kn kn in + let mp,dir,l = KerName.repr kn in let mp'' = replace_mp_in_mp mpfrom mpto mp in if mp==mp'' then kn - else make_kn mp'' dir l + else KerName.make mp'' dir l let rec mp_in_mp mp mp1 = match mp1 with - | _ when mp_eq mp1 mp -> true + | _ when ModPath.equal mp1 mp -> true | MPdot (mp2,l) -> mp_in_mp mp mp2 | _ -> false @@ -446,7 +446,7 @@ let subset_prefixed_by mp resolver = match hint with | Inline _ -> rslv | Equiv _ -> - if mp_in_mp mp (modpath kn) then Deltamap.add_kn kn hint rslv else rslv + if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv in Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver @@ -515,7 +515,7 @@ let add_delta_resolver resolver1 resolver2 = let substition_prefixed_by k mp subst = let mp_prefixmp kmp (mp_to,reso) sub = - if mp_in_mp mp kmp && not (mp_eq mp kmp) then + if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then let new_key = replace_mp_in_mp mp k kmp in Umap.add_mp new_key (mp_to,reso) sub else sub diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index f1d0e4279..1aa7ba519 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -9,7 +9,7 @@ (** {6 [Mod_subst] } *) open Names -open Term +open Constr (** {6 Delta resolver} *) @@ -20,44 +20,44 @@ type delta_resolver val empty_delta_resolver : delta_resolver val add_mp_delta_resolver : - module_path -> module_path -> delta_resolver -> delta_resolver + ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver val add_kn_delta_resolver : - kernel_name -> kernel_name -> delta_resolver -> delta_resolver + KerName.t -> KerName.t -> delta_resolver -> delta_resolver val add_inline_delta_resolver : - kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver + KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver (** Effect of a [delta_resolver] on a module path, on a kernel name *) -val mp_of_delta : delta_resolver -> module_path -> module_path -val kn_of_delta : delta_resolver -> kernel_name -> kernel_name +val mp_of_delta : delta_resolver -> ModPath.t -> ModPath.t +val kn_of_delta : delta_resolver -> KerName.t -> KerName.t (** Build a constant whose canonical part is obtained via a resolver *) -val constant_of_delta_kn : delta_resolver -> kernel_name -> constant +val constant_of_delta_kn : delta_resolver -> KerName.t -> Constant.t (** Same, but a 2nd resolver is tried if the 1st one had no effect *) val constant_of_deltas_kn : - delta_resolver -> delta_resolver -> kernel_name -> constant + delta_resolver -> delta_resolver -> KerName.t -> Constant.t (** Same for inductive names *) -val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive +val mind_of_delta_kn : delta_resolver -> KerName.t -> MutInd.t val mind_of_deltas_kn : - delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive + delta_resolver -> delta_resolver -> KerName.t -> MutInd.t (** Extract the set of inlined constant in the resolver *) -val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list +val inline_of_delta : int option -> delta_resolver -> (int * KerName.t) list (** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *) -val mp_in_delta : module_path -> delta_resolver -> bool -val con_in_delta : constant -> delta_resolver -> bool -val mind_in_delta : mutual_inductive -> delta_resolver -> bool +val mp_in_delta : ModPath.t -> delta_resolver -> bool +val con_in_delta : Constant.t -> delta_resolver -> bool +val mind_in_delta : MutInd.t -> delta_resolver -> bool (** {6 Substitution} *) @@ -72,15 +72,15 @@ val is_empty_subst : substitution -> bool composition. Most often this is not what you want. For sequential composition, try [join (map_mbid mp delta) subs] **) val add_mbid : - MBId.t -> module_path -> delta_resolver -> substitution -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution -> substitution val add_mp : - module_path -> module_path -> delta_resolver -> substitution -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution -> substitution (** map_* create a new substitution [arg2/arg1]\{arg3\} *) val map_mbid : - MBId.t -> module_path -> delta_resolver -> substitution + MBId.t -> ModPath.t -> delta_resolver -> substitution val map_mp : - module_path -> module_path -> delta_resolver -> substitution + ModPath.t -> ModPath.t -> delta_resolver -> substitution (** sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -117,10 +117,10 @@ val debug_pr_delta : delta_resolver -> Pp.t as well [==] *) val subst_mp : - substitution -> module_path -> module_path + substitution -> ModPath.t -> ModPath.t val subst_mind : - substitution -> mutual_inductive -> mutual_inductive + substitution -> MutInd.t -> MutInd.t val subst_ind : substitution -> inductive -> inductive @@ -128,10 +128,10 @@ val subst_ind : val subst_pind : substitution -> pinductive -> pinductive val subst_kn : - substitution -> kernel_name -> kernel_name + substitution -> KerName.t -> KerName.t val subst_con : - substitution -> pconstant -> constant * constr + substitution -> pconstant -> Constant.t * constr val subst_pcon : substitution -> pconstant -> pconstant @@ -140,10 +140,10 @@ val subst_pcon_term : substitution -> pconstant -> pconstant * constr val subst_con_kn : - substitution -> constant -> constant * constr + substitution -> Constant.t -> Constant.t * constr -val subst_constant : - substitution -> constant -> constant +val subst_constant : + substitution -> Constant.t -> Constant.t (** Here the semantics is completely unclear. What does "Hint Unfold t" means when "t" is a parameter? @@ -154,7 +154,7 @@ val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) -val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name +val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t (** [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) @@ -171,6 +171,5 @@ val occur_mbid : MBId.t -> substitution -> bool val repr_substituted : 'a substituted -> substitution list option * 'a -val force_constr : Term.constr substituted -> Term.constr -val subst_constr : - substitution -> Term.constr substituted -> Term.constr substituted +val force_constr : constr substituted -> constr +val subst_constr : substitution -> constr substituted -> constr substituted diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 8568bf14b..f7e755f00 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = environment, because they do not appear in the type of the definition. Any inconsistency will be raised at a later stage when joining the environment. *) - let env' = Environ.push_context ~strict:true ctx env' in - let c',cst = match cb.const_body with - | Undef _ | OpaqueDef _ -> - let j = Typeops.infer env' c in - let typ = cb.const_type in - let cst' = Reduction.infer_conv_leq env' (Environ.universes env') - j.uj_type typ in - j.uj_val, cst' - | Def cs -> - let c' = Mod_subst.force_constr cs in - c, Reduction.infer_conv env' (Environ.universes env') c c' - in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx) + let env' = Environ.push_context ~strict:true ctx env' in + let c',cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j = Typeops.infer env' c in + let typ = cb.const_type in + let cst' = Reduction.infer_conv_leq env' (Environ.universes env') + j.uj_type typ in + j.uj_val, cst' + | Def cs -> + let c' = Mod_subst.force_constr cs in + c, Reduction.infer_conv env' (Environ.universes env') c c' + in + let ctx = Univ.ContextSet.of_context ctx in + c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx | Polymorphic_const uctx -> let subst, ctx = Univ.abstract_universes ctx in let c = Vars.subst_univs_level_constr subst c in diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index dcabb1334..1225c3e1e 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -21,16 +21,16 @@ open Names *) val translate_module : - env -> module_path -> inline -> module_entry -> module_body + env -> ModPath.t -> inline -> module_entry -> module_body (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg] cannot be [None] (and of course [mod_expr] is [Abstract]). *) val translate_modtype : - env -> module_path -> inline -> module_type_entry -> module_type_body + env -> ModPath.t -> inline -> module_type_entry -> module_type_body (** Low-level function for translating a module struct entry : - - We translate to a module when a [module_path] is given, + - We translate to a module when a [ModPath.t] is given, otherwise to a module type. - The first output is the expanded signature - The second output is the algebraic expression, kept mostly for @@ -40,14 +40,14 @@ type 'alg translation = module_signature * 'alg * delta_resolver * Univ.ContextSet.t val translate_mse : - env -> module_path option -> inline -> module_struct_entry -> + env -> ModPath.t option -> inline -> module_struct_entry -> module_alg_expr translation (** From an already-translated (or interactive) implementation and an (optional) signature entry, produces a final [module_body] *) val finalize_module : - env -> module_path -> (module_expression option) translation -> + env -> ModPath.t -> (module_expression option) translation -> (module_type_entry * inline) option -> module_body @@ -55,5 +55,5 @@ val finalize_module : module type given to an Include *) val translate_mse_incl : - bool -> env -> module_path -> inline -> module_struct_entry -> + bool -> env -> ModPath.t -> inline -> module_struct_entry -> unit translation diff --git a/kernel/modops.ml b/kernel/modops.ml index 76915e917..11e6be659 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -17,7 +17,7 @@ open Util open Names -open Term +open Constr open Declarations open Declareops open Environ @@ -59,7 +59,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -68,7 +68,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -266,9 +266,9 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge mp = let perform rkaction env = match rkaction with - |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e - |_ -> + | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term.") in @@ -403,8 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = let constr = Mod_subst.force_constr body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> - error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + error_no_such_label_sub (Constant.label con) + (ModPath.to_string (Constant.modpath con)) in make_inline delta constants diff --git a/kernel/modops.mli b/kernel/modops.mli index e2a94b691..bbb4c918c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Declarations open Entries @@ -26,9 +26,9 @@ val destr_nofunctor : ('ty,'a) functorize -> 'a (** Conversions between [module_body] and [module_type_body] *) val module_type_of_module : module_body -> module_type_body -val module_body_of_type : module_path -> module_type_body -> module_body +val module_body_of_type : ModPath.t -> module_type_body -> module_body -val check_modpath_equiv : env -> module_path -> module_path -> unit +val check_modpath_equiv : env -> ModPath.t -> ModPath.t -> unit val implem_smartmap : (module_signature -> module_signature) -> @@ -43,7 +43,7 @@ val subst_structure : substitution -> structure_body -> structure_body (** {6 Adding to an environment } *) val add_structure : - module_path -> structure_body -> delta_resolver -> env -> env + ModPath.t -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env @@ -53,19 +53,19 @@ the native compiler. The linking information is updated. *) val add_linked_module : module_body -> Pre_env.link_info -> env -> env (** same, for a module type *) -val add_module_type : module_path -> module_type_body -> env -> env +val add_module_type : ModPath.t -> module_type_body -> env -> env (** {6 Strengthening } *) -val strengthen : module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> ModPath.t -> module_type_body val inline_delta_resolver : - env -> inline -> module_path -> MBId.t -> module_type_body -> + env -> inline -> ModPath.t -> MBId.t -> module_type_body -> delta_resolver -> delta_resolver -val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body +val strengthen_and_subst_mb : module_body -> ModPath.t -> bool -> module_body -val subst_modtype_and_resolver : module_type_body -> module_path -> +val subst_modtype_and_resolver : module_type_body -> ModPath.t -> module_type_body (** {6 Cleaning a module expression from bounded parts } @@ -118,7 +118,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -127,7 +127,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -153,4 +153,4 @@ val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a -val error_include_restricted_functor : module_path -> 'a +val error_include_restricted_functor : ModPath.t -> 'a diff --git a/kernel/names.ml b/kernel/names.ml index cb27104d1..b02c0b840 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -179,6 +179,8 @@ struct | [] -> "<>" | sl -> String.concat "." (List.rev_map Id.to_string sl) + let print dp = str (to_string dp) + let initial = [default_module_name] module Hdir = Hashcons.Hlist(Id) diff --git a/kernel/names.mli b/kernel/names.mli index d97fd2b3a..709ebeb7f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -113,6 +113,8 @@ end (** {6 Type aliases} *) type name = Name.t = Anonymous | Name of Id.t +[@@ocaml.deprecated "Use Name.t"] + type variable = Id.t type module_ident = Id.t @@ -157,6 +159,7 @@ sig val hcons : t -> t (** Hashconsing of directory paths. *) + val print : t -> Pp.t end (** {6 Names of structure elements } *) @@ -298,7 +301,6 @@ module KNset : CSig.SetS with type elt = KerName.t module KNpred : Predicate.S with type elt = KerName.t module KNmap : Map.ExtS with type key = KerName.t and module Set := KNset - (** {6 Constant Names } *) module Constant: @@ -572,54 +574,55 @@ module Idmap : module type of Id.Map (** {5 Directory paths} *) type dir_path = DirPath.t -(** @deprecated Alias for [DirPath.t]. *) +[@@ocaml.deprecated "Alias for [DirPath.t]."] -val dir_path_ord : dir_path -> dir_path -> int -(** @deprecated Same as [DirPath.compare]. *) +val dir_path_ord : DirPath.t -> DirPath.t -> int +[@@ocaml.deprecated "Same as [DirPath.compare]."] -val dir_path_eq : dir_path -> dir_path -> bool -(** @deprecated Same as [DirPath.equal]. *) +val dir_path_eq : DirPath.t -> DirPath.t -> bool +[@@ocaml.deprecated "Same as [DirPath.equal]."] -val make_dirpath : module_ident list -> dir_path -(** @deprecated Same as [DirPath.make]. *) +val make_dirpath : module_ident list -> DirPath.t +[@@ocaml.deprecated "Same as [DirPath.make]."] -val repr_dirpath : dir_path -> module_ident list -(** @deprecated Same as [DirPath.repr]. *) +val repr_dirpath : DirPath.t -> module_ident list +[@@ocaml.deprecated "Same as [DirPath.repr]."] -val empty_dirpath : dir_path -(** @deprecated Same as [DirPath.empty]. *) +val empty_dirpath : DirPath.t +[@@ocaml.deprecated "Same as [DirPath.empty]."] -val is_empty_dirpath : dir_path -> bool -(** @deprecated Same as [DirPath.is_empty]. *) +val is_empty_dirpath : DirPath.t -> bool +[@@ocaml.deprecated "Same as [DirPath.is_empty]."] -val string_of_dirpath : dir_path -> string -(** @deprecated Same as [DirPath.to_string]. *) +val string_of_dirpath : DirPath.t -> string +[@@ocaml.deprecated "Same as [DirPath.to_string]."] val initial_dir : DirPath.t -(** @deprecated Same as [DirPath.initial]. *) +[@@ocaml.deprecated "Same as [DirPath.initial]."] (** {5 Labels} *) type label = Label.t +[@@ocaml.deprecated "Same as [Label.t]."] (** Alias type *) -val mk_label : string -> label -(** @deprecated Same as [Label.make]. *) +val mk_label : string -> Label.t +[@@ocaml.deprecated "Same as [Label.make]."] -val string_of_label : label -> string -(** @deprecated Same as [Label.to_string]. *) +val string_of_label : Label.t -> string +[@@ocaml.deprecated "Same as [Label.to_string]."] -val pr_label : label -> Pp.t -(** @deprecated Same as [Label.print]. *) +val pr_label : Label.t -> Pp.t +[@@ocaml.deprecated "Same as [Label.print]."] -val label_of_id : Id.t -> label -(** @deprecated Same as [Label.of_id]. *) +val label_of_id : Id.t -> Label.t +[@@ocaml.deprecated "Same as [Label.of_id]."] -val id_of_label : label -> Id.t -(** @deprecated Same as [Label.to_id]. *) +val id_of_label : Label.t -> Id.t +[@@ocaml.deprecated "Same as [Label.to_id]."] -val eq_label : label -> label -> bool -(** @deprecated Same as [Label.equal]. *) +val eq_label : Label.t -> Label.t -> bool +[@@ocaml.deprecated "Same as [Label.equal]."] (** {5 Unique bound module names} *) @@ -627,89 +630,89 @@ type mod_bound_id = MBId.t (** Alias type. *) val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int -(** @deprecated Same as [MBId.compare]. *) +[@@ocaml.deprecated "Same as [MBId.compare]."] val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool -(** @deprecated Same as [MBId.equal]. *) +[@@ocaml.deprecated "Same as [MBId.equal]."] val make_mbid : DirPath.t -> Id.t -> mod_bound_id -(** @deprecated Same as [MBId.make]. *) +[@@ocaml.deprecated "Same as [MBId.make]."] val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t -(** @deprecated Same as [MBId.repr]. *) +[@@ocaml.deprecated "Same as [MBId.repr]."] val id_of_mbid : mod_bound_id -> Id.t -(** @deprecated Same as [MBId.to_id]. *) +[@@ocaml.deprecated "Same as [MBId.to_id]."] val string_of_mbid : mod_bound_id -> string -(** @deprecated Same as [MBId.to_string]. *) +[@@ocaml.deprecated "Same as [MBId.to_string]."] val debug_string_of_mbid : mod_bound_id -> string -(** @deprecated Same as [MBId.debug_to_string]. *) +[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] (** {5 Names} *) -val name_eq : name -> name -> bool -(** @deprecated Same as [Name.equal]. *) +val name_eq : Name.t -> Name.t -> bool +[@@ocaml.deprecated "Same as [Name.equal]."] (** {5 Module paths} *) type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t - | MPdot of module_path * Label.t -(** @deprecated Alias type *) + | MPdot of ModPath.t * Label.t +[@@ocaml.deprecated "Alias type"] -val mp_ord : module_path -> module_path -> int -(** @deprecated Same as [ModPath.compare]. *) +val mp_ord : ModPath.t -> ModPath.t -> int +[@@ocaml.deprecated "Same as [ModPath.compare]."] -val mp_eq : module_path -> module_path -> bool -(** @deprecated Same as [ModPath.equal]. *) +val mp_eq : ModPath.t -> ModPath.t -> bool +[@@ocaml.deprecated "Same as [ModPath.equal]."] -val check_bound_mp : module_path -> bool -(** @deprecated Same as [ModPath.is_bound]. *) +val check_bound_mp : ModPath.t -> bool +[@@ocaml.deprecated "Same as [ModPath.is_bound]."] -val string_of_mp : module_path -> string -(** @deprecated Same as [ModPath.to_string]. *) +val string_of_mp : ModPath.t -> string +[@@ocaml.deprecated "Same as [ModPath.to_string]."] -val initial_path : module_path -(** @deprecated Same as [ModPath.initial]. *) +val initial_path : ModPath.t +[@@ocaml.deprecated "Same as [ModPath.initial]."] (** {5 Kernel names} *) type kernel_name = KerName.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] -val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name -(** @deprecated Same as [KerName.make]. *) +val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t +[@@ocaml.deprecated "Same as [KerName.make]."] -val repr_kn : kernel_name -> module_path * DirPath.t * Label.t -(** @deprecated Same as [KerName.repr]. *) +val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [KerName.repr]."] -val modpath : kernel_name -> module_path -(** @deprecated Same as [KerName.modpath]. *) +val modpath : KerName.t -> ModPath.t +[@@ocaml.deprecated "Same as [KerName.modpath]."] -val label : kernel_name -> Label.t -(** @deprecated Same as [KerName.label]. *) +val label : KerName.t -> Label.t +[@@ocaml.deprecated "Same as [KerName.label]."] -val string_of_kn : kernel_name -> string -(** @deprecated Same as [KerName.to_string]. *) +val string_of_kn : KerName.t -> string +[@@ocaml.deprecated "Same as [KerName.to_string]."] -val pr_kn : kernel_name -> Pp.t -(** @deprecated Same as [KerName.print]. *) +val pr_kn : KerName.t -> Pp.t +[@@ocaml.deprecated "Same as [KerName.print]."] -val kn_ord : kernel_name -> kernel_name -> int -(** @deprecated Same as [KerName.compare]. *) +val kn_ord : KerName.t -> KerName.t -> int +[@@ocaml.deprecated "Same as [KerName.compare]."] (** {5 Constant names} *) type constant = Constant.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] module Projection : sig type t - - val make : constant -> bool -> t + + val make : Constant.t -> bool -> t module SyntacticOrd : sig val compare : t -> t -> int @@ -717,7 +720,7 @@ module Projection : sig val hash : t -> int end - val constant : t -> constant + val constant : t -> Constant.t val unfolded : t -> bool val unfold : t -> t @@ -727,8 +730,8 @@ module Projection : sig (** Hashconsing of projections. *) val compare : t -> t -> int - - val map : (constant -> constant) -> t -> t + + val map : (Constant.t -> Constant.t) -> t -> t val to_string : t -> string val print : t -> Pp.t @@ -737,100 +740,100 @@ end type projection = Projection.t -val constant_of_kn_equiv : KerName.t -> KerName.t -> constant -(** @deprecated Same as [Constant.make] *) +val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make]"] -val constant_of_kn : KerName.t -> constant -(** @deprecated Same as [Constant.make1] *) +val constant_of_kn : KerName.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make1]"] -val make_con : ModPath.t -> DirPath.t -> Label.t -> constant -(** @deprecated Same as [Constant.make3] *) +val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.make3]"] -val repr_con : constant -> ModPath.t * DirPath.t * Label.t -(** @deprecated Same as [Constant.repr3] *) +val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [Constant.repr3]"] -val user_con : constant -> KerName.t -(** @deprecated Same as [Constant.user] *) +val user_con : Constant.t -> KerName.t +[@@ocaml.deprecated "Same as [Constant.user]"] -val canonical_con : constant -> KerName.t -(** @deprecated Same as [Constant.canonical] *) +val canonical_con : Constant.t -> KerName.t +[@@ocaml.deprecated "Same as [Constant.canonical]"] -val con_modpath : constant -> ModPath.t -(** @deprecated Same as [Constant.modpath] *) +val con_modpath : Constant.t -> ModPath.t +[@@ocaml.deprecated "Same as [Constant.modpath]"] -val con_label : constant -> Label.t -(** @deprecated Same as [Constant.label] *) +val con_label : Constant.t -> Label.t +[@@ocaml.deprecated "Same as [Constant.label]"] -val eq_constant : constant -> constant -> bool -(** @deprecated Same as [Constant.equal] *) +val eq_constant : Constant.t -> Constant.t -> bool +[@@ocaml.deprecated "Same as [Constant.equal]"] -val con_ord : constant -> constant -> int -(** @deprecated Same as [Constant.CanOrd.compare] *) +val con_ord : Constant.t -> Constant.t -> int +[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] -val con_user_ord : constant -> constant -> int -(** @deprecated Same as [Constant.UserOrd.compare] *) +val con_user_ord : Constant.t -> Constant.t -> int +[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] -val con_with_label : constant -> Label.t -> constant -(** @deprecated Same as [Constant.change_label] *) +val con_with_label : Constant.t -> Label.t -> Constant.t +[@@ocaml.deprecated "Same as [Constant.change_label]"] -val string_of_con : constant -> string -(** @deprecated Same as [Constant.to_string] *) +val string_of_con : Constant.t -> string +[@@ocaml.deprecated "Same as [Constant.to_string]"] -val pr_con : constant -> Pp.t -(** @deprecated Same as [Constant.print] *) +val pr_con : Constant.t -> Pp.t +[@@ocaml.deprecated "Same as [Constant.print]"] -val debug_pr_con : constant -> Pp.t -(** @deprecated Same as [Constant.debug_print] *) +val debug_pr_con : Constant.t -> Pp.t +[@@ocaml.deprecated "Same as [Constant.debug_print]"] -val debug_string_of_con : constant -> string -(** @deprecated Same as [Constant.debug_to_string] *) +val debug_string_of_con : Constant.t -> string +[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] (** {5 Mutual Inductive names} *) type mutual_inductive = MutInd.t -(** @deprecated Alias type *) +[@@ocaml.deprecated "Alias type"] -val mind_of_kn : KerName.t -> mutual_inductive -(** @deprecated Same as [MutInd.make1] *) +val mind_of_kn : KerName.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make1]"] -val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive -(** @deprecated Same as [MutInd.make] *) +val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make]"] -val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive -(** @deprecated Same as [MutInd.make3] *) +val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t +[@@ocaml.deprecated "Same as [MutInd.make3]"] -val user_mind : mutual_inductive -> KerName.t -(** @deprecated Same as [MutInd.user] *) +val user_mind : MutInd.t -> KerName.t +[@@ocaml.deprecated "Same as [MutInd.user]"] -val canonical_mind : mutual_inductive -> KerName.t -(** @deprecated Same as [MutInd.canonical] *) +val canonical_mind : MutInd.t -> KerName.t +[@@ocaml.deprecated "Same as [MutInd.canonical]"] -val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t -(** @deprecated Same as [MutInd.repr3] *) +val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t +[@@ocaml.deprecated "Same as [MutInd.repr3]"] -val eq_mind : mutual_inductive -> mutual_inductive -> bool -(** @deprecated Same as [MutInd.equal] *) +val eq_mind : MutInd.t -> MutInd.t -> bool +[@@ocaml.deprecated "Same as [MutInd.equal]"] -val mind_ord : mutual_inductive -> mutual_inductive -> int -(** @deprecated Same as [MutInd.CanOrd.compare] *) +val mind_ord : MutInd.t -> MutInd.t -> int +[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] -val mind_user_ord : mutual_inductive -> mutual_inductive -> int -(** @deprecated Same as [MutInd.UserOrd.compare] *) +val mind_user_ord : MutInd.t -> MutInd.t -> int +[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] -val mind_label : mutual_inductive -> Label.t -(** @deprecated Same as [MutInd.label] *) +val mind_label : MutInd.t -> Label.t +[@@ocaml.deprecated "Same as [MutInd.label]"] -val mind_modpath : mutual_inductive -> ModPath.t -(** @deprecated Same as [MutInd.modpath] *) +val mind_modpath : MutInd.t -> ModPath.t +[@@ocaml.deprecated "Same as [MutInd.modpath]"] -val string_of_mind : mutual_inductive -> string -(** @deprecated Same as [MutInd.to_string] *) +val string_of_mind : MutInd.t -> string +[@@ocaml.deprecated "Same as [MutInd.to_string]"] -val pr_mind : mutual_inductive -> Pp.t -(** @deprecated Same as [MutInd.print] *) +val pr_mind : MutInd.t -> Pp.t +[@@ocaml.deprecated "Same as [MutInd.print]"] -val debug_pr_mind : mutual_inductive -> Pp.t -(** @deprecated Same as [MutInd.debug_print] *) +val debug_pr_mind : MutInd.t -> Pp.t +[@@ocaml.deprecated "Same as [MutInd.debug_print]"] -val debug_string_of_mind : mutual_inductive -> string -(** @deprecated Same as [MutInd.debug_to_string] *) +val debug_string_of_mind : MutInd.t -> string +[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6e9991ac5..c558e9ed0 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -8,7 +8,7 @@ open CErrors open Names -open Term +open Constr open Declarations open Util open Nativevalues @@ -25,7 +25,7 @@ to OCaml code. *) (** Local names **) (* The first component is there for debugging purposes only *) -type lname = { lname : name; luid : int } +type lname = { lname : Name.t; luid : int } let eq_lname ln1 ln2 = Int.equal ln1.luid ln2.luid @@ -50,13 +50,13 @@ let fresh_lname n = type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) - | Gconstant of string * constant (* prefix, constant name *) - | Gproj of string * constant (* prefix, constant name *) - | Gcase of label option * int - | Gpred of label option * int - | Gfixtype of label option * int - | Gnorm of label option * int - | Gnormtbl of label option * int + | Gconstant of string * Constant.t (* prefix, constant name *) + | Gproj of string * Constant.t (* prefix, constant name *) + | Gcase of Label.t option * int + | Gpred of Label.t option * int + | Gfixtype of Label.t option * int + | Gnorm of Label.t option * int + | Gnormtbl of Label.t option * int | Ginternal of string | Grel of int | Gnamed of Id.t @@ -142,9 +142,9 @@ let fresh_gnormtbl l = type symbol = | SymbValue of Nativevalues.t - | SymbSort of sorts - | SymbName of name - | SymbConst of constant + | SymbSort of Sorts.t + | SymbName of Name.t + | SymbConst of Constant.t | SymbMatch of annot_sw | SymbInd of inductive | SymbMeta of metavariable @@ -163,7 +163,7 @@ let eq_symbol sy1 sy2 = | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 | SymbEvar (evk1,args1), SymbEvar (evk2,args2) -> - Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2 + Evar.equal evk1 evk2 && Array.for_all2 Constr.equal args1 args2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 | _, _ -> false @@ -296,7 +296,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option let eq_primitive p1 p2 = match p1, p2 with @@ -921,7 +921,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * CPrimitives.t * prim_aux array + | PAprim of string * Constant.t * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -1504,7 +1504,7 @@ let string_of_dirpath = function (* OCaml as a module identifier. *) let string_of_dirpath s = "N"^string_of_dirpath s -let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir) +let mod_uid_of_dirpath dir = string_of_dirpath (DirPath.repr dir) let link_info_of_dirpath dir = Linked (mod_uid_of_dirpath dir ^ ".") @@ -1523,19 +1523,19 @@ let string_of_label_def l = let rec list_of_mp acc = function | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp | MPfile dp -> - let dp = repr_dirpath dp in + let dp = DirPath.repr dp in string_of_dirpath dp :: acc - | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc + | MPbound mbid -> ("X"^string_of_id (MBId.to_id mbid))::acc let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,dp,l) = repr_kn kn in + let (mp,dp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l -let string_of_con c = string_of_kn (user_con c) -let string_of_mind mind = string_of_kn (user_mind mind) +let string_of_con c = string_of_kn (Constant.user c) +let string_of_mind mind = string_of_kn (MutInd.user mind) let string_of_gname g = match g with @@ -1877,7 +1877,7 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix in - let l = con_label con in + let l = Constant.label con in let auxdefs,code = if no_univs then compile_with_fv env sigma None [] (Some l) code else @@ -2016,7 +2016,7 @@ let compile_mind_deps env prefix ~interactive (* This function compiles all necessary dependencies of t, and generates code in reverse order, as well as linking information updates *) let rec compile_deps env sigma prefix ~interactive init t = - match kind_of_term t with + match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> let c,u = get_alias env c in @@ -2048,8 +2048,8 @@ let rec compile_deps env sigma prefix ~interactive init t = | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - fold_constr (compile_deps env sigma prefix ~interactive) init t - | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t + Constr.fold (compile_deps env sigma prefix ~interactive) init t + | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t let compile_constant_field env prefix con acc cb = let (gl, _) = diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index ae6fb1bd6..d08f49095 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Names +open Constr open Declarations open Pre_env open Nativelambda @@ -32,11 +32,11 @@ val clear_symbols : unit -> unit val get_value : symbols -> int -> Nativevalues.t -val get_sort : symbols -> int -> sorts +val get_sort : symbols -> int -> Sorts.t -val get_name : symbols -> int -> name +val get_name : symbols -> int -> Name.t -val get_const : symbols -> int -> constant +val get_const : symbols -> int -> Constant.t val get_match : symbols -> int -> Nativevalues.annot_sw @@ -60,20 +60,20 @@ val empty_updates : code_location_updates val register_native_file : string -> unit -val compile_constant_field : env -> string -> constant -> +val compile_constant_field : env -> string -> Constant.t -> global list -> constant_body -> global list -val compile_mind_field : string -> module_path -> label -> +val compile_mind_field : string -> ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code val mk_norm_code : env -> evars -> string -> constr -> linkable_code -val mk_library_header : dir_path -> global list +val mk_library_header : DirPath.t -> global list -val mod_uid_of_dirpath : dir_path -> string +val mod_uid_of_dirpath : DirPath.t -> string -val link_info_of_dirpath : dir_path -> link_info +val link_info_of_dirpath : DirPath.t -> link_info val update_locations : code_location_updates -> unit diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index a62a079da..9f9102f7d 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -154,7 +154,7 @@ let warn_no_native_compiler = (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin + if not Coq_config.native_compiler then begin warn_no_native_compiler (); vm_conv cv_pb env t1 t2 end diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index fbbcce744..769deacae 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Reduction open Nativelambda diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 73f18f7a7..928283a4d 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Term +open Constr open Nativevalues (** This file defines the lambda code for the native compiler. It has been @@ -20,17 +20,17 @@ type uint = | UintDecomp of prefix * constructor * lambda and lambda = - | Lrel of name * int + | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) | Levar of existential * lambda (* type *) | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda + | Llam of Name.t array * lambda + | Llet of Name.t * lambda * lambda | Lapp of lambda * lambda array | Lconst of prefix * pconstant - | Lproj of prefix * constant (* prefix, projection name *) - | Lprim of prefix * constant * CPrimitives.t * lambda array + | Lproj of prefix * Constant.t (* prefix, projection name *) + | Lprim of prefix * Constant.t * CPrimitives.t * lambda array | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda @@ -43,11 +43,11 @@ and lambda = (* A partially applied constructor *) | Luint of uint | Lval of Nativevalues.t - | Lsort of sorts + | Lsort of Sorts.t | Lind of prefix * pinductive | Llazy | Lforce -and lam_branches = (constructor * name array * lambda) array +and lam_branches = (constructor * Name.t array * lambda) array -and fix_decl = name array * lambda array * lambda array +and fix_decl = Name.t array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 508112b35..de4dc2107 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -8,7 +8,7 @@ open Util open Names open Esubst -open Term +open Constr open Declarations open Pre_env open Nativevalues @@ -378,7 +378,7 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) type t = { - name_rel : name Vect.t; + name_rel : Name.t Vect.t; construct_tbl : constructor_info ConstrTable.t; } @@ -417,9 +417,9 @@ module Renv = (* What about pattern matching ?*) let is_lazy prefix t = - match kind_of_term t with + match kind t with | App (f,args) -> - begin match kind_of_term f with + begin match kind f with | Construct (c,_) -> let entry = mkInd (fst c) in (try @@ -448,7 +448,7 @@ let empty_evars = let empty_ids = [||] let rec lambda_of_constr env sigma c = - match kind_of_term c with + match kind c with | Meta mv -> let ty = meta_type sigma mv in Lmeta (mv, lambda_of_constr env sigma ty) @@ -480,7 +480,7 @@ let rec lambda_of_constr env sigma c = Lprod(ld, Llam([|id|], lc)) | Lambda _ -> - let params, body = decompose_lam c in + let params, body = Term.decompose_lam c in let ids = get_names (List.rev params) in Renv.push_rels env ids; let lb = lambda_of_constr env sigma body in @@ -561,7 +561,7 @@ let rec lambda_of_constr env sigma c = Lcofix(init, (names, ltypes, lbodies)) and lambda_of_app env sigma f args = - match kind_of_term f with + match kind f with | Const (kn,u as c) -> let kn,u = get_alias !global_env c in let cb = lookup_constant kn !global_env in @@ -656,7 +656,7 @@ let compile_static_int31 fc args = if not fc then raise Not_found else Luint (UintVal (Uint31.of_int (Array.fold_left - (fun temp_i -> fun t -> match kind_of_term t with + (fun temp_i -> fun t -> match kind t with | Construct ((_,d),_) -> 2*temp_i+d-1 | _ -> raise NotClosed) 0 args))) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 156e4f834..933fbc660 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Term +open Constr open Pre_env open Nativeinstr @@ -18,13 +18,13 @@ type evars = val empty_evars : evars -val decompose_Llam : lambda -> Names.name array * lambda -val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda +val decompose_Llam : lambda -> Name.t array * lambda +val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda val is_lazy : prefix -> constr -> bool val mk_lazy : lambda -> lambda -val get_mind_prefix : env -> mutual_inductive -> string +val get_mind_prefix : env -> MutInd.t -> string val get_alias : env -> pconstant -> pconstant @@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array -> val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda -> lambda -val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array -> +val compile_prim : CPrimitives.t -> Constant.t -> bool -> prefix -> lambda array -> lambda diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index e9c0e171a..4e7d6b218 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -87,7 +87,7 @@ let call_compiler ?profile:(profile=false) ml_filename = [] in let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] then + if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then (* We play safe for now, and use the native compiler with -Oclassic, however it is likely that `native_compute` users can benefit from tweaking here. diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index a262a9f58..b74d4fdd0 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -21,7 +21,7 @@ val get_ml_filename : unit -> string * string val compile : string -> global list -> profile:bool -> bool * string -val compile_library : Names.dir_path -> global list -> string -> bool +val compile_library : Names.DirPath.t -> global list -> string -> bool val call_linker : ?fatal:bool -> string -> string -> code_location_updates option -> unit diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 3e273dde2..c68f78121 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -26,7 +26,7 @@ let rec translate_mod prefix mp env mod_expr acc = and translate_field prefix mp env acc (l,x) = match x with | SFBconst cb -> - let con = make_con mp empty_dirpath l in + let con = Constant.make3 mp DirPath.empty l in (if !Flags.debug then let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index f327ba224..72e3d8041 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -13,5 +13,5 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : module_path -> dir_path -> env -> module_signature -> +val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> global list * symbols diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 1c9996d89..ae66362ca 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -5,10 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open Names -open CErrors + open Util +open CErrors +open Names +open Constr (** This module defines the representation of values internally used by the native compiler *) @@ -51,17 +52,17 @@ type atom = | Arel of int | Aconstant of pconstant | Aind of pinductive - | Asort of sorts + | Asort of Sorts.t | Avar of Id.t | Acase of annot_sw * accumulator * t * (t -> t) | Afix of t array * t array * rec_pos * int (* types, bodies, rec_pos, pos *) | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t - | Aprod of name * t * (t -> t) + | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of existential * t - | Aproj of constant * accumulator + | Aproj of Constant.t * accumulator let accumulate_tag = 0 @@ -111,6 +112,7 @@ let mk_ind_accu ind u = mk_accu (Aind (ind,Univ.Instance.of_array u)) let mk_sort_accu s u = + let open Sorts in match s with | Prop _ -> mk_accu (Asort s) | Type s -> diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 0e2db8486..18b877745 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Names (** This modules defines the representation of values internally used by @@ -43,33 +43,33 @@ type atom = | Arel of int | Aconstant of pconstant | Aind of pinductive - | Asort of sorts + | Asort of Sorts.t | Avar of Id.t | Acase of annot_sw * accumulator * t * (t -> t) | Afix of t array * t array * rec_pos * int | Acofix of t array * t array * int * t | Acofixe of t array * t array * int * t - | Aprod of name * t * (t -> t) + | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t | Aevar of existential * t - | Aproj of constant * accumulator + | Aproj of Constant.t * accumulator (* Constructors *) val mk_accu : atom -> t val mk_rel_accu : int -> t val mk_rels_accu : int -> int -> t array -val mk_constant_accu : constant -> Univ.Level.t array -> t +val mk_constant_accu : Constant.t -> Univ.Level.t array -> t val mk_ind_accu : inductive -> Univ.Level.t array -> t -val mk_sort_accu : sorts -> Univ.Level.t array -> t +val mk_sort_accu : Sorts.t -> Univ.Level.t array -> t val mk_var_accu : Id.t -> t val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) -val mk_prod_accu : name -> t -> t -> t +val mk_prod_accu : Name.t -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t val mk_evar_accu : existential -> t -> t -val mk_proj_accu : constant -> accumulator -> t +val mk_proj_accu : Constant.t -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t val mk_const : tag -> t diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 400f9feee..45a62d55a 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -8,7 +8,7 @@ open Names open Univ -open Term +open Constr open Mod_subst type work_list = (Instance.t * Id.t array) Cmap.t * @@ -17,7 +17,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } -type proofterm = (constr * Univ.universe_context_set) Future.computation +type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) | Direct of cooking_info list * proofterm @@ -138,7 +138,7 @@ let get_proof { opaque_val = prfs; opaque_dir = odp } = function module FMap = Future.UUIDMap -let a_constr = Future.from_val (Term.mkRel 1) +let a_constr = Future.from_val (mkRel 1) let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : cooking_info list = [] diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index a0418a022..20d76ce23 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Mod_subst (** This module implements the handling of opaque proof terms. @@ -19,7 +19,7 @@ open Mod_subst When it is [turn_indirect] the data is relocated to an opaque table and the [opaque] is turned into an index. *) -type proofterm = (constr * Univ.universe_context_set) Future.computation +type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaquetab type opaque @@ -36,10 +36,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab (** From a [opaque] back to a [constr]. This might use the indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr -val force_constraints : opaquetab -> opaque -> Univ.universe_context_set -val get_proof : opaquetab -> opaque -> Term.constr Future.computation +val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t +val get_proof : opaquetab -> opaque -> constr Future.computation val get_constraints : - opaquetab -> opaque -> Univ.universe_context_set Future.computation option + opaquetab -> opaque -> Univ.ContextSet.t Future.computation option val subst_opaque : substitution -> opaque -> opaque val iter_direct_opaque : (constr -> unit) -> opaque -> opaque @@ -63,7 +63,7 @@ val join_opaque : opaquetab -> opaque -> unit val dump : opaquetab -> Constr.t Future.computation array * - Univ.universe_context_set Future.computation array * + Univ.ContextSet.t Future.computation array * cooking_info list array * int Future.UUIDMap.t @@ -75,7 +75,7 @@ val dump : opaquetab -> *) val set_indirect_opaque_accessor : - (DirPath.t -> int -> Term.constr Future.computation) -> unit + (DirPath.t -> int -> constr Future.computation) -> unit val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit + (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 94738d618..c5254b453 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,7 @@ open Util open Names -open Term +open Constr open Declarations module NamedDecl = Context.Named.Declaration diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index f2a009b86..054ae1743 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Declarations (** The type of environments. *) @@ -88,9 +88,9 @@ val env_of_named : Id.t -> env -> env (** Global constants *) -val lookup_constant_key : constant -> env -> constant_key -val lookup_constant : constant -> env -> constant_body +val lookup_constant_key : Constant.t -> env -> constant_key +val lookup_constant : Constant.t -> env -> constant_body (** Mutual Inductives *) -val lookup_mind_key : mutual_inductive -> env -> mind_key -val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +val lookup_mind_key : MutInd.t -> env -> mind_key +val lookup_mind : MutInd.t -> env -> mutual_inductive_body diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2bf9f43a5..c07ac973b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -18,7 +18,7 @@ open CErrors open Util open Names -open Term +open Constr open Vars open Environ open CClosure @@ -57,12 +57,14 @@ let compare_stack_shape stk1 stk2 = Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | (_,_) -> false in + | [], _ :: _ + | (Zproj _ | ZcaseT _ | Zfix _) :: _, _ -> false + in compare_rec 0 stk1 stk2 type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of constant * lift + | Zlproj of Constant.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -107,11 +109,11 @@ let pure_stack lfts stk = (****************************************************************************) let whd_betaiota env t = - match kind_of_term t with + match kind t with | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t | _ -> whd_val (create_clos_infos betaiota env) (inject t) end @@ -121,37 +123,46 @@ let nf_betaiota env t = norm_val (create_clos_infos betaiota env) (inject t) let whd_betaiotazeta env x = - match kind_of_term x with - | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| + match kind x with + | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> x | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ + | Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos betaiotazeta env) (inject x) end - | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) + | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ -> + whd_val (create_clos_infos betaiotazeta env) (inject x) let whd_all env t = - match kind_of_term t with + match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ -> t - | _ -> whd_val (create_clos_infos all env) (inject t) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _ + | Const _ |Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos all env) (inject t) end - | _ -> whd_val (create_clos_infos all env) (inject t) + | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ -> + whd_val (create_clos_infos all env) (inject t) let whd_allnolet env t = - match kind_of_term t with + match kind t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t | App (c, _) -> - begin match kind_of_term c with + begin match kind c with | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t - | _ -> whd_val (create_clos_infos allnolet env) (inject t) + | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _ + | Const _ | Case _ | Fix _ | CoFix _ | Proj _ -> + whd_val (create_clos_infos allnolet env) (inject t) end - | _ -> whd_val (create_clos_infos allnolet env) (inject t) + | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ -> + whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) @@ -189,7 +200,7 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; + compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; @@ -201,7 +212,7 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t let sort_cmp_universes env pb s0 s1 (u, check) = (check.compare env pb s0 s1 u, check) @@ -239,7 +250,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (eq_constant c1 c2) then + if not (Constant.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> @@ -309,11 +320,11 @@ let unfold_projection infos p c = else None (* Conversion between [lft1]term1 and [lft2]term2 *) -let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv +let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = + eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) -and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = +and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Control.check_for_interrupt (); (* First head reduce both terms *) let whd = whd_stack (infos_with_reds infos betaiotazeta) in @@ -331,20 +342,20 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> - (match kind_of_term a1, kind_of_term a2 with + (match kind a1, kind a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | _ -> raise NotConvertible) | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) -> if Evar.equal ev1 ev2 then - let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in - convert_vect env l2r infos el1 el2 + let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in + convert_vect l2r infos el1 el2 (Array.map (mk_clos env1) args1) (Array.map (mk_clos env2) args2) cuniv else raise NotConvertible @@ -352,14 +363,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 index known to be bound to no constant *) | (FRel n, FRel m) -> if Int.equal (reloc_rel n el1) (reloc_rel m el2) - then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try let cuniv = conv_table_key infos fl1 fl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in @@ -379,7 +390,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in - eqappr env cv_pb l2r infos app1 app2 cuniv) + eqappr cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -387,42 +398,42 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then - let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 u1 + let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 u1 else (* Two projections in WHNF: unfold *) raise NotConvertible) | (FProj (p1,c1), t2) -> (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> (match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -434,15 +445,15 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given ill-typed terms (FLambda)."); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in - let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in - ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv + let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in + ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (FProd)."); (* Luo's system *) - let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in - ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv + let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in + ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv (* Eta-expansion on the fly *) | (FLambda _, _) -> @@ -452,7 +463,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in - eqappr env CONV l2r infos + eqappr CONV l2r infos (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv | (_, FLambda _) -> let () = match v2 with @@ -461,34 +472,34 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = anomaly (Pp.str "conversion was given unreduced term (FLambda).") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in - eqappr env CONV l2r infos + eqappr CONV l2r infos (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -497,9 +508,9 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = if eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in let cuniv = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> @@ -508,16 +519,16 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> if Int.equal j1 j2 && eq_ind ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else - let mind = Environ.lookup_mind (fst ind1) env in + let mind = Environ.lookup_mind (fst ind1) (info_env infos) in let cuniv = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> @@ -527,7 +538,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) u2 (CClosure.stack_args_size v2) cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -535,14 +546,14 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let v1, v2 = eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> @@ -553,11 +564,11 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) -> @@ -568,28 +579,28 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let fty2 = Array.map (mk_clos e2) tys2 in let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in - let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in + let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in let cuniv = - convert_vect env l2r infos + convert_vect l2r infos (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) - | (FLOCKED,_) | (_,FLOCKED) ) -> assert false + | (FLOCKED,_) | (_,FLOCKED) ) | (FCast _, _) | (_, FCast _) -> assert false - (* In all other cases, terms are not convertible *) - | _ -> raise NotConvertible + | (FRel _ | FAtom _ | FInd _ | FFix _ | FCoFix _ + | FProd _ | FEvar _), _ -> raise NotConvertible -and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv = +and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv) + (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv -and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = +and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in let lv2 = Array.length v2 in if Int.equal lv1 lv2 @@ -597,7 +608,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let rec fold n cuniv = if n >= lv1 then cuniv else - let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in + let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in fold (n+1) cuniv in fold 0 cuniv else raise NotConvertible @@ -605,7 +616,7 @@ and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv = let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in - ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs + ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs let check_eq univs u u' = @@ -615,6 +626,7 @@ let check_leq univs u u' = if not (UGraph.check_leq univs u u') then raise NotConvertible let check_sort_cmp_universes env pb s0 s1 univs = + let open Sorts in match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -734,6 +746,7 @@ let infer_leq (univs, cstrs as cuniv) u u' = univs, cstrs' let infer_cmp_universes env pb s0 s1 univs = + let open Sorts in match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -820,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -847,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* Profiling *) let infer_conv_universes = if Flags.profile then - let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in - Profile.profile8 infer_conv_universes_key infer_conv_universes + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -869,7 +882,7 @@ let warn_bytecode_compiler_failed = (fun () -> strbrk "Bytecode compiler failed, " ++ strbrk "falling back to standard conversion") -let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f +let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f let vm_conv cv_pb env t1 t2 = try !vm_conv cv_pb env t1 t2 @@ -882,22 +895,22 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) let beta_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l - | _ -> applist (substl subst c, l) in + | _ -> Term.applist (substl subst c, l) in app [] c l let beta_appvect c v = beta_applist c (Array.to_list v) @@ -905,7 +918,7 @@ let beta_appvect c v = beta_applist c (Array.to_list v) let beta_app c a = beta_applist c [a] (* Compatibility *) -let betazeta_appvect = lambda_appvect_assum +let betazeta_appvect = Term.lambda_appvect_assum (********************************************************************) (* Special-Purpose Reduction *) @@ -918,7 +931,7 @@ let betazeta_appvect = lambda_appvect_assum * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_all env t) with + match kind (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") @@ -930,7 +943,7 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = let t = whd_all env c in - match kind_of_term t with + match kind t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in decrec (push_rel d env) (Context.Rel.add d m) c0 @@ -942,7 +955,7 @@ let dest_prod env = let dest_prod_assum env = let rec prodec_rec env l ty = let rty = whd_allnolet env ty in - match kind_of_term rty with + match kind rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in prodec_rec (push_rel d env) (Context.Rel.add d l) c @@ -952,7 +965,7 @@ let dest_prod_assum env = | Cast (c,_,_) -> prodec_rec env l c | _ -> let rty' = whd_all env rty in - if Term.eq_constr rty' rty then l, rty + if Constr.equal rty' rty then l, rty else prodec_rec env l rty' in prodec_rec env Context.Rel.empty @@ -960,7 +973,7 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = let rty = whd_allnolet env ty in - match kind_of_term rty with + match kind rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in lamec_rec (push_rel d env) (Context.Rel.add d l) c @@ -976,7 +989,7 @@ exception NotArity let dest_arity env c = let l, c = dest_prod_assum env c in - match kind_of_term c with + match kind c with | Sort s -> l,s | _ -> raise NotArity diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 253c0874f..573e4c8bd 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Environ (*********************************************************************** @@ -37,7 +37,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; + compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; @@ -49,9 +49,9 @@ type 'a universe_state = 'a * 'a universe_compare type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b -type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t -val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> +val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare (* [flex] should be true for constants, false for inductive types and @@ -115,7 +115,7 @@ val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity -val dest_arity : env -> types -> arity (* raises NotArity if not an arity *) +val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 5fbd914f3..88cf93acc 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -14,7 +14,7 @@ for evaluation in the bytecode virtual machine *) open Names -open Term +open Constr (* The retroknowledge defines a bijective correspondance between some [entry]-s (which are, in fact, merely terms) and [field]-s which @@ -102,7 +102,7 @@ module Reactive = Map.Make (EntryOrd) type reactive_info = {(*information required by the compiler of the VM *) vm_compiling : (*fastcomputation flag -> continuation -> result *) - (bool->Cbytecodes.comp_env->constr array -> + (bool -> Cbytecodes.comp_env -> constr array -> int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) option; vm_constant_static : @@ -117,7 +117,7 @@ type reactive_info = {(*information required by the compiler of the VM *) (* fastcomputation flag -> cont -> result *) vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; (* tag (= compiled int for instance) -> result *) - vm_decompile_const : (int -> Term.constr) option; + vm_decompile_const : (int -> constr) option; native_compiling : (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 18a12a4ef..e4d78ba14 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr type retroknowledge @@ -117,7 +117,7 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes recover the elements of that type from their compiled form if it's non standard (it is used (and can be used) only when the compiled form is not a block *) -val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr +val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr val get_native_compiling_info : retroknowledge -> entry -> Nativeinstr.prefix -> @@ -163,7 +163,7 @@ type reactive_info = {(*information required by the compiler of the VM *) (* fastcomputation flag -> cont -> result *) vm_before_match : (bool -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes) option; (* tag (= compiled int for instance) -> result *) - vm_decompile_const : (int -> Term.constr) option; + vm_decompile_const : (int -> constr) option; native_compiling : (bool -> Nativeinstr.prefix -> Nativeinstr.lambda array -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fd024b215..5150ad411 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -114,7 +114,7 @@ module DPMap = Map.Make(DirPath) type safe_environment = { env : Environ.env; - modpath : module_path; + modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; paramresolver : Mod_subst.delta_resolver; @@ -125,7 +125,7 @@ type safe_environment = future_cst : Univ.ContextSet.t Future.computation list; engagement : engagement option; required : vodigest DPMap.t; - loads : (module_path * module_body) list; + loads : (ModPath.t * module_body) list; local_retroknowledge : Retroknowledge.action list; native_symbols : Nativecode.symbols DPMap.t } @@ -143,7 +143,7 @@ let rec library_dp_of_senv senv = let empty_environment = { env = Environ.empty_env; - modpath = initial_path; + modpath = ModPath.initial; modvariant = NONE; modresolver = Mod_subst.empty_delta_resolver; paramresolver = Mod_subst.empty_delta_resolver; @@ -160,7 +160,7 @@ let empty_environment = let is_initial senv = match senv.revstruct, senv.modvariant with - | [], NONE -> ModPath.equal senv.modpath initial_path + | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false let delta_of_senv senv = senv.modresolver,senv.paramresolver @@ -249,14 +249,14 @@ let universes_of_private eff = in match cb.const_universes with | Monomorphic_const ctx -> - (Univ.ContextSet.of_context ctx) :: acc + ctx :: acc | Polymorphic_const _ -> acc ) acc l | Entries.SEsubproof (c, cb, e) -> match cb.const_universes with | Monomorphic_const ctx -> - (Univ.ContextSet.of_context ctx) :: acc + ctx :: acc | Polymorphic_const _ -> acc ) [] (Term_typing.uniq_seff eff) @@ -389,7 +389,6 @@ let push_named_def (id,de) senv = | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true in - let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs | OpaqueDef o -> @@ -425,9 +424,8 @@ let labels_of_mib mib = let globalize_constant_universes env cb = match cb.const_universes with - | Monomorphic_const ctx -> - let cstrs = Univ.ContextSet.of_context ctx in - Now (false, cstrs) :: + | Monomorphic_const cstrs -> + Now (false, cstrs) :: (match cb.const_body with | (Undef _ | Def _) -> [] | OpaqueDef lc -> @@ -443,7 +441,7 @@ let globalize_constant_universes env cb = let globalize_mind_universes mb = match mb.mind_universes with | Monomorphic_ind ctx -> - [Now (false, Univ.ContextSet.of_context ctx)] + [Now (false, ctx)] | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] @@ -458,8 +456,8 @@ let constraints_of_sfb env sfb = It also performs the corresponding [add_constraints]. *) type generic_name = - | C of constant - | I of mutual_inductive + | C of Constant.t + | I of MutInd.t | M (** name already known, cf the mod_mp field *) | MT (** name already known, cf the mod_mp field *) @@ -502,7 +500,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constant_role + Constant.t * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -521,7 +519,7 @@ let add_constant_aux no_section senv (kn, cb) = let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver - (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' + (Mod_subst.add_inline_delta_resolver (Constant.user kn) (lev,None)) senv' | _ -> senv' in senv'' @@ -535,7 +533,7 @@ let export_private_constants ~in_section ce senv = (ce, exported), senv let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in + let kn = Constant.make3 senv.modpath dir l in let no_section = DirPath.is_empty dir in let senv = let cb = @@ -562,7 +560,7 @@ let check_mind mie lab = let add_mind dir l mie senv = let () = check_mind mie l in - let kn = make_mind senv.modpath dir l in + let kn = MutInd.make3 senv.modpath dir l in let mib = Term_typing.translate_mind senv.env kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib @@ -860,7 +858,7 @@ let export ?except senv dir = } in let ast, symbols = - if !Flags.native_compiler then + if !Flags.output_native_objects then Nativelibrary.dump_library mp dir senv.env str else [], Nativecode.empty_symbols in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f0f273f35..a30bb37e6 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -60,8 +60,8 @@ val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> constant -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -69,7 +69,7 @@ val inline_private_constants_in_constr : val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry -val universes_of_private : private_constants -> Univ.universe_context_set list +val universes_of_private : private_constants -> Univ.ContextSet.t list val is_curmod_library : safe_environment -> bool @@ -84,13 +84,13 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - (Id.t * Term.types * bool (* polymorphic *)) + (Id.t * Constr.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer (** Insertion of global axioms or definitions *) @@ -103,7 +103,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constant_role + Constant.t * private_constant_role val export_private_constants : in_section:bool -> private_constants Entries.constant_entry -> @@ -113,33 +113,33 @@ val export_private_constants : in_section:bool -> unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - constant safe_transformer + Constant.t safe_transformer (** Adding an inductive type *) val add_mind : DirPath.t -> Label.t -> Entries.mutual_inductive_entry -> - mutual_inductive safe_transformer + MutInd.t safe_transformer (** Adding a module or a module type *) val add_module : Label.t -> Entries.module_entry -> Declarations.inline -> - (module_path * Mod_subst.delta_resolver) safe_transformer + (ModPath.t * Mod_subst.delta_resolver) safe_transformer val add_modtype : Label.t -> Entries.module_type_entry -> Declarations.inline -> - module_path safe_transformer + ModPath.t safe_transformer (** Adding universe constraints *) val push_context_set : - bool -> Univ.universe_context_set -> safe_transformer0 + bool -> Univ.ContextSet.t -> safe_transformer0 val push_context : - bool -> Univ.universe_context -> safe_transformer0 + bool -> Univ.UContext.t -> safe_transformer0 val add_constraints : - Univ.constraints -> safe_transformer0 + Univ.Constraint.t -> safe_transformer0 (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) @@ -150,9 +150,9 @@ val set_typing_flags : Declarations.typing_flags -> safe_transformer0 (** {6 Interactive module functions } *) -val start_module : Label.t -> module_path safe_transformer +val start_module : Label.t -> ModPath.t safe_transformer -val start_modtype : Label.t -> module_path safe_transformer +val start_modtype : Label.t -> ModPath.t safe_transformer val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> @@ -166,17 +166,17 @@ val allow_delayed_constants : bool ref val end_module : Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> - (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer + (ModPath.t * MBId.t list * Mod_subst.delta_resolver) safe_transformer -val end_modtype : Label.t -> (module_path * MBId.t list) safe_transformer +val end_modtype : Label.t -> (ModPath.t * MBId.t list) safe_transformer val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer -val current_modpath : safe_environment -> module_path +val current_modpath : safe_environment -> ModPath.t -val current_dirpath : safe_environment -> dir_path +val current_dirpath : safe_environment -> DirPath.t (** {6 Libraries : loading and saving compilation units } *) @@ -186,26 +186,26 @@ type native_library = Nativecode.global list val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols -val start_library : DirPath.t -> module_path safe_transformer +val start_library : DirPath.t -> ModPath.t safe_transformer val export : ?except:Future.UUIDSet.t -> safe_environment -> DirPath.t -> - module_path * compiled_library * native_library + ModPath.t * compiled_library * native_library (* Constraints are non empty iff the file is a vi2vo *) -val import : compiled_library -> Univ.universe_context_set -> vodigest -> - module_path safe_transformer +val import : compiled_library -> Univ.ContextSet.t -> vodigest -> + ModPath.t safe_transformer (** {6 Safe typing judgments } *) type judgment -val j_val : judgment -> Term.constr -val j_type : judgment -> Term.constr +val j_val : judgment -> Constr.constr +val j_type : judgment -> Constr.constr (** The safe typing of a term returns a typing judgment. *) -val typing : safe_environment -> Term.constr -> judgment +val typing : safe_environment -> Constr.constr -> judgment (** {6 Queries } *) @@ -221,9 +221,9 @@ open Retroknowledge val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a val register : - field -> Retroknowledge.entry -> Term.constr -> safe_transformer0 + field -> Retroknowledge.entry -> Constr.constr -> safe_transformer0 -val register_inline : constant -> safe_transformer0 +val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.constant Names.tableKey -> Conv_oracle.level -> safe_environment + safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment diff --git a/kernel/sorts.ml b/kernel/sorts.ml index cf5207e8d..07688840d 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -14,7 +14,7 @@ type family = InProp | InSet | InType type t = | Prop of contents (* proposition types *) - | Type of universe + | Type of Universe.t let prop = Prop Null let set = Prop Pos @@ -91,7 +91,7 @@ module Hsorts = struct type _t = t type t = _t - type u = universe -> universe + type u = Universe.t -> Universe.t let hashcons huniv = function | Type u as c -> diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 3426d6fd3..65ea75138 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -14,7 +14,7 @@ type family = InProp | InSet | InType type t = | Prop of contents (** Prop and Set *) -| Type of Univ.universe (** Type *) +| Type of Univ.Universe.t (** Type *) val set : t val prop : t @@ -38,5 +38,5 @@ module List : sig val intersect : family list -> family list -> family list end -val univ_of_sort : t -> Univ.universe -val sort_of_univ : Univ.universe -> t +val univ_of_sort : t -> Univ.Universe.t +val sort_of_univ : Univ.Universe.t -> t diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index b564b2a8c..2913c6dfa 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -12,10 +12,11 @@ (* This module checks subtyping of module types *) (*i*) -open Util open Names open Univ +open Util open Term +open Constr open Declarations open Declareops open Reduction @@ -63,11 +64,11 @@ let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = try Label.Map.find l map.objs - with Not_found -> error_no_such_label_sub l (string_of_mp mp) + with Not_found -> error_no_such_label_sub l (ModPath.to_string mp) let get_mod mp map l = try Label.Map.find l map.mods - with Not_found -> error_no_such_label_sub l (string_of_mp mp) + with Not_found -> error_no_such_label_sub l (ModPath.to_string mp) let make_labmap mp list = let add_one (l,e) map = @@ -77,7 +78,7 @@ let make_labmap mp list = | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods } | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods } in - List.fold_right add_one list empty_labmap + CList.fold_right add_one list empty_labmap let check_conv_error error why cst poly f env a1 a2 = @@ -153,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let (ctx2,s2) = dest_arity env t2 in let s1,s2 = match s1, s2 with - | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort + | Type _, Type _ -> (* shortcut here *) Sorts.prop, Sorts.prop | (Prop _, Type _) | (Type _,Prop _) -> error (NotConvertibleInductiveField name) | _ -> (s1, s2) in @@ -181,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in cst in - let mind = mind_of_kn kn1 in + let mind = MutInd.make1 kn1 in let check_cons_types i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst @@ -216,7 +217,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x); if mib1.mind_record <> None then begin - let rec names_prod_letin t = match kind_of_term t with + let rec names_prod_letin t = match kind t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) | Cast(t,_,_) -> names_prod_letin t @@ -272,13 +273,13 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = | Type u when not (is_univ_variable u) -> (* Both types are inferred, no need to recheck them. We cheat and collapse the types to Prop *) - mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) + mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) | Prop _ -> (* The type in the interface is inferred, it may be the case that the type in the implementation is smaller because the body is more reduced. We safely collapse the upper type to Prop *) - mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort) + mkArity (ctx1,Sorts.prop), mkArity (ctx2,Sorts.prop) | Type _ -> (* The type in the interface is inferred and the type in the implementation is not inferred or is inferred but from a diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index b24c20aa0..67df3759e 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -10,4 +10,4 @@ open Univ open Declarations open Environ -val check_subtypes : env -> module_type_body -> module_type_body -> constraints +val check_subtypes : env -> module_type_body -> module_type_body -> Constraint.t diff --git a/kernel/term.ml b/kernel/term.ml index 0e0af2f59..aa8805952 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -11,6 +11,7 @@ open Pp open CErrors open Names open Vars +open Constr (**********************************************************************) (** Redeclaration of types from module Constr *) @@ -20,7 +21,7 @@ type contents = Sorts.contents = Pos | Null type sorts = Sorts.t = | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) + | Type of Univ.Universe.t (** Type *) type sorts_family = Sorts.family = InProp | InSet | InType @@ -30,7 +31,7 @@ type constr = Constr.t type types = Constr.t (** Same as [constr], for documentation purposes. *) -type existential_key = Constr.existential_key +type existential_key = Evar.t type existential = Constr.existential type metavariable = Constr.metavariable @@ -67,7 +68,7 @@ type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint type 'a puniverses = 'a Univ.puniverses (** Simply type aliases *) -type pconstant = constant puniverses +type pconstant = Constant.t puniverses type pinductive = inductive puniverses type pconstructor = constructor puniverses @@ -83,7 +84,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Lambda of Name.t * 'types * 'constr | LetIn of Name.t * 'constr * 'types * 'constr | App of 'constr * 'constr array - | Const of (constant * 'univs) + | Const of (Constant.t * 'univs) | Ind of (inductive * 'univs) | Construct of (constructor * 'univs) | Case of case_info * 'constr * 'constr * 'constr array @@ -165,167 +166,52 @@ let hcons_types = Constr.hcons (* Non primitive term destructors *) (**********************************************************************) -(* Destructor operations : partial functions - Raise [DestKO] if the const has not the expected form *) - -exception DestKO - +exception DestKO = DestKO (* Destructs a de Bruijn index *) -let destRel c = match kind_of_term c with - | Rel n -> n - | _ -> raise DestKO - -(* Destructs an existential variable *) -let destMeta c = match kind_of_term c with - | Meta n -> n - | _ -> raise DestKO - -let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false - -(* Destructs a variable *) -let destVar c = match kind_of_term c with - | Var id -> id - | _ -> raise DestKO - -(* Destructs a type *) -let isSort c = match kind_of_term c with - | Sort _ -> true - | _ -> false - -let destSort c = match kind_of_term c with - | Sort s -> s - | _ -> raise DestKO - -let rec isprop c = match kind_of_term c with - | Sort (Prop _) -> true - | Cast (c,_,_) -> isprop c - | _ -> false - -let rec is_Prop c = match kind_of_term c with - | Sort (Prop Null) -> true - | Cast (c,_,_) -> is_Prop c - | _ -> false - -let rec is_Set c = match kind_of_term c with - | Sort (Prop Pos) -> true - | Cast (c,_,_) -> is_Set c - | _ -> false - -let rec is_Type c = match kind_of_term c with - | Sort (Type _) -> true - | Cast (c,_,_) -> is_Type c - | _ -> false - -let is_small = Sorts.is_small - -let iskind c = isprop c || is_Type c - -(* Tests if an evar *) -let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false - -let isEvar_or_Meta c = match kind_of_term c with - | Evar _ | Meta _ -> true - | _ -> false - -(* Destructs a casted term *) -let destCast c = match kind_of_term c with - | Cast (t1,k,t2) -> (t1,k,t2) - | _ -> raise DestKO - -let isCast c = match kind_of_term c with Cast _ -> true | _ -> false - - -(* Tests if a de Bruijn index *) -let isRel c = match kind_of_term c with Rel _ -> true | _ -> false -let isRelN n c = - match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false - -(* Tests if a variable *) -let isVar c = match kind_of_term c with Var _ -> true | _ -> false -let isVarId id c = - match kind_of_term c with Var id' -> Id.equal id id' | _ -> false - -(* Tests if an inductive *) -let isInd c = match kind_of_term c with Ind _ -> true | _ -> false - -(* Destructs the product (x:t1)t2 *) -let destProd c = match kind_of_term c with - | Prod (x,t1,t2) -> (x,t1,t2) - | _ -> raise DestKO - -let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false - -(* Destructs the abstraction [x:t1]t2 *) -let destLambda c = match kind_of_term c with - | Lambda (x,t1,t2) -> (x,t1,t2) - | _ -> raise DestKO - -let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false - -(* Destructs the let [x:=b:t1]t2 *) -let destLetIn c = match kind_of_term c with - | LetIn (x,b,t1,t2) -> (x,b,t1,t2) - | _ -> raise DestKO - -let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false - -(* Destructs an application *) -let destApp c = match kind_of_term c with - | App (f,a) -> (f, a) - | _ -> raise DestKO - +let destRel = destRel +let destMeta = destRel +let isMeta = isMeta +let destVar = destVar +let isSort = isSort +let destSort = destSort +let isprop = isprop +let is_Prop = is_Prop +let is_Set = is_Set +let is_Type = is_Type +let is_small = is_small +let iskind = iskind +let isEvar = isEvar +let isEvar_or_Meta = isEvar_or_Meta +let destCast = destCast +let isCast = isCast +let isRel = isRel +let isRelN = isRelN +let isVar = isVar +let isVarId = isVarId +let isInd = isInd +let destProd = destProd +let isProd = isProd +let destLambda = destLambda +let isLambda = isLambda +let destLetIn = destLetIn +let isLetIn = isLetIn +let destApp = destApp let destApplication = destApp - -let isApp c = match kind_of_term c with App _ -> true | _ -> false - -(* Destructs a constant *) -let destConst c = match kind_of_term c with - | Const kn -> kn - | _ -> raise DestKO - -let isConst c = match kind_of_term c with Const _ -> true | _ -> false - -(* Destructs an existential variable *) -let destEvar c = match kind_of_term c with - | Evar (kn, a as r) -> r - | _ -> raise DestKO - -(* Destructs a (co)inductive type named kn *) -let destInd c = match kind_of_term c with - | Ind (kn, a as r) -> r - | _ -> raise DestKO - -(* Destructs a constructor *) -let destConstruct c = match kind_of_term c with - | Construct (kn, a as r) -> r - | _ -> raise DestKO - -let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false - -(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) -let destCase c = match kind_of_term c with - | Case (ci,p,c,v) -> (ci,p,c,v) - | _ -> raise DestKO - -let isCase c = match kind_of_term c with Case _ -> true | _ -> false - -let isProj c = match kind_of_term c with Proj _ -> true | _ -> false - -let destProj c = match kind_of_term c with - | Proj (p, c) -> (p, c) - | _ -> raise DestKO - -let destFix c = match kind_of_term c with - | Fix fix -> fix - | _ -> raise DestKO - -let isFix c = match kind_of_term c with Fix _ -> true | _ -> false - -let destCoFix c = match kind_of_term c with - | CoFix cofix -> cofix - | _ -> raise DestKO - -let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false +let isApp = isApp +let destConst = destConst +let isConst = isConst +let destEvar = destEvar +let destInd = destInd +let destConstruct = destConstruct +let isConstruct = isConstruct +let destCase = destCase +let isCase = isCase +let isProj = isProj +let destProj = destProj +let destFix = destFix +let isFix = isFix +let destCoFix = destCoFix +let isCoFix = isCoFix (******************************************************************) (* Flattening and unflattening of embedded applications and casts *) diff --git a/kernel/term.mli b/kernel/term.mli index d5aaf6ad0..f5cb72f4e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -7,6 +7,7 @@ (************************************************************************) open Names +open Constr (** {5 Redeclaration of types from module Constr and Sorts} @@ -15,166 +16,133 @@ open Names *) -type contents = Sorts.contents = Pos | Null - -type sorts = Sorts.t = - | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) - -type sorts_family = Sorts.family = InProp | InSet | InType - -type 'a puniverses = 'a Univ.puniverses - -(** Simply type aliases *) -type pconstant = constant puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type constr = Constr.constr -(** Alias types, for compatibility. *) - -type types = Constr.types -(** Same as [constr], for documentation purposes. *) - -type existential_key = Constr.existential_key - -type existential = Constr.existential - -type metavariable = Constr.metavariable - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : case_style } - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : case_printing - } - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -type rec_declaration = Constr.rec_declaration -type fixpoint = Constr.fixpoint -type cofixpoint = Constr.cofixpoint -type 'constr pexistential = 'constr Constr.pexistential -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of 'constr pexistential - | Sort of 'sort - | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (constant * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) pfixpoint - | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr - -type values = Constr.values +exception DestKO +[@@ocaml.deprecated "Alias for [Constr.DestKO]"] (** {5 Simple term case analysis. } *) - val isRel : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isRel]"] val isRelN : int -> constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isRelN]"] val isVar : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isVar]"] val isVarId : Id.t -> constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isVarId]"] val isInd : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isInd]"] val isEvar : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isEvar]"] val isMeta : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isMeta]"] val isEvar_or_Meta : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"] val isSort : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isSort]"] val isCast : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isCast]"] val isApp : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isApp]"] val isLambda : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isLambda]"] val isLetIn : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isletIn]"] val isProd : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isProp]"] val isConst : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isConst]"] val isConstruct : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isConstruct]"] val isFix : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isFix]"] val isCoFix : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isCoFix]"] val isCase : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isCase]"] val isProj : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isProj]"] val is_Prop : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.is_Prop]"] val is_Set : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.is_Set]"] val isprop : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.isprop]"] val is_Type : constr -> bool +[@@ocaml.deprecated "Alias for [Constr.is_Type]"] val iskind : constr -> bool -val is_small : sorts -> bool +[@@ocaml.deprecated "Alias for [Constr.is_kind]"] +val is_small : Sorts.t -> bool +[@@ocaml.deprecated "Alias for [Constr.is_small]"] (** {5 Term destructors } *) (** Destructor operations are partial functions and @raise DestKO if the term has not the expected form. *) -exception DestKO - (** Destructs a de Bruijn index *) val destRel : constr -> int +[@@ocaml.deprecated "Alias for [Constr.destRel]"] (** Destructs an existential variable *) val destMeta : constr -> metavariable +[@@ocaml.deprecated "Alias for [Constr.destMeta]"] (** Destructs a variable *) val destVar : constr -> Id.t +[@@ocaml.deprecated "Alias for [Constr.destVar]"] (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) -val destSort : constr -> sorts +val destSort : constr -> Sorts.t +[@@ocaml.deprecated "Alias for [Constr.destSort]"] (** Destructs a casted term *) val destCast : constr -> constr * cast_kind * constr +[@@ocaml.deprecated "Alias for [Constr.destCast]"] (** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) val destProd : types -> Name.t * types * types +[@@ocaml.deprecated "Alias for [Constr.destProd]"] (** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) val destLambda : constr -> Name.t * types * constr +[@@ocaml.deprecated "Alias for [Constr.destLambda]"] (** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) val destLetIn : constr -> Name.t * constr * types * constr +[@@ocaml.deprecated "Alias for [Constr.destLetIn]"] (** Destructs an application *) val destApp : constr -> constr * constr array +[@@ocaml.deprecated "Alias for [Constr.destApp]"] (** Obsolete synonym of destApp *) val destApplication : constr -> constr * constr array +[@@ocaml.deprecated "Alias for [Constr.destApplication]"] (** Decompose any term as an applicative term; the list of args can be empty *) val decompose_app : constr -> constr * constr list +[@@ocaml.deprecated "Alias for [Constr.decompose_app]"] (** Same as [decompose_app], but returns an array. *) val decompose_appvect : constr -> constr * constr array +[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] (** Destructs a constant *) -val destConst : constr -> constant puniverses +val destConst : constr -> Constant.t Univ.puniverses +[@@ocaml.deprecated "Alias for [Constr.destConst]"] (** Destructs an existential variable *) val destEvar : constr -> existential +[@@ocaml.deprecated "Alias for [Constr.destEvar]"] (** Destructs a (co)inductive type *) -val destInd : constr -> inductive puniverses +val destInd : constr -> inductive Univ.puniverses +[@@ocaml.deprecated "Alias for [Constr.destInd]"] (** Destructs a constructor *) -val destConstruct : constr -> constructor puniverses +val destConstruct : constr -> constructor Univ.puniverses +[@@ocaml.deprecated "Alias for [Constr.destConstruct]"] (** Destructs a [match c as x in I args return P with ... | Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args @@ -182,9 +150,11 @@ return P in t1], or [if c then t1 else t2]) @return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array +[@@ocaml.deprecated "Alias for [Constr.destCase]"] (** Destructs a projection *) val destProj : constr -> projection * constr +[@@ocaml.deprecated "Alias for [Constr.destProj]"] (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} @@ -194,9 +164,10 @@ val destProj : constr -> projection * constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) val destFix : constr -> fixpoint +[@@ocaml.deprecated "Alias for [Constr.destFix]"] val destCoFix : constr -> cofixpoint - +[@@ocaml.deprecated "Alias for [Constr.destCoFix]"] (** {5 Derived constructors} *) @@ -354,7 +325,7 @@ val strip_lam_assum : constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * sorts +type arity = Context.Rel.t * Sorts.t (** Build an "arity" from its canonical form *) val mkArity : arity -> types @@ -368,7 +339,7 @@ val isArity : types -> bool (** {5 Kind of type} *) type ('constr, 'types) kind_of_type = - | SortType of sorts + | SortType of Sorts.t | CastType of 'types * 'types | ProdType of Name.t * 'types * 'types | LetInType of Name.t * 'constr * 'types * 'types @@ -378,23 +349,23 @@ val kind_of_type : types -> (constr, types) kind_of_type (** {5 Redeclaration of stuff from module [Sorts]} *) -val set_sort : sorts -(** Alias for Sorts.set *) +val set_sort : Sorts.t +[@@ocaml.deprecated "Alias for Sorts.set"] -val prop_sort : sorts -(** Alias for Sorts.prop *) +val prop_sort : Sorts.t +[@@ocaml.deprecated "Alias for Sorts.prop"] -val type1_sort : sorts -(** Alias for Sorts.type1 *) +val type1_sort : Sorts.t +[@@ocaml.deprecated "Alias for Sorts.type1"] -val sorts_ord : sorts -> sorts -> int -(** Alias for Sorts.compare *) +val sorts_ord : Sorts.t -> Sorts.t -> int +[@@ocaml.deprecated "Alias for Sorts.compare"] -val is_prop_sort : sorts -> bool -(** Alias for Sorts.is_prop *) +val is_prop_sort : Sorts.t -> bool +[@@ocaml.deprecated "Alias for Sorts.is_prop"] -val family_of_sort : sorts -> sorts_family -(** Alias for Sorts.family *) +val family_of_sort : Sorts.t -> Sorts.family +[@@ocaml.deprecated "Alias for Sorts.family"] (** {5 Redeclaration of stuff from module [Constr]} @@ -403,90 +374,215 @@ val family_of_sort : sorts -> sorts_family (** {6 Term constructors. } *) val mkRel : int -> constr +[@@ocaml.deprecated "Alias for Constr.mkRel"] val mkVar : Id.t -> constr +[@@ocaml.deprecated "Alias for Constr.mkVar"] val mkMeta : metavariable -> constr +[@@ocaml.deprecated "Alias for Constr.mkMeta"] val mkEvar : existential -> constr -val mkSort : sorts -> types +[@@ocaml.deprecated "Alias for Constr.mkEvar"] +val mkSort : Sorts.t -> types +[@@ocaml.deprecated "Alias for Constr.mkSort"] val mkProp : types +[@@ocaml.deprecated "Alias for Constr.mkProp"] val mkSet : types -val mkType : Univ.universe -> types +[@@ocaml.deprecated "Alias for Constr.mkSet"] +val mkType : Univ.Universe.t -> types +[@@ocaml.deprecated "Alias for Constr.mkType"] val mkCast : constr * cast_kind * constr -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkProd : Name.t * types * types -> types +[@@ocaml.deprecated "Alias for Constr"] val mkLambda : Name.t * types * constr -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkLetIn : Name.t * constr * types * constr -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkApp : constr * constr array -> constr -val mkConst : constant -> constr +[@@ocaml.deprecated "Alias for Constr"] +val mkConst : Constant.t -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkProj : projection * constr -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkInd : inductive -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkConstruct : constructor -> constr -val mkConstU : constant puniverses -> constr -val mkIndU : inductive puniverses -> constr -val mkConstructU : constructor puniverses -> constr +[@@ocaml.deprecated "Alias for Constr"] +val mkConstU : Constant.t Univ.puniverses -> constr +[@@ocaml.deprecated "Alias for Constr"] +val mkIndU : inductive Univ.puniverses -> constr +[@@ocaml.deprecated "Alias for Constr"] +val mkConstructU : constructor Univ.puniverses -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkConstructUi : (pinductive * int) -> constr +[@@ocaml.deprecated "Alias for Constr"] val mkCase : case_info * constr * constr * constr array -> constr +[@@ocaml.deprecated "Alias for Constr.mkCase"] val mkFix : fixpoint -> constr +[@@ocaml.deprecated "Alias for Constr.mkFix"] val mkCoFix : cofixpoint -> constr +[@@ocaml.deprecated "Alias for Constr.mkCoFix"] (** {6 Aliases} *) val eq_constr : constr -> constr -> bool -(** Alias for [Constr.equal] *) +[@@ocaml.deprecated "Alias for Constr.equal"] (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) val eq_constr_univs : constr UGraph.check_function +[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"] (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe constraints in [u]. *) val leq_constr_univs : constr UGraph.check_function +[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"] (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and ignoring universe instances. *) val eq_constr_nounivs : constr -> constr -> bool +[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"] val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -(** Alias for [Constr.kind] *) +[@@ocaml.deprecated "Alias for Constr.kind"] val compare : constr -> constr -> int -(** Alias for [Constr.compare] *) +[@@ocaml.deprecated "Alias for [Constr.compare]"] val constr_ord : constr -> constr -> int -(** Alias for [Term.compare] *) +[@@ocaml.deprecated "Alias for [Term.compare]"] val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a -(** Alias for [Constr.fold] *) +[@@ocaml.deprecated "Alias for [Constr.fold]"] val map_constr : (constr -> constr) -> constr -> constr -(** Alias for [Constr.map] *) +[@@ocaml.deprecated "Alias for [Constr.map]"] val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -(** Alias for [Constr.map_with_binders] *) +[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] -val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses -val univ_of_sort : sorts -> Univ.universe -val sort_of_univ : Univ.universe -> sorts +val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses +[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] +val univ_of_sort : Sorts.t -> Univ.Universe.t +[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] +val sort_of_univ : Univ.Universe.t -> Sorts.t +[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"] val iter_constr : (constr -> unit) -> constr -> unit -(** Alias for [Constr.iter] *) +[@@ocaml.deprecated "Alias for [Constr.iter]"] val iter_constr_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -(** Alias for [Constr.iter_with_binders] *) +[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool -(** Alias for [Constr.compare_head] *) +[@@ocaml.deprecated "Alias for [Constr.compare_head]"] + +type constr = Constr.constr +[@@ocaml.deprecated "Alias for Constr.t"] + +(** Alias types, for compatibility. *) + +type types = Constr.types +[@@ocaml.deprecated "Alias for Constr.types"] + +type contents = Sorts.contents = Pos | Null +[@@ocaml.deprecated "Alias for Sorts.contents"] + +type sorts = Sorts.t = + | Prop of Sorts.contents (** Prop and Set *) + | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.t"] + +type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] + +type 'a puniverses = 'a Univ.puniverses +[@@ocaml.deprecated "Alias for Constr.puniverses"] + +(** Simply type aliases *) +type pconstant = Constr.pconstant +[@@ocaml.deprecated "Alias for Constr.pconstant"] +type pinductive = Constr.pinductive +[@@ocaml.deprecated "Alias for Constr.pinductive"] +type pconstructor = Constr.pconstructor +[@@ocaml.deprecated "Alias for Constr.pconstructor"] +type existential_key = Evar.t +[@@ocaml.deprecated "Alias for Evar.t"] +type existential = Constr.existential +[@@ocaml.deprecated "Alias for Constr.existential"] +type metavariable = Constr.metavariable +[@@ocaml.deprecated "Alias for Constr.metavariable"] + +type case_style = Constr.case_style = + LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle +[@@ocaml.deprecated "Alias for Constr.case_style"] + +type case_printing = Constr.case_printing = + { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style } +[@@ocaml.deprecated "Alias for Constr.case_printing"] + +type case_info = Constr.case_info = + { ci_ind : inductive; + ci_npar : int; + ci_cstr_ndecls : int array; + ci_cstr_nargs : int array; + ci_pp_info : Constr.case_printing + } +[@@ocaml.deprecated "Alias for Constr.case_info"] + +type cast_kind = Constr.cast_kind = + VMcast | NATIVEcast | DEFAULTcast | REVERTcast +[@@ocaml.deprecated "Alias for Constr.cast_kind"] + +type rec_declaration = Constr.rec_declaration +[@@ocaml.deprecated "Alias for Constr.rec_declaration"] +type fixpoint = Constr.fixpoint +[@@ocaml.deprecated "Alias for Constr.fixpoint"] +type cofixpoint = Constr.cofixpoint +[@@ocaml.deprecated "Alias for Constr.cofixpoint"] +type 'constr pexistential = 'constr Constr.pexistential +[@@ocaml.deprecated "Alias for Constr.pexistential"] +type ('constr, 'types) prec_declaration = + ('constr, 'types) Constr.prec_declaration +[@@ocaml.deprecated "Alias for Constr.prec_declaration"] +type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint +[@@ocaml.deprecated "Alias for Constr.pfixpoint"] +type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint +[@@ocaml.deprecated "Alias for Constr.pcofixpoint"] -val hash_constr : constr -> int -(** Alias for [Constr.hash] *) +type ('constr, 'types, 'sort, 'univs) kind_of_term = + ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = + | Rel of int + | Var of Id.t + | Meta of Constr.metavariable + | Evar of 'constr Constr.pexistential + | Sort of 'sort + | Cast of 'constr * Constr.cast_kind * 'types + | Prod of Name.t * 'types * 'types + | Lambda of Name.t * 'types * 'constr + | LetIn of Name.t * 'constr * 'types * 'constr + | App of 'constr * 'constr array + | Const of (Constant.t * 'univs) + | Ind of (inductive * 'univs) + | Construct of (constructor * 'univs) + | Case of Constr.case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) Constr.pfixpoint + | CoFix of ('constr, 'types) Constr.pcofixpoint + | Proj of projection * 'constr +[@@ocaml.deprecated "Alias for Constr.kind_of_term"] + +type values = Constr.values +[@@ocaml.deprecated "Alias for Constr.values"] -(*********************************************************************) +val hash_constr : Constr.constr -> int +[@@ocaml.deprecated "Alias for Constr.hash"] -val hcons_sorts : sorts -> sorts -(** Alias for [Constr.hashcons_sorts] *) +val hcons_sorts : Sorts.t -> Sorts.t +[@@ocaml.deprecated "Alias for [Sorts.hcons]"] -val hcons_constr : constr -> constr -(** Alias for [Constr.hashcons] *) +val hcons_constr : Constr.constr -> Constr.constr +[@@ocaml.deprecated "Alias for [Constr.hcons]"] -val hcons_types : types -> types -(** Alias for [Constr.hashcons] *) +val hcons_types : Constr.types -> Constr.types +[@@ocaml.deprecated "Alias for [Constr.hcons]"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e28c8e826..70dd6438d 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -15,7 +15,7 @@ open CErrors open Util open Names -open Term +open Constr open Declarations open Environ open Entries @@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff = | _ -> assert false in match cb.const_universes with - | Monomorphic_const cnstctx -> + | Monomorphic_const univs -> (** Abstract over the term at the top of the proof *) let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in - let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) | Polymorphic_const auctx -> @@ -154,7 +153,7 @@ let inline_side_effects env body ctx side_eff = (** Lift free rel variables *) if n <= k then t else mkRel (n + len - i - 1) - | _ -> map_constr_with_binders ((+) 1) (fun k t -> subst_const i k t) k t + | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t in let map_args i (na, b, ty, opaque) = (** Both the type and the body may mention other constants *) @@ -199,13 +198,13 @@ let check_signatures curmb sl = let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in - match sl, kind_of_term b with + match sl, kind b with | (None|Some 0), _ -> b, e, acc | Some sl, LetIn (n,c,ty,bo) -> aux (Some (sl-1)) bo (Environ.push_rel (LocalDef (n,c,ty)) e) (`Let(n,c,ty)::acc) | Some sl, App(hd,arg) -> - begin match kind_of_term hd with + begin match kind hd with | Lambda (n,ty,bo) -> aux (Some (sl-1)) bo (Environ.push_rel (LocalAssum (n,ty)) e) (`Cut(n,ty,arg)::acc) @@ -228,24 +227,30 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:state_id Feedback.Complete) -let abstract_constant_universes abstract uctx = - if not abstract then +let abstract_constant_universes abstract = function + | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx - else - let sbst, auctx = Univ.abstract_universes uctx in - sbst, Polymorphic_const auctx + | Polymorphic_const_entry uctx -> + if not abstract then + Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx) + else + let sbst, auctx = Univ.abstract_universes uctx in + sbst, Polymorphic_const auctx let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with - | ParameterEntry (ctx,poly,(t,uctx),nl) -> - let env = push_context ~strict:(not poly) uctx env in + | ParameterEntry (ctx,(t,uctx),nl) -> + let env = match uctx with + | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env + | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env + in let j = infer env t in - let abstract = poly && not (Option.is_empty kn) in + let abstract = not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in - let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in + let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in { Cooking.cook_body = Undef nl; cook_type = t; @@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; const_entry_universes = Monomorphic_const_entry univs } as c) -> - let env = push_context ~strict:true univs env in + let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -283,7 +288,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx in - let c = hcons_constr j.uj_val in + let c = Constr.hcons j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in @@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let poly, univs = match c.const_entry_universes with + let poly, univsctx = match c.const_entry_universes with | Monomorphic_const_entry univs -> false, univs - | Polymorphic_const_entry univs -> true, univs + | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs in - let univsctx = Univ.ContextSet.of_context univs in let ctx = Univ.ContextSet.union univsctx ctx in let body, ctx, _ = match trust with | Pure -> body, ctx, [] | SideEffects _ -> inline_side_effects env body ctx side_eff in let env = push_context_set ~strict:(not poly) ctx env in - let abstract = poly && not (Option.is_empty kn) in - let usubst, univs = - abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) - in + let abstract = not (Option.is_empty kn) in + let ctx = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) + else Monomorphic_const_entry ctx + in + let usubst, univs = abstract_constant_universes abstract ctx in let j = infer env body in let typ = match typ with | None -> @@ -325,7 +331,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let _ = judge_of_cast env j DEFAULTcast tj in Vars.subst_univs_level_constr usubst t in - let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in + let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) else Def (Mod_subst.from_val def) @@ -359,7 +365,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry in let term, typ = pb.proj_eta in { - Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; cook_proj = Some pb; cook_universes = univs; @@ -525,7 +531,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effect_role + Constant.t * constant_body * side_effect_role let export_side_effects mb env ce = match ce with @@ -556,7 +562,7 @@ let export_side_effects mb env ce = let env = Environ.add_constant kn cb env in match cb.const_universes with | Monomorphic_const ctx -> - Environ.push_context ~strict:true ctx env + Environ.push_context_set ~strict:true ctx env | Polymorphic_const _ -> env end | kn, cb, `Opaque(_, ctx), _ -> @@ -564,7 +570,7 @@ let export_side_effects mb env ce = let env = Environ.add_constant kn cb env in match cb.const_universes with | Monomorphic_const cstctx -> - let env = Environ.push_context ~strict:true cstctx env in + let env = Environ.push_context_set ~strict:true cstctx env in Environ.push_context_set ~strict:true ctx env | Polymorphic_const _ -> env end diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index b16f81c5a..55da4197e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Declarations open Entries @@ -19,7 +19,7 @@ type _ trust = | SideEffects : structure_body -> side_effects trust val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> - constant_def * types * Univ.universe_context + constant_def * types * Univ.ContextSet.t val translate_local_assum : env -> types -> types @@ -47,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - 'a trust -> env -> constant -> 'a constant_entry -> + 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body type side_effect_role = @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effect_role + Constant.t * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -66,14 +66,14 @@ val export_side_effects : exported_side_effect list * unit constant_entry val translate_mind : - env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body + env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body -val translate_recipe : env -> constant -> Cooking.recipe -> constant_body +val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> constant option -> +val infer_declaration : trust:'a trust -> env -> Constant.t option -> 'a constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + Constant.t -> env -> Cooking.result -> constant_body diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 9813fc566..781c6bfbc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Reduction @@ -45,8 +45,8 @@ type ('constr, 'types) ptype_error = | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr - | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment - * (sorts_family * sorts_family * arity_error) option + | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -59,7 +59,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error @@ -115,6 +115,7 @@ let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) let error_elim_explain kp ki = + let open Sorts in match kp,ki with | (InType | InSet), InProp -> NonInformativeToInformative | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 95a963da2..72861f6e4 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ (** Type errors. {% \label{%}typeerrors{% }%} *) @@ -46,8 +46,8 @@ type ('constr, 'types) ptype_error = | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment | ReferenceVariables of Id.t * 'constr - | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment - * (sorts_family * sorts_family * arity_error) option + | ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment + * (Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info | NumberBranches of ('constr, 'types) punsafe_judgment * int @@ -60,7 +60,7 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.constraints + | UnsatisfiedConstraints of Univ.Constraint.t type type_error = (constr, types) ptype_error @@ -77,8 +77,8 @@ val error_assumption : env -> unsafe_judgment -> 'a val error_reference_variables : env -> Id.t -> constr -> 'a val error_elim_arity : - env -> pinductive -> sorts_family list -> constr -> unsafe_judgment -> - (sorts_family * sorts_family * arity_error) option -> 'a + env -> pinductive -> Sorts.family list -> constr -> unsafe_judgment -> + (Sorts.family * Sorts.family * arity_error) option -> 'a val error_case_not_inductive : env -> unsafe_judgment -> 'a @@ -103,6 +103,6 @@ val error_ill_formed_rec_body : val error_ill_typed_rec_body : env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a -val error_elim_explain : sorts_family -> sorts_family -> arity_error +val error_elim_explain : Sorts.family -> Sorts.family -> arity_error -val error_unsatisfied_constraints : env -> Univ.constraints -> 'a +val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b40badd7c..4a935f581 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -10,7 +10,8 @@ open CErrors open Util open Names open Univ -open Term +open Sorts +open Constr open Vars open Declarations open Environ @@ -38,7 +39,7 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let check_type env c t = - match kind_of_term(whd_all env t) with + match kind(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -57,7 +58,7 @@ let check_assumption env t ty = (* Prop and Set *) -let type1 = mkSort type1_sort +let type1 = mkSort Sorts.type1 (* Type of Type(i). *) @@ -152,7 +153,7 @@ let type_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then typ else - (match kind_of_term (whd_all env typ) with + (match kind (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try @@ -298,9 +299,9 @@ let type_of_projection env p c ct = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); + assert(MutInd.equal pb.proj_ind (fst ind)); let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty + substl (c :: CList.rev args) ty (* Fixpoints. *) @@ -325,7 +326,7 @@ let check_fixpoint env lna lar vdef vdeft = arbitraires et non plus des variables *) let rec execute env cstr = let open Context.Rel.Declaration in - match kind_of_term cstr with + match kind cstr with (* Atomic terms *) | Sort s -> type_of_sort s @@ -346,7 +347,7 @@ let rec execute env cstr = | App (f,args) -> let argst = execute_array env args in let ft = - match kind_of_term f with + match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args @@ -434,8 +435,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 96be6c14a..5584b6ab4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -7,8 +7,8 @@ (************************************************************************) open Names +open Constr open Univ -open Term open Environ open Entries @@ -41,8 +41,8 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : contents -> unsafe_judgment -val judge_of_type : universe -> unsafe_judgment +val judge_of_prop_contents : Sorts.contents -> unsafe_judgment +val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) val type_of_relative : env -> int -> types @@ -71,8 +71,8 @@ val judge_of_abstraction : -> unsafe_judgment (** {6 Type of a product. } *) -val sort_of_product : env -> sorts -> sorts -> sorts -val type_of_product : env -> Name.t -> sorts -> sorts -> types +val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t +val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types val judge_of_product : env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 9793dd881..f1e8d1031 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -890,23 +890,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + let key = CProfile.declare_profile "merge_constraints" in + CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + let key = CProfile.declare_profile "check_constraints" in + CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + let check_eq_key = CProfile.declare_profile "check_eq" in + CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq + diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 2fe555018..f71d83d85 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -9,63 +9,64 @@ open Univ (** {6 Graphs of universes. } *) - type t - type universes = t +[@@ocaml.deprecated "Use UGraph.t"] -type 'a check_function = universes -> 'a -> 'a -> bool -val check_leq : universe check_function -val check_eq : universe check_function -val check_eq_level : universe_level check_function +type 'a check_function = t -> 'a -> 'a -> bool -(** The empty graph of universes *) -val empty_universes : universes +val check_leq : Universe.t check_function +val check_eq : Universe.t check_function +val check_eq_level : Level.t check_function (** The initial graph of universes: Prop < Set *) -val initial_universes : universes +val initial_universes : t + +(** Check if we are in the initial case *) +val is_initial_universes : t -> bool + +(** Check equality of instances w.r.t. a universe graph *) +val check_eq_instances : Instance.t check_function + +(** {6 ... } *) +(** Merge of constraints in a universes graph. + The function [merge_constraints] merges a set of constraints in a given + universes graph. It raises the exception [UniverseInconsistency] if the + constraints are not satisfiable. *) -val is_initial_universes : universes -> bool +val enforce_constraint : univ_constraint -> t -> t +val merge_constraints : Constraint.t -> t -> t -val sort_universes : universes -> universes +val check_constraint : t -> univ_constraint -> bool +val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. @raises AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared -val add_universe : universe_level -> bool -> universes -> universes +val add_universe : Level.t -> bool -> t -> t -(** {6 ... } *) -(** Merge of constraints in a universes graph. - The function [merge_constraints] merges a set of constraints in a given - universes graph. It raises the exception [UniverseInconsistency] if the - constraints are not satisfiable. *) +(** {6 Pretty-printing of universes. } *) -val enforce_constraint : univ_constraint -> universes -> universes -val merge_constraints : constraints -> universes -> universes +val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t -val constraints_of_universes : universes -> constraints +(** The empty graph of universes *) +val empty_universes : t +[@@ocaml.deprecated "Use UGraph.initial_universes"] -val check_constraint : universes -> univ_constraint -> bool -val check_constraints : constraints -> universes -> bool +val sort_universes : t -> t -val check_eq_instances : Instance.t check_function -(** Check equality of instances w.r.t. a universe graph *) +val constraints_of_universes : t -> Constraint.t val check_subtype : AUContext.t check_function (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of [ctx1]. *) -(** {6 Pretty-printing of universes. } *) - -val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t - (** {6 Dumping to a file } *) val dump_universes : - (constraint_type -> string -> string -> unit) -> - universes -> unit + (constraint_type -> string -> string -> unit) -> t -> unit (** {6 Debugging} *) -val check_universes_invariants : universes -> unit +val check_universes_invariants : t -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 7fe4f8274..8cf9028fb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -192,6 +192,10 @@ module Level = struct let make m n = make (Level (n, Names.DirPath.hcons m)) + let name u = + match data u with + | Level (n, d) -> Some (d, n) + | _ -> None end (** Level maps *) @@ -337,19 +341,16 @@ struct returning [SuperSame] if they refer to the same level at potentially different increments or [SuperDiff] if they are different. The booleans indicate if the left expression is "smaller" than the right one in both cases. *) - let super (u,n as x) (v,n' as y) = + let super (u,n) (v,n') = let cmp = Level.compare u v in if Int.equal cmp 0 then SuperSame (n < n') else - match x, y with - | (l,0), (l',0) -> - let open RawLevel in - (match Level.data l, Level.data l' with - | Prop, Prop -> SuperSame false - | Prop, _ -> SuperSame true - | _, Prop -> SuperSame false - | _, _ -> SuperDiff cmp) - | _, _ -> SuperDiff cmp + let open RawLevel in + match Level.data u, n, Level.data v, n' with + | Prop, _, Prop, _ -> SuperSame (n < n') + | Prop, 0, _, _ -> SuperSame true + | _, _, Prop, 0 -> SuperSame false + | _, _, _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -499,6 +500,7 @@ struct let smartmap = List.smartmap + let map = List.map end type universe = Universe.t @@ -1053,6 +1055,7 @@ struct let constraints (univs, cst) = cst let levels (univs, cst) = univs + let size (univs,_) = LSet.cardinal univs end type universe_context_set = ContextSet.t diff --git a/kernel/univ.mli b/kernel/univ.mli index 94116e473..459394439 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -7,7 +7,6 @@ (************************************************************************) (** Universes. *) - module Level : sig type t @@ -20,11 +19,11 @@ sig val is_small : t -> bool (** Is the universe set or prop? *) - + val is_prop : t -> bool val is_set : t -> bool (** Is it specifically Prop or Set *) - + val compare : t -> t -> int (** Comparison function *) @@ -46,21 +45,24 @@ sig val var : int -> t val var_index : t -> int option + + val name : t -> (Names.DirPath.t * int) option end type universe_level = Level.t -(** Alias name. *) +[@@ocaml.deprecated "Use Level.t"] (** Sets of universe levels *) -module LSet : -sig - include CSig.SetS with type elt = universe_level - +module LSet : +sig + include CSig.SetS with type elt = Level.t + val pr : (Level.t -> Pp.t) -> t -> Pp.t (** Pretty-printing *) end type universe_set = LSet.t +[@@ocaml.deprecated "Use LSet.t"] module Universe : sig @@ -106,83 +108,86 @@ sig val super : t -> t (** The universe strictly above *) - + val sup : t -> t -> t (** The l.u.b. of 2 universes *) - val type0m : t + val type0m : t (** image of Prop in the universes hierarchy *) - - val type0 : t + + val type0 : t (** image of Set in the universes hierarchy *) - - val type1 : t + + val type1 : t (** the universe of the type of Prop/Set *) val exists : (Level.t * int -> bool) -> t -> bool val for_all : (Level.t * int -> bool) -> t -> bool + + val map : (Level.t * int -> 'a) -> t -> 'a list end type universe = Universe.t +[@@ocaml.deprecated "Use Universe.t"] (** Alias name. *) -val pr_uni : universe -> Pp.t - -(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... +val pr_uni : Universe.t -> Pp.t + +(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) -val type0m_univ : universe -val type0_univ : universe -val type1_univ : universe +val type0m_univ : Universe.t +val type0_univ : Universe.t +val type1_univ : Universe.t -val is_type0_univ : universe -> bool -val is_type0m_univ : universe -> bool -val is_univ_variable : universe -> bool -val is_small_univ : universe -> bool +val is_type0_univ : Universe.t -> bool +val is_type0m_univ : Universe.t -> bool +val is_univ_variable : Universe.t -> bool +val is_small_univ : Universe.t -> bool -val sup : universe -> universe -> universe -val super : universe -> universe +val sup : Universe.t -> Universe.t -> Universe.t +val super : Universe.t -> Universe.t -val universe_level : universe -> universe_level option +val universe_level : Universe.t -> Level.t option (** [univ_level_mem l u] Is l is mentionned in u ? *) -val univ_level_mem : universe_level -> universe -> bool +val univ_level_mem : Level.t -> Universe.t -> bool (** [univ_level_rem u v min] removes [u] from [v], resulting in [min] if [v] was exactly [u]. *) -val univ_level_rem : universe_level -> universe -> universe -> universe +val univ_level_rem : Level.t -> Universe.t -> Universe.t -> Universe.t (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq -type univ_constraint = universe_level * constraint_type * universe_level +type univ_constraint = Level.t * constraint_type * Level.t module Constraint : sig include Set.S with type elt = univ_constraint end type constraints = Constraint.t +[@@ocaml.deprecated "Use Constraint.t"] -val empty_constraint : constraints -val union_constraint : constraints -> constraints -> constraints -val eq_constraint : constraints -> constraints -> bool +val empty_constraint : Constraint.t +val union_constraint : Constraint.t -> Constraint.t -> Constraint.t +val eq_constraint : Constraint.t -> Constraint.t -> bool -(** A value with universe constraints. *) -type 'a constrained = 'a * constraints +(** A value with universe Constraint.t. *) +type 'a constrained = 'a * Constraint.t (** Constrained *) -val constraints_of : 'a constrained -> constraints - -(** Enforcing constraints. *) +val constraints_of : 'a constrained -> Constraint.t -type 'a constraint_function = 'a -> 'a -> constraints -> constraints +(** Enforcing Constraint.t. *) +type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t -val enforce_eq : universe constraint_function -val enforce_leq : universe constraint_function -val enforce_eq_level : universe_level constraint_function -val enforce_leq_level : universe_level constraint_function +val enforce_eq : Universe.t constraint_function +val enforce_leq : Universe.t constraint_function +val enforce_eq_level : Level.t constraint_function +val enforce_leq_level : Level.t constraint_function (** Type explanation is used to decorate error messages to provide useful explanation why a given constraint is rejected. It is composed @@ -194,19 +199,19 @@ val enforce_leq_level : universe_level constraint_function universes in the path are canonical. Note that each step does not necessarily correspond to an actual constraint, but reflect how the system stores the graph and may result from combination of several - constraints... + Constraint.t... *) -type explanation = (constraint_type * universe) list -type univ_inconsistency = constraint_type * universe * universe * explanation option +type explanation = (constraint_type * Universe.t) list +type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option exception UniverseInconsistency of univ_inconsistency (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) -module LMap : +module LMap : sig - include CMap.ExtS with type key = universe_level and module Set := LSet + include CMap.ExtS with type key = Level.t and module Set := LSet val union : 'a t -> 'a t -> 'a t (** [union x y] favors the bindings in the first map. *) @@ -226,18 +231,18 @@ type 'a universe_map = 'a LMap.t (** {6 Substitution} *) -type universe_subst_fn = universe_level -> universe -type universe_level_subst_fn = universe_level -> universe_level +type universe_subst_fn = Level.t -> Universe.t +type universe_level_subst_fn = Level.t -> Level.t (** A full substitution, might involve algebraic universes *) -type universe_subst = universe universe_map -type universe_level_subst = universe_level universe_map +type universe_subst = Universe.t universe_map +type universe_level_subst = Level.t universe_map val level_subst_of : universe_subst_fn -> universe_level_subst_fn (** {6 Universe instances} *) -module Instance : +module Instance : sig type t (** A universe instance represents a vector of argument universes @@ -279,49 +284,51 @@ sig end type universe_instance = Instance.t +[@@ocaml.deprecated "Use Instance.t"] -val enforce_eq_instances : universe_instance constraint_function +val enforce_eq_instances : Instance.t constraint_function -type 'a puniverses = 'a * universe_instance +type 'a puniverses = 'a * Instance.t val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool -(** A vector of universe levels with universe constraints, - representiong local universe variables and associated constraints *) +(** A vector of universe levels with universe Constraint.t, + representiong local universe variables and associated Constraint.t *) module UContext : -sig +sig type t val make : Instance.t constrained -> t val empty : t val is_empty : t -> bool - + val instance : t -> Instance.t - val constraints : t -> constraints + val constraints : t -> Constraint.t - val dest : t -> Instance.t * constraints + val dest : t -> Instance.t * Constraint.t (** Keeps the order of the instances *) val union : t -> t -> t - (* the number of universes in the context *) + (** the number of universes in the context *) val size : t -> int end type universe_context = UContext.t +[@@ocaml.deprecated "Use UContext.t"] module AUContext : -sig +sig type t val repr : t -> UContext.t (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of - the context and [cstr] the abstracted constraints. *) + the context and [cstr] the abstracted Constraint.t. *) val empty : t val is_empty : t -> bool @@ -335,68 +342,71 @@ sig val union : t -> t -> t val instantiate : Instance.t -> t -> Constraint.t - (** Generate the set of instantiated constraints **) + (** Generate the set of instantiated Constraint.t **) end type abstract_universe_context = AUContext.t +[@@ocaml.deprecated "Use AUContext.t"] (** Universe info for inductive types: A context of universe levels - with universe constraints, representing local universe variables - and constraints, together with a context of universe levels with - universe constraints, representing conditions for subtyping used + with universe Constraint.t, representing local universe variables + and Constraint.t, together with a context of universe levels with + universe Constraint.t, representing conditions for subtyping used for inductive types. This data structure maintains the invariant that the context for - subtyping constraints is exactly twice as big as the context for - universe constraints. *) + subtyping Constraint.t is exactly twice as big as the context for + universe Constraint.t. *) module CumulativityInfo : sig type t - val make : universe_context * universe_context -> t + val make : UContext.t * UContext.t -> t val empty : t val is_empty : t -> bool - val univ_context : t -> universe_context - val subtyp_context : t -> universe_context + val univ_context : t -> UContext.t + val subtyp_context : t -> UContext.t - (** This function takes a universe context representing constraints + (** This function takes a universe context representing Constraint.t of an inductive and a Instance.t of fresh universe names for the subtyping (with the same length as the context in the given universe context) and produces a UInfoInd.t that with the trivial subtyping relation. *) - val from_universe_context : universe_context -> universe_instance -> t + val from_universe_context : UContext.t -> Instance.t -> t val subtyping_susbst : t -> universe_level_subst end type cumulativity_info = CumulativityInfo.t +[@@ocaml.deprecated "Use CumulativityInfo.t"] module ACumulativityInfo : sig type t - val univ_context : t -> abstract_universe_context - val subtyp_context : t -> abstract_universe_context + val univ_context : t -> AUContext.t + val subtyp_context : t -> AUContext.t end type abstract_cumulativity_info = ACumulativityInfo.t +[@@ocaml.deprecated "Use ACumulativityInfo.t"] (** Universe contexts (as sets) *) module ContextSet : -sig - type t = universe_set constrained +sig + type t = LSet.t constrained val empty : t val is_empty : t -> bool - val singleton : universe_level -> t + val singleton : Level.t -> t val of_instance : Instance.t -> t - val of_set : universe_set -> t + val of_set : LSet.t -> t val equal : t -> t -> bool val union : t -> t -> t @@ -406,39 +416,43 @@ sig much smaller than the right one. *) val diff : t -> t -> t - val add_universe : universe_level -> t -> t - val add_constraints : constraints -> t -> t + val add_universe : Level.t -> t -> t + val add_constraints : Constraint.t -> t -> t val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) val sort_levels : Level.t array -> Level.t array - val to_context : t -> universe_context - val of_context : universe_context -> t + val to_context : t -> UContext.t + val of_context : UContext.t -> t + + val constraints : t -> Constraint.t + val levels : t -> LSet.t - val constraints : t -> constraints - val levels : t -> universe_set + (** the number of universes in the context *) + val size : t -> int end -(** A set of universes with universe constraints. - We linearize the set to a list after typechecking. +(** A set of universes with universe Constraint.t. + We linearize the set to a list after typechecking. Beware, representation could change. *) type universe_context_set = ContextSet.t +[@@ocaml.deprecated "Use ContextSet.t"] (** A value in a universe context (resp. context set). *) -type 'a in_universe_context = 'a * universe_context -type 'a in_universe_context_set = 'a * universe_context_set +type 'a in_universe_context = 'a * UContext.t +type 'a in_universe_context_set = 'a * ContextSet.t val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool (** Substitution of universes. *) -val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level -val subst_univs_level_universe : universe_level_subst -> universe -> universe -val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints +val subst_univs_level_level : universe_level_subst -> Level.t -> Level.t +val subst_univs_level_universe : universe_level_subst -> Universe.t -> Universe.t +val subst_univs_level_constraints : universe_level_subst -> Constraint.t -> Constraint.t val subst_univs_level_abstract_universe_context : - universe_level_subst -> abstract_universe_context -> abstract_universe_context -val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance + universe_level_subst -> AUContext.t -> AUContext.t +val subst_univs_level_instance : universe_level_subst -> Instance.t -> Instance.t (** Level to universe substitutions. *) @@ -446,32 +460,32 @@ val empty_subst : universe_subst val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn -val subst_univs_universe : universe_subst_fn -> universe -> universe -val subst_univs_constraints : universe_subst_fn -> constraints -> constraints +val subst_univs_universe : universe_subst_fn -> Universe.t -> Universe.t +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t (** Substitution of instances *) -val subst_instance_instance : universe_instance -> universe_instance -> universe_instance -val subst_instance_universe : universe_instance -> universe -> universe +val subst_instance_instance : Instance.t -> Instance.t -> Instance.t +val subst_instance_universe : Instance.t -> Universe.t -> Universe.t -val make_instance_subst : universe_instance -> universe_level_subst -val make_inverse_instance_subst : universe_instance -> universe_level_subst +val make_instance_subst : Instance.t -> universe_level_subst +val make_inverse_instance_subst : Instance.t -> universe_level_subst -val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context +val abstract_universes : UContext.t -> universe_level_subst * AUContext.t -val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info +val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t -val make_abstract_instance : abstract_universe_context -> universe_instance +val make_abstract_instance : AUContext.t -> Instance.t (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.t -val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t -val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t -val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t -val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t -val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t -val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t -val explain_universe_inconsistency : (Level.t -> Pp.t) -> +val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t +val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t +val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t +val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t +val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t +val explain_universe_inconsistency : (Level.t -> Pp.t) -> univ_inconsistency -> Pp.t val pr_universe_level_subst : universe_level_subst -> Pp.t @@ -479,23 +493,28 @@ val pr_universe_subst : universe_subst -> Pp.t (** {6 Hash-consing } *) -val hcons_univ : universe -> universe -val hcons_constraints : constraints -> constraints -val hcons_universe_set : universe_set -> universe_set -val hcons_universe_context : universe_context -> universe_context -val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context -val hcons_universe_context_set : universe_context_set -> universe_context_set -val hcons_cumulativity_info : cumulativity_info -> cumulativity_info -val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info +val hcons_univ : Universe.t -> Universe.t +val hcons_constraints : Constraint.t -> Constraint.t +val hcons_universe_set : LSet.t -> LSet.t +val hcons_universe_context : UContext.t -> UContext.t +val hcons_abstract_universe_context : AUContext.t -> AUContext.t +val hcons_universe_context_set : ContextSet.t -> ContextSet.t +val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t +val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t (******) (* deprecated: use qualified names instead *) -val compare_levels : universe_level -> universe_level -> int -val eq_levels : universe_level -> universe_level -> bool +val compare_levels : Level.t -> Level.t -> int +[@@ocaml.deprecated "Use Level.compare"] + +val eq_levels : Level.t -> Level.t -> bool +[@@ocaml.deprecated "Use Level.equal"] (** deprecated: Equality of formal universe expressions. *) -val equal_universes : universe -> universe -> bool +val equal_universes : Universe.t -> Universe.t -> bool +[@@ocaml.deprecated "Use Universe.equal"] -(** Universes of constraints *) -val universes_of_constraints : constraints -> universe_set +(** Universes of Constraint.t *) +val universes_of_constraints : Constraint.t -> LSet.t +[@@ocaml.deprecated "Use Constraint.universes_of"] diff --git a/kernel/vars.ml b/kernel/vars.ml index d0dad02ec..eae917b5a 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -133,8 +133,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -274,8 +274,8 @@ let subst_univs_constr subst c = let subst_univs_constr = if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr let subst_univs_level_constr subst c = @@ -347,12 +347,12 @@ let subst_instance_constr subst c = in aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx -type id_key = constant tableKey +type id_key = Constant.t tableKey let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index 59dc09a75..964de4e95 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -141,8 +141,8 @@ val subst_univs_level_constr : universe_level_subst -> constr -> constr val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t (** Instance substitution for polymorphism. *) -val subst_instance_constr : universe_instance -> constr -> constr -val subst_instance_context : universe_instance -> Context.Rel.t -> Context.Rel.t +val subst_instance_constr : Instance.t -> constr -> constr +val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t -type id_key = constant tableKey +type id_key = Constant.t tableKey val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 0e452621c..3ef297b1f 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = let mib = Environ.lookup_mind mi env in let ulen = match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx + | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx | Declarations.Cumulative_ind cumi -> Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) @@ -204,4 +204,4 @@ let vm_conv cv_pb env t1 t2 = let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () -let _ = Reduction.set_vm_conv vm_conv +let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv diff --git a/kernel/vconv.mli b/kernel/vconv.mli index f4e680c69..7f727df47 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Environ open Reduction diff --git a/kernel/vm.ml b/kernel/vm.ml index 6b7a86d6f..51101f88e 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -7,7 +7,8 @@ (************************************************************************) open Names -open Term +open Sorts +open Constr open Cbytecodes external set_drawinstr : unit -> unit = "coq_set_drawinstr" @@ -137,7 +138,7 @@ type vswitch = { type atom = | Aid of Vars.id_key | Aind of inductive - | Atype of Univ.universe + | Atype of Univ.Universe.t (* Zippers *) @@ -152,7 +153,7 @@ type stack = zipper list type to_up = values type whd = - | Vsort of sorts + | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -160,7 +161,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack - | Vuniv_level of Univ.universe_level + | Vuniv_level of Univ.Level.t (************************************************) (* Abstract machine *****************************) @@ -216,7 +217,7 @@ let apply_varray vf varray = (* Destructors ***********************************) (*************************************************) -let uni_lvl_val (v : values) : Univ.universe_level = +let uni_lvl_val (v : values) : Univ.Level.t = let whd = Obj.magic v in match whd with | Vuniv_level lvl -> lvl @@ -357,7 +358,7 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = constant tableKey + type t = Constant.t tableKey let equal = Names.eq_table_key Constant.equal open Hashset.Combine let hash = function @@ -654,10 +655,10 @@ let apply_whd k whd = let rec pr_atom a = Pp.(match a with | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Names.pr_con c + | ConstKey c -> Constant.print c | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" | Atype _ -> str "Atype(") and pr_whd w = Pp.(match w with @@ -679,4 +680,4 @@ and pr_zipper z = | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")") + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index df638acc1..bc38452d4 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,5 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + open Names -open Term +open Constr open Cbytecodes (** Debug printing *) @@ -23,7 +31,7 @@ type arguments type atom = | Aid of Vars.id_key | Aind of inductive - | Atype of Univ.universe + | Atype of Univ.Universe.t (** Zippers *) @@ -38,7 +46,7 @@ type stack = zipper list type to_up type whd = - | Vsort of sorts + | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -46,7 +54,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vatom_stk of atom * stack - | Vuniv_level of Univ.universe_level + | Vuniv_level of Univ.Level.t (** For debugging purposes only *) @@ -59,14 +67,14 @@ val pr_stack : stack -> Pp.t val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values -val val_of_constant : constant -> values +val val_of_constant : Constant.t -> values external val_of_annot_switch : annot_switch -> values = "%identity" (** Destructors *) val whd_val : values -> whd -val uni_lvl_val : values -> Univ.universe_level +val uni_lvl_val : values -> Univ.Level.t (** Arguments *) |