+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="package">
- <key name="input_name">CoRN</key>
- <key name="output_name">CoRN-Decl</key>
- <key name="input_base_uri">cic:/CoRN</key>
- <key name="output_base_uri">cic:/matita/CoRN-Decl</key>
- <key name="input_path">/projects/helm/exportation/CoRN</key>
- <key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
- <key name="script_type">.v</key>
- <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
- <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
- <key name="coercion">nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con</key>
- </section>
-</helm_registry>
}
type status = {
- helm_dir: string;
heading_path: string;
heading_lines: int;
input_package: string;
output_base_uri: string;
input_path: string;
output_path: string;
- script_ext: string;
+ input_type: string;
+ output_type: T.output_kind;
coercions: (string * string) list;
files: string list;
requires: (string * string) list;
let set_files st =
let eof ich = try Some (input_line ich) with End_of_file -> None in
let trim l = Filename.chop_extension (Str.string_after l 2) in
- let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.script_ext in
+ let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_type in
let ich = Unix.open_process_in cmd in
let rec aux files =
match eof ich with
{st with requires = requires}
let init () =
- let default_registry = "transcript" in
+ let transcript_dir = Filename.dirname Sys.argv.(0) in
+ let default_registry = Filename.concat transcript_dir "transcript" in
load_registry default_registry
-let make registry =
+let make cwd registry =
let id x = x in
let get_coercions = R.get_list (R.pair id id) in
+ let get_output_type key =
+ match R.get_string key with
+ | "procedural" -> T.Procedural
+ | "declarative" -> T.Declarative
+ | _ -> failwith "unknown output type"
+ in
load_registry registry;
let st = {
- helm_dir = R.get_string "transcript.helm_dir";
heading_path = R.get_string "transcript.heading_path";
heading_lines = R.get_int "transcript.heading_lines";
input_package = R.get_string "package.input_name";
output_base_uri = R.get_string "package.output_base_uri";
input_path = R.get_string "package.input_path";
output_path = R.get_string "package.output_path";
- script_ext = R.get_string "package.script_type";
+ input_type = R.get_string "package.input_type";
+ output_type = get_output_type "package.output_type";
coercions = get_coercions "package.coercion";
files = [];
requires = [];
scripts = Array.make default_scripts default_script
} in
+ let st = {st with
+ heading_path = Filename.concat cwd st.heading_path;
+ output_path = Filename.concat cwd st.output_path;
+ } in
prerr_endline "reading file names ...";
let st = set_files st in
let st = set_requires st in
st.scripts.(i) <- {name = name; contents = contents}
let set_heading st name =
- let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in
+ let heading = st.heading_path, st.heading_lines in
set_items st name [T.Heading heading]
let set_baseuri st name =
let cmd = Printf.sprintf "mkdir -p %s" path in
let _ = Sys.command cmd in
let och = open_out name in
- G.commit och script.contents;
+ G.commit st.output_type och script.contents;
close_out och;
st.scripts.(i) <- default_script
| item -> path, Some item
in
Printf.eprintf "processing file name: %s ...\n" name; flush stderr;
- let file = Filename.concat st.input_path (name ^ st.script_ext) in
+ let file = Filename.concat st.input_path (name ^ st.input_type) in
let ich = open_in file in
let lexbuf = Lexing.from_channel ich in
try
val init: unit -> unit
-val make: string -> status
+val make: string -> string -> status
val produce: status -> unit
let coercion value =
command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
-let inline (uri, prefix) =
- command_of_macro (G.Inline (floc, G.Declarative, uri, prefix))
+let inline (kind, uri, prefix) =
+ let kind = match kind with
+ | T.Declarative -> G.Declarative
+ | T.Procedural -> G.Procedural None
+ in
+ command_of_macro (G.Inline (floc, kind, uri, prefix))
let out_alias och name uri =
Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri
-let commit och items =
+let commit kind och items =
let trd (_, _, x) = x in
- let trd_rth (_, _, x, y) = x, y in
+ let trd_rth kind (_, _, x, y) = kind, x, y in
let commit = function
| T.Heading heading -> out_preamble och heading
| T.Line line -> out_line_comment och line
| T.Coercion specs -> out_unexported och "COERCION" (snd specs)
| T.Notation specs -> out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _) -> out_alias och (UriManager.name_of_uri (UriManager.uri_of_string src)) src
- | T.Inline specs -> out_command och (inline (trd_rth specs))
+ | T.Inline specs -> out_command och (inline (trd_rth kind specs))
| T.Section specs -> out_unexported och "UNEXPORTED" (trd specs)
| T.Comment comment -> out_comment och comment
| T.Unexport unexport -> out_unexported och "UNEXPORTED" unexport
* http://cs.unibo.it/helm/.
*)
-val commit: out_channel -> Types.items -> unit
+val commit: Types.output_kind -> out_channel -> Types.items -> unit
val string_of_inline_kind: Types.inline_kind -> string
*)
let main =
- let help = "Usage: transcript [ <package> | <conf_file> ]*" in
- let process_package package = Engine.produce (Engine.make package) in
+ let cwd = ref Filename.current_dir_name in
+ let help = "Usage: transcript [ -C <dir> ] [ <package> | <conf_file> ]*" in
+ let help_C = " set working directory to <dir>" in
+ let set_cwd dir = cwd := dir in
+ let process_package package = Engine.produce (Engine.make !cwd package) in
Engine.init ();
Arg.parse [
+ ("-C", Arg.String set_cwd, help_C)
] process_package help
<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
<section name="transcript">
- <key name="helm_dir">/home/fguidi/svn/software</key>
- <key name="heading_path">matita/matita.ma.templ</key>
+ <key name="heading_path">matita.ma.templ</key>
<key name="heading_lines">14</key>
</section>
</helm_registry>
type inline_kind = Con | Ind | Var
+type output_kind = Declarative | Procedural
+
type source = string
type prefix = string
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="package">
+ <key name="input_name">CoRN</key>
+ <key name="output_name">CoRN</key>
+ <key name="input_base_uri">cic:/CoRN</key>
+ <key name="output_base_uri">cic:/matita/CoRN-Procedural</key>
+ <key name="input_path">/projects/helm/exportation/CoRN</key>
+ <key name="output_path">contribs/CoRN-Procedural</key>
+ <key name="input_type">.v</key>
+ <key name="output_type">procedural</key>
+ <key name="coercion">Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con</key>
+ <key name="coercion">Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2)</key>
+ <key name="coercion">nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con</key>
+ </section>
+</helm_registry>
--- /dev/null
+include ../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+H=@
+
+MATITAOPTIONS=
+
+TRANSCRIPT = $(BIN)../components/binaries/transcript/transcript.opt
+
+LOG = log.txt
+
+MMAS = $(shell find -name "*.mma")
+MAS = $(MMAS:%.mma=%.ma)
+
+$(DIR) all:
+ $(H)$(RM) $(LOG)
+ $(H)$(BIN)matitac $(MATITAOPTIONS) 2>> $(LOG)
+$(DIR).opt opt all.opt:
+ $(H)$(RM) $(LOG)
+ $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
+clean:
+ $(H)$(BIN)matitaclean $(MATITAOPTIONS)
+ $(H)$(RM) $(MAS)
+clean.opt:
+ $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS)
+ $(H)$(RM) $(MAS)
+depend:
+ $$(H)(BIN)matitadep $(MATITAOPTIONS)
+depend.opt:
+ $(H)$(BIN)matitadep.opt $(MATITAOPTIONS)
+
+ifneq ($(strip $(MAS)),)
+clean.ma:
+ $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS)
+ $(H)$(RM) $(MAS)
+else
+clean.ma:
+ $(H)echo no files to clean
+endif
+
+mma: transcript.conf.xml CoRN.conf.xml
+ $(H)$(TRANSCRIPT) -C $(BIN) CoRN
--- /dev/null
+baseuri=cic:/matita/CoRN-Procedural
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="transcript">
+ <key name="heading_path">matita.ma.templ</key>
+ <key name="heading_lines">14</key>
+ </section>
+</helm_registry>
LOG = log.txt
-DEVELS = Legacy-2 Base-2 LambdaDelta-2
-
-MAS = $(shell find $(DEVELS) -mindepth 2 -name "*.ma")
+MMAS = $(shell find -name "*.mma")
+MAS = $(MMAS:%.mma=%.ma)
$(DIR) all:
$(H)$(RM) $(LOG)
projects / helm.git / commitdiff