yann@Dedukti-2.7

src/eksporti.ml

@@ -88,6 +88,4 @@ Available options for the selected mode:"
     Format.printf "%s\n" s;
     Arg.usage (Arg.align Cli.options) usage
   | e          ->
-    let module Denv = Api.Env.Default in
-    let module Derr = Api.Errors.Make(Denv) in
-    raise (Derr.graceful_fail None e)
+    raise Api.Env.(fail_env_error (dummy ()) Kernel.Basic.dloc e)

src/json/compile.ml

@@ -5,7 +5,7 @@ open Console
 open Extras
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module Jt = Json_types
 
@@ -165,15 +165,15 @@ struct
       let art2exp (sys, pth) =
         let item =
           if List.mem_eq B.mident_eq mdl M.encoding then None else
-            Some(M.item_of_entry mdl e)
+            Some (M.item_of_entry denv mdl e)
         in
         let ext = List.assoc sys Systems.exts in
         let file =
           Filename.(pth </> (B.string_of_mident mdl <.> ext))
         in
         { Jt.system = Systems.to_string sys
         ; file
-        ; etype = Option.map (M.string_of_item sys) item }
+        ; etype = Option.map (M.string_of_item denv sys) item }
       in
       (* Add section to download Dedukti file *)
       let exp =

src/json/compile.mli

@@ -1,5 +1,5 @@
 open Kernel
-open Parsing
+open Parsers
 
 val json_include : string ref
 (** Directory containing json files. Allows to read back already created json

src/json/makefile.ml

@@ -26,8 +26,7 @@ let want : string list -> Key.t list =
     json files stemming from [ms]. *)
 let json : (DkTools.Mident.t -> DkTools.entry list pp) -> string ->
   (Key.t, Value.t) rule = fun pp_entries tg ->
-  let module E = Api.Env.Default in
-  let md = E.init Filename.(dirname tg </> !/tg <.> "dk") in
+  let md = DkTools.init Filename.(dirname tg </> !/tg <.> "dk") in
   let md_deps =
     Deps.deps_of_md md |> DkTools.MdSet.to_seq |> List.of_seq
   in
@@ -43,9 +42,10 @@ let json : (DkTools.Mident.t -> DkTools.entry list pp) -> string ->
     let ochan = open_out tg in
     let ofmt = Format.formatter_of_out_channel ochan in
     let entries =
-      let inchan = open_in (Api.Dep.get_file md) in
-      let r = Parsing.Parser.Parse_channel.parse md inchan in
-      close_in inchan;
+      let open Parsers.Parser in
+      let input = input_from_file (DkTools.get_file md) in
+      let r = parse input in
+      Parsers.Parser.close input;
       r
     in
     pp_entries ofmt entries;

src/middleware/midAgda.ml

@@ -1,6 +1,6 @@
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module R = Kernel.Rule
 module T = Kernel.Term
 module U = Core.Uri
@@ -12,7 +12,7 @@ type tx =
   | TxCons (** Constructor of a type *)
   | TxProj (** Projection *)
 
-type item = Parsing.Entry.entry
+type item = Parsers.Entry.entry
 
 exception IllTaxon
 (** Exception raised when reading an ill formed taxon. *)

src/middleware/midCtpicef.ml

@@ -1,7 +1,7 @@
 open Core
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Uri
 
@@ -67,9 +67,9 @@ let label = function
 
 (* TODO: Define cic items, and how to print them on the website
    depending on the export system *)
-type item = Kernel.Basic.mident * Parsing.Entry.entry
-let item_of_entry md e = (md,e)
-let string_of_item target (md,e) = match target with
+type item = Kernel.Basic.mident * Parsers.Entry.entry
+let item_of_entry _ md e = (md,e)
+let string_of_item _ target (md,e) = match target with
   | Systems.Latex -> Ctpicef.Latex.export_to_string md e
   | sys -> Console.exit_with "Encoding ctpicef doesn't support target: %s"
              (Systems.to_string sys)

src/middleware/midCupicef.ml

@@ -1,7 +1,7 @@
 open Core
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Uri
 
@@ -67,11 +67,11 @@ let label = function
 
 (* TODO: Define cic items, and how to print them on the website
    depending on the export system *)
