diff options
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." |