diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cbytegen.ml | 20 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/section.ml | 74 |
3 files changed, 49 insertions, 47 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b3a4bd7471..59ae8c0745 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -130,7 +130,7 @@ type comp_env = { nb_uni_stack : int ; (* number of universes on the stack, *) (* universes are always at the bottom. *) nb_stack : int; (* number of variables on the stack *) - in_stack : int list; (* position in the stack *) + in_stack : int Range.t; (* position in the stack *) nb_rec : int; (* number of mutually recursive functions *) pos_rec : instruction list; (* instruction d'acces pour les variables *) (* de point fix ou de cofix *) @@ -158,7 +158,7 @@ let empty_comp_env ()= { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 0; @@ -188,13 +188,13 @@ let ensure_stack_capacity f x = (*i Creation functions for comp_env *) let rec add_param n sz l = - if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l) + if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l) let comp_env_fun ?(univs=0) arity = { arity; nb_uni_stack = univs ; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = 0; pos_rec = []; offset = 1; @@ -206,7 +206,7 @@ let comp_env_fix_type rfv = { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 1; @@ -221,7 +221,7 @@ let comp_env_fix ndef curr_pos arity rfv = { arity; nb_uni_stack = 0; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = ndef; pos_rec = !prec; offset = 2 * (ndef - curr_pos - 1)+1; @@ -232,7 +232,7 @@ let comp_env_cofix_type ndef rfv = { arity = 0; nb_uni_stack = 0; nb_stack = 0; - in_stack = []; + in_stack = Range.empty; nb_rec = 0; pos_rec = []; offset = 1+ndef; @@ -247,7 +247,7 @@ let comp_env_cofix ndef arity rfv = { arity; nb_uni_stack = 0; nb_stack = arity; - in_stack = add_param arity 0 []; + in_stack = add_param arity 0 Range.empty; nb_rec = ndef; pos_rec = !prec; offset = ndef+1; @@ -264,7 +264,7 @@ let push_param n sz r = let push_local sz r = { r with nb_stack = r.nb_stack + 1; - in_stack = (sz + 1) :: r.in_stack } + in_stack = Range.cons (sz + 1) r.in_stack } (*i Compilation of variables *) let find_at fv env = FvMap.find fv env.fv_fwd @@ -280,7 +280,7 @@ let pos_named id r = let pos_rel i r sz = if i <= r.nb_stack then - Kacc(sz - (List.nth r.in_stack (i-1))) + Kacc(sz - (Range.get r.in_stack (i-1))) else let i = i - r.nb_stack in if i <= r.nb_rec then diff --git a/kernel/environ.mli b/kernel/environ.mli index 79e632daa0..f489b13a3b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -176,6 +176,8 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a +val match_named_context_val : named_context_val -> (named_declaration * lazy_val * named_context_val) option + (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a diff --git a/kernel/section.ml b/kernel/section.ml index 8c36f16799..c285b31b70 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -21,31 +21,31 @@ type section_entry = type 'a entry_map = 'a Cmap.t * 'a Mindmap.t type 'a t = { - sec_prev : 'a t option; + prev : 'a t option; (** Section surrounding the current one *) - sec_context : int; + context : int; (** Length of the named context suffix that has been introduced locally *) - sec_mono_universes : ContextSet.t; - sec_poly_universes : Name.t array * UContext.t; + mono_universes : ContextSet.t; + poly_universes : Name.t array * UContext.t; (** Universes local to the section *) all_poly_univs : Univ.Level.t array; (** All polymorphic universes, including from previous sections. *) has_poly_univs : bool; (** Are there polymorphic universes or constraints, including in previous sections. *) - sec_entries : section_entry list; + entries : section_entry list; (** Definitions introduced in the section *) - sec_data : (Instance.t * AUContext.t) entry_map; + data : (Instance.t * AUContext.t) entry_map; (** Additional data synchronized with the section *) - sec_custom : 'a; + custom : 'a; } -let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth prev +let rec depth sec = 1 + match sec.prev with None -> 0 | Some prev -> depth prev let has_poly_univs sec = sec.has_poly_univs let all_poly_univs sec = sec.all_poly_univs -let map_custom f sec = {sec with sec_custom = f sec.sec_custom} +let map_custom f sec = {sec with custom = f sec.custom} let find_emap e (cmap, imap) = match e with | SecDefinition con -> Cmap.find con cmap @@ -56,22 +56,22 @@ let add_emap e v (cmap, imap) = match e with | SecInductive ind -> (cmap, Mindmap.add ind v imap) let push_local sec = - { sec with sec_context = sec.sec_context + 1 } + { sec with context = sec.context + 1 } let push_context (nas, ctx) sec = if UContext.is_empty ctx then sec else - let (snas, sctx) = sec.sec_poly_universes in - let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in + let (snas, sctx) = sec.poly_universes in + let poly_universes = (Array.append snas nas, UContext.union sctx ctx) in let all_poly_univs = Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx) in - { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true } + { sec with poly_universes; all_poly_univs; has_poly_univs = true } let rec is_polymorphic_univ u sec = - let (_, uctx) = sec.sec_poly_universes in + let (_, uctx) = sec.poly_universes in let here = Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in - here || Option.cata (is_polymorphic_univ u) false sec.sec_prev + here || Option.cata (is_polymorphic_univ u) false sec.prev let push_constraints uctx sec = if sec.has_poly_univs && @@ -80,25 +80,25 @@ let push_constraints uctx sec = (snd uctx) then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes."); - let uctx' = sec.sec_mono_universes in - let sec_mono_universes = (ContextSet.union uctx uctx') in - { sec with sec_mono_universes } + let uctx' = sec.mono_universes in + let mono_universes = (ContextSet.union uctx uctx') in + { sec with mono_universes } -let open_section ~custom sec_prev = +let open_section ~custom prev = { - sec_prev; - sec_context = 0; - sec_mono_universes = ContextSet.empty; - sec_poly_universes = ([||], UContext.empty); - all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev; - has_poly_univs = Option.cata has_poly_univs false sec_prev; - sec_entries = []; - sec_data = (Cmap.empty, Mindmap.empty); - sec_custom = custom; + prev; + context = 0; + mono_universes = ContextSet.empty; + poly_universes = ([||], UContext.empty); + all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] prev; + has_poly_univs = Option.cata has_poly_univs false prev; + entries = []; + data = (Cmap.empty, Mindmap.empty); + custom = custom; } let close_section sec = - sec.sec_prev, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom + sec.prev, sec.entries, sec.mono_universes, sec.custom let make_decl_univs (nas,uctx) = abstract_universes nas uctx @@ -109,8 +109,8 @@ let push_global ~poly e sec = section polymorphic universes are present.") else { sec with - sec_entries = e :: sec.sec_entries; - sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data; + entries = e :: sec.entries; + data = add_emap e (make_decl_univs sec.poly_universes) sec.data; } let push_constant ~poly con s = push_global ~poly (SecDefinition con) s @@ -131,7 +131,7 @@ let empty_segment = { let extract_hyps sec vars used = (* Keep the section-local segment of variables *) - let vars = List.firstn sec.sec_context vars in + let vars = List.firstn sec.context vars in (* Only keep the part that is used by the declaration *) List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars @@ -139,7 +139,7 @@ let section_segment_of_entry vars e hyps sec = (* [vars] are the named hypotheses, [hyps] the subset that is declared by the global *) let hyps = extract_hyps sec vars hyps in - let inst, auctx = find_emap e sec.sec_data in + let inst, auctx = find_emap e sec.data in { abstr_ctx = hyps; abstr_subst = inst; @@ -166,7 +166,7 @@ let extract_worklist info = info.abstr_subst, args let replacement_context env sec = - let cmap, imap = sec.sec_data in + let cmap, imap = sec.data in let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con sec) cmap in let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind sec) imap in (cmap, imap) @@ -175,9 +175,9 @@ let is_in_section env gr sec = let open GlobRef in match gr with | VarRef id -> - let vars = List.firstn sec.sec_context (Environ.named_context env) in + let vars = List.firstn sec.context (Environ.named_context env) in List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars | ConstRef con -> - Cmap.mem con (fst sec.sec_data) + Cmap.mem con (fst sec.data) | IndRef (ind, _) | ConstructRef ((ind, _), _) -> - Mindmap.mem ind (snd sec.sec_data) + Mindmap.mem ind (snd sec.data) |