EXEC = matex
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
MATEX = ./$(EXEC).native
PROBE = ../probe/probe.native
--- /dev/null
+(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
module F = Filename
module L = List
module P = Printf
-module S = String
+(* module S = String *)
module U = NUri
module R = NReference
module T = TeX
module O = TeXOutput
module A = Anticipate
-module M = Meta
+(* module M = Meta *)
module N = Alpha
type status = {
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
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
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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module L = List
+(* module L = List *)
module P = Printf
module S = String
| [] -> 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
module X = Ground
module G = Options
module E = Engine
-module O = TeXOutput
+(* module O = TeXOutput *)
module K = Kernel
let help_O = "<dir> Set this output directory"
+++ /dev/null
-EXEC = matitadep
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
--- /dev/null
+(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
+++ /dev/null
-EXEC = probe
-VERSION=0.1.0
-
-REQUIRES = helm-ng_library
-
-include ../Makefile.common
--- /dev/null
+(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
+
module A = Array
module F = Filename
-module P = Printf
module S = String
module Y = Sys
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
| (_, 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 ->
+++ /dev/null
-EXEC = xoa
-VERSION=0.2.0
-
-REQUIRES = helm-registry
-
-include ../Makefile.common
--- /dev/null
+(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
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
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
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
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
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val get_preamble: string -> string
+val get_preamble: unit -> string
val exists_out: string -> bool
let incremental = ref true
let separate = ref false
+let preamble =
+ L.get_preamble ()
+
let clear () =
incremental := true;
separate := false;
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
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");
projects / helm.git / commitdiff