diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 269 |
1 files changed, 141 insertions, 128 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index eaddace4..123e7a6d 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors open Names -open Term +open Constr open Declarations open Util open Nativevalues @@ -16,6 +18,8 @@ open Nativeinstr open Nativelambda open Pre_env +[@@@ocaml.warning "-32-37"] + (** 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. *) @@ -23,7 +27,7 @@ to OCaml code. *) (** Local names **) (* The first component is there for debugging purposes only *) -type lname = { lname : name; luid : int } +type lname = { lname : Name.t; luid : int } let eq_lname ln1 ln2 = Int.equal ln1.luid ln2.luid @@ -40,35 +44,35 @@ 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 * pinductive (* prefix, inductive name *) - | Gconstruct of string * pconstructor (* prefix, constructor name *) - | Gconstant of string * pconstant (* prefix, constant name *) - | Gproj 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 + | Gind of string * inductive (* prefix, inductive name *) + | Gconstruct of string * constructor (* prefix, constructor name *) + | Gconstant of string * Constant.t (* prefix, constant name *) + | Gproj of string * Constant.t (* prefix, constant name *) + | Gcase of Label.t option * int + | Gpred of Label.t option * int + | Gfixtype of Label.t option * int + | Gnorm of Label.t option * int + | Gnormtbl of Label.t option * int | Ginternal of string | Grel of int - | Gnamed of identifier + | Gnamed of Id.t let eq_gname gn1 gn2 = match gn1, gn2 with | Gind (s1, ind1), Gind (s2, ind2) -> - String.equal s1 s2 && Univ.eq_puniverses eq_ind ind1 ind2 + String.equal s1 s2 && eq_ind ind1 ind2 | Gconstruct (s1, c1), Gconstruct (s2, c2) -> - String.equal s1 s2 && Univ.eq_puniverses eq_constructor c1 c2 + String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> - String.equal s1 s2 && Univ.eq_puniverses Constant.equal c1 c2 + String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, c1), Gproj (s2, c2) -> + String.equal s1 s2 && Constant.equal c1 c2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -84,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 @@ -92,12 +98,12 @@ let dummy_gname = open Hashset.Combine let gname_hash gn = match gn with -| Gind (s, (ind,u)) -> - combinesmall 1 (combine3 (String.hash s) (ind_hash ind) (Univ.Instance.hash u)) -| Gconstruct (s, (c,u)) -> - combinesmall 2 (combine3 (String.hash s) (constructor_hash c) (Univ.Instance.hash u)) -| Gconstant (s, (c,u)) -> - combinesmall 3 (combine3 (String.hash s) (Constant.hash c) (Univ.Instance.hash u)) +| Gind (s, ind) -> + combinesmall 1 (combine (String.hash s) (ind_hash ind)) +| Gconstruct (s, c) -> + combinesmall 2 (combine (String.hash s) (constructor_hash c)) +| Gconstant (s, c) -> + combinesmall 3 (combine (String.hash s) (Constant.hash c)) | Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i)) | Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i)) | Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i)) @@ -110,40 +116,30 @@ let gname_hash gn = match gn with 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) @@ -152,13 +148,13 @@ let fresh_gnormtbl l = type symbol = | SymbValue of Nativevalues.t - | SymbSort of sorts - | SymbName of name - | SymbConst of constant + | SymbSort of Sorts.t + | SymbName of Name.t + | SymbConst of Constant.t | SymbMatch of annot_sw | SymbInd of inductive | SymbMeta of metavariable - | SymbEvar of existential + | SymbEvar of Evar.t | SymbLevel of Univ.Level.t let dummy_symb = SymbValue (dummy_value ()) @@ -172,8 +168,7 @@ let eq_symbol sy1 sy2 = | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2 | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2 | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2 - | SymbEvar (evk1,args1), SymbEvar (evk2,args2) -> - Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2 + | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 | _, _ -> false @@ -186,10 +181,7 @@ let hash_symbol symb = | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) | SymbInd ind -> combinesmall 6 (ind_hash ind) | SymbMeta m -> combinesmall 7 m - | SymbEvar (evk,args) -> - let evh = Evar.hash evk in - let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in - combinesmall 8 hl + | SymbEvar evk -> combinesmall 8 (Evar.hash evk) | SymbLevel l -> combinesmall 9 (Univ.Level.hash l) module HashedTypeSymbol = struct @@ -211,47 +203,47 @@ let empty_symbols = [||] let get_value tbl i = match tbl.(i) with | SymbValue v -> v - | _ -> anomaly (Pp.str "get_value failed") + | _ -> anomaly (Pp.str "get_value failed.") let get_sort tbl i = match tbl.(i) with | SymbSort s -> s - | _ -> anomaly (Pp.str "get_sort failed") + | _ -> anomaly (Pp.str "get_sort failed.") let get_name tbl i = match tbl.(i) with | SymbName id -> id - | _ -> anomaly (Pp.str "get_name failed") + | _ -> anomaly (Pp.str "get_name failed.") let get_const tbl i = match tbl.(i) with | SymbConst kn -> kn - | _ -> anomaly (Pp.str "get_const failed") + | _ -> anomaly (Pp.str "get_const failed.") let get_match tbl i = match tbl.(i) with | SymbMatch case_info -> case_info - | _ -> anomaly (Pp.str "get_match failed") + | _ -> anomaly (Pp.str "get_match failed.") let get_ind tbl i = match tbl.(i) with | SymbInd ind -> ind - | _ -> anomaly (Pp.str "get_ind failed") + | _ -> anomaly (Pp.str "get_ind failed.") let get_meta tbl i = match tbl.(i) with | SymbMeta m -> m - | _ -> anomaly (Pp.str "get_meta failed") + | _ -> anomaly (Pp.str "get_meta failed.") let get_evar tbl i = match tbl.(i) with | SymbEvar ev -> ev - | _ -> anomaly (Pp.str "get_evar failed") + | _ -> anomaly (Pp.str "get_evar failed.") let get_level tbl i = match tbl.(i) with | SymbLevel u -> u - | _ -> anomaly (Pp.str "get_level failed") + | _ -> anomaly (Pp.str "get_level failed.") let push_symbol x = try HashtblSymbol.find symb_tbl x @@ -276,7 +268,7 @@ type primitive = | Mk_fix of rec_pos * int | Mk_cofix of int | Mk_rel of int - | Mk_var of identifier + | Mk_var of Id.t | Mk_proj | Is_accu | Is_int @@ -306,7 +298,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of Primitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option let eq_primitive p1 p2 = match p1, p2 with @@ -371,9 +363,9 @@ let primitive_hash = function | MLsub -> 33 | MLmul -> 34 | MLmagic -> 35 - | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim) + | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim) | Coq_primitive (prim, Some (prefix,kn)) -> - combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim)) + combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim)) | Mk_proj -> 38 | MLarrayget -> 39 | Mk_empty_instance -> 40 @@ -635,7 +627,7 @@ let decompose_MLlam c = (*s Global declaration *) type global = -(* | Gtblname of gname * identifier array *) +(* | Gtblname of gname * Id.t array *) | Gtblnorm of gname * lname array * mllambda array | Gtblfixtype of gname * lname array * mllambda array | Glet of gname * mllambda @@ -742,7 +734,7 @@ type env = 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; + env_named : (Id.t * mllambda) list ref; env_univ : lname option} let empty_env univ () = @@ -931,7 +923,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * Primitives.t * prim_aux array + | PAprim of string * Constant.t * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -998,11 +990,11 @@ let compile_prim decl cond paux = | Int31lt -> if Sys.word_size = 64 then app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|] - else app_prim (Coq_primitive (Primitives.Int31lt,None)) args + else app_prim (Coq_primitive (CPrimitives.Int31lt,None)) args | Int31le -> if Sys.word_size = 64 then app_prim Mk_bool [|(app_prim MLle (args_to_int args))|] - else app_prim (Coq_primitive (Primitives.Int31le, None)) args + else app_prim (Coq_primitive (CPrimitives.Int31le, None)) args | Int31lsl -> of_int (mk_lsl (args_to_int args)) | Int31lsr -> of_int (mk_lsr (args_to_int args)) | Int31land -> of_int (mk_land (args_to_int args)) @@ -1057,11 +1049,12 @@ let ml_of_instance instance u = let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) - | Levar(ev,ty) -> + | Levar(evk,ty,args) -> let tyn = fresh_lname Anonymous in - let i = push_symbol (SymbEvar ev) in + let i = push_symbol (SymbEvar evk) in + let args = MLarray(Array.map (ml_of_lam env l) args) in MLlet(tyn, ml_of_lam env l ty, - MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in @@ -1078,9 +1071,9 @@ let ml_of_instance instance u = 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) -> - let args = ml_of_instance env.env_univ (snd c) in - mkMLapp (MLglobal(Gconstant (prefix,c))) args + | Lconst (prefix, (c, u)) -> + let args = ml_of_instance env.env_univ u in + mkMLapp (MLglobal(Gconstant (prefix, c))) args | Lproj (prefix,c) -> MLglobal(Gproj (prefix,c)) | Lprim _ -> let decl,cond,paux = extract_prim (ml_of_lam env l) t in @@ -1291,17 +1284,17 @@ let ml_of_instance instance u = MLconstruct(prefix,cn,args) | Lconstruct (prefix, (cn,u)) -> let uargs = ml_of_instance env.env_univ u in - mkMLapp (MLglobal (Gconstruct (prefix, (cn,u)))) uargs + mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs | Luint v -> (match v with | UintVal i -> MLapp(MLprimitive Mk_uint, [|MLuint i|]) | UintDigits (prefix,cn,ds) -> - let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let c = MLglobal (Gconstruct (prefix, cn)) in let ds = Array.map (ml_of_lam env l) ds in let i31 = MLapp (MLprimitive Mk_I31_accu, [|c|]) in MLapp(i31, ds) | UintDecomp (prefix,cn,t) -> - let c = MLglobal (Gconstruct (prefix, (cn, Univ.Instance.empty))) in + let c = MLglobal (Gconstruct (prefix, cn)) in let t = ml_of_lam env l t in MLapp (MLprimitive Decomp_uint, [|c;t|])) | Lval v -> @@ -1314,9 +1307,9 @@ let ml_of_instance instance u = in let uarg = MLapp(MLprimitive MLmagic, [|uarg|]) in MLapp(MLprimitive Mk_sort, [|get_sort_code i; uarg|]) - | Lind (prefix, pind) -> - let uargs = ml_of_instance env.env_univ (snd pind) in - mkMLapp (MLglobal (Gind (prefix, pind))) uargs + | Lind (prefix, (ind, u)) -> + let uargs = ml_of_instance env.env_univ u in + mkMLapp (MLglobal (Gind (prefix, ind))) uargs | Llazy -> MLglobal (Ginternal "lazy") | Lforce -> MLglobal (Ginternal "Lazy.force") @@ -1514,7 +1507,7 @@ let string_of_dirpath = function (* 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 mod_uid_of_dirpath dir = string_of_dirpath (DirPath.repr dir) let link_info_of_dirpath dir = Linked (mod_uid_of_dirpath dir ^ ".") @@ -1533,27 +1526,27 @@ let string_of_label_def l = 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 + let dp = DirPath.repr dp in string_of_dirpath dp :: acc - | MPbound mbid -> ("X"^string_of_id (id_of_mbid mbid))::acc + | MPbound mbid -> ("X"^string_of_id (MBId.to_id 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,dp,l) = KerName.repr 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_con c = string_of_kn (Constant.user c) +let string_of_mind mind = string_of_kn (MutInd.user mind) let string_of_gname g = match g with - | Gind (prefix, ((mind,i), _)) -> + | Gind (prefix, (mind, i)) -> Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i - | Gconstruct (prefix, (((mind, i), j), _)) -> + | Gconstruct (prefix, ((mind, i), j)) -> Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1) - | Gconstant (prefix, (c,_)) -> + | Gconstant (prefix, c) -> Format.sprintf "%sconst_%s" prefix (string_of_con c) | Gproj (prefix, c) -> Format.sprintf "%sproj_%s" prefix (string_of_con c) @@ -1731,7 +1724,7 @@ let pp_mllam fmt l = | 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) + Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_accu -> Format.fprintf fmt "is_accu" | Is_int -> Format.fprintf fmt "is_int" @@ -1762,11 +1755,10 @@ let pp_mllam fmt l = | MLarrayget -> Format.fprintf fmt "Array.get" | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty" | Coq_primitive (op,None) -> - Format.fprintf fmt "no_check_%s" (Primitives.to_string op) + Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op) | Coq_primitive (op, Some (prefix,kn)) -> - let u = Univ.Instance.empty in - Format.fprintf fmt "%s %a" (Primitives.to_string op) - pp_mllam (MLglobal (Gconstant (prefix,(kn,u)))) + Format.fprintf fmt "%s %a" (CPrimitives.to_string op) + pp_mllam (MLglobal (Gconstant (prefix, kn))) in Format.fprintf fmt "@[%a@]" pp_mllam l @@ -1841,17 +1833,17 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = 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 = Context.Rel.length env.env_rel_context in + let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx 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 sigma univ auxdefs n = - let open Context.Rel in - let n = length env.env_rel_context - n in - let open Declaration in - match lookup n env.env_rel_context with + let open Context.Rel.Declaration in + let decl = Pre_env.lookup_rel n env in + let n = List.length env.env_rel_context.env_rel_ctx - n in + match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in @@ -1872,9 +1864,10 @@ and compile_named env sigma univ auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> - let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty + let no_univs = + match cb.const_universes with + | Monomorphic_const _ -> true + | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0 in begin match cb.const_body with | Def t -> @@ -1887,9 +1880,9 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix in - let l = con_label con in + let l = Constant.label con in let auxdefs,code = - if Univ.Instance.is_empty u then compile_with_fv env sigma None [] (Some l) code + if no_univs then compile_with_fv env sigma None [] (Some l) code else let univ = fresh_univ () in let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in @@ -1897,25 +1890,24 @@ let compile_constant env sigma prefix ~interactive con cb = in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); let code = - optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs) + optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); code, name | _ -> let i = push_symbol (SymbConst con) in let args = - if Univ.Instance.is_empty u then [|get_const_code i; MLarray [||]|] + if no_univs then [|get_const_code i; MLarray [||]|] else [|get_const_code i|] in (* let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const) *) - [Glet(Gconstant ("",(con,u)), mkMLapp (MLprimitive Mk_const) args)], + [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)], if interactive then LinkedInteractive prefix else Linked prefix end | Some pb -> - let u = Univ.Instance.empty in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -1930,19 +1922,21 @@ let compile_constant env sigma prefix ~interactive con cb = let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; asw_reloc = tbl; asw_finite = true } in let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in let _, arity = tbl.(0) in let ci_uid = fresh_lname Anonymous in let cargs = Array.init arity (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) in let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in + let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in let gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in - Glet(Gconstant ("",(con,u)), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal + Glet(Gconstant ("", con), mkMLlam fargs (MLapp (MLglobal gn, [|MLlocal arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix @@ -1966,18 +1960,18 @@ let is_code_loaded ~interactive name = if is_loaded_native_file s then true else (name := NotLinked; false) -let param_name = Name (id_of_string "params") -let arg_name = Name (id_of_string "arg") +let param_name = Name (Id.of_string "params") +let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = - let u = Declareops.inductive_instance mb in + let u = Declareops.inductive_polymorphic_context mb in 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), u)) in + let name = Gind ("", (mind, i)) in let accu = let args = - if Univ.Instance.is_empty u then + if Int.equal (Univ.AUContext.size u) 0 then [|get_ind_code j; MLarray [||]|] else [|get_ind_code j|] in @@ -1989,7 +1983,7 @@ let compile_mind prefix ~interactive mb mind stack = 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,u)), + Glet(Gconstruct ("", c), mkMLlam (Array.append params args) (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in @@ -2026,21 +2020,22 @@ let compile_mind_deps env prefix ~interactive (* 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 sigma prefix ~interactive init t = - match kind_of_term t with +let compile_deps env sigma prefix ~interactive init t = + let rec aux env lvl init t = + match kind t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in - let cb,(nameref,_) = lookup_constant_key c env in - let (_, (_, const_updates)) = init in - if is_code_loaded ~interactive nameref - || (Cmap_env.mem c const_updates) - then init - else + let c,u = get_alias env c in + let cb,(nameref,_) = lookup_constant_key c env in + let (_, (_, const_updates)) = init in + if is_code_loaded ~interactive nameref + || (Cmap_env.mem c const_updates) + then init + else let comp_stack, (mind_updates, const_updates) = match cb.const_proj, cb.const_body with | None, Def t -> - compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) + aux env lvl init (Mod_subst.force_constr t) | Some pb, _ -> let mind = pb.proj_ind in compile_mind_deps env prefix ~interactive init mind @@ -2055,12 +2050,30 @@ let rec compile_deps env sigma prefix ~interactive init t = | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let term = mkApp (mkConst (Projection.constant p), [|c|]) in - compile_deps env sigma prefix ~interactive init term + aux env lvl init term | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in - fold_constr (compile_deps env sigma prefix ~interactive) init t - | _ -> fold_constr (compile_deps env sigma prefix ~interactive) init t + fold_constr_with_binders succ (aux env) lvl init t + | Var id -> + let open Context.Named.Declaration in + begin match lookup_named id env with + | LocalDef (_,t,_) -> + aux env lvl init t + | _ -> init + end + | Rel n when n > lvl -> + let open Context.Rel.Declaration in + let decl = lookup_rel n env in + let env = env_of_rel n env in + begin match decl with + | LocalDef (_,t,_) -> + aux env lvl init t + | LocalAssum _ -> init + end + | _ -> fold_constr_with_binders succ (aux env) lvl init t + in + aux env 0 init t let compile_constant_field env prefix con acc cb = let (gl, _) = |