diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/constr.ml | 33 | ||||
-rw-r--r-- | kernel/constr.mli | 2 | ||||
-rw-r--r-- | kernel/names.ml | 2 | ||||
-rw-r--r-- | kernel/nativecode.ml | 14 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 90 | ||||
-rw-r--r-- | kernel/nativevalues.ml | 3 | ||||
-rw-r--r-- | kernel/reduction.ml | 4 | ||||
-rw-r--r-- | kernel/subtyping.ml | 2 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/term.mli | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 4 | ||||
-rw-r--r-- | kernel/uGraph.ml | 16 | ||||
-rw-r--r-- | kernel/uGraph.mli | 3 | ||||
-rw-r--r-- | kernel/univ.ml | 4 | ||||
-rw-r--r-- | kernel/vars.ml | 2 | ||||
-rw-r--r-- | kernel/vars.mli | 4 |
17 files changed, 37 insertions, 152 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 5a7561bf5..eecceb32a 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -107,7 +107,16 @@ type constr = t type existential = existential_key * constr array type rec_declaration = Name.t array * constr array * constr array type fixpoint = (int array * int) * rec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) type cofixpoint = int * rec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) type types = constr @@ -115,7 +124,7 @@ type types = constr (* Term constructors *) (*********************) -(* Constructs a DeBrujin index with number n *) +(* Constructs a de Bruijn index with number n *) let rels = [|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8; Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|] @@ -978,28 +987,6 @@ module Hcaseinfo = Hashcons.Make(CaseinfoHash) let case_info_hash = CaseinfoHash.hash -module Hsorts = - Hashcons.Make( - struct - open Sorts - - type t = Sorts.t - type u = universe -> universe - let hashcons huniv = function - Prop c -> Prop c - | Type u -> Type (huniv u) - let eq s1 s2 = - s1 == s2 || - match (s1,s2) with - (Prop c1, Prop c2) -> c1 == c2 - | (Type u1, Type u2) -> u1 == u2 - |_ -> false - let hash = function - | Prop Null -> 0 | Prop Pos -> 1 - | Type u -> 2 + Universe.hash u - end) - -(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *) let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate Hcaseinfo.hcons hcons_ind let hcons = diff --git a/kernel/constr.mli b/kernel/constr.mli index 700c235e6..e0954160f 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -70,7 +70,7 @@ type types = constr (** {6 Term constructors. } *) -(** Constructs a DeBrujin index (DB indices begin at 1) *) +(** Constructs a de Bruijn index (DB indices begin at 1) *) val mkRel : int -> constr (** Constructs a Variable *) diff --git a/kernel/names.ml b/kernel/names.ml index 5c10badbe..811b4a62a 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -542,7 +542,6 @@ module KerPair = struct end module SyntacticOrd = struct - type t = kernel_pair let compare x y = match x, y with | Same knx, Same kny -> KerName.compare knx kny | Dual (knux,kncx), Dual (knuy,kncy) -> @@ -865,7 +864,6 @@ struct let hash (c, b) = (if b then 0 else 1) + Constant.hash c module SyntacticOrd = struct - type t = constant * bool let compare (c, b) (c', b') = if b = b' then Constant.SyntacticOrd.compare c c' else -1 let equal (c, b as x) (c', b' as x') = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d9659d681..5130aa9a4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -16,6 +16,8 @@ open Nativeinstr open Nativelambda open Pre_env +[@@@ocaml.warning "-32-37"] + (** This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) @@ -40,8 +42,6 @@ module LNset = Set.Make(LNord) let lname_ctr = ref (-1) -let reset_lname = lname_ctr := -1 - let fresh_lname n = incr lname_ctr; { lname = n; luid = !lname_ctr } @@ -110,40 +110,30 @@ let gname_hash gn = match gn with let case_ctr = ref (-1) -let reset_gcase () = case_ctr := -1 - let fresh_gcase l = incr case_ctr; Gcase (l,!case_ctr) let pred_ctr = ref (-1) -let reset_gpred () = pred_ctr := -1 - let fresh_gpred l = incr pred_ctr; Gpred (l,!pred_ctr) let fixtype_ctr = ref (-1) -let reset_gfixtype () = fixtype_ctr := -1 - let fresh_gfixtype l = incr fixtype_ctr; Gfixtype (l,!fixtype_ctr) let norm_ctr = ref (-1) -let reset_norm () = norm_ctr := -1 - let fresh_gnorm l = incr norm_ctr; Gnorm (l,!norm_ctr) let normtbl_ctr = ref (-1) -let reset_normtbl () = normtbl_ctr := -1 - let fresh_gnormtbl l = incr normtbl_ctr; Gnormtbl (l,!normtbl_ctr) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3c0afe380..3593d94c2 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -141,7 +141,7 @@ let native_conv_gen pb sigma env univs t1 t2 = let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Feedback.msg_debug (Pp.str time_info); - (* TODO change 0 when we can have deBruijn *) + (* TODO change 0 when we can have de Bruijn *) fst (conv_val env pb 0 !rt1 !rt2 univs) end | _ -> anomaly (Pp.str "Compilation failure") diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 366f9a0a6..72d9c4851 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -16,7 +16,6 @@ open Nativeinstr module RelDecl = Context.Rel.Declaration -(** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -161,10 +160,6 @@ let rec lam_exsubst subst lam = | Lrel(id,i) -> lam_subst_rel lam id i subst | _ -> map_lam_with_binders liftn lam_exsubst subst lam -let lam_subst subst lam = - if is_subs_id subst then lam - else lam_exsubst subst lam - let lam_subst_args subst args = if is_subs_id subst then args else Array.smartmap (lam_exsubst subst) args @@ -278,71 +273,6 @@ and reduce_lapp substf lids body substa largs = Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) | [], _::_ -> simplify_app substf body substa (Array.of_list largs) - -(* [occurrence kind k lam]: - If [kind] is [true] return [true] if the variable [k] does not appear in - [lam], return [false] if the variable appear one time and not - under a lambda, a fixpoint, a cofixpoint; else raise Not_found. - If [kind] is [false] return [false] if the variable does not appear in [lam] - else raise [Not_found] -*) - -let rec occurrence k kind lam = - match lam with - | Lrel (_,n) -> - if Int.equal n k then - if kind then false else raise Not_found - else kind - | Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind - | Lprod(dom, codom) -> - occurrence k (occurrence k kind dom) codom - | Llam(ids,body) -> - let _ = occurrence (k+Array.length ids) false body in kind - | Llet(_,def,body) -> - occurrence (k+1) (occurrence k kind def) body - | Lapp(f, args) -> - occurrence_args k (occurrence k kind f) args - | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) -> - occurrence_args k kind args - | Lcase(_,t,a,br) -> - let kind = occurrence k (occurrence k kind t) a in - let r = ref kind in - Array.iter (fun (_,ids,c) -> - r := occurrence (k+Array.length ids) kind c && !r) br; - !r - | Lif (t, bt, bf) -> - let kind = occurrence k kind t in - kind && occurrence k kind bt && occurrence k kind bf - | Lfix(_,(ids,ltypes,lbodies)) - | Lcofix(_,(ids,ltypes,lbodies)) -> - let kind = occurrence_args k kind ltypes in - let _ = occurrence_args (k+Array.length ids) false lbodies in - kind - -and occurrence_args k kind args = - Array.fold_left (occurrence k) kind args - -let occur_once lam = - try let _ = occurrence 1 true lam in true - with Not_found -> false - -(* [remove_let lam] remove let expression in [lam] if the variable is *) -(* used at most once time in the body, and does not appear under *) -(* a lambda or a fix or a cofix *) - -let rec remove_let subst lam = - match lam with - | Lrel(id,i) -> lam_subst_rel lam id i subst - | Llet(id,def,body) -> - let def' = remove_let subst def in - if occur_once body then remove_let (cons def' subst) body - else - let body' = remove_let (lift subst) body in - if def == def' && body == body' then lam else Llet(id,def',body') - | _ -> map_lam_with_binders liftn remove_let subst lam - - (*s Translation from [constr] to [lambda] *) (* Translation of constructor *) @@ -407,8 +337,6 @@ module Vect = size = 0; } - let length v = v.size - let extend v = if Int.equal v.size (Array.length v.elems) then let new_size = min (2*v.size) Sys.max_array_length in @@ -422,33 +350,15 @@ module Vect = v.elems.(v.size) <- a; v.size <- v.size + 1 - let push_pos v a = - let pos = v.size in - push v a; - pos - let popn v n = v.size <- max 0 (v.size - n) let pop v = popn v 1 - let get v n = - if v.size <= n then invalid_arg "Vect.get:index out of bounds"; - v.elems.(n) - let get_last v n = if v.size <= n then invalid_arg "Vect.get:index out of bounds"; v.elems.(v.size - n - 1) - - let last v = - if Int.equal v.size 0 then invalid_arg "Vect.last:index out of bounds"; - v.elems.(v.size - 1) - - let clear v = v.size <- 0 - - let to_array v = Array.sub v.elems 0 v.size - end let empty_args = [||] diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 965ed67b0..8d5f6388c 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -334,6 +334,7 @@ let l_or accu x y = if is_int x && is_int y then no_check_l_or x y else accu x y +[@@@ocaml.warning "-37"] type coq_carry = | Caccu of t | C0 of t @@ -430,7 +431,7 @@ let addmuldiv accu x y z = if is_int x && is_int y && is_int z then no_check_addmuldiv x y z else accu x y z - +[@@@ocaml.warning "-34"] type coq_bool = | Baccu of t | Btrue diff --git a/kernel/reduction.ml b/kernel/reduction.ml index cd975ee9a..ba714ada2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -487,14 +487,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FInd (ind1,u1), FInd (ind2,u2)) -> if eq_ind ind1 ind2 then - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in 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 - (let cuniv = convert_instances false u1 u2 cuniv in + (let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) else raise NotConvertible diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c8ceb064d..d0fdf9fda 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -117,7 +117,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = - (* Due to sort-polymorphism in inductive types, the conclusions of + (* Due to template polymorphism, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds of the types of the constructors. diff --git a/kernel/term.ml b/kernel/term.ml index e5a681375..03562d9f3 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -169,7 +169,7 @@ let hcons_types = Constr.hcons exception DestKO -(* Destructs a DeBrujin index *) +(* Destructs a de Bruijn index *) let destRel c = match kind_of_term c with | Rel n -> n | _ -> raise DestKO diff --git a/kernel/term.mli b/kernel/term.mli index a9bb67705..241ef322f 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -127,7 +127,7 @@ val is_small : sorts -> bool exception DestKO -(** Destructs a DeBrujin index *) +(** Destructs a de Bruijn index *) val destRel : constr -> int (** Destructs an existential variable *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7d9a2aac0..dbc0dcb73 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -367,15 +367,13 @@ let rec execute env cstr = let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) let args = Array.map (fun t -> lazy t) argst in type_of_constant_knowing_parameters env cst args | _ -> - (* Full or no sort-polymorphism *) + (* No template polymorphism *) execute env f in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4884d0deb..6971c0a2b 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -354,13 +354,15 @@ let get_new_edges g to_merge = UMap.empty to_merge in let ltle = - UMap.fold (fun _ n acc -> - UMap.merge (fun _ strict1 strict2 -> - match strict1, strict2 with - | Some true, _ | _, Some true -> Some true - | _, _ -> Some false) - acc n.ltle) - to_merge_lvl UMap.empty + let fold _ n acc = + let fold u strict acc = + if strict then UMap.add u strict acc + else if UMap.mem u acc then acc + else UMap.add u false acc + in + UMap.fold fold n.ltle acc + in + UMap.fold fold to_merge_lvl UMap.empty in let ltle, _ = clean_ltle g ltle in let ltle = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index ed52832fa..935a3cab4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -62,3 +62,6 @@ val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds val dump_universes : (constraint_type -> string -> string -> unit) -> universes -> unit + +(** {6 Debugging} *) +val check_universes_invariants : universes -> unit diff --git a/kernel/univ.ml b/kernel/univ.ml index 09f884ecd..afe9cbe8d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -440,10 +440,6 @@ struct let set = make Level.set let type1 = hcons (Level.set, 1) - let is_prop = function - | (l,0) -> Level.is_prop l - | _ -> false - let is_small = function | (l,0) -> Level.is_small l | _ -> false diff --git a/kernel/vars.ml b/kernel/vars.ml index 4affb5f9f..f1c0a4f08 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -27,7 +27,7 @@ let closedn n c = in try closed_rec n c; true with LocalOccur -> false -(* [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *) let closed0 c = closedn 0 c diff --git a/kernel/vars.mli b/kernel/vars.mli index adeac422e..df5c55118 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -11,10 +11,10 @@ open Constr (** {6 Occur checks } *) -(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *) +(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *) val closedn : int -> constr -> bool -(** [closed0 M] is true iff [M] is a (deBruijn) closed term *) +(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *) val closed0 : constr -> bool (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *) |