aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 17:37:00 +0000
committerGravatar mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-22 17:37:00 +0000
commit6b908b5185a55a27a82c2b0fce4713812adde156 (patch)
treec2857724d8b22ae3d7a91b3a683a57206caf9b54 /kernel
parent62ce65dadb0afb8815b26069246832662846c7ec (diff)
New implementation of the conversion test, using normalization by evaluation to
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
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 2f031c11a..6c22db3a2 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 7adb00da6..03acb87a9 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 bc721dce3..62a3170f2 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 2595aae07..5b5e1750c 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 a32892a41..20742d341 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 ffd588e57..165af63cf 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 872a6c905..07f24583e 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 000000000..d156afc26
--- /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 000000000..0f01ae80e
--- /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 000000000..4ba305660
--- /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 000000000..2cb5ac797
--- /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 000000000..2ca274799
--- /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 000000000..0c454256e
--- /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 000000000..f8474bf19
--- /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 000000000..0cbe4ccd5
--- /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 000000000..c90691ee4
--- /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 000000000..7b74b00c5
--- /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 000000000..fc4255aaf
--- /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 000000000..3994f53fd
--- /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 9aa70c9eb..6a7248749 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 acc97380a..9d1d12573 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 412ccfa31..d04d3fe78 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 8f86123c0..7cddde954 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 a66e5fb2b..e4657ce28 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 b20e0a1d0..753fc990d 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 ccb6a4a7d..1cd006f25 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 c2f046a20..d001a258e 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 8509edaf9..e61168200 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.39.1) at 2024-05-29 12:05:50 +0000