diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2013-12-29 10:53:06 -0500 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2013-12-29 11:04:25 -0500 |
commit | 381b2c6e77cd204aa143192a5a65e8832ae0633b (patch) | |
tree | 2f26dca0d8085664d9bffde2c0dde5939c456b84 /kernel | |
parent | 651094ccfd2d8106a8b0e75c27dc89afb369d4b3 (diff) |
Got rid of unused lazy flag in the native compiler.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/nativecode.ml | 18 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 9 | ||||
-rw-r--r-- | kernel/pre_env.ml | 7 | ||||
-rw-r--r-- | kernel/pre_env.mli | 4 |
4 files changed, 18 insertions, 20 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 219ccd220..4e34cd60f 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1170,7 +1170,7 @@ let string_of_dirpath s = "N"^string_of_dirpath s let mod_uid_of_dirpath dir = string_of_dirpath (repr_dirpath dir) let link_info_of_dirpath dir = - ref (Linked (mod_uid_of_dirpath dir ^ ".", false)) + ref (Linked (mod_uid_of_dirpath dir ^ ".")) let string_of_name x = match x with @@ -1487,8 +1487,8 @@ let compile_constant env prefix ~interactive con body = let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let name = - if interactive then LinkedInteractive (prefix, is_lazy) - else Linked (prefix, is_lazy) + if interactive then LinkedInteractive prefix + else Linked prefix in let l = con_label con in let auxdefs,code = compile_with_fv env [] (Some l) code in @@ -1499,8 +1499,8 @@ let compile_constant env prefix ~interactive con body = | _ -> let i = push_symbol (SymbConst con) in [Glet(Gconstant ("",con), MLapp (MLprimitive Mk_const, [|get_const_code i|]))], - if interactive then LinkedInteractive (prefix, false) - else Linked (prefix, false) + if interactive then LinkedInteractive prefix + else Linked prefix let loaded_native_files = ref ([] : string list) @@ -1513,10 +1513,10 @@ let register_native_file s = let is_code_loaded ~interactive name = match !name with | NotLinked -> false - | LinkedInteractive (s,_) -> + | LinkedInteractive s -> if (interactive && is_loaded_native_file s) then true else (name := NotLinked; false) - | Linked (s,_) -> + | Linked s -> if is_loaded_native_file s then true else (name := NotLinked; false) @@ -1565,8 +1565,8 @@ let compile_mind_deps env prefix ~interactive compile_mind prefix ~interactive mib mind comp_stack in let name = - if interactive then LinkedInteractive (prefix, false) - else Linked (prefix, false) + if interactive then LinkedInteractive prefix + else Linked prefix in let upd = (nameref, name) in let mind_updates = Mindmap_env.add mind upd mind_updates in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 7e46a0550..800c8e5fb 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,7 +14,6 @@ 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 @@ -90,15 +89,15 @@ let get_mind_prefix env mind = let _,name = lookup_mind_key mind env in match !name with | NotLinked -> "" - | Linked (s,_) -> s - | LinkedInteractive (s,_) -> s + | Linked s -> s + | LinkedInteractive s -> s let get_const_prefix env c = let _,(nameref,_) = lookup_constant_key c env in match !nameref with | NotLinked -> "" - | Linked (s,_) -> s - | LinkedInteractive (s,_) -> s + | Linked s -> s + | LinkedInteractive s -> s (* A generic map function *) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index d96492020..64d9d1a17 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -27,12 +27,11 @@ open Declarations (* used by the VM. *) type key = int option ref -(** Linking information for the native compiler. The boolean flag indicates if - the term is protected by a lazy tag. *) +(** Linking information for the native compiler. *) type link_info = - | Linked of string * bool - | LinkedInteractive of string * bool + | Linked of string + | LinkedInteractive of string | NotLinked type constant_key = constant_body * (link_info ref * key) diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index b6b6b4828..93c8b15f7 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -15,8 +15,8 @@ open Declarations (** The type of environments. *) type link_info = - | Linked of string * bool - | LinkedInteractive of string * bool + | Linked of string + | LinkedInteractive of string | NotLinked type key = int option ref |