diff options
| author | mdenes | 2013-01-22 17:37:00 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 17:37:00 +0000 |
| commit | 6b908b5185a55a27a82c2b0fce4713812adde156 (patch) | |
| tree | c2857724d8b22ae3d7a91b3a683a57206caf9b54 | |
| parent | 62ce65dadb0afb8815b26069246832662846c7ec (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
82 files changed, 3705 insertions, 89 deletions
@@ -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 diff --git a/Makefile.build b/Makefile.build index 2f0a398f39..661e762dea 100644 --- a/Makefile.build +++ b/Makefile.build @@ -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)) diff --git a/Makefile.common b/Makefile.common index a5b3a29d82..f4731d2789 100644 --- a/Makefile.common +++ b/Makefile.common @@ -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) ########################################################################### diff --git a/dev/printers.mllib b/dev/printers.mllib index 29fa827dca..85e1d6fe65 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -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 diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6e1bf92f5e..aa7d820451 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -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 diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index ec14717305..540e78b0b6 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -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$ >> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 4499791620..54049ac5bc 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -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 diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index 97f9b04848..1096ecb1f8 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -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 diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 3a044018c4..164fd60c9e 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -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 *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2f031c11a0..6c22db3a2c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -151,4 +151,4 @@ let cook_constant env r = let j = make_judge (constr_of_def body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in - (body, typ, cb.const_constraints, const_hyps) + (body, typ, cb.const_constraints, cb.const_inline_code, const_hyps) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7adb00da61..03acb87a91 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type recipe = { val cook_constant : env -> recipe -> - constant_def * constant_type * constraints * Sign.section_context + constant_def * constant_type * constraints * bool * Sign.section_context (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index bc721dce34..62a3170f22 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -83,12 +83,20 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr +type native_name = + | Linked of string + | LinkedLazy of string + | LinkedInteractive of string + | NotLinked + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted; - const_constraints : constraints } + const_constraints : constraints; + const_native_name : native_name ref; + const_inline_code : bool } let body_of_constant cb = match cb.const_body with | Undef _ -> None @@ -131,7 +139,9 @@ let subst_const_body sub cb = { const_body = subst_const_def sub cb.const_body; const_type = subst_const_type sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - const_constraints = cb.const_constraints} + const_constraints = cb.const_constraints; + const_native_name = ref NotLinked; + const_inline_code = cb.const_inline_code } (* Hash-consing of [constant_body] *) @@ -317,6 +327,10 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : constraints; + (* Data for native compilation *) + (* Status of the code (linked or not, and where) *) + mind_native_name : native_name ref; + } let subst_indarity sub = function @@ -353,7 +367,8 @@ let subst_mind sub mib = mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints } + mind_constraints = mib.mind_constraints; + mind_native_name = ref NotLinked } let hcons_indarity = function | Monomorphic a -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2595aae07c..5b5e1750c1 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -62,12 +62,20 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr +type native_name = + | Linked of string + | LinkedLazy of string + | LinkedInteractive of string + | NotLinked + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : to_patch_substituted; - const_constraints : constraints } + const_constraints : constraints; + const_native_name : native_name ref; + const_inline_code : bool } val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body @@ -181,6 +189,11 @@ type mutual_inductive_body = { mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *) +(** {8 Data for native compilation } *) + + mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) + + } val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body diff --git a/kernel/entries.mli b/kernel/entries.mli index a32892a418..20742d3419 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -53,8 +53,9 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; const_entry_secctx : section_context option; - const_entry_type : types option; - const_entry_opaque : bool } + const_entry_type : types option; + const_entry_opaque : bool; + const_entry_inline_code : bool } type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ffd588e57d..165af63cff 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -668,7 +668,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = mind_nparams_rec = nmr; mind_params_ctxt = params; mind_packets = packets; - mind_constraints = cst + mind_constraints = cst; + mind_native_name = ref NotLinked } (************************************************************************) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 872a6c9054..07f24583e1 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -7,14 +7,19 @@ Sign Cbytecodes Copcodes Cemitcodes +Nativevalues Declarations Retroknowledge Pre_env Cbytegen +Nativelambda +Nativecode +Nativelib Environ Conv_oracle Closure Reduction +Nativeconv Type_errors Modops Inductive @@ -24,6 +29,7 @@ Cooking Term_typing Subtyping Mod_typing +Nativelibrary Safe_typing Vm diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml new file mode 100644 index 0000000000..d156afc268 --- /dev/null +++ b/kernel/nativecode.ml @@ -0,0 +1,1496 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Errors +open Term +open Names +open Declarations +open Util +open Nativevalues +open Nativelambda +open Pre_env +open Sign + +(** This file defines the mllambda code generation phase of the native +compiler. mllambda represents a fragment of ML, and can easily be printed +to OCaml code. *) + +(** Local names {{{**) + +type lname = { lname : name; luid : int } + +let dummy_lname = { lname = Anonymous; luid = -1 } + +module LNord = + struct + type t = lname + let compare l1 l2 = l1.luid - l2.luid + end +module LNmap = Map.Make(LNord) +module LNset = Set.Make(LNord) + +let lname_ctr = ref (-1) + +let reset_lname = lname_ctr := -1 + +let fresh_lname n = + incr lname_ctr; + { lname = n; luid = !lname_ctr } + (**}}}**) + +(** Global names {{{ **) +type gname = + | Gind of string * inductive (* prefix, inductive name *) + | Gconstruct of string * constructor (* prefix, constructor name *) + | Gconstant of string * constant (* prefix, constant name *) + | Gcase of label option * int + | Gpred of label option * int + | Gfixtype of label option * int + | Gnorm of label option * int + | Gnormtbl of label option * int + | Ginternal of string + | Grel of int + | Gnamed of identifier + +let case_ctr = ref (-1) + +let reset_gcase () = case_ctr := -1 + +let fresh_gcase l = + incr case_ctr; + Gcase (l,!case_ctr) + +let pred_ctr = ref (-1) + +let reset_gpred () = pred_ctr := -1 + +let fresh_gpred l = + incr pred_ctr; + Gpred (l,!pred_ctr) + +let fixtype_ctr = ref (-1) + +let reset_gfixtype () = fixtype_ctr := -1 + +let fresh_gfixtype l = + incr fixtype_ctr; + Gfixtype (l,!fixtype_ctr) + +let norm_ctr = ref (-1) + +let reset_norm () = norm_ctr := -1 + +let fresh_gnorm l = + incr norm_ctr; + Gnorm (l,!norm_ctr) + +let normtbl_ctr = ref (-1) + +let reset_normtbl () = normtbl_ctr := -1 + +let fresh_gnormtbl l = + incr normtbl_ctr; + Gnormtbl (l,!normtbl_ctr) + (**}}}**) + +(** Symbols (pre-computed values) {{{**) + +let val_ctr = ref (-1) + +type symbol = + | SymbValue of Nativevalues.t + | SymbSort of sorts + | SymbName of name + | SymbConst of constant + | SymbMatch of annot_sw + | SymbInd of inductive + +let get_value tbl i = + match tbl.(i) with + | SymbValue v -> v + | _ -> anomaly "get_value failed" + +let get_sort tbl i = + match tbl.(i) with + | SymbSort s -> s + | _ -> anomaly "get_sort failed" + +let get_name tbl i = + match tbl.(i) with + | SymbName id -> id + | _ -> anomaly "get_name failed" + +let get_const tbl i = + match tbl.(i) with + | SymbConst kn -> kn + | _ -> anomaly "get_const failed" + +let get_match tbl i = + match tbl.(i) with + | SymbMatch case_info -> case_info + | _ -> anomaly "get_match failed" + +let get_ind tbl i = + match tbl.(i) with + | SymbInd ind -> ind + | _ -> anomaly "get_ind failed" + +let symbols_list = ref ([] : symbol list) + +let reset_symbols_list l = + symbols_list := l; + val_ctr := List.length l - 1 + +let push_symbol x = + incr val_ctr; + symbols_list := x :: !symbols_list; + !val_ctr + +let symbols_tbl_name = Ginternal "symbols_tbl" + +let get_symbols_tbl () = Array.of_list (List.rev !symbols_list) +(**}}}**) + +(** Lambda to Mllambda {{{**) + +type primitive = + | Mk_prod + | Mk_sort + | Mk_ind + | Mk_const + | Mk_sw + | Mk_fix of rec_pos * int + | Mk_cofix of int + | Mk_rel of int + | Mk_var of identifier + | Is_accu + | Is_int + | Is_array + | Cast_accu + | Upd_cofix + | Force_cofix + | Val_to_int + | Val_of_int + | Val_of_bool + (* Coq primitive with check *) + | Chead0 of (string * constant) option + | Ctail0 of (string * constant) option + | Cadd of (string * constant) option + | Csub of (string * constant) option + | Cmul of (string * constant) option + | Cdiv of (string * constant) option + | Crem of (string * constant) option + | Clsr of (string * constant) option + | Clsl of (string * constant) option + | Cand of (string * constant) option + | Cor of (string * constant) option + | Cxor of (string * constant) option + | Caddc of (string * constant) option + | Csubc of (string * constant) option + | CaddCarryC of (string * constant) option + | CsubCarryC of (string * constant) option + | Cmulc of (string * constant) option + | Cdiveucl of (string * constant) option + | Cdiv21 of (string * constant) option + | CaddMulDiv of (string * constant) option + | Ceq of (string * constant) option + | Clt of (string * constant) option + | Cle of (string * constant) option + | Clt_b + | Cle_b + | Ccompare of (string * constant) option + | Cprint of (string * constant) option + | Carraymake of (string * constant) option + | Carrayget of (string * constant) option + | Carraydefault of (string * constant) option + | Carrayset of (string * constant) option + | Carraycopy of (string * constant) option + | Carrayreroot of (string * constant) option + | Carraylength of (string * constant) option + | Carrayinit of (string * constant) option + | Carraymap of (string * constant) option + (* Caml primitive *) + | MLand + | MLle + | MLlt + | MLinteq + | MLlsl + | MLlsr + | MLland + | MLlor + | MLlxor + | MLadd + | MLsub + | MLmul + | MLmagic + +type mllambda = + | MLlocal of lname + | MLglobal of gname + | MLprimitive of primitive + | MLlam of lname array * mllambda + | MLletrec of (lname * lname array * mllambda) array * mllambda + | MLlet of lname * mllambda * mllambda + | MLapp of mllambda * mllambda array + | MLif of mllambda * mllambda * mllambda + | MLmatch of annot_sw * mllambda * mllambda * mllam_branches + (* argument, prefix, accu branch, branches *) + | MLconstruct of string * constructor * mllambda array + (* prefix, constructor name, arguments *) + | MLint of bool * int (* true if the type sould be int *) + | MLparray of mllambda array + | MLsetref of string * mllambda + | MLsequence of mllambda * mllambda + +and mllam_branches = ((constructor * lname option array) list * mllambda) array + +let fv_lam l = + let rec aux l bind fv = + match l with + | MLlocal l -> + if LNset.mem l bind then fv else LNset.add l fv + | MLglobal _ | MLprimitive _ | MLint _ -> fv + | MLlam (ln,body) -> + let bind = Array.fold_right LNset.add ln bind in + aux body bind fv + | MLletrec(bodies,def) -> + let bind = + Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in + let fv_body (_,ln,body) fv = + let bind = Array.fold_right LNset.add ln bind in + aux body bind fv in + Array.fold_right fv_body bodies (aux def bind fv) + | MLlet(l,def,body) -> + aux body (LNset.add l bind) (aux def bind fv) + | MLapp(f,args) -> + let fv_arg arg fv = aux arg bind fv in + Array.fold_right fv_arg args (aux f bind fv) + | MLif(t,b1,b2) -> + aux t bind (aux b1 bind (aux b2 bind fv)) + | MLmatch(_,a,p,bs) -> + let fv = aux a bind (aux p bind fv) in + let fv_bs (cargs, body) fv = + let bind = + List.fold_right (fun (_,args) bind -> + Array.fold_right + (fun o bind -> match o with + | Some l -> LNset.add l bind + | _ -> bind) args bind) + cargs bind in + aux body bind fv in + Array.fold_right fv_bs bs fv + (* argument, accu branch, branches *) + | MLconstruct (_,_,p) | MLparray p -> + Array.fold_right (fun a fv -> aux a bind fv) p fv + | MLsetref(_,l) -> aux l bind fv + | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) in + aux l LNset.empty LNset.empty + + +let mkMLlam params body = + if Array.length params = 0 then body + else + match body with + | MLlam (params', body) -> MLlam(Array.append params params', body) + | _ -> MLlam(params,body) + +let mkMLapp f args = + if Array.length args = 0 then f + else + match f with + | MLapp(f,args') -> MLapp(f,Array.append args' args) + | _ -> MLapp(f,args) + +let empty_params = [||] + +let decompose_MLlam c = + match c with + | MLlam(ids,c) -> ids,c + | _ -> empty_params,c + +(*s Global declaration *) +type global = +(* | Gtblname of gname * identifier array *) + | Gtblnorm of gname * lname array * mllambda array + | Gtblfixtype of gname * lname array * mllambda array + | Glet of gname * mllambda + | Gletcase of + gname * lname array * annot_sw * mllambda * mllambda * mllam_branches + | Gopen of string + | Gtype of inductive * int array + (* ind name, arities of constructors *) + +let global_stack = ref ([] : global list) + +let push_global_let gn body = + global_stack := Glet(gn,body) :: !global_stack + +let push_global_fixtype gn params body = + global_stack := Gtblfixtype(gn,params,body) :: !global_stack + +let push_global_norm name params body = + global_stack := Gtblnorm(name, params, body)::!global_stack + +let push_global_case name params annot a accu bs = + global_stack := Gletcase(name,params, annot, a, accu, bs)::!global_stack + +(*s Compilation environment *) + +type env = + { env_rel : mllambda list; (* (MLlocal lname) list *) + env_bound : int; (* length of env_rel *) + (* free variables *) + env_urel : (int * mllambda) list ref; (* list of unbound rel *) + env_named : (identifier * mllambda) list ref } + +let empty_env () = + { env_rel = []; + env_bound = 0; + env_urel = ref []; + env_named = ref [] + } + +let push_rel env id = + let local = fresh_lname id in + local, { env with + env_rel = MLlocal local :: env.env_rel; + env_bound = env.env_bound + 1 + } + +let push_rels env ids = + let lnames, env_rel = + Array.fold_left (fun (names,env_rel) id -> + let local = fresh_lname id in + (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in + Array.of_list (List.rev lnames), { env with + env_rel = env_rel; + env_bound = env.env_bound + Array.length ids + } + +let get_rel env id i = + if i <= env.env_bound then + List.nth env.env_rel (i-1) + else + let i = i - env.env_bound in + try List.assoc i !(env.env_urel) + with Not_found -> + let local = MLlocal (fresh_lname id) in + env.env_urel := (i,local) :: !(env.env_urel); + local + +let get_var env id = + try List.assoc id !(env.env_named) + with Not_found -> + let local = MLlocal (fresh_lname (Name id)) in + env.env_named := (id, local)::!(env.env_named); + local + +(*s Traduction of lambda to mllambda *) + +let get_prod_name codom = + match codom with + | MLlam(ids,_) -> ids.(0).lname + | _ -> assert false + +let get_lname (_,l) = + match l with + | MLlocal id -> id + | _ -> raise (Invalid_argument "Nativecode.get_lname") + +let fv_params env = + let fvn, fvr = !(env.env_named), !(env.env_urel) in + let size = List.length fvn + List.length fvr in + if size = 0 then empty_params + else begin + let params = Array.make size dummy_lname in + let fvn = ref fvn in + let i = ref 0 in + while !fvn <> [] do + params.(!i) <- get_lname (List.hd !fvn); + fvn := List.tl !fvn; + incr i + done; + let fvr = ref fvr in + while !fvr <> [] do + params.(!i) <- get_lname (List.hd !fvr); + fvr := List.tl !fvr; + incr i + done; + params + end + +let generalize_fv env body = + mkMLlam (fv_params env) body + +let empty_args = [||] + +let fv_args env fvn fvr = + let size = List.length fvn + List.length fvr in + if size = 0 then empty_args + else + begin + let args = Array.make size (MLint (false,0)) in + let fvn = ref fvn in + let i = ref 0 in + while !fvn <> [] do + args.(!i) <- get_var env (fst (List.hd !fvn)); + fvn := List.tl !fvn; + incr i + done; + let fvr = ref fvr in + while !fvr <> [] do + let (k,_ as kml) = List.hd !fvr in + let n = get_lname kml in + args.(!i) <- get_rel env n.lname k; + fvr := List.tl !fvr; + incr i + done; + args + end + +let get_value_code i = + MLapp (MLglobal (Ginternal "get_value"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +let get_sort_code i = + MLapp (MLglobal (Ginternal "get_sort"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +let get_name_code i = + MLapp (MLglobal (Ginternal "get_name"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +let get_const_code i = + MLapp (MLglobal (Ginternal "get_const"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +let get_match_code i = + MLapp (MLglobal (Ginternal "get_match"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +let get_ind_code i = + MLapp (MLglobal (Ginternal "get_ind"), [|MLglobal symbols_tbl_name;MLint(true,i)|]) + +type rlist = + | Rnil + | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' +and rlist' = rlist ref + +let rm_params fv params = + Array.map (fun l -> if LNset.mem l fv then Some l else None) params + +let rec insert cargs body rl = + match !rl with + | Rnil -> + let fv = fv_lam body in + let (c,params) = cargs in + let params = rm_params fv params in + rl:= Rcons(ref [(c,params)], fv, body, ref Rnil) + | Rcons(l,fv,body',rl) -> + if body = body' then + let (c,params) = cargs in + let params = rm_params fv params in + l := (c,params)::!l + else insert cargs body rl + +let rec to_list rl = + match !rl with + | Rnil -> [] + | Rcons(l,_,body,tl) -> (!l,body)::to_list tl + +let merge_branches t = + let newt = ref Rnil in + Array.iter (fun (c,args,body) -> insert (c,args) body newt) t; + Array.of_list (to_list newt) + + let rec ml_of_lam env l t = + match t with + | Lrel(id ,i) -> get_rel env id i + | Lvar id -> get_var env id + | Lprod(dom,codom) -> + let dom = ml_of_lam env l dom in + let codom = ml_of_lam env l codom in + let n = get_prod_name codom in + let i = push_symbol (SymbName n) in + MLapp(MLprimitive Mk_prod, [|get_name_code i;dom;codom|]) + | Llam(ids,body) -> + let lnames,env = push_rels env ids in + MLlam(lnames, ml_of_lam env l body) + | Lrec(id,body) -> + let ids,body = decompose_Llam body in + let lname, env = push_rel env id in + let lnames, env = push_rels env ids in + MLletrec([|lname, lnames, ml_of_lam env l body|], MLlocal lname) + | Llet(id,def,body) -> + let def = ml_of_lam env l def in + let lname, env = push_rel env id in + let body = ml_of_lam env l body in + MLlet(lname,def,body) + | Lapp(f,args) -> + MLapp(ml_of_lam env l f, Array.map (ml_of_lam env l) args) + | Lconst (prefix,c) -> MLglobal(Gconstant (prefix,c)) + | Lcase (annot,p,a,bs) -> + (* let predicate_uid fv_pred = compilation of p + let rec case_uid fv a_uid = + match a_uid with + | Accu _ => mk_sw (predicate_uid fv_pred) (case_uid fv) a_uid + | Ci argsi => compilation of branches + compile case = case_uid fv (compilation of a) *) + (* Compilation of the predicate *) + (* Remark: if we do not want to compile the predicate we + should a least compute the fv, then store the lambda representation + of the predicate (not the mllambda) *) + let env_p = empty_env () in + let pn = fresh_gpred l in + let mlp = ml_of_lam env_p l p in + let mlp = generalize_fv env_p mlp in + let (pfvn,pfvr) = !(env_p.env_named), !(env_p.env_urel) in + push_global_let pn mlp; + (* Compilation of the case *) + let env_c = empty_env () in + let a_uid = fresh_lname Anonymous in + let la_uid = MLlocal a_uid in + (* compilation of branches *) + let ml_br (c,params, body) = + let lnames, env = push_rels env_c params in + (c, lnames, ml_of_lam env l body) in + let bs = Array.map ml_br bs in + let cn = fresh_gcase l in + (* Compilation of accu branch *) + let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in + let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in + let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in + (* remark : the call to fv_args does not add free variables in env_c *) + let i = push_symbol (SymbMatch annot) in + let accu = + MLapp(MLprimitive Mk_sw, + [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]); + pred; + cn_fv |]) in +(* let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in + let case = generalize_fv env_c body in *) + push_global_case cn + (Array.append (fv_params env_c) [|a_uid|]) annot la_uid accu (merge_branches bs); + + (* Final result *) + let arg = ml_of_lam env l a in + let force = + if annot.asw_finite then arg + else MLapp(MLprimitive Force_cofix, [|arg|]) in + mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] + | Lareint args -> + let res = ref (MLapp(MLprimitive Is_int, [|ml_of_lam env l args.(0)|]))in + for i = 1 to Array.length args - 1 do + let t = MLapp(MLprimitive Is_int, [|ml_of_lam env l args.(i)|]) in + res := MLapp(MLprimitive MLand, [|!res;t|]) + done; + !res + | Lif(t,bt,bf) -> + MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) + | Lfix ((rec_pos,start), (ids, tt, tb)) -> + (* let type_f fvt = [| type fix |] + let norm_f1 fv f1 .. fn params1 = body1 + .. + let norm_fn fv f1 .. fn paramsn = bodyn + let norm fv f1 .. fn = + [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|] + compile fix = + let rec f1 params1 = + if is_accu rec_pos.(1) then mk_fix (type_f fvt) (norm fv) params1 + else norm_f1 fv f1 .. fn params1 + and .. and fn paramsn = + if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn + else norm_fn fv f1 .. fv paramsn in + start + *) + (* Compilation of type *) + let env_t = empty_env () in + let ml_t = Array.map (ml_of_lam env_t l) tt in + let params_t = fv_params env_t in + let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in + let gft = fresh_gfixtype l in + push_global_fixtype gft params_t ml_t; + let mk_type = MLapp(MLglobal gft, args_t) in + (* Compilation of norm_i *) + let ndef = Array.length ids in + let lf,env_n = push_rels (empty_env ()) ids in + let t_params = Array.make ndef [||] in + let t_norm_f = Array.make ndef (Gnorm (l,-1)) in + let ml_of_fix i body = + let idsi,bodyi = decompose_Llam body in + let paramsi, envi = push_rels env_n idsi in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + mkMLlam paramsi bodyi in + let tnorm = Array.mapi ml_of_fix tb in + let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in + let fv_params = fv_params env_n in + let fv_args' = Array.map (fun id -> MLlocal id) fv_params in + let norm_params = Array.append fv_params lf in + Array.iteri (fun i body -> + push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm; + let norm = fresh_gnormtbl l in + push_global_norm norm fv_params + (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f); + (* Compilation of fix *) + let fv_args = fv_args env fvn fvr in + let lf, env = push_rels env ids in + let lf_args = Array.map (fun id -> MLlocal id) lf in + let mk_norm = MLapp(MLglobal norm, fv_args) in + let mkrec i lname = + let paramsi = t_params.(i) in + let reci = MLlocal (paramsi.(rec_pos.(i))) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let body = + MLif(MLapp(MLprimitive Is_accu,[|reci|]), + mkMLapp + (MLapp(MLprimitive (Mk_fix(rec_pos,i)), + [|mk_type; mk_norm|])) + pargsi, + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi])) + in + (lname, paramsi, body) in + MLletrec(Array.mapi mkrec lf, lf_args.(start)) + | Lcofix (start, (ids, tt, tb)) -> + (* Compilation of type *) + let env_t = empty_env () in + let ml_t = Array.map (ml_of_lam env_t l) tt in + let params_t = fv_params env_t in + let args_t = fv_args env !(env_t.env_named) !(env_t.env_urel) in + let gft = fresh_gfixtype l in + push_global_fixtype gft params_t ml_t; + let mk_type = MLapp(MLglobal gft, args_t) in + (* Compilation of norm_i *) + let ndef = Array.length ids in + let lf,env_n = push_rels (empty_env ()) ids in + let t_params = Array.make ndef [||] in + let t_norm_f = Array.make ndef (Gnorm (l,-1)) in + let ml_of_fix i body = + let idsi,bodyi = decompose_Llam body in + let paramsi, envi = push_rels env_n idsi in + t_norm_f.(i) <- fresh_gnorm l; + let bodyi = ml_of_lam envi l bodyi in + t_params.(i) <- paramsi; + mkMLlam paramsi bodyi in + let tnorm = Array.mapi ml_of_fix tb in + let fvn,fvr = !(env_n.env_named), !(env_n.env_urel) in + let fv_params = fv_params env_n in + let fv_args' = Array.map (fun id -> MLlocal id) fv_params in + let norm_params = Array.append fv_params lf in + Array.iteri (fun i body -> + push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm; + let norm = fresh_gnormtbl l in + push_global_norm norm fv_params + (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f); + (* Compilation of fix *) + let fv_args = fv_args env fvn fvr in + let mk_norm = MLapp(MLglobal norm, fv_args) in + let lnorm = fresh_lname Anonymous in + let ltype = fresh_lname Anonymous in + let lf, env = push_rels env ids in + let lf_args = Array.map (fun id -> MLlocal id) lf in + let upd i lname cont = + let paramsi = t_params.(i) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let uniti = fresh_lname Anonymous in + let body = + MLlam(Array.append paramsi [|uniti|], + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi])) in + MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]), + cont) in + let upd = Array.fold_right_i upd lf lf_args.(start) in + let mk_let i lname cont = + MLlet(lname, + MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]), + cont) in + let init = Array.fold_right_i mk_let lf upd in + MLlet(lnorm, mk_norm, MLlet(ltype, mk_type, init)) + (* + let mkrec i lname = + let paramsi = t_params.(i) in + let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let uniti = fresh_lname Anonymous in + let body = + MLapp( MLprimitive(Mk_cofix i), + [|mk_type;mk_norm; + MLlam([|uniti|], + MLapp(MLglobal t_norm_f.(i), + Array.concat [fv_args;lf_args;pargsi]))|]) in + (lname, paramsi, body) in + MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) + + | Lmakeblock (prefix,cn,_,args) -> + MLconstruct(prefix,cn,Array.map (ml_of_lam env l) args) + | Lconstruct (prefix, cn) -> + MLglobal (Gconstruct (prefix, cn)) + | Lval v -> + let i = push_symbol (SymbValue v) in get_value_code i + | Lsort s -> + let i = push_symbol (SymbSort s) in + MLapp(MLprimitive Mk_sort, [|get_sort_code i|]) + | Lind (prefix, ind) -> MLglobal (Gind (prefix, ind)) + | Llazy -> MLglobal (Ginternal "lazy") + | Lforce -> MLglobal (Ginternal "Lazy.force") + +let mllambda_of_lambda auxdefs l t = + let env = empty_env () in + global_stack := auxdefs; + let ml = ml_of_lam env l t in + let fv_rel = !(env.env_urel) in + let fv_named = !(env.env_named) in + (* build the free variables *) + let get_lname (_,t) = + match t with + | MLlocal x -> x + | _ -> assert false in + let params = + List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in + if params = [] then + (!global_stack, ([],[]), ml) + (* final result : global list, fv, ml *) + else + (!global_stack, (fv_named, fv_rel), mkMLlam (Array.of_list params) ml) + (**}}}**) + +(** Code optimization {{{**) + +(** Optimization of match and fix *) + +let can_subst l = + match l with + | MLlocal _ | MLint _ | MLglobal _ -> true + | _ -> false + +let subst s l = + if LNmap.is_empty s then l + else + let rec aux l = + match l with + | MLlocal id -> (try LNmap.find id s with _ -> l) + | MLglobal _ | MLprimitive _ | MLint _ -> l + | MLlam(params,body) -> MLlam(params, aux body) + | MLletrec(defs,body) -> + let arec (f,params,body) = (f,params,aux body) in + MLletrec(Array.map arec defs, aux body) + | MLlet(id,def,body) -> MLlet(id,aux def, aux body) + | MLapp(f,args) -> MLapp(aux f, Array.map aux args) + | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2) + | MLmatch(annot,a,accu,bs) -> + let auxb (cargs,body) = (cargs,aux body) in + MLmatch(annot,a,aux accu, Array.map auxb bs) + | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args) + | MLparray p -> MLparray(Array.map aux p) + | MLsetref(s,l1) -> MLsetref(s,aux l1) + | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) + in + aux l + +let add_subst id v s = + match v with + | MLlocal id' when id.luid = id'.luid -> s + | _ -> LNmap.add id v s + +let subst_norm params args s = + let len = Array.length params in + assert (Array.length args = len && Array.for_all can_subst args); + let s = ref s in + for i = 0 to len - 1 do + s := add_subst params.(i) args.(i) !s + done; + !s + +let subst_case params args s = + let len = Array.length params in + assert (len > 0 && + Array.length args = len && + let r = ref true and i = ref 0 in + (* we test all arguments excepted the last *) + while !i < len - 1 && !r do r := can_subst args.(!i); incr i done; + !r); + let s = ref s in + for i = 0 to len - 2 do + s := add_subst params.(i) args.(i) !s + done; + !s, params.(len-1), args.(len-1) + +let empty_gdef = Int.Map.empty, Int.Map.empty +let get_norm (gnorm, _) i = Int.Map.find i gnorm +let get_case (_, gcase) i = Int.Map.find i gcase + +let all_lam n bs = + let f (_, l) = + match l with + | MLlam(params, _) -> Array.length params = n + | _ -> false in + Array.for_all f bs + +let commutative_cut annot a accu bs args = + let mkb (c,b) = + match b with + | MLlam(params, body) -> + (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args) + | _ -> assert false in + MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs) + +let optimize gdef l = + let rec optimize s l = + match l with + | MLlocal id -> (try LNmap.find id s with _ -> l) + | MLglobal _ | MLprimitive _ | MLint _ -> l + | MLlam(params,body) -> + MLlam(params, optimize s body) + | MLletrec(decls,body) -> + let opt_rec (f,params,body) = (f,params,optimize s body ) in + MLletrec(Array.map opt_rec decls, optimize s body) + | MLlet(id,def,body) -> + let def = optimize s def in + if can_subst def then optimize (add_subst id def s) body + else MLlet(id,def,optimize s body) + | MLapp(f, args) -> + let args = Array.map (optimize s) args in + begin match f with + | MLglobal (Gnorm (_,i)) -> + (try + let params,body = get_norm gdef i in + let s = subst_norm params args s in + optimize s body + with Not_found -> MLapp(optimize s f, args)) + | MLglobal (Gcase (_,i)) -> + (try + let params,body = get_case gdef i in + let s, id, arg = subst_case params args s in + if can_subst arg then optimize (add_subst id arg s) body + else MLlet(id, arg, optimize s body) + with Not_found -> MLapp(optimize s f, args)) + | _ -> + let f = optimize s f in + match f with + | MLmatch (annot,a,accu,bs) -> + if all_lam (Array.length args) bs then + commutative_cut annot a accu bs args + else MLapp(f, args) + | _ -> MLapp(f, args) + + end + | MLif(t,b1,b2) -> + let t = optimize s t in + let b1 = optimize s b1 in + let b2 = optimize s b2 in + begin match t, b2 with + | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + when l1 = l2 -> MLmatch(annot, l1, b1, bs) + | _, _ -> MLif(t, b1, b2) + end + | MLmatch(annot,a,accu,bs) -> + let opt_b (cargs,body) = (cargs,optimize s body) in + MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs) + | MLconstruct(prefix,c,args) -> + MLconstruct(prefix,c,Array.map (optimize s) args) + | MLparray p -> MLparray (Array.map (optimize s) p) + | MLsetref(r,l) -> MLsetref(r, optimize s l) + | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) + in + optimize LNmap.empty l + +let optimize_stk stk = + let add_global gdef g = + match g with + | Glet (Gnorm (_,i), body) -> + let (gnorm, gcase) = gdef in + (Int.Map.add i (decompose_MLlam body) gnorm, gcase) + | Gletcase(Gcase (_,i), params, annot,a,accu,bs) -> + let (gnorm,gcase) = gdef in + (gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase) + | Gletcase _ -> assert false + | _ -> gdef in + let gdef = List.fold_left add_global empty_gdef stk in + let optimize_global g = + match g with + | Glet(Gconstant (prefix, c), body) -> + Glet(Gconstant (prefix, c), optimize gdef body) + | _ -> g in + List.map optimize_global stk + (**}}}**) + +(** Printing to ocaml {{{**) +(* Redefine a bunch of functions in module Names to generate names + acceptable to OCaml. *) +let string_of_id s = Unicode.ascii_of_ident (string_of_id s) +let string_of_label l = Unicode.ascii_of_ident (string_of_label l) + +let string_of_dirpath = function + | [] -> "_" + | sl -> String.concat "_" (List.map string_of_id (List.rev sl)) + +(* The first letter of the file name has to be a capital to be accepted by *) +(* OCaml as a module identifier. *) +let string_of_dirpath s = "N"^string_of_dirpath s + +let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir) + +let string_of_name x = + match x with + | Anonymous -> "anonymous" (* assert false *) + | Name id -> string_of_id id + +let string_of_label_def l = + match l with + | None -> "" + | Some l -> string_of_label l + +(* Relativization of module paths *) +let rec list_of_mp acc = function + | MPdot (mp,l) -> list_of_mp (string_of_label l::acc) mp + | MPfile dp -> + let dp = repr_dirpath dp in + string_of_dirpath dp :: acc + | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc + +let list_of_mp mp = list_of_mp [] mp + +let string_of_kn kn = + let (mp,dp,l) = repr_kn kn in + let mp = list_of_mp mp in + String.concat "_" mp ^ "_" ^ string_of_label l + +let string_of_con c = string_of_kn (user_con c) +let string_of_mind mind = string_of_kn (user_mind mind) + +let string_of_gname g = + match g with + | Gind (prefix, (mind, i)) -> + Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i + | Gconstruct (prefix, ((mind, i), j)) -> + Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) + | Gconstant (prefix, c) -> + Format.sprintf "%sconst_%s" prefix (string_of_con c) + | Gcase (l,i) -> + Format.sprintf "case_%s_%i" (string_of_label_def l) i + | Gpred (l,i) -> + Format.sprintf "pred_%s_%i" (string_of_label_def l) i + | Gfixtype (l,i) -> + Format.sprintf "fixtype_%s_%i" (string_of_label_def l) i + | Gnorm (l,i) -> + Format.sprintf "norm_%s_%i" (string_of_label_def l) i + | Ginternal s -> Format.sprintf "%s" s + | Gnormtbl (l,i) -> + Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i + | Grel i -> + Format.sprintf "rel_%i" i + | Gnamed id -> + Format.sprintf "named_%s" (string_of_id id) + +let pp_gname fmt g = + Format.fprintf fmt "%s" (string_of_gname g) + +let pp_lname fmt ln = + let s = Unicode.ascii_of_ident (string_of_name ln.lname) in + Format.fprintf fmt "x_%s_%i" s ln.luid + +let pp_ldecls fmt ids = + let len = Array.length ids in + for i = 0 to len - 1 do + Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i) + done + +let string_of_construct prefix ((mind,i),j) = + let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in + prefix ^ id + +let pp_int fmt i = + if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i + +let pp_mllam fmt l = + + let rec pp_mllam fmt l = + match l with + | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln + | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g + | MLprimitive p -> Format.fprintf fmt "@[%a@]" pp_primitive p + | MLlam(ids,body) -> + Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]" + pp_ldecls ids pp_mllam body + | MLletrec(defs, body) -> + Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs + pp_mllam body + | MLlet(id,def,body) -> + Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]" + pp_lname id pp_mllam def pp_mllam body + | MLapp(f, args) -> + Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args + | MLif(t,l1,l2) -> + Format.fprintf fmt "@[(if %a then@\n %a@\nelse@\n %a)@]" + pp_mllam t pp_mllam l1 pp_mllam l2 + | MLmatch (asw, c, accu_br, br) -> + let mind,i = asw.asw_ind in + let prefix = asw.asw_prefix in + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]" + pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br + + | MLconstruct(prefix,c,args) -> + Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" + (string_of_construct prefix c) pp_cargs args + | MLint(int, i) -> + if int then pp_int fmt i + else Format.fprintf fmt "(val_of_int %a)" pp_int i + | MLparray p -> + Format.fprintf fmt "@[(parray_of_array@\n [|"; + for i = 0 to Array.length p - 2 do + Format.fprintf fmt "%a;" pp_mllam p.(i) + done; + Format.fprintf fmt "%a|])@]" pp_mllam p.(Array.length p - 1) + | MLsetref (s, body) -> + Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body + | MLsequence(l1,l2) -> + Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2 + + and pp_letrec fmt defs = + let len = Array.length defs in + let pp_one_rec i (fn, argsn, body) = + Format.fprintf fmt "%a%a =@\n %a" + pp_lname fn + pp_ldecls argsn pp_mllam body in + Format.fprintf fmt "@[let rec "; + pp_one_rec 0 defs.(0); + for i = 1 to len - 1 do + Format.fprintf fmt "@\nand "; + pp_one_rec i defs.(i) + done; + + and pp_blam fmt l = + match l with + | MLprimitive (Mk_prod | Mk_sort) + | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ -> + Format.fprintf fmt "(%a)" pp_mllam l + | MLconstruct(_,_,args) when Array.length args > 0 -> + Format.fprintf fmt "(%a)" pp_mllam l + | _ -> pp_mllam fmt l + + and pp_args sep fmt args = + let sep = if sep then " " else "," in + let len = Array.length args in + if len > 0 then begin + Format.fprintf fmt "%a" pp_blam args.(0); + for i = 1 to len - 1 do + Format.fprintf fmt "%s%a" sep pp_blam args.(i) + done + end + + and pp_cargs fmt args = + let len = Array.length args in + match len with + | 0 -> () + | 1 -> Format.fprintf fmt " %a" pp_blam args.(0) + | _ -> Format.fprintf fmt "(%a)" (pp_args false) args + + and pp_cparam fmt param = + match param with + | Some l -> pp_mllam fmt (MLlocal l) + | None -> Format.fprintf fmt "_" + + and pp_cparams fmt params = + let len = Array.length params in + match len with + | 0 -> () + | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0) + | _ -> + let aux fmt params = + Format.fprintf fmt "%a" pp_cparam params.(0); + for i = 1 to len - 1 do + Format.fprintf fmt ",%a" pp_cparam params.(i) + done in + Format.fprintf fmt "(%a)" aux params + + and pp_branches prefix fmt bs = + let pp_branch (cargs,body) = + let pp_c fmt (cn,args) = + Format.fprintf fmt "| %s%a " + (string_of_construct prefix cn) pp_cparams args in + let rec pp_cargs fmt cargs = + match cargs with + | [] -> () + | cargs::cargs' -> + Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in + Format.fprintf fmt "%a ->@\n %a@\n" + pp_cargs cargs pp_mllam body + in + Array.iter pp_branch bs + + and pp_vprim o s = + match o with + | None -> Format.fprintf fmt "no_check_%s" s + | Some (prefix,kn) -> + Format.fprintf fmt "%s %a" s pp_mllam (MLglobal (Gconstant (prefix,kn))) + + and pp_primitive fmt = function + | Mk_prod -> Format.fprintf fmt "mk_prod_accu" + | Mk_sort -> Format.fprintf fmt "mk_sort_accu" + | Mk_ind -> Format.fprintf fmt "mk_ind_accu" + | Mk_const -> Format.fprintf fmt "mk_constant_accu" + | Mk_sw -> Format.fprintf fmt "mk_sw_accu" + | Mk_fix(rec_pos,start) -> + let pp_rec_pos fmt rec_pos = + Format.fprintf fmt "@[[| %i" rec_pos.(0); + for i = 1 to Array.length rec_pos - 1 do + Format.fprintf fmt "; %i" rec_pos.(i) + done; + Format.fprintf fmt " |]@]" in + Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start + | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start + | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i + | Mk_var id -> + Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) + | Is_accu -> Format.fprintf fmt "is_accu" + | Is_int -> Format.fprintf fmt "is_int" + | Is_array -> Format.fprintf fmt "is_parray" + | Cast_accu -> Format.fprintf fmt "cast_accu" + | Upd_cofix -> Format.fprintf fmt "upd_cofix" + | Force_cofix -> Format.fprintf fmt "force_cofix" + | Val_to_int -> Format.fprintf fmt "val_to_int" + | Val_of_int -> Format.fprintf fmt "val_of_int" + | Val_of_bool -> Format.fprintf fmt "of_bool" + | Chead0 o -> pp_vprim o "head0" + | Ctail0 o -> pp_vprim o "tail0" + | Cadd o -> pp_vprim o "add" + | Csub o -> pp_vprim o "sub" + | Cmul o -> pp_vprim o "mul" + | Cdiv o -> pp_vprim o "div" + | Crem o -> pp_vprim o "rem" + | Clsr o -> pp_vprim o "l_sr" + | Clsl o -> pp_vprim o "l_sl" + | Cand o -> pp_vprim o "l_and" + | Cor o -> pp_vprim o "l_or" + | Cxor o -> pp_vprim o "l_xor" + | Caddc o -> pp_vprim o "addc" + | Csubc o -> pp_vprim o "subc" + | CaddCarryC o -> pp_vprim o "addCarryC" + | CsubCarryC o -> pp_vprim o "subCarryC" + | Cmulc o -> pp_vprim o "mulc" + | Cdiveucl o -> pp_vprim o "diveucl" + | Cdiv21 o -> pp_vprim o "div21" + | CaddMulDiv o -> pp_vprim o "addMulDiv" + | Ceq o -> pp_vprim o "eq" + | Clt o -> pp_vprim o "lt" + | Cle o -> pp_vprim o "le" + | Clt_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<)" else Format.fprintf fmt "lt_b" + | Cle_b -> if Sys.word_size = 64 then Format.fprintf fmt "(<=)" else Format.fprintf fmt "le_b" + | Ccompare o -> pp_vprim o "compare" + | Cprint o -> pp_vprim o "print" + | Carraymake o -> pp_vprim o "arraymake" + | Carrayget o -> pp_vprim o "arrayget" + | Carraydefault o -> pp_vprim o "arraydefault" + | Carrayset o -> pp_vprim o "arrayset" + | Carraycopy o -> pp_vprim o "arraycopy" + | Carrayreroot o -> pp_vprim o "arrayreroot" + | Carraylength o -> pp_vprim o "arraylength" + | Carrayinit o -> pp_vprim o "arrayinit" + | Carraymap o -> pp_vprim o "arraymap" + (* Caml primitive *) + | MLand -> Format.fprintf fmt "(&&)" + | MLle -> Format.fprintf fmt "(<=)" + | MLlt -> Format.fprintf fmt "(<)" + | MLinteq -> Format.fprintf fmt "(==)" + | MLlsl -> Format.fprintf fmt "(lsl)" + | MLlsr -> Format.fprintf fmt "(lsr)" + | MLland -> Format.fprintf fmt "(land)" + | MLlor -> Format.fprintf fmt "(lor)" + | MLlxor -> Format.fprintf fmt "(lxor)" + | MLadd -> Format.fprintf fmt "(+)" + | MLsub -> Format.fprintf fmt "(-)" + | MLmul -> Format.fprintf fmt "( * )" + | MLmagic -> Format.fprintf fmt "Obj.magic" + + in + Format.fprintf fmt "@[%a@]" pp_mllam l + +let pp_array fmt t = + let len = Array.length t in + Format.fprintf fmt "@[[|"; + for i = 0 to len - 2 do + Format.fprintf fmt "%a; " pp_mllam t.(i) + done; + if len > 0 then + Format.fprintf fmt "%a" pp_mllam t.(len - 1); + Format.fprintf fmt "|]@]" + +let pp_global fmt g = + match g with + | Glet (gn, c) -> + let ids, c = decompose_MLlam c in + Format.fprintf fmt "@[let %a%a =@\n %a@]@\n@." pp_gname gn + pp_ldecls ids + pp_mllam c + | Gopen s -> + Format.fprintf fmt "@[open %s@]@." s + | Gtype ((mind, i), lar) -> + let l = string_of_mind mind in + let rec aux s ar = + if ar = 0 then s else aux (s^" * Nativevalues.t") (ar-1) in + let pp_const_sig i fmt j ar = + let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in + Format.fprintf fmt " | Construct_%s_%i_%i %s@\n" l i j sig_str + in + let pp_const_sigs i fmt lar = + Format.fprintf fmt " | Accu_%s_%i of Nativevalues.t@\n" l i; + Array.iteri (pp_const_sig i fmt) lar + in + Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar + | Gtblfixtype (g, params, t) -> + Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g + pp_ldecls params pp_array t + | Gtblnorm (g, params, t) -> + Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g + pp_ldecls params pp_array t + | Gletcase(g,params,annot,a,accu,bs) -> + Format.fprintf fmt "@[let rec %a %a =@\n %a@]@\n@." + pp_gname g pp_ldecls params + pp_mllam (MLmatch(annot,a,accu,bs))(**}}}**) + +(** Compilation of elements in environment {{{**) +let rec compile_with_fv env auxdefs l t = + let (auxdefs,(fv_named,fv_rel),ml) = mllambda_of_lambda auxdefs l t in + if fv_named = [] && fv_rel = [] then (auxdefs,ml) + else apply_fv env (fv_named,fv_rel) auxdefs ml + +and apply_fv env (fv_named,fv_rel) auxdefs ml = + let get_rel_val (n,_) auxdefs = + (* + match !(lookup_rel_native_val n env) with + | NVKnone -> + *) + compile_rel env auxdefs n +(* | NVKvalue (v,d) -> assert false *) + in + let get_named_val (id,_) auxdefs = + (* + match !(lookup_named_native_val id env) with + | NVKnone -> + *) + compile_named env auxdefs id +(* | NVKvalue (v,d) -> assert false *) + in + let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in + let auxdefs = List.fold_right get_named_val fv_named auxdefs in + let lvl = rel_context_length env.env_rel_context in + let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in + let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in + let aux_name = fresh_lname Anonymous in + auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) + +and compile_rel env auxdefs n = + let (_,body,_) = lookup_rel n env.env_rel_context in + let n = rel_context_length env.env_rel_context - n in + match body with + | Some t -> + let code = lambda_of_constr env t in + let auxdefs,code = compile_with_fv env auxdefs None code in + Glet(Grel n, code)::auxdefs + | None -> + Glet(Grel n, MLprimitive (Mk_rel n))::auxdefs + +and compile_named env auxdefs id = + let (_,body,_) = lookup_named id env.env_named_context in + match body with + | Some t -> + let code = lambda_of_constr env t in + let auxdefs,code = compile_with_fv env auxdefs None code in + Glet(Gnamed id, code)::auxdefs + | None -> + Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs + +let compile_constant env prefix con body = + match body with + | Def t -> + let t = Declarations.force t in + let code = lambda_of_constr env t in + let code, name = + if is_lazy t then mk_lazy code, LinkedLazy prefix + else code, Linked prefix + in + let l = con_label con in + let auxdefs,code = compile_with_fv env [] (Some l) code in + let l = + optimize_stk (Glet(Gconstant ("",con),code)::auxdefs) + in + l, name + | _ -> + let i = push_symbol (SymbConst con) in + [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))], + Linked prefix + +let loaded_native_files = ref ([] : string list) + +let register_native_file s = + if not (List.mem s !loaded_native_files) then + loaded_native_files := s :: !loaded_native_files + +let is_code_loaded ~interactive name = + match !name with + | NotLinked -> false + | LinkedInteractive s -> + if (interactive && List.mem s !loaded_native_files) then true + else (name := NotLinked; false) + | LinkedLazy s | Linked s -> + if List.mem s !loaded_native_files then true else (name := NotLinked; false) + +let param_name = Name (id_of_string "params") +let arg_name = Name (id_of_string "arg") + +let compile_mind prefix mb mind stack = + let f i stack ob = + let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in + let j = push_symbol (SymbInd (mind,i)) in + let name = Gind ("", (mind, i)) in + let accu = + Glet(name, MLapp (MLprimitive Mk_ind, [|get_ind_code j|])) + in + let nparams = mb.mind_nparams in + let params = + Array.init nparams (fun i -> {lname = param_name; luid = i}) in + let add_construct j acc (_,arity) = + let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in + let c = (mind,i), (j+1) in + Glet(Gconstruct ("",c), + mkMLlam (Array.append params args) + (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc + in + Array.fold_left_i add_construct (gtype::accu::stack) ob.mind_reloc_tbl + in + let upd = (mb.mind_native_name, Linked prefix) in + Array.fold_left_i f stack mb.mind_packets, upd + +type code_location_update = + Declarations.native_name ref * Declarations.native_name +type code_location_updates = + code_location_update Mindmap_env.t * code_location_update Cmap_env.t + +type linkable_code = global list * code_location_updates + +let empty_updates = Mindmap_env.empty, Cmap_env.empty + +let compile_mind_deps env prefix ~interactive + (comp_stack, (mind_updates, const_updates) as init) mind = + let mib = lookup_mind mind env in + if is_code_loaded ~interactive mib.mind_native_name + || Mindmap_env.mem mind mind_updates + then init + else + let comp_stack, upd = compile_mind prefix mib mind comp_stack in + let mind_updates = Mindmap_env.add mind upd mind_updates in + (comp_stack, (mind_updates, const_updates)) + +(* This function compiles all necessary dependencies of t, and generates code in + reverse order, as well as linking information updates *) +let rec compile_deps env prefix ~interactive init t = + match kind_of_term t with + | Meta _ -> raise (Invalid_argument "Nativecode.get_deps: Meta") + | Evar _ -> raise (Invalid_argument "Nativecode.get_deps: Evar") + | Ind (mind,_) -> compile_mind_deps env prefix ~interactive init mind + | Const c -> + let c = get_allias env c in + let cb = lookup_constant c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive cb.const_native_name + || cb.const_inline_code + || (Cmap_env.mem c const_updates) + then init + else + let comp_stack, (mind_updates, const_updates) = match cb.const_body with + | Def t -> compile_deps env prefix ~interactive init (Declarations.force t) + | _ -> init + in + let code, name = compile_constant env prefix c cb.const_body in + let comp_stack = code@comp_stack in + let const_updates = Cmap_env.add c (cb.const_native_name, name) const_updates in + comp_stack, (mind_updates, const_updates) + | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind + | _ -> fold_constr (compile_deps env prefix ~interactive) init t + +let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb = + reset_symbols_list symb; + let acc = (code, (mupds, cupds)) in + match cb.const_body with + | Def t -> + let t = Declarations.force t in + let (code, (mupds, cupds)) = compile_deps env prefix ~interactive:false acc t in + let (gl, name) = compile_constant env prefix con cb.const_body in + let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in + gl@code, !symbols_list, (mupds, cupds) + | _ -> + let (gl, name) = compile_constant env prefix con cb.const_body in + let cupds = Cmap_env.add con (cb.const_native_name, name) cupds in + gl@code, !symbols_list, (mupds, cupds) + +let compile_mind_field prefix mp l (code, symb, (mupds, cupds)) mb = + let mind = make_mind mp empty_dirpath l in + reset_symbols_list symb; + let code, upd = compile_mind prefix mb mind code in + let mupds = Mindmap_env.add mind upd mupds in + code, !symbols_list, (mupds, cupds) + +let mk_open s = Gopen s + +let mk_internal_let s code = + Glet(Ginternal s, code) + +(* ML Code for conversion function *) +let mk_conv_code env prefix t1 t2 = + let gl, (mind_updates, const_updates) = + let init = ([], empty_updates) in + compile_deps env prefix ~interactive:true init t1 + in + let gl, (mind_updates, const_updates) = + let init = (gl, (mind_updates, const_updates)) in + compile_deps env prefix ~interactive:true init t2 + in + let gl = List.rev gl in + let code1 = lambda_of_constr env t1 in + let code2 = lambda_of_constr env t2 in + let (gl,code1) = compile_with_fv env gl None code1 in + let (gl,code2) = compile_with_fv env gl None code2 in + let g1 = MLglobal (Ginternal "t1") in + let g2 = MLglobal (Ginternal "t2") in + let header = Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_symbols_tbl"), + [|MLglobal (Ginternal "()")|])) in + header::(gl@ + [mk_internal_let "t1" code1; + mk_internal_let "t2" code2; + Glet(Ginternal "_", MLsetref("rt1",g1)); + Glet(Ginternal "_", MLsetref("rt2",g2))]), + (mind_updates, const_updates) + +let mk_norm_code env prefix t = + let gl, (mind_updates, const_updates) = + let init = ([], empty_updates) in + compile_deps env prefix ~interactive:true init t + in + let gl = List.rev gl in + let code = lambda_of_constr env t in + let (gl,code) = compile_with_fv env gl None code in + let g1 = MLglobal (Ginternal "t1") in + let header = Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_symbols_tbl"), + [|MLglobal (Ginternal "()")|])) in + header::(gl@ + [mk_internal_let "t1" code; + Glet(Ginternal "_", MLsetref("rt1",g1))]), (mind_updates, const_updates) + +let mk_library_header dir = + let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in + [Glet(Ginternal "symbols_tbl", + MLapp (MLglobal (Ginternal "get_library_symbols_tbl"), + [|MLglobal (Ginternal libname)|]))] + +let update_location (r,v) = r := v + +let update_locations (ind_updates,const_updates) = + Mindmap_env.iter (fun _ -> update_location) ind_updates; + Cmap_env.iter (fun _ -> update_location) const_updates +(** }}} **) + +(* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli new file mode 100644 index 0000000000..0f01ae80e7 --- /dev/null +++ b/kernel/nativecode.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Term +open Names +open Declarations +open Pre_env +open Nativelambda + +(** This file defines the mllambda code generation phase of the native +compiler. mllambda represents a fragment of ML, and can easily be printed +to OCaml code. *) + +type mllambda +type global + +val pp_global : Format.formatter -> global -> unit + +val mk_open : string -> global + +type symbol + +val get_value : symbol array -> int -> Nativevalues.t + +val get_sort : symbol array -> int -> sorts + +val get_name : symbol array -> int -> name + +val get_const : symbol array -> int -> constant + +val get_match : symbol array -> int -> Nativevalues.annot_sw + +val get_ind : symbol array -> int -> inductive + +val get_symbols_tbl : unit -> symbol array + +type code_location_update +type code_location_updates +type linkable_code = global list * code_location_updates + +val empty_updates : code_location_updates + +val register_native_file : string -> unit + +val compile_constant_field : env -> string -> constant -> + global list * symbol list * code_location_updates -> + constant_body -> + global list * symbol list * code_location_updates + +val compile_mind_field : string -> module_path -> label -> + global list * symbol list * code_location_updates -> + mutual_inductive_body -> + global list * symbol list * code_location_updates + +val mk_conv_code : env -> string -> constr -> constr -> linkable_code +val mk_norm_code : env -> string -> constr -> linkable_code + +val mk_library_header : dir_path -> global list + +val mod_uid_of_dirpath : dir_path -> string + +val update_locations : code_location_updates -> unit diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml new file mode 100644 index 0000000000..4ba3056600 --- /dev/null +++ b/kernel/nativeconv.ml @@ -0,0 +1,153 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Errors +open Names +open Term +open Univ +open Pre_env +open Nativelib +open Reduction +open Declarations +open Util +open Nativevalues +open Nativelambda +open Nativecode + +(** This module implements the conversion test by compiling to OCaml code *) + +let rec conv_val pb lvl v1 v2 cu = + if v1 == v2 then cu + else + match kind_of_value v1, kind_of_value v2 with + | Vaccu k1, Vaccu k2 -> + conv_accu pb lvl k1 k2 cu + | Vfun f1, Vfun f2 -> + let v = mk_rel_accu lvl in + conv_val CONV (lvl+1) (f1 v) (f2 v) cu + | Vconst i1, Vconst i2 -> + if i1 = i2 then cu else raise NotConvertible + | Vblock b1, Vblock b2 -> + let n1 = block_size b1 in + if block_tag b1 <> block_tag b2 || n1 <> block_size b2 then + raise NotConvertible; + let rec aux lvl max b1 b2 i cu = + if i = max then + conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu + else + let cu = + conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu in + aux lvl max b1 b2 (i+1) cu in + aux lvl (n1-1) b1 b2 0 cu + | Vfun f1, _ -> + conv_val CONV lvl v1 (fun x -> v2 x) cu + | _, Vfun f2 -> + conv_val CONV lvl (fun x -> v1 x) v2 cu + | _, _ -> raise NotConvertible + +and conv_accu pb lvl k1 k2 cu = + let n1 = accu_nargs k1 in + if n1 <> accu_nargs k2 then raise NotConvertible; + if n1 = 0 then + conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu + else + let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in + List.fold_right2 (conv_val CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + +and conv_atom pb lvl a1 a2 cu = + if a1 == a2 then cu + else + match a1, a2 with + | Arel i1, Arel i2 -> + if i1 <> i2 then raise NotConvertible; + cu + | Aind ind1, Aind ind2 -> + if not (eq_ind ind1 ind2) then raise NotConvertible; + cu + | Aconstant c1, Aconstant c2 -> + if not (eq_constant c1 c2) then raise NotConvertible; + cu + | Asort s1, Asort s2 -> + sort_cmp pb s1 s2 cu + | Avar id1, Avar id2 -> + if id1 <> id2 then raise NotConvertible; + cu + | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> + if a1.asw_ind <> a2.asw_ind then raise NotConvertible; + let cu = conv_accu CONV lvl ac1 ac2 cu in + let tbl = a1.asw_reloc in + let len = Array.length tbl in + if len = 0 then conv_val CONV lvl p1 p2 cu + else + let cu = conv_val CONV lvl p1 p2 cu in + let max = len - 1 in + let rec aux i cu = + let tag,arity = tbl.(i) in + let ci = + if arity = 0 then mk_const tag + else mk_block tag (mk_rels_accu lvl arity) in + let bi1 = bs1 ci and bi2 = bs2 ci in + if i = max then conv_val CONV (lvl + arity) bi1 bi2 cu + else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in + aux 0 cu + | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) -> + if s1 <> s2 || rp1 <> rp2 then raise NotConvertible; + if f1 == f2 then cu + else conv_fix lvl t1 f1 t2 f2 cu + | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)), + (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) -> + if s1 <> s2 then raise NotConvertible; + if f1 == f2 then cu + else + if Array.length f1 <> Array.length f2 then raise NotConvertible + else conv_fix lvl t1 f1 t2 f2 cu + | Aprod(_,d1,c1), Aprod(_,d2,c2) -> + let cu = conv_val CONV lvl d1 d2 cu in + let v = mk_rel_accu lvl in + conv_val pb (lvl + 1) (d1 v) (d2 v) cu + | _, _ -> raise NotConvertible + +(* Precondition length t1 = length f1 = length f2 = length t2 *) +and conv_fix lvl t1 f1 t2 f2 cu = + let len = Array.length f1 in + let max = len - 1 in + let fargs = mk_rels_accu lvl len in + let flvl = lvl + len in + let rec aux i cu = + let cu = conv_val CONV lvl t1.(i) t2.(i) cu in + let fi1 = napply f1.(i) fargs in + let fi2 = napply f2.(i) fargs in + if i = max then conv_val CONV flvl fi1 fi2 cu + else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in + aux 0 cu + +let native_conv pb env t1 t2 = + if !Flags.no_native_compiler then begin + let msg = "Native compiler is disabled, "^ + "falling back to VM conversion test." in + Pp.msg_warning (Pp.str msg); + vm_conv pb env t1 t2 + end + else + let env = Environ.pre_env env in + let ml_filename, prefix = get_ml_filename () in + let code, upds = mk_conv_code env prefix t1 t2 in + match compile ml_filename code with + | (0,fn) -> + begin + if !Flags.debug then Pp.msg_debug (Pp.str "Running test..."); + let t0 = Sys.time () in + call_linker ~fatal:true prefix fn (Some upds); + let t1 = Sys.time () in + let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in + if !Flags.debug then Pp.msg_debug (Pp.str time_info); + (* TODO change 0 when we can have deBruijn *) + conv_val pb 0 !rt1 !rt2 empty_constraint + end + | _ -> anomaly "Compilation failure" + +let _ = set_nat_conv native_conv diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli new file mode 100644 index 0000000000..2cb5ac7973 --- /dev/null +++ b/kernel/nativeconv.mli @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Term +open Univ +open Environ +open Reduction + +(** This module implements the conversion test by compiling to OCaml code *) + +val native_conv : conv_pb -> types conversion_function diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml new file mode 100644 index 0000000000..2ca2747994 --- /dev/null +++ b/kernel/nativelambda.ml @@ -0,0 +1,676 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Util +open Names +open Esubst +open Term +open Declarations +open Pre_env +open Nativevalues + +(** This file defines the lambda code generation phase of the native compiler *) + +type lambda = + | Lrel of name * int + | Lvar of identifier + | Lprod of lambda * lambda + | Llam of name array * lambda + | Lrec of name * lambda + | Llet of name * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of string * constant (* prefix, constant name *) + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lareint of lambda array + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of string * constructor * int * lambda array + (* prefix, constructor name, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of string * constructor (* prefix, constructor name *) + (* A partially applied constructor *) + | Lval of Nativevalues.t + | Lsort of sorts + | Lind of string * inductive (* prefix, inductive name *) + | Llazy + | Lforce + +and lam_branches = (constructor * name array * lambda) array + +and fix_decl = name array * lambda array * lambda array + +(*s Constructors *) + +let mkLapp f args = + if Array.length args = 0 then f + else + match f with + | Lapp(f', args') -> Lapp (f', Array.append args' args) + | _ -> Lapp(f, args) + +let mkLlam ids body = + if Array.length ids = 0 then body + else + match body with + | Llam(ids', body) -> Llam(Array.append ids ids', body) + | _ -> Llam(ids, body) + +let decompose_Llam lam = + match lam with + | Llam(ids,body) -> ids, body + | _ -> [||], lam + +(*s Operators on substitution *) +let subst_id = subs_id 0 +let lift = subs_lift +let liftn = subs_liftn +let cons v subst = subs_cons([|v|], subst) +let shift subst = subs_shft (1, subst) + +(* Linked code location utilities *) +let get_mind_prefix env mind = + let mib = lookup_mind mind env in + match !(mib.mind_native_name) with + | NotLinked -> "" + | Linked s -> s + | LinkedLazy s -> s + | LinkedInteractive s -> s + +let get_const_prefix env c = + let cb = lookup_constant c env in + match !(cb.const_native_name) with + | NotLinked -> "" + | Linked s -> s + | LinkedLazy s -> s + | LinkedInteractive s -> s + +(* A generic map function *) + +let map_lam_with_binders g f n lam = + match lam with + | Lrel _ | Lvar _ | Lconst _ | Lval _ + | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce -> lam + | Lprod(dom,codom) -> + let dom' = f n dom in + let codom' = f n codom in + if dom == dom' && codom == codom' then lam else Lprod(dom',codom') + | Llam(ids,body) -> + let body' = f (g (Array.length ids) n) body in + if body == body' then lam else mkLlam ids body' + | Lrec(id,body) -> + let body' = f (g 1 n) body in + if body == body' then lam else Lrec(id,body') + | Llet(id,def,body) -> + let def' = f n def in + let body' = f (g 1 n) body in + if body == body' && def == def' then lam else Llet(id,def',body') + | Lapp(fct,args) -> + let fct' = f n fct in + let args' = Array.smartmap (f n) args in + if fct == fct' && args == args' then lam else mkLapp fct' args' + | Lcase(annot,t,a,br) -> + let t' = f n t in + let a' = f n a in + let on_b b = + let (cn,ids,body) = b in + let body' = + let len = Array.length ids in + if len = 0 then f n body + else f (g (Array.length ids) n) body in + if body == body' then b else (cn,ids,body') in + let br' = Array.smartmap on_b br in + if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br') + | Lareint a -> + let a' = Array.smartmap (f n) a in + if a == a' then lam else Lareint a' + | Lif(t,bt,bf) -> + let t' = f n t in + let bt' = f n bt in + let bf' = f n bf in + if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf') + | Lfix(init,(ids,ltypes,lbodies)) -> + let ltypes' = Array.smartmap (f n) ltypes in + let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + if ltypes == ltypes' && lbodies == lbodies' then lam + else Lfix(init,(ids,ltypes',lbodies')) + | Lcofix(init,(ids,ltypes,lbodies)) -> + let ltypes' = Array.smartmap (f n) ltypes in + let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in + if ltypes == ltypes' && lbodies == lbodies' then lam + else Lcofix(init,(ids,ltypes',lbodies')) + | Lmakeblock(prefix,cn,tag,args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Lmakeblock(prefix,cn,tag,args') + +(*s Lift and substitution *) + +let rec lam_exlift el lam = + match lam with + | Lrel(id,i) -> + let i' = reloc_rel i el in + if i == i' then lam else Lrel(id,i') + | _ -> map_lam_with_binders el_liftn lam_exlift el lam + +let lam_lift k lam = + if k = 0 then lam + else lam_exlift (el_shft k el_id) lam + +let lam_subst_rel lam id n subst = + match expand_rel n subst with + | Inl(k,v) -> lam_lift k v + | Inr(n',_) -> + if n == n' then lam + else Lrel(id, n') + +let rec lam_exsubst subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + | _ -> map_lam_with_binders liftn lam_exsubst subst lam + +let lam_subst subst lam = + if is_subs_id subst then lam + else lam_exsubst subst lam + +let lam_subst_args subst args = + if is_subs_id subst then args + else Array.smartmap (lam_exsubst subst) args + +(** Simplification of lambda expression *) + +(* [simplify subst lam] simplify the expression [lam_subst subst lam] *) +(* that is : *) +(* - Reduce [let] is the definition can be substituted i.e: *) +(* - a variable (rel or identifier) *) + (* - a constant *) +(* - a structured constant *) +(* - a function *) +(* - Transform beta redex into [let] expression *) +(* - Move arguments under [let] *) +(* Invariant : Terms in [subst] are already simplified and can be *) +(* substituted *) + +let can_subst lam = + match lam with + | Lrel _ | Lvar _ | Lconst _ + | Lval _ | Lsort _ | Lind _ | Llam _ | Lconstruct _ -> true + | _ -> false + +let can_merge_if bt bf = + match bt, bf with + | Llam(idst,_), Llam(idsf,_) -> true + | _ -> false + +let merge_if t bt bf = + let (idst,bodyt) = decompose_Llam bt in + let (idsf,bodyf) = decompose_Llam bf in + let nt = Array.length idst in + let nf = Array.length idsf in + let common,idst,idsf = + if nt = nf then idst, [||], [||] + else + if nt < nf then idst,[||], Array.sub idsf nt (nf - nt) + else idsf, Array.sub idst nf (nt - nf), [||] in + Llam(common, + Lif(lam_lift (Array.length common) t, + mkLlam idst bodyt, + mkLlam idsf bodyf)) + +let rec simplify subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + + | Llet(id,def,body) -> + let def' = simplify subst def in + if can_subst def' then simplify (cons def' subst) body + else + let body' = simplify (lift subst) body in + if def == def' && body == body' then lam + else Llet(id,def',body') + + | Lapp(f,args) -> + begin match simplify_app subst f subst args with + | Lapp(f',args') when f == f' && args == args' -> lam + | lam' -> lam' + end + + | Lif(t,bt,bf) -> + let t' = simplify subst t in + let bt' = simplify subst bt in + let bf' = simplify subst bf in + if can_merge_if bt' bf' then merge_if t' bt' bf' + else + if t == t' && bt == bt' && bf == bf' then lam + else Lif(t',bt',bf') + | _ -> map_lam_with_binders liftn simplify subst lam + +and simplify_app substf f substa args = + match f with + | Lrel(id, i) -> + begin match lam_subst_rel f id i substf with + | Llam(ids, body) -> + reduce_lapp + subst_id (Array.to_list ids) body + substa (Array.to_list args) + | f' -> mkLapp f' (simplify_args substa args) + end + | Llam(ids, body) -> + reduce_lapp substf (Array.to_list ids) body substa (Array.to_list args) + | Llet(id, def, body) -> + let def' = simplify substf def in + if can_subst def' then + simplify_app (cons def' substf) body substa args + else + Llet(id, def', simplify_app (lift substf) body (shift substa) args) + | Lapp(f, args') -> + let args = Array.append + (lam_subst_args substf args') (lam_subst_args substa args) in + simplify_app substf f subst_id args + | _ -> mkLapp (simplify substf f) (simplify_args substa args) + +and simplify_args subst args = Array.smartmap (simplify subst) args + +and reduce_lapp substf lids body substa largs = + match lids, largs with + | id::lids, a::largs -> + let a = simplify substa a in + if can_subst a then + reduce_lapp (cons a substf) lids body substa largs + else + let body = reduce_lapp (lift substf) lids body (shift substa) largs in + Llet(id, a, body) + | [], [] -> simplify substf body + | _::_, _ -> + Llam(Array.of_list lids, simplify (liftn (List.length lids) substf) body) + | [], _::_ -> simplify_app substf body substa (Array.of_list largs) + + +(* [occurence kind k lam]: + If [kind] is [true] return [true] if the variable [k] does not appear in + [lam], return [false] if the variable appear one time and not + under a lambda, a fixpoint, a cofixpoint; else raise Not_found. + If [kind] is [false] return [false] if the variable does not appear in [lam] + else raise [Not_found] +*) + +let rec occurence k kind lam = + match lam with + | Lrel (_,n) -> + if n = k then + if kind then false else raise Not_found + else kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ + | Lconstruct _ | Llazy | Lforce -> kind + | Lprod(dom, codom) -> + occurence k (occurence k kind dom) codom + | Llam(ids,body) -> + let _ = occurence (k+Array.length ids) false body in kind + | Lrec(id,body) -> + let _ = occurence (k+1) false body in kind + | Llet(_,def,body) -> + occurence (k+1) (occurence k kind def) body + | Lapp(f, args) -> + occurence_args k (occurence k kind f) args + | Lmakeblock(_,_,_,args) -> + occurence_args k kind args + | Lcase(_,t,a,br) -> + let kind = occurence k (occurence k kind t) a in + let r = ref kind in + Array.iter (fun (_,ids,c) -> + r := occurence (k+Array.length ids) kind c && !r) br; + !r + | Lareint a -> + occurence_args k kind a + | Lif (t, bt, bf) -> + let kind = occurence k kind t in + kind && occurence k kind bt && occurence k kind bf + | Lfix(_,(ids,ltypes,lbodies)) + | Lcofix(_,(ids,ltypes,lbodies)) -> + let kind = occurence_args k kind ltypes in + let _ = occurence_args (k+Array.length ids) false lbodies in + kind + +and occurence_args k kind args = + Array.fold_left (occurence k) kind args + +let occur_once lam = + try let _ = occurence 1 true lam in true + with Not_found -> false + +(* [remove_let lam] remove let expression in [lam] if the variable is *) +(* used at most once time in the body, and does not appear under *) +(* a lambda or a fix or a cofix *) + +let rec remove_let subst lam = + match lam with + | Lrel(id,i) -> lam_subst_rel lam id i subst + | Llet(id,def,body) -> + let def' = remove_let subst def in + if occur_once body then remove_let (cons def' subst) body + else + let body' = remove_let (lift subst) body in + if def == def' && body == body' then lam else Llet(id,def',body') + | _ -> map_lam_with_binders liftn remove_let subst lam + + +(*s Translation from [constr] to [lambda] *) + +(* Translation of constructor *) + +let is_value lc = + match lc with + | Lval _ -> true + | Lmakeblock(_,_,_,args) when Array.length args = 0 -> true + | _ -> false + +let get_value lc = + match lc with + | Lval v -> v + | Lmakeblock(_,_,tag,args) when Array.length args = 0 -> + Nativevalues.mk_int tag + | _ -> raise Not_found + +let make_args start _end = + Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) + +(* Translation of constructors *) + +let makeblock env cn tag args = + if Array.for_all is_value args && Array.length args > 0 then + let args = Array.map get_value args in + Lval (Nativevalues.mk_block tag args) + else + let prefix = get_mind_prefix env (fst (fst cn)) in + Lmakeblock(prefix, cn, tag, args) + +(* Translation of constants *) + +let rec get_allias env kn = + let tps = (lookup_constant kn env).const_body_code in + match Cemitcodes.force tps with + | Cemitcodes.BCallias kn' -> get_allias env kn' + | _ -> kn + +(*i Global environment *) + +let global_env = ref empty_env + +let set_global_env env = global_env := env + +let get_names decl = + let decl = Array.of_list decl in + Array.map fst decl + +(* Rel Environment *) +module Vect = + struct + type 'a t = { + mutable elems : 'a array; + mutable size : int; + } + + let make n a = { + elems = Array.make n a; + size = 0; + } + + let length v = v.size + + let extend v = + if v.size = Array.length v.elems then + let new_size = min (2*v.size) Sys.max_array_length in + if new_size <= v.size then raise (Invalid_argument "Vect.extend"); + let new_elems = Array.make new_size v.elems.(0) in + Array.blit v.elems 0 new_elems 0 (v.size); + v.elems <- new_elems + + let push v a = + extend v; + v.elems.(v.size) <- a; + v.size <- v.size + 1 + + let push_pos v a = + let pos = v.size in + push v a; + pos + + let popn v n = + v.size <- max 0 (v.size - n) + + let pop v = popn v 1 + + let get v n = + if v.size <= n then raise + (Invalid_argument "Vect.get:index out of bounds"); + v.elems.(n) + + let get_last v n = + if v.size <= n then raise + (Invalid_argument "Vect.get:index out of bounds"); + v.elems.(v.size - n - 1) + + + let last v = + if v.size = 0 then raise + (Invalid_argument "Vect.last:index out of bounds"); + v.elems.(v.size - 1) + + let clear v = v.size <- 0 + + let to_array v = Array.sub v.elems 0 v.size + + end + +let empty_args = [||] + +module Renv = + struct + + type constructor_info = tag * int * int (* nparam nrealargs *) + + type t = { + name_rel : name Vect.t; + construct_tbl : (constructor, constructor_info) Hashtbl.t; + + } + + + let make () = { + name_rel = Vect.make 16 Anonymous; + construct_tbl = Hashtbl.create 111 + } + + let push_rel env id = Vect.push env.name_rel id + + let push_rels env ids = + Array.iter (push_rel env) ids + + let pop env = Vect.pop env.name_rel + + let popn env n = + for i = 1 to n do pop env done + + let get env n = + Lrel (Vect.get_last env.name_rel (n-1), n) + + let get_construct_info env c = + try Hashtbl.find env.construct_tbl c + with Not_found -> + let ((mind,j), i) = c in + let oib = lookup_mind mind !global_env in + let oip = oib.mind_packets.(j) in + let tag,arity = oip.mind_reloc_tbl.(i-1) in + let nparams = oib.mind_nparams in + let r = (tag, nparams, arity) in + Hashtbl.add env.construct_tbl c r; + r + end + +let is_lazy t = (* APPROXIMATION *) + isApp t || isLetIn t + +let empty_ids = [||] + +let rec lambda_of_constr env c = +(* try *) + match kind_of_term c with + | Meta _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr: Meta") + | Evar _ -> raise (Invalid_argument "Nativelambda.lambda_of_constr : Evar") + + | Cast (c, _, _) -> lambda_of_constr env c + + | Rel i -> Renv.get env i + + | Var id -> Lvar id + + | Sort s -> Lsort s + | Ind ind -> + let prefix = get_mind_prefix !global_env (fst ind) in + Lind (prefix, ind) + + | Prod(id, dom, codom) -> + let ld = lambda_of_constr env dom in + Renv.push_rel env id; + let lc = lambda_of_constr env codom in + Renv.pop env; + Lprod(ld, Llam([|id|], lc)) + + | Lambda _ -> + let params, body = decompose_lam c in + let ids = get_names (List.rev params) in + Renv.push_rels env ids; + let lb = lambda_of_constr env body in + Renv.popn env (Array.length ids); + mkLlam ids lb + + | LetIn(id, def, _, body) -> + let ld = lambda_of_constr env def in + Renv.push_rel env id; + let lb = lambda_of_constr env body in + Renv.pop env; + Llet(id, ld, lb) + + | App(f, args) -> lambda_of_app env f args + + | Const _ -> lambda_of_app env c empty_args + + | Construct _ -> lambda_of_app env c empty_args + + | Case(ci,t,a,branches) -> + let (mind,i as ind) = ci.ci_ind in + let mib = lookup_mind mind !global_env in + let oib = mib.mind_packets.(i) in + let tbl = oib.mind_reloc_tbl in + (* Building info *) + let prefix = get_mind_prefix !global_env mind in + let annot_sw = + { asw_ind = ind; + asw_ci = ci; + asw_reloc = tbl; + asw_finite = mib.mind_finite; + asw_prefix = prefix} + in + (* translation of the argument *) + let la = lambda_of_constr env a in + (* translation of the type *) + let lt = lambda_of_constr env t in + (* translation of branches *) + let mk_branch i b = + let cn = (ind,i+1) in + let _, arity = tbl.(i) in + let b = lambda_of_constr env b in + if arity = 0 then (cn, empty_ids, b) + else + match b with + | Llam(ids, body) when Array.length ids = arity -> (cn, ids, body) + | _ -> + let ids = Array.make arity Anonymous in + let args = make_args arity 1 in + let ll = lam_lift arity b in + (cn, ids, mkLapp ll args) in + let bs = Array.mapi mk_branch branches in + Lcase(annot_sw, lt, la, bs) + + | Fix(rec_init,(names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args env 0 type_bodies in + Renv.push_rels env names; + let lbodies = lambda_of_args env 0 rec_bodies in + Renv.popn env (Array.length names); + Lfix(rec_init, (names, ltypes, lbodies)) + + | CoFix(init,(names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args env 0 type_bodies in + Renv.push_rels env names; + let lbodies = lambda_of_args env 0 rec_bodies in + Renv.popn env (Array.length names); + Lcofix(init, (names, ltypes, lbodies)) + +and lambda_of_app env f args = + match kind_of_term f with + | Const kn -> + let kn = get_allias !global_env kn in + let cb = lookup_constant kn !global_env in + begin match cb.const_body with + | Def csubst -> + if cb.const_inline_code then lambda_of_app env (force csubst) args + else + let prefix = get_const_prefix !global_env kn in + let t = + if is_lazy (force csubst) then mkLapp Lforce [|Lconst (prefix, kn)|] + else Lconst (prefix, kn) + in + mkLapp t (lambda_of_args env 0 args) + | OpaqueDef _ | Undef _ -> + let prefix = get_const_prefix !global_env kn in + mkLapp (Lconst (prefix, kn)) (lambda_of_args env 0 args) + end + | Construct c -> + let tag, nparams, arity = Renv.get_construct_info env c in + let expected = nparams + arity in + let nargs = Array.length args in + if nargs = expected then + let args = lambda_of_args env nparams args in + makeblock !global_env c tag args + else + let prefix = get_mind_prefix !global_env (fst (fst c)) in + mkLapp (Lconstruct (prefix, c)) (lambda_of_args env 0 args) + | _ -> + let f = lambda_of_constr env f in + let args = lambda_of_args env 0 args in + mkLapp f args + +and lambda_of_args env start args = + let nargs = Array.length args in + if start < nargs then + Array.init (nargs - start) + (fun i -> lambda_of_constr env args.(start + i)) + else empty_args + +let optimize lam = + let lam = simplify subst_id lam in +(* if Flags.vm_draw_opt () then + (msgerrnl (str "Simplify = \n" ++ pp_lam lam);flush_all()); + let lam = remove_let subst_id lam in + if Flags.vm_draw_opt () then + (msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *) + lam + +let lambda_of_constr env c = + set_global_env env; + let env = Renv.make () in + let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in + Renv.push_rels env (Array.of_list ids); + let lam = lambda_of_constr env c in +(* if Flags.vm_draw_opt () then begin + (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); + (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); + end; *) + optimize lam + +let mk_lazy c = + mkLapp Llazy [|c|] diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli new file mode 100644 index 0000000000..0c454256e1 --- /dev/null +++ b/kernel/nativelambda.mli @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Util +open Names +open Esubst +open Term +open Declarations +open Pre_env +open Nativevalues + +(** This file defines the lambda code generation phase of the native compiler *) + +type lambda = + | Lrel of name * int + | Lvar of identifier + | Lprod of lambda * lambda + | Llam of name array * lambda + | Lrec of name * lambda + | Llet of name * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of string * constant (* prefix, constant name *) + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lareint of lambda array + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of string * constructor * int * lambda array + (* prefix, constructor name, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of string * constructor (* prefix, constructor name *) + (* A partially applied constructor *) + | Lval of Nativevalues.t + | Lsort of sorts + | Lind of string * inductive (* prefix, inductive name *) + | Llazy + | Lforce + +and lam_branches = (constructor * name array * lambda) array + +and fix_decl = name array * lambda array * lambda array + +val decompose_Llam : lambda -> Names.name array * lambda + +val is_lazy : constr -> bool +val mk_lazy : lambda -> lambda + +val get_allias : env -> constant -> constant + +val lambda_of_constr : env -> types -> lambda diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml new file mode 100644 index 0000000000..f8474bf199 --- /dev/null +++ b/kernel/nativelib.ml @@ -0,0 +1,91 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Term +open Util +open Nativevalues +open Declarations +open Nativecode +open Pre_env +open Errors +open Envars + +(** This file provides facilities to access OCaml compiler and dynamic linker, +used by the native compiler. *) + +let get_load_paths = + ref (fun _ -> anomaly "get_load_paths not initialized" : unit -> string list) + +let open_header = ["Nativevalues"; + "Nativecode"; + "Nativelib"; + "Nativeconv"; + "Declaremods"] +let open_header = List.map mk_open open_header + +(* Global settings and utilies for interface with OCaml *) +let compiler_name = + Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ()) + +let ( / ) a b = Filename.concat a b + +(* We have to delay evaluation of include_dirs because coqlib cannot be guessed +until flags have been properly initialized *) +let include_dirs () = [Filename.temp_dir_name; + coqlib ~fail:Errors.error / "kernel"; + coqlib ~fail:Errors.error / "library"] + +(* Pointer to the function linking an ML object into coq's toplevel *) +let load_obj = ref (fun x -> () : string -> unit) + +let rt1 = ref (dummy_value ()) +let rt2 = ref (dummy_value ()) + +let get_ml_filename () = + let filename = Filename.temp_file "Coq_native" ".ml" in + let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in + filename, prefix + +let write_ml_code ml_filename ?(header=[]) code = + let header = open_header@header in + let ch_out = open_out ml_filename in + let fmt = Format.formatter_of_out_channel ch_out in + List.iter (pp_global fmt) (header@code); + close_out ch_out + +let call_compiler ml_filename load_path = + let include_dirs = List.map Filename.quote (include_dirs () @ load_path) in + let include_dirs = String.concat " -I " include_dirs in + let f = Filename.chop_extension ml_filename in + let link_filename = f ^ ".cmo" in + let link_filename = Dynlink.adapt_filename link_filename in + let comp_cmd = + Format.sprintf "%s -%s -o %s -rectypes -w -A -I %s %s" + compiler_name (if Dynlink.is_native then "shared" else "c") + (Filename.quote link_filename) include_dirs (Filename.quote ml_filename) + in + let res = Sys.command comp_cmd in + Sys.rename (f^".ml") (f^".native"); + res, link_filename + +let compile ml_filename code = + write_ml_code ml_filename code; + call_compiler ml_filename (!get_load_paths()) + +let call_linker ~fatal prefix f upds = + rt1 := dummy_value (); + rt2 := dummy_value (); + (try + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix + with | Dynlink.Error e -> + let msg = "Dynlink error, " ^ Dynlink.error_message e in + if fatal then anomaly msg else Pp.msg_warning (Pp.str msg) + | _ -> let msg = "Dynlink error" in + if fatal then anomaly msg else Pp.msg_warning (Pp.str msg)); + match upds with Some upds -> update_locations upds | _ -> () diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli new file mode 100644 index 0000000000..0cbe4ccd5e --- /dev/null +++ b/kernel/nativelib.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Term +open Nativevalues +open Nativecode +open Pre_env + +(** This file provides facilities to access OCaml compiler and dynamic linker, +used by the native compiler. *) + +val get_load_paths : (unit -> string list) ref + +val load_obj : (string -> unit) ref + +val get_ml_filename : unit -> string * string + +val write_ml_code : string -> + ?header:Nativecode.global list -> global list -> unit + +val call_compiler : string -> string list -> int * string + +val compile : string -> global list -> int * string + +val call_linker : + fatal:bool -> string -> string -> code_location_updates option -> unit + +val rt1 : Nativevalues.t ref +val rt2 : Nativevalues.t ref diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml new file mode 100644 index 0000000000..c90691ee4b --- /dev/null +++ b/kernel/nativelibrary.ml @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Declarations +open Environ +open Mod_subst +open Modops +open Nativecode +open Nativelib + +(** This file implements separate compilation for libraries in the native +compiler *) + +let rec translate_mod prefix mp env mod_expr acc = + match mod_expr with + | SEBident mp' -> assert false + | SEBstruct msb -> + let env' = add_signature mp msb empty_delta_resolver env in + List.fold_left (translate_field prefix mp env') acc msb + | SEBfunctor (mbid,mtb,meb) -> acc + | SEBapply (f,x,_) -> assert false + | SEBwith _ -> assert false +and translate_field prefix mp env (code, values, upds as acc) (l,x) = + match x with + | SFBconst cb -> + let con = make_con mp empty_dirpath l in + compile_constant_field (pre_env env) prefix con acc cb + | SFBmind mb -> + compile_mind_field prefix mp l acc mb + | SFBmodule md -> + translate_mod prefix md.mod_mp env md.mod_type acc + | SFBmodtype mdtyp -> + translate_mod prefix mdtyp.typ_mp env mdtyp.typ_expr acc + +let dump_library mp dp env mod_expr = + if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library..."); + match mod_expr with + | SEBstruct msb -> + let env = add_signature mp msb empty_delta_resolver env in + let prefix = mod_uid_of_dirpath dp ^ "." in + let t0 = Sys.time () in + let mlcode, values, upds = + List.fold_left (translate_field prefix mp env) ([],[],empty_updates) + msb + in + let t1 = Sys.time () in + let time_info = Format.sprintf "Compiled library. Time: %.5f@." (t1-.t0) in + if !Flags.debug then Pp.msg_debug (Pp.str time_info); + List.rev mlcode, Array.of_list (List.rev values), upds + | _ -> assert false + + +let compile_library dir code load_path f = + let header = mk_library_header dir in + let ml_filename = f^".ml" in + write_ml_code ml_filename ~header code; + fst (call_compiler ml_filename load_path) diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli new file mode 100644 index 0000000000..7b74b00c52 --- /dev/null +++ b/kernel/nativelibrary.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Declarations +open Environ +open Nativecode + +(** This file implements separate compilation for libraries in the native +compiler *) + +val dump_library : module_path -> dir_path -> env -> struct_expr_body -> + global list * symbol array * code_location_updates + +val compile_library : + dir_path -> global list -> string list -> string -> int diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml new file mode 100644 index 0000000000..fc4255aaf8 --- /dev/null +++ b/kernel/nativevalues.ml @@ -0,0 +1,259 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Term +open Names +open Errors + +(** This modules defines the representation of values internally used by +the native compiler *) + +type t = t -> t + +type accumulator (* = t (* a block [0:code;atom;arguments] *) *) + +type tag = int + +type arity = int + +type reloc_table = (tag * arity) array + +type annot_sw = { + asw_ind : inductive; + asw_ci : case_info; + asw_reloc : reloc_table; + asw_finite : bool; + asw_prefix : string + } + +type sort_annot = string * int + +type rec_pos = int array + +type atom = + | Arel of int + | Aconstant of constant + | Aind of inductive + | Asort of sorts + | Avar of identifier + | Acase of annot_sw * accumulator * t * (t -> t) + | Afix of t array * t array * rec_pos * int + | Acofix of t array * t array * int * t + | Acofixe of t array * t array * int * t + | Aprod of name * t * (t -> t) + +let accumulate_tag = 0 + +let accumulate_code (k:accumulator) (x:t) = + let o = Obj.repr k in + let osize = Obj.size o in + let r = Obj.new_block accumulate_tag (osize + 1) in + for i = 0 to osize - 1 do + Obj.set_field r i (Obj.field o i) + done; + Obj.set_field r osize (Obj.repr x); + (Obj.obj r:t) + +let rec accumulate (x:t) = + accumulate_code (Obj.magic accumulate) x + +let raccumulate = ref accumulate + +let mk_accu_gen rcode (a:atom) = +(* Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *) + let r = Obj.new_block 0 3 in + Obj.set_field r 0 (Obj.field (Obj.magic rcode) 0); + Obj.set_field r 1 (Obj.field (Obj.magic rcode) 1); + Obj.set_field r 2 (Obj.magic a); + (Obj.magic r:t);; + +let mk_accu (a:atom) = mk_accu_gen accumulate a + +let mk_rel_accu i = + mk_accu (Arel i) + +let rel_tbl_size = 100 +let rel_tbl = Array.init rel_tbl_size mk_rel_accu + +let mk_rel_accu i = + if i < rel_tbl_size then rel_tbl.(i) + else mk_rel_accu i + +let mk_rels_accu lvl len = + Array.init len (fun i -> mk_rel_accu (lvl + i)) + +let napply (f:t) (args: t array) = + Array.fold_left (fun f a -> f a) f args + +let mk_constant_accu kn = + mk_accu (Aconstant kn) + +let mk_ind_accu s = + mk_accu (Aind s) + +let mk_sort_accu s = + mk_accu (Asort s) + +let mk_var_accu id = + mk_accu (Avar id) + +let mk_sw_accu annot c p ac = + mk_accu (Acase(annot,c,p,ac)) + +let mk_prod_accu s dom codom = + mk_accu (Aprod (s,dom,codom)) + +let atom_of_accu (k:accumulator) = + (Obj.magic (Obj.field (Obj.magic k) 2) : atom) + +let set_atom_of_accu (k:accumulator) (a:atom) = + Obj.set_field (Obj.magic k) 2 (Obj.magic a) + +let accu_nargs (k:accumulator) = + let nargs = Obj.size (Obj.magic k) - 3 in +(* if nargs < 0 then Format.eprintf "nargs = %i\n" nargs; *) + assert (nargs >= 0); + nargs + +let args_of_accu (k:accumulator) = + let nargs = accu_nargs k in + let f i = (Obj.magic (Obj.field (Obj.magic k) (nargs-i+2)) : t) in + let t = Array.init nargs f in + Array.to_list t + +let is_accu x = + let o = Obj.repr x in + Obj.is_block o && Obj.tag o = accumulate_tag + +(*let accumulate_fix_code (k:accumulator) (a:t) = + match atom_of_accu k with + | Afix(frec,_,rec_pos,_,_) -> + let nargs = accu_nargs k in + if nargs <> rec_pos || is_accu a then + accumulate_code k a + else + let r = ref frec in + for i = 0 to nargs - 1 do + r := !r (arg_of_accu k i) + done; + !r a + | _ -> assert false + + +let rec accumulate_fix (x:t) = + accumulate_fix_code (Obj.magic accumulate_fix) x + +let raccumulate_fix = ref accumulate_fix *) + +let is_atom_fix (a:atom) = + match a with + | Afix _ -> true + | _ -> false + +let mk_fix_accu rec_pos pos types bodies = + mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos)) + +let mk_cofix_accu pos types norm = + mk_accu_gen accumulate (Acofix(types,norm,pos,(Obj.magic 0 : t))) + +let upd_cofix (cofix :t) (cofix_fun : t) = + let atom = atom_of_accu (Obj.magic cofix) in + match atom with + | Acofix (typ,norm,pos,_) -> + set_atom_of_accu (Obj.magic cofix) (Acofix(typ,norm,pos,cofix_fun)) + | _ -> assert false + +let force_cofix (cofix : t) = + if is_accu cofix then + let accu = (Obj.magic cofix : accumulator) in + let atom = atom_of_accu accu in + match atom with + | Acofix(typ,norm,pos,f) -> + let f = ref f in + let args = List.rev (args_of_accu accu) in + List.iter (fun x -> f := !f x) args; + let v = !f (Obj.magic ()) in + set_atom_of_accu accu (Acofixe(typ,norm,pos,v)); + v + | Acofixe(_,_,_,v) -> v + | _ -> cofix + else cofix + +let mk_const tag = Obj.magic tag + +let mk_block tag args = + let nargs = Array.length args in + let r = Obj.new_block tag nargs in + for i = 0 to nargs - 1 do + Obj.set_field r i (Obj.magic args.(i)) + done; + (Obj.magic r : t) + +(* Two instances of dummy_value should not be pointer equal, otherwise + comparing them as terms would succeed *) +let dummy_value : unit -> t = fun () _ -> anomaly "Evaluation failed" + +let cast_accu v = (Obj.magic v:accumulator) + +let mk_int x = Obj.magic x + +type block + +let block_size (b:block) = + Obj.size (Obj.magic b) + +let block_field (b:block) i = (Obj.magic (Obj.field (Obj.magic b) i) : t) + +let block_tag (b:block) = + Obj.tag (Obj.magic b) + +type kind_of_value = + | Vaccu of accumulator + | Vfun of (t -> t) + | Vconst of int + | Vblock of block + +let kind_of_value (v:t) = + let o = Obj.repr v in + if Obj.is_int o then Vconst (Obj.magic v) + else + let tag = Obj.tag o in + if tag = accumulate_tag then + Vaccu (Obj.magic v) + else + if (tag < Obj.lazy_tag) then Vblock (Obj.magic v) + else + (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); + or ??? what is 1002*) + Vfun v + +let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i) +let bohcnv = Array.init 256 (fun i -> i - + (if 0x30 <= i then 0x30 else 0) - + (if 0x41 <= i then 0x7 else 0) - + (if 0x61 <= i then 0x20 else 0)) + +let hex_of_bin ch = hobcnv.(int_of_char ch) +let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1])) + +let str_encode expr = + let mshl_expr = Marshal.to_string expr [] in + let payload = Buffer.create (String.length mshl_expr * 2) in + String.iter (fun c -> Buffer.add_string payload (hex_of_bin c)) mshl_expr; + Buffer.contents payload + +let str_decode s = + let mshl_expr_len = String.length s / 2 in + let mshl_expr = Buffer.create mshl_expr_len in + let buf = String.create 2 in + for i = 0 to mshl_expr_len - 1 do + String.blit s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex buf) + done; + Marshal.from_string (Buffer.contents mshl_expr) 0 + + diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli new file mode 100644 index 0000000000..3994f53fd1 --- /dev/null +++ b/kernel/nativevalues.mli @@ -0,0 +1,102 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Term +open Names + +(** This modules defines the representation of values internally used by +the native compiler. Be careful when removing apparently dead code from this +interface, as it may be used by programs generated at runtime. *) + +type t = t -> t + +type accumulator + +type tag = int +type arity = int + +type reloc_table = (tag * arity) array + +type annot_sw = { + asw_ind : inductive; + asw_ci : case_info; + asw_reloc : reloc_table; + asw_finite : bool; + asw_prefix : string + } + +type sort_annot = string * int + +type rec_pos = int array + +type atom = + | Arel of int + | Aconstant of constant + | Aind of inductive + | Asort of sorts + | Avar of identifier + | Acase of annot_sw * accumulator * t * (t -> t) + | Afix of t array * t array * rec_pos * int + | Acofix of t array * t array * int * t + | Acofixe of t array * t array * int * t + | Aprod of name * t * (t -> t) + +(* Constructors *) + +val mk_accu : atom -> t +val mk_rel_accu : int -> t +val mk_rels_accu : int -> int -> t array +val mk_constant_accu : constant -> t +val mk_ind_accu : inductive -> t +val mk_sort_accu : sorts -> t +val mk_var_accu : identifier -> t +val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) +val mk_prod_accu : name -> t -> t -> t +val mk_fix_accu : rec_pos -> int -> t array -> t array -> t +val mk_cofix_accu : int -> t array -> t array -> t +val upd_cofix : t -> t -> unit +val force_cofix : t -> t +val mk_const : tag -> t +val mk_block : tag -> t array -> t + + +val mk_int : int -> t + +val napply : t -> t array -> t +(* Functions over accumulators *) + +val dummy_value : unit -> t +val atom_of_accu : accumulator -> atom +val args_of_accu : accumulator -> t list +val accu_nargs : accumulator -> int + +val cast_accu : t -> accumulator +(* Functions over block: i.e constructors *) + +type block + +val block_size : block -> int +val block_field : block -> int -> t +val block_tag : block -> int + + + +(* kind_of_value *) + +type kind_of_value = + | Vaccu of accumulator + | Vfun of (t -> t) + | Vconst of int + | Vblock of block + +val kind_of_value : t -> kind_of_value + +(* *) +val is_accu : t -> bool + +val str_encode : 'a -> string +val str_decode : string -> 'a diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 9aa70c9eb3..6a72487495 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -464,6 +464,16 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v2 (* option for conversion *) +let nat_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) +let set_nat_conv f = nat_conv := f + +let native_conv cv_pb env t1 t2 = + if eq_constr t1 t2 then empty_constraint + else begin + let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in + let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in + !nat_conv cv_pb env t1 t2 + end let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) let set_vm_conv f = vm_conv := f diff --git a/kernel/reduction.mli b/kernel/reduction.mli index acc97380a1..9d1d125730 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -54,6 +54,9 @@ val conv_leq_vecti : val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function +val set_nat_conv : (conv_pb -> types conversion_function) -> unit +val native_conv : conv_pb -> types conversion_function + val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 412ccfa31d..d04d3fe783 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -631,6 +631,9 @@ let set_engagement c senv = type compiled_library = Dir_path.t * module_body * library_info list * engagement option + * Nativecode.symbol array + +type native_library = Nativecode.global list (* We check that only initial state Require's were performed before [start_library] was called *) @@ -698,9 +701,16 @@ let export senv dir = mod_type_alg = None; mod_constraints = senv.univ; mod_delta = senv.modinfo.resolver; - mod_retroknowledge = senv.local_retroknowledge} + mod_retroknowledge = senv.local_retroknowledge + } + in + let ast, values = + if !Flags.no_native_compiler then [], [||] + else let ast, values, upds = Nativelibrary.dump_library mp dir senv.env str in + Nativecode.update_locations upds; + ast, values in - mp, (dir,mb,senv.imports,engagement senv.env) + mp, (dir,mb,senv.imports,engagement senv.env,values), ast let check_imports senv needed = @@ -731,7 +741,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let import (dp,mb,depends,engmt) digest senv = +let import (dp,mb,depends,engmt,values) digest senv = check_imports senv depends; check_engagement senv.env engmt; let mp = MPfile dp in @@ -745,7 +755,7 @@ let import (dp,mb,depends,engmt) digest senv = resolver = add_delta_resolver mb.mod_delta senv.modinfo.resolver}; imports = (dp,digest)::senv.imports; - loads = (mp,mb)::senv.loads } + loads = (mp,mb)::senv.loads }, values (* Store the body of modules' opaque constants inside a table. @@ -829,7 +839,7 @@ end = struct | SEBwith (seb,wdcl) -> SEBwith (traverse_modexpr seb,wdcl) in - fun (dp,mb,depends,s) -> (dp,traverse_module mb,depends,s) + fun (dp,mb,depends,s,val_tbl) -> (dp,traverse_module mb,depends,s,val_tbl) (* To disburden a library from opaque definitions, we simply traverse it and add an indirection between the module body diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 8f86123c04..7cddde954f 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -101,14 +101,16 @@ val delta_of_senv : safe_environment -> delta_resolver*delta_resolver (** exporting and importing modules *) type compiled_library +type native_library = Nativecode.global list + val start_library : Dir_path.t -> safe_environment -> module_path * safe_environment val export : safe_environment -> Dir_path.t - -> module_path * compiled_library + -> module_path * compiled_library * native_library val import : compiled_library -> Digest.t -> safe_environment - -> module_path * safe_environment + -> module_path * safe_environment * Nativecode.symbol array (** Remove the body of opaque constants *) diff --git a/kernel/term.ml b/kernel/term.ml index a66e5fb2be..e4657ce28c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -37,7 +37,7 @@ type metavariable = int (* This defines the strategy to use for verifiying a Cast *) (* Warning: REVERTcast is not exported to vo-files; as of r14492, it has to *) (* come after the vo-exported cast_kind so as to be compatible with coqchk *) -type cast_kind = VMcast | DEFAULTcast | REVERTcast +type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast (* This defines Cases annotations *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle @@ -155,7 +155,7 @@ let mkSort = function (* (that means t2 is declared as the type of t1) *) let mkCast (t1,k2,t2) = match t1 with - | Cast (c,k1, _) when k1 == VMcast && k1 == k2 -> Cast (c,k1,t2) + | Cast (c,k1, _) when (k1 == VMcast || k1 == NATIVEcast) && k1 == k2 -> Cast (c,k1,t2) | _ -> Cast (t1,k2,t2) (* Constructs the product (x:t1)t2 *) diff --git a/kernel/term.mli b/kernel/term.mli index b20e0a1d08..753fc990dd 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -95,8 +95,8 @@ val mkSet : types val mkType : Univ.universe -> types -(** This defines the strategy to use for verifiying a Cast *) -type cast_kind = VMcast | DEFAULTcast | REVERTcast +(* This defines the strategy to use for verifiying a Cast *) +type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast (** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the type t{_ 2} (that means t2 is declared as the type of t1). *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ccb6a4a7d7..1cd006f25a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -99,11 +99,11 @@ let infer_declaration env dcl = then OpaqueDef (Declarations.opaque_from_val j.uj_val) else Def (Declarations.from_val j.uj_val) in - def, typ, cst, c.const_entry_secctx + def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx | ParameterEntry (ctx,t,nl) -> let (j,cst) = infer env t in let t = hcons_constr (Typeops.assumption_of_judgment env j) in - Undef nl, NonPolymorphicType t, cst, ctx + Undef nl, NonPolymorphicType t, cst, false, ctx let global_vars_set_constant_type env = function | NonPolymorphicType t -> global_vars_set env t @@ -113,7 +113,7 @@ let global_vars_set_constant_type env = function (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty -let build_constant_declaration env kn (def,typ,cst,ctx) = +let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) = let hyps = let inferred = let ids_typ = global_vars_set_constant_type env typ in @@ -138,7 +138,9 @@ let build_constant_declaration env kn (def,typ,cst,ctx) = const_body = def; const_type = typ; const_body_code = tps; - const_constraints = cst } + const_constraints = cst; + const_native_name = ref NotLinked; + const_inline_code = inline_code } (*s Global and local constant declaration. *) @@ -147,8 +149,8 @@ let translate_constant env kn ce = let translate_recipe env kn r = build_constant_declaration env kn - (let def,typ,cst,hyps = Cooking.cook_constant env r in - def,typ,cst,Some hyps) + (let def,typ,cst,inline,hyps = Cooking.cook_constant env r in + def,typ,cst,inline,Some hyps) (* Insertion of inductive types. *) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index c2f046a20f..d001a258eb 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,10 +22,10 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - constant_def * constant_type * constraints * Sign.section_context option + constant_def * constant_type * constraints * bool * Sign.section_context option val build_constant_declaration : env -> 'a -> - constant_def * constant_type * constraints * Sign.section_context option -> + constant_def * constant_type * constraints * bool * Sign.section_context option -> constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8509edaf95..e611682002 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -280,7 +280,11 @@ let judge_of_cast env cj k tj = conv_leq false env cj.uj_type expected_type | REVERTcast -> cj.uj_val, - conv_leq true env cj.uj_type expected_type in + conv_leq true env cj.uj_type expected_type + | NATIVEcast -> + mkCast (cj.uj_val, k, expected_type), + native_conv CUMUL env cj.uj_type expected_type + in { uj_val = c; uj_type = expected_type }, cst diff --git a/lib/flags.ml b/lib/flags.ml index ffb324d535..765574cb4b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -160,3 +160,9 @@ let default_inline_level = 100 let inline_level = ref default_inline_level let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level + +(* Disabling native code compilation for conversion and normalization *) +let no_native_compiler = ref false + +(* Print the mod uid associated to a vo file by the native compiler *) +let print_mod_uid = ref false diff --git a/lib/flags.mli b/lib/flags.mli index f529dd5df0..6b26c50d9e 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -100,3 +100,9 @@ val camlp4bin : string ref val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int + +(* Disabling native code compilation for conversion and normalization *) +val no_native_compiler : bool ref + +(* Print the mod uid associated to a vo file by the native compiler *) +val print_mod_uid : bool ref diff --git a/library/declare.ml b/library/declare.ml index 20e5bdddc5..5c10728436 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -186,6 +186,7 @@ let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds { Entries.const_entry_body = body; const_entry_type = types; const_entry_opaque = opaque; + const_entry_inline_code = false; const_entry_secctx = None } in declare_constant ~internal id diff --git a/library/declaremods.ml b/library/declaremods.ml index 0d9ffb29eb..99704d1c0c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -652,22 +652,27 @@ type library_objects = let register_library dir cenv objs digest = let mp = MPfile dir in - let substobjs, keep = + let substobjs, keep, values = try ignore(Global.lookup_module mp); (* if it's in the environment, the cached objects should be correct *) Dirmap.find dir !library_cache with Not_found -> - if not (mp_eq mp (Global.import cenv digest)) then + let mp', values = Global.import cenv digest in + if not (mp_eq mp mp') then anomaly "Unexpected disk module name"; let mp,substitute,keep = objs in let substobjs = [], mp, substitute in - let modobjs = substobjs, keep in + let modobjs = substobjs, keep, values in library_cache := Dirmap.add dir modobjs !library_cache; modobjs in do_module false "register_library" load_objects 1 dir mp substobjs keep +let get_library_symbols_tbl dir = + let _,_,values = Dirmap.find dir !library_cache in + values + let start_library dir = let mp = Global.start_library dir in openmod_info:=mp,[],None,[]; @@ -680,9 +685,9 @@ let set_end_library_hook f = end_library_hook := f let end_library dir = !end_library_hook(); let prefix, lib_stack = Lib.end_compilation dir in - let mp,cenv = Global.export dir in + let mp,cenv,ast = Global.export dir in let substitute, keep, _ = Lib.classify_segment lib_stack in - cenv,(mp,substitute,keep) + cenv,(mp,substitute,keep),ast (* implementation of Export M and Import M *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 1b661faef4..f3c06b158f 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -112,10 +112,13 @@ val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Digest.t -> unit +val get_library_symbols_tbl : library_name -> Nativecode.symbol array + val start_library : library_name -> unit val end_library : - library_name -> Safe_typing.compiled_library * library_objects + library_name -> + Safe_typing.compiled_library * library_objects * Safe_typing.native_library (** set a function to be executed at end_library *) val set_end_library_hook : (unit -> unit) -> unit diff --git a/library/global.ml b/library/global.ml index f56cb7d615..e47085c896 100644 --- a/library/global.ml +++ b/library/global.ml @@ -141,9 +141,9 @@ let start_library dir = let export s = export !global_env s let import cenv digest = - let mp,newenv = import cenv digest !global_env in + let mp,newenv,values = import cenv digest !global_env in global_env := newenv; - mp + mp, values diff --git a/library/global.mli b/library/global.mli index 4908d35fb4..141cfe50b0 100644 --- a/library/global.mli +++ b/library/global.mli @@ -91,8 +91,9 @@ val exists_objlabel : Label.t -> bool (** Compiled modules *) val start_library : Dir_path.t -> module_path -val export : Dir_path.t -> module_path * compiled_library -val import : compiled_library -> Digest.t -> module_path +val export : Dir_path.t -> module_path * compiled_library * native_library +val import : compiled_library -> Digest.t -> + module_path * Nativecode.symbol array (** {6 ... } *) (** Function to get an environment from the constants part of the global diff --git a/library/library.ml b/library/library.ml index e2b74c6689..a944db45c6 100644 --- a/library/library.ml +++ b/library/library.ml @@ -222,8 +222,15 @@ let opened_libraries () = be performed first, thus the libraries_loaded_list ... *) let register_loaded_library m = + let link m = + let dirname = Filename.dirname (library_full_filename m.library_name) in + let prefix = Nativecode.mod_uid_of_dirpath m.library_name ^ "." in + let f = prefix ^ "cmo" in + let f = Dynlink.adapt_filename f in + Nativelib.call_linker ~fatal:false prefix (Filename.concat dirname f) None + in let rec aux = function - | [] -> [m] + | [] -> link m; [m] | m'::_ as l when Dir_path.equal m'.library_name m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; @@ -461,6 +468,8 @@ let rec_intern_by_filename_only id f = let m = try intern_from_file f with Sys_error s -> error s in (* Only the base name is expected to match *) check_library_short_name f m.library_name id; + if !Flags.print_mod_uid then + print_endline (Nativecode.mod_uid_of_dirpath m.library_name); (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin @@ -632,7 +641,7 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) let save_library_to dir f = - let cenv, seg = Declaremods.end_library dir in + let cenv, seg, ast = Declaremods.end_library dir in let cenv, table = LightenLibrary.save cenv in let md = { md_name = dir; @@ -654,8 +663,17 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; System.marshal_out ch table; - close_out ch - with e -> msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f'; raise e + close_out ch; + if not !Flags.no_native_compiler then begin + let lp = List.map CUnix.string_of_physical_path (get_load_paths ()) in + let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in + match Nativelibrary.compile_library dir ast lp fn with + | 0 -> () + | _ -> anomaly "Library compilation failure" + end + with e -> + msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f'; + raise e (************************************************************************) (*s Display the memory use of a library. *) @@ -667,3 +685,8 @@ let mem s = h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" (CObj.size_kb m) (CObj.size_kb m.library_compiled) (CObj.size_kb m.library_objects))) + +let get_load_paths_str () = + List.map CUnix.string_of_physical_path (get_load_paths ()) + +let _ = Nativelib.get_load_paths := get_load_paths_str diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3f246b48cc..08c1f19170 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -169,6 +169,10 @@ GEXTEND Gram CCast(!@loc,c1, CastVM c2) | c1 = operconstr; "<:"; c2 = SELF -> CCast(!@loc,c1, CastVM c2) + | c1 = operconstr; "<<:"; c2 = binder_constr -> + CCast(!@loc,c1, CastNative c2) + | c1 = operconstr; "<<:"; c2 = SELF -> + CCast(!@loc,c1, CastNative c2) | c1 = operconstr; ":";c2 = binder_constr -> CCast(!@loc,c1, CastConv c2) | c1 = operconstr; ":"; c2 = SELF -> diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 7b46289385..79f532781d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -176,7 +176,7 @@ GEXTEND Gram let t, ty = match mpv with | Term t -> (match t with - | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty) + | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty) | _ -> mpv, None) | _ -> mpv, None in Def (na, t, Option.default (Term (CHole (Loc.ghost, None))) ty) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 0f256749c6..6daceb03da 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -346,6 +346,7 @@ GEXTEND Gram | IDENT "lazy"; s = strategy_flag -> Lazy s | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po + | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ] @@ -359,6 +360,7 @@ GEXTEND Gram | IDENT "lazy"; s = strategy_flag -> Lazy s | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po + | IDENT "native_compute"; po = OPT pattern_occ -> CbvNative po | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul | IDENT "fold"; cl = LIST1 constr -> Fold cl | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index af66998675..fb5524945d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -342,7 +342,7 @@ GEXTEND Gram (oc,DefExpr (id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | l = binders; ":="; b = lconstr -> fun id -> match b with - | CCast(_,b, (CastConv t|CastVM t)) -> + | CCast(_,b, (CastConv t|CastVM t|CastNative t)) -> (None,DefExpr(id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t))) | _ -> (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ] diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f549adf7ae..700beaff59 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -339,7 +339,9 @@ let generate_functional_principle { const_entry_body = value; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false + } in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7785cbe592..a74ae84e24 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -409,7 +409,7 @@ let is_free_in id = | GRec _ -> raise (UserError("",str "Not handled GRec")) | GSort _ -> false | GHole _ -> false - | GCast (_,b,(CastConv t|CastVM t)) -> is_free_in b || is_free_in t + | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (_,b,CastCoerce) -> is_free_in b and is_free_in_br (_,ids,_,rt) = (not (List.mem id ids)) && is_free_in rt @@ -590,7 +590,7 @@ let ids_of_glob_constr c = | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc - | GCast (loc,c,(CastConv t|CastVM t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc + | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc | GLetTuple (_,nal,(na,po),b,c) -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e662cd41d1..4b87a9b9cc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -60,7 +60,8 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = let ce = {const_entry_body = value; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false } in + const_entry_opaque = false; + const_entry_inline_code = false} in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_named false diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index c89e06f7c2..3bb57a3b36 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -147,7 +147,8 @@ let decl_constant na c = { const_entry_body = c; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = true }, + const_entry_opaque = true; + const_entry_inline_code = false}, IsProof Lemma)) (* Calling a global tactic *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d9d82faa2b..545366a70f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -401,7 +401,12 @@ let rec detype (isgoal:bool) avoid env t = | Cast (c1,k,c2) -> let d1 = detype isgoal avoid env c1 in let d2 = detype isgoal avoid env c2 in - GCast(dl,d1,if k == VMcast then CastVM d2 else CastConv d2) + let cast = match k with + | VMcast -> CastVM d2 + | NATIVEcast -> CastNative d2 + | _ -> CastConv d2 + in + GCast(dl,d1,cast) | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 65c21f1be2..e219bbeb15 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -104,7 +104,11 @@ let fold_glob_constr f acc = (List.fold_left (fun acc (na,k,bbd,bty) -> fold (Option.fold_left fold acc bbd) bty)) acc bl in Array.fold_left fold (Array.fold_left fold acc tyl) bv - | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c + | GCast (_,c,k) -> + let r = match k with + | CastConv t | CastVM t | CastNative t -> fold acc t | CastCoerce -> acc + in + fold r c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc and fold_pattern acc (_,idl,p,c) = fold acc c @@ -150,7 +154,8 @@ let occur_glob_constr id = (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in occur_fix bl) idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false) + | GCast (loc,c,k) -> (occur c) or (match k with CastConv t + | CastVM t | CastNative t -> occur t | CastCoerce -> false) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) @@ -208,7 +213,7 @@ let free_glob_vars = in Array.fold_left_i vars_fix vs idl | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t -> vars bounded v t | _ -> v) + (match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v) | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs and vars_pattern bounded vs (loc,idl,p,c) = diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 1050123e18..264deeb051 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -16,12 +16,14 @@ let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) | CastCoerce -> CastCoerce + | CastNative a -> CastNative (f a) let smartmap_cast_type f c = match c with | CastConv a -> let a' = f a in if a' == a then c else CastConv a' | CastVM a -> let a' = f a in if a' == a then c else CastVM a' | CastCoerce -> CastCoerce + | CastNative a -> let a' = f a in if a' == a then c else CastNative a' (** Printing of [intro_pattern] *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml new file mode 100644 index 0000000000..84ad8e3dd8 --- /dev/null +++ b/pretyping/nativenorm.ml @@ -0,0 +1,347 @@ +(************************************************************************) +(* 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 Environ +open Reduction +open Univ +open Declarations +open Names +open Inductive +open Util +open Unix +open Nativecode +open Inductiveops +open Closure +open Nativevalues + +(** This module implements normalization by evaluation to OCaml code *) + +exception Find_at of int + +let invert_tag cst tag reloc_tbl = + try + for j = 0 to Array.length reloc_tbl - 1 do + let tagj,arity = reloc_tbl.(j) in + if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then + raise (Find_at j) + else () + done;raise Not_found + with Find_at j -> (j+1) + +let decompose_prod env t = + let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in + if name = Anonymous then (Name (id_of_string "x"),dom,codom) + else res + +let app_type env c = + let t = whd_betadeltaiota env c in + try destApp t with _ -> (t,[||]) + + +let find_rectype_a env c = + let (t, l) = app_type env c in + match kind_of_term t with + | Ind ind -> (ind, l) + | _ -> raise Not_found + +(* Instantiate inductives and parameters in constructor type *) + +let type_constructor mind mib typ params = + let s = ind_subst mind mib in + let ctyp = substl s typ in + let nparams = Array.length params in + if nparams = 0 then ctyp + else + let _,ctyp = decompose_prod_n nparams ctyp in + substl (List.rev (Array.to_list params)) ctyp + +let construct_of_constr_notnative const env tag (mind, _ as ind) allargs = + let mib,mip = lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let i = invert_tag const tag mip.mind_reloc_tbl in + let params = Array.sub allargs 0 nparams in + let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in + (mkApp(mkConstruct(ind,i), params), ctyp) + + +let construct_of_constr const env tag typ = + let t, l = app_type env typ in + match kind_of_term t with + | Ind ind -> + construct_of_constr_notnative const env tag ind l + | _ -> assert false + +let construct_of_constr_const env tag typ = + fst (construct_of_constr true env tag typ) + +let construct_of_constr_block = construct_of_constr false + +let build_branches_type env (mind,_ as _ind) mib mip params dep p = + let rtbl = mip.mind_reloc_tbl in + (* [build_one_branch i cty] construit le type de la ieme branche (commence + a 0) et les lambda correspondant aux realargs *) + let build_one_branch i cty = + let typi = type_constructor mind mib cty params in + let decl,indapp = Term.decompose_prod typi in + let ind,cargs = find_rectype_a env indapp in + let nparams = Array.length params in + let carity = snd (rtbl.(i)) in + let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in + let codom = + let papp = mkApp(lift (List.length decl) p,crealargs) in + if dep then + let cstr = ith_constructor_of_inductive ind (i+1) in + let relargs = Array.init carity (fun i -> mkRel (carity-i)) in + let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in + mkApp(papp,[|dep_cstr|]) + else papp + in + decl, codom + in Array.mapi build_one_branch mip.mind_nf_lc + +let build_case_type dep p realargs c = + if dep then mkApp(mkApp(p, realargs), [|c|]) + else mkApp(p, realargs) + +(* TODO move this function *) +let type_of_rel env n = + let (_,_,ty) = lookup_rel n env in + lift n ty + +let type_of_prop = mkSort type1_sort + +let type_of_sort s = + match s with + | Prop _ -> type_of_prop + | Type u -> mkType (Univ.super u) + +let type_of_var env id = + try let (_,_,ty) = lookup_named id env in ty + with Not_found -> + anomaly ("type_of_var: variable "^(string_of_id id)^" unbound") + +let sort_of_product env domsort rangsort = + match (domsort, rangsort) with + (* Product rule (s,Prop,Prop) *) + | (_, Prop Null) -> rangsort + (* Product rule (Prop/Set,Set,Set) *) + | (Prop _, Prop Pos) -> rangsort + (* Product rule (Type,Set,?) *) + | (Type u1, Prop Pos) -> + if engagement env = Some ImpredicativeSet then + (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) + rangsort + else + (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) + Type (sup u1 type0_univ) + (* Product rule (Prop,Type_i,Type_i) *) + | (Prop Pos, Type u2) -> Type (sup type0_univ u2) + (* Product rule (Prop,Type_i,Type_i) *) + | (Prop Null, Type _) -> rangsort + (* Product rule (Type_i,Type_i,Type_i) *) + | (Type u1, Type u2) -> Type (sup u1 u2) + +(* normalisation of values *) + +let branch_of_switch lvl ans bs = + let tbl = ans.asw_reloc in + let branch i = + 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 + bs ci in + Array.init (Array.length tbl) branch + +let rec nf_val env v typ = + match kind_of_value v with + | Vaccu accu -> nf_accu env accu + | Vfun f -> + let lvl = nb_rel env in + let name,dom,codom = + try decompose_prod env typ + with _ -> (* TODO: is this the right exception to raise? *) + raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ)) + in + let env = push_rel (name,None,dom) env in + let body = nf_val env (f (mk_rel_accu lvl)) codom in + mkLambda(name,dom,body) + | Vconst n -> construct_of_constr_const env n typ + | Vblock b -> + let capp,ctyp = construct_of_constr_block env (block_tag b) typ in + let args = nf_bargs env b ctyp in + mkApp(capp,args) + +and nf_type env v = + match kind_of_value v with + | Vaccu accu -> nf_accu env accu + | _ -> assert false + +and nf_type_sort env v = + match kind_of_value v with + | Vaccu accu -> + let t,s = nf_accu_type env accu in + let s = try destSort s with _ -> assert false in + t, s + | _ -> assert false + +and nf_accu env accu = + let atom = atom_of_accu accu in + if accu_nargs accu = 0 then nf_atom env atom + else + let a,typ = nf_atom_type env atom in + let _, args = nf_args env accu typ in + mkApp(a,Array.of_list args) + +and nf_accu_type env accu = + let atom = atom_of_accu accu in + if accu_nargs accu = 0 then nf_atom_type env atom + else + let a,typ = nf_atom_type env atom in + let t, args = nf_args env accu typ in + mkApp(a,Array.of_list args), t + +and nf_args env accu t = + let aux arg (t,l) = + let _,dom,codom = try decompose_prod env t with _ -> exit 123 in + let c = nf_val env arg dom in + (subst1 c codom, c::l) + in + let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in + t, List.rev l + +and nf_bargs env b t = + let t = ref t in + let len = block_size b in + Array.init len + (fun i -> + let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in + let c = nf_val env (block_field b i) dom in + t := subst1 c codom; c) + +and nf_atom env atom = + match atom with + | Arel i -> mkRel (nb_rel env - i) + | Aconstant cst -> mkConst cst + | Aind ind -> mkInd ind + | Asort s -> mkSort s + | Avar id -> mkVar id + | Aprod(n,dom,codom) -> + let dom = nf_type env dom in + let vn = mk_rel_accu (nb_rel env) in + let env = push_rel (n,None,dom) env in + let codom = nf_type env (codom vn) in + mkProd(n,dom,codom) + | _ -> fst (nf_atom_type env atom) + +and nf_atom_type env atom = + match atom with + | Arel i -> + let n = (nb_rel env - i) in + mkRel n, type_of_rel env n + | Aconstant cst -> + mkConst cst, Typeops.type_of_constant env cst + | Aind ind -> + mkInd ind, Inductiveops.type_of_inductive env ind + | Asort s -> + mkSort s, type_of_sort s + | Avar id -> + mkVar id, type_of_var env id + | Acase(ans,accu,p,bs) -> + let a,ta = nf_accu_type env accu in + let (mind,_ as ind),allargs = find_rectype_a env ta in + let (mib,mip) = Inductive.lookup_mind_specif env ind in + let nparams = mib.mind_nparams in + let params,realargs = Array.chop nparams allargs in + let pT = + hnf_prod_applist env + (Inductiveops.type_of_inductive env ind) (Array.to_list params) in + let pT = whd_betadeltaiota env pT in + let dep, p = nf_predicate env ind mip params p pT in + (* Calcul du type des branches *) + let btypes = build_branches_type env ind mib mip params dep p in + (* calcul des branches *) + let bsw = branch_of_switch (nb_rel env) ans bs in + let mkbranch i v = + let decl,codom = btypes.(i) in + let env = + List.fold_right + (fun (name,t) env -> push_rel (name,None,t) env) decl env in + let b = nf_val env v codom in + compose_lam decl b + in + let branchs = Array.mapi mkbranch bsw in + let tcase = build_case_type dep p realargs a in + let ci = ans.asw_ci in + mkCase(ci, p, a, branchs), tcase + | Afix(tt,ft,rp,s) -> + let tt = Array.map (nf_type env) tt in + let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in + let lvl = nb_rel env in + let fargs = mk_rels_accu lvl (Array.length ft) in + let env = push_rec_types (name,tt,[||]) env in + let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in + mkFix((rp,s),(name,tt,ft)), tt.(s) + | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) -> + let tt = Array.map (nf_type env) tt in + let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in + let lvl = nb_rel env in + let fargs = mk_rels_accu lvl (Array.length ft) in + let env = push_rec_types (name,tt,[||]) env in + let ft = Array.mapi (fun i v -> nf_val env (napply v fargs) tt.(i)) ft in + mkCoFix(s,(name,tt,ft)), tt.(s) + | Aprod(n,dom,codom) -> + let dom,s1 = nf_type_sort env dom in + let vn = mk_rel_accu (nb_rel env) in + let env = push_rel (n,None,dom) env in + let codom,s2 = nf_type_sort env (codom vn) in + mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2) + +and nf_predicate env ind mip params v pT = + match kind_of_value v, kind_of_term pT with + | Vfun f, Prod _ -> + let k = nb_rel env in + let vb = f (mk_rel_accu k) in + let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in + let dep,body = + nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in + dep, mkLambda(name,dom,body) + | Vfun f, _ -> + let k = nb_rel env in + let vb = f (mk_rel_accu k) in + let name = Name (id_of_string "c") in + let n = mip.mind_nrealargs in + let rargs = Array.init n (fun i -> mkRel (n-i)) in + let params = if n=0 then params else Array.map (lift n) params in + let dom = mkApp(mkInd ind,Array.append params rargs) in + let body = nf_type (push_rel (name,None,dom) env) vb in + true, mkLambda(name,dom,body) + | _, _ -> false, nf_type env v + +let native_norm env c ty = + if !Flags.no_native_compiler then + error "Native_compute reduction has been disabled" + else + let penv = Environ.pre_env env in + (* + Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); + Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); + *) + let ml_filename, prefix = Nativelib.get_ml_filename () in + let code, upd = mk_norm_code penv prefix c in + match Nativelib.compile ml_filename code with + | 0,fn -> + if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ..."); + let t0 = Sys.time () in + Nativelib.call_linker ~fatal:true prefix fn (Some upd); + 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); + nf_val env !Nativelib.rt1 ty + | _ -> anomaly "Compilation failure" diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli new file mode 100644 index 0000000000..ecc3489bee --- /dev/null +++ b/pretyping/nativenorm.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 Names +open Term +open Environ +open Reduction + +(** This module implements normalization by evaluation to OCaml code *) + +val native_norm : env -> constr -> types -> constr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 358d53e48f..15395ca7f9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -637,8 +637,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj - | CastConv t | CastVM t -> - let k = (match k with CastVM _ -> VMcast | _ -> DEFAULTcast) in + | CastConv t | CastVM t | CastNative t -> + let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in let tval = nf_evar !evdref tj.utj_val in let cj = match k with @@ -654,6 +654,19 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function end else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") + | NATIVEcast -> + let cj = pretype empty_tycon env evdref lvar c in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + if not (occur_existential cty || occur_existential tval) then + begin + try + ignore (Nativeconv.native_conv Reduction.CUMUL env cty tval); cj + with Reduction.NotConvertible -> + error_actual_type_loc loc env !evdref cj tval + end + else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++ + str "unresolved arguments remain.") + | _ -> pretype (mk_tycon tval) env evdref lvar c in diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index ea08e7c5d2..506c59ef39 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -5,6 +5,7 @@ Reductionops Vnorm Namegen Inductiveops +Nativenorm Retyping Cbv Pretype_errors diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f1f31ec6e3..0fb3a99a47 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -621,6 +621,10 @@ let whd_betaiota_preserving_vm_cast env sigma t = let c = zip (whrec (c,empty_stack)) in let t = zip (whrec (t,empty_stack)) in (mkCast(c,VMcast,t),stack) + | Cast (c,NATIVEcast,t) -> + let c = zip (whrec (c,empty_stack)) in + let t = zip (whrec (t,empty_stack)) in + (mkCast(c,NATIVEcast,t),stack) | Cast (c,DEFAULTcast,_) -> whrec (c, stack) | App (f,cl) -> whrec (f, append_stack_app cl stack) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index e7f4a0b245..9f6715a7d9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -258,7 +258,7 @@ let pr_binder_among_many pr_c = function pr_binder true pr_c (nal,k,t) | LocalRawDef (na,c) -> let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t)) -> c, t + | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t | _ -> c, CHole (Loc.ghost, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) @@ -540,6 +540,7 @@ let pr pr sep inherited a = match b with | CastConv b -> str ":" ++ pr mt (-lcast,E) b | CastVM b -> str "<:" ++ pr mt (-lcast,E) b + | CastNative b -> str "<<:" ++ pr mt (-lcast,E) b | CastCoerce -> str ":>"), lcast | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom @@ -637,6 +638,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function | Red true -> error "Shouldn't be accessible from user." | ExtraRedExpr s -> str s | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o + | CbvNative o -> str "native_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o let pr_may_eval test prc prlc pr2 pr3 = function | ConstrEval (r,c) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index c48882c1a1..45ef3efadf 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -347,10 +347,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; let res = mk_refgoals sigma goal goalacc ty t in - (** we keep the casts (in particular VMcast) except + (** we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) if isMeta t then begin - assert (k != VMcast); + assert (k != VMcast && k != NATIVEcast); res end else let (gls,cty,sigma,trm) = res in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c5a1902280..ed985f2927 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -270,7 +270,8 @@ let close_proof () = (fun (c,t) -> { Entries.const_entry_body = c; const_entry_secctx = section_vars; const_entry_type = Some t; - const_entry_opaque = true }) + const_entry_opaque = true; + const_entry_inline_code = false }) proofs_and_types in let { compute_guard=cg ; strength=str ; hook=hook } = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index c4c821a9e5..91ef038ee5 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -28,6 +28,9 @@ let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp +let cbv_native env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Nativenorm.native_norm env c ctyp let set_strategy_one ref l = let k = @@ -206,7 +209,16 @@ let rec reduction_of_red_expr = function let redfun = contextually b lp vmfun in (redfun, VMcast) | CbvVm None -> (cbv_vm, VMcast) - + | CbvNative (Some lp) -> + let b = is_reference (snd lp) in + let lp = out_with_occurrences lp in + let nativefun _ env map c = + let tpe = Retyping.get_type_of env map c in + Nativenorm.native_norm env c tpe + in + let redfun = contextually b lp nativefun in + (redfun, NATIVEcast) + | CbvNative None -> (cbv_native, NATIVEcast) let subst_flags subs flags = { flags with rConst = List.map subs flags.rConst } diff --git a/tactics/leminv.ml b/tactics/leminv.ml index fa2931c807..942cdc77e0 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -231,7 +231,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op = { const_entry_body = invProof; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false }, + const_entry_opaque = false; + const_entry_inline_code = false + }, IsProof Lemma) in () diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index b2a79dda36..811ee03c71 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1763,7 +1763,8 @@ let declare_projection n instance_id r = { const_entry_body = term; const_entry_secctx = None; const_entry_type = Some typ; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false } in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 89cca15c8a..8fbab3ca1d 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -460,6 +460,7 @@ let intern_red_expr ist = function | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o) + | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r let intern_in_hyp_as ist lf (id,ipat) = diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 96634f963e..ac349bd8dc 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -591,6 +591,8 @@ let interp_red_expr ist sigma env = function sigma , Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | CbvVm o -> sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) + | CbvNative o -> + sigma , CbvNative (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o) | (Red _ | Hnf | ExtraRedExpr _ as r) -> sigma , r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 007ec9c6fa..d2d6de6239 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -122,6 +122,7 @@ let subst_redexp subst = function | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l) | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o) | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o) + | CbvNative o -> CbvNative (Option.map (subst_pattern_with_occurrences subst) o) | (Red _ | Hnf | ExtraRedExpr _ as r) -> r let subst_raw_may_eval subst = function diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0f0e43021d..c769fb3ba2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -262,8 +262,13 @@ let bind_red_expr_occurrences occs nbcl redexp = error_illegal_clause () else CbvVm (Some (occs,c)) + | CbvNative (Some (occl,c)) -> + if occl != AllOccurrences then + error_illegal_clause () + else + CbvNative (Some (occs,c)) | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ - | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None -> + | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None | CbvNative None -> error_occurrences_not_unsupported () | Unfold [] | Pattern [] -> assert false diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 20d3b2c1e8..3eb77bc063 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -182,7 +182,8 @@ let declare_record_instance gr ctx params = let ce = { const_entry_body= def; const_entry_secctx = None; const_entry_type=None; - const_entry_opaque=false } in + const_entry_opaque=false; + const_entry_inline_code = false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def @@ -197,8 +198,9 @@ let declare_class_instance gr ctx params = let ce = Entries.DefinitionEntry { const_entry_type = Some typ; const_entry_secctx = None; - const_entry_body= def; - const_entry_opaque=false } in + const_entry_body = def; + const_entry_opaque = false; + const_entry_inline_code = false } in try let cst = Declare.declare_constant ident (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in diff --git a/toplevel/class.ml b/toplevel/class.ml index 6f0ac17934..9d93d39f68 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -217,7 +217,9 @@ let build_id_coercion idf_opt source = { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_secctx = None; const_entry_type = Some typ_f; - const_entry_opaque = false } in + const_entry_opaque = false; + const_entry_inline_code = true + } in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 21838bf684..03fc6bd1fe 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -105,7 +105,8 @@ let declare_instance_constant k pri global imps ?hook id term termtype = { const_entry_body = term; const_entry_secctx = None; const_entry_type = Some termtype; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false } in DefinitionEntry entry, kind in let kn = Declare.declare_constant id cdecl in diff --git a/toplevel/command.ml b/toplevel/command.ml index fc039d968b..55ee2a37ca 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -82,7 +82,9 @@ let interp_definition bl red_option c ctypopt = { const_entry_body = body; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false + } | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls ~evdref ~fail_evar:false env_bl ctyp in let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in @@ -98,7 +100,9 @@ let interp_definition bl red_option c ctypopt = { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false + } in red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps @@ -503,8 +507,9 @@ let declare_fix kind f def t imps = const_entry_body = def; const_entry_secctx = None; const_entry_type = Some t; - const_entry_opaque = false } - in + const_entry_opaque = false; + const_entry_inline_code = false + } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in Autoinstance.search_declaration (ConstRef kn); @@ -696,7 +701,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = { const_entry_body = Evarutil.nf_evar !isevars body; const_entry_secctx = None; const_entry_type = Some ty; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false} in let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index f039a6c40f..e03c3e9b59 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -128,7 +128,9 @@ let define internal id c = { const_entry_body = c; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false }, + const_entry_opaque = false; + const_entry_inline_code = false + }, Decl_kinds.IsDefinition Scheme) in (match internal with | KernelSilent -> () diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 2f01e73232..a0300738b5 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -120,7 +120,9 @@ let define id internal c t = { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_opaque = false }, + const_entry_opaque = false; + const_entry_inline_code = false + }, Decl_kinds.IsDefinition Scheme) in definition_message id; kn diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index eea41c1523..e35b8de0e7 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -220,7 +220,9 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = { const_entry_body = body_i; const_entry_secctx = None; const_entry_type = Some t_i; - const_entry_opaque = opaq } in + const_entry_opaque = opaq; + const_entry_inline_code = false + } in let kn = declare_constant id (DefinitionEntry const, k) in (Global,ConstRef kn,imps) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 0aa15edda2..cf5f644652 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -72,10 +72,14 @@ let load = ref WithoutTop let is_native = Dynlink.is_native (* Sets and initializes a toplevel (if any) *) -let set_top toplevel = load := WithTop toplevel +let set_top toplevel = load := + WithTop toplevel; + Nativelib.load_obj := toplevel.load_obj (* Removes the toplevel (if any) *) -let remove ()= load := WithoutTop +let remove () = + load := WithoutTop; + Nativelib.load_obj := (fun x -> () : string -> unit) (* Tests if an Ocaml toplevel runs under Coq *) let is_ocaml_top () = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index e9f31bbca8..fd51564531 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -508,7 +508,8 @@ let declare_definition prg = { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false} in progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits @@ -586,7 +587,8 @@ let declare_obligation prg obl body = { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some ty; - const_entry_opaque = opaque } + const_entry_opaque = opaque; + const_entry_inline_code = false} in let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) diff --git a/toplevel/record.ml b/toplevel/record.ml index 17b07005e3..7926aecbd7 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -201,7 +201,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls const_entry_body = proj; const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_opaque = false } in + const_entry_opaque = false; + const_entry_inline_code = false } in let k = (DefinitionEntry cie,IsDefinition kind) in let kn = declare_constant ~internal:KernelSilent fid k in Declare.definition_message fid; @@ -304,7 +305,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls { const_entry_body = class_body; const_entry_secctx = None; const_entry_type = class_type; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false } in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) @@ -316,7 +318,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls { const_entry_body = proj_body; const_entry_secctx = None; const_entry_type = Some proj_type; - const_entry_opaque = false } + const_entry_opaque = false; + const_entry_inline_code = false } in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 935606fc4d..3d8a1eb76b 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -160,7 +160,7 @@ let rec uri_of_constr c = | GLetIn (_,na,b,c) -> url_string "let "; url_of_name na; url_string "\\def "; uri_of_constr b; url_string " in "; uri_of_constr c - | GCast (_,c, (CastConv t|CastVM t)) -> + | GCast (_,c, (CastConv t|CastVM t|CastNative t)) -> uri_of_constr c; url_string ":"; uri_of_constr t | GRec _ | GIf _ | GLetTuple _ | GCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint." |