[WIP] Logipedia: Update to Dedukti 2.7

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;

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

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. *)

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. *)

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)
 

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

src/cupicef/latex.ml

@@ -1,4 +1,4 @@
-open Parsing.Entry
+open Parsers.Entry
 open Kernel.Term
 open Kernel.Basic
 open Format

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

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

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

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