diff --git a/src/core/build_template.ml b/src/core/build_template.ml index 2174d4e..2094d6f 100644 --- a/src/core/build_template.ml +++ b/src/core/build_template.ml @@ -122,7 +122,7 @@ struct log_rule ~lvl:3 "%s" cmd; run0 cmd (); (* NOTE [init] actually loads [src] into signature *) - ignore @@ Api.Env.Default.init src; + (* ignore @@ Api.Env.Default.init src; *) (* FIXME: Why this line is useful? *) Value.written out in target (Key.create out) +< Key.create src |> @@ -142,9 +142,10 @@ struct let ochan = open_out tg in let ofmt = Format.formatter_of_out_channel ochan in let entries = - let inchan = open_in src in - let e = Parsing.Parser.Parse_channel.parse md inchan in - close_in inchan; + let open Parsers.Parser in + let input = input_from_file src in + let e = parse input in + Parsers.Parser.close input; e in pp_entries ofmt entries; diff --git a/src/core/console.ml b/src/core/console.ml index db3e276..a98d314 100644 --- a/src/core/console.ml +++ b/src/core/console.ml @@ -84,7 +84,7 @@ struct (** Common options. *) let options : t list = [ ( "-I" - , Arg.String Kernel.Basic.add_path + , Arg.String Api.Files.add_path , " Add folder to Dedukti path" ) ; ( "-d" , Arg.Set_string indir diff --git a/src/core/deps.ml b/src/core/deps.ml index b24a13a..cfe8fb7 100644 --- a/src/core/deps.ml +++ b/src/core/deps.ml @@ -2,7 +2,7 @@ open Extras open Console open Kernel.Basic open Kernel.Term -open Parsing.Entry +open Parsers.Entry open Kernel.Rule let log_dep = new_logger "deps" @@ -65,7 +65,7 @@ let deps_of_entry : mident -> entry -> name list = fun mid e -> | _ -> assert false in let module D = Api.Dep in - D.compute_ideps := true; (* Compute dependencies of items *) + D.compute_all_deps := true; (* Compute dependencies of items *) D.make mid [e]; let name = mk_name mid id in try D.(NameSet.elements (get_data name).down) @@ -74,18 +74,11 @@ let deps_of_entry : mident -> entry -> name list = fun mid e -> let deps_of_md : mident -> DkTools.MdSet.t = fun md -> log_dep ~lvl:4 "of [%a]" Api.Pp.Default.print_mident md; - let file = Api.Dep.get_file md in - let inchan = open_in file in - Api.Dep.compute_ideps := false; - let entries = Parsing.Parser.Parse_channel.parse md inchan in - close_in inchan; - let module E = Api.Env.Make(Kernel.Reduction.Default) in - let module ErrorHandler = Api.Errors.Make(E) in - begin try Api.Dep.make md entries - with e -> ErrorHandler.graceful_fail None e - end; - let deps = Hashtbl.find Api.Dep.deps md in - Api.Dep.MDepSet.fold (fun (m,_) acc -> DkTools.MdSet.add m acc) + let file = Api.Files.get_file md in + Api.Dep.compute_all_deps := false; + let deps = Api.Processor.handle_files [file] Api.Processor.Dependencies in + let deps = Hashtbl.find deps md in + Kernel.Basic.MidentSet.fold (fun m acc -> DkTools.MdSet.add m acc) deps.deps DkTools.MdSet.empty (** Use build system to compute dependencies. *) diff --git a/src/core/deps.mli b/src/core/deps.mli index 914d06e..6216b64 100644 --- a/src/core/deps.mli +++ b/src/core/deps.mli @@ -1,6 +1,6 @@ open Extras open Kernel -open Parsing +open Parsers module QSet : Set.S with type elt = string (** Sets of strings. *) diff --git a/src/core/extras.ml b/src/core/extras.ml index 39128b3..31d7a05 100644 --- a/src/core/extras.ml +++ b/src/core/extras.ml @@ -96,14 +96,15 @@ module DkTools = struct module MdSet = Set.Make(Mident) (* TODO use Api.Dep.MDepSet everywhere? *) - let get_file : Mident.t -> string = Api.Dep.get_file - let init : string -> Mident.t = Api.Env.Default.init - type entry = Parsing.Entry.entry + let get_file : Mident.t -> string = Api.Files.get_file + let init : string -> Mident.t = Kernel.Basic.mk_mident - let get_path : unit -> string list = Kernel.Basic.get_path + type entry = Parsers.Entry.entry - let id_of_entry : Parsing.Entry.entry -> Kernel.Basic.ident = - let open Parsing.Entry in + let get_path : unit -> string list = Api.Files.get_path + + let id_of_entry : Parsers.Entry.entry -> Kernel.Basic.ident = + let open Parsers.Entry in function | Decl(_,id,_,_,_) -> id | Def(_,id,_,_,_,_) -> id @@ -128,7 +129,7 @@ module NameHashtbl = Hashtbl.Make(struct let hash = Hashtbl.hash end) module NameMap = Map.Make(struct - type t = Api.Dep.NameSet.elt + type t = Kernel.Basic.NameSet.elt let compare : t -> t -> int = Stdlib.compare end) diff --git a/src/ctpicef/latex.ml b/src/ctpicef/latex.ml index a488489..995f00e 100644 --- a/src/ctpicef/latex.ml +++ b/src/ctpicef/latex.ml @@ -1,4 +1,4 @@ -let export_to_string _ (e:Parsing.Entry.entry) = +let export_to_string _ (e:Parsers.Entry.entry) = ignore e; assert false diff --git a/src/cupicef/latex.ml b/src/cupicef/latex.ml index 5417ef3..cb740e6 100644 --- a/src/cupicef/latex.ml +++ b/src/cupicef/latex.ml @@ -1,4 +1,4 @@ -open Parsing.Entry +open Parsers.Entry open Kernel.Term open Kernel.Basic open Format diff --git a/src/export/export.ml b/src/export/export.ml index 0c94784..14ec6d8 100644 --- a/src/export/export.ml +++ b/src/export/export.ml @@ -12,11 +12,11 @@ sig val target : Systems.t (** Which target system to export to. *) - val compile : Kernel.Basic.mident -> Parsing.Entry.entry list -> ast + val compile : Kernel.Basic.mident -> Parsers.Entry.entry list -> ast (** [compile md es] builds an ast out of a list of Dedukti entries [es] coming from module [md]. *) - val decompile : ast -> Parsing.Entry.entry list + val decompile : ast -> Parsers.Entry.entry list (** [decompile ast] returns the list of Dedukti entries coming from ast [ast]. *) @@ -47,7 +47,7 @@ module GenBuildSys (E:S) : Makefile.S = struct (Key.t, Value.t) generator list = fun ext entries_pp -> let sysrule = function | Key.File(p) when Filename.extension p = ext -> - let srcmd = dk_of p |> Api.Env.Default.init in + let srcmd = dk_of p |> Kernel.Basic.mk_mident in Some(Rule.entry_printer p entries_pp srcmd) | _ -> None in diff --git a/src/sttfa/compile_type.ml b/src/sttfa/compile_type.ml index ff712db..e3351bb 100644 --- a/src/sttfa/compile_type.ml +++ b/src/sttfa/compile_type.ml @@ -2,7 +2,7 @@ open Sttfadk open Environ open Ast -module Denv = Api.Env.Default +module Denv = Api.Env module Dpp = Api.Pp.Default module Reduction = Kernel.Reduction diff --git a/src/sttfa/export/pvs.ml b/src/sttfa/export/pvs.ml index b677041..1197b3c 100644 --- a/src/sttfa/export/pvs.ml +++ b/src/sttfa/export/pvs.ml @@ -3,7 +3,7 @@ module D = Core.Deps module Basic = Kernel.Basic module Signature = Kernel.Signature module F = Format -module Denv = Api.Env.Default +module Denv = Api.Env let extension = "pvs" @@ -307,8 +307,14 @@ let remove_transitive_deps mdeps deps = let remove_dep dep deps = let md = Basic.mk_mident dep in let deps_from_signature md = - let deps = Signature.get_md_deps Basic.dloc md in - (D.QSet.of_list (List.map Basic.string_of_mident deps)) + match Api.Files.(find_dk ~ignore:false md (get_path ())) with + | None -> failwith "PVS EXPORT: Internal error, please report" + | Some file -> + let input = Parsers.Parser.input_from_file file in + let md = Parsers.Parser.md_of_input input in + Parsers.Parser.handle input (fun entry -> Api.Dep.make md [entry]); + let file_deps = Hashtbl.find Api.Dep.deps md in + Kernel.Basic.(MidentSet.fold (fun m md_deps -> D.QSet.add (string_of_mident m) md_deps) file_deps.deps) D.QSet.empty in let md_deps = match mdeps with diff --git a/src/sttfa/makefile.ml b/src/sttfa/makefile.ml index fd31fbe..bfcb998 100644 --- a/src/sttfa/makefile.ml +++ b/src/sttfa/makefile.ml @@ -8,7 +8,7 @@ let mk_generators : string -> (DkTools.Mident.t -> DkTools.entry list pp) -> (Key.t, Value.t) generator list = fun ext entries_pp -> let sysrule = function | Key.File(p) when Filename.extension p = ext -> - let srcmd = dk_of p |> Api.Env.Default.init in + let srcmd = dk_of p |> Kernel.Basic.mk_mident in Some(Rule.entry_printer p entries_pp srcmd) | _ -> None in