-type item = Kernel.Basic.mident * Parsing.Entry.entry
-let item_of_entry  md e = (md,e)
-let string_of_item target (md,e) = match target with
+type item = Kernel.Basic.mident * Parsers.Entry.entry
+let item_of_entry _ md e = (md,e)
+let string_of_item _ target (md,e) = match target with
   | Systems.Latex -> Cupicef.Latex.export_to_string md e
   | sys -> Console.exit_with "Encoding cupicef doesn't support target: %s"
              (Systems.to_string sys)
 
-let get_exporter = Cupicef.Latex.get_exporter
+let get_exporter _ = Cupicef.Latex.get_exporter

src/middleware/midSttfa.ml

@@ -1,6 +1,6 @@
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Core.Uri
 
@@ -77,9 +77,9 @@ let label = function
   | TxDef -> ("body", Some("type_annotation"))
   | TxThm -> ("statement", None)
 
-let item_of_entry mident entry = Sttfa__Compile.compile_entry mident entry
+let item_of_entry denv mident entry = Sttfa__Compile.compile_entry denv mident entry
 
-let string_of_item target =
-  Sttfa.Exporter.export_to_system_as_string target
+let string_of_item denv target =
+  Sttfa.Exporter.export_to_system_as_string denv target
 
 let get_exporter = Sttfa.Exporter.get_sttfa_exporter

src/middleware/middleware.ml

@@ -27,7 +27,7 @@ module type S = sig
   val encoding : DkTools.Mident.t list
   (** List of modules that encode the theory. *)
 
-  val tx_of_entry : Parsing.Entry.entry -> tx option
+  val tx_of_entry : Parsers.Entry.entry -> tx option
   (** [tx_of_entry e] returns a taxon of an entry [e], if it is
       taxon-associated entry (ie. a declaration, not a command). *)
 
@@ -58,20 +58,20 @@ module type S = sig
   (** [label tx] returns labels for the fields {!Json_types.item.term} and
       {!Json_types.item.term_opt}. *)
 
-  val item_of_entry : DkTools.Mident.t -> DkTools.entry -> item
+  val item_of_entry : Api.Env.t -> DkTools.Mident.t -> DkTools.entry -> item
   (** [item_of_entry md entry] returns an item of the logic given an appropriate
       Dedukti entry [entry] of module [md]. *)
 
   (** {b NOTE} The export section of the website will
       - Display the output of {!val:string_of_item} for all statements
       - Offer to download the whole file processed with {!val:get_exporter}. *)
 
-  val string_of_item : Systems.t -> item -> string
+  val string_of_item : Api.Env.t -> Systems.t -> item -> string
   (** [string_of_item system item] returns a string representation
       of [item] in the export system [system].
       This will be printed on the website in the export fields. *)
 
-  val get_exporter : Systems.t -> (module Export.S)
+  val get_exporter : Api.Env.t -> Systems.t -> (module Export.S)
   (** [get_exporter system] Generate an Exporter module to the given system.
       This allows to handle export through the Makefile system. *)
 end
@@ -90,8 +90,8 @@ struct
   let is_axiomatic _ = false
   let fields_of_def _ _ t = t,None
   let label _ = "dummy",None
-  let item_of_entry _ _ = ()
-  let string_of_item _ _ = "dummy"
+  let item_of_entry _ _ _ = ()
+  let string_of_item _ _ _ = "dummy"
   let get_exporter _ = assert false
 end
 

src/sttfa/compile.ml

@@ -9,24 +9,24 @@ module CType  = Compile_type
 module CTerm  = Compile_term
 module CProof = Compile_proof
 module Term = Kernel.Term
-module Entry = Parsing.Entry
+module Entry = Parsers.Entry
 
 let log_sttfa = new_logger "stfc"
 let log_sttfa = log_sttfa.logger
 
-let compile_declaration name ty =
+let compile_declaration denv name ty =
   match ty with
   | Term.App (cst, a, []) when is_sttfa_const sttfa_etap cst ->
     (* Format.eprintf "[COMPILE] parameter: %a@." Pp.print_name name ; *)
