Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

New implementation of the conversion test, using normalization by eva…

…luation 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
  • Loading branch information...
commit 6b908b5185a55a27a82c2b0fce4713812adde156 1 parent 62ce65d
mdenes authored
Showing with 3,705 additions and 89 deletions.
  1. +1 −1  Makefile
  2. +1 −1  Makefile.build
  3. +10 −1 Makefile.common
  4. +6 −0 dev/printers.mllib
  5. +1 −0  dev/top_printers.ml
  6. +1 −0  grammar/q_coqast.ml4
  7. +1 −1  interp/topconstr.ml
  8. +1 −0  intf/genredexpr.mli
  9. +1 −0  intf/misctypes.mli
  10. +1 −1  kernel/cooking.ml
  11. +1 −1  kernel/cooking.mli
  12. +18 −3 kernel/declarations.ml
  13. +14 −1 kernel/declarations.mli
  14. +3 −2 kernel/entries.mli
  15. +2 −1  kernel/indtypes.ml
  16. +6 −0 kernel/kernel.mllib
  17. +1,496 −0 kernel/nativecode.ml
  18. +66 −0 kernel/nativecode.mli
  19. +153 −0 kernel/nativeconv.ml
  20. +15 −0 kernel/nativeconv.mli
  21. +676 −0 kernel/nativelambda.ml
  22. +55 −0 kernel/nativelambda.mli
  23. +91 −0 kernel/nativelib.ml
  24. +34 −0 kernel/nativelib.mli
  25. +63 −0 kernel/nativelibrary.ml
  26. +20 −0 kernel/nativelibrary.mli
  27. +259 −0 kernel/nativevalues.ml
  28. +102 −0 kernel/nativevalues.mli
  29. +10 −0 kernel/reduction.ml
  30. +3 −0  kernel/reduction.mli
  31. +15 −5 kernel/safe_typing.ml
  32. +4 −2 kernel/safe_typing.mli
  33. +2 −2 kernel/term.ml
  34. +2 −2 kernel/term.mli
  35. +8 −6 kernel/term_typing.ml
  36. +2 −2 kernel/term_typing.mli
  37. +5 −1 kernel/typeops.ml
  38. +6 −0 lib/flags.ml
  39. +6 −0 lib/flags.mli
  40. +1 −0  library/declare.ml
  41. +10 −5 library/declaremods.ml
  42. +4 −1 library/declaremods.mli
  43. +2 −2 library/global.ml
  44. +3 −2 library/global.mli
  45. +27 −4 library/library.ml
  46. +4 −0 parsing/g_constr.ml4
  47. +1 −1  parsing/g_ltac.ml4
  48. +2 −0  parsing/g_tactic.ml4
  49. +1 −1  parsing/g_vernac.ml4
  50. +3 −1 plugins/funind/functional_principles_types.ml
  51. +2 −2 plugins/funind/glob_termops.ml
  52. +2 −1  plugins/funind/recdef.ml
  53. +2 −1  plugins/setoid_ring/newring.ml4
  54. +6 −1 pretyping/detyping.ml
  55. +8 −3 pretyping/glob_ops.ml
  56. +2 −0  pretyping/miscops.ml
  57. +347 −0 pretyping/nativenorm.ml
  58. +15 −0 pretyping/nativenorm.mli
  59. +15 −2 pretyping/pretyping.ml
  60. +1 −0  pretyping/pretyping.mllib
  61. +4 −0 pretyping/reductionops.ml
  62. +3 −1 printing/ppconstr.ml
  63. +2 −2 proofs/logic.ml
  64. +2 −1  proofs/proof_global.ml
  65. +13 −1 proofs/redexpr.ml
  66. +3 −1 tactics/leminv.ml
  67. +2 −1  tactics/rewrite.ml4
  68. +1 −0  tactics/tacintern.ml
  69. +2 −0  tactics/tacinterp.ml
  70. +1 −0  tactics/tacsubst.ml
  71. +6 −1 tactics/tactics.ml
  72. +5 −3 toplevel/autoinstance.ml
  73. +3 −1 toplevel/class.ml
  74. +2 −1  toplevel/classes.ml
  75. +11 −5 toplevel/command.ml
  76. +3 −1 toplevel/ind_tables.ml
  77. +3 −1 toplevel/indschemes.ml
  78. +3 −1 toplevel/lemmas.ml
  79. +6 −2 toplevel/mltop.ml
  80. +4 −2 toplevel/obligations.ml
  81. +6 −3 toplevel/record.ml
  82. +1 −1  toplevel/whelp.ml4
