From: Ferruccio Guidi Date: Tue, 22 Jul 2008 12:43:10 +0000 (+0000) Subject: transcript: now we can generate procedural output X-Git-Tag: make_still_working~4893 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=298868e07163c21863d542136733d24bfbec2482;p=helm.git transcript: now we can generate procedural output CoRN-Procedural: development started: we aim at the procedural reconstruction of CoRN --- diff --git a/helm/software/components/binaries/transcript/CoRN.conf.xml b/helm/software/components/binaries/transcript/CoRN.conf.xml deleted file mode 100644 index e904b4d4e..000000000 --- a/helm/software/components/binaries/transcript/CoRN.conf.xml +++ /dev/null @@ -1,15 +0,0 @@ - - -
- CoRN - CoRN-Decl - cic:/CoRN - cic:/matita/CoRN-Decl - /projects/helm/exportation/CoRN - $(transcript.helm_dir)/matita/contribs/CoRN-Decl - .v - Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con - Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) - nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con -
- diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 66c6c33be..7e561e9b0 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -34,7 +34,6 @@ type script = { } type status = { - helm_dir: string; heading_path: string; heading_lines: int; input_package: string; @@ -43,7 +42,8 @@ type status = { 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; @@ -68,7 +68,7 @@ let load_registry registry = 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 @@ -85,15 +85,21 @@ let set_requires st = {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"; @@ -102,12 +108,17 @@ let make registry = 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 @@ -130,7 +141,7 @@ let set_items st name items = 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 = @@ -157,7 +168,7 @@ let commit 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 @@ -196,7 +207,7 @@ let produce st = | 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 diff --git a/helm/software/components/binaries/transcript/engine.mli b/helm/software/components/binaries/transcript/engine.mli index 8016d71cf..5de8db2e6 100644 --- a/helm/software/components/binaries/transcript/engine.mli +++ b/helm/software/components/binaries/transcript/engine.mli @@ -27,6 +27,6 @@ type status val init: unit -> unit -val make: string -> status +val make: string -> string -> status val produce: status -> unit diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index 1616c18a9..ef2105afb 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -81,15 +81,19 @@ let require value = 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 @@ -98,7 +102,7 @@ let commit och items = | 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 diff --git a/helm/software/components/binaries/transcript/grafite.mli b/helm/software/components/binaries/transcript/grafite.mli index 53aff6990..3bbd35c7b 100644 --- a/helm/software/components/binaries/transcript/grafite.mli +++ b/helm/software/components/binaries/transcript/grafite.mli @@ -23,6 +23,6 @@ * 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 diff --git a/helm/software/components/binaries/transcript/top.ml b/helm/software/components/binaries/transcript/top.ml index 387d47f12..5ef75dab7 100644 --- a/helm/software/components/binaries/transcript/top.ml +++ b/helm/software/components/binaries/transcript/top.ml @@ -24,8 +24,12 @@ *) let main = - let help = "Usage: transcript [ | ]*" in - let process_package package = Engine.produce (Engine.make package) in + let cwd = ref Filename.current_dir_name in + let help = "Usage: transcript [ -C ] [ | ]*" in + let help_C = " set working directory to " 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 diff --git a/helm/software/components/binaries/transcript/transcript.conf.xml b/helm/software/components/binaries/transcript/transcript.conf.xml index d79636f39..ba028de36 100644 --- a/helm/software/components/binaries/transcript/transcript.conf.xml +++ b/helm/software/components/binaries/transcript/transcript.conf.xml @@ -1,8 +1,7 @@
- /home/fguidi/svn/software - matita/matita.ma.templ + matita.ma.templ 14
diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index de7c1036e..f0c8212bc 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -27,6 +27,8 @@ type local = bool type inline_kind = Con | Ind | Var +type output_kind = Declarative | Procedural + type source = string type prefix = string diff --git a/helm/software/matita/contribs/CoRN-Procedural/CoRN.conf.xml b/helm/software/matita/contribs/CoRN-Procedural/CoRN.conf.xml new file mode 100644 index 000000000..03f6ad891 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Procedural/CoRN.conf.xml @@ -0,0 +1,16 @@ + + +
+ CoRN + CoRN + cic:/CoRN + cic:/matita/CoRN-Procedural + /projects/helm/exportation/CoRN + contribs/CoRN-Procedural + .v + procedural + Z_of_nat cic:/Coq/ZArith/BinInt/Z_of_nat.con + Zpos cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) + nat_of_P cic:/Coq/NArith/BinPos/nat_of_P.con +
+ diff --git a/helm/software/matita/contribs/CoRN-Procedural/Makefile b/helm/software/matita/contribs/CoRN-Procedural/Makefile new file mode 100644 index 000000000..fad6ecef6 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Procedural/Makefile @@ -0,0 +1,43 @@ +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 diff --git a/helm/software/matita/contribs/CoRN-Procedural/root b/helm/software/matita/contribs/CoRN-Procedural/root new file mode 100644 index 000000000..48c1ed611 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Procedural/root @@ -0,0 +1 @@ +baseuri=cic:/matita/CoRN-Procedural diff --git a/helm/software/matita/contribs/CoRN-Procedural/transcript.conf.xml b/helm/software/matita/contribs/CoRN-Procedural/transcript.conf.xml new file mode 100644 index 000000000..ba028de36 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Procedural/transcript.conf.xml @@ -0,0 +1,7 @@ + + +
+ matita.ma.templ + 14 +
+ diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index 28fe09079..fef14b2b8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -8,9 +8,8 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass 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)