diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 9 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/nativeinstr.mli | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 12 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 1 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 6 | ||||
| -rw-r--r-- | kernel/nativevalues.mli | 4 |
7 files changed, 16 insertions, 20 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index cc35a70cbf..ad10c86945 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1067,12 +1067,11 @@ let ml_of_instance instance u = let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) - | Levar(evk,ty,args) -> - let tyn = fresh_lname Anonymous in + | Levar(evk, args) -> let i = push_symbol (SymbEvar evk) in + (** Arguments are *not* reversed in evar instances in native compilation *) let args = MLarray(Array.map (ml_of_lam env l) args) in - MLlet(tyn, ml_of_lam env l ty, - MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|]) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in @@ -1749,7 +1748,7 @@ let pp_mllam fmt l = | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i | Mk_var id -> - Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) + Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 931b8bbc86..c75dde843e 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu = match a1, a2 with | Ameta (m1,_), Ameta (m2,_) -> if Int.equal m1 m2 then cu else raise NotConvertible - | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + | Aevar (ev1, args1), Aevar (ev2, args2) -> if Evar.equal ev1 ev2 then Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu else raise NotConvertible diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 5075bd3d14..2d8e2ba2f0 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -25,7 +25,7 @@ and lambda = | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) - | Levar of Evar.t * lambda (* type *) * lambda array (* arguments *) + | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index cec0ee57d5..122fe95df4 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -23,7 +23,6 @@ exception NotClosed type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } (*s Constructors *) @@ -88,7 +87,7 @@ let get_const_prefix env c = let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam + | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -139,6 +138,9 @@ let rec map_lam_with_binders g f n lam = | Luint u -> let u' = map_uint g f n u in if u == u' then lam else Luint u' + | Levar (evk, args) -> + let args' = Array.Smart.map (f n) args in + if args == args' then lam else Levar (evk, args') and map_uint g f n u = match u with @@ -386,13 +388,10 @@ let is_lazy env prefix 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 = [||] @@ -420,9 +419,8 @@ let rec lambda_of_constr cache env sigma c = | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> - let ty = evar_type sigma ev in let args = Array.map (lambda_of_constr cache env sigma) args in - Levar(evk, lambda_of_constr cache env sigma ty, args) + Levar(evk, args) | Some t -> lambda_of_constr cache env sigma t) | Cast (c, _, _) -> lambda_of_constr cache env sigma c diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index efe1700cd7..7b20258929 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -15,7 +15,6 @@ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } val empty_evars : evars diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 91f6add1c3..3bf23f1468 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -63,7 +63,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t * t array + | Aevar of Evar.t * t array | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 @@ -135,8 +135,8 @@ let mk_prod_accu s dom codom = let mk_meta_accu mv ty = mk_accu (Ameta (mv,ty)) -let mk_evar_accu ev ty args = - mk_accu (Aevar (ev,ty,args)) +let mk_evar_accu ev args = + mk_accu (Aevar (ev, args)) let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 6bbf15160c..10689941e8 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -53,7 +53,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t (* type *) * t array (* arguments *) + | Aevar of Evar.t * t array (* arguments *) | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -70,7 +70,7 @@ val mk_prod_accu : Name.t -> 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_meta_accu : metavariable -> t -val mk_evar_accu : Evar.t -> t -> t array -> t +val mk_evar_accu : Evar.t -> t array -> t val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t |