diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e08d913bc6..c558e9ed03 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -8,7 +8,7 @@ open CErrors open Names -open Term +open Constr open Declarations open Util open Nativevalues @@ -25,7 +25,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 @@ -50,16 +50,16 @@ let fresh_lname n = type gname = | Gind of string * inductive (* prefix, inductive name *) | Gconstruct of string * constructor (* prefix, constructor name *) - | Gconstant of string * constant (* 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 + | 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 @@ -142,9 +142,9 @@ 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 @@ -163,7 +163,7 @@ let eq_symbol sy1 sy2 = | 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 + Evar.equal evk1 evk2 && Array.for_all2 Constr.equal args1 args2 | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2 | _, _ -> false @@ -266,7 +266,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 @@ -296,7 +296,7 @@ type primitive = | MLmagic | MLarrayget | Mk_empty_instance - | Coq_primitive of CPrimitives.t * (prefix * constant) option + | Coq_primitive of CPrimitives.t * (prefix * Constant.t) option let eq_primitive p1 p2 = match p1, p2 with @@ -625,7 +625,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 @@ -732,7 +732,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 () = @@ -921,7 +921,7 @@ let merge_branches t = type prim_aux = - | PAprim of string * constant * CPrimitives.t * prim_aux array + | PAprim of string * Constant.t * CPrimitives.t * prim_aux array | PAml of mllambda let add_check cond args = @@ -1504,7 +1504,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 ^ ".") @@ -1523,19 +1523,19 @@ 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 @@ -1877,7 +1877,7 @@ 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 no_univs then compile_with_fv env sigma None [] (Some l) code else @@ -1955,8 +1955,8 @@ 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_polymorphic_context mb in @@ -2016,7 +2016,7 @@ 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 + 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 @@ -2048,8 +2048,8 @@ let rec compile_deps env sigma prefix ~interactive init t = | 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 + Constr.fold (compile_deps env sigma prefix ~interactive) init t + | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t let compile_constant_field env prefix con acc cb = let (gl, _) = |