diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:45:03 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-05 12:51:52 +0100 |
commit | d041f19a7274b6065ca3ef565f0d8b8be08ef0d7 (patch) | |
tree | 283194e5249935fb30580e7353e82072ea9caffd /kernel | |
parent | 76579aff8f8534cbc990b5ea2652b33655512213 (diff) |
[native_compute] Fix handling of evars in conversion
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/nativecode.ml | 17 | ||||
-rw-r--r-- | kernel/nativecode.mli | 2 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 9 | ||||
-rw-r--r-- | kernel/nativeinstr.mli | 2 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 5 | ||||
-rw-r--r-- | kernel/nativevalues.ml | 6 | ||||
-rw-r--r-- | kernel/nativevalues.mli | 4 |
7 files changed, 24 insertions, 21 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 613b2f2ec..8fa254053 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -148,7 +148,7 @@ type symbol = | SymbMatch of annot_sw | SymbInd of inductive | SymbMeta of metavariable - | SymbEvar of existential + | SymbEvar of Evar.t | SymbLevel of Univ.Level.t let dummy_symb = SymbValue (dummy_value ()) @@ -162,8 +162,7 @@ let eq_symbol sy1 sy2 = | 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 Constr.equal args1 args2 + | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 | _, _ -> false @@ -176,10 +175,7 @@ let hash_symbol symb = | 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 + | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) module HashedTypeSymbol = struct @@ -1047,11 +1043,12 @@ 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(ev,ty) -> + | Levar(evk,ty,args) -> let tyn = fresh_lname Anonymous in - let i = push_symbol (SymbEvar ev) in + let i = push_symbol (SymbEvar evk) in + 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|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index d08f49095..7d20054f7 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -44,7 +44,7 @@ val get_ind : symbols -> int -> inductive val get_meta : symbols -> int -> metavariable -val get_evar : symbols -> int -> existential +val get_evar : symbols -> int -> Evar.t val get_level : symbols -> int -> Univ.Level.t diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 6c755290d..bfa982136 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -60,7 +60,12 @@ and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu else match a1, a2 with - | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false + | Ameta (m1,_), Ameta (m2,_) -> + if Int.equal m1 m2 then cu else raise NotConvertible + | 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 | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> @@ -112,7 +117,7 @@ and conv_atom env pb lvl a1 a2 cu = else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ - | Aproj _, _ -> raise NotConvertible + | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) and conv_fix env lvl t1 f1 t2 f2 cu = diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 928283a4d..48ad88444 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -23,7 +23,7 @@ and lambda = | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) - | Levar of existential * lambda (* type *) + | Levar of Evar.t * lambda (* type *) * 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 b333b0fb9..29b3e59da 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -453,11 +453,12 @@ let rec lambda_of_constr env sigma c = let ty = meta_type sigma mv in Lmeta (mv, lambda_of_constr env sigma ty) - | Evar ev -> + | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> let ty = evar_type sigma ev in - Levar(ev, lambda_of_constr env sigma ty) + let args = Array.map (lambda_of_constr env sigma) args in + Levar(evk, lambda_of_constr env sigma ty, args) | Some t -> lambda_of_constr env sigma t) | Cast (c, _, _) -> lambda_of_constr env sigma c diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 95a8fc5a4..3d47b1672 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -61,7 +61,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of existential * t + | Aevar of Evar.t * t * t array | Aproj of Constant.t * accumulator let accumulate_tag = 0 @@ -132,8 +132,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 = - mk_accu (Aevar (ev,ty)) +let mk_evar_accu ev ty args = + mk_accu (Aevar (ev,ty,args)) let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 17d6978cd..993842740 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -51,7 +51,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of existential * t + | Aevar of Evar.t * t (* type *) * t array (* arguments *) | Aproj of Constant.t * accumulator (* Constructors *) @@ -68,7 +68,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 : existential -> t -> t +val mk_evar_accu : Evar.t -> t -> t array -> t val mk_proj_accu : Constant.t -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t |