Dedukti import and export

.gitignore

@@ -0,0 +1,2 @@
+_build/
+**/*.exe

components/dedukti/deduktiImport.ml

@@ -0,0 +1,25 @@
+(* TODO: Forse baseuri e' gia' in status *)
+let rec eval_from_dedukti_stream ~asserted ~baseuri status buf =
+  try
+    let entry = Parsers.Parser.read buf in
+    Parsers.Entry.pp_entry Format.err_formatter entry;
+    let objs = ObjectConstruction.obj_of_entry status ~baseuri buf entry in
+    let check_and_add ((uri, _, _, _, _) as obj) =
+      HLog.message ("Tradotto!" ^ status#ppobj obj);
+      let status = NCicLibrary.add_obj status obj in
+      let xxaliases = GrafiteDisambiguate.aliases_for_objs status [ uri ] in
+      let mode = GrafiteAst.WithPreferences in
+      (* MATITA 1.0: fixme *)
+      let status = GrafiteEngine.eval_alias status (mode, xxaliases) in
+      status
+    in
+    (* TODO per fixare gli alias guardare matitaengine.ml da righe circa 230 235 *)
+    let status =
+      Option.fold ~none:status
+        ~some:(fun list ->
+          List.fold_left (fun _ obj -> check_and_add obj) status list)
+        objs
+    in
+
+    eval_from_dedukti_stream ~asserted ~baseuri status buf
+  with End_of_file -> (asserted, status)

components/dedukti/deduktiImport.mli

@@ -0,0 +1,7 @@
+(* TODO *)
+val eval_from_dedukti_stream :
+  asserted:'a ->
+  baseuri:string ->
+  (#GrafiteTypes.status as 'b) ->
+  Parsers.Parser.stream ->
+  'a * 'b

components/dedukti/dune

@@ -0,0 +1,7 @@
+(library
+ (name helm_dedukti)
+ (libraries helm_ng_library dedukti.parsers helm_ng_disambiguation helm_grafite_engine)
+ (wrapped false))
+(env
+  (_
+    (flags (:standard -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-42))))