aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml21
-rw-r--r--kernel/declarations.mli15
-rw-r--r--kernel/entries.mli5
-rw-r--r--kernel/indtypes.ml3
-rw-r--r--kernel/kernel.mllib6
-rw-r--r--kernel/nativecode.ml1496
-rw-r--r--kernel/nativecode.mli66
-rw-r--r--kernel/nativeconv.ml153
-rw-r--r--kernel/nativeconv.mli15
-rw-r--r--kernel/nativelambda.ml676
-rw-r--r--kernel/nativelambda.mli55
-rw-r--r--kernel/nativelib.ml91
-rw-r--r--kernel/nativelib.mli34
-rw-r--r--kernel/nativelibrary.ml63
-rw-r--r--kernel/nativelibrary.mli20
-rw-r--r--kernel/nativevalues.ml259
-rw-r--r--kernel/nativevalues.mli102
-rw-r--r--kernel/reduction.ml10
-rw-r--r--kernel/reduction.mli3
-rw-r--r--kernel/safe_typing.ml20
-rw-r--r--kernel/safe_typing.mli6
-rw-r--r--kernel/term.ml4
-rw-r--r--kernel/term.mli4
-rw-r--r--kernel/term_typing.ml14
-rw-r--r--kernel/term_typing.mli4
-rw-r--r--kernel/typeops.ml6
28 files changed, 3126 insertions, 29 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 2f031c11a0..6c22db3a2c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -151,4 +151,4 @@ let cook_constant env r =
let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
- (body, typ, cb.const_constraints, const_hyps)
+ (body, typ, cb.const_constraints, cb.const_inline_code, const_hyps)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 7adb00da61..03acb87a91 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -23,7 +23,7 @@ type recipe = {
val cook_constant :
env -> recipe ->
- constant_def * constant_type * constraints * Sign.section_context
+ constant_def * constant_type * constraints * bool * Sign.section_context
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index bc721dce34..62a3170f22 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -83,12 +83,20 @@ type constant_def =
| Def of constr_substituted
| OpaqueDef of lazy_constr
+type native_name =
+ | Linked of string
+ | LinkedLazy of string
+ | LinkedInteractive of string
+ | NotLinked
+
type constant_body = {
const_hyps : section_context; (* New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : Cemitcodes.to_patch_substituted;
- const_constraints : constraints }
+ const_constraints : constraints;
+ const_native_name : native_name ref;
+ const_inline_code : bool }
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
@@ -131,7 +139,9 @@ let subst_const_body sub cb = {
const_body = subst_const_def sub cb.const_body;
const_type = subst_const_type sub cb.const_type;
const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
- const_constraints = cb.const_constraints}
+ const_constraints = cb.const_constraints;
+ const_native_name = ref NotLinked;
+ const_inline_code = cb.const_inline_code }
(* Hash-consing of [constant_body] *)
@@ -317,6 +327,10 @@ type mutual_inductive_body = {
(* Universes constraints enforced by the inductive declaration *)
mind_constraints : constraints;
+ (* Data for native compilation *)
+ (* Status of the code (linked or not, and where) *)
+ mind_native_name : native_name ref;
+
}
let subst_indarity sub = function
@@ -353,7 +367,8 @@ let subst_mind sub mib =
mind_params_ctxt =
map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
- mind_constraints = mib.mind_constraints }
+ mind_constraints = mib.mind_constraints;
+ mind_native_name = ref NotLinked }
let hcons_indarity = function
| Monomorphic a ->
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2595aae07c..5b5e1750c1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -62,12 +62,20 @@ type constant_def =
| Def of constr_substituted
| OpaqueDef of lazy_constr
+type native_name =
+ | Linked of string
+ | LinkedLazy of string
+ | LinkedInteractive of string
+ | NotLinked
+
type constant_body = {
const_hyps : section_context; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : to_patch_substituted;
- const_constraints : constraints }
+ const_constraints : constraints;
+ const_native_name : native_name ref;
+ const_inline_code : bool }
val subst_const_def : substitution -> constant_def -> constant_def
val subst_const_body : substitution -> constant_body -> constant_body
@@ -181,6 +189,11 @@ type mutual_inductive_body = {
mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *)
+(** {8 Data for native compilation } *)
+
+ mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
+
+
}
val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/entries.mli b/kernel/entries.mli
index a32892a418..20742d3419 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -53,8 +53,9 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
const_entry_secctx : section_context option;
- const_entry_type : types option;
- const_entry_opaque : bool }
+ const_entry_type : types option;
+ const_entry_opaque : bool;
+ const_entry_inline_code : bool }
type inline = int option (* inlining level, None for no inlining *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ffd588e57d..165af63cff 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -668,7 +668,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
mind_nparams_rec = nmr;
mind_params_ctxt = params;
mind_packets = packets;
- mind_constraints = cst
+ mind_constraints = cst;
+ mind_native_name = ref NotLinked
}
(************************************************************************)
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 872a6c9054..07f24583e1 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -7,14 +7,19 @@ Sign
Cbytecodes
Copcodes
Cemitcodes
+Nativevalues
Declarations
Retroknowledge
Pre_env
Cbytegen
+Nativelambda
+Nativecode
+Nativelib
Environ
Conv_oracle
Closure
Reduction
+Nativeconv
Type_errors
Modops
Inductive
@@ -24,6 +29,7 @@ Cooking
Term_typing
Subtyping
Mod_typing
+Nativelibrary
Safe_typing
Vm
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
new file mode 100644
index 0000000000..d156afc268
--- /dev/null
+++ b/kernel/nativecode.ml
@@ -0,0 +1,1496 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Errors
+open Term
+open Names
+open Declarations
+open Util
+open Nativevalues
+open Nativelambda
+open Pre_env
+open Sign
+
+(** This file defines the mllambda code generation phase of the native
+compiler. mllambda represents a fragment of ML, and can easily be printed
+to OCaml code. *)
+
+(** Local names {{{**)
+
+type lname = { lname : name; luid : int }
+
+let dummy_lname = { lname = Anonymous; luid = -1 }
+
+module LNord =
+ struct
+ type t = lname
+ let compare l1 l2 = l1.luid - l2.luid
+ end
+module LNmap = Map.Make(LNord)
+module LNset = Set.Make(LNord)
+
+let lname_ctr = ref (-1)
+
+let reset_lname = lname_ctr := -1
+
+let fresh_lname n =
+ incr lname_ctr;
+ { lname = n; luid = !lname_ctr }
+ (**}}}**)
+
+(** Global names {{{ **)
+type gname =
+ | Gind of string * inductive (* prefix, inductive name *)
+ | Gconstruct of string * constructor (* prefix, constructor name *)
+ | Gconstant of string * constant (* prefix, constant name *)
+ | Gcase of label option * int
+ | Gpred of label option * int
+ | Gfixtype of label option * int
+ | Gnorm of label option * int
+ | Gnormtbl of label option * int
+ | Ginternal of string
+ | Grel of int
+ | Gnamed of identifier
+
+let case_ctr = ref (-1)
+
+let reset_gcase () = case_ctr := -1
+
+let fresh_gcase l =
+ incr case_ctr;
+ Gcase (l,!case_ctr)
+
+let pred_ctr = ref (-1)
+
+let reset_gpred () = pred_ctr := -1
+
+let fresh_gpred l =
+ incr pred_ctr;
+ Gpred (l,!pred_ctr)
+
+let fixtype_ctr = ref (-1)
+
+let reset_gfixtype () = fixtype_ctr := -1
+
+let fresh_gfixtype l =
+ incr fixtype_ctr;
+ Gfixtype (l,!fixtype_ctr)
+
+let norm_ctr = ref (-1)
+
+let reset_norm () = norm_ctr := -1
+
+let fresh_gnorm l =
+ incr norm_ctr;
+ Gnorm (l,!norm_ctr)
+
+let normtbl_ctr = ref (-1)
+
+let reset_normtbl () = normtbl_ctr := -1
+
+let fresh_gnormtbl l =
+ incr normtbl_ctr;
+ Gnormtbl (l,!normtbl_ctr)
+ (**}}}**)
+
+(** Symbols (pre-computed values) {{{**)
+
+let val_ctr = ref (-1)
+
+type symbol =
+ | SymbValue of Nativevalues.t
+ | SymbSort of sorts
+ | SymbName of name
+ | SymbConst of constant
+ | SymbMatch of annot_sw
+ | SymbInd of inductive
+
+let get_value tbl i =
+ match tbl.(i) with
+ | SymbValue v -> v
+ | _ -> anomaly "get_value failed"
+
+let get_sort tbl i =
+ match tbl.(i) with
+ | SymbSort s -> s
+ | _ -> anomaly "get_sort failed"
+
+let get_name tbl i =
+ match tbl.(i) with
+ | SymbName id -> id
+ | _ -> anomaly "get_name failed"
+
+let get_const tbl i =
+ match tbl.(i) with
+ | SymbConst kn -> kn
+ | _ -> anomaly "get_const failed"
+
+let get_match tbl i =
+ match tbl.(i) with
+ | SymbMatch case_info -> case_info
+ | _ -> anomaly "get_match failed"
+
+let get_ind tbl i =
+ match tbl.(i) with
+ | SymbInd ind -> ind
+ | _ -> anomaly "get_ind failed"
+
+let symbols_list = ref ([] : symbol list)
+
+let reset_symbols_list l =
+ symbols_list := l;
+ val_ctr := List.length l - 1
+
+let push_symbol x =
+ incr val_ctr;
+ symbols_list := x :: !symbols_list;
+ !val_ctr
+
+let symbols_tbl_name = Ginternal "symbols_tbl"
+
+let get_symbols_tbl () = Array.of_list (List.rev !symbols_list)
+(**}}}**)
+
+(** Lambda to Mllambda {{{**)
+
+type primitive =
+ | Mk_prod
+ | Mk_sort
+ | Mk_ind
+ | Mk_const
+ | Mk_sw
+ | Mk_fix of rec_pos * int
+ | Mk_cofix of int
+ | Mk_rel of int
+ | Mk_var of identifier
+ | Is_accu
+ | Is_int
+ | Is_array
+ | Cast_accu
+ | Upd_cofix
+ | Force_cofix
+ | Val_to_int
+ | Val_of_int
+ | Val_of_bool
+ (* Coq primitive with check *)
+ | Chead0 of (string * constant) option
+ | Ctail0 of (string * constant) option
+ | Cadd of (string * constant) option
+ | Csub of (string * constant) option
+ | Cmul of (string * constant) option
+ | Cdiv of (string * constant) option
+ | Crem of (string * constant) option
+ | Clsr of (string * constant) option
+ | Clsl of (string * constant) option
+ | Cand of (string * constant) option
+ | Cor of (string * constant) option
+ | Cxor of (string * constant) option
+ | Caddc of (string * constant) option
+ | Csubc of (string * constant) option
+ | CaddCarryC of (string * constant) option
+ | CsubCarryC of (string * constant) option
+ | Cmulc of (string * constant) option
+ | Cdiveucl of (string * constant) option
+ | Cdiv21 of (string * constant) option
+ | CaddMulDiv of (string * constant) option
+ | Ceq of (string * constant) option
+ | Clt of (string * constant) option
+ | Cle of (string * constant) option
+ | Clt_b
+ | Cle_b
+ | Ccompare of (string * constant) option
+ | Cprint of (string * constant) option
+ | Carraymake of (string * constant) option
+ | Carrayget of (string * constant) option
+ | Carraydefault of (string * constant) option
+ | Carrayset of (string * constant) option
+ | Carraycopy of (string * constant) option
+ | Carrayreroot of (string * constant) option
+ | Carraylength of (string * constant) option
+ | Carrayinit of (string * constant) option
+ | Carraymap of (string * constant) option
+ (* Caml primitive *)
+ | MLand
+ | MLle
+ | MLlt
+ | MLinteq
+ | MLlsl
+ | MLlsr
+ | MLland
+ | MLlor
+ | MLlxor
+ | MLadd
+ | MLsub
+ | MLmul
+ | MLmagic
+
+type mllambda =
+ | MLlocal of lname
+ | MLglobal of gname
+ | MLprimitive of primitive
+ | MLlam of lname array * mllambda
+ | MLletrec of (lname * lname array * mllambda) array * mllambda
+ | MLlet of lname * mllambda * mllambda
+ | MLapp of mllambda * mllambda array
+ | MLif of mllambda * mllambda * mllambda
+ | MLmatch of annot_sw * mllambda * mllambda * mllam_branches
+ (* argument, prefix, accu branch, branches *)
+ | MLconstruct of string * constructor * mllambda array
+ (* prefix, constructor name, arguments *)
+ | MLint of bool * int (* true if the type sould be int *)
+ | MLparray of mllambda array
+ | MLsetref of string * mllambda
+ | MLsequence of mllambda * mllambda
+
+and mllam_branches = ((constructor * lname option array) list * mllambda) array
+
+let fv_lam l =
+ let rec aux l bind fv =
+ match l with
+ | MLlocal l ->
+ if LNset.mem l bind then fv else LNset.add l fv
+ | MLglobal _ | MLprimitive _ | MLint _ -> fv
+ | MLlam (ln,body) ->
+ let bind = Array.fold_right LNset.add ln bind in
+ aux body bind fv
+ | MLletrec(bodies,def) ->
+ let bind =
+ Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in
+ let fv_body (_,ln,body) fv =
+ let bind = Array.fold_right LNset.add ln bind in
+ aux body bind fv in
+ Array.fold_right fv_body bodies (aux def bind fv)
+ | MLlet(l,def,body) ->
+ aux body (LNset.add l bind) (aux def bind fv)
+ | MLapp(f,args) ->
+ let fv_arg arg fv = aux arg bind fv in
+ Array.fold_right fv_arg args (aux f bind fv)
+ | MLif(t,b1,b2) ->
+ aux t bind (aux b1 bind (aux b2 bind fv))
+ | MLmatch(_,a,p,bs) ->
+ let fv = aux a bind (aux p bind fv) in
+ let fv_bs (cargs, body) fv =
+ let bind =
+ List.fold_right (fun (_,args) bind ->
+ Array.fold_right
+ (fun o bind -> match o with
+ | Some l -> LNset.add l bind
+ | _ -> bind) args bind)
+ cargs bind in
+ aux body bind fv in
+ Array.fold_right fv_bs bs fv
+ (* argument, accu branch, branches *)
+ | MLconstruct (_,_,p) | MLparray p ->
+ Array.fold_right (fun a fv -> aux a bind fv) p fv
+ | MLsetref(_,l) -> aux l bind fv
+ | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) in
+ aux l LNset.empty LNset.empty
+
+
+let mkMLlam params body =
+ if Array.length params = 0 then body
+ else
+ match body with
+ | MLlam (params', body) -> MLlam(Array.append params params', body)
+ | _ -> MLlam(params,body)
+
+let mkMLapp f args =
+ if Array.length args = 0 then f
+ else
+ match f with
+ | MLapp(f,args') -> MLapp(f,Array.append args' args)
+ | _ -> MLapp(f,args)
+
+let empty_params = [||]
+
+let decompose_MLlam c =
+ match c with
+ | MLlam(ids,c) -> ids,c
+ | _ -> empty_params,c
+
+(*s Global declaration *)
+type global =
+(* | Gtblname of gname * identifier array *)
+ | Gtblnorm of gname * lname array * mllambda array
+ | Gtblfixtype of gname * lname array * mllambda array
+ | Glet of gname * mllambda
+ | Gletcase of
+ gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
+ | Gopen of string
+ | Gtype of inductive * int array
+ (* ind name, arities of constructors *)
+
+let global_stack = ref ([] : global list)
+
+let push_global_let gn body =
+ global_stack := Glet(gn,body) :: !global_stack
+
+let push_global_fixtype gn params body =
+ global_stack := Gtblfixtype(gn,params,body) :: !global_stack
+
+let push_global_norm name params body =
+ global_stack := Gtblnorm(name, params, body)::!global_stack
+
+let push_global_case name params annot a accu bs =
+ global_stack := Gletcase(name,params, annot, a, accu, bs)::!global_stack
+
+(*s Compilation environment *)
+
+type env =
+ { env_rel : mllambda list; (* (MLlocal lname) list *)
+ env_bound : int; (* length of env_rel *)
+ (* free variables *)
+ env_urel : (int * mllambda) list ref; (* list of unbound rel *)
+ env_named : (identifier * mllambda) list ref }
+
+let empty_env () =
+ { env_rel = [];
+ env_bound = 0;
+ env_urel = ref [];
+ env_named = ref []
+ }
+
+let push_rel env id =
+ let local = fresh_lname id in
+ local, { env with
+ env_rel = MLlocal local :: env.env_rel;
+ env_bound = env.env_bound + 1
+ }
+
+let push_rels env ids =
+ let lnames, env_rel =
+ Array.fold_left (fun (names,env_rel) id ->
+ let local = fresh_lname id in
+ (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in
+ Array.of_list (List.rev lnames), { env with
+ env_rel = env_rel;
+ env_bound = env.env_bound + Array.length ids
+ }
+
+let get_rel env id i =
+ if i <= env.env_bound then
+ List.nth env.env_rel (i-1)
+ else
+ let i = i - env.env_bound in
+ try List.assoc i !(env.env_urel)
+ with Not_found ->
+ let local = MLlocal (fresh_lname id) in
+ env.env_urel := (i,local) :: !(env.env_urel);
+ local
+
+let get_var env id =
+ try List.assoc id !(env.env_named)
+ with Not_found ->
+ let local = MLlocal (fresh_lname (Name id)) in
+ env.env_named := (id, local)::!(env.env_named);
+ local
+
+(*s Traduction of lambda to mllambda *)
+
+let get_prod_name codom =
+ match codom with
+ | MLlam(ids,_) -> ids.(0).lname
+ | _ -> assert false
+
+let get_lname (_,l) =
+ match l with
+ | MLlocal id -> id
+ | _ -> raise (Invalid_argument "Nativecode.get_lname")
+
+let fv_params env =
+ let fvn, fvr = !(env.env_named), !(env.env_urel) in
+ let size = List.length fvn + List.length fvr in
+ if size = 0 then empty_params
+ else begin
+ let params = Array.make size dummy_lname in
+ let fvn = ref fvn in
+ let i = ref 0 in
+ while !fvn <> [] do
+ params.(!i) <- get_lname (List.hd !fvn);
+ fvn := List.tl !fvn;
+ incr i
+ done;
+ let fvr = ref fvr in
+ while !fvr <> [] do
+ params.(!i) <- get_lname (List.hd !fvr);
+ fvr := List.tl !fvr;
+ incr i
+ done;
+ params
+ end
+
+let generalize_fv env body =
+ mkMLlam (fv_params env) body
+
+let empty_args = [||]
+
+let fv_args env fvn fvr =
+ let size = List.length fvn + List.length fvr in
+ if size = 0 then empty_args
+ else
+ begin
+ let args = Array.make size (MLint (false,0)) in
+ let fvn = ref fvn in
+ let i = ref 0 in
+ while !fvn <> [] do
+ args.(!i) <- get_var env (fst (List.hd !fvn));
+ fvn := List.tl !fvn;
+ incr i
+ done;
+ let fvr = ref fvr in
+ while !fvr <> [] do
+ let (k,_ as kml) = List.hd !fvr in
+ let n = get_lname kml in
+ args.(!i) <- get_rel env n.lname k;
+ fvr := List.tl !fvr;
+ incr i
+ done;
+ args
+ end
+
+let get_value_code i =
+ MLapp (MLglobal (Ginternal "get_value"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_sort_code i =
+ MLapp (MLglobal (Ginternal "get_sort"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_name_code i =
+ MLapp (MLglobal (Ginternal "get_name"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_const_code i =
+ MLapp (MLglobal (Ginternal "get_const"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_match_code i =
+ MLapp (MLglobal (Ginternal "get_match"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+let get_ind_code i =
+ MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|])
+
+type rlist =
+ | Rnil
+ | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist'
+and rlist' = rlist ref
+
+let rm_params fv params =
+ Array.map (fun l -> if LNset.mem l fv then Some l else None) params
+
+let rec insert cargs body rl =
+ match !rl with
+ | Rnil ->
+ let fv = fv_lam body in
+ let (c,params) = cargs in
+ let params = rm_params fv params in
+ rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
+ | Rcons(l,fv,body',rl) ->
+ if body = body' then
+ let (c,params) = cargs in
+ let params = rm_params fv params in
+ l := (c,params)::!l
+ else insert cargs body rl
+
+let rec to_list rl =
+ match !rl with
+ | Rnil -> []
+ | Rcons(l,_,body,tl) -> (!l,body)::to_list tl
+
+let merge_branches t =
+ let newt = ref Rnil in
+ Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
+ Array.of_list (to_list newt)
+
+ let rec ml_of_lam env l t =
+ match t with
+ | Lrel(id ,i) -> get_rel env id i
+ | Lvar id -> get_var env id
+ | Lprod(dom,codom) ->
+ let dom = ml_of_lam env l dom in
+ let codom = ml_of_lam env l codom in
+ let n = get_prod_name codom in
+ let i = push_symbol (SymbName n) in
+ MLapp(MLprimitive Mk_prod, [|get_name_code i;dom;codom|])
+ | Llam(ids,body) ->
+ let lnames,env = push_rels env ids in
+ MLlam(lnames, ml_of_lam env l body)
+ | Lrec(id,body) ->
+ let ids,body = decompose_Llam body in
+ let lname, env = push_rel env id in
+ let lnames, env = push_rels env ids in
+ MLletrec([|lname, lnames, ml_of_lam env l body|], MLlocal lname)
+ | Llet(id,def,body) ->
+ let def = ml_of_lam env l def in
+ let lname, env = push_rel env id in
+ let body = ml_of_lam env l body in
+ MLlet(lname,def,body)
+ | Lapp(f,args) ->
+ MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args)
+ | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c))
+ | Lcase (annot,p,a,bs) ->
+ (* let predicate_uid fv_pred = compilation of p
+ let rec case_uid fv a_uid =
+ match a_uid with
+ | Accu _ => mk_sw (predicate_uid fv_pred) (case_uid fv) a_uid
+ | Ci argsi => compilation of branches
+ compile case = case_uid fv (compilation of a) *)
+ (* Compilation of the predicate *)
+ (* Remark: if we do not want to compile the predicate we
+ should a least compute the fv, then store the lambda representation
+ of the predicate (not the mllambda) *)
+ let env_p = empty_env () in
+ let pn = fresh_gpred l in
+ let mlp = ml_of_lam env_p l p in
+ let mlp = generalize_fv env_p mlp in
+ let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in
+ push_global_let pn mlp;
+ (* Compilation of the case *)
+ let env_c = empty_env () in
+ let a_uid = fresh_lname Anonymous in
+ let la_uid = MLlocal a_uid in
+ (* compilation of branches *)
+ let ml_br (c,params, body) =
+ let lnames, env = push_rels env_c params in
+ (c, lnames, ml_of_lam env l body) in
+ let bs = Array.map ml_br bs in
+ let cn = fresh_gcase l in
+ (* Compilation of accu branch *)
+ let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in
+ let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in
+ let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in
+ (* remark : the call to fv_args does not add free variables in env_c *)
+ let i = push_symbol (SymbMatch annot) in
+ let accu =
+ MLapp(MLprimitive Mk_sw,
+ [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]);
+ pred;
+ cn_fv |]) in
+(* let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
+ let case = generalize_fv env_c body in *)
+ push_global_case cn
+ (Array.append (fv_params env_c) [|a_uid|]) annot la_uid accu (merge_branches bs);
+
+ (* Final result *)
+ let arg = ml_of_lam env l a in
+ let force =
+ if annot.asw_finite then arg
+ else MLapp(MLprimitive Force_cofix, [|arg|]) in
+ mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
+ | Lareint args ->
+ let res = ref (MLapp(MLprimitive Is_int, [|ml_of_lam env l args.(0)|]))in
+ for i = 1 to Array.length args - 1 do
+ let t = MLapp(MLprimitive Is_int, [|ml_of_lam env l args.(i)|]) in
+ res := MLapp(MLprimitive MLand, [|!res;t|])
+ done;
+ !res
+ | Lif(t,bt,bf) ->
+ MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
+ | Lfix ((rec_pos,start), (ids, tt, tb)) ->
+ (* let type_f fvt = [| type fix |]
+ let norm_f1 fv f1 .. fn params1 = body1
+ ..
+ let norm_fn fv f1 .. fn paramsn = bodyn
+ let norm fv f1 .. fn =
+ [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|]
+ compile fix =
+ let rec f1 params1 =
+ if is_accu rec_pos.(1) then mk_fix (type_f fvt) (norm fv) params1
+ else norm_f1 fv f1 .. fn params1
+ and .. and fn paramsn =
+ if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn
+ else norm_fn fv f1 .. fv paramsn in
+ start
+ *)
+ (* Compilation of type *)
+ let env_t = empty_env () in
+ let ml_t = Array.map (ml_of_lam env_t l) tt in
+ let params_t = fv_params env_t in
+ let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
+ let gft = fresh_gfixtype l in
+ push_global_fixtype gft params_t ml_t;
+ let mk_type = MLapp(MLglobal gft, args_t) in
+ (* Compilation of norm_i *)
+ let ndef = Array.length ids in
+ let lf,env_n = push_rels (empty_env ()) ids in
+ let t_params = Array.make ndef [||] in
+ let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
+ let ml_of_fix i body =
+ let idsi,bodyi = decompose_Llam body in
+ let paramsi, envi = push_rels env_n idsi in
+ t_norm_f.(i) <- fresh_gnorm l;
+ let bodyi = ml_of_lam envi l bodyi in
+ t_params.(i) <- paramsi;
+ mkMLlam paramsi bodyi in
+ let tnorm = Array.mapi ml_of_fix tb in
+ let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
+ let fv_params = fv_params env_n in
+ let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
+ let norm_params = Array.append fv_params lf in
+ Array.iteri (fun i body ->
+ push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm;
+ let norm = fresh_gnormtbl l in
+ push_global_norm norm fv_params
+ (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f);
+ (* Compilation of fix *)
+ let fv_args = fv_args env fvn fvr in
+ let lf, env = push_rels env ids in
+ let lf_args = Array.map (fun id -> MLlocal id) lf in
+ let mk_norm = MLapp(MLglobal norm, fv_args) in
+ let mkrec i lname =
+ let paramsi = t_params.(i) in
+ let reci = MLlocal (paramsi.(rec_pos.(i))) in
+ let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+ let body =
+ MLif(MLapp(MLprimitive Is_accu,[|reci|]),
+ mkMLapp
+ (MLapp(MLprimitive (Mk_fix(rec_pos,i)),
+ [|mk_type; mk_norm|]))
+ pargsi,
+ MLapp(MLglobal t_norm_f.(i),
+ Array.concat [fv_args;lf_args;pargsi]))
+ in
+ (lname, paramsi, body) in
+ MLletrec(Array.mapi mkrec lf, lf_args.(start))
+ | Lcofix (start, (ids, tt, tb)) ->
+ (* Compilation of type *)
+ let env_t = empty_env () in
+ let ml_t = Array.map (ml_of_lam env_t l) tt in
+ let params_t = fv_params env_t in
+ let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in
+ let gft = fresh_gfixtype l in
+ push_global_fixtype gft params_t ml_t;
+ let mk_type = MLapp(MLglobal gft, args_t) in
+ (* Compilation of norm_i *)
+ let ndef = Array.length ids in
+ let lf,env_n = push_rels (empty_env ()) ids in
+ let t_params = Array.make ndef [||] in
+ let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
+ let ml_of_fix i body =
+ let idsi,bodyi = decompose_Llam body in
+ let paramsi, envi = push_rels env_n idsi in
+ t_norm_f.(i) <- fresh_gnorm l;
+ let bodyi = ml_of_lam envi l bodyi in
+ t_params.(i) <- paramsi;
+ mkMLlam paramsi bodyi in
+ let tnorm = Array.mapi ml_of_fix tb in
+ let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in
+ let fv_params = fv_params env_n in
+ let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
+ let norm_params = Array.append fv_params lf in
+ Array.iteri (fun i body ->
+ push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm;
+ let norm = fresh_gnormtbl l in
+ push_global_norm norm fv_params
+ (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f);
+ (* Compilation of fix *)
+ let fv_args = fv_args env fvn fvr in
+ let mk_norm = MLapp(MLglobal norm, fv_args) in
+ let lnorm = fresh_lname Anonymous in
+ let ltype = fresh_lname Anonymous in
+ let lf, env = push_rels env ids in
+ let lf_args = Array.map (fun id -> MLlocal id) lf in
+ let upd i lname cont =
+ let paramsi = t_params.(i) in
+ let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+ let uniti = fresh_lname Anonymous in
+ let body =
+ MLlam(Array.append paramsi [|uniti|],
+ MLapp(MLglobal t_norm_f.(i),
+ Array.concat [fv_args;lf_args;pargsi])) in
+ MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]),
+ cont) in
+ let upd = Array.fold_right_i upd lf lf_args.(start) in
+ let mk_let i lname cont =
+ MLlet(lname,
+ MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]),
+ cont) in
+ let init = Array.fold_right_i mk_let lf upd in
+ MLlet(lnorm, mk_norm, MLlet(ltype, mk_type, init))
+ (*
+ let mkrec i lname =
+ let paramsi = t_params.(i) in
+ let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+ let uniti = fresh_lname Anonymous in
+ let body =
+ MLapp( MLprimitive(Mk_cofix i),
+ [|mk_type;mk_norm;
+ MLlam([|uniti|],
+ MLapp(MLglobal t_norm_f.(i),
+ Array.concat [fv_args;lf_args;pargsi]))|]) in
+ (lname, paramsi, body) in
+ MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
+
+ | Lmakeblock (prefix,cn,_,args) ->
+ MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args)
+ | Lconstruct (prefix, cn) ->
+ MLglobal (Gconstruct (prefix, cn))
+ | Lval v ->
+ let i = push_symbol (SymbValue v) in get_value_code i
+ | Lsort s ->
+ let i = push_symbol (SymbSort s) in
+ MLapp(MLprimitive Mk_sort, [|get_sort_code i|])
+ | Lind (prefix, ind) -> MLglobal (Gind (prefix, ind))
+ | Llazy -> MLglobal (Ginternal "lazy")
+ | Lforce -> MLglobal (Ginternal "Lazy.force")
+
+let mllambda_of_lambda auxdefs l t =
+ let env = empty_env () in
+ global_stack := auxdefs;
+ let ml = ml_of_lam env l t in
+ let fv_rel = !(env.env_urel) in
+ let fv_named = !(env.env_named) in
+ (* build the free variables *)
+ let get_lname (_,t) =
+ match t with
+ | MLlocal x -> x
+ | _ -> assert false in
+ let params =
+ List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in
+ if params = [] then
+ (!global_stack, ([],[]), ml)
+ (* final result : global list, fv, ml *)
+ else
+ (!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml)
+ (**}}}**)
+
+(** Code optimization {{{**)
+
+(** Optimization of match and fix *)
+
+let can_subst l =
+ match l with
+ | MLlocal _ | MLint _ | MLglobal _ -> true
+ | _ -> false
+
+let subst s l =
+ if LNmap.is_empty s then l
+ else
+ let rec aux l =
+ match l with
+ | MLlocal id -> (try LNmap.find id s with _ -> l)
+ | MLglobal _ | MLprimitive _ | MLint _ -> l
+ | MLlam(params,body) -> MLlam(params, aux body)
+ | MLletrec(defs,body) ->
+ let arec (f,params,body) = (f,params,aux body) in
+ MLletrec(Array.map arec defs, aux body)
+ | MLlet(id,def,body) -> MLlet(id,aux def, aux body)
+ | MLapp(f,args) -> MLapp(aux f, Array.map aux args)
+ | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2)
+ | MLmatch(annot,a,accu,bs) ->
+ let auxb (cargs,body) = (cargs,aux body) in
+ MLmatch(annot,a,aux accu, Array.map auxb bs)
+ | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args)
+ | MLparray p -> MLparray(Array.map aux p)
+ | MLsetref(s,l1) -> MLsetref(s,aux l1)
+ | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
+ in
+ aux l
+
+let add_subst id v s =
+ match v with
+ | MLlocal id' when id.luid = id'.luid -> s
+ | _ -> LNmap.add id v s
+
+let subst_norm params args s =
+ let len = Array.length params in
+ assert (Array.length args = len && Array.for_all can_subst args);
+ let s = ref s in
+ for i = 0 to len - 1 do
+ s := add_subst params.(i) args.(i) !s
+ done;
+ !s
+
+let subst_case params args s =
+ let len = Array.length params in
+ assert (len > 0 &&
+ Array.length args = len &&
+ let r = ref true and i = ref 0 in
+ (* we test all arguments excepted the last *)
+ while !i < len - 1 && !r do r := can_subst args.(!i); incr i done;
+ !r);
+ let s = ref s in
+ for i = 0 to len - 2 do
+ s := add_subst params.(i) args.(i) !s
+ done;
+ !s, params.(len-1), args.(len-1)
+
+let empty_gdef = Int.Map.empty, Int.Map.empty
+let get_norm (gnorm, _) i = Int.Map.find i gnorm
+let get_case (_, gcase) i = Int.Map.find i gcase
+
+let all_lam n bs =
+ let f (_, l) =
+ match l with
+ | MLlam(params, _) -> Array.length params = n
+ | _ -> false in
+ Array.for_all f bs
+
+let commutative_cut annot a accu bs args =
+ let mkb (c,b) =
+ match b with
+ | MLlam(params, body) ->
+ (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args)
+ | _ -> assert false in
+ MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs)
+
+let optimize gdef l =
+ let rec optimize s l =
+ match l with
+ | MLlocal id -> (try LNmap.find id s with _ -> l)
+ | MLglobal _ | MLprimitive _ | MLint _ -> l
+ | MLlam(params,body) ->
+ MLlam(params, optimize s body)
+ | MLletrec(decls,body) ->
+ let opt_rec (f,params,body) = (f,params,optimize s body ) in
+ MLletrec(Array.map opt_rec decls, optimize s body)
+ | MLlet(id,def,body) ->
+ let def = optimize s def in
+ if can_subst def then optimize (add_subst id def s) body
+ else MLlet(id,def,optimize s body)
+ | MLapp(f, args) ->
+ let args = Array.map (optimize s) args in
+ begin match f with
+ | MLglobal (Gnorm (_,i)) ->
+ (try
+ let params,body = get_norm gdef i in
+ let s = subst_norm params args s in
+ optimize s body
+ with Not_found -> MLapp(optimize s f, args))
+ | MLglobal (Gcase (_,i)) ->
+ (try
+ let params,body = get_case gdef i in
+ let s, id, arg = subst_case params args s in
+ if can_subst arg then optimize (add_subst id arg s) body
+ else MLlet(id, arg, optimize s body)
+ with Not_found -> MLapp(optimize s f, args))
+ | _ ->
+ let f = optimize s f in
+ match f with
+ | MLmatch (annot,a,accu,bs) ->
+ if all_lam (Array.length args) bs then
+ commutative_cut annot a accu bs args
+ else MLapp(f, args)
+ | _ -> MLapp(f, args)
+
+ end
+ | MLif(t,b1,b2) ->
+ let t = optimize s t in
+ let b1 = optimize s b1 in
+ let b2 = optimize s b2 in
+ begin match t, b2 with
+ | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs)
+ when l1 = l2 -> MLmatch(annot, l1, b1, bs)
+ | _, _ -> MLif(t, b1, b2)
+ end
+ | MLmatch(annot,a,accu,bs) ->
+ let opt_b (cargs,body) = (cargs,optimize s body) in
+ MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
+ | MLconstruct(prefix,c,args) ->
+ MLconstruct(prefix,c,Array.map (optimize s) args)
+ | MLparray p -> MLparray (Array.map (optimize s) p)
+ | MLsetref(r,l) -> MLsetref(r, optimize s l)
+ | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
+ in
+ optimize LNmap.empty l
+
+let optimize_stk stk =
+ let add_global gdef g =
+ match g with
+ | Glet (Gnorm (_,i), body) ->
+ let (gnorm, gcase) = gdef in
+ (Int.Map.add i (decompose_MLlam body) gnorm, gcase)
+ | Gletcase(Gcase (_,i), params, annot,a,accu,bs) ->
+ let (gnorm,gcase) = gdef in
+ (gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase)
+ | Gletcase _ -> assert false
+ | _ -> gdef in
+ let gdef = List.fold_left add_global empty_gdef stk in
+ let optimize_global g =
+ match g with
+ | Glet(Gconstant (prefix, c), body) ->
+ Glet(Gconstant (prefix, c), optimize gdef body)
+ | _ -> g in
+ List.map optimize_global stk
+ (**}}}**)
+
+(** Printing to ocaml {{{**)
+(* Redefine a bunch of functions in module Names to generate names
+ acceptable to OCaml. *)
+let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
+let string_of_label l = Unicode.ascii_of_ident (string_of_label l)
+
+let string_of_dirpath = function
+ | [] -> "_"
+ | sl -> String.concat "_" (List.map string_of_id (List.rev sl))
+
+(* The first letter of the file name has to be a capital to be accepted by *)
+(* OCaml as a module identifier. *)
+let string_of_dirpath s = "N"^string_of_dirpath s
+
+let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir)
+
+let string_of_name x =
+ match x with
+ | Anonymous -> "anonymous" (* assert false *)
+ | Name id -> string_of_id id
+
+let string_of_label_def l =
+ match l with
+ | None -> ""
+ | Some l -> string_of_label l
+
+(* Relativization of module paths *)
+let rec list_of_mp acc = function
+ | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp
+ | MPfile dp ->
+ let dp = repr_dirpath dp in
+ string_of_dirpath dp :: acc
+ | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc
+
+let list_of_mp mp = list_of_mp [] mp
+
+let string_of_kn kn =
+ let (mp,dp,l) = repr_kn kn in
+ let mp = list_of_mp mp in
+ String.concat "_" mp ^ "_" ^ string_of_label l
+
+let string_of_con c = string_of_kn (user_con c)
+let string_of_mind mind = string_of_kn (user_mind mind)
+
+let string_of_gname g =
+ match g with
+ | Gind (prefix, (mind, i)) ->
+ Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
+ | Gconstruct (prefix, ((mind, i), j)) ->
+ Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
+ | Gconstant (prefix, c) ->
+ Format.sprintf "%sconst_%s" prefix (string_of_con c)
+ | Gcase (l,i) ->
+ Format.sprintf "case_%s_%i" (string_of_label_def l) i
+ | Gpred (l,i) ->
+ Format.sprintf "pred_%s_%i" (string_of_label_def l) i
+ | Gfixtype (l,i) ->
+ Format.sprintf "fixtype_%s_%i" (string_of_label_def l) i
+ | Gnorm (l,i) ->
+ Format.sprintf "norm_%s_%i" (string_of_label_def l) i
+ | Ginternal s -> Format.sprintf "%s" s
+ | Gnormtbl (l,i) ->
+ Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i
+ | Grel i ->
+ Format.sprintf "rel_%i" i
+ | Gnamed id ->
+ Format.sprintf "named_%s" (string_of_id id)
+
+let pp_gname fmt g =
+ Format.fprintf fmt "%s" (string_of_gname g)
+
+let pp_lname fmt ln =
+ let s = Unicode.ascii_of_ident (string_of_name ln.lname) in
+ Format.fprintf fmt "x_%s_%i" s ln.luid
+
+let pp_ldecls fmt ids =
+ let len = Array.length ids in
+ for i = 0 to len - 1 do
+ Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
+ done
+
+let string_of_construct prefix ((mind,i),j) =
+ let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in
+ prefix ^ id
+
+let pp_int fmt i =
+ if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i
+
+let pp_mllam fmt l =
+
+ let rec pp_mllam fmt l =
+ match l with
+ | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln
+ | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g
+ | MLprimitive p -> Format.fprintf fmt "@[%a@]" pp_primitive p
+ | MLlam(ids,body) ->
+ Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]"
+ pp_ldecls ids pp_mllam body
+ | MLletrec(defs, body) ->
+ Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs
+ pp_mllam body
+ | MLlet(id,def,body) ->
+ Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]"
+ pp_lname id pp_mllam def pp_mllam body
+ | MLapp(f, args) ->
+ Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args
+ | MLif(t,l1,l2) ->
+ Format.fprintf fmt "@[(if %a then@\n %a@\nelse@\n %a)@]"
+ pp_mllam t pp_mllam l1 pp_mllam l2
+ | MLmatch (asw, c, accu_br, br) ->
+ let mind,i = asw.asw_ind in
+ let prefix = asw.asw_prefix in
+ let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
+ Format.fprintf fmt
+ "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]"
+ pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
+
+ | MLconstruct(prefix,c,args) ->
+ Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]"
+ (string_of_construct prefix c) pp_cargs args
+ | MLint(int, i) ->
+ if int then pp_int fmt i
+ else Format.fprintf fmt "(val_of_int %a)" pp_int i
+ | MLparray p ->
+ Format.fprintf fmt "@[(parray_of_array@\n [|";
+ for i = 0 to Array.length p - 2 do
+ Format.fprintf fmt "%a;" pp_mllam p.(i)
+ done;
+ Format.fprintf fmt "%a|])@]" pp_mllam p.(Array.length p - 1)
+ | MLsetref (s, body) ->
+ Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
+ | MLsequence(l1,l2) ->
+ Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2
+
+ and pp_letrec fmt defs =
+ let len = Array.length defs in
+ let pp_one_rec i (fn, argsn, body) =
+ Format.fprintf fmt "%a%a =@\n %a"
+ pp_lname fn
+ pp_ldecls argsn pp_mllam body in
+ Format.fprintf fmt "@[let rec ";
+ pp_one_rec 0 defs.(0);
+ for i = 1 to len - 1 do
+ Format.fprintf fmt "@\nand ";
+ pp_one_rec i defs.(i)
+ done;
+
+ and pp_blam fmt l =
+ match l with
+ | MLprimitive (Mk_prod | Mk_sort)
+ | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
+ Format.fprintf fmt "(%a)" pp_mllam l
+ | MLconstruct(_,_,args) when Array.length args > 0 ->
+ Format.fprintf fmt "(%a)" pp_mllam l
+ | _ -> pp_mllam fmt l
+
+ and pp_args sep fmt args =
+ let sep = if sep then " " else "," in
+ let len = Array.length args in
+ if len > 0 then begin
+ Format.fprintf fmt "%a" pp_blam args.(0);
+ for i = 1 to len - 1 do
+ Format.fprintf fmt "%s%a" sep pp_blam args.(i)
+ done
+ end
+
+ and pp_cargs fmt args =
+ let len = Array.length args in
+ match len with
+ | 0 -> ()
+ | 1 -> Format.fprintf fmt " %a" pp_blam args.(0)
+ | _ -> Format.fprintf fmt "(%a)" (pp_args false) args
+
+ and pp_cparam fmt param =
+ match param with
+ | Some l -> pp_mllam fmt (MLlocal l)
+ | None -> Format.fprintf fmt "_"
+
+ and pp_cparams fmt params =
+ let len = Array.length params in
+ match len with
+ | 0 -> ()
+ | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0)
+ | _ ->
+ let aux fmt params =
+ Format.fprintf fmt "%a" pp_cparam params.(0);
+ for i = 1 to len - 1 do
+ Format.fprintf fmt ",%a" pp_cparam params.(i)
+ done in
+ Format.fprintf fmt "(%a)" aux params
+
+ and pp_branches prefix fmt bs =
+ let pp_branch (cargs,body) =
+ let pp_c fmt (cn,args) =
+ Format.fprintf fmt "| %s%a "
+ (string_of_construct prefix cn) pp_cparams args in
+ let rec pp_cargs fmt cargs =
+ match cargs with
+ | [] -> ()
+ | cargs::cargs' ->
+ Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in
+ Format.fprintf fmt "%a ->@\n %a@\n"
+ pp_cargs cargs pp_mllam body
+ in
+ Array.iter pp_branch bs
+
+ and pp_vprim o s =
+ match o with
+ | None -> Format.fprintf fmt "no_check_%s" s
+ | Some (prefix,kn) ->
+ Format.fprintf fmt "%s %a" s pp_mllam (MLglobal (Gconstant (prefix,kn)))
+
+ and pp_primitive fmt = function
+ | Mk_prod -> Format.fprintf fmt "mk_prod_accu"
+ | Mk_sort -> Format.fprintf fmt "mk_sort_accu"
+ | Mk_ind -> Format.fprintf fmt "mk_ind_accu"
+ | Mk_const -> Format.fprintf fmt "mk_constant_accu"
+ | Mk_sw -> Format.fprintf fmt "mk_sw_accu"
+ | Mk_fix(rec_pos,start) ->
+ let pp_rec_pos fmt rec_pos =
+ Format.fprintf fmt "@[[| %i" rec_pos.(0);
+ for i = 1 to Array.length rec_pos - 1 do
+ Format.fprintf fmt "; %i" rec_pos.(i)
+ done;
+ Format.fprintf fmt " |]@]" in
+ Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start
+ | 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)
+ | Is_accu -> Format.fprintf fmt "is_accu"
+ | Is_int -> Format.fprintf fmt "is_int"
+ | Is_array -> Format.fprintf fmt "is_parray"
+ | Cast_accu -> Format.fprintf fmt "cast_accu"
+ | Upd_cofix -> Format.fprintf fmt "upd_cofix"
+ | Force_cofix -> Format.fprintf fmt "force_cofix"
+ | Val_to_int -> Format.fprintf fmt "val_to_int"
+ | Val_of_int -> Format.fprintf fmt "val_of_int"
+ | Val_of_bool -> Format.fprintf fmt "of_bool"
+ | Chead0 o -> pp_vprim o "head0"
+ | Ctail0 o -> pp_vprim o "tail0"
+ | Cadd o -> pp_vprim o "add"
+ | Csub o -> pp_vprim o "sub"
+ | Cmul o -> pp_vprim o "mul"
+ | Cdiv o -> pp_vprim o "div"
+ | Crem o -> pp_vprim o "rem"
+ | Clsr o -> pp_vprim o "l_sr"
+ | Clsl o -> pp_vprim o "l_sl"
+ | Cand o -> pp_vprim o "l_and"
+ | Cor o -> pp_vprim o "l_or"
+ | Cxor o -> pp_vprim o "l_xor"
+ | Caddc o -> pp_vprim o "addc"
+ | Csubc o -> pp_vprim o "subc"
+ | CaddCarryC o -> pp_vprim o "addCarryC"
+ | CsubCarryC o -> pp_vprim o "subCarryC"
+ | Cmulc o -> pp_vprim o "mulc"
+ | Cdiveucl o -> pp_vprim o "diveucl"
+ | Cdiv21 o -> pp_vprim o "div21"
+ | CaddMulDiv o -> pp_vprim o "addMulDiv"
+ | Ceq o -> pp_vprim o "eq"
+ | Clt o -> pp_vprim o "lt"
+ | Cle o -> pp_vprim o "le"
+ | Clt_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b"
+ | Cle_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b"
+ | Ccompare o -> pp_vprim o "compare"
+ | Cprint o -> pp_vprim o "print"
+ | Carraymake o -> pp_vprim o "arraymake"
+ | Carrayget o -> pp_vprim o "arrayget"
+ | Carraydefault o -> pp_vprim o "arraydefault"
+ | Carrayset o -> pp_vprim o "arrayset"
+ | Carraycopy o -> pp_vprim o "arraycopy"
+ | Carrayreroot o -> pp_vprim o "arrayreroot"
+ | Carraylength o -> pp_vprim o "arraylength"
+ | Carrayinit o -> pp_vprim o "arrayinit"
+ | Carraymap o -> pp_vprim o "arraymap"
+ (* Caml primitive *)
+ | MLand -> Format.fprintf fmt "(&&)"
+ | MLle -> Format.fprintf fmt "(<=)"
+ | MLlt -> Format.fprintf fmt "(<)"
+ | MLinteq -> Format.fprintf fmt "(==)"
+ | MLlsl -> Format.fprintf fmt "(lsl)"
+ | MLlsr -> Format.fprintf fmt "(lsr)"
+ | MLland -> Format.fprintf fmt "(land)"
+ | MLlor -> Format.fprintf fmt "(lor)"
+ | MLlxor -> Format.fprintf fmt "(lxor)"
+ | MLadd -> Format.fprintf fmt "(+)"
+ | MLsub -> Format.fprintf fmt "(-)"
+ | MLmul -> Format.fprintf fmt "( * )"
+ | MLmagic -> Format.fprintf fmt "Obj.magic"
+
+ in
+ Format.fprintf fmt "@[%a@]" pp_mllam l
+
+let pp_array fmt t =
+ let len = Array.length t in
+ Format.fprintf fmt "@[[|";
+ for i = 0 to len - 2 do
+ Format.fprintf fmt "%a; " pp_mllam t.(i)
+ done;
+ if len > 0 then
+ Format.fprintf fmt "%a" pp_mllam t.(len - 1);
+ Format.fprintf fmt "|]@]"
+
+let pp_global fmt g =
+ match g with
+ | Glet (gn, c) ->
+ let ids, c = decompose_MLlam c in
+ Format.fprintf fmt "@[let %a%a =@\n %a@]@\n@." pp_gname gn
+ pp_ldecls ids
+ pp_mllam c
+ | Gopen s ->
+ Format.fprintf fmt "@[open %s@]@." s
+ | Gtype ((mind, i), lar) ->
+ let l = string_of_mind mind in
+ let rec aux s ar =
+ if ar = 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
+ let pp_const_sig i fmt j ar =
+ let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
+ Format.fprintf fmt " | Construct_%s_%i_%i %s@\n" l i j sig_str
+ in
+ let pp_const_sigs i fmt lar =
+ Format.fprintf fmt " | Accu_%s_%i of Nativevalues.t@\n" l i;
+ Array.iteri (pp_const_sig i fmt) lar
+ in
+ Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar
+ | Gtblfixtype (g, params, t) ->
+ Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g
+ pp_ldecls params pp_array t
+ | Gtblnorm (g, params, t) ->
+ Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g
+ pp_ldecls params pp_array t
+ | Gletcase(g,params,annot,a,accu,bs) ->
+ Format.fprintf fmt "@[let rec %a %a =@\n %a@]@\n@."
+ pp_gname g pp_ldecls params
+ pp_mllam (MLmatch(annot,a,accu,bs))(**}}}**)
+
+(** Compilation of elements in environment {{{**)
+let rec compile_with_fv env auxdefs l t =
+ let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in
+ if fv_named = [] && fv_rel = [] then (auxdefs,ml)
+ else apply_fv env (fv_named,fv_rel) auxdefs ml
+
+and apply_fv env (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
+(* | NVKvalue (v,d) -> assert false *)
+ in
+ let get_named_val (id,_) auxdefs =
+ (*
+ match !(lookup_named_native_val id env) with
+ | NVKnone ->
+ *)
+ compile_named env auxdefs id
+(* | NVKvalue (v,d) -> assert false *)
+ in
+ let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in
+ let auxdefs = List.fold_right get_named_val fv_named auxdefs in
+ let lvl = rel_context_length env.env_rel_context in
+ let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in
+ let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in
+ 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 =
+ 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
+ Glet(Grel n, code)::auxdefs
+ | None ->
+ Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs
+
+and compile_named env 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
+ Glet(Gnamed id, code)::auxdefs
+ | None ->
+ Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
+
+let compile_constant env prefix con body =
+ match body with
+ | Def t ->
+ let t = Declarations.force t in
+ let code = lambda_of_constr env t in
+ let code, name =
+ if is_lazy t then mk_lazy code, LinkedLazy prefix
+ else code, Linked prefix
+ in
+ let l = con_label con in
+ let auxdefs,code = compile_with_fv env [] (Some l) code in
+ let l =
+ optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
+ in
+ l, name
+ | _ ->
+ let i = push_symbol (SymbConst con) in
+ [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))],
+ Linked prefix
+
+let loaded_native_files = ref ([] : string list)
+
+let register_native_file s =
+ if not (List.mem s !loaded_native_files) then
+ loaded_native_files := s :: !loaded_native_files
+
+let is_code_loaded ~interactive name =
+ match !name with
+ | NotLinked -> false
+ | LinkedInteractive s ->
+ if (interactive && List.mem s !loaded_native_files) then true
+ else (name := NotLinked; false)
+ | LinkedLazy s | Linked s ->
+ if List.mem s !loaded_native_files then true else (name := NotLinked; false)
+
+let param_name = Name (id_of_string "params")
+let arg_name = Name (id_of_string "arg")
+
+let compile_mind prefix mb mind stack =
+ let f i stack ob =
+ let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
+ let j = push_symbol (SymbInd (mind,i)) in
+ let name = Gind ("", (mind, i)) in
+ let accu =
+ Glet(name, MLapp (MLprimitive Mk_ind, [|get_ind_code j|]))
+ in
+ let nparams = mb.mind_nparams in
+ let params =
+ Array.init nparams (fun i -> {lname = param_name; luid = i}) in
+ let add_construct j acc (_,arity) =
+ let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in
+ let c = (mind,i), (j+1) in
+ Glet(Gconstruct ("",c),
+ mkMLlam (Array.append params args)
+ (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
+ in
+ Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl
+ in
+ let upd = (mb.mind_native_name, Linked prefix) in
+ Array.fold_left_i f stack mb.mind_packets, upd
+
+type code_location_update =
+ Declarations.native_name ref * Declarations.native_name
+type code_location_updates =
+ code_location_update Mindmap_env.t * code_location_update Cmap_env.t
+
+type linkable_code = global list * code_location_updates
+
+let empty_updates = Mindmap_env.empty, Cmap_env.empty
+
+let compile_mind_deps env prefix ~interactive
+ (comp_stack, (mind_updates, const_updates) as init) mind =
+ let mib = lookup_mind mind env in
+ if is_code_loaded ~interactive mib.mind_native_name
+ || Mindmap_env.mem mind mind_updates
+ then init
+ else
+ let comp_stack, upd = compile_mind prefix mib mind comp_stack in
+ let mind_updates = Mindmap_env.add mind upd mind_updates in
+ (comp_stack, (mind_updates, const_updates))
+
+(* 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 =
+ match kind_of_term t with
+ | Meta _ -> raise (Invalid_argument "Nativecode.get_deps: Meta")
+ | Evar _ -> raise (Invalid_argument "Nativecode.get_deps: Evar")
+ | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind
+ | Const c ->
+ let c = get_allias env c in
+ let cb = lookup_constant c env in
+ let (_, (_, const_updates)) = init in
+ if is_code_loaded ~interactive cb.const_native_name
+ || cb.const_inline_code
+ || (Cmap_env.mem c const_updates)
+ then init
+ else
+ let comp_stack, (mind_updates, const_updates) = match cb.const_body with
+ | Def t -> compile_deps env prefix ~interactive init (Declarations.force t)
+ | _ -> init
+ in
+ let code, name = compile_constant env prefix c cb.const_body in
+ let comp_stack = code@comp_stack in
+ let const_updates = Cmap_env.add c (cb.const_native_name, name) const_updates in
+ comp_stack, (mind_updates, const_updates)
+ | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind
+ | _ -> fold_constr (compile_deps env prefix ~interactive) init t
+
+let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb =
+ reset_symbols_list symb;
+ let acc = (code, (mupds, cupds)) in
+ match cb.const_body with
+ | Def t ->
+ let t = Declarations.force t in
+ let (code, (mupds, cupds)) = compile_deps env prefix ~interactive:false acc t in
+ let (gl, name) = compile_constant env prefix con cb.const_body in
+ let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
+ gl@code, !symbols_list, (mupds, cupds)
+ | _ ->
+ let (gl, name) = compile_constant env prefix con cb.const_body in
+ let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in
+ gl@code, !symbols_list, (mupds, cupds)
+
+let compile_mind_field prefix mp l (code, symb, (mupds, cupds)) mb =
+ let mind = make_mind mp empty_dirpath l in
+ reset_symbols_list symb;
+ let code, upd = compile_mind prefix mb mind code in
+ let mupds = Mindmap_env.add mind upd mupds in
+ code, !symbols_list, (mupds, cupds)
+
+let mk_open s = Gopen s
+
+let mk_internal_let s code =
+ Glet(Ginternal s, code)
+
+(* ML Code for conversion function *)
+let mk_conv_code env prefix t1 t2 =
+ let gl, (mind_updates, const_updates) =
+ let init = ([], empty_updates) in
+ compile_deps env 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
+ in
+ let gl = List.rev gl 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 g1 = MLglobal (Ginternal "t1") in
+ let g2 = MLglobal (Ginternal "t2") in
+ let header = Glet(Ginternal "symbols_tbl",
+ MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ [|MLglobal (Ginternal "()")|])) in
+ header::(gl@
+ [mk_internal_let "t1" code1;
+ mk_internal_let "t2" code2;
+ Glet(Ginternal "_", MLsetref("rt1",g1));
+ Glet(Ginternal "_", MLsetref("rt2",g2))]),
+ (mind_updates, const_updates)
+
+let mk_norm_code env prefix t =
+ let gl, (mind_updates, const_updates) =
+ let init = ([], empty_updates) in
+ compile_deps env prefix ~interactive:true init t
+ in
+ let gl = List.rev gl in
+ let code = lambda_of_constr env t in
+ let (gl,code) = compile_with_fv env gl None code in
+ let g1 = MLglobal (Ginternal "t1") in
+ let header = Glet(Ginternal "symbols_tbl",
+ MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ [|MLglobal (Ginternal "()")|])) in
+ header::(gl@
+ [mk_internal_let "t1" code;
+ Glet(Ginternal "_", MLsetref("rt1",g1))]), (mind_updates, const_updates)
+
+let mk_library_header dir =
+ let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
+ [Glet(Ginternal "symbols_tbl",
+ MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+ [|MLglobal (Ginternal libname)|]))]
+
+let update_location (r,v) = r := v
+
+let update_locations (ind_updates,const_updates) =
+ Mindmap_env.iter (fun _ -> update_location) ind_updates;
+ Cmap_env.iter (fun _ -> update_location) const_updates
+(** }}} **)
+
+(* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
new file mode 100644
index 0000000000..0f01ae80e7
--- /dev/null
+++ b/kernel/nativecode.mli
@@ -0,0 +1,66 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Term
+open Names
+open Declarations
+open Pre_env
+open Nativelambda
+
+(** This file defines the mllambda code generation phase of the native
+compiler. mllambda represents a fragment of ML, and can easily be printed
+to OCaml code. *)
+
+type mllambda
+type global
+
+val pp_global : Format.formatter -> global -> unit
+
+val mk_open : string -> global
+
+type symbol
+
+val get_value : symbol array -> int -> Nativevalues.t
+
+val get_sort : symbol array -> int -> sorts
+
+val get_name : symbol array -> int -> name
+
+val get_const : symbol array -> int -> constant
+
+val get_match : symbol array -> int -> Nativevalues.annot_sw
+
+val get_ind : symbol array -> int -> inductive
+
+val get_symbols_tbl : unit -> symbol array
+
+type code_location_update
+type code_location_updates
+type linkable_code = global list * code_location_updates
+
+val empty_updates : code_location_updates
+
+val register_native_file : string -> unit
+
+val compile_constant_field : env -> string -> constant ->
+ global list * symbol list * code_location_updates ->
+ constant_body ->
+ global list * symbol list * code_location_updates
+
+val compile_mind_field : string -> module_path -> label ->
+ global list * symbol list * code_location_updates ->
+ mutual_inductive_body ->
+ global list * symbol list * code_location_updates
+
+val mk_conv_code : env -> string -> constr -> constr -> linkable_code
+val mk_norm_code : env -> string -> constr -> linkable_code
+
+val mk_library_header : dir_path -> global list
+
+val mod_uid_of_dirpath : dir_path -> string
+
+val update_locations : code_location_updates -> unit
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
new file mode 100644
index 0000000000..4ba3056600
--- /dev/null
+++ b/kernel/nativeconv.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Errors
+open Names
+open Term
+open Univ
+open Pre_env
+open Nativelib
+open Reduction
+open Declarations
+open Util
+open Nativevalues
+open Nativelambda
+open Nativecode
+
+(** This module implements the conversion test by compiling to OCaml code *)
+
+let rec conv_val pb lvl v1 v2 cu =
+ if v1 == v2 then cu
+ else
+ match kind_of_value v1, kind_of_value v2 with
+ | Vaccu k1, Vaccu k2 ->
+ conv_accu pb lvl k1 k2 cu
+ | Vfun f1, Vfun f2 ->
+ let v = mk_rel_accu lvl in
+ conv_val CONV (lvl+1) (f1 v) (f2 v) cu
+ | Vconst i1, Vconst i2 ->
+ if i1 = i2 then cu else raise NotConvertible
+ | Vblock b1, Vblock b2 ->
+ let n1 = block_size b1 in
+ if block_tag b1 <> block_tag b2 || n1 <> block_size b2 then
+ raise NotConvertible;
+ let rec aux lvl max b1 b2 i cu =
+ if i = max then
+ conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu
+ else
+ let cu =
+ conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu in
+ aux lvl max b1 b2 (i+1) cu in
+ aux lvl (n1-1) b1 b2 0 cu
+ | Vfun f1, _ ->
+ conv_val CONV lvl v1 (fun x -> v2 x) cu
+ | _, Vfun f2 ->
+ conv_val CONV lvl (fun x -> v1 x) v2 cu
+ | _, _ -> raise NotConvertible
+
+and conv_accu pb lvl k1 k2 cu =
+ let n1 = accu_nargs k1 in
+ if n1 <> accu_nargs k2 then raise NotConvertible;
+ if n1 = 0 then
+ conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
+ else
+ let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+ List.fold_right2 (conv_val CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
+
+and conv_atom pb lvl a1 a2 cu =
+ if a1 == a2 then cu
+ else
+ match a1, a2 with
+ | Arel i1, Arel i2 ->
+ if i1 <> i2 then raise NotConvertible;
+ cu
+ | Aind ind1, Aind ind2 ->
+ if not (eq_ind ind1 ind2) then raise NotConvertible;
+ cu
+ | Aconstant c1, Aconstant c2 ->
+ if not (eq_constant c1 c2) then raise NotConvertible;
+ cu
+ | Asort s1, Asort s2 ->
+ sort_cmp pb s1 s2 cu
+ | Avar id1, Avar id2 ->
+ if id1 <> id2 then raise NotConvertible;
+ cu
+ | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
+ if a1.asw_ind <> a2.asw_ind then raise NotConvertible;
+ let cu = conv_accu CONV lvl ac1 ac2 cu in
+ let tbl = a1.asw_reloc in
+ let len = Array.length tbl in
+ if len = 0 then conv_val CONV lvl p1 p2 cu
+ else
+ let cu = conv_val CONV lvl p1 p2 cu in
+ let max = len - 1 in
+ let rec aux i cu =
+ let tag,arity = tbl.(i) in
+ let ci =
+ if arity = 0 then mk_const tag
+ else mk_block tag (mk_rels_accu lvl arity) in
+ let bi1 = bs1 ci and bi2 = bs2 ci in
+ if i = max then conv_val CONV (lvl + arity) bi1 bi2 cu
+ else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in
+ aux 0 cu
+ | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
+ if s1 <> s2 || rp1 <> rp2 then raise NotConvertible;
+ if f1 == f2 then cu
+ else conv_fix lvl t1 f1 t2 f2 cu
+ | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
+ (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
+ if s1 <> s2 then raise NotConvertible;
+ if f1 == f2 then cu
+ else
+ if Array.length f1 <> Array.length f2 then raise NotConvertible
+ else conv_fix lvl t1 f1 t2 f2 cu
+ | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
+ let cu = conv_val CONV lvl d1 d2 cu in
+ let v = mk_rel_accu lvl in
+ conv_val pb (lvl + 1) (d1 v) (d2 v) cu
+ | _, _ -> raise NotConvertible
+
+(* Precondition length t1 = length f1 = length f2 = length t2 *)
+and conv_fix lvl t1 f1 t2 f2 cu =
+ let len = Array.length f1 in
+ let max = len - 1 in
+ let fargs = mk_rels_accu lvl len in
+ let flvl = lvl + len in
+ let rec aux i cu =
+ let cu = conv_val CONV lvl t1.(i) t2.(i) cu in
+ let fi1 = napply f1.(i) fargs in
+ let fi2 = napply f2.(i) fargs in
+ if i = max then conv_val CONV flvl fi1 fi2 cu
+ else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
+ aux 0 cu
+
+let native_conv pb env t1 t2 =
+ if !Flags.no_native_compiler then begin
+ let msg = "Native compiler is disabled, "^
+ "falling back to VM conversion test." in
+ Pp.msg_warning (Pp.str msg);
+ vm_conv pb env t1 t2
+ end
+ 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
+ match compile ml_filename code with
+ | (0,fn) ->
+ begin
+ if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
+ let t0 = Sys.time () in
+ call_linker ~fatal:true prefix fn (Some upds);
+ let t1 = Sys.time () in
+ let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+ if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+ (* TODO change 0 when we can have deBruijn *)
+ conv_val pb 0 !rt1 !rt2 empty_constraint
+ end
+ | _ -> anomaly "Compilation failure"
+
+let _ = set_nat_conv native_conv
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
new file mode 100644
index 0000000000..2cb5ac7973
--- /dev/null
+++ b/kernel/nativeconv.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Term
+open Univ
+open Environ
+open Reduction
+
+(** This module implements the conversion test by compiling to OCaml code *)
+
+val native_conv : conv_pb -> types conversion_function
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
new file mode 100644
index 0000000000..2ca2747994
--- /dev/null
+++ b/kernel/nativelambda.ml
@@ -0,0 +1,676 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Util
+open Names
+open Esubst
+open Term
+open Declarations
+open Pre_env
+open Nativevalues
+
+(** This file defines the lambda code generation phase of the native compiler *)
+
+type lambda =
+ | Lrel of name * int
+ | Lvar of identifier
+ | Lprod of lambda * lambda
+ | Llam of name array * lambda
+ | Lrec of name * lambda
+ | Llet of name * lambda * lambda
+ | Lapp of lambda * lambda array
+ | Lconst of string * constant (* prefix, constant name *)
+ | Lcase of annot_sw * lambda * lambda * lam_branches
+ (* annotations, term being matched, accu, branches *)
+ | Lareint of lambda array
+ | Lif of lambda * lambda * lambda
+ | Lfix of (int array * int) * fix_decl
+ | Lcofix of int * fix_decl
+ | Lmakeblock of string * constructor * int * lambda array
+ (* prefix, constructor name, constructor tag, arguments *)
+ (* A fully applied constructor *)
+ | Lconstruct of string * constructor (* prefix, constructor name *)
+ (* A partially applied constructor *)
+ | Lval of Nativevalues.t
+ | Lsort of sorts
+ | Lind of string * inductive (* prefix, inductive name *)
+ | Llazy
+ | Lforce
+
+and lam_branches = (constructor * name array * lambda) array
+
+and fix_decl = name array * lambda array * lambda array
+
+(*s Constructors *)
+
+let mkLapp f args =
+ if Array.length args = 0 then f
+ else
+ match f with
+ | Lapp(f', args') -> Lapp (f', Array.append args' args)
+ | _ -> Lapp(f, args)
+
+let mkLlam ids body =
+ if Array.length ids = 0 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
+ | _ -> [||], lam
+
+(*s Operators on substitution *)
+let subst_id = subs_id 0
+let lift = subs_lift
+let liftn = subs_liftn
+let cons v subst = subs_cons([|v|], subst)
+let shift subst = subs_shft (1, subst)
+
+(* Linked code location utilities *)
+let get_mind_prefix env mind =
+ let mib = lookup_mind mind env in
+ match !(mib.mind_native_name) with
+ | NotLinked -> ""
+ | Linked s -> s
+ | LinkedLazy s -> s
+ | LinkedInteractive s -> s
+
+let get_const_prefix env c =
+ let cb = lookup_constant c env in
+ match !(cb.const_native_name) with
+ | NotLinked -> ""
+ | Linked s -> s
+ | LinkedLazy s -> s
+ | LinkedInteractive s -> s
+
+(* A generic map function *)
+
+let map_lam_with_binders g f n lam =
+ match lam with
+ | Lrel _ | Lvar _ | Lconst _ | Lval _
+ | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce -> lam
+ | Lprod(dom,codom) ->
+ let dom' = f n dom in
+ let codom' = f n codom in
+ if dom == dom' && codom == codom' then lam else Lprod(dom',codom')
+ | Llam(ids,body) ->
+ let body' = f (g (Array.length ids) n) body in
+ if body == body' then lam else mkLlam ids body'
+ | Lrec(id,body) ->
+ let body' = f (g 1 n) body in
+ if body == body' then lam else Lrec(id,body')
+ | Llet(id,def,body) ->
+ let def' = f n def in
+ let body' = f (g 1 n) body in
+ if body == body' && def == def' then lam else Llet(id,def',body')
+ | Lapp(fct,args) ->
+ let fct' = f n fct in
+ let args' = Array.smartmap (f n) args in
+ if fct == fct' && args == args' then lam else mkLapp fct' args'
+ | Lcase(annot,t,a,br) ->
+ let t' = f n t in
+ let a' = f n a in
+ let on_b b =
+ let (cn,ids,body) = b in
+ let body' =
+ let len = Array.length ids in
+ if len = 0 then f n body
+ else f (g (Array.length ids) n) body in
+ if body == body' then b else (cn,ids,body') in
+ let br' = Array.smartmap on_b br in
+ if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
+ | Lareint a ->
+ let a' = Array.smartmap (f n) a in
+ if a == a' then lam else Lareint a'
+ | Lif(t,bt,bf) ->
+ let t' = f n t in
+ let bt' = f n bt in
+ let bf' = f n bf in
+ if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
+ | Lfix(init,(ids,ltypes,lbodies)) ->
+ let ltypes' = Array.smartmap (f n) ltypes in
+ let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+ if ltypes == ltypes' && lbodies == lbodies' then lam
+ else Lfix(init,(ids,ltypes',lbodies'))
+ | Lcofix(init,(ids,ltypes,lbodies)) ->
+ let ltypes' = Array.smartmap (f n) ltypes in
+ let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+ if ltypes == ltypes' && lbodies == lbodies' then lam
+ else Lcofix(init,(ids,ltypes',lbodies'))
+ | Lmakeblock(prefix,cn,tag,args) ->
+ let args' = Array.smartmap (f n) args in
+ if args == args' then lam else Lmakeblock(prefix,cn,tag,args')
+
+(*s Lift and substitution *)
+
+let rec lam_exlift el lam =
+ match lam with
+ | Lrel(id,i) ->
+ let i' = reloc_rel i el in
+ if i == i' then lam else Lrel(id,i')
+ | _ -> map_lam_with_binders el_liftn lam_exlift el lam
+
+let lam_lift k lam =
+ if k = 0 then lam
+ else lam_exlift (el_shft k el_id) lam
+
+let lam_subst_rel lam id n subst =
+ match expand_rel n subst with
+ | Inl(k,v) -> lam_lift k v
+ | Inr(n',_) ->
+ if n == n' then lam
+ else Lrel(id, n')
+
+let rec lam_exsubst subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+ | _ -> map_lam_with_binders liftn lam_exsubst subst lam
+
+let lam_subst subst lam =
+ if is_subs_id subst then lam
+ else lam_exsubst subst lam
+
+let lam_subst_args subst args =
+ if is_subs_id subst then args
+ else Array.smartmap (lam_exsubst subst) args
+
+(** Simplification of lambda expression *)
+
+(* [simplify subst lam] simplify the expression [lam_subst subst lam] *)
+(* that is : *)
+(* - Reduce [let] is the definition can be substituted i.e: *)
+(* - a variable (rel or identifier) *)
+ (* - a constant *)
+(* - a structured constant *)
+(* - a function *)
+(* - Transform beta redex into [let] expression *)
+(* - Move arguments under [let] *)
+(* Invariant : Terms in [subst] are already simplified and can be *)
+(* substituted *)
+
+let can_subst lam =
+ match lam with
+ | Lrel _ | Lvar _ | Lconst _
+ | Lval _ | Lsort _ | Lind _ | Llam _ | Lconstruct _ -> true
+ | _ -> false
+
+let can_merge_if bt bf =
+ match bt, bf with
+ | Llam(idst,_), Llam(idsf,_) -> true
+ | _ -> false
+
+let merge_if t bt bf =
+ let (idst,bodyt) = decompose_Llam bt in
+ let (idsf,bodyf) = decompose_Llam bf in
+ let nt = Array.length idst in
+ let nf = Array.length idsf in
+ let common,idst,idsf =
+ if nt = nf then idst, [||], [||]
+ else
+ if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
+ else idsf, Array.sub idst nf (nt - nf), [||] in
+ Llam(common,
+ Lif(lam_lift (Array.length common) t,
+ mkLlam idst bodyt,
+ mkLlam idsf bodyf))
+
+let rec simplify subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+
+ | Llet(id,def,body) ->
+ let def' = simplify subst def in
+ if can_subst def' then simplify (cons def' subst) body
+ else
+ let body' = simplify (lift subst) body in
+ if def == def' && body == body' then lam
+ else Llet(id,def',body')
+
+ | Lapp(f,args) ->
+ begin match simplify_app subst f subst args with
+ | Lapp(f',args') when f == f' && args == args' -> lam
+ | lam' -> lam'
+ end
+
+ | Lif(t,bt,bf) ->
+ let t' = simplify subst t in
+ let bt' = simplify subst bt in
+ let bf' = simplify subst bf in
+ if can_merge_if bt' bf' then merge_if t' bt' bf'
+ else
+ if t == t' && bt == bt' && bf == bf' then lam
+ else Lif(t',bt',bf')
+ | _ -> map_lam_with_binders liftn simplify subst lam
+
+and simplify_app substf f substa args =
+ match f with
+ | Lrel(id, i) ->
+ begin match lam_subst_rel f id i substf with
+ | Llam(ids, body) ->
+ reduce_lapp
+ subst_id (Array.to_list ids) body
+ substa (Array.to_list args)
+ | f' -> mkLapp f' (simplify_args substa args)
+ end
+ | Llam(ids, body) ->
+ reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args)
+ | Llet(id, def, body) ->
+ let def' = simplify substf def in
+ if can_subst def' then
+ simplify_app (cons def' substf) body substa args
+ else
+ Llet(id, def', simplify_app (lift substf) body (shift substa) args)
+ | Lapp(f, args') ->
+ let args = Array.append
+ (lam_subst_args substf args') (lam_subst_args substa args) in
+ simplify_app substf f subst_id args
+ | _ -> mkLapp (simplify substf f) (simplify_args substa args)
+
+and simplify_args subst args = Array.smartmap (simplify subst) args
+
+and reduce_lapp substf lids body substa largs =
+ match lids, largs with
+ | id::lids, a::largs ->
+ let a = simplify substa a in
+ if can_subst a then
+ reduce_lapp (cons a substf) lids body substa largs
+ else
+ let body = reduce_lapp (lift substf) lids body (shift substa) largs in
+ Llet(id, a, body)
+ | [], [] -> simplify substf body
+ | _::_, _ ->
+ Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body)
+ | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
+
+
+(* [occurence kind k lam]:
+ If [kind] is [true] return [true] if the variable [k] does not appear in
+ [lam], return [false] if the variable appear one time and not
+ under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
+ If [kind] is [false] return [false] if the variable does not appear in [lam]
+ else raise [Not_found]
+*)
+
+let rec occurence k kind lam =
+ match lam with
+ | Lrel (_,n) ->
+ if n = k then
+ if kind then false else raise Not_found
+ else kind
+ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _
+ | Lconstruct _ | Llazy | Lforce -> kind
+ | Lprod(dom, codom) ->
+ occurence k (occurence k kind dom) codom
+ | Llam(ids,body) ->
+ let _ = occurence (k+Array.length ids) false body in kind
+ | Lrec(id,body) ->
+ let _ = occurence (k+1) false body in kind
+ | Llet(_,def,body) ->
+ occurence (k+1) (occurence k kind def) body
+ | Lapp(f, args) ->
+ occurence_args k (occurence k kind f) args
+ | Lmakeblock(_,_,_,args) ->
+ occurence_args k kind args
+ | Lcase(_,t,a,br) ->
+ let kind = occurence k (occurence k kind t) a in
+ let r = ref kind in
+ Array.iter (fun (_,ids,c) ->
+ r := occurence (k+Array.length ids) kind c && !r) br;
+ !r
+ | Lareint a ->
+ occurence_args k kind a
+ | Lif (t, bt, bf) ->
+ let kind = occurence k kind t in
+ kind && occurence k kind bt && occurence k kind bf
+ | Lfix(_,(ids,ltypes,lbodies))
+ | Lcofix(_,(ids,ltypes,lbodies)) ->
+ let kind = occurence_args k kind ltypes in
+ let _ = occurence_args (k+Array.length ids) false lbodies in
+ kind
+
+and occurence_args k kind args =
+ Array.fold_left (occurence k) kind args
+
+let occur_once lam =
+ try let _ = occurence 1 true lam in true
+ with Not_found -> false
+
+(* [remove_let lam] remove let expression in [lam] if the variable is *)
+(* used at most once time in the body, and does not appear under *)
+(* a lambda or a fix or a cofix *)
+
+let rec remove_let subst lam =
+ match lam with
+ | Lrel(id,i) -> lam_subst_rel lam id i subst
+ | Llet(id,def,body) ->
+ let def' = remove_let subst def in
+ if occur_once body then remove_let (cons def' subst) body
+ else
+ let body' = remove_let (lift subst) body in
+ if def == def' && body == body' then lam else Llet(id,def',body')
+ | _ -> map_lam_with_binders liftn remove_let subst lam
+
+
+(*s Translation from [constr] to [lambda] *)
+
+(* Translation of constructor *)
+
+let is_value lc =
+ match lc with
+ | Lval _ -> true
+ | Lmakeblock(_,_,_,args) when Array.length args = 0 -> true
+ | _ -> false
+
+let get_value lc =
+ match lc with
+ | Lval v -> v
+ | Lmakeblock(_,_,tag,args) when Array.length args = 0 ->
+ Nativevalues.mk_int tag
+ | _ -> raise Not_found
+
+let make_args start _end =
+ Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
+
+(* Translation of constructors *)
+
+let makeblock env cn tag args =
+ if Array.for_all is_value args && Array.length args > 0 then
+ let args = Array.map get_value args in
+ Lval (Nativevalues.mk_block tag args)
+ else
+ let prefix = get_mind_prefix env (fst (fst cn)) in
+ Lmakeblock(prefix, cn, tag, args)
+
+(* Translation of constants *)
+
+let rec get_allias env kn =
+ let tps = (lookup_constant kn env).const_body_code in
+ match Cemitcodes.force tps with
+ | Cemitcodes.BCallias kn' -> get_allias env kn'
+ | _ -> kn
+
+(*i Global environment *)
+
+let global_env = ref empty_env
+
+let set_global_env env = global_env := env
+
+let get_names decl =
+ let decl = Array.of_list decl in
+ Array.map fst decl
+
+(* Rel Environment *)
+module Vect =
+ struct
+ type 'a t = {
+ mutable elems : 'a array;
+ mutable size : int;
+ }
+
+ let make n a = {
+ elems = Array.make n a;
+ size = 0;
+ }
+
+ let length v = v.size
+
+ let extend v =
+ if v.size = Array.length v.elems then
+ let new_size = min (2*v.size) Sys.max_array_length in
+ if new_size <= v.size then raise (Invalid_argument "Vect.extend");
+ let new_elems = Array.make new_size v.elems.(0) in
+ Array.blit v.elems 0 new_elems 0 (v.size);
+ v.elems <- new_elems
+
+ let push v a =
+ extend v;
+ v.elems.(v.size) <- a;
+ v.size <- v.size + 1
+
+ let push_pos v a =
+ let pos = v.size in
+ push v a;
+ pos
+
+ let popn v n =
+ v.size <- max 0 (v.size - n)
+
+ let pop v = popn v 1
+
+ let get v n =
+ if v.size <= n then raise
+ (Invalid_argument "Vect.get:index out of bounds");
+ v.elems.(n)
+
+ let get_last v n =
+ if v.size <= n then raise
+ (Invalid_argument "Vect.get:index out of bounds");
+ v.elems.(v.size - n - 1)
+
+
+ let last v =
+ if v.size = 0 then raise
+ (Invalid_argument "Vect.last:index out of bounds");
+ v.elems.(v.size - 1)
+
+ let clear v = v.size <- 0
+
+ let to_array v = Array.sub v.elems 0 v.size
+
+ end
+
+let empty_args = [||]
+
+module Renv =
+ struct
+
+ type constructor_info = tag * int * int (* nparam nrealargs *)
+
+ type t = {
+ name_rel : name Vect.t;
+ construct_tbl : (constructor, constructor_info) Hashtbl.t;
+
+ }
+
+
+ let make () = {
+ name_rel = Vect.make 16 Anonymous;
+ construct_tbl = Hashtbl.create 111
+ }
+
+ let push_rel env id = Vect.push env.name_rel id
+
+ let push_rels env ids =
+ Array.iter (push_rel env) ids
+
+ let pop env = Vect.pop env.name_rel
+
+ let popn env n =
+ for i = 1 to n do pop env done
+
+ let get env n =
+ Lrel (Vect.get_last env.name_rel (n-1), n)
+
+ let get_construct_info env c =
+ try Hashtbl.find env.construct_tbl c
+ with Not_found ->
+ let ((mind,j), i) = c in
+ let oib = lookup_mind mind !global_env in
+ let oip = oib.mind_packets.(j) in
+ let tag,arity = oip.mind_reloc_tbl.(i-1) in
+ let nparams = oib.mind_nparams in
+ let r = (tag, nparams, arity) in
+ Hashtbl.add env.construct_tbl c r;
+ r
+ end
+
+let is_lazy t = (* APPROXIMATION *)
+ isApp t || isLetIn t
+
+let empty_ids = [||]
+
+let rec lambda_of_constr env c =
+(* try *)
+ match kind_of_term c with
+ | Meta _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr: Meta")
+ | Evar _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr : Evar")
+
+ | Cast (c, _, _) -> lambda_of_constr env 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
+ Renv.push_rel env id;
+ let lc = lambda_of_constr env codom in
+ Renv.pop env;
+ Lprod(ld, Llam([|id|], lc))
+
+ | Lambda _ ->
+ 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
+ Renv.popn env (Array.length ids);
+ mkLlam ids lb
+
+ | LetIn(id, def, _, body) ->
+ let ld = lambda_of_constr env def in
+ Renv.push_rel env id;
+ let lb = lambda_of_constr env body in
+ Renv.pop env;
+ Llet(id, ld, lb)
+
+ | App(f, args) -> lambda_of_app env f args
+
+ | Const _ -> lambda_of_app env c empty_args
+
+ | Construct _ -> lambda_of_app env c empty_args
+
+ | Case(ci,t,a,branches) ->
+ let (mind,i as ind) = ci.ci_ind in
+ let mib = lookup_mind mind !global_env in
+ let oib = mib.mind_packets.(i) in
+ let tbl = oib.mind_reloc_tbl in
+ (* Building info *)
+ let prefix = get_mind_prefix !global_env mind in
+ let annot_sw =
+ { asw_ind = ind;
+ asw_ci = ci;
+ asw_reloc = tbl;
+ asw_finite = mib.mind_finite;
+ asw_prefix = prefix}
+ in
+ (* translation of the argument *)
+ let la = lambda_of_constr env a in
+ (* translation of the type *)
+ let lt = lambda_of_constr env 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
+ if arity = 0 then (cn, empty_ids, b)
+ else
+ match b with
+ | Llam(ids, body) when Array.length ids = arity -> (cn, ids, body)
+ | _ ->
+ let ids = Array.make arity Anonymous in
+ let args = make_args arity 1 in
+ let ll = lam_lift arity b in
+ (cn, ids, mkLapp ll args) in
+ let bs = Array.mapi mk_branch branches in
+ Lcase(annot_sw, lt, la, bs)
+
+ | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
+ let ltypes = lambda_of_args env 0 type_bodies in
+ Renv.push_rels env names;
+ let lbodies = lambda_of_args env 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
+ Renv.push_rels env names;
+ let lbodies = lambda_of_args env 0 rec_bodies in
+ Renv.popn env (Array.length names);
+ Lcofix(init, (names, ltypes, lbodies))
+
+and lambda_of_app env f args =
+ match kind_of_term f with
+ | Const kn ->
+ let kn = get_allias !global_env kn in
+ let cb = lookup_constant kn !global_env in
+ begin match cb.const_body with
+ | Def csubst ->
+ if cb.const_inline_code then lambda_of_app env (force csubst) args
+ else
+ let prefix = get_const_prefix !global_env kn in
+ let t =
+ if is_lazy (force csubst) then mkLapp Lforce [|Lconst (prefix, kn)|]
+ else Lconst (prefix, kn)
+ in
+ mkLapp t (lambda_of_args env 0 args)
+ | OpaqueDef _ | Undef _ ->
+ let prefix = get_const_prefix !global_env kn in
+ mkLapp (Lconst (prefix, kn)) (lambda_of_args env 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 nargs = expected then
+ let args = lambda_of_args env 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)
+ | _ ->
+ let f = lambda_of_constr env f in
+ let args = lambda_of_args env 0 args in
+ mkLapp f args
+
+and lambda_of_args env 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))
+ else empty_args
+
+let optimize lam =
+ let lam = simplify subst_id lam in
+(* if Flags.vm_draw_opt () then
+ (msgerrnl (str "Simplify = \n" ++ pp_lam lam);flush_all());
+ let lam = remove_let subst_id lam in
+ if Flags.vm_draw_opt () then
+ (msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *)
+ lam
+
+let lambda_of_constr env 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
+(* 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());
+ end; *)
+ optimize lam
+
+let mk_lazy c =
+ mkLapp Llazy [|c|]
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
new file mode 100644
index 0000000000..0c454256e1
--- /dev/null
+++ b/kernel/nativelambda.mli
@@ -0,0 +1,55 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Util
+open Names
+open Esubst
+open Term
+open Declarations
+open Pre_env
+open Nativevalues
+
+(** This file defines the lambda code generation phase of the native compiler *)
+
+type lambda =
+ | Lrel of name * int
+ | Lvar of identifier
+ | Lprod of lambda * lambda
+ | Llam of name array * lambda
+ | Lrec of name * lambda
+ | Llet of name * lambda * lambda
+ | Lapp of lambda * lambda array
+ | Lconst of string * constant (* prefix, constant name *)
+ | Lcase of annot_sw * lambda * lambda * lam_branches
+ (* annotations, term being matched, accu, branches *)
+ | Lareint of lambda array
+ | Lif of lambda * lambda * lambda
+ | Lfix of (int array * int) * fix_decl
+ | Lcofix of int * fix_decl
+ | Lmakeblock of string * constructor * int * lambda array
+ (* prefix, constructor name, constructor tag, arguments *)
+ (* A fully applied constructor *)
+ | Lconstruct of string * constructor (* prefix, constructor name *)
+ (* A partially applied constructor *)
+ | Lval of Nativevalues.t
+ | Lsort of sorts
+ | Lind of string * inductive (* prefix, inductive name *)
+ | Llazy
+ | Lforce
+
+and lam_branches = (constructor * name array * lambda) array
+
+and fix_decl = name array * lambda array * lambda array
+
+val decompose_Llam : lambda -> Names.name array * lambda
+
+val is_lazy : constr -> bool
+val mk_lazy : lambda -> lambda
+
+val get_allias : env -> constant -> constant
+
+val lambda_of_constr : env -> types -> lambda
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
new file mode 100644
index 0000000000..f8474bf199
--- /dev/null
+++ b/kernel/nativelib.ml
@@ -0,0 +1,91 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Names
+open Term
+open Util
+open Nativevalues
+open Declarations
+open Nativecode
+open Pre_env
+open Errors
+open Envars
+
+(** This file provides facilities to access OCaml compiler and dynamic linker,
+used by the native compiler. *)
+
+let get_load_paths =
+ ref (fun _ -> anomaly "get_load_paths not initialized" : unit -> string list)
+
+let open_header = ["Nativevalues";
+ "Nativecode";
+ "Nativelib";
+ "Nativeconv";
+ "Declaremods"]
+let open_header = List.map mk_open open_header
+
+(* Global settings and utilies for interface with OCaml *)
+let compiler_name =
+ Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ())
+
+let ( / ) a b = Filename.concat a b
+
+(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
+until flags have been properly initialized *)
+let include_dirs () = [Filename.temp_dir_name;
+ coqlib ~fail:Errors.error / "kernel";
+ coqlib ~fail:Errors.error / "library"]
+
+(* Pointer to the function linking an ML object into coq's toplevel *)
+let load_obj = ref (fun x -> () : string -> unit)
+
+let rt1 = ref (dummy_value ())
+let rt2 = ref (dummy_value ())
+
+let get_ml_filename () =
+ let filename = Filename.temp_file "Coq_native" ".ml" in
+ let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in
+ filename, prefix
+
+let write_ml_code ml_filename ?(header=[]) code =
+ let header = open_header@header in
+ let ch_out = open_out ml_filename in
+ let fmt = Format.formatter_of_out_channel ch_out in
+ List.iter (pp_global fmt) (header@code);
+ close_out ch_out
+
+let call_compiler ml_filename load_path =
+ let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in
+ let include_dirs = String.concat " -I " include_dirs in
+ let f = Filename.chop_extension ml_filename in
+ let link_filename = f ^ ".cmo" in
+ let link_filename = Dynlink.adapt_filename link_filename in
+ let comp_cmd =
+ Format.sprintf "%s -%s -o %s -rectypes -w -A -I %s %s"
+ compiler_name (if Dynlink.is_native then "shared" else "c")
+ (Filename.quote link_filename) include_dirs (Filename.quote ml_filename)
+ in
+ let res = Sys.command comp_cmd in
+ Sys.rename (f^".ml") (f^".native");
+ res, link_filename
+
+let compile ml_filename code =
+ write_ml_code ml_filename code;
+ call_compiler ml_filename (!get_load_paths())
+
+let call_linker ~fatal prefix f upds =
+ rt1 := dummy_value ();
+ rt2 := dummy_value ();
+ (try
+ if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
+ register_native_file prefix
+ with | Dynlink.Error e ->
+ let msg = "Dynlink error, " ^ Dynlink.error_message e in
+ if fatal then anomaly msg else Pp.msg_warning (Pp.str msg)
+ | _ -> let msg = "Dynlink error" in
+ if fatal then anomaly msg else Pp.msg_warning (Pp.str msg));
+ match upds with Some upds -> update_locations upds | _ -> ()
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
new file mode 100644
index 0000000000..0cbe4ccd5e
--- /dev/null
+++ b/kernel/nativelib.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Names
+open Term
+open Nativevalues
+open Nativecode
+open Pre_env
+
+(** This file provides facilities to access OCaml compiler and dynamic linker,
+used by the native compiler. *)
+
+val get_load_paths : (unit -> string list) ref
+
+val load_obj : (string -> unit) ref
+
+val get_ml_filename : unit -> string * string
+
+val write_ml_code : string ->
+ ?header:Nativecode.global list -> global list -> unit
+
+val call_compiler : string -> string list -> int * string
+
+val compile : string -> global list -> int * string
+
+val call_linker :
+ fatal:bool -> string -> string -> code_location_updates option -> unit
+
+val rt1 : Nativevalues.t ref
+val rt2 : Nativevalues.t ref
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
new file mode 100644
index 0000000000..c90691ee4b
--- /dev/null
+++ b/kernel/nativelibrary.ml
@@ -0,0 +1,63 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Names
+open Declarations
+open Environ
+open Mod_subst
+open Modops
+open Nativecode
+open Nativelib
+
+(** This file implements separate compilation for libraries in the native
+compiler *)
+
+let rec translate_mod prefix mp env mod_expr acc =
+ match mod_expr with
+ | SEBident mp' -> assert false
+ | SEBstruct msb ->
+ let env' = add_signature mp msb empty_delta_resolver env in
+ List.fold_left (translate_field prefix mp env') acc msb
+ | SEBfunctor (mbid,mtb,meb) -> acc
+ | SEBapply (f,x,_) -> assert false
+ | SEBwith _ -> assert false
+and translate_field prefix mp env (code, values, upds as acc) (l,x) =
+ match x with
+ | SFBconst cb ->
+ let con = make_con mp empty_dirpath l in
+ compile_constant_field (pre_env env) prefix con acc cb
+ | SFBmind mb ->
+ compile_mind_field prefix mp l acc mb
+ | SFBmodule md ->
+ translate_mod prefix md.mod_mp env md.mod_type acc
+ | SFBmodtype mdtyp ->
+ translate_mod prefix mdtyp.typ_mp env mdtyp.typ_expr acc
+
+let dump_library mp dp env mod_expr =
+ if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+ match mod_expr with
+ | SEBstruct msb ->
+ let env = add_signature mp msb empty_delta_resolver env in
+ let prefix = mod_uid_of_dirpath dp ^ "." in
+ let t0 = Sys.time () in
+ let mlcode, values, upds =
+ List.fold_left (translate_field prefix mp env) ([],[],empty_updates)
+ msb
+ in
+ let t1 = Sys.time () in
+ let time_info = Format.sprintf "Compiled library. Time: %.5f@." (t1-.t0) in
+ if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+ List.rev mlcode, Array.of_list (List.rev values), upds
+ | _ -> assert false
+
+
+let compile_library dir code load_path f =
+ let header = mk_library_header dir in
+ let ml_filename = f^".ml" in
+ write_ml_code ml_filename ~header code;
+ fst (call_compiler ml_filename load_path)
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
new file mode 100644
index 0000000000..7b74b00c52
--- /dev/null
+++ b/kernel/nativelibrary.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Names
+open Declarations
+open Environ
+open Nativecode
+
+(** This file implements separate compilation for libraries in the native
+compiler *)
+
+val dump_library : module_path -> dir_path -> env -> struct_expr_body ->
+ global list * symbol array * code_location_updates
+
+val compile_library :
+ dir_path -> global list -> string list -> string -> int
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
new file mode 100644
index 0000000000..fc4255aaf8
--- /dev/null
+++ b/kernel/nativevalues.ml
@@ -0,0 +1,259 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Term
+open Names
+open Errors
+
+(** This modules defines the representation of values internally used by
+the native compiler *)
+
+type t = t -> t
+
+type accumulator (* = t (* a block [0:code;atom;arguments] *) *)
+
+type tag = int
+
+type arity = int
+
+type reloc_table = (tag * arity) array
+
+type annot_sw = {
+ asw_ind : inductive;
+ asw_ci : case_info;
+ asw_reloc : reloc_table;
+ asw_finite : bool;
+ asw_prefix : string
+ }
+
+type sort_annot = string * int
+
+type rec_pos = int array
+
+type atom =
+ | Arel of int
+ | Aconstant of constant
+ | Aind of inductive
+ | Asort of sorts
+ | Avar of identifier
+ | Acase of annot_sw * accumulator * t * (t -> t)
+ | Afix of t array * t array * rec_pos * int
+ | Acofix of t array * t array * int * t
+ | Acofixe of t array * t array * int * t
+ | Aprod of name * t * (t -> t)
+
+let accumulate_tag = 0
+
+let accumulate_code (k:accumulator) (x:t) =
+ let o = Obj.repr k in
+ let osize = Obj.size o in
+ let r = Obj.new_block accumulate_tag (osize + 1) in
+ for i = 0 to osize - 1 do
+ Obj.set_field r i (Obj.field o i)
+ done;
+ Obj.set_field r osize (Obj.repr x);
+ (Obj.obj r:t)
+
+let rec accumulate (x:t) =
+ accumulate_code (Obj.magic accumulate) x
+
+let raccumulate = ref accumulate
+
+let mk_accu_gen rcode (a:atom) =
+(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *)
+ let r = Obj.new_block 0 3 in
+ Obj.set_field r 0 (Obj.field (Obj.magic rcode) 0);
+ Obj.set_field r 1 (Obj.field (Obj.magic rcode) 1);
+ Obj.set_field r 2 (Obj.magic a);
+ (Obj.magic r:t);;
+
+let mk_accu (a:atom) = mk_accu_gen accumulate a
+
+let mk_rel_accu i =
+ mk_accu (Arel i)
+
+let rel_tbl_size = 100
+let rel_tbl = Array.init rel_tbl_size mk_rel_accu
+
+let mk_rel_accu i =
+ if i < rel_tbl_size then rel_tbl.(i)
+ else mk_rel_accu i
+
+let mk_rels_accu lvl len =
+ Array.init len (fun i -> mk_rel_accu (lvl + i))
+
+let napply (f:t) (args: t array) =
+ Array.fold_left (fun f a -> f a) f args
+
+let mk_constant_accu kn =
+ mk_accu (Aconstant kn)
+
+let mk_ind_accu s =
+ mk_accu (Aind s)
+
+let mk_sort_accu s =
+ mk_accu (Asort s)
+
+let mk_var_accu id =
+ mk_accu (Avar id)
+
+let mk_sw_accu annot c p ac =
+ mk_accu (Acase(annot,c,p,ac))
+
+let mk_prod_accu s dom codom =
+ mk_accu (Aprod (s,dom,codom))
+
+let atom_of_accu (k:accumulator) =
+ (Obj.magic (Obj.field (Obj.magic k) 2) : atom)
+
+let set_atom_of_accu (k:accumulator) (a:atom) =
+ Obj.set_field (Obj.magic k) 2 (Obj.magic a)
+
+let accu_nargs (k:accumulator) =
+ let nargs = Obj.size (Obj.magic k) - 3 in
+(* if nargs < 0 then Format.eprintf "nargs = %i\n" nargs; *)
+ assert (nargs >= 0);
+ nargs
+
+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
+
+let is_accu x =
+ let o = Obj.repr x in
+ Obj.is_block o && Obj.tag o = accumulate_tag
+
+(*let accumulate_fix_code (k:accumulator) (a:t) =
+ match atom_of_accu k with
+ | Afix(frec,_,rec_pos,_,_) ->
+ let nargs = accu_nargs k in
+ if nargs <> rec_pos || is_accu a then
+ accumulate_code k a
+ else
+ let r = ref frec in
+ for i = 0 to nargs - 1 do
+ r := !r (arg_of_accu k i)
+ done;
+ !r a
+ | _ -> assert false
+
+
+let rec accumulate_fix (x:t) =
+ accumulate_fix_code (Obj.magic accumulate_fix) x
+
+let raccumulate_fix = ref accumulate_fix *)
+
+let is_atom_fix (a:atom) =
+ match a with
+ | Afix _ -> true
+ | _ -> false
+
+let mk_fix_accu rec_pos pos types bodies =
+ mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos))
+
+let mk_cofix_accu pos types norm =
+ mk_accu_gen accumulate (Acofix(types,norm,pos,(Obj.magic 0 : t)))
+
+let upd_cofix (cofix :t) (cofix_fun : t) =
+ let atom = atom_of_accu (Obj.magic cofix) in
+ match atom with
+ | Acofix (typ,norm,pos,_) ->
+ set_atom_of_accu (Obj.magic cofix) (Acofix(typ,norm,pos,cofix_fun))
+ | _ -> assert false
+
+let force_cofix (cofix : t) =
+ if is_accu cofix then
+ let accu = (Obj.magic cofix : accumulator) in
+ 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));
+ v
+ | Acofixe(_,_,_,v) -> v
+ | _ -> cofix
+ else cofix
+
+let mk_const tag = Obj.magic tag
+
+let mk_block tag args =
+ let nargs = Array.length args in
+ let r = Obj.new_block tag nargs in
+ for i = 0 to nargs - 1 do
+ Obj.set_field r i (Obj.magic args.(i))
+ done;
+ (Obj.magic r : t)
+
+(* Two instances of dummy_value should not be pointer equal, otherwise
+ comparing them as terms would succeed *)
+let dummy_value : unit -> t = fun () _ -> anomaly "Evaluation failed"
+
+let cast_accu v = (Obj.magic v:accumulator)
+
+let mk_int x = Obj.magic x
+
+type block
+
+let block_size (b:block) =
+ Obj.size (Obj.magic b)
+
+let block_field (b:block) i = (Obj.magic (Obj.field (Obj.magic b) i) : t)
+
+let block_tag (b:block) =
+ Obj.tag (Obj.magic b)
+
+type kind_of_value =
+ | Vaccu of accumulator
+ | Vfun of (t -> t)
+ | Vconst of int
+ | Vblock of block
+
+let kind_of_value (v:t) =
+ let o = Obj.repr v in
+ if Obj.is_int o then Vconst (Obj.magic v)
+ else
+ let tag = Obj.tag o in
+ if tag = accumulate_tag then
+ Vaccu (Obj.magic v)
+ else
+ if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
+ else
+ (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag);
+ or ??? what is 1002*)
+ Vfun v
+
+let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
+let bohcnv = Array.init 256 (fun i -> i -
+ (if 0x30 <= i then 0x30 else 0) -
+ (if 0x41 <= i then 0x7 else 0) -
+ (if 0x61 <= i then 0x20 else 0))
+
+let hex_of_bin ch = hobcnv.(int_of_char ch)
+let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1]))
+
+let str_encode expr =
+ let mshl_expr = Marshal.to_string expr [] in
+ let payload = Buffer.create (String.length mshl_expr * 2) in
+ String.iter (fun c -> Buffer.add_string payload (hex_of_bin c)) mshl_expr;
+ Buffer.contents payload
+
+let str_decode s =
+ let mshl_expr_len = String.length s / 2 in
+ let mshl_expr = Buffer.create mshl_expr_len in
+ let buf = String.create 2 in
+ for i = 0 to mshl_expr_len - 1 do
+ String.blit s (2*i) buf 0 2;
+ Buffer.add_char mshl_expr (bin_of_hex buf)
+ done;
+ Marshal.from_string (Buffer.contents mshl_expr) 0
+
+
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
new file mode 100644
index 0000000000..3994f53fd1
--- /dev/null
+++ b/kernel/nativevalues.mli
@@ -0,0 +1,102 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+open Term
+open Names
+
+(** This modules defines the representation of values internally used by
+the native compiler. Be careful when removing apparently dead code from this
+interface, as it may be used by programs generated at runtime. *)
+
+type t = t -> t
+
+type accumulator
+
+type tag = int
+type arity = int
+
+type reloc_table = (tag * arity) array
+
+type annot_sw = {
+ asw_ind : inductive;
+ asw_ci : case_info;
+ asw_reloc : reloc_table;
+ asw_finite : bool;
+ asw_prefix : string
+ }
+
+type sort_annot = string * int
+
+type rec_pos = int array
+
+type atom =
+ | Arel of int
+ | Aconstant of constant
+ | Aind of inductive
+ | Asort of sorts
+ | Avar of identifier
+ | Acase of annot_sw * accumulator * t * (t -> t)
+ | Afix of t array * t array * rec_pos * int
+ | Acofix of t array * t array * int * t
+ | Acofixe of t array * t array * int * t
+ | Aprod of name * t * (t -> t)
+
+(* Constructors *)
+
+val mk_accu : atom -> t
+val mk_rel_accu : int -> t
+val mk_rels_accu : int -> int -> t array
+val mk_constant_accu : constant -> t
+val mk_ind_accu : inductive -> t
+val mk_sort_accu : sorts -> t
+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 upd_cofix : t -> t -> unit
+val force_cofix : t -> t
+val mk_const : tag -> t
+val mk_block : tag -> t array -> t
+
+
+val mk_int : int -> t
+
+val napply : t -> t array -> t
+(* Functions over accumulators *)
+
+val dummy_value : unit -> t
+val atom_of_accu : accumulator -> atom
+val args_of_accu : accumulator -> t list
+val accu_nargs : accumulator -> int
+
+val cast_accu : t -> accumulator
+(* Functions over block: i.e constructors *)
+
+type block
+
+val block_size : block -> int
+val block_field : block -> int -> t
+val block_tag : block -> int
+
+
+
+(* kind_of_value *)
+
+type kind_of_value =
+ | Vaccu of accumulator
+ | Vfun of (t -> t)
+ | Vconst of int
+ | Vblock of block
+
+val kind_of_value : t -> kind_of_value
+
+(* *)
+val is_accu : t -> bool
+
+val str_encode : 'a -> string
+val str_decode : string -> 'a
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 9aa70c9eb3..6a72487495 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -464,6 +464,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 set_nat_conv f = nat_conv := f
+
+let native_conv cv_pb 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
+ end
let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
let set_vm_conv f = vm_conv := f
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index acc97380a1..9d1d125730 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -54,6 +54,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_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
val default_conv : conv_pb -> ?l2r:bool -> types conversion_function
val default_conv_leq : ?l2r:bool -> types conversion_function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 412ccfa31d..d04d3fe783 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -631,6 +631,9 @@ let set_engagement c senv =
type compiled_library =
Dir_path.t * module_body * library_info list * engagement option
+ * Nativecode.symbol array
+
+type native_library = Nativecode.global list
(* We check that only initial state Require's were performed before
[start_library] was called *)
@@ -698,9 +701,16 @@ let export senv dir =
mod_type_alg = None;
mod_constraints = senv.univ;
mod_delta = senv.modinfo.resolver;
- mod_retroknowledge = senv.local_retroknowledge}
+ mod_retroknowledge = senv.local_retroknowledge
+ }
+ in
+ let ast, values =
+ if !Flags.no_native_compiler then [], [||]
+ else let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in
+ Nativecode.update_locations upds;
+ ast, values
in
- mp, (dir,mb,senv.imports,engagement senv.env)
+ mp, (dir,mb,senv.imports,engagement senv.env,values), ast
let check_imports senv needed =
@@ -731,7 +741,7 @@ loaded by side-effect once and for all (like it is done in OCaml).
Would this be correct with respect to undo's and stuff ?
*)
-let import (dp,mb,depends,engmt) digest senv =
+let import (dp,mb,depends,engmt,values) digest senv =
check_imports senv depends;
check_engagement senv.env engmt;
let mp = MPfile dp in
@@ -745,7 +755,7 @@ let import (dp,mb,depends,engmt) digest senv =
resolver =
add_delta_resolver mb.mod_delta senv.modinfo.resolver};
imports = (dp,digest)::senv.imports;
- loads = (mp,mb)::senv.loads }
+ loads = (mp,mb)::senv.loads }, values
(* Store the body of modules' opaque constants inside a table.
@@ -829,7 +839,7 @@ end = struct
| SEBwith (seb,wdcl) ->
SEBwith (traverse_modexpr seb,wdcl)
in
- fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s)
+ fun (dp,mb,depends,s,val_tbl) -> (dp,traverse_module mb,depends,s,val_tbl)
(* To disburden a library from opaque definitions, we simply
traverse it and add an indirection between the module body
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 8f86123c04..7cddde954f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -101,14 +101,16 @@ val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
(** exporting and importing modules *)
type compiled_library
+type native_library = Nativecode.global list
+
val start_library : Dir_path.t -> safe_environment
-> module_path * safe_environment
val export : safe_environment -> Dir_path.t
- -> module_path * compiled_library
+ -> module_path * compiled_library * native_library
val import : compiled_library -> Digest.t -> safe_environment
- -> module_path * safe_environment
+ -> module_path * safe_environment * Nativecode.symbol array
(** Remove the body of opaque constants *)
diff --git a/kernel/term.ml b/kernel/term.ml
index a66e5fb2be..e4657ce28c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -37,7 +37,7 @@ type metavariable = int
(* This defines the strategy to use for verifiying a Cast *)
(* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *)
(* come after the vo-exported cast_kind so as to be compatible with coqchk *)
-type cast_kind = VMcast | DEFAULTcast | REVERTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
(* This defines Cases annotations *)
type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
@@ -155,7 +155,7 @@ let mkSort = function
(* (that means t2 is declared as the type of t1) *)
let mkCast (t1,k2,t2) =
match t1 with
- | Cast (c,k1, _) when k1 == VMcast && k1 == k2 -> Cast (c,k1,t2)
+ | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2)
| _ -> Cast (t1,k2,t2)
(* Constructs the product (x:t1)t2 *)
diff --git a/kernel/term.mli b/kernel/term.mli
index b20e0a1d08..753fc990dd 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -95,8 +95,8 @@ val mkSet : types
val mkType : Univ.universe -> types
-(** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | DEFAULTcast | REVERTcast
+(* This defines the strategy to use for verifiying a Cast *)
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
type t{_ 2} (that means t2 is declared as the type of t1). *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index ccb6a4a7d7..1cd006f25a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -99,11 +99,11 @@ let infer_declaration env dcl =
then OpaqueDef (Declarations.opaque_from_val j.uj_val)
else Def (Declarations.from_val j.uj_val)
in
- def, typ, cst, c.const_entry_secctx
+ def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
| ParameterEntry (ctx,t,nl) ->
let (j,cst) = infer env t in
let t = hcons_constr (Typeops.assumption_of_judgment env j) in
- Undef nl, NonPolymorphicType t, cst, ctx
+ Undef nl, NonPolymorphicType t, cst, false, ctx
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
@@ -113,7 +113,7 @@ let global_vars_set_constant_type env = function
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
-let build_constant_declaration env kn (def,typ,cst,ctx) =
+let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) =
let hyps =
let inferred =
let ids_typ = global_vars_set_constant_type env typ in
@@ -138,7 +138,9 @@ let build_constant_declaration env kn (def,typ,cst,ctx) =
const_body = def;
const_type = typ;
const_body_code = tps;
- const_constraints = cst }
+ const_constraints = cst;
+ const_native_name = ref NotLinked;
+ const_inline_code = inline_code }
(*s Global and local constant declaration. *)
@@ -147,8 +149,8 @@ let translate_constant env kn ce =
let translate_recipe env kn r =
build_constant_declaration env kn
- (let def,typ,cst,hyps = Cooking.cook_constant env r in
- def,typ,cst,Some hyps)
+ (let def,typ,cst,inline,hyps = Cooking.cook_constant env r in
+ def,typ,cst,inline,Some hyps)
(* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c2f046a20f..d001a258eb 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
types * Univ.constraints
val infer_declaration : env -> constant_entry ->
- constant_def * constant_type * constraints * Sign.section_context option
+ constant_def * constant_type * constraints * bool * Sign.section_context option
val build_constant_declaration : env -> 'a ->
- constant_def * constant_type * constraints * Sign.section_context option ->
+ constant_def * constant_type * constraints * bool * Sign.section_context option ->
constant_body
val translate_constant : env -> constant -> constant_entry -> constant_body
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8509edaf95..e611682002 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -280,7 +280,11 @@ let judge_of_cast env cj k tj =
conv_leq false env cj.uj_type expected_type
| REVERTcast ->
cj.uj_val,
- conv_leq true env cj.uj_type expected_type in
+ 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
+ in
{ uj_val = c;
uj_type = expected_type },
cst
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 10:49:27 +0000