diff options
Diffstat (limited to 'kernel')
32 files changed, 263 insertions, 194 deletions
diff --git a/kernel/closure.ml b/kernel/cClosure.ml index 960bdb649a..d475f097ce 100644 --- a/kernel/closure.ml +++ b/kernel/cClosure.ml @@ -19,7 +19,7 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) -open Errors +open CErrors open Util open Pp open Names @@ -37,17 +37,20 @@ let delta = ref 0 let eta = ref 0 let zeta = ref 0 let evar = ref 0 -let iota = ref 0 +let nb_match = ref 0 +let fix = ref 0 +let cofix = ref 0 let prune = ref 0 let reset () = - beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0; - prune := 0 + beta := 0; delta := 0; zeta := 0; evar := 0; nb_match := 0; fix := 0; + cofix := 0; evar := 0; prune := 0 let stop() = Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ - int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ + int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++ + str " cofix=" ++ int !cofix ++ str" prune=" ++ int !prune ++ str"]") let incr_cnt red cnt = @@ -78,7 +81,9 @@ module type RedFlagsSig = sig val fBETA : red_kind val fDELTA : red_kind val fETA : red_kind - val fIOTA : red_kind + val fMATCH : red_kind + val fFIX : red_kind + val fCOFIX : red_kind val fZETA : red_kind val fCONST : constant -> red_kind val fVAR : Id.t -> red_kind @@ -103,14 +108,19 @@ module RedFlags = (struct r_eta : bool; r_const : transparent_state; r_zeta : bool; - r_iota : bool } + r_match : bool; + r_fix : bool; + r_cofix : bool } - type red_kind = BETA | DELTA | ETA | IOTA | ZETA + type red_kind = BETA | DELTA | ETA | MATCH | FIX + | COFIX | ZETA | CONST of constant | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA - let fIOTA = IOTA + let fMATCH = MATCH + let fFIX = FIX + let fCOFIX = COFIX let fZETA = ZETA let fCONST kn = CONST kn let fVAR id = VAR id @@ -120,7 +130,9 @@ module RedFlags = (struct r_eta = false; r_const = all_opaque; r_zeta = false; - r_iota = false } + r_match = false; + r_fix = false; + r_cofix = false } let red_add red = function | BETA -> { red with r_beta = true } @@ -129,7 +141,9 @@ module RedFlags = (struct | CONST kn -> let (l1,l2) = red.r_const in { red with r_const = l1, Cpred.add kn l2 } - | IOTA -> { red with r_iota = true } + | MATCH -> { red with r_match = true } + | FIX -> { red with r_fix = true } + | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> let (l1,l2) = red.r_const in @@ -140,9 +154,11 @@ module RedFlags = (struct | ETA -> { red with r_eta = false } | DELTA -> { red with r_delta = false } | CONST kn -> - let (l1,l2) = red.r_const in + let (l1,l2) = red.r_const in { red with r_const = l1, Cpred.remove kn l2 } - | IOTA -> { red with r_iota = false } + | MATCH -> { red with r_match = false } + | FIX -> { red with r_fix = false } + | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> let (l1,l2) = red.r_const in @@ -165,11 +181,13 @@ module RedFlags = (struct let c = Id.Pred.mem id l in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta - | IOTA -> incr_cnt red.r_iota iota + | MATCH -> incr_cnt red.r_match nb_match + | FIX -> incr_cnt red.r_fix fix + | COFIX -> incr_cnt red.r_cofix cofix | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta - let red_projection red p = + let red_projection red p = if Projection.unfolded p then true else red_set red (fCONST (Projection.constant p)) @@ -177,15 +195,20 @@ end : RedFlagsSig) open RedFlags -let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA] -let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] -let betaiota = mkflags [fBETA;fIOTA] +let all = mkflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX] +let allnolet = mkflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX] let beta = mkflags [fBETA] -let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] +let betadeltazeta = mkflags [fBETA;fDELTA;fZETA] +let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX] +let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let betazeta = mkflags [fBETA;fZETA] +let delta = mkflags [fDELTA] +let zeta = mkflags [fZETA] +let nored = no_red (* Removing fZETA for finer behaviour would break many developments *) -let unfold_side_flags = [fBETA;fIOTA;fZETA] -let unfold_side_red = mkflags [fBETA;fIOTA;fZETA] +let unfold_side_flags = [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let unfold_side_red = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] let unfold_red kn = let flag = match kn with | EvalVarRef id -> fVAR id @@ -215,7 +238,7 @@ type table_key = constant puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' - + module IdKeyHash = struct open Hashset.Combine @@ -238,7 +261,7 @@ type 'a infos_cache = { i_rels : constr option array; i_tab : 'a KeyTable.t } -and 'a infos = { +and 'a infos = { i_flags : reds; i_cache : 'a infos_cache } @@ -297,7 +320,7 @@ let defined_rels flags env = (* else (0,[])*) let create mk_cl flgs env evars = - let cache = + let cache = { i_repr = mk_cl; i_env = env; i_sigma = evars; @@ -647,7 +670,7 @@ let rec zip m stk = | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s - | Zproj (i,j,cst) :: s -> + | Zproj (i,j,cst) :: s -> zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s | Zfix(fx,par)::s -> zip fx (par @ append_stack [|m|] s) @@ -754,7 +777,7 @@ let rec try_drop_parameters depth n argstk = let aft = Array.sub args n (q-n) in reloc_rargs depth (append_stack aft s) | Zshift(k)::s -> try_drop_parameters (depth-k) n s - | [] -> + | [] -> if Int.equal n 0 then [] else raise Not_found | _ -> assert false @@ -763,23 +786,23 @@ let rec try_drop_parameters depth n argstk = let drop_parameters depth n argstk = try try_drop_parameters depth n argstk with Not_found -> - (* we know that n < stack_args_size(argstk) (if well-typed term) *) + (* we know that n < stack_args_size(argstk) (if well-typed term) *) anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor") (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding - to the conversion of the eta expansion of t, considered as an inhabitant + to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive - of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + of the constructor term [c] + @raises Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with | Some (Some (_,projs,pbs)) when - mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + mib.Declarations.mind_finite == Decl_kinds.BiFinite -> (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') -> arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in @@ -789,12 +812,12 @@ let eta_expand_ind_stack env ind m s (f, s') = let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) term = FProj (Projection.make p true, right) }) projs in - argss, [Zapp hstack] + argss, [Zapp hstack] | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) let rec project_nth_arg n argstk = match argstk with - | Zapp args :: s -> + | Zapp args :: s -> let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) @@ -849,7 +872,7 @@ let rec knh info m stk = (match try Some (lookup_projection p (info_env info)) with Not_found -> None with | None -> (m, stk) | Some pb -> - knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, + knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, Projection.constant p) :: zupdate m stk)) else (m,stk) @@ -896,23 +919,27 @@ let rec knr info m stk = (match ref_value_cache info (RelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> + | FConstruct((ind,c),u) -> + let use_match = red_set info.i_flags fMATCH in + let use_fix = red_set info.i_flags fFIX in + if use_match || use_fix then (match strip_update_shift_app m stk with - | (depth, args, ZcaseT(ci,_,br,e)::s) -> + | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in knit info e br.(c-1) (rargs@s) - | (_, cargs, Zfix(fx,par)::s) -> + | (_, cargs, Zfix(fx,par)::s) when use_fix -> let rarg = fapp_stack(m,cargs) in let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in knit info fxe fxbd stk' - | (depth, args, Zproj (n, m, cst)::s) -> + | (depth, args, Zproj (n, m, cst)::s) when use_match -> let rargs = drop_parameters depth n args in let rarg = project_nth_arg m rargs in kni info rarg s | (_,args,s) -> (m,args@s)) - | FCoFix _ when red_set info.i_flags fIOTA -> + else (m,stk) + | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in @@ -947,8 +974,8 @@ let rec zip_term zfun m stk = let t = mkCase(ci, zfun (mk_clos e p), m, Array.map (fun b -> zfun (mk_clos e b)) br) in zip_term zfun t s - | Zproj(_,_,p)::s -> - let t = mkProj (Projection.make p true, m) in + | Zproj(_,_,p)::s -> + let t = mkProj (Projection.make p true, m) in zip_term zfun t s | Zfix(fx,par)::s -> let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in @@ -1028,18 +1055,17 @@ let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env let env_of_infos infos = infos.i_cache.i_env -let infos_with_reds infos reds = +let infos_with_reds infos reds = { infos with i_flags = reds } -let unfold_reference info key = +let unfold_reference info key = match key with | ConstKey (kn,_) -> if red_set info.i_flags (fCONST kn) then - ref_value_cache info key + ref_value_cache info key else None - | VarKey i -> + | VarKey i -> if red_set info.i_flags (fVAR i) then ref_value_cache info key else None | _ -> ref_value_cache info key - diff --git a/kernel/closure.mli b/kernel/cClosure.mli index 8e172290fb..077756ac74 100644 --- a/kernel/closure.mli +++ b/kernel/cClosure.mli @@ -41,8 +41,10 @@ module type RedFlagsSig = sig val fBETA : red_kind val fDELTA : red_kind val fETA : red_kind - (** This flag is never used by the kernel reduction but pretyping does *) - val fIOTA : red_kind + (** The fETA flag is never used by the kernel reduction but pretyping does *) + val fMATCH : red_kind + val fFIX : red_kind + val fCOFIX : red_kind val fZETA : red_kind val fCONST : constant -> red_kind val fVAR : Id.t -> red_kind @@ -64,7 +66,7 @@ module type RedFlagsSig = sig (** Tests if a reduction kind is set *) val red_set : reds -> red_kind -> bool - + (** This tests if the projection is in unfolded state already or is unfodable due to delta. *) val red_projection : reds -> projection -> bool @@ -73,11 +75,18 @@ end module RedFlags : RedFlagsSig open RedFlags -val beta : reds -val betaiota : reds -val betadeltaiota : reds -val betaiotazeta : reds -val betadeltaiotanolet : reds +(* These flags do not contain eta *) +val all : reds +val allnolet : reds +val beta : reds +val betadeltazeta : reds +val betaiota : reds +val betaiotazeta : reds +val betazeta : reds +val delta : reds +val zeta : reds +val nored : reds + val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds @@ -86,7 +95,7 @@ val unfold_red : evaluable_global_reference -> reds type table_key = constant puniverses tableKey type 'a infos_cache -type 'a infos = { +type 'a infos = { i_flags : reds; i_cache : 'a infos_cache } @@ -195,16 +204,16 @@ val whd_val : clos_infos -> fconstr -> constr val whd_stack : clos_infos -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding - to the conversion of the eta expansion of t, considered as an inhabitant +(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding + to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive - of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + of the constructor term [c] + @raises Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) -val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> +val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (fconstr * stack) -> stack * stack (** Conversion auxiliary functions to do step by step normalisation *) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index a705e3004f..8d4de523a1 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -142,11 +142,29 @@ type fv = fv_elem array exception NotClosed +module Fv_elem = +struct +type t = fv_elem + +let compare e1 e2 = match e1, e2 with +| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 +| FVnamed _, _ -> -1 +| FVrel _, FVnamed _ -> 1 +| FVrel r1, FVrel r2 -> Int.compare r1 r2 +| FVrel _, FVuniv_var _ -> -1 +| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 +| FVuniv_var i1, _ -> 1 + +end + +module FvMap = Map.Make(Fv_elem) + (*spiwack: both type have been moved from Cbytegen because I needed then for the retroknowledge *) type vm_env = { size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list (* [fvn; ... ;fv1] *) + fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (* reverse mapping *) } diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 6fa0841af9..5f1f09d00c 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -139,11 +139,14 @@ type fv = fv_elem array closed terms. *) exception NotClosed +module FvMap : Map.S with type key = fv_elem + (*spiwack: both type have been moved from Cbytegen because I needed them for the retroknowledge *) type vm_env = { size : int; (** length of the list [n] *) - fv_rev : fv_elem list (** [fvn; ... ;fv1] *) + fv_rev : fv_elem list; (** [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (** reverse mapping *) } diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 8cbc3ab445..008955d804 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -93,7 +93,12 @@ open Pre_env type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t -let empty_fv = { size= 0; fv_rev = [] } +let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } +let push_fv d e = { + size = e.size + 1; + fv_rev = d :: e.fv_rev; + fv_fwd = FvMap.add d e.size e.fv_fwd; +} let fv r = !(r.in_env) @@ -184,20 +189,15 @@ let push_local sz r = in_stack = (sz + 1) :: r.in_stack } (*i Compilation of variables *) -let find_at f l = - let rec aux n = function - | [] -> raise Not_found - | hd :: tl -> if f hd then n else aux (n + 1) tl - in aux 1 l +let find_at fv env = FvMap.find fv env.fv_fwd let pos_named id r = let env = !(r.in_env) in let cid = FVnamed id in - let f = function FVnamed id' -> Id.equal id id' | _ -> false in - try Kenvacc(r.offset + env.size - (find_at f env.fv_rev)) + try Kenvacc(r.offset + find_at cid env) with Not_found -> let pos = env.size in - r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev}; + r.in_env := push_fv cid env; Kenvacc (r.offset + pos) let pos_rel i r sz = @@ -212,11 +212,10 @@ let pos_rel i r sz = let i = i - r.nb_rec in let db = FVrel(i) in let env = !(r.in_env) in - let f = function FVrel j -> Int.equal i j | _ -> false in - try Kenvacc(r.offset + env.size - (find_at f env.fv_rev)) + try Kenvacc(r.offset + find_at db env) with Not_found -> let pos = env.size in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + r.in_env := push_fv db env; Kenvacc(r.offset + pos) let pos_universe_var i r sz = @@ -224,15 +223,11 @@ let pos_universe_var i r sz = Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) else let env = !(r.in_env) in - let f = function - | FVuniv_var u -> Int.equal i u - | _ -> false - in - try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + let db = FVuniv_var i in + try Kenvacc (r.offset + find_at db env) with Not_found -> let pos = env.size in - let db = FVuniv_var i in - r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ; + r.in_env := push_fv db env; Kenvacc(r.offset + pos) (*i Examination of the continuation *) @@ -907,7 +902,7 @@ let compile fail_on_error ?universes:(universes=0) env c = Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then Errors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.errorlabstrm "compile" else (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 462413bd38..3f1cf92487 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = | _ -> Cpred.add c oracle.cst_trstate in { oracle with cst_opacity; cst_trstate; } - | RelKey _ -> Errors.error "set_strategy: RelKey" + | RelKey _ -> CErrors.error "set_strategy: RelKey" let fold_strategy f { var_opacity; cst_opacity; } accu = let fvar id lvl accu = f (VarKey id) lvl accu in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6dc2a617dd..1345991503 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -13,7 +13,7 @@ (* This module implements kernel-level discharching of local declarations over global constants and inductive types *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 047da682ad..e195618b6b 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -219,17 +219,9 @@ and eval_to_patch env (buff,pl,fv) = eval_tcode tc vm_env and val_of_constr env c = - let (_,fun_code,_ as ccfv) = - try match compile true env c with - | Some v -> v - | None -> assert false - with reraise -> - let reraise = Errors.push reraise in - let () = print_string "can not compile \n" in - let () = Format.print_flush () in - iraise reraise - in - eval_to_patch env (to_memory ccfv) + match compile true env c with + | Some v -> eval_to_patch env (to_memory v) + | None -> assert false let set_transparent_const kn = () (* !?! *) let set_opaque_const kn = () (* !?! *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 7d8c3c0af6..7351a87d44 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,7 +20,7 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index c2c8ee2424..bd91c689d2 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -35,12 +35,12 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> {utj_val = c; utj_type = s } | _ -> error_not_type env (make_judge c t) let check_type env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -157,7 +157,7 @@ let judge_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_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6942e1334..de97268b37 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -50,7 +50,7 @@ let is_indices_matter () = !indices_matter let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else - let t' = whd_betadeltaiota env t in + let t' = whd_all env t in if noccur_between x nvars t' then Some t' else None @@ -129,7 +129,7 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in @@ -409,7 +409,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_betadeltaiota env params.(param_index)) with + match kind_of_term (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -436,7 +436,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_betadeltaiota env p) with + ( match kind_of_term (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) @@ -466,7 +466,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_betadeltaiota env c in + let c' = whd_all env c in match kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -495,7 +495,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( constructor [cn] has a type of the shape [… -> c … -> P], where, 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_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -513,7 +513,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in - let largs = List.map (whd_betadeltaiota env) largs in + let largs = List.map (whd_all env) largs in let nmr1 = (match ra with Mrec _ -> compute_rec_par ienv paramsctxt nmr largs @@ -603,7 +603,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( inductive type. *) 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_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8e26370ecf..3c4c2796ee 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -29,20 +29,20 @@ let lookup_mind_specif env (kn,tyi) = (mib, mib.mind_packets.(tyi)) let find_rectype env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term 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_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) @@ -313,7 +313,7 @@ let check_allowed_sort ksort specif = 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_betadeltaiota env pt in + let pt' = whd_all env pt in match kind_of_term pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = @@ -323,7 +323,7 @@ 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_betadeltaiota env' a2) with + let ksort = match kind_of_term (whd_all env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in @@ -563,7 +563,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -586,7 +586,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_betadeltaiota env c in + let c' = whd_all env c in match kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -618,7 +618,7 @@ close to check_positive in indtypes.ml, but does no positivity check and does no 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_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -677,7 +677,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_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> @@ -706,7 +706,7 @@ let restrict_spec env spec p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,args = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_all env s) in match kind_of_term i with | Ind i -> begin match spec with @@ -727,7 +727,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_betadeltaiota renv.env t) in + let f,l = decompose_app (whd_all renv.env t) in match kind_of_term f with | Rel k -> subterm_var k renv | Case (ci,p,c,lbr) -> @@ -854,11 +854,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = - let t = whd_betadeltaiota env ar in + let t = whd_all env ar in match stack, kind_of_term t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in - let ty, args = decompose_app (whd_betadeltaiota env a) in + let ty, args = decompose_app (whd_all env a) in let elt = match kind_of_term ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -990,6 +990,10 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l + | Proj (p, c) -> + List.iter (check_rec_call renv []) l; + check_rec_call renv [] c + | Var id -> begin let open Context.Named.Declaration in @@ -1009,8 +1013,6 @@ let check_one_fix renv recpos trees def = | (Evar _ | Meta _) -> () | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *) - - | Proj (p, c) -> check_rec_call renv [] c and check_nested_fix_body renv decr recArgsDecrArg body = if Int.equal decr 0 then @@ -1047,7 +1049,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_betadeltaiota env def) with + match kind_of_term (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 @@ -1101,7 +1103,7 @@ let anomaly_ill_typed () = anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in + let b = whd_all env c in match kind_of_term b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b @@ -1113,7 +1115,7 @@ let rec codomain_is_coind env c = 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_betadeltaiota env t) in + let c,args = decompose_app (whd_all env t) in match kind_of_term c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 1e132e3ab2..15f213ce9c 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -25,7 +25,7 @@ Nativelambda Nativecode Nativelib Environ -Closure +CClosure Reduction Nativeconv Type_errors diff --git a/kernel/modops.ml b/kernel/modops.ml index 6fe7e382c6..0f0056ed43 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -264,7 +264,7 @@ let add_retroknowledge mp = |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e |_ -> - Errors.anomaly ~label:"Modops.add_retroknowledge" + CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term") in fun lclrk env -> diff --git a/kernel/names.ml b/kernel/names.ml index 9abc9842a8..9267a64d61 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -36,7 +36,7 @@ struct let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 44cf21cff0..ad5b04f3d1 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors + +open CErrors open Names open Term open Declarations @@ -21,8 +22,12 @@ to OCaml code. *) (** Local names **) +(* The first component is there for debugging purposes only *) type lname = { lname : name; luid : int } +let eq_lname ln1 ln2 = + Int.equal ln1.luid ln2.luid + let dummy_lname = { lname = Anonymous; luid = -1 } module LNord = @@ -81,6 +86,9 @@ let eq_gname gn1 gn2 = | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 | _ -> false +let dummy_gname = + Grel 0 + open Hashset.Combine let gname_hash gn = match gn with @@ -403,9 +411,13 @@ let opush_lnames n env lns = let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = match t1, t2 with | MLlocal ln1, MLlocal ln2 -> + (try Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2) + with Not_found -> + eq_lname ln1 ln2) | MLglobal gn1', MLglobal gn2' -> eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2') + || (eq_gname gn1 gn2' && eq_gname gn2 gn1') | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2 | MLlam (lns1, ml1), MLlam (lns2, ml2) -> Int.equal (Array.length lns1) (Array.length lns2) && @@ -718,6 +730,11 @@ let push_global_norm gn params body = let push_global_case gn params annot a accu bs = push_global gn (Gletcase (gn, params, annot, a, accu, bs)) +(* Compares [t1] and [t2] up to alpha-equivalence. [t1] and [t2] may contain + free variables. *) +let eq_mllambda t1 t2 = + eq_mllambda dummy_gname dummy_gname 0 LNmap.empty LNmap.empty t1 t2 + (*s Compilation environment *) type env = @@ -896,9 +913,7 @@ let rec insert cargs body rl = let params = rm_params fv params in rl:= Rcons(ref [(c,params)], fv, body, ref Rnil) | Rcons(l,fv,body',rl) -> - (** ppedrot: It seems we only want to factorize common branches. It should - not matter to do so with a subapproximation by (==). *) - if body == body' then + if eq_mllambda body body' then let (c,params) = cargs in let params = rm_params fv params in l := (c,params)::!l @@ -1445,12 +1460,14 @@ let optimize gdef l = end | MLif(t,b1,b2) -> + (* This optimization is critical: it applies to all fixpoints that start + by matching on their recursive argument *) let t = optimize s t in let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) - when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *) + when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end | MLmatch(annot,a,accu,bs) -> @@ -1929,13 +1946,15 @@ let compile_constant env sigma prefix ~interactive con cb = arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix -let loaded_native_files = ref ([] : string list) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) + +let loaded_native_files = ref StringSet.empty -let is_loaded_native_file s = String.List.mem s !loaded_native_files +let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = - if not (is_loaded_native_file s) then - loaded_native_files := s :: !loaded_native_files + loaded_native_files := StringSet.add s !loaded_native_files let is_code_loaded ~interactive name = match !name with diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 2f985e15ac..3c0afe3805 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors + +open CErrors open Names open Nativelib open Reduction diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index d4a67b3999..1c58c7445c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -8,7 +8,7 @@ open Util open Nativevalues open Nativecode -open Errors +open CErrors open Envars (** This file provides facilities to access OCaml compiler and dynamic linker, @@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds = if not (Sys.file_exists f) then begin let msg = "Cannot find native compiler file " ^ f in - if fatal then Errors.error msg + if fatal then CErrors.error msg else if !Flags.debug then Feedback.msg_debug (Pp.str msg) end else @@ -133,7 +133,7 @@ let call_linker ?(fatal=true) prefix f upds = if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix with Dynlink.Error e as exn -> - let exn = Errors.push exn in + let exn = CErrors.push exn in let msg = "Dynlink error, " ^ Dynlink.error_message e in if fatal then (Feedback.msg_error (Pp.str msg); iraise exn) else if !Flags.debug then Feedback.msg_debug (Pp.str msg)); diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index d6fdfefa02..8093df3044 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -7,7 +7,7 @@ (************************************************************************) open Term open Names -open Errors +open CErrors open Util (** This module defines the representation of values internally used by diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 0c8772d8d2..130f1eb039 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -26,10 +26,10 @@ let empty_opaquetab = Int.Map.empty, DirPath.initial (* hooks *) let default_get_opaque dp _ = - Errors.error + CErrors.error ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) let default_get_univ dp _ = - Errors.error + CErrors.error ("Cannot access universe constraints of opaque proofs in library " ^ DirPath.to_string dp) @@ -45,8 +45,8 @@ let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with | Indirect (_,_,i) -> if not (Int.Map.mem i prfs) - then Errors.anomaly (Pp.str "Indirect in a different table") - else Errors.anomaly (Pp.str "Already an indirect opaque") + then CErrors.anomaly (Pp.str "Indirect in a different table") + else CErrors.anomaly (Pp.str "Already an indirect opaque") | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in let id = Int.Map.cardinal prfs in @@ -54,21 +54,21 @@ let turn_indirect dp o (prfs,odp) = match o with let ndp = if DirPath.equal dp odp then odp else if DirPath.equal odp DirPath.initial then dp - else Errors.anomaly + else CErrors.anomaly (Pp.str "Using the same opaque table for multiple dirpaths") in Indirect ([],dp,id), (prfs, ndp) let subst_opaque sub = function | Indirect (s,dp,i) -> Indirect (sub::s,dp,i) - | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque") + | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque") let iter_direct_opaque f = function - | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u)) let discharge_direct_opaque ~cook_constr ci = function - | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque") + | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque") | Direct (d,cu) -> Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u)) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 710bfa19b8..6c664f7918 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,13 +15,13 @@ (* Equal inductive types by Jacek Chrzaszcz as part of the module system, Aug 2002 *) -open Errors +open CErrors open Util open Names open Term open Vars open Environ -open Closure +open CClosure open Esubst open Context.Rel.Declaration @@ -107,17 +107,17 @@ let whd_betaiotazeta env x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t - | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) + | _ -> whd_val (create_clos_infos all env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t - | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) + | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) @@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible -> (* else the oracle tells which constant is to be expanded *) - let oracle = Closure.oracle_of_infos infos in + let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with @@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = else raise NotConvertible let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = - let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in + let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs @@ -731,7 +731,7 @@ let betazeta_appvect = lambda_appvect_assum * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -742,7 +742,7 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in match kind_of_term t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in @@ -754,7 +754,7 @@ let dest_prod env = (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in @@ -764,7 +764,7 @@ let dest_prod_assum env = prodec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let rty' = whd_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in @@ -772,7 +772,7 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3896446925..9812c45f7b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -12,9 +12,11 @@ open Environ (*********************************************************************** s Reduction functions *) +(* None of these functions do eta reduction *) + val whd_betaiotazeta : env -> constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr val whd_betaiota : env -> constr -> constr val nf_betaiota : env -> constr -> constr diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fc61559301..09f7bd75cd 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -190,7 +190,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." + CErrors.error "Needs option -impredicative-set." | _ -> () end @@ -344,10 +344,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - Errors.error + CErrors.error ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") with Not_found -> - Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") in Array.iter check needed @@ -365,7 +365,7 @@ let safe_push_named d env = let _ = try let _ = Environ.lookup_named id env in - Errors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.error ("Identifier "^Id.to_string id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -815,8 +815,8 @@ let export ?except senv dir = let senv = try join_safe_environment ?except senv with e -> - let e = Errors.push e in - Errors.errorlabstrm "export" (Errors.iprint e) + let e = CErrors.push e in + CErrors.errorlabstrm "export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -851,6 +851,9 @@ let export ?except senv dir = let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; + if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then + CErrors.errorlabstrm "Safe_typing.import" + (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true @@ -900,7 +903,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - Errors.error "Register inline: an evaluable constant is expected"; + CErrors.error "Register inline: an evaluable constant is expected"; let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5efc1078ee..c8ceb064d5 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -110,7 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 in let u = if poly then - Errors.error ("Checking of subtyping of polymorphic" ^ + CErrors.error ("Checking of subtyping of polymorphic" ^ " inductive types not implemented") else Instance.empty in @@ -347,7 +347,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = Mod_subst.force_constr lc2 in check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -364,7 +364,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 4416770fe4..15f187e5c4 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -8,7 +8,7 @@ open Util open Pp -open Errors +open CErrors open Names open Vars diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index be84cae6da..749b5dbafa 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -12,7 +12,7 @@ (* This module provides the main entry points for type-checking basic declarations *) -open Errors +open CErrors open Util open Names open Term diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0ea68e2bcc..0059111c09 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Univ @@ -37,7 +37,7 @@ let check_constraints cst env = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env j = - match kind_of_term(whd_betadeltaiota env j.uj_type) with + match kind_of_term(whd_all env j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -137,7 +137,7 @@ let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with | Sort (Type u) -> - let ind, l = decompose_app (whd_betadeltaiota env c) in + let ind, l = decompose_app (whd_all env c) in if isInd ind && List.is_empty l then let mis = lookup_mind_specif env (fst (destInd ind)) in let nparams = Inductive.inductive_params mis in @@ -233,7 +233,7 @@ let judge_of_apply env funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> (try let () = conv_leq false env hj.uj_type c1 in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00883ddd84..e2712615be 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Util open Univ @@ -132,7 +131,7 @@ let change_node g n = let rec repr g u = let a = try UMap.find u g.entries - with Not_found -> anomaly ~label:"Univ.repr" + with Not_found -> CErrors.anomaly ~label:"Univ.repr" (str"Universe " ++ Level.pr u ++ str" undefined") in match a with diff --git a/kernel/univ.ml b/kernel/univ.ml index 126f95f1f1..9224ec48d7 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -16,7 +16,7 @@ Sozeau, Pierre-Marie Pédrot *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. diff --git a/kernel/vars.ml b/kernel/vars.ml index b935ab6b91..2ca749d505 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -173,7 +173,7 @@ let subst_of_rel_context_instance sign l = | LocalDef (_,c,_)::sign', args' -> aux (substl subst c :: subst) sign' args' | [], [] -> subst - | _ -> Errors.anomaly (Pp.str "Instance and signature do not match") + | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l let adjust_subst_to_rel_context sign l = diff --git a/kernel/vconv.ml b/kernel/vconv.ml index c729a6ce29..894f5296a8 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -116,14 +116,14 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = | Atype _ , _ | _, Atype _ -> assert false | Aind _, _ | Aid _, _ -> raise NotConvertible -and conv_stack env ?from:(from=0) k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in diff --git a/kernel/vm.ml b/kernel/vm.ml index 7029876438..eb992ef892 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -232,7 +232,7 @@ let uni_lvl_val (v : values) : Univ.universe_level = | Vatom_stk (a,stk) -> str "Vatom_stk" | _ -> assert false in - Errors.anomaly + CErrors.anomaly Pp.( strbrk "Parsing virtual machine value expected universe level, got " ++ pr) @@ -282,7 +282,7 @@ let rec whd_accu a stk = | _ -> assert false end | tg -> - Errors.anomaly + CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg) external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" @@ -306,7 +306,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else Vconstr_block(Obj.obj o) |