From ef225b816c82d4fad37993f963804e51152f4dac Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 10 Jan 2023 17:59:08 +0100 Subject: [PATCH] auxiliary executables (xoa, matitadep, probe, matex) ported to dune --- matita/components/binaries/matex/Makefile | 5 -- matita/components/binaries/matex/dune | 12 ++++ matita/components/binaries/matex/engine.ml | 14 ++-- matita/components/binaries/matex/ground.ml | 4 +- matita/components/binaries/matex/matex.ml | 2 +- matita/components/binaries/matitadep/Makefile | 6 -- matita/components/binaries/matitadep/dune | 12 ++++ matita/components/binaries/probe/Makefile | 6 -- matita/components/binaries/probe/dune | 15 +++++ .../components/binaries/probe/matitaList.ml | 1 - matita/components/binaries/probe/nCicScan.ml | 4 +- matita/components/binaries/xoa/Makefile | 6 -- matita/components/binaries/xoa/dune | 12 ++++ matita/components/binaries/xoa/engine.ml | 6 +- matita/components/binaries/xoa/lib.ml | 64 +++++++++---------- matita/components/binaries/xoa/lib.mli | 2 +- matita/components/binaries/xoa/xoa.ml | 7 +- 17 files changed, 104 insertions(+), 74 deletions(-) create mode 100644 matita/components/binaries/matex/dune delete mode 100644 matita/components/binaries/matitadep/Makefile create mode 100644 matita/components/binaries/matitadep/dune delete mode 100644 matita/components/binaries/probe/Makefile create mode 100644 matita/components/binaries/probe/dune delete mode 100644 matita/components/binaries/xoa/Makefile create mode 100644 matita/components/binaries/xoa/dune diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile index b437afb5b..7783a0570 100644 --- a/matita/components/binaries/matex/Makefile +++ b/matita/components/binaries/matex/Makefile @@ -1,9 +1,4 @@ EXEC = matex -VERSION=0.1.0 - -REQUIRES = helm-ng_library - -include ../Makefile.common MATEX = ./$(EXEC).native PROBE = ../probe/probe.native diff --git a/matita/components/binaries/matex/dune b/matita/components/binaries/matex/dune new file mode 100644 index 000000000..e49bde67a --- /dev/null +++ b/matita/components/binaries/matex/dune @@ -0,0 +1,12 @@ +(executable + (name matex) + (public_name matex) + (promote (until-clean)) + (libraries helm_ng_library) + (modules_without_implementation) + (modules alpha anticipate engine ground options TeXOutput kernel meta TeX matex) +) + +(env + (_ + (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 324d114a9..aef518025 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -12,7 +12,7 @@ module F = Filename module L = List module P = Printf -module S = String +(* module S = String *) module U = NUri module R = NReference @@ -26,7 +26,7 @@ module K = Kernel module T = TeX module O = TeXOutput module A = Anticipate -module M = Meta +(* module M = Meta *) module N = Alpha type status = { @@ -86,7 +86,7 @@ let get_head = function end | _ -> None -let proc_sort st is = function +let proc_sort _st is = function | C.Prop -> T.Macro "PROP" :: is | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is @@ -214,7 +214,7 @@ let rec proc_proof st ris t = match t with let ris = T.Macro "STEP" :: mk_inferred st t ris in let tts = L.rev_map (proc_term st []) rts in mk_exit st (T.rev_mk_args tts ris) - | C.Match (w, u, v, ts) -> + | C.Match (_w, _u, v, ts) -> let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in let ris = T.Macro "DEST" :: mk_inferred st t ris in let tts = L.rev_map (proc_term st []) rts in @@ -290,13 +290,13 @@ let proc_pair s ss u = function O.out_text och (text_t s name t); close_out och -let proc_fun ss (r, s, i, u, t) = +let proc_fun ss (_r, s, _i, u, t) = proc_pair s (s :: ss) u (Some t) -let proc_constructor ss (r, s, u) = +let proc_constructor ss (_r, s, u) = proc_pair s (s :: ss) u None -let proc_type ss (r, s, u, cs) = +let proc_type ss (_r, s, u, cs) = proc_pair s (s :: ss) u None; L.iter (proc_constructor ss) cs diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml index 7eebedb7d..3c75b4032 100644 --- a/matita/components/binaries/matex/ground.ml +++ b/matita/components/binaries/matex/ground.ml @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module L = List +(* module L = List *) module P = Printf module S = String @@ -48,7 +48,7 @@ let rec foldi_left mapi i a = function | [] -> a | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl -let rec rev_mapi mapi i l = +let rev_mapi mapi i l = let map i a hd = mapi i hd :: a in foldi_left map i [] l diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml index ddd413049..66faa9859 100644 --- a/matita/components/binaries/matex/matex.ml +++ b/matita/components/binaries/matex/matex.ml @@ -19,7 +19,7 @@ module L = Librarian module X = Ground module G = Options module E = Engine -module O = TeXOutput +(* module O = TeXOutput *) module K = Kernel let help_O = " Set this output directory" diff --git a/matita/components/binaries/matitadep/Makefile b/matita/components/binaries/matitadep/Makefile deleted file mode 100644 index 2fe33e60b..000000000 --- a/matita/components/binaries/matitadep/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -EXEC = matitadep -VERSION=0.1.0 - -REQUIRES = helm-ng_library - -include ../Makefile.common diff --git a/matita/components/binaries/matitadep/dune b/matita/components/binaries/matitadep/dune new file mode 100644 index 000000000..8988331ee --- /dev/null +++ b/matita/components/binaries/matitadep/dune @@ -0,0 +1,12 @@ +(executable + (name matitadep) + (public_name matitadep) + (promote (until-clean)) + (libraries helm_ng_library) + (modules_without_implementation) + (modules matitadep) +) + +(env + (_ + (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings diff --git a/matita/components/binaries/probe/Makefile b/matita/components/binaries/probe/Makefile deleted file mode 100644 index 24daac41d..000000000 --- a/matita/components/binaries/probe/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -EXEC = probe -VERSION=0.1.0 - -REQUIRES = helm-ng_library - -include ../Makefile.common diff --git a/matita/components/binaries/probe/dune b/matita/components/binaries/probe/dune new file mode 100644 index 000000000..19e20a3a5 --- /dev/null +++ b/matita/components/binaries/probe/dune @@ -0,0 +1,15 @@ +(ocamllex macLexer) + +(executable + (name probe) + (public_name probe) + (promote (until-clean)) + (libraries helm_ng_library) + (modules_without_implementation) + (modules macLexer engine error matitaRemove nCicScan matitaList options probe) +) + +(env + (_ + (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings + diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 95250b26c..e00f0c76c 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -11,7 +11,6 @@ module A = Array module F = Filename -module P = Printf module S = String module Y = Sys diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index 736baafbc..3accc4e71 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -39,7 +39,7 @@ let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour) let add_ind n = O.add_xflavour n `Inductive -let rec set_list c ts cts = +let set_list c ts cts = let map cts t = (c, t) :: cts in L.fold_left map cts ts @@ -84,7 +84,7 @@ let rec scan_term st = function | (_, C.Sort _) :: tl -> scan_term (inc st) tl | (c, C.Rel i) :: tl -> scan_term (scan_lref st c i) tl | (_, C.Const p) :: tl -> scan_term (scan_gref st p) tl - | (_, C.Appl []) :: tl -> X.malformed () + | (_, C.Appl []) :: _ -> X.malformed () | (c, C.Appl ts) :: tl -> scan_term (add st (pred (L.length ts))) (set_list c ts tl) | (c, C.Match (_, t0, t1, ts)) :: tl -> diff --git a/matita/components/binaries/xoa/Makefile b/matita/components/binaries/xoa/Makefile deleted file mode 100644 index 1933a2003..000000000 --- a/matita/components/binaries/xoa/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -EXEC = xoa -VERSION=0.2.0 - -REQUIRES = helm-registry - -include ../Makefile.common diff --git a/matita/components/binaries/xoa/dune b/matita/components/binaries/xoa/dune new file mode 100644 index 000000000..631bbcb99 --- /dev/null +++ b/matita/components/binaries/xoa/dune @@ -0,0 +1,12 @@ +(executable + (name xoa) + (public_name xoa) + (promote (until-clean)) + (libraries helm_registry) + (modules_without_implementation) + (modules ast lib ast engine xoa) +) + +(env + (_ + (flags (:standard -thread -rectypes -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70-50-29)))) ; -29 for non portable strings diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml index 47770e710..1c5ae3318 100644 --- a/matita/components/binaries/xoa/engine.ml +++ b/matita/components/binaries/xoa/engine.ml @@ -52,7 +52,7 @@ let mk_exists ooch noch c v = let pre_appl n = P.sprintf "%s %s" (pre n) ele_seq in let pre_type = string_iter " → " pre_appl c in - let qm n = "?" in + let qm _n = "?" in let qm_set = string_iter " " qm v in let qm_pre = string_iter " " qm c in @@ -99,7 +99,7 @@ let mk_or ooch noch c = let pre_list = string_iter "," pre c in let pre_seq = string_iter " " pre c in - let qm n = "?" in + let qm _n = "?" in let qm_pre = string_iter " " qm c in let term n = P.sprintf "term 29 P%u" (c - n) in @@ -139,7 +139,7 @@ let mk_and ooch noch c = let pre_type = string_iter " → " pre c in let pre_seq = string_iter " " pre c in - let qm n = "?" in + let qm _n = "?" in let qm_pre = string_iter " " qm c in let term n = P.sprintf "term 34 P%u" (c - n) in diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml index f2bf31757..9684dc558 100644 --- a/matita/components/binaries/xoa/lib.ml +++ b/matita/components/binaries/xoa/lib.ml @@ -14,51 +14,51 @@ module K = Sys module R = Helm_registry -let template = "matita.ma.templ" +let template = "../../../matita/matita.ma.templ" let myself = F.basename Sys.argv.(0) -let get_preamble conf = - R.load_from conf; - let rt_base_dir = R.get_string "matita.rt_base_dir" in - F.concat rt_base_dir template +let rt_base_dir = F.dirname Sys.argv.(0) + +let get_preamble () = + F.concat rt_base_dir template let copy_preamble preamble och = - let ich = open_in preamble in - let rec read () = - Printf.fprintf och "%s\n" (input_line ich); read () - in - try read () with End_of_file -> close_in ich + let ich = open_in preamble in + let rec read () = + Printf.fprintf och "%s\n" (input_line ich); read () + in + try read () with End_of_file -> close_in ich let print_header def och = let msg = if def then "LOGIC" else "GROUND NOTATION" in - let stars = String.make (72 - String.length msg) '*' in - Printf.fprintf och "(* %s %s*)\n\n" msg stars + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars let print_comment och = - let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in - let stars = String.make (72 - String.length msg) '*' in - Printf.fprintf och "(* %s %s*)\n\n" msg stars + let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars let exists_out name = - let path = [ - R.get_string "xoa.output_dir"; - name - ] in - let name = List.fold_left F.concat "" path in - K.file_exists (name ^ ".ma") + let path = [ + R.get_string "xoa.output_dir"; + name + ] in + let name = List.fold_left F.concat "" path in + K.file_exists (name ^ ".ma") let open_out def preamble name = - let path = [ - R.get_string "xoa.output_dir"; - name - ] in - let name = List.fold_left F.concat "" path in - let och = open_out (name ^ ".ma") in - copy_preamble preamble och; - print_header def och; - print_comment och; - och + let path = [ + R.get_string "xoa.output_dir"; + name + ] in + let name = List.fold_left F.concat "" path in + let och = open_out (name ^ ".ma") in + copy_preamble preamble och; + print_header def och; + print_comment och; + och let out_include och s = - Printf.fprintf och "include \"%s\".\n\n" s + Printf.fprintf och "include \"%s\".\n\n" s diff --git a/matita/components/binaries/xoa/lib.mli b/matita/components/binaries/xoa/lib.mli index cc66968d3..2cd5fb53f 100644 --- a/matita/components/binaries/xoa/lib.mli +++ b/matita/components/binaries/xoa/lib.mli @@ -9,7 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -val get_preamble: string -> string +val get_preamble: unit -> string val exists_out: string -> bool diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index 64ce87b17..3d35f1932 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -18,6 +18,9 @@ module E = Engine let incremental = ref true let separate = ref false +let preamble = + L.get_preamble () + let clear () = incremental := true; separate := false; @@ -33,7 +36,7 @@ let unm_and s = Scanf.sscanf s "%u" A.mk_and let process_centralized conf = - let preamble = L.get_preamble conf in + R.load_from conf; if R.has "xoa.objects" && R.has "xoa.notations" then begin let ooch = L.open_out true preamble (R.get_string "xoa.objects") in let noch = L.open_out false preamble (R.get_string "xoa.notations") in @@ -71,7 +74,7 @@ let generate (p, o, n) d = end let process_distributed conf = - let preamble = L.get_preamble conf in + R.load_from conf; if R.has "xoa.objects" && R.has "xoa.notations" then begin let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in List.iter (generate st) (R.get_list unm_ex "xoa.ex"); -- 2.39.2