2  Makefile
View
@@ -222,7 +222,7 @@ cleanconfig:
distclean: clean cleanconfig
voclean:
- find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
+ find theories plugins test-suite -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" | xargs rm -f
devdocclean:
find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
2  Makefile.build
View
@@ -125,7 +125,7 @@ endif
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
-SYSMOD:=str unix
+SYSMOD:=str unix dynlink
SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
11 Makefile.common
View
@@ -323,9 +323,18 @@ ALLSTDLIB := test-suite/misc/universes/all_stdlib
# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+
ALLMODS:=$(call vo_to_mod,$(ALLVO))
-LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
+LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \
+ $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \
+ $(call vo_to_obj,$(PLUGINSVO))
+
LIBFILESLIGHT:=$(THEORIESLIGHTVO)
###########################################################################
6 dev/printers.mllib
View
@@ -44,14 +44,19 @@ Sign
Cbytecodes
Copcodes
Cemitcodes
+Nativevalues
Declarations
Retroknowledge
Pre_env
+Nativelambda
+Nativecode
+Nativelib
Cbytegen
Environ
Conv_oracle
Closure
Reduction
+Nativeconv
Type_errors
Modops
Inductive
@@ -61,6 +66,7 @@ Cooking
Term_typing
Subtyping
Mod_typing
+Nativelibrary
Safe_typing
Summary
1  dev/top_printers.ml
View
@@ -156,6 +156,7 @@ let cast_kind_display k =
| VMcast -> "VMcast"
| DEFAULTcast -> "DEFAULTcast"
| REVERTcast -> "REVERTcast"
+ | NATIVEcast -> "NATIVEcast"
let constr_display csr =
let rec term_display c = match kind_of_term c with
1  grammar/q_coqast.ml4
View
@@ -196,6 +196,7 @@ let mlexpr_of_red_expr = function
let f = mlexpr_of_list mlexpr_of_occ_constr in
<:expr< Genredexpr.Pattern $f l$ >>
| Genredexpr.CbvVm o -> <:expr< Genredexpr.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
+ | Genredexpr.CbvNative o -> <:expr< Genredexpr.CbvNative $mlexpr_of_option mlexpr_of_occ_constr o$ >>
| Genredexpr.ExtraRedExpr s ->
<:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
2  interp/topconstr.ml
View
@@ -105,7 +105,7 @@ let fold_constr_expr_with_binders g f n acc = function
| CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
| CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a]
- | CCast (loc,a,(CastConv b|CastVM b)) -> f n (f n acc a) b
+ | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
| CCast (loc,a,CastCoerce) -> f n acc a
| CNotation (_,_,(l,ll,bll)) ->
(* The following is an approximation: we don't know exactly if
1  intf/genredexpr.mli
View
@@ -41,6 +41,7 @@ type ('a,'b,'c) red_expr_gen =
| Pattern of 'a Locus.with_occurrences list
| ExtraRedExpr of string
| CbvVm of 'c Locus.with_occurrences option
+ | CbvNative of 'c Locus.with_occurrences option
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
1  intf/misctypes.mli
View
@@ -58,6 +58,7 @@ type 'a cast_type =
| CastConv of 'a
| CastVM of 'a
| CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+ | CastNative of 'a
(** Bindings *)
2  kernel/cooking.ml
View
@@ -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)
2  kernel/cooking.mli
View
@@ -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]. } *)
21 kernel/declarations.ml
View
@@ -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 ->
15 kernel/declarations.mli
View
@@ -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
5 kernel/entries.mli
View
@@ -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 *)
3  kernel/indtypes.ml
View
@@ -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
}
(************************************************************************)
6 kernel/kernel.mllib
View
@@ -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
1,496 kernel/nativecode.ml
View
@@ -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: *)
66 kernel/nativecode.mli
View
@@ -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
153 kernel/nativeconv.ml
View
@@ -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
15 kernel/nativeconv.mli
View
@@ -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
676 kernel/nativelambda.ml
View
@@ -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')