aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/nativecode.ml115
-rw-r--r--kernel/nativecode.mli8
-rw-r--r--kernel/nativeconv.ml4
-rw-r--r--kernel/nativeconv.mli3
-rw-r--r--kernel/nativelambda.ml110
-rw-r--r--kernel/nativelambda.mli13
-rw-r--r--kernel/nativevalues.ml8
-rw-r--r--kernel/nativevalues.mli6
-rw-r--r--kernel/reduction.ml7
-rw-r--r--kernel/reduction.mli5
-rw-r--r--kernel/typeops.ml5
11 files changed, 191 insertions, 93 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4e34cd60f6..7d542c1073 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -130,6 +130,8 @@ type symbol =
| SymbConst of constant
| SymbMatch of annot_sw
| SymbInd of inductive
+ | SymbMeta of metavariable
+ | SymbEvar of existential
let dummy_symb = SymbValue (dummy_value ())
@@ -141,6 +143,9 @@ let eq_symbol sy1 sy2 =
| SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
| SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
| SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
+ | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
+ | SymbEvar (evk1,args1), SymbEvar (evk2,args2) ->
+ Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2
| _, _ -> false
open Hashset.Combine
@@ -153,6 +158,11 @@ let hash_symbol symb =
| SymbConst c -> combinesmall 4 (Constant.hash c)
| SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
| SymbInd ind -> combinesmall 6 (ind_hash ind)
+ | SymbMeta m -> combinesmall 7 m
+ | SymbEvar (evk,args) ->
+ let evh = Evar.hash evk in
+ let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in
+ combinesmall 8 hl
module HashedTypeSymbol = struct
type t = symbol
@@ -196,6 +206,16 @@ let get_ind tbl i =
| SymbInd ind -> ind
| _ -> anomaly (Pp.str "get_ind failed")
+let get_meta tbl i =
+ match tbl.(i) with
+ | SymbMeta m -> m
+ | _ -> anomaly (Pp.str "get_meta failed")
+
+let get_evar tbl i =
+ match tbl.(i) with
+ | SymbEvar ev -> ev
+ | _ -> anomaly (Pp.str "get_evar failed")
+
let push_symbol x =
try HashtblSymbol.find symb_tbl x
with Not_found ->
@@ -209,7 +229,7 @@ let get_symbols_tbl () =
HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl(**}}}**)
(** Lambda to Mllambda {{{**)
-
+
type primitive =
| Mk_prod
| Mk_sort
@@ -224,6 +244,8 @@ type primitive =
| Cast_accu
| Upd_cofix
| Force_cofix
+ | Mk_meta
+ | Mk_evar
let eq_primitive p1 p2 =
match p1, p2 with
@@ -240,6 +262,8 @@ let eq_primitive p1 p2 =
| Cast_accu, Cast_accu -> true
| Upd_cofix, Upd_cofix -> true
| Force_cofix, Force_cofix -> true
+ | Mk_meta, Mk_meta -> true
+ | Mk_evar, Mk_evar -> true
| _ -> false
type mllambda =
@@ -709,6 +733,12 @@ let get_match_code i =
let get_ind_code i =
MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+let get_meta_code i =
+ MLapp (MLglobal (Ginternal "get_meta"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_evar_code i =
+ MLapp (MLglobal (Ginternal "get_evar"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
type rlist =
| Rnil
| Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist'
@@ -745,6 +775,15 @@ let merge_branches t =
match t with
| Lrel(id ,i) -> get_rel env id i
| Lvar id -> get_var env id
+ | Lmeta(mv,ty) ->
+ let tyn = fresh_lname Anonymous in
+ let i = push_symbol (SymbMeta mv) in
+ MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
+ | Levar(ev,ty) ->
+ let tyn = fresh_lname Anonymous in
+ let i = push_symbol (SymbEvar ev) in
+ MLlet(tyn, ml_of_lam env l ty,
+ MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn|]))
| Lprod(dom,codom) ->
let dom = ml_of_lam env l dom in
let codom = ml_of_lam env l codom in
@@ -1299,7 +1338,7 @@ let pp_mllam fmt l =
and pp_blam fmt l =
match l with
- | MLprimitive (Mk_prod | Mk_sort)
+ | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
| MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
Format.fprintf fmt "(%a)" pp_mllam l
| MLconstruct(_,_,args) when Array.length args > 0 ->
@@ -1314,7 +1353,7 @@ let pp_mllam fmt l =
for i = 1 to len - 1 do
Format.fprintf fmt "%s%a" sep pp_blam args.(i)
done
- end
+ end
and pp_cargs fmt args =
let len = Array.length args in
@@ -1378,6 +1417,8 @@ let pp_mllam fmt l =
| Cast_accu -> Format.fprintf fmt "cast_accu"
| Upd_cofix -> Format.fprintf fmt "upd_cofix"
| Force_cofix -> Format.fprintf fmt "force_cofix"
+ | Mk_meta -> Format.fprintf fmt "mk_meta_accu"
+ | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
in
Format.fprintf fmt "@[%a@]" pp_mllam l
@@ -1428,18 +1469,18 @@ let pp_global fmt g =
Format.fprintf fmt "@[(* %s *)@]@." s(**}}}**)
(** Compilation of elements in environment {{{**)
-let rec compile_with_fv env auxdefs l t =
+let rec compile_with_fv env sigma auxdefs l t =
let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
if List.is_empty fv_named && List.is_empty fv_rel then (auxdefs,ml)
- else apply_fv env (fv_named,fv_rel) auxdefs ml
+ else apply_fv env sigma (fv_named,fv_rel) auxdefs ml
-and apply_fv env (fv_named,fv_rel) auxdefs ml =
+and apply_fv env sigma (fv_named,fv_rel) auxdefs ml =
let get_rel_val (n,_) auxdefs =
(*
match !(lookup_rel_native_val n env) with
| NVKnone ->
*)
- compile_rel env auxdefs n
+ compile_rel env sigma auxdefs n
(* | NVKvalue (v,d) -> assert false *)
in
let get_named_val (id,_) auxdefs =
@@ -1447,7 +1488,7 @@ and apply_fv env (fv_named,fv_rel) auxdefs ml =
match !(lookup_named_native_val id env) with
| NVKnone ->
*)
- compile_named env auxdefs id
+ compile_named env sigma auxdefs id
(* | NVKvalue (v,d) -> assert false *)
in
let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
@@ -1458,32 +1499,32 @@ and apply_fv env (fv_named,fv_rel) auxdefs ml =
let aux_name = fresh_lname Anonymous in
auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
-and compile_rel env auxdefs n =
+and compile_rel env sigma auxdefs n =
let (_,body,_) = lookup_rel n env.env_rel_context in
let n = rel_context_length env.env_rel_context - n in
match body with
| Some t ->
- let code = lambda_of_constr env t in
- let auxdefs,code = compile_with_fv env auxdefs None code in
+ let code = lambda_of_constr env sigma t in
+ let auxdefs,code = compile_with_fv env sigma auxdefs None code in
Glet(Grel n, code)::auxdefs
| None ->
Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
-and compile_named env auxdefs id =
+and compile_named env sigma auxdefs id =
let (_,body,_) = lookup_named id env.env_named_context in
match body with
| Some t ->
- let code = lambda_of_constr env t in
- let auxdefs,code = compile_with_fv env auxdefs None code in
+ let code = lambda_of_constr env sigma t in
+ let auxdefs,code = compile_with_fv env sigma auxdefs None code in
Glet(Gnamed id, code)::auxdefs
| None ->
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
-let compile_constant env prefix ~interactive con body =
+let compile_constant env sigma prefix ~interactive con body =
match body with
| Def t ->
let t = Lazyconstr.force t in
- let code = lambda_of_constr env t in
+ let code = lambda_of_constr env sigma t in
let is_lazy = is_lazy t in
let code = if is_lazy then mk_lazy code else code in
let name =
@@ -1491,7 +1532,7 @@ let compile_constant env prefix ~interactive con body =
else Linked prefix
in
let l = con_label con in
- let auxdefs,code = compile_with_fv env [] (Some l) code in
+ let auxdefs,code = compile_with_fv env sigma [] (Some l) code in
let code =
optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
in
@@ -1574,10 +1615,8 @@ let compile_mind_deps env prefix ~interactive
(* This function compiles all necessary dependencies of t, and generates code in
reverse order, as well as linking information updates *)
-let rec compile_deps env prefix ~interactive init t =
+let rec compile_deps env sigma prefix ~interactive init t =
match kind_of_term t with
- | Meta _ -> invalid_arg "Nativecode.compile_deps: Meta"
- | Evar _ -> invalid_arg "Nativecode.compile_deps: Evar"
| Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
| Const c ->
let c = get_allias env c in
@@ -1588,10 +1627,13 @@ let rec compile_deps env prefix ~interactive init t =
then init
else
let comp_stack, (mind_updates, const_updates) = match cb.const_body with
- | Def t -> compile_deps env prefix ~interactive init (Lazyconstr.force t)
+ | Def t ->
+ compile_deps env sigma prefix ~interactive init (Lazyconstr.force t)
| _ -> init
in
- let code, name = compile_constant env prefix ~interactive c cb.const_body in
+ let code, name =
+ compile_constant env sigma prefix ~interactive c cb.const_body
+ in
let comp_stack = code@comp_stack in
let const_updates = Cmap_env.add c (nameref, name) const_updates in
comp_stack, (mind_updates, const_updates)
@@ -1599,12 +1641,13 @@ let rec compile_deps env prefix ~interactive init t =
| Case (ci, p, c, ac) ->
let mind = fst ci.ci_ind in
let init = compile_mind_deps env prefix ~interactive init mind in
- fold_constr (compile_deps env prefix ~interactive) init t
- | _ -> fold_constr (compile_deps env prefix ~interactive) init t
+ fold_constr (compile_deps env sigma prefix ~interactive) init t
+ | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t
let compile_constant_field env prefix con acc cb =
let (gl, _) =
- compile_constant ~interactive:false env prefix con cb.const_body
+ compile_constant ~interactive:false env empty_evars prefix
+ con cb.const_body
in
gl@acc
@@ -1618,19 +1661,19 @@ let mk_internal_let s code =
Glet(Ginternal s, code)
(* ML Code for conversion function *)
-let mk_conv_code env prefix t1 t2 =
+let mk_conv_code env sigma prefix t1 t2 =
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env prefix ~interactive:true init t1
+ compile_deps env sigma prefix ~interactive:true init t1
in
let gl, (mind_updates, const_updates) =
let init = (gl, (mind_updates, const_updates)) in
- compile_deps env prefix ~interactive:true init t2
+ compile_deps env sigma prefix ~interactive:true init t2
in
- let code1 = lambda_of_constr env t1 in
- let code2 = lambda_of_constr env t2 in
- let (gl,code1) = compile_with_fv env gl None code1 in
- let (gl,code2) = compile_with_fv env gl None code2 in
+ let code1 = lambda_of_constr env sigma t1 in
+ let code2 = lambda_of_constr env sigma t2 in
+ let (gl,code1) = compile_with_fv env sigma gl None code1 in
+ let (gl,code2) = compile_with_fv env sigma gl None code2 in
let t1 = mk_internal_let "t1" code1 in
let t2 = mk_internal_let "t2" code2 in
let g1 = MLglobal (Ginternal "t1") in
@@ -1643,13 +1686,13 @@ let mk_conv_code env prefix t1 t2 =
[|MLglobal (Ginternal "()")|])) in
header::gl, (mind_updates, const_updates)
-let mk_norm_code env prefix t =
+let mk_norm_code env sigma prefix t =
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
- compile_deps env prefix ~interactive:true init t
+ compile_deps env sigma prefix ~interactive:true init t
in
- let code = lambda_of_constr env t in
- let (gl,code) = compile_with_fv env gl None code in
+ let code = lambda_of_constr env sigma t in
+ let (gl,code) = compile_with_fv env sigma gl None code in
let t1 = mk_internal_let "t1" code in
let g1 = MLglobal (Ginternal "t1") in
let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index f6a0c79f4f..7e70949635 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -38,6 +38,10 @@ val get_match : symbol array -> int -> Nativevalues.annot_sw
val get_ind : symbol array -> int -> inductive
+val get_meta : symbol array -> int -> metavariable
+
+val get_evar : symbol array -> int -> existential
+
val get_symbols_tbl : unit -> symbol array
type code_location_update
@@ -56,8 +60,8 @@ val compile_constant_field : env -> string -> constant ->
val compile_mind_field : string -> module_path -> label ->
global list -> mutual_inductive_body -> global list
-val mk_conv_code : env -> string -> constr -> constr -> linkable_code
-val mk_norm_code : env -> string -> constr -> linkable_code
+val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code
+val mk_norm_code : env -> evars -> string -> constr -> linkable_code
val mk_library_header : dir_path -> global list
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 14b55e91a2..3435e1d753 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -127,7 +127,7 @@ and conv_fix lvl t1 f1 t2 f2 cu =
else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
aux 0 cu
-let native_conv pb env t1 t2 =
+let native_conv pb sigma env t1 t2 =
if !Flags.no_native_compiler then begin
let msg = "Native compiler is disabled, "^
"falling back to VM conversion test." in
@@ -137,7 +137,7 @@ let native_conv pb env t1 t2 =
else
let env = Environ.pre_env env in
let ml_filename, prefix = get_ml_filename () in
- let code, upds = mk_conv_code env prefix t1 t2 in
+ let code, upds = mk_conv_code env sigma prefix t1 t2 in
match compile ml_filename code with
| (0,fn) ->
begin
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 2cb5ac7973..2481300763 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -9,7 +9,8 @@ open Term
open Univ
open Environ
open Reduction
+open Nativelambda
(** This module implements the conversion test by compiling to OCaml code *)
-val native_conv : conv_pb -> types conversion_function
+val native_conv : conv_pb -> evars -> types conversion_function
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 800c8e5fb1..258f03efdb 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -17,6 +17,8 @@ open Nativevalues
type lambda =
| Lrel of name * int
| Lvar of identifier
+ | Lmeta of metavariable * lambda (* type *)
+ | Levar of existential * lambda (* type *)
| Lprod of lambda * lambda
| Llam of name array * lambda
| Llet of name * lambda * lambda
@@ -41,23 +43,28 @@ type lambda =
and lam_branches = (constructor * name array * lambda) array
and fix_decl = name array * lambda array * lambda array
-
+
+type evars =
+ { evars_val : existential -> constr option;
+ evars_typ : existential -> types;
+ evars_metas : metavariable -> types }
+
(*s Constructors *)
-
+
let mkLapp f args =
if Array.is_empty args then f
else
match f with
| Lapp(f', args') -> Lapp (f', Array.append args' args)
| _ -> Lapp(f, args)
-
+
let mkLlam ids body =
if Array.is_empty ids then body
else
match body with
| Llam(ids', body) -> Llam(Array.append ids ids', body)
| _ -> Llam(ids, body)
-
+
let decompose_Llam lam =
match lam with
| Llam(ids,body) -> ids, body
@@ -103,8 +110,8 @@ let get_const_prefix env c =
let map_lam_with_binders g f n lam =
match lam with
- | Lrel _ | Lvar _ | Lconst _ | Lval _
- | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce -> lam
+ | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lconstruct _
+ | Llazy | Lforce | Lmeta _ | Levar _ -> lam
| Lprod(dom,codom) ->
let dom' = f n dom in
let codom' = f n codom in
@@ -199,8 +206,8 @@ let lam_subst_args subst args =
let can_subst lam =
match lam with
- | Lrel _ | Lvar _ | Lconst _
- | Lval _ | Lsort _ | Lind _ | Llam _ | Lconstruct _ -> true
+ | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Llam _
+ | Lconstruct _ | Lmeta _ | Levar _ -> true
| _ -> false
let can_merge_if bt bf =
@@ -307,7 +314,7 @@ let rec occurence k kind lam =
if kind then false else raise Not_found
else kind
| Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _
- | Lconstruct _ | Llazy | Lforce -> kind
+ | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
| Lprod(dom, codom) ->
occurence k (occurence k kind dom) codom
| Llam(ids,body) ->
@@ -509,29 +516,48 @@ module Renv =
let is_lazy t = (* APPROXIMATION *)
isApp t || isLetIn t
+let evar_value sigma ev = sigma.evars_val ev
+
+let evar_type sigma ev = sigma.evars_typ ev
+
+let meta_type sigma mv = sigma.evars_metas mv
+
+let empty_evars =
+ { evars_val = (fun _ -> None);
+ evars_typ = (fun _ -> assert false);
+ evars_metas = (fun _ -> assert false) }
+
let empty_ids = [||]
-let rec lambda_of_constr env c =
-(* try *)
+let rec lambda_of_constr env sigma c =
match kind_of_term c with
- | Meta _ -> invalid_arg "Nativelambda.lambda_of_constr: Meta"
- | Evar _ -> invalid_arg "Nativelambda.lambda_of_constr : Evar"
+ | Meta mv ->
+ let ty = meta_type sigma mv in
+ Lmeta (mv, lambda_of_constr env sigma ty)
- | Cast (c, _, _) -> lambda_of_constr env c
+ | Evar ev ->
+ (match evar_value sigma ev with
+ | None ->
+ let ty = evar_type sigma ev in
+ Levar(ev, lambda_of_constr env sigma ty)
+ | Some t -> lambda_of_constr env sigma t)
+
+ | Cast (c, _, _) -> lambda_of_constr env sigma c
| Rel i -> Renv.get env i
| Var id -> Lvar id
| Sort s -> Lsort s
+
| Ind ind ->
let prefix = get_mind_prefix !global_env (fst ind) in
Lind (prefix, ind)
-
+
| Prod(id, dom, codom) ->
- let ld = lambda_of_constr env dom in
+ let ld = lambda_of_constr env sigma dom in
Renv.push_rel env id;
- let lc = lambda_of_constr env codom in
+ let lc = lambda_of_constr env sigma codom in
Renv.pop env;
Lprod(ld, Llam([|id|], lc))
@@ -539,22 +565,22 @@ let rec lambda_of_constr env c =
let params, body = decompose_lam c in
let ids = get_names (List.rev params) in
Renv.push_rels env ids;
- let lb = lambda_of_constr env body in
+ let lb = lambda_of_constr env sigma body in
Renv.popn env (Array.length ids);
mkLlam ids lb
| LetIn(id, def, _, body) ->
- let ld = lambda_of_constr env def in
+ let ld = lambda_of_constr env sigma def in
Renv.push_rel env id;
- let lb = lambda_of_constr env body in
+ let lb = lambda_of_constr env sigma body in
Renv.pop env;
Llet(id, ld, lb)
- | App(f, args) -> lambda_of_app env f args
+ | App(f, args) -> lambda_of_app env sigma f args
- | Const _ -> lambda_of_app env c empty_args
+ | Const _ -> lambda_of_app env sigma c empty_args
- | Construct _ -> lambda_of_app env c empty_args
+ | Construct _ -> lambda_of_app env sigma c empty_args
| Case(ci,t,a,branches) ->
let (mind,i as ind) = ci.ci_ind in
@@ -571,14 +597,14 @@ let rec lambda_of_constr env c =
asw_prefix = prefix}
in
(* translation of the argument *)
- let la = lambda_of_constr env a in
+ let la = lambda_of_constr env sigma a in
(* translation of the type *)
- let lt = lambda_of_constr env t in
+ let lt = lambda_of_constr env sigma t in
(* translation of branches *)
let mk_branch i b =
let cn = (ind,i+1) in
let _, arity = tbl.(i) in
- let b = lambda_of_constr env b in
+ let b = lambda_of_constr env sigma b in
if Int.equal arity 0 then (cn, empty_ids, b)
else
match b with
@@ -592,20 +618,20 @@ let rec lambda_of_constr env c =
Lcase(annot_sw, lt, la, bs)
| Fix(rec_init,(names,type_bodies,rec_bodies)) ->
- let ltypes = lambda_of_args env 0 type_bodies in
+ let ltypes = lambda_of_args env sigma 0 type_bodies in
Renv.push_rels env names;
- let lbodies = lambda_of_args env 0 rec_bodies in
+ let lbodies = lambda_of_args env sigma 0 rec_bodies in
Renv.popn env (Array.length names);
Lfix(rec_init, (names, ltypes, lbodies))
| CoFix(init,(names,type_bodies,rec_bodies)) ->
- let ltypes = lambda_of_args env 0 type_bodies in
+ let ltypes = lambda_of_args env sigma 0 type_bodies in
Renv.push_rels env names;
- let lbodies = lambda_of_args env 0 rec_bodies in
+ let lbodies = lambda_of_args env sigma 0 rec_bodies in
Renv.popn env (Array.length names);
Lcofix(init, (names, ltypes, lbodies))
-and lambda_of_app env f args =
+and lambda_of_app env sigma f args =
match kind_of_term f with
| Const kn ->
let kn = get_allias !global_env kn in
@@ -613,7 +639,7 @@ and lambda_of_app env f args =
begin match cb.const_body with
| Def csubst ->
if cb.const_inline_code then
- lambda_of_app env (Lazyconstr.force csubst) args
+ lambda_of_app env sigma (Lazyconstr.force csubst) args
else
let prefix = get_const_prefix !global_env kn in
let t =
@@ -621,31 +647,31 @@ and lambda_of_app env f args =
mkLapp Lforce [|Lconst (prefix, kn)|]
else Lconst (prefix, kn)
in
- mkLapp t (lambda_of_args env 0 args)
+ mkLapp t (lambda_of_args env sigma 0 args)
| OpaqueDef _ | Undef _ ->
let prefix = get_const_prefix !global_env kn in
- mkLapp (Lconst (prefix, kn)) (lambda_of_args env 0 args)
+ mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
end
| Construct c ->
let tag, nparams, arity = Renv.get_construct_info env c in
let expected = nparams + arity in
let nargs = Array.length args in
if Int.equal nargs expected then
- let args = lambda_of_args env nparams args in
+ let args = lambda_of_args env sigma nparams args in
makeblock !global_env c tag args
else
let prefix = get_mind_prefix !global_env (fst (fst c)) in
- mkLapp (Lconstruct (prefix, c)) (lambda_of_args env 0 args)
+ mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args)
| _ ->
- let f = lambda_of_constr env f in
- let args = lambda_of_args env 0 args in
+ let f = lambda_of_constr env sigma f in
+ let args = lambda_of_args env sigma 0 args in
mkLapp f args
-and lambda_of_args env start args =
+and lambda_of_args env sigma start args =
let nargs = Array.length args in
if start < nargs then
Array.init (nargs - start)
- (fun i -> lambda_of_constr env args.(start + i))
+ (fun i -> lambda_of_constr env sigma args.(start + i))
else empty_args
let optimize lam =
@@ -657,12 +683,12 @@ let optimize lam =
(msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *)
lam
-let lambda_of_constr env c =
+let lambda_of_constr env sigma c =
set_global_env env;
let env = Renv.make () in
let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
Renv.push_rels env (Array.of_list ids);
- let lam = lambda_of_constr env c in
+ let lam = lambda_of_constr env sigma c in
(* if Flags.vm_draw_opt () then begin
(msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all());
(msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all());
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 997efd969f..860283e065 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -18,6 +18,8 @@ open Nativevalues
type lambda =
| Lrel of name * int
| Lvar of identifier
+ | Lmeta of metavariable * lambda (* type *)
+ | Levar of existential * lambda (* type *)
| Lprod of lambda * lambda
| Llam of name array * lambda
| Llet of name * lambda * lambda
@@ -40,9 +42,16 @@ type lambda =
| Lforce
and lam_branches = (constructor * name array * lambda) array
-
+
and fix_decl = name array * lambda array * lambda array
+type evars =
+ { evars_val : existential -> constr option;
+ evars_typ : existential -> types;
+ evars_metas : metavariable -> types }
+
+val empty_evars : evars
+
val decompose_Llam : lambda -> Names.name array * lambda
val decompose_Llam_Llet : lambda -> (Names.name * lambda option) array * lambda
@@ -51,4 +60,4 @@ val mk_lazy : lambda -> lambda
val get_allias : env -> constant -> constant
-val lambda_of_constr : env -> types -> lambda
+val lambda_of_constr : env -> evars -> Constr.constr -> lambda
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index c38b720311..c3e2b3ab75 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -58,6 +58,8 @@ type atom =
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
| Aprod of name * t * (t -> t)
+ | Ameta of metavariable * t
+ | Aevar of existential * t
let accumulate_tag = 0
@@ -120,6 +122,12 @@ let mk_sw_accu annot c p ac =
let mk_prod_accu s dom codom =
mk_accu (Aprod (s,dom,codom))
+let mk_meta_accu mv ty =
+ mk_accu (Ameta (mv,ty))
+
+let mk_evar_accu ev ty =
+ mk_accu (Aevar (ev,ty))
+
let atom_of_accu (k:accumulator) =
(Obj.magic (Obj.field (Obj.magic k) 2) : atom)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index c8adb07e50..150811b72c 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -50,6 +50,8 @@ type atom =
| Acofix of t array * t array * int * t
| Acofixe of t array * t array * int * t
| Aprod of name * t * (t -> t)
+ | Ameta of metavariable * t
+ | Aevar of existential * t
(* Constructors *)
@@ -63,7 +65,9 @@ val mk_var_accu : identifier -> t
val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
val mk_prod_accu : name -> t -> t -> t
val mk_fix_accu : rec_pos -> int -> t array -> t array -> t
-val mk_cofix_accu : int -> t array -> t array -> t
+val mk_cofix_accu : int -> t array -> t array -> t
+val mk_meta_accu : metavariable -> t
+val mk_evar_accu : existential -> t -> t
val upd_cofix : t -> t -> unit
val force_cofix : t -> t
val mk_const : tag -> t
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index db858e0a04..f7805459f2 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -474,15 +474,16 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
v2
(* option for conversion *)
-let nat_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
+let nat_conv = ref (fun cv_pb sigma ->
+ fconv cv_pb false (sigma.Nativelambda.evars_val))
let set_nat_conv f = nat_conv := f
-let native_conv cv_pb env t1 t2 =
+let native_conv cv_pb sigma env t1 t2 =
if eq_constr t1 t2 then empty_constraint
else begin
let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
- !nat_conv cv_pb env t1 t2
+ !nat_conv cv_pb sigma env t1 t2
end
let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6e4634194d..2d117cc96c 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -55,8 +55,9 @@ val conv_leq_vecti :
val set_vm_conv : (conv_pb -> types conversion_function) -> unit
val vm_conv : conv_pb -> types conversion_function
-val set_nat_conv : (conv_pb -> types conversion_function) -> unit
-val native_conv : conv_pb -> types conversion_function
+val set_nat_conv :
+ (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
+val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
val default_conv : conv_pb -> ?l2r:bool -> types conversion_function
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a9cc151cf7..6c4cb45742 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -271,8 +271,9 @@ let judge_of_cast env cj k tj =
cj.uj_val,
conv_leq true env cj.uj_type expected_type
| NATIVEcast ->
- mkCast (cj.uj_val, k, expected_type),
- native_conv CUMUL env cj.uj_type expected_type
+ let sigma = Nativelambda.empty_evars in
+ mkCast (cj.uj_val, k, expected_type),
+ native_conv CUMUL sigma env cj.uj_type expected_type
in
{ uj_val = c;
uj_type = expected_type },
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 21:45:24 +0000