diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indTyping.ml | 10 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 21 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 31 |
3 files changed, 40 insertions, 22 deletions
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d9ccf81619..b19472dc99 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,16 +197,14 @@ let unbounded_from_below u cstrs = is u_k and is contributing. *) let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = let check_level l = - if Univ.LSet.mem l (Univ.ContextSet.levels uctx) && - unbounded_from_below l (Univ.ContextSet.constraints uctx) && - not (Univ.LSet.mem l ctor_levels) then - Some l - else None + Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + unbounded_from_below l (Univ.ContextSet.constraints uctx) && + not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in let univs = if template_check then - Univ.LSet.filter (fun l -> Option.has_some (check_level l) || Univ.Level.is_prop l) univs + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs else univs (* Doesn't check the universes can be generalized *) in let fold acc = function diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index ab915e2b8d..0d900c2ec9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -487,18 +487,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in - let transf num = - let arity = List.length (dest_subterms recarg).(num) in - if Int.equal arity 0 then - let p = (!nconst, 0) in - incr nconst; p - else - let p = (!nblock + 1, arity) in - incr nblock; p - (* les tag des constructeur constant commence a 0, - les tag des constructeur non constant a 1 (0 => accumulator) *) + let transf arity = + if Int.equal arity 0 then + let p = (!nconst, 0) in + incr nconst; p + else + let p = (!nblock + 1, arity) in + incr nblock; p + (* les tag des constructeur constant commence a 0, + les tag des constructeur non constant a 1 (0 => accumulator) *) in - let rtbl = Array.init (List.length cnames) transf in + let rtbl = Array.map transf consnrealargs in (* Build the inductive packet *) { mind_typename = id; mind_arity = arity; diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1cef729916..a62b51e8aa 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -27,15 +27,35 @@ let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) let output_dir = ".coq-native" -(* Extension of genereted ml files, stored for debugging purposes *) +(* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" let ( / ) = Filename.concat -(* We have to delay evaluation of include_dirs because coqlib cannot be guessed -until flags have been properly initialized *) +(* Directory for temporary files for the conversion and normalisation + (as opposed to compiling the library itself, which uses [output_dir]). *) +let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") + +let () = at_exit (fun () -> + if Lazy.is_val my_temp_dir then + try + let d = Lazy.force my_temp_dir in + Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); + Unix.rmdir d + with e -> + Feedback.msg_warning + Pp.(str "Native compile: failed to cleanup: " ++ + str(Printexc.to_string e) ++ fnl())) + +(* We have to delay evaluation of include_dirs because coqlib cannot + be guessed until flags have been properly initialized. It also lets + us avoid forcing [my_temp_dir] if we don't need it (eg stdlib file + without native compute or native conv uses). *) let include_dirs () = - [Filename.get_temp_dir_name (); Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] + let base = [Envars.coqlib () / "kernel"; Envars.coqlib () / "library"] in + if Lazy.is_val my_temp_dir + then (Lazy.force my_temp_dir) :: base + else base (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun _x -> () : string -> unit) @@ -44,7 +64,8 @@ let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) let get_ml_filename () = - let filename = Filename.temp_file "Coq_native" source_ext in + let temp_dir = Lazy.force my_temp_dir in + let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in filename, prefix |