-      let ty' = CType.compile_type empty_env a in
+      let ty' = CType.compile_type denv empty_env a in
       Parameter (of_name name, ty')
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eta cst ->
     (* Format.eprintf "[COMPILE] parameter: %a@." Pp.print_name name ; *)
-      let ty' = CType.compile__type empty_env a in
+      let ty' = CType.compile__type denv empty_env a in
       Parameter (of_name name, Ty ty')
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eps cst ->
     (* Format.eprintf "[COMPILE] axiom: %a@." Pp.print_name name ; *)
-      let te' = CTerm.compile_term empty_env a in
+      let te' = CTerm.compile_term denv empty_env a in
       Axiom (of_name name, te')
   | _ ->
     if Sttfadk.is_tyop ty then
@@ -36,53 +36,53 @@ let compile_declaration name ty =
       end
     else assert false
 
-let compile_definition name ty term =
+let compile_definition denv name ty term =
   match ty with
   | Term.App (cst, a, []) when is_sttfa_const sttfa_etap cst ->
-    Definition(of_name name, CType.compile_type empty_env a, CTerm.compile_term empty_env term)
+    Definition(of_name name, CType.compile_type denv empty_env a, CTerm.compile_term denv empty_env term)
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eps cst ->
     (* The statement written and the one we get from the proof are beta,delta convertible. *)
-    let j, proof = CProof.compile_proof empty_env term in
-    let a' = CTerm.compile_term empty_env a in
+    let j, proof = CProof.compile_proof denv empty_env term in
+    let a' = CTerm.compile_term denv empty_env a in
     let proof' =
       if j.thm = a' then proof
       else
         Conv
           ( {j with thm=a'}
           , proof
-          , Sttfatyping.Tracer.annotate empty_env j.thm a'
+          , Sttfatyping.Tracer.annotate denv empty_env j.thm a'
           )
     in
-    Theorem (of_name name, CTerm.compile_term empty_env a, proof')
+    Theorem (of_name name, CTerm.compile_term denv empty_env a, proof')
   | _ ->
     if is_tyop ty then
       begin
         (* Format.eprintf "[COMPILE] typeop: %a@." Pp.print_name name ; *)
-        let vars,ty = CType.compile_type_definition empty_env term in
+        let vars,ty = CType.compile_type_definition denv empty_env term in
         TypeDef(of_name name, vars, ty)
       end
     else
       assert false
 
-let compile_entry : Basic.mident * Entry.entry -> item =
+let compile_entry denv : Basic.mident * Entry.entry -> item =
   fun (md, e) ->
-  let open Parsing.Entry in
-  let module Ev = Api.Env.Default in
+  let open Parsers.Entry in
+  let module Ev = Api.Env in
   let module Pp = Api.Pp.Default in
   match e with
   | Decl(l,id,sc,st,ty) ->
-    Ev.declare l id sc st ty;
+    Ev.declare denv l id sc st ty;
     log_sttfa ~lvl:6 "compiling decl [%a]" Pp.print_ident id;
-    compile_declaration (Basic.mk_name md id) ty
+    compile_declaration denv (Basic.mk_name md id) ty
   | Def(l,id,sc,f,Some ty,te) ->
-    Ev.define l id sc f te (Some ty);
+    Ev.define denv l id sc f te (Some ty);
     log_sttfa ~lvl:6 "compiling def [%a]" Pp.print_ident id;
-    compile_definition (Basic.mk_name md id) ty te
+    compile_definition denv (Basic.mk_name md id) ty te
   | Def(_)   -> exit_with "Definition without types are not supported"
   | Rules(_) -> exit_with "Rules are not part of the sttforall logic"
   | _        -> exit_with "Dedukti Commands are not supported"
 
 (** Memoized [compile_entry]. *)
-let compile_entry : Basic.mident -> Entry.entry -> item =
+let compile_entry denv : Basic.mident -> Entry.entry -> item =
   let eq (m, e) (m', e') = Kernel.Basic.mident_eq m m' && Stdlib.(=) e e' in
-  let f = memoize ~eq compile_entry in fun m e -> f (m, e)
+  let f = memoize ~eq (compile_entry denv) in fun m e -> f (m, e)