diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/.merlin.in | 8 | ||||
| -rw-r--r-- | kernel/cClosure.ml | 55 | ||||
| -rw-r--r-- | kernel/constr.ml | 24 | ||||
| -rw-r--r-- | kernel/constr.mli | 53 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 18 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
7 files changed, 68 insertions, 94 deletions
diff --git a/kernel/.merlin.in b/kernel/.merlin.in new file mode 100644 index 0000000000..912ff61496 --- /dev/null +++ b/kernel/.merlin.in @@ -0,0 +1,8 @@ +FLG -rectypes -thread -safe-string -w +a-4-44-50 + +S ../clib +B ../clib +S ../config +B ../config +S ../lib +B ../lib diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c4c96c9b55..003b49535f 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -551,45 +551,7 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v -(* Translate the head constructor of t from constr to fconstr. This - function is parameterized by the function to apply on the direct - subterms. - Could be used insted of mk_clos. *) -let mk_clos_deep clos_fun env t = - match kind t with - | (Rel _|Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> - mk_clos env t - | Cast (a,k,b) -> - { norm = Red; - term = FCast (clos_fun env a, k, clos_fun env b)} - | App (f,v) -> - { norm = Red; - term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) } - | Proj (p,c) -> - { norm = Red; - term = FProj (p, clos_fun env c) } - | Case (ci,p,c,v) -> - { norm = Red; - term = FCaseT (ci, p, clos_fun env c, v, env) } - | Fix fx -> - { norm = Cstr; term = FFix (fx, env) } - | CoFix cfx -> - { norm = Cstr; term = FCoFix(cfx,env) } - | Lambda _ -> - { norm = Cstr; term = mk_lambda env t } - | Prod (n,t,c) -> - { norm = Whnf; - term = FProd (n, clos_fun env t, clos_fun (subs_lift env) c) } - | LetIn (n,b,t,c) -> - { norm = Red; - term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) } - | Evar ev -> - { norm = Red; term = FEvar(ev,env) } - -(* A better mk_clos? *) -let mk_clos2 = mk_clos_deep mk_clos - -(* The inverse of mk_clos_deep: move back to constr *) +(* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with | FRel i -> mkRel (reloc_rel i lfts) @@ -922,13 +884,18 @@ and knht info e t stk = knht info e a (append_stack (mk_clos_vect e b) stk) | Case(ci,p,t,br) -> knht info e t (ZcaseT(ci, p, br, e)::stk) - | Fix _ -> knh info (mk_clos2 e t) stk + | Fix fx -> knh info { norm = Cstr; term = FFix (fx, e) } stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (_p,_c) -> knh info (mk_clos2 e t) stk - | (Lambda _|Prod _|Construct _|CoFix _|Ind _| - LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> - (mk_clos2 e t, stk) + | Proj (p, c) -> knh info { norm = Red; term = FProj (p, mk_clos e c) } stk + | (Ind _|Const _|Construct _|Var _|Meta _ | Sort _) -> (mk_clos e t, stk) + | CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk + | Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk + | Prod (n, t, c) -> + { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk + | LetIn (n,b,t,c) -> + { norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk + | Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk (************************************************************************) diff --git a/kernel/constr.ml b/kernel/constr.ml index b25f38d630..c97969c0e0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -237,6 +237,17 @@ let mkVar id = Var id let kind c = c +let rec kind_nocast_gen kind c = + match kind c with + | Cast (c, _, _) -> kind_nocast_gen kind c + | App (h, outer) as k -> + (match kind_nocast_gen kind h with + | App (h, inner) -> App (h, Array.append inner outer) + | _ -> k) + | k -> k + +let kind_nocast c = kind_nocast_gen kind c + (* The other way around. We treat specifically smart constructors *) let of_kind = function | App (f, a) -> mkApp (f, a) @@ -755,10 +766,10 @@ let map_with_binders g f l c0 = match kind c0 with let bl' = Array.Fun1.Smart.map f l' bl in mkCoFix (ln,(lna,tl',bl')) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and [c2] (using [k1] to expose the structure of [c1] and [k2] to expose @@ -772,19 +783,16 @@ type constr_compare_fn = int -> constr -> constr -> bool calls to {!Array.equal_norefl}). *) let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t1 t2 = - match kind1 t1, kind2 t2 with + match kind_nocast_gen kind1 t1, kind_nocast_gen kind2 t2 with + | Cast _, _ | _, Cast _ -> assert false (* kind_nocast *) | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 | Sort s1, Sort s2 -> leq_sorts s1 s2 - | Cast (c1, _, _), _ -> leq nargs c1 t2 - | _, Cast (c2, _, _) -> leq nargs t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> eq 0 t1 t2 && leq 0 c1 c2 | Lambda (_,t1,c1), Lambda (_,t2,c2) -> eq 0 t1 t2 && eq 0 c1 c2 | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> eq 0 b1 b2 && eq 0 t1 t2 && leq nargs c1 c2 (* Why do we suddenly make a special case for Cast here? *) - | App (Cast (c1, _, _), l1), _ -> leq nargs (mkApp (c1, l1)) t2 - | _, App (Cast (c2, _, _), l2) -> leq nargs t1 (mkApp (c2, l2)) | App (c1, l1), App (c2, l2) -> let len = Array.length l1 in Int.equal len (Array.length l2) && diff --git a/kernel/constr.mli b/kernel/constr.mli index ea38dabd5c..2efdae007c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -241,6 +241,11 @@ 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 +val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) + +val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + (** {6 Simple case analysis} *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -518,50 +523,50 @@ val iter_with_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -type constr_compare_fn = int -> constr -> constr -> bool +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : constr_compare_fn -> constr_compare_fn +val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = GlobRef.t -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> 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, [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen : instance_compare_fn -> +val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn val compare_head_gen_leq_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [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 @@ -570,11 +575,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : instance_compare_fn -> +val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn -> + constr constr_compare_fn (** {6 Hashconsing} *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index b4126dd68c..d294f2060e 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -11,7 +11,6 @@ open Util open Nativevalues open Nativecode open CErrors -open Envars (** This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler. *) @@ -37,7 +36,7 @@ let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) let include_dirs () = - [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] + [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun _x -> () : string -> unit) @@ -89,16 +88,7 @@ let call_compiler ?profile:(profile=false) ml_filename = else [] in - let flambda_args = - 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. - *) - ["-Oclassic"] - else - [] - in + let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in let args = initial_args @ profile_args @ @@ -108,9 +98,9 @@ let call_compiler ?profile:(profile=false) ml_filename = ::"-w"::"a" ::include_dirs) @ ["-impl"; ml_filename] in - if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args))); + if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); try - let res = CUnix.sys_command (ocamlfind ()) args in + let res = CUnix.sys_command (Envars.ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9d302c69fb..b036aa6a67 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -273,7 +273,6 @@ let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst let push_context_set poly ctx = add_constraints (Now (poly,ctx)) -let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx)) let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 08b97b718e..6e0febaa3f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -128,9 +128,6 @@ val add_modtype : val push_context_set : bool -> Univ.ContextSet.t -> safe_transformer0 -val push_context : - bool -> Univ.UContext.t -> safe_transformer0 - val add_constraints : Univ.Constraint.t -> safe_transformer0 |