aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml111
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/cbytegen.ml168
-rw-r--r--kernel/constr.ml16
-rw-r--r--kernel/constr.mli30
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/cooking.mli1
-rw-r--r--kernel/declarations.ml3
-rw-r--r--kernel/declareops.ml3
-rw-r--r--kernel/entries.ml5
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/esubst.ml23
-rw-r--r--kernel/esubst.mli7
-rw-r--r--kernel/indtypes.ml57
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/mod_subst.ml11
-rw-r--r--kernel/mod_subst.mli2
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/names.ml17
-rw-r--r--kernel/names.mli6
-rw-r--r--kernel/term_typing.ml31
21 files changed, 242 insertions, 260 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 1d8861cbc..c9362bce6 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -587,78 +587,95 @@ let mk_clos_deep clos_fun env t =
let mk_clos2 = mk_clos_deep mk_clos
(* The inverse of mk_clos_deep: move back to constr *)
-let rec to_constr constr_fun lfts v =
+let rec to_constr lfts v =
match v.term with
| FRel i -> mkRel (reloc_rel i lfts)
| FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
| FFlex (VarKey x) -> mkVar x
| FAtom c -> exliftn lfts c
| FCast (a,k,b) ->
- mkCast (constr_fun lfts a, k, constr_fun lfts b)
+ mkCast (to_constr lfts a, k, to_constr lfts b)
| FFlex (ConstKey op) -> mkConstU op
| FInd op -> mkIndU op
| FConstruct op -> mkConstructU op
| FCaseT (ci,p,c,ve,env) ->
- mkCase (ci, constr_fun lfts (mk_clos env p),
- constr_fun lfts c,
- Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
- | FFix ((op,(lna,tys,bds)),e) ->
+ if is_subs_id env && is_lift_id lfts then
+ mkCase (ci, p, to_constr lfts c, ve)
+ else
+ let subs = comp_subs lfts env in
+ mkCase (ci, subst_constr subs p,
+ to_constr lfts c,
+ Array.map (fun b -> subst_constr subs b) ve)
+ | FFix ((op,(lna,tys,bds)) as fx, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkFix fx
+ else
let n = Array.length bds in
- let ftys = Array.Fun1.map mk_clos e tys in
- let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
- let lfts' = el_liftn n lfts in
- mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
- Array.Fun1.map constr_fun lfts' fbds))
- | FCoFix ((op,(lna,tys,bds)),e) ->
+ let subs_ty = comp_subs lfts e in
+ let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+ let tys = Array.Fun1.map subst_constr subs_ty tys in
+ let bds = Array.Fun1.map subst_constr subs_bd bds in
+ mkFix (op, (lna, tys, bds))
+ | FCoFix ((op,(lna,tys,bds)) as cfx, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkCoFix cfx
+ else
let n = Array.length bds in
- let ftys = Array.Fun1.map mk_clos e tys in
- let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
- let lfts' = el_liftn (Array.length bds) lfts in
- mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
- Array.Fun1.map constr_fun lfts' fbds))
+ let subs_ty = comp_subs lfts e in
+ let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+ let tys = Array.Fun1.map subst_constr subs_ty tys in
+ let bds = Array.Fun1.map subst_constr subs_bd bds in
+ mkCoFix (op, (lna, tys, bds))
| FApp (f,ve) ->
- mkApp (constr_fun lfts f,
- Array.Fun1.map constr_fun lfts ve)
+ mkApp (to_constr lfts f,
+ Array.Fun1.map to_constr lfts ve)
| FProj (p,c) ->
- mkProj (p,constr_fun lfts c)
+ mkProj (p,to_constr lfts c)
- | FLambda _ ->
- let (na,ty,bd) = destFLambda mk_clos2 v in
- mkLambda (na, constr_fun lfts ty,
- constr_fun (el_lift lfts) bd)
+ | FLambda (len, tys, f, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ Term.compose_lam (List.rev tys) f
+ else
+ let subs = comp_subs lfts e in
+ let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in
+ let f = subst_constr (subs_liftn len subs) f in
+ Term.compose_lam (List.rev tys) f
| FProd (n,t,c) ->
- mkProd (n, constr_fun lfts t,
- constr_fun (el_lift lfts) c)
+ mkProd (n, to_constr lfts t,
+ to_constr (el_lift lfts) c)
| FLetIn (n,b,t,f,e) ->
- let fc = mk_clos2 (subs_lift e) f in
- mkLetIn (n, constr_fun lfts b,
- constr_fun lfts t,
- constr_fun (el_lift lfts) fc)
+ let subs = comp_subs (el_lift lfts) (subs_lift e) in
+ mkLetIn (n, to_constr lfts b,
+ to_constr lfts t,
+ subst_constr subs f)
| FEvar ((ev,args),env) ->
- mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
- | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
+ let subs = comp_subs lfts env in
+ mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+ | FLIFT (k,a) -> to_constr (el_shft k lfts) a
| FCLOS (t,env) ->
- let fr = mk_clos2 env t in
- let unfv = update v fr.norm fr.term in
- to_constr constr_fun lfts unfv
+ if is_subs_id env && is_lift_id lfts then t
+ else
+ let subs = comp_subs lfts env in
+ subst_constr subs t
| FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
+and subst_constr subst c = match Constr.kind c with
+| Rel i ->
+ begin match expand_rel i subst with
+ | Inl (k, lazy v) -> Vars.lift k v
+ | Inr (m, _) -> mkRel m
+ end
+| _ ->
+ Constr.map_with_binders Esubst.subs_lift subst_constr subst c
+
+and comp_subs el s =
+ Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
+
(* This function defines the correspondance between constr and
fconstr. When we find a closure whose substitution is the identity,
then we directly return the constr to avoid possibly huge
reallocation. *)
-let term_of_fconstr =
- let rec term_of_fconstr_lift lfts v =
- 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 ->
- 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
- term_of_fconstr_lift el_id
-
-
+let term_of_fconstr c = to_constr el_id c
(* fstrong applies unfreeze_fun recursively on the (freeze) term and
* yields a term. Assumes that the unfreeze_fun never returns a
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 63daa4a7c..f8f98f0ab 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -244,6 +244,6 @@ val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
-val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val to_constr : lift -> fconstr -> constr
(** End of cbn debug section i*)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index df5b17da3..7a27a3d20 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -399,55 +399,55 @@ let code_makeblock ~stack_size ~arity ~tag cont =
Kpush :: nest_block tag arity cont
end
-let compile_structured_constant reloc sc sz cont =
+let compile_structured_constant cenv sc sz cont =
set_max_stack_size sz;
Kconst sc :: cont
(* compiling application *)
-let comp_args comp_expr reloc args sz cont =
+let comp_args comp_expr cenv args sz cont =
let nargs_m_1 = Array.length args - 1 in
- let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
+ let c = ref (comp_expr cenv args.(0) (sz + nargs_m_1) cont) in
for i = 1 to nargs_m_1 do
- c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
+ c := comp_expr cenv args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
done;
!c
-let comp_app comp_fun comp_arg reloc f args sz cont =
+let comp_app comp_fun comp_arg cenv f args sz cont =
let nargs = Array.length args in
- if Int.equal nargs 0 then comp_fun reloc f sz cont
+ if Int.equal nargs 0 then comp_fun cenv f sz cont
else
match is_tailcall cont with
| Some k ->
- comp_args comp_arg reloc args sz
+ comp_args comp_arg cenv args sz
(Kpush ::
- comp_fun reloc f (sz + nargs)
+ comp_fun cenv f (sz + nargs)
(Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
| None ->
if nargs < 4 then
- comp_args comp_arg reloc args sz
- (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont)))
+ comp_args comp_arg cenv args sz
+ (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
else
let lbl,cont1 = label_code cont in
Kpush_retaddr lbl ::
- (comp_args comp_arg reloc args (sz + 3)
- (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
+ (comp_args comp_arg cenv args (sz + 3)
+ (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1))))
(* Compiling free variables *)
-let compile_fv_elem reloc fv sz cont =
+let compile_fv_elem cenv fv sz cont =
match fv with
- | FVrel i -> pos_rel i reloc sz :: cont
- | FVnamed id -> pos_named id reloc :: cont
- | FVuniv_var i -> pos_universe_var i reloc sz :: cont
- | FVevar evk -> pos_evar evk reloc :: cont
+ | FVrel i -> pos_rel i cenv sz :: cont
+ | FVnamed id -> pos_named id cenv :: cont
+ | FVuniv_var i -> pos_universe_var i cenv sz :: cont
+ | FVevar evk -> pos_evar evk cenv :: cont
-let rec compile_fv reloc l sz cont =
+let rec compile_fv cenv l sz cont =
match l with
| [] -> cont
- | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont
+ | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem cenv fvn sz cont
| fvn :: tl ->
- compile_fv_elem reloc fvn sz
- (Kpush :: compile_fv reloc tl (sz + 1) cont)
+ compile_fv_elem cenv fvn sz
+ (Kpush :: compile_fv cenv tl (sz + 1) cont)
(* Compiling constants *)
@@ -472,58 +472,58 @@ let make_areconst n else_lbl cont =
Kareconst (n, else_lbl)::cont
(* sz is the size of the local stack *)
-let rec compile_lam env reloc lam sz cont =
+let rec compile_lam env cenv lam sz cont =
set_max_stack_size sz;
match lam with
- | Lrel(_, i) -> pos_rel i reloc sz :: cont
+ | Lrel(_, i) -> pos_rel i cenv sz :: cont
- | Lval v -> compile_structured_constant reloc v sz cont
+ | Lval v -> compile_structured_constant cenv v sz cont
| Lproj (n,kn,arg) ->
- compile_lam env reloc arg sz (Kproj (n,kn) :: cont)
+ compile_lam env cenv arg sz (Kproj (n,kn) :: cont)
- | Lvar id -> pos_named id reloc :: cont
+ | Lvar id -> pos_named id cenv :: cont
| Levar (evk, args) ->
if Array.is_empty args then
- compile_fv_elem reloc (FVevar evk) sz cont
+ compile_fv_elem cenv (FVevar evk) sz cont
else
- comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont
+ comp_app compile_fv_elem (compile_lam env) cenv (FVevar evk) args sz cont
- | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont
+ | Lconst (kn,u) -> compile_constant env cenv kn u [||] sz cont
| Lind (ind,u) ->
if Univ.Instance.is_empty u then
- compile_structured_constant reloc (Const_ind ind) sz cont
- else comp_app compile_structured_constant compile_universe reloc
+ compile_structured_constant cenv (Const_ind ind) sz cont
+ else comp_app compile_structured_constant compile_universe cenv
(Const_ind ind) (Univ.Instance.to_array u) sz cont
| Lsort (Sorts.Prop _ as s) ->
- compile_structured_constant reloc (Const_sort s) sz cont
+ compile_structured_constant cenv (Const_sort s) sz cont
| Lsort (Sorts.Type u) ->
(* We represent universes as a global constant with local universes
"compacted", i.e. as [u arg0 ... argn] where we will substitute (after
evaluation) [Var 0,...,Var n] with values of [arg0,...,argn] *)
let u,s = Univ.compact_univ u in
- let compile_get_univ reloc idx sz cont =
+ let compile_get_univ cenv idx sz cont =
set_max_stack_size sz;
- compile_fv_elem reloc (FVuniv_var idx) sz cont
+ compile_fv_elem cenv (FVuniv_var idx) sz cont
in
if List.is_empty s then
- compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont
+ compile_structured_constant cenv (Const_sort (Sorts.Type u)) sz cont
else
- comp_app compile_structured_constant compile_get_univ reloc
+ comp_app compile_structured_constant compile_get_univ cenv
(Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
| Llet (id,def,body) ->
- compile_lam env reloc def sz
+ compile_lam env cenv def sz
(Kpush ::
- compile_lam env (push_local sz reloc) body (sz+1) (add_pop 1 cont))
+ compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont))
| Lprod (dom,codom) ->
let cont1 =
- Kpush :: compile_lam env reloc dom (sz+1) (Kmakeprod :: cont) in
- compile_lam env reloc codom sz cont1
+ Kpush :: compile_lam env cenv dom (sz+1) (Kmakeprod :: cont) in
+ compile_lam env cenv codom sz cont1
| Llam (ids,body) ->
let arity = Array.length ids in
@@ -534,12 +534,12 @@ let rec compile_lam env reloc lam sz cont =
in
fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
let fv = fv r_fun in
- compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
+ compile_fv cenv fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
| Lapp (f, args) ->
begin match f with
- | Lconst (kn,u) -> compile_constant env reloc kn u args sz cont
- | _ -> comp_app (compile_lam env) (compile_lam env) reloc f args sz cont
+ | Lconst (kn,u) -> compile_constant env cenv kn u args sz cont
+ | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont
end
| Lfix ((rec_args, init), (decl, types, bodies)) ->
@@ -571,7 +571,7 @@ let rec compile_lam env reloc lam sz cont =
fun_code := [Ksequence(fcode,!fun_code)]
done;
let fv = !rfv in
- compile_fv reloc fv.fv_rev sz
+ compile_fv cenv fv.fv_rev sz
(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
@@ -607,7 +607,7 @@ let rec compile_lam env reloc lam sz cont =
done;
let fv = !rfv in
set_max_stack_size (sz + fv.size + ndef + 2);
- compile_fv reloc fv.fv_rev sz
+ compile_fv cenv fv.fv_rev sz
(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
@@ -625,7 +625,7 @@ let rec compile_lam env reloc lam sz cont =
let branch1, cont = make_branch cont in
(* Compilation of the return type *)
let fcode =
- ensure_stack_capacity (compile_lam env reloc t sz) [Kpop sz; Kstop]
+ ensure_stack_capacity (compile_lam env cenv t sz) [Kpop sz; Kstop]
in
let lbl_typ,fcode = label_code fcode in
fun_code := [Ksequence(fcode,!fun_code)];
@@ -653,7 +653,7 @@ let rec compile_lam env reloc lam sz cont =
(* Compilation of constant branches *)
for i = nconst - 1 downto 0 do
let aux =
- compile_lam env reloc branches.constant_branches.(i) sz_b (branch::!c)
+ compile_lam env cenv branches.constant_branches.(i) sz_b (branch::!c)
in
let lbl_b,code_b = label_code aux in
lbl_consts.(i) <- lbl_b;
@@ -665,7 +665,7 @@ let rec compile_lam env reloc lam sz cont =
let (ids, body) = branches.nonconstant_branches.(i) in
let arity = Array.length ids in
let code_b =
- compile_lam env (push_param arity sz_b reloc)
+ compile_lam env (push_param arity sz_b cenv)
body (sz_b+arity) (add_pop arity (branch::!c)) in
let code_b =
if tag < last_variant_tag then begin
@@ -703,25 +703,25 @@ let rec compile_lam env reloc lam sz cont =
| Kbranch lbl -> Kpush_retaddr lbl :: !c
| _ -> !c
in
- compile_lam env reloc a sz code_sw
+ compile_lam env cenv a sz code_sw
| Lmakeblock (tag,args) ->
let arity = Array.length args in
let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
- comp_args (compile_lam env) reloc args sz cont
+ comp_args (compile_lam env) cenv args sz cont
| Lprim (kn, ar, op, args) ->
- op_compilation env ar op kn reloc args sz cont
+ op_compilation env ar op kn cenv args sz cont
| Luint v ->
(match v with
- | UintVal i -> compile_structured_constant reloc (Const_b0 (Uint31.to_int i)) sz cont
+ | UintVal i -> compile_structured_constant cenv (Const_b0 (Uint31.to_int i)) sz cont
| UintDigits ds ->
let nargs = Array.length ds in
if Int.equal nargs 31 then
let (escape,labeled_cont) = make_branch cont in
let else_lbl = Label.create() in
- comp_args (compile_lam env) reloc ds sz
+ comp_args (compile_lam env) cenv ds sz
( Kisconst else_lbl::Kareconst(30,else_lbl)::Kcompint31::escape::Klabel else_lbl::Kmakeblock(31, 1)::labeled_cont)
else
let code_construct cont = (* spiwack: variant of the global code_construct
@@ -737,40 +737,40 @@ let rec compile_lam env reloc lam sz cont =
Kclosure(lbl,0) :: cont
in
comp_app (fun _ _ _ cont -> code_construct cont)
- (compile_lam env) reloc () ds sz cont
+ (compile_lam env) cenv () ds sz cont
| UintDecomp t ->
let escape_lbl, labeled_cont = label_code cont in
- compile_lam env reloc t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
+ compile_lam env cenv t sz ((Kisconst escape_lbl)::Kdecompint31::labeled_cont))
(* spiwack : compilation of constants with their arguments.
Makes a special treatment with 31-bit integer addition *)
-and compile_get_global reloc (kn,u) sz cont =
+and compile_get_global cenv (kn,u) sz cont =
set_max_stack_size sz;
if Univ.Instance.is_empty u then
Kgetglobal kn :: cont
else
comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
- compile_universe reloc () (Univ.Instance.to_array u) sz cont
+ compile_universe cenv () (Univ.Instance.to_array u) sz cont
-and compile_universe reloc uni sz cont =
+and compile_universe cenv uni sz cont =
set_max_stack_size sz;
match Univ.Level.var_index uni with
- | None -> compile_structured_constant reloc (Const_univ_level uni) sz cont
- | Some idx -> pos_universe_var idx reloc sz :: cont
+ | None -> compile_structured_constant cenv (Const_univ_level uni) sz cont
+ | Some idx -> pos_universe_var idx cenv sz :: cont
-and compile_constant env reloc kn u args sz cont =
+and compile_constant env cenv kn u args sz cont =
set_max_stack_size sz;
if Univ.Instance.is_empty u then
(* normal compilation *)
comp_app (fun _ _ sz cont ->
- compile_get_global reloc (kn,u) sz cont)
- (compile_lam env) reloc () args sz cont
+ compile_get_global cenv (kn,u) sz cont)
+ (compile_lam env) cenv () args sz cont
else
- let compile_arg reloc constr_or_uni sz cont =
+ let compile_arg cenv constr_or_uni sz cont =
match constr_or_uni with
- | ArgLambda t -> compile_lam env reloc t sz cont
- | ArgUniv uni -> compile_universe reloc uni sz cont
+ | ArgLambda t -> compile_lam env cenv t sz cont
+ | ArgUniv uni -> compile_universe cenv uni sz cont
in
let u = Univ.Instance.to_array u in
let lu = Array.length u in
@@ -779,7 +779,7 @@ and compile_constant env reloc kn u args sz cont =
(fun i -> if i < lu then ArgUniv u.(i) else ArgLambda args.(i-lu))
in
comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
- compile_arg reloc () all sz cont
+ compile_arg cenv () all sz cont
(*template for n-ary operation, invariant: n>=1,
the operations does the following :
@@ -788,34 +788,34 @@ and compile_constant env reloc kn u args sz cont =
3/ if at least one is not, branches to the normal behavior:
Kgetglobal (get_alias !global_env kn) *)
and op_compilation env n op =
- let code_construct reloc kn sz cont =
+ let code_construct cenv kn sz cont =
let f_cont =
let else_lbl = Label.create () in
Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
op:: Kreturn 0:: Klabel else_lbl::
(* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
- compile_get_global reloc kn sz (
+ compile_get_global cenv kn sz (
Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
in
let lbl = Label.create () in
fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
Kclosure(lbl, 0)::cont
in
- fun kn reloc args sz cont ->
+ fun kn cenv args sz cont ->
let nargs = Array.length args in
if Int.equal nargs n then (*if it is a fully applied addition*)
let (escape, labeled_cont) = make_branch cont in
let else_lbl = Label.create () in
assert (n < 4);
- comp_args (compile_lam env) reloc args sz
+ comp_args (compile_lam env) cenv args sz
(Kisconst else_lbl::(make_areconst (n-1) else_lbl
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs < 4 and non-tailcall cont*)
- compile_get_global reloc kn (sz+n) (Kapply n::labeled_cont))))
+ compile_get_global cenv kn (sz+n) (Kapply n::labeled_cont))))
else
- comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
- (compile_lam env) reloc () args sz cont
+ comp_app (fun cenv _ sz cont -> code_construct cenv kn sz cont)
+ (compile_lam env) cenv () args sz cont
let is_univ_copy max u =
@@ -846,11 +846,11 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
Label.reset_label_counter ();
let cont = [Kstop] in
try
- let reloc, init_code =
+ let cenv, init_code =
if Int.equal universes 0 then
let lam = lambda_of_constr ~optimize:true env c in
- let reloc = empty_comp_env () in
- reloc, ensure_stack_capacity (compile_lam env reloc lam 0) cont
+ let cenv = empty_comp_env () in
+ cenv, ensure_stack_capacity (compile_lam env cenv lam 0) cont
else
(* We are going to generate a lambda, but merge the universe closure
* with the function closure if it exists.
@@ -858,7 +858,7 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
let lam = lambda_of_constr ~optimize:true env c in
let params, body = decompose_Llam lam in
let arity = Array.length params in
- let reloc = empty_comp_env () in
+ let cenv = empty_comp_env () in
let full_arity = arity + universes in
let r_fun = comp_env_fun ~univs:universes arity in
let lbl_fun = Label.create () in
@@ -869,12 +869,12 @@ let compile ~fail_on_error ?universes:(universes=0) env c =
fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
let fv = fv r_fun in
let init_code =
- ensure_stack_capacity (compile_fv reloc fv.fv_rev 0)
+ ensure_stack_capacity (compile_fv cenv fv.fv_rev 0)
(Kclosure(lbl_fun,fv.size) :: cont)
in
- reloc, init_code
+ cenv, init_code
in
- let fv = List.rev (!(reloc.in_env).fv_rev) in
+ let fv = List.rev (!(cenv.in_env).fv_rev) in
(if !dump_bytecode then
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
@@ -922,13 +922,13 @@ let op2_compilation op =
fun_code := [Ksequence (add_grab 2 lbl f_cont, !fun_code)];
Kclosure(lbl, 0)::cont
in
- fun normal fc _ reloc args sz cont ->
+ fun normal fc _ cenv args sz cont ->
if not fc then raise Not_found else
let nargs = Array.length args in
if nargs=2 then (*if it is a fully applied addition*)
let (escape, labeled_cont) = make_branch cont in
let else_lbl = Label.create () in
- comp_args compile_constr reloc args sz
+ comp_args compile_constr cenv args sz
(Kisconst else_lbl::(make_areconst 1 else_lbl
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
@@ -940,5 +940,5 @@ let op2_compilation op =
code_construct normal cont
else
comp_app (fun _ _ _ cont -> code_construct normal cont)
- compile_constr reloc () args sz cont *)
+ compile_constr cenv () args sz cont *)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c11b9ebf4..418229330 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -107,21 +107,13 @@ type t = (t, t, Sorts.t, Instance.t) kind_of_term
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
+type rec_declaration = (constr, types) prec_declaration
+type fixpoint = (constr, types) pfixpoint
+type cofixpoint = (constr, types) pcofixpoint
+
(*********************)
(* Term constructors *)
(*********************)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 742a13919..bf7b5e87b 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -161,8 +161,26 @@ val mkCase : case_info * constr * constr * constr array -> constr
where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
-type rec_declaration = Name.t array * types array * constr array
-type fixpoint = (int array * int) * rec_declaration
+type ('constr, 'types) prec_declaration =
+ Name.t array * 'types array * 'constr array
+type ('constr, 'types) pfixpoint =
+ (int array * int) * ('constr, 'types) prec_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 ('constr, 'types) pcofixpoint =
+ int * ('constr, 'types) prec_declaration
+ (* The component [int] tells which component of the block of
+ cofixpoint is returned *)
+
+type rec_declaration = (constr, types) prec_declaration
+
+type fixpoint = (constr, types) pfixpoint
val mkFix : fixpoint -> constr
(** If [funnames = [|f1,.....fn|]]
@@ -176,7 +194,7 @@ val mkFix : fixpoint -> constr
...
with fn = bn.]
*)
-type cofixpoint = int * rec_declaration
+type cofixpoint = (constr, types) pcofixpoint
val mkCoFix : cofixpoint -> constr
@@ -185,12 +203,6 @@ 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 = Evar.t * 'constr array
-type ('constr, 'types) prec_declaration =
- Name.t array * 'types array * 'constr array
-type ('constr, 'types) pfixpoint =
- (int array * int) * ('constr, 'types) prec_declaration
-type ('constr, 'types) pcofixpoint =
- int * ('constr, 'types) prec_declaration
type ('constr, 'types, 'sort, 'univs) kind_of_term =
| Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 8a79bcf22..c7a84f617 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -155,7 +155,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
@@ -229,7 +228,6 @@ let cook_constant ~hcons env { from = cb; info } =
{
cook_body = body;
cook_type = typ;
- cook_proj = cb.const_proj;
cook_universes = univs;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0d907f3de..76c79335f 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,6 @@ type inline = bool
type result = {
cook_body : constant_def;
cook_type : types;
- cook_proj : bool;
cook_universes : constant_universes;
cook_inline : inline;
cook_context : Context.Named.t option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7bd70c050..7bd7d6c9c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -54,8 +54,6 @@ type projection_body = {
proj_npars : int;
proj_arg : int; (** Projection index, starting from 0 *)
proj_type : types; (* Type under params *)
- proj_eta : constr * types; (* Eta-expanded term and type *)
- proj_body : constr; (* For compatibility with VMs only, the match version *)
}
(* Global declarations (i.e. constants) can be either: *)
@@ -87,7 +85,6 @@ type constant_body = {
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
- const_proj : bool;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 75c0e5b4c..1b73096f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -86,7 +86,7 @@ let subst_const_def sub def = match def with
let subst_const_proj sub pb =
{ pb with proj_ind = subst_mind sub pb.proj_ind;
proj_type = subst_mps sub pb.proj_type;
- proj_body = subst_const_type sub pb.proj_body }
+ }
let subst_const_body sub cb =
assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -100,7 +100,6 @@ let subst_const_body sub cb =
{ const_hyps = [];
const_body = body';
const_type = type';
- const_proj = cb.const_proj;
const_body_code =
Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 94da00c7e..3c555f8c7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
Context.Named.t option * types in_constant_universes_entry * inline
-type projection_entry = {
- proj_entry_ind : MutInd.t;
- proj_entry_arg : int }
-
type 'a constant_entry =
| DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
- | ProjectionEntry of projection_entry
(** {6 Modules } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index fb89576dd..2d6c9117b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -490,7 +490,7 @@ let lookup_projection cst env =
Cmap_env.find (Projection.constant cst) env.env_globals.env_projections
let is_projection cst env =
- (lookup_constant cst env).const_proj
+ Cmap_env.mem cst env.env_globals.env_projections
(* Mutual Inductives *)
let polymorphic_ind (mind,i) env =
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 4b8edf63f..9fc3b11d7 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -134,6 +134,29 @@ let rec exp_rel lams k subs =
let expand_rel k subs = exp_rel 0 k subs
+let rec subs_map f = function
+| ESID _ as s -> s
+| CONS (x, s) -> CONS (Array.map f x, subs_map f s)
+| SHIFT (n, s) -> SHIFT (n, subs_map f s)
+| LIFT (n, s) -> LIFT (n, subs_map f s)
+
+let rec lift_subst mk_cl s1 s2 = match s1 with
+| ELID -> subs_map (fun c -> mk_cl ELID c) s2
+| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2)
+| ELLFT (k, s) ->
+ match s2 with
+ | CONS(x,s') ->
+ CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s')
+ | ESID n -> lift_subst mk_cl s (ESID (n + k))
+ | SHIFT(k',s') ->
+ if k<k'
+ then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s')))
+ else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s')
+ | LIFT(k',s') ->
+ if k<k'
+ then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s'))
+ else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s')
+
let rec comp mk_cl s1 s2 =
match (s1, s2) with
| _, ESID _ -> s1
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index a674c425a..475b64f47 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -72,3 +72,10 @@ val el_liftn : int -> lift -> lift
val el_lift : lift -> lift
val reloc_rel : int -> lift -> int
val is_lift_id : lift -> bool
+
+(** Lift applied to substitution: [lift_subst mk_clos el s] computes a
+ substitution equivalent to applying el then s. Argument
+ mk_clos is used when a closure has to be created, i.e. when
+ el is applied on an element of s.
+*)
+val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 439acd15b..14f2a3d8f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -797,16 +797,13 @@ exception UndefinableExpansion
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+let compute_projections ((kn, _ as ind), u) nparamargs params
mind_consnrealdecls mind_consnrealargs paramslet ctx =
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. *)
- let indty, paramsletsubst =
- (* [ty] = [Ind inst] is typed in context [params] *)
- let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
- let ty = mkApp (mkIndU indu, inst) in
+ let paramsletsubst =
(* [Ind inst] is typed in context [params-wo-let] *)
let inst' = rel_list 0 nparamargs in
(* {params-wo-let |- subst:params] *)
@@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
(* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *)
let subst = (* For the record parameter: *)
mkRel 1 :: List.map (lift 1) subst in
- ty, subst
+ subst
in
- let ci =
- let print_info =
- { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
- { ci_ind = ind;
- ci_npar = nparamargs;
- ci_cstr_ndecls = mind_consnrealdecls;
- ci_cstr_nargs = mind_consnrealargs;
- ci_pp_info = print_info }
- in
- let len = List.length ctx in
- let x = Name x in
- let compat_body ccl i =
- (* [ccl] is defined in context [params;x:indty] *)
- (* [ccl'] is defined in context [params;x:indty;x:indty] *)
- let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 indty, ccl') in
- let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
- let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
- in
- let projections decl (i, j, kns, pbs, subst, letsubst) =
+ let projections decl (i, j, kns, pbs, letsubst) =
match decl with
| LocalDef (na,c,t) ->
(* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
let c = liftn 1 j c in
(* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
- to [params, x:I |- c(params,proj1 x,..,projj x)] *)
- let c1 = substl subst c in
- (* From [params, x:I |- subst:field1,..,fieldj]
- to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
- is represented with instance of field1 last *)
- let subst = c1 :: subst in
- (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *)
let c2 = substl letsubst c in
(* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)]
to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *)
let letsubst = c2 :: letsubst in
- (i, j+1, kns, pbs, subst, letsubst)
+ (i, j+1, kns, pbs, letsubst)
| LocalAssum (na,t) ->
match na with
| Name id ->
@@ -868,21 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
let projty = substl letsubst t in
(* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
to [params, x:I |- t(proj1 x,..,projj x)] *)
- let ty = substl subst t in
- let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
- let compat = compat_body ty (j - 1) in
- let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
- let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
let body = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = projty; proj_eta = etab, etat;
- proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs,
- fterm :: subst, fterm :: letsubst)
+ proj_arg = i; proj_type = projty; } in
+ (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, subst, letsubst) =
- List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ let (_, _, kns, pbs, letsubst) =
+ List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
in
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
@@ -987,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
(try
let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
- compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt
+ compute_projections indsp nparamargs paramsctxt
pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
in Some (Some (rid, kns, projs))
with UndefinableExpansion -> Some None)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 5a38172c2..45228e35e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct
val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool
-val compute_projections : pinductive -> Id.t -> Id.t ->
+val compute_projections : pinductive ->
int -> Context.Rel.t -> int array -> int array ->
Context.Rel.t -> Context.Rel.t ->
(Constant.t array * projection_body array)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 0027ebecf..a47af56ca 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -24,7 +24,7 @@ open Constr
is the term into which we should inline. *)
type delta_hint =
- | Inline of int * constr option
+ | Inline of int * (Univ.AUContext.t * constr) option
| Equiv of KerName.t
(* NB: earlier constructor Prefix_equiv of ModPath.t
@@ -158,7 +158,7 @@ let find_prefix resolve mp =
(** Applying a resolver to a kernel name *)
-exception Change_equiv_to_inline of (int * constr)
+exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr))
let solve_delta_kn resolve kn =
try
@@ -300,9 +300,10 @@ let subst_con0 sub (cst,u) =
let knu = KerName.make mpu dir l in
let knc = if mpu == mpc then knu else KerName.make mpc dir l in
match search_delta_inline resolve knu knc with
- | Some t ->
+ | Some (ctx, t) ->
(* In case of inlining, discard the canonical part (cf #2608) *)
- Constant.make1 knu, t
+ let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in
+ Constant.make1 knu, Vars.subst_instance_constr u t
| None ->
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
@@ -482,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver =
| Equiv kequ ->
(try Equiv (subst_kn_delta subst kequ)
with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
- | Inline (lev,Some t) -> Inline (lev,Some (subst_mps subst t))
+ | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index b14d39207..76a1d173b 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
KerName.t -> KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver :
- KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
+ KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 203817118..22f523a9a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
| Undef _ | OpaqueDef _ -> l
| Def body ->
let constr = Mod_subst.force_constr body in
- add_inline_delta_resolver kn (lev, Some constr) l
+ let ctx = Declareops.constant_polymorphic_context constant in
+ add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
with Not_found ->
error_no_such_label_sub (Constant.label con)
(ModPath.to_string (Constant.modpath con))
diff --git a/kernel/names.ml b/kernel/names.ml
index 54f089e60..1d2a7c4ce 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@
the module system, Aug 2002 *)
(* Abstraction over the type of constant for module inlining by Claudio
Sacerdoti, Nov 2004 *)
-(* Miscellaneous features or improvements by Hugo Herbelin,
+(* Miscellaneous features or improvements by Hugo Herbelin,
Élie Soubiran, ... *)
open Pp
@@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath)
module KerName = struct
type t = {
- canary : Canary.t;
modpath : ModPath.t;
dirpath : DirPath.t;
knlabel : Label.t;
@@ -372,16 +371,14 @@ module KerName = struct
(** Lazily computed hash. If unset, it is set to negative values. *)
}
- let canary = Canary.obj
-
type kernel_name = t
let make modpath dirpath knlabel =
- { modpath; dirpath; knlabel; refhash = -1; canary; }
+ { modpath; dirpath; knlabel; refhash = -1; }
let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
let make2 modpath knlabel =
- { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; }
+ { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
let modpath kn = kn.modpath
let label kn = kn.knlabel
@@ -437,7 +434,7 @@ module KerName = struct
* (string -> string)
let hashcons (hmod,hdir,hstr) kn =
let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
- { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
+ { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
let eq kn1 kn2 =
kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
kn1.knlabel == kn2.knlabel
@@ -852,3 +849,9 @@ let eq_egr e1 e2 = match e1, e2 with
EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
| EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
| _, _ -> false
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/kernel/names.mli b/kernel/names.mli
index f988b559a..4eb5adb62 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -605,3 +605,9 @@ type evaluable_global_reference =
| EvalConstRef of Constant.t
val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index db1109e75..37bf679c5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = Undef nl;
cook_type = t;
- cook_proj = false;
cook_universes = univs;
cook_inline = false;
cook_context = ctx;
@@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = Monomorphic_const univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_proj = false;
cook_universes = univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
- | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
- let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
- let kn, pb =
- match mib.mind_record with
- | Some (Some (id, kns, pbs)) ->
- if i < Array.length pbs then
- kns.(i), pbs.(i)
- else assert false
- | _ -> assert false
- in
- let univs =
- match mib.mind_universes with
- | Monomorphic_ind ctx -> Monomorphic_const ctx
- | Polymorphic_ind auctx -> Polymorphic_const auctx
- | Cumulative_ind acumi ->
- Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
- in
- let term, typ = pb.proj_eta in
- {
- Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term));
- cook_type = typ;
- cook_proj = true;
- cook_universes = univs;
- cook_inline = false;
- cook_context = None;
- }
-
let record_aux env s_ty s_bo =
let in_ty = keep_hyps env s_ty in
let v =
@@ -464,7 +434,6 @@ let build_constant_declaration kn env result =
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_proj = result.cook_proj;
const_body_code = tps;
const_universes = univs;
const_inline_code = result.cook_inline;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 18:20:47 +0000