diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 23 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 4 | ||||
| -rw-r--r-- | kernel/constr.ml | 5 | ||||
| -rw-r--r-- | kernel/constr.mli | 4 | ||||
| -rw-r--r-- | kernel/csymtable.ml | 2 | ||||
| -rw-r--r-- | kernel/csymtable.mli | 2 | ||||
| -rw-r--r-- | kernel/inductive.ml | 24 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 1 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 23 | ||||
| -rw-r--r-- | kernel/nativecode.mli | 2 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 11 | ||||
| -rw-r--r-- | kernel/nativeinstr.mli | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.ml | 5 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 18 | ||||
| -rw-r--r-- | kernel/nativevalues.mli | 6 | ||||
| -rw-r--r-- | kernel/pre_env.ml | 3 | ||||
| -rw-r--r-- | kernel/pre_env.mli | 4 | ||||
| -rw-r--r-- | kernel/reduction.ml | 48 | ||||
| -rw-r--r-- | kernel/term.ml | 2 | ||||
| -rw-r--r-- | kernel/term.mli | 4 | ||||
| -rw-r--r-- | kernel/vconv.ml | 1 | ||||
| -rw-r--r-- | kernel/vconv.mli | 2 | ||||
| -rw-r--r-- | kernel/vm.ml | 546 | ||||
| -rw-r--r-- | kernel/vm.mli | 106 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 525 | ||||
| -rw-r--r-- | kernel/vmvalues.mli | 144 |
26 files changed, 802 insertions, 715 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index b1181157e1..219ea5b24a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -91,6 +91,7 @@ module type RedFlagsSig = sig val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds val red_add_transparent : reds -> transparent_state -> reds + val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> projection -> bool @@ -164,6 +165,8 @@ module RedFlags = (struct let (l1,l2) = red.r_const in { red with r_const = Id.Pred.remove id l1, l2 } + let red_transparent red = red.r_const + let red_add_transparent red tr = { red with r_const = tr } @@ -847,6 +850,14 @@ let contract_fix_vect fix = in (subs_cons(Array.init nfix make_body, env), thisbody) +let unfold_projection info p = + if red_projection info.i_flags p + then + let open Declarations in + let pb = lookup_projection p (info_env info) in + Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p)) + else None + (*********************************************************************) (* A machine that inspects the head of a term until it finds an atom or a subterm that may produce a redex (abstraction, @@ -865,15 +876,9 @@ let rec knh info m stk = | (None, stk') -> (m,stk')) | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - let unf = Projection.unfolded p in - if unf || red_set info.i_flags (fCONST (Projection.constant p)) then - (match try Some (lookup_projection p (info_env info)) with Not_found -> None with - | None -> (m, stk) - | Some pb -> - knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - Projection.constant p) - :: zupdate m stk)) - else (m,stk) + (match unfold_projection info p with + | None -> (m, stk) + | Some s -> knh info c (s :: zupdate m stk)) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 119b70e301..c43fc46239 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -61,6 +61,9 @@ module type RedFlagsSig = sig (** Adds a reduction kind to a set *) val red_add_transparent : reds -> transparent_state -> reds + (** Retrieve the transparent state of the reduction flags *) + val red_transparent : reds -> transparent_state + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds @@ -163,6 +166,7 @@ val stack_tail : int -> stack -> stack val stack_nth : stack -> int -> fconstr val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack +val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use diff --git a/kernel/constr.ml b/kernel/constr.ml index 5930cfadc6..1ff1fcc4c0 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1178,8 +1178,3 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) - -(*******) -(* Type of abstract machine values *) -(** FIXME: nothing to do there *) -type values diff --git a/kernel/constr.mli b/kernel/constr.mli index 98bf713082..19ffa8fe30 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -459,7 +459,3 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr - -(**************************************) - -type values diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 712c66f11d..2bbb867cd4 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -15,7 +15,7 @@ open Util open Names open Constr -open Vm +open Vmvalues open Cemitcodes open Cbytecodes open Declarations diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 91bb30e7ed..fc935f6ee9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -12,7 +12,7 @@ open Names open Constr open Pre_env -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values val set_opaque_const : Constant.t -> unit val set_transparent_const : Constant.t -> unit diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 28a09b81b0..722705bd70 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -796,18 +796,18 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | Subterm (s, wf) -> - (* We take the subterm specs of the constructor of the record *) - let wf_args = (dest_subterms wf).(0) in - (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - Subterm (Strict, List.nth wf_args n) - | Dead_code -> Dead_code - | Not_subterm -> Not_subterm) + (match subt with + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | CoFix _ -> Not_subterm diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 917e4f6f14..749854b8cd 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -16,6 +16,7 @@ Cemitcodes Opaqueproof Declarations Entries +Vmvalues Nativevalues CPrimitives Declareops diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ffe19510a6..8fa2540536 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 @@ -1919,15 +1916,17 @@ let compile_constant env sigma prefix ~interactive con cb = let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; asw_reloc = tbl; asw_finite = true } in let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in let _, arity = tbl.(0) in let ci_uid = fresh_lname Anonymous in let cargs = Array.init arity (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) in let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in let gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index d08f49095e..7d20054f77 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 9f9102f7d2..bfa9821360 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -54,13 +54,18 @@ and conv_accu env pb lvl k1 k2 cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in - List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + Array.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu 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 928283a4d8..48ad884440 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 b333b0fb9c..29b3e59da8 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 ae66362ca3..3d47b1672e 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)) @@ -153,8 +153,7 @@ let accu_nargs (k:accumulator) = let args_of_accu (k:accumulator) = let nargs = accu_nargs k in let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in - let t = Array.init nargs f in - Array.to_list t + Array.init nargs f let is_accu x = let o = Obj.repr x in @@ -179,11 +178,10 @@ let force_cofix (cofix : t) = let atom = atom_of_accu accu in match atom with | Acofix(typ,norm,pos,f) -> - let f = ref f in - let args = List.rev (args_of_accu accu) in - List.iter (fun x -> f := !f x) args; - let v = !f (Obj.magic ()) in - set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); + let args = args_of_accu accu in + let f = Array.fold_right (fun arg f -> f arg) args f in + let v = f (Obj.magic ()) in + set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); v | Acofixe(_,_,_,v) -> v | _ -> cofix diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 18b877745b..993842740b 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 @@ -84,7 +84,7 @@ val napply : t -> t array -> t val dummy_value : unit -> t val atom_of_accu : accumulator -> atom -val args_of_accu : accumulator -> t list +val args_of_accu : accumulator -> t array val accu_nargs : accumulator -> int val cast_accu : t -> accumulator diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 3ef15105ae..6c5e1cde5a 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -15,7 +15,6 @@ open Util open Names -open Constr open Declarations module NamedDecl = Context.Named.Declaration @@ -50,7 +49,7 @@ type stratification = { } type val_kind = - | VKvalue of (values * Id.Set.t) CEphemeron.key + | VKvalue of (Vmvalues.values * Id.Set.t) CEphemeron.key | VKnone type lazy_val = val_kind ref diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 335ca1057f..a6b57bd1b3 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -36,9 +36,9 @@ type stratification = { type lazy_val -val force_lazy_val : lazy_val -> (values * Id.Set.t) option +val force_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val -val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit +val build_lazy_val : lazy_val -> (Vmvalues.values * Id.Set.t) -> unit type named_context_val = private { env_named_ctx : Context.Named.t; diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c07ac973b8..1724f210db 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -308,17 +308,6 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true | FLOCKED -> assert false -let unfold_projection infos p c = - let unf = Projection.unfolded p in - if unf || RedFlags.red_set infos.i_flags (RedFlags.fCONST (Projection.constant p)) then - (match try Some (lookup_projection p (info_env infos)) with Not_found -> None with - | Some pb -> - let s = Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, - Projection.constant p) in - Some (c, s) - | None -> None) - else None - (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv @@ -396,13 +385,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Projections: prefer unfolding to first-order unification, which will happen naturally if the terms c1, c2 are not in constructor form *) - (match unfold_projection infos p1 c1 with - | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + (match unfold_projection infos p1 with + | Some s1 -> + eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> - match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + match unfold_projection infos p2 with + | Some s2 -> + eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then @@ -412,9 +401,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = raise NotConvertible) | (FProj (p1,c1), t2) -> - (match unfold_projection infos p1 c1 with - | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv + (match unfold_projection infos p1 with + | Some s1 -> + eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> @@ -425,9 +414,9 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> raise NotConvertible)) | (t1, FProj (p2,c2)) -> - (match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv + (match unfold_projection infos p2 with + | Some s2 -> + eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> (match t1 with | FFlex fl1 -> @@ -479,7 +468,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + (** By virtue of the previous case analyses, we know [c2] is rigid. + Conversion check to rigid terms eventually implies full weak-head + reduction, so instead of repeatedly performing small-step + unfoldings, we perform reduction with all flags on. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r1 = whd_stack (infos_with_reds infos all) def1 v1 in + eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -493,7 +488,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + (** Symmetrical case of above. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r2 = whd_stack (infos_with_reds infos all) def2 v2 in + eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> diff --git a/kernel/term.ml b/kernel/term.ml index aa88059524..fae990d45f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | CoFix of ('constr, 'types) pcofixpoint | Proj of projection * 'constr -type values = Constr.values +type values = Vmvalues.values (**********************************************************************) (** Redeclaration of functions from module Constr *) diff --git a/kernel/term.mli b/kernel/term.mli index f5cb72f4e8..c9a8cf6e1e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -572,8 +572,8 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Proj of projection * 'constr [@@ocaml.deprecated "Alias for Constr.kind_of_term"] -type values = Constr.values -[@@ocaml.deprecated "Alias for Constr.values"] +type values = Vmvalues.values +[@@ocaml.deprecated "Alias for Vmvalues.values"] val hash_constr : Constr.constr -> int [@@ocaml.deprecated "Alias for Constr.hash"] diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3ef297b1f4..8c76581478 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -3,6 +3,7 @@ open Names open Environ open Reduction open Vm +open Vmvalues open Csymtable let val_of_constr env c = diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 7f727df475..c3c9636e89 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,4 +19,4 @@ val vm_conv : conv_pb -> types kernel_conversion_function val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function (** Precompute a VM value from a constr *) -val val_of_constr : env -> constr -> values +val val_of_constr : env -> constr -> Vmvalues.values diff --git a/kernel/vm.ml b/kernel/vm.ml index 51101f88e4..352ea74a41 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -6,47 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Sorts -open Constr open Cbytecodes +open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" -(******************************************) -(* Utility Functions about Obj ************) -(******************************************) - -external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" -external offset : Obj.t -> int = "coq_offset" - -(*******************************************) -(* Initalization of the abstract machine ***) -(*******************************************) - -external init_vm : unit -> unit = "init_coq_vm" - -let _ = init_vm () - -(*******************************************) -(* Machine code *** ************************) -(*******************************************) - -type tcode -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) - -external mkAccuCode : int -> tcode = "coq_makeaccu" external mkPopStopCode : int -> tcode = "coq_pushpop" -external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -external int_tcode : tcode -> int -> int = "coq_int_tcode" - -external accumulate : unit -> tcode = "accumulate_code" -let accumulate = accumulate () - -external is_accumulate : tcode -> bool = "coq_is_accumulate_code" - let popstop_tbl = ref (Array.init 30 mkPopStopCode) let popstop_code i = @@ -62,106 +28,6 @@ let popstop_code i = let stop = popstop_code 0 -(******************************************************) -(* Abstract data types and utility functions **********) -(******************************************************) - -(* Values of the abstract machine *) -let val_of_obj v = ((Obj.obj v):values) -let crazy_val = (val_of_obj (Obj.repr 0)) - -(* Abstract data *) -type vprod -type vfun -type vfix -type vcofix -type vblock -type arguments - -type vm_env -type vstack = values array - -type vswitch = { - sw_type_code : tcode; - sw_code : tcode; - sw_annot : annot_switch; - sw_stk : vstack; - sw_env : vm_env - } - -(* Representation of values *) -(* + Products : *) -(* - vprod = 0_[ dom | codom] *) -(* dom : values, codom : vfun *) -(* *) -(* + Functions have two representations : *) -(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) -(* C:tcode, fvi : values *) -(* Remark : a function and its environment is the same value. *) -(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) -(* *) -(* + Fixpoints : *) -(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) -(* One single block to represent all of the fixpoints, each fixpoint *) -(* is the pointer to the field holding the pointer to its code, and *) -(* the infix tag is used to know where the block starts. *) -(* - Partial application follows the scheme of partially applied *) -(* functions. Note: only fixpoints not having been applied to its *) -(* recursive argument are coded this way. When the rec. arg. is *) -(* applied, either it's a constructor and the fix reduces, or it's *) -(* and the fix is coded as an accumulator. *) -(* *) -(* + Cofixpoints : see cbytegen.ml *) -(* *) -(* + vblock's encode (non constant) constructors as in Ocaml, but *) -(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) -(* accumulators. *) -(* *) -(* + vm_env is the type of the machine environments (i.e. a function or *) -(* a fixpoint) *) -(* *) -(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) -(* - representation of [accu] : tag_[....] *) -(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) -(* -- 10_[accu|proj name] : a projection blocked by an accu *) -(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) -(* -- 12_[accu|vswitch] : a match blocked by an accu *) -(* -- 13_[fcofix] : a cofix function *) -(* -- 14_[fcofix|val] : a cofix function, val represent the value *) -(* of the function applied to arg1 ... argn *) -(* The [arguments] type, which is abstracted as an array, represents : *) -(* tag[ _ | _ |v1|... | vn] *) -(* Generally the first field is a code pointer. *) - -(* Do not edit this type without editing C code, especially "coq_values.h" *) - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(* Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix*arguments (* Possibly empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up = values - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t (************************************************) (* Abstract machine *****************************) @@ -178,389 +44,72 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" external interprete : tcode -> values -> vm_env -> int -> values = "coq_interprete_ml" - - (* Functions over arguments *) -let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 -let arg args i = - if 0 <= i && i < (nargs args) then - val_of_obj (Obj.field (Obj.repr args) (i+2)) - else invalid_arg - ("Vm.arg size = "^(string_of_int (nargs args))^ - " acces "^(string_of_int i)) (* Apply a value to arguments contained in [vargs] *) let apply_arguments vf vargs = let n = nargs vargs in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; push_arguments vargs; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end (* Apply value [vf] to an array of argument values [varray] *) let apply_varray vf varray = let n = Array.length varray in - if Int.equal n 0 then vf + if Int.equal n 0 then fun_val vf else begin push_ra stop; (* The fun code of [vf] will make sure we have enough stack, so we put 0 here. *) push_vstack varray 0; - interprete (fun_code vf) vf (Obj.magic vf) (n - 1) + interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(*************************************************) -(* Destructors ***********************************) -(*************************************************) - -let uni_lvl_val (v : values) : Univ.Level.t = - let whd = Obj.magic v in - match whd with - | Vuniv_level lvl -> lvl - | _ -> - let pr = - let open Pp in - match whd with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" - | _ -> assert false - in - CErrors.anomaly - Pp.( strbrk "Parsing virtual machine value expected universe level, got " - ++ pr ++ str ".") - -let rec whd_accu a stk = - let stk = - if Int.equal (Obj.size a) 2 then stk - else Zapp (Obj.obj a) :: stk in - let at = Obj.field a 1 in - match Obj.tag at with - | i when Int.equal i type_atom_tag -> - begin match stk with - | [Zapp args] -> - let u = ref (Obj.obj (Obj.field at 0)) in - for i = 0 to nargs args - 1 do - u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) - done; - Vsort (Type !u) - | _ -> assert false - end - | i when i <= max_atom_tag -> - Vatom_stk(Obj.magic at, stk) - | i when Int.equal i proj_tag -> - let zproj = Zproj (Obj.obj (Obj.field at 0)) in - whd_accu (Obj.field at 1) (zproj :: stk) - | i when Int.equal i fix_app_tag -> - let fa = Obj.field at 1 in - let zfix = - Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in - whd_accu (Obj.field at 0) (zfix :: stk) - | i when Int.equal i switch_tag -> - let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in - whd_accu (Obj.field at 0) (zswitch :: stk) - | i when Int.equal i cofix_tag -> - let vcfx = Obj.obj (Obj.field at 0) in - let to_up = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcfx, to_up, None) - | [Zapp args] -> Vcofix(vcfx, to_up, Some args) - | _ -> assert false - end - | i when Int.equal i cofix_evaluated_tag -> - let vcofix = Obj.obj (Obj.field at 0) in - let res = Obj.obj a in - begin match stk with - | [] -> Vcofix(vcofix, res, None) - | [Zapp args] -> Vcofix(vcofix, res, Some args) - | _ -> assert false - end - | tg -> - CErrors.anomaly - Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") - -external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" - -let whd_val : values -> whd = - fun v -> - let o = Obj.repr v in - if Obj.is_int o then Vconstr_const (Obj.obj o) - else - let tag = Obj.tag o in - if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) - else - if tag = Obj.closure_tag || tag = Obj.infix_tag then - (match kind_of_closure o with - | 0 -> Vfun(Obj.obj o) - | 1 -> Vfix(Obj.obj o, None) - | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) - | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) - else - Vconstr_block(Obj.obj o) - -(**********************************************) -(* Constructors *******************************) -(**********************************************) - -let obj_of_atom : atom -> Obj.t = - fun a -> - let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); - Obj.set_field res 1 (Obj.repr a); - res - -(* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = - match str with - | Const_sorts s -> Obj.repr (Vsort s) - | Const_ind ind -> obj_of_atom (Aind ind) - | Const_proj p -> Obj.repr p - | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res - | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) - -let val_of_obj o = ((Obj.obj o) : values) - -let val_of_str_const str = val_of_obj (obj_of_str_const str) - -let val_of_atom a = val_of_obj (obj_of_atom a) - -let atom_of_proj kn v = - let r = Obj.new_block proj_tag 2 in - Obj.set_field r 0 (Obj.repr kn); - Obj.set_field r 1 (Obj.repr v); - ((Obj.obj r) : atom) - -let val_of_proj kn v = - val_of_atom (atom_of_proj kn v) - -module IdKeyHash = -struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal - open Hashset.Combine - let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) - | VarKey id -> combinesmall 2 (Id.hash id) - | RelKey i -> combinesmall 3 (Int.hash i) -end - -module KeyTable = Hashtbl.Make(IdKeyHash) - -let idkey_tbl = KeyTable.create 31 - -let val_of_idkey key = - try KeyTable.find idkey_tbl key - with Not_found -> - let v = val_of_atom (Aid key) in - KeyTable.add idkey_tbl key v; - v - -let val_of_rel k = val_of_idkey (RelKey k) - -let val_of_named id = val_of_idkey (VarKey id) - -let val_of_constant c = val_of_idkey (ConstKey c) - -external val_of_annot_switch : annot_switch -> values = "%identity" - +(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) - -(*************************************************) -(** Operations manipulating data types ***********) -(*************************************************) - -(* Functions over products *) - -let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) -let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) - -(* Functions over vfun *) - -external closure_arity : vfun -> int = "coq_closure_arity" - -let body_of_vfun k vf = +let reduce_fun k vf = let vargs = mkrel_vstack k 1 in - apply_varray (Obj.magic vf) vargs + apply_varray vf vargs let decompose_vfun2 k vf1 vf2 = let arity = min (closure_arity vf1) (closure_arity vf2) in assert (0 < arity && arity < Sys.max_array_length); let vargs = mkrel_vstack k arity in - let v1 = apply_varray (Obj.magic vf1) vargs in - let v2 = apply_varray (Obj.magic vf2) vargs in + let v1 = apply_varray vf1 vargs in + let v2 = apply_varray vf2 vargs in arity, v1, v2 -(* Functions over fixpoint *) - -let first o = (offset_closure o (offset o)) -let last o = (Obj.field o (Obj.size o - 1)) - -let current_fix vf = - (offset (Obj.repr vf) / 2) - -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) - -let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 - -let rec_args vf = - let fb = first (Obj.repr vf) in - let size = Obj.size (last fb) in - Array.init size (unsafe_rec_arg fb) - -exception FALSE - -let check_fix f1 f2 = - let i1, i2 = current_fix f1, current_fix f2 in - (* Checking starting point *) - if i1 = i2 then - let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in - let n = Obj.size (last fb1) in - (* Checking number of definitions *) - if n = Obj.size (last fb2) then - (* Checking recursive arguments *) - try - for i = 0 to n - 1 do - if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i - then raise FALSE - done; - true - with FALSE -> false - else false - else false - (* Functions over vfix *) -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" - -let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; - ref (Array.init len mkAccuCode) - -let relaccu_code i = - let len = Array.length !relaccu_tbl in - if i < len then !relaccu_tbl.(i) - else - begin - realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; - relaccu_tbl := - Array.init nl - (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); - !relaccu_tbl.(i) - end let reduce_fix k vf = - let fb = first (Obj.repr vf) in + let fb = first_fix vf in (* computing types *) - let fc_typ = ((Obj.obj (last fb)) : tcode array) in + let fc_typ = fix_types fb in let ndef = Array.length fc_typ in - let et = offset_closure fb (2*(ndef - 1)) in + let et = offset_closure_fix fb (2*(ndef - 1)) in let ftyp = Array.map - (fun c -> interprete c crazy_val (Obj.magic et) 0) fc_typ in + (fun c -> interprete c crazy_val et 0) fc_typ in (* Construction of the environment of fix bodies *) - let e = Obj.dup fb in - for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) - done; - let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in - let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); - Obj.set_field res 1 (offset_closure e (2*i)); - ((Obj.obj res) : vfun) in - (Array.init ndef fix_body, ftyp) - -(* Functions over vcofix *) - -let get_fcofix vcf i = - match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with - | Vcofix(vcfi, _, _) -> vcfi - | _ -> assert false - -let current_cofix vcf = - let ndef = Obj.size (last (Obj.repr vcf)) in - let rec find_cofix pos = - if pos < ndef then - if get_fcofix vcf pos == vcf then pos - else find_cofix (pos+1) - else raise Not_found in - try find_cofix 0 - with Not_found -> assert false - -let check_cofix vcf1 vcf2 = - (current_cofix vcf1 = current_cofix vcf2) && - (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + (mk_fix_body k ndef fb, ftyp) let reduce_cofix k vcf = - let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in + let fc_typ = cofix_types vcf in let ndef = Array.length fc_typ in let ftyp = (* Evaluate types *) - Array.map (fun c -> interprete c crazy_val (Obj.magic vcf) 0) fc_typ in + Array.map (fun c -> interprete c crazy_val (cofix_env vcf) 0) fc_typ in (* Construction of the environment of cofix bodies *) - let e = Obj.dup (Obj.repr vcf) in - for i = 0 to ndef - 1 do - Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) - done; - - let cofix_body i = - let vcfi = get_fcofix vcf i in - let c = Obj.field (Obj.repr vcfi) 0 in - Obj.set_field e 0 c; - let atom = Obj.new_block cofix_tag 1 in - let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); - Obj.set_field self 1 (Obj.repr atom); - apply_varray (Obj.obj e) [|Obj.obj self|] in - (Array.init ndef cofix_body, ftyp) - - -(* Functions over vblock *) - -let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) -let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) -let bfield b i = - if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) - else invalid_arg "Vm.bfield" - - -(* Functions over vswitch *) - -let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl - -let case_info sw = sw.sw_annot.ci + (mk_cofix_body apply_varray k ndef vcf, ftyp) let type_of_switch sw = (* The fun code of types will make sure we have enough stack, so we put 0 @@ -568,20 +117,6 @@ let type_of_switch sw = push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 -let branch_arg k (tag,arity) = - if Int.equal arity 0 then ((Obj.magic tag):values) - else - let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 - else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); - b,1 in - for i = ofs to ofs + arity - 1 do - Obj.set_field b i (Obj.repr (val_of_rel (k+i))) - done; - val_of_obj b - let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then @@ -603,8 +138,8 @@ let branch_of_switch k sw = (* t = a stk --> t v *) let rec apply_stack a stk v = match stk with - | [] -> apply_varray a [|v|] - | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v + | [] -> apply_varray (fun_of_val a) [|v|] + | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v | Zfix(f,args) :: stk -> let a,stk = @@ -615,7 +150,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args+ nargs args') in a, stk | _ -> @@ -623,7 +158,7 @@ let rec apply_stack a stk v = push_val a; push_arguments args; let a = - interprete (fun_code f) (Obj.magic f) (Obj.magic f) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) in a, stk in apply_stack a stk v @@ -634,50 +169,21 @@ let apply_whd k whd = let v = val_of_rel k in match whd with | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false - | Vfun f -> body_of_vfun k f + | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; push_val v; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) 0 + interprete (fix_code f) (fix_val f) (fix_env f) 0 | Vfix(f, Some args) -> push_ra stop; push_val v; push_arguments args; - interprete (fun_code f) (Obj.magic f) (Obj.magic f) (nargs args) + interprete (fix_code f) (fix_val f) (fix_env f) (nargs args) | Vcofix(_,to_up,_) -> push_ra stop; push_val v; - interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0 + interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v | Vuniv_level lvl -> assert false -let rec pr_atom a = - Pp.(match a with - | Aid c -> str "Aid(" ++ (match c with - | ConstKey c -> Constant.print c - | RelKey i -> str "#" ++ int i - | _ -> str "...") ++ str ")" - | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") -and pr_whd w = - Pp.(match w with - | Vsort _ -> str "Vsort" - | Vprod _ -> str "Vprod" - | Vfun _ -> str "Vfun" - | Vfix _ -> str "Vfix" - | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" - | Vuniv_level _ -> assert false) -and pr_stack stk = - Pp.(match stk with - | [] -> str "[]" - | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) -and pr_zipper z = - Pp.(match z with - | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" - | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vm.mli b/kernel/vm.mli index bc38452d4f..c6d92ba266 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -6,118 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Constr -open Cbytecodes +open Vmvalues (** Debug printing *) val set_drawinstr : unit -> unit -(** Machine code *) - -type tcode - -(** Values *) - -type vprod -type vfun -type vfix -type vcofix -type vblock -type vswitch -type arguments - -type atom = - | Aid of Vars.id_key - | Aind of inductive - | Atype of Univ.Universe.t - -(** Zippers *) - -type zipper = - | Zapp of arguments - | Zfix of vfix * arguments (** might be empty *) - | Zswitch of vswitch - | Zproj of Constant.t (* name of the projection *) - -type stack = zipper list - -type to_up - -type whd = - | Vsort of Sorts.t - | Vprod of vprod - | Vfun of vfun - | Vfix of vfix * arguments option - | Vcofix of vcofix * to_up * arguments option - | Vconstr_const of int - | Vconstr_block of vblock - | Vatom_stk of atom * stack - | Vuniv_level of Univ.Level.t - -(** For debugging purposes only *) - -val pr_atom : atom -> Pp.t -val pr_whd : whd -> Pp.t -val pr_stack : stack -> Pp.t - -(** Constructors *) - -val val_of_str_const : structured_constant -> values -val val_of_rel : int -> values -val val_of_named : Id.t -> values -val val_of_constant : Constant.t -> values - -external val_of_annot_switch : annot_switch -> values = "%identity" - -(** Destructors *) - -val whd_val : values -> whd -val uni_lvl_val : values -> Univ.Level.t - -(** Arguments *) - -val nargs : arguments -> int -val arg : arguments -> int -> values - -(** Product *) - -val dom : vprod -> values -val codom : vprod -> vfun - -(** Function *) - -val body_of_vfun : int -> vfun -> values -val decompose_vfun2 : int -> vfun -> vfun -> int * values * values - -(** Fix *) - -val current_fix : vfix -> int -val check_fix : vfix -> vfix -> bool -val rec_args : vfix -> int array val reduce_fix : int -> vfix -> vfun array * values array (** bodies , types *) -(** CoFix *) - -val current_cofix : vcofix -> int -val check_cofix : vcofix -> vcofix -> bool val reduce_cofix : int -> vcofix -> values array * values array (** bodies , types *) -(** Block *) +val type_of_switch : vswitch -> values -val btag : vblock -> int -val bsize : vblock -> int -val bfield : vblock -> int -> values +val branch_of_switch : int -> vswitch -> (int * values) array -(** Switch *) +val reduce_fun : int -> vfun -> values -val check_switch : vswitch -> vswitch -> bool -val case_info : vswitch -> case_info -val type_of_switch : vswitch -> values -val branch_of_switch : int -> vswitch -> (int * values) array +(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current + DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced + bodies under those lambdas. *) +val decompose_vfun2 : int -> vfun -> vfun -> int * values * values (** Apply a value *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml new file mode 100644 index 0000000000..1102cdec18 --- /dev/null +++ b/kernel/vmvalues.ml @@ -0,0 +1,525 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Sorts +open Cbytecodes + +(*******************************************) +(* Initalization of the abstract machine ***) +(* Necessary for [relaccu_tbl] *) +(*******************************************) + +external init_vm : unit -> unit = "init_coq_vm" + +let _ = init_vm () + +(******************************************************) +(* Abstract data types and utility functions **********) +(******************************************************) + +(* Values of the abstract machine *) +type values +let val_of_obj v = ((Obj.obj v):values) +let crazy_val = (val_of_obj (Obj.repr 0)) + +(* Abstract data *) +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments + +let fun_val v = (Obj.magic v : values) +let fix_val v = (Obj.magic v : values) +let cofix_upd_val v = (Obj.magic v : values) + +type vm_env +let fun_env v = (Obj.magic v : vm_env) +let fix_env v = (Obj.magic v : vm_env) +let cofix_env v = (Obj.magic v : vm_env) +let cofix_upd_env v = (Obj.magic v : vm_env) +type vstack = values array + +let fun_of_val v = (Obj.magic v : vfun) + +(*******************************************) +(* Machine code *** ************************) +(*******************************************) + +type tcode + +external mkAccuCode : int -> tcode = "coq_makeaccu" +external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" + +let tcode_of_obj v = ((Obj.obj v):tcode) +let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) +let fix_code v = fun_code v +let cofix_upd_code v = fun_code v + + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +(* Representation of values *) +(* + Products : *) +(* - vprod = 0_[ dom | codom] *) +(* dom : values, codom : vfun *) +(* *) +(* + Functions have two representations : *) +(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *) +(* C:tcode, fvi : values *) +(* Remark : a function and its environment is the same value. *) +(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *) +(* *) +(* + Fixpoints : *) +(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *) +(* One single block to represent all of the fixpoints, each fixpoint *) +(* is the pointer to the field holding the pointer to its code, and *) +(* the infix tag is used to know where the block starts. *) +(* - Partial application follows the scheme of partially applied *) +(* functions. Note: only fixpoints not having been applied to its *) +(* recursive argument are coded this way. When the rec. arg. is *) +(* applied, either it's a constructor and the fix reduces, or it's *) +(* and the fix is coded as an accumulator. *) +(* *) +(* + Cofixpoints : see cbytegen.ml *) +(* *) +(* + vblock's encode (non constant) constructors as in Ocaml, but *) +(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *) +(* accumulators. *) +(* *) +(* + vm_env is the type of the machine environments (i.e. a function or *) +(* a fixpoint) *) +(* *) +(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *) +(* - representation of [accu] : tag_[....] *) +(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *) +(* -- 10_[accu|proj name] : a projection blocked by an accu *) +(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *) +(* -- 12_[accu|vswitch] : a match blocked by an accu *) +(* -- 13_[fcofix] : a cofix function *) +(* -- 14_[fcofix|val] : a cofix function, val represent the value *) +(* of the function applied to arg1 ... argn *) +(* The [arguments] type, which is abstracted as an array, represents : *) +(* tag[ _ | _ |v1|... | vn] *) +(* Generally the first field is a code pointer. *) + +(* Do not edit this type without editing C code, especially "coq_values.h" *) + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(* Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix*arguments (* Possibly empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type to_update = values + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(* Functions over arguments *) +let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2 +let arg args i = + if 0 <= i && i < (nargs args) then + val_of_obj (Obj.field (Obj.repr args) (i+2)) + else invalid_arg + ("Vm.arg size = "^(string_of_int (nargs args))^ + " acces "^(string_of_int i)) + +(*************************************************) +(* Destructors ***********************************) +(*************************************************) + +let uni_lvl_val (v : values) : Univ.Level.t = + let whd = Obj.magic v in + match whd with + | Vuniv_level lvl -> lvl + | _ -> + let pr = + let open Pp in + match whd with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk" + | _ -> assert false + in + CErrors.anomaly + Pp.( strbrk "Parsing virtual machine value expected universe level, got " + ++ pr ++ str ".") + +let rec whd_accu a stk = + let stk = + if Int.equal (Obj.size a) 2 then stk + else Zapp (Obj.obj a) :: stk in + let at = Obj.field a 1 in + match Obj.tag at with + | i when Int.equal i type_atom_tag -> + begin match stk with + | [Zapp args] -> + let u = ref (Obj.obj (Obj.field at 0)) in + for i = 0 to nargs args - 1 do + u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i))) + done; + Vsort (Type !u) + | _ -> assert false + end + | i when i <= max_atom_tag -> + Vatom_stk(Obj.magic at, stk) + | i when Int.equal i proj_tag -> + let zproj = Zproj (Obj.obj (Obj.field at 0)) in + whd_accu (Obj.field at 1) (zproj :: stk) + | i when Int.equal i fix_app_tag -> + let fa = Obj.field at 1 in + let zfix = + Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in + whd_accu (Obj.field at 0) (zfix :: stk) + | i when Int.equal i switch_tag -> + let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in + whd_accu (Obj.field at 0) (zswitch :: stk) + | i when Int.equal i cofix_tag -> + let vcfx = Obj.obj (Obj.field at 0) in + let to_up = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcfx, to_up, None) + | [Zapp args] -> Vcofix(vcfx, to_up, Some args) + | _ -> assert false + end + | i when Int.equal i cofix_evaluated_tag -> + let vcofix = Obj.obj (Obj.field at 0) in + let res = Obj.obj a in + begin match stk with + | [] -> Vcofix(vcofix, res, None) + | [Zapp args] -> Vcofix(vcofix, res, Some args) + | _ -> assert false + end + | tg -> + CErrors.anomaly + Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") + +external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" +external is_accumulate : tcode -> bool = "coq_is_accumulate_code" +external int_tcode : tcode -> int -> int = "coq_int_tcode" +external accumulate : unit -> tcode = "accumulate_code" +let accumulate = accumulate () + +let whd_val : values -> whd = + fun v -> + let o = Obj.repr v in + if Obj.is_int o then Vconstr_const (Obj.obj o) + else + let tag = Obj.tag o in + if tag = accu_tag then + ( + if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) + else + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o)) + else + if tag = Obj.closure_tag || tag = Obj.infix_tag then + (match kind_of_closure o with + | 0 -> Vfun(Obj.obj o) + | 1 -> Vfix(Obj.obj o, None) + | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) + | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) + | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work.")) + else + Vconstr_block(Obj.obj o) + +(**********************************************) +(* Constructors *******************************) +(**********************************************) + +let obj_of_atom : atom -> Obj.t = + fun a -> + let res = Obj.new_block accu_tag 2 in + Obj.set_field res 0 (Obj.repr accumulate); + Obj.set_field res 1 (Obj.repr a); + res + +(* obj_of_str_const : structured_constant -> Obj.t *) +let rec obj_of_str_const str = + match str with + | Const_sorts s -> Obj.repr (Vsort s) + | Const_ind ind -> obj_of_atom (Aind ind) + | Const_proj p -> Obj.repr p + | Const_b0 tag -> Obj.repr tag + | Const_bn(tag, args) -> + let len = Array.length args in + let res = Obj.new_block tag len in + for i = 0 to len - 1 do + Obj.set_field res i (obj_of_str_const args.(i)) + done; + res + | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_type u -> obj_of_atom (Atype u) + +let val_of_obj o = ((Obj.obj o) : values) + +let val_of_str_const str = val_of_obj (obj_of_str_const str) + +let val_of_atom a = val_of_obj (obj_of_atom a) + +let atom_of_proj kn v = + let r = Obj.new_block proj_tag 2 in + Obj.set_field r 0 (Obj.repr kn); + Obj.set_field r 1 (Obj.repr v); + ((Obj.obj r) : atom) + +let val_of_proj kn v = + val_of_atom (atom_of_proj kn v) + +module IdKeyHash = +struct + type t = Constant.t tableKey + let equal = Names.eq_table_key Constant.equal + open Hashset.Combine + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) +end + +module KeyTable = Hashtbl.Make(IdKeyHash) + +let idkey_tbl = KeyTable.create 31 + +let val_of_idkey key = + try KeyTable.find idkey_tbl key + with Not_found -> + let v = val_of_atom (Aid key) in + KeyTable.add idkey_tbl key v; + v + +let val_of_rel k = val_of_idkey (RelKey k) + +let val_of_named id = val_of_idkey (VarKey id) + +let val_of_constant c = val_of_idkey (ConstKey c) + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(*************************************************) +(** Operations manipulating data types ***********) +(*************************************************) + +(* Functions over products *) + +let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) +let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1)) + +(* Functions over vfun *) + +external closure_arity : vfun -> int = "coq_closure_arity" + +(* Functions over fixpoint *) + +external offset : Obj.t -> int = "coq_offset" +external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" + +let first o = (offset_closure o (offset o)) +let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) + +let last o = (Obj.field o (Obj.size o - 1)) +let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) + +let current_fix vf = - (offset (Obj.repr vf) / 2) + +let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) + +let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 + +let rec_args vf = + let fb = first (Obj.repr vf) in + let size = Obj.size (last fb) in + Array.init size (unsafe_rec_arg fb) + +exception FALSE + +let check_fix f1 f2 = + let i1, i2 = current_fix f1, current_fix f2 in + (* Checking starting point *) + if i1 = i2 then + let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in + let n = Obj.size (last fb1) in + (* Checking number of definitions *) + if n = Obj.size (last fb2) then + (* Checking recursive arguments *) + try + for i = 0 to n - 1 do + if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i + then raise FALSE + done; + true + with FALSE -> false + else false + else false + +external atom_rel : unit -> atom array = "get_coq_atom_tbl" +external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" + +let relaccu_tbl = + let atom_rel = atom_rel() in + let len = Array.length atom_rel in + for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + ref (Array.init len mkAccuCode) + +let relaccu_code i = + let len = Array.length !relaccu_tbl in + if i < len then !relaccu_tbl.(i) + else + begin + realloc_atom_rel i; + let atom_rel = atom_rel () in + let nl = Array.length atom_rel in + for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + relaccu_tbl := + Array.init nl + (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); + !relaccu_tbl.(i) + end + +let mk_fix_body k ndef fb = + let e = Obj.dup (Obj.repr fb) in + for i = 0 to ndef - 1 do + Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + done; + let fix_body i = + let jump_grabrec c = offset_tcode c 2 in + let c = jump_grabrec (unsafe_fb_code fb i) in + let res = Obj.new_block Obj.closure_tag 2 in + Obj.set_field res 0 (Obj.repr c); + Obj.set_field res 1 (offset_closure e (2*i)); + ((Obj.obj res) : vfun) in + Array.init ndef fix_body + +(* Functions over vcofix *) + +let get_fcofix vcf i = + match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with + | Vcofix(vcfi, _, _) -> vcfi + | _ -> assert false + +let current_cofix vcf = + let ndef = Obj.size (last (Obj.repr vcf)) in + let rec find_cofix pos = + if pos < ndef then + if get_fcofix vcf pos == vcf then pos + else find_cofix (pos+1) + else raise Not_found in + try find_cofix 0 + with Not_found -> assert false + +let check_cofix vcf1 vcf2 = + (current_cofix vcf1 = current_cofix vcf2) && + (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) + +let mk_cofix_body apply_varray k ndef vcf = + let e = Obj.dup (Obj.repr vcf) in + for i = 0 to ndef - 1 do + Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i))) + done; + + let cofix_body i = + let vcfi = get_fcofix vcf i in + let c = Obj.field (Obj.repr vcfi) 0 in + Obj.set_field e 0 c; + let atom = Obj.new_block cofix_tag 1 in + let self = Obj.new_block accu_tag 2 in + Obj.set_field self 0 (Obj.repr accumulate); + Obj.set_field self 1 (Obj.repr atom); + apply_varray (Obj.obj e) [|Obj.obj self|] in + Array.init ndef cofix_body + +(* Functions over vblock *) + +let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b) +let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b) +let bfield b i = + if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i) + else invalid_arg "Vm.bfield" + + +(* Functions over vswitch *) + +let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl + +let branch_arg k (tag,arity) = + if Int.equal arity 0 then ((Obj.magic tag):values) + else + let b, ofs = + if tag < last_variant_tag then Obj.new_block tag arity, 0 + else + let b = Obj.new_block last_variant_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + b,1 in + for i = ofs to ofs + arity - 1 do + Obj.set_field b i (Obj.repr (val_of_rel (k+i))) + done; + val_of_obj b + +(* Printing *) + +let rec pr_atom a = + Pp.(match a with + | Aid c -> str "Aid(" ++ (match c with + | ConstKey c -> Constant.print c + | RelKey i -> str "#" ++ int i + | _ -> str "...") ++ str ")" + | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" + | Atype _ -> str "Atype(") +and pr_whd w = + Pp.(match w with + | Vsort _ -> str "Vsort" + | Vprod _ -> str "Vprod" + | Vfun _ -> str "Vfun" + | Vfix _ -> str "Vfix" + | Vcofix _ -> str "Vcofix" + | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" + | Vconstr_block b -> str "Vconstr_block" + | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" + | Vuniv_level _ -> assert false) +and pr_stack stk = + Pp.(match stk with + | [] -> str "[]" + | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk) +and pr_zipper z = + Pp.(match z with + | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" + | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch s -> str "Zswitch(...)" + | Zproj c -> str "Zproj(" ++ Constant.print c ++ str ")") diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli new file mode 100644 index 0000000000..350f71372f --- /dev/null +++ b/kernel/vmvalues.mli @@ -0,0 +1,144 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Cbytecodes + +(** Values *) + +type values +type vm_env +type vprod +type vfun +type vfix +type vcofix +type vblock +type arguments +type vstack = values array +type to_update + +val fun_val : vfun -> values +val fix_val : vfix -> values +val cofix_upd_val : to_update -> values + +val fun_env : vfun -> vm_env +val fix_env : vfix -> vm_env +val cofix_env : vcofix -> vm_env +val cofix_upd_env : to_update -> vm_env + +(** Cast a value known to be a function, unsafe in general *) +val fun_of_val : values -> vfun + +val crazy_val : values + +(** Machine code *) + +type tcode + +type vswitch = { + sw_type_code : tcode; + sw_code : tcode; + sw_annot : annot_switch; + sw_stk : vstack; + sw_env : vm_env + } + +external mkAccuCode : int -> tcode = "coq_makeaccu" + +val fun_code : vfun -> tcode +val fix_code : vfix -> tcode +val cofix_upd_code : to_update -> tcode + +type atom = + | Aid of Vars.id_key + | Aind of inductive + | Atype of Univ.Universe.t + +(** Zippers *) + +type zipper = + | Zapp of arguments + | Zfix of vfix * arguments (** might be empty *) + | Zswitch of vswitch + | Zproj of Constant.t (* name of the projection *) + +type stack = zipper list + +type whd = + | Vsort of Sorts.t + | Vprod of vprod + | Vfun of vfun + | Vfix of vfix * arguments option + | Vcofix of vcofix * to_update * arguments option + | Vconstr_const of int + | Vconstr_block of vblock + | Vatom_stk of atom * stack + | Vuniv_level of Univ.Level.t + +(** For debugging purposes only *) + +val pr_atom : atom -> Pp.t +val pr_whd : whd -> Pp.t +val pr_stack : stack -> Pp.t + +(** Constructors *) + +val val_of_str_const : structured_constant -> values +val val_of_rel : int -> values +val val_of_named : Id.t -> values +val val_of_constant : Constant.t -> values +val val_of_proj : Constant.t -> values -> values +val val_of_atom : atom -> values + +external val_of_annot_switch : annot_switch -> values = "%identity" + +(** Destructors *) + +val whd_val : values -> whd +val uni_lvl_val : values -> Univ.Level.t + +(** Arguments *) + +val nargs : arguments -> int +val arg : arguments -> int -> values + +(** Product *) + +val dom : vprod -> values +val codom : vprod -> vfun + +(** Fun *) +external closure_arity : vfun -> int = "coq_closure_arity" + +(** Fix *) + +val current_fix : vfix -> int +val check_fix : vfix -> vfix -> bool +val rec_args : vfix -> int array +val first_fix : vfix -> vfix +val fix_types : vfix -> tcode array +val cofix_types : vcofix -> tcode array +external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +val mk_fix_body : int -> int -> vfix -> vfun array + +(** CoFix *) + +val current_cofix : vcofix -> int +val check_cofix : vcofix -> vcofix -> bool +val mk_cofix_body : (vfun -> vstack -> values) -> int -> int -> vcofix -> values array + +(** Block *) + +val btag : vblock -> int +val bsize : vblock -> int +val bfield : vblock -> int -> values + +(** Switch *) + +val check_switch : vswitch -> vswitch -> bool +val branch_arg : int -> Cbytecodes.tag * int -> values |