From: Claudio Sacerdoti Coen Date: Fri, 15 Oct 2010 15:17:14 +0000 (+0000) Subject: transcript removed (currently useless) X-Git-Tag: make_still_working~2779 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=308d9394c3f8c0919427fcc7e00842e105840b4e;p=helm.git transcript removed (currently useless) --- diff --git a/matita/components/binaries/transcript/.depend b/matita/components/binaries/transcript/.depend deleted file mode 100644 index 87d1ed25c..000000000 --- a/matita/components/binaries/transcript/.depend +++ /dev/null @@ -1,24 +0,0 @@ -gallina8Parser.cmi: types.cmo -grafiteParser.cmi: types.cmo -grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: -gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi -gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi -gallina8Lexer.cmo: options.cmo gallina8Parser.cmi -gallina8Lexer.cmx: options.cmx gallina8Parser.cmx -grafiteParser.cmo: types.cmo options.cmo grafiteParser.cmi -grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi -grafiteLexer.cmo: options.cmo grafiteParser.cmi -grafiteLexer.cmx: options.cmx grafiteParser.cmx -grafite.cmo: types.cmo options.cmo grafite.cmi -grafite.cmx: types.cmx options.cmx grafite.cmi -engine.cmo: types.cmo options.cmo grafiteParser.cmi grafiteLexer.cmo \ - grafite.cmi gallina8Parser.cmi gallina8Lexer.cmo engine.cmi -engine.cmx: types.cmx options.cmx grafiteParser.cmx grafiteLexer.cmx \ - grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi -top.cmo: options.cmo engine.cmi -top.cmx: options.cmx engine.cmx diff --git a/matita/components/binaries/transcript/.depend.opt b/matita/components/binaries/transcript/.depend.opt deleted file mode 100644 index f17459162..000000000 --- a/matita/components/binaries/transcript/.depend.opt +++ /dev/null @@ -1,24 +0,0 @@ -gallina8Parser.cmi: types.cmx -grafiteParser.cmi: types.cmx -grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: -gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi -gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi -gallina8Lexer.cmo: options.cmx gallina8Parser.cmi -gallina8Lexer.cmx: options.cmx gallina8Parser.cmx -grafiteParser.cmo: types.cmx options.cmx grafiteParser.cmi -grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi -grafiteLexer.cmo: options.cmx grafiteParser.cmi -grafiteLexer.cmx: options.cmx grafiteParser.cmx -grafite.cmo: types.cmx options.cmx grafite.cmi -grafite.cmx: types.cmx options.cmx grafite.cmi -engine.cmo: types.cmx options.cmx grafiteParser.cmi grafiteLexer.cmx \ - grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi -engine.cmx: types.cmx options.cmx grafiteParser.cmx grafiteLexer.cmx \ - grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi -top.cmo: options.cmx engine.cmi -top.cmx: options.cmx engine.cmx diff --git a/matita/components/binaries/transcript/Makefile b/matita/components/binaries/transcript/Makefile deleted file mode 100644 index b3cc00a0c..000000000 --- a/matita/components/binaries/transcript/Makefile +++ /dev/null @@ -1,108 +0,0 @@ -include ../../../Makefile.defs - -H=@ - -REQUIRES = unix str helm-grafite_parser - -MLS = types.ml options.ml \ - gallina8Parser.ml gallina8Lexer.ml \ - grafiteParser.ml grafiteLexer.ml \ - grafite.ml engine.ml top.ml -MLIS = gallina8Parser.mli grafiteParser.mli grafite.mli engine.mli -CLEAN = gallina8Parser.ml gallina8Parser.mli gallina8Lexer.ml \ - grafiteParser.ml grafiteParser.mli grafiteLexer.ml - -PACKAGES = CoRN - -LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) - -CMOS = $(MLS:%.ml=%.cmo) -CMXS = $(MLS:%.ml=%.cmx) -CMIS = $(MLIS:%.mli=%.cmi) -EXTRAS = - -OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes -OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes -OCAMLDEP = $(OCAMLFIND) ocamldep -OCAMLYACC = ocamlyacc -OCAMLLEX = ocamllex - -all: transcript .depend - @echo -n - -opt: transcript.opt $(EXTRAS) .depend.opt - @echo -n - -transcript: $(CMIS) $(CMOS) $(EXTRAS) - @echo " OCAMLC $(CMOS)" - $(H)$(OCAMLC) -o $@ $(CMOS) - -transcript.opt: $(CMIS) $(CMXS) $(EXTRAS) - @echo " OCAMLOPT $(CMXS)" - $(H)$(OCAMLOPT) -o $@ $(CMXS) - -clean: - $(H)rm -f *.cm[iox] *.a *.o *.output - $(H)rm -f transcript transcript.opt $(CLEAN) - -.depend: $(MLIS) $(MLS) $(EXTRAS) - @echo " OCAMLDEP $(MLIS) $(MLS)" - $(H)$(OCAMLDEP) $(MLIS) $(MLS) > .depend - -.depend.opt: $(MLIS) $(MLS) $(EXTRAS) - @echo " OCAMLDEP -native $(MLIS) $(MLS)" - $(H)$(OCAMLDEP) -native $(MLIS) $(MLS) > .depend.opt - -test: transcript transcript.conf.xml $(PACKAGES:%=%.conf.xml) - @echo " TRANSCRIPT $(PACKAGES)" - $(H)$< $(PACKAGES) - -test.opt: transcript.opt transcript.conf.xml $(PACKAGES:%=%.conf.xml) - @echo " TRANSCRIPT.OPT $(PACKAGES)" - $(H)$< $(PACKAGES) - -export: clean - $(H)rm -f *~ - @echo " TAR transcript" - $(H)cd .. && tar --exclude=transcript/.svn -czf transcript.tgz transcript - -depend: .depend - -depend.opt: .depend.opt - -%.cmi: %.mli $(EXTRAS) - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.cmo %.cmi: %.ml $(EXTRAS) $(LIBRARIES) - @echo " OCAMLC $<" - $(H)$(OCAMLC) -c $< -%.o %.cmx %.cmi: %.ml $(EXTRAS) $(LIBRARIES_OPT) - @echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) -c $< -%.ml %.mli: %.mly $(EXTRAS) - @echo " OCAMLYACC $<" - $(H)$(OCAMLYACC) -v $< -%.ml: %.mll $(EXTRAS) - @echo " OCAMLLEX $<" - $(H)$(OCAMLLEX) $< - -ifeq ($(MAKECMDGOALS),) - include .depend -endif - -ifeq ($(MAKECMDGOALS), all) - include .depend -endif - -ifeq ($(MAKECMDGOALS), opt) - include .depend.opt -endif - -ifeq ($(MAKECMDGOALS), test) - include .depend -endif - -ifeq ($(MAKECMDGOALS), test.opt) - include .depend.opt -endif diff --git a/matita/components/binaries/transcript/engine.ml b/matita/components/binaries/transcript/engine.ml deleted file mode 100644 index 39d4d8ddd..000000000 --- a/matita/components/binaries/transcript/engine.ml +++ /dev/null @@ -1,296 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -module R = Helm_registry -module X = HExtlib -module HG = Http_getter -module GA = GrafiteAst - -module T = Types -module G = Grafite -module O = Options - -type script = { - name : string; - is_ma : bool; - contents: T.items -} - -type status = { - heading_path: string; - heading_lines: int; - input_package: string; - output_package: string; - input_base_uri: string; - output_base_uri: string; - input_path: string; - output_path: string; - input_type: T.input_kind; - output_type: T.output_kind; - input_ext: string; - remove_lines: int; - excludes: string list; - includes: (string * string) list; - iparams: (string * string) list; - coercions: (string * string) list; - files: string list; - requires: (string * string) list; - scripts: script array -} - -let default_script = { - name = ""; is_ma = false; contents = [] -} - -let default_scripts = 2 - -let suffix = ".conf.xml" - -let load_registry registry = - let registry = - if Filename.check_suffix registry suffix then registry - else registry ^ suffix - in - Printf.eprintf "reading configuration %s ...\n" registry; flush stderr; - R.load_from 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.input_ext in - let ich = Unix.open_process_in cmd in - let rec aux files = match eof ich with - | None -> List.rev files - | Some l -> - let l = trim l in - if List.mem l st.excludes then aux files else - if !O.sources = [] || List.mem l !O.sources then aux (l :: files) else - aux files - in - let files = aux [] in - let _ = Unix.close_process_in ich in - {st with files = files} - -let set_requires st = - let map file = (Filename.basename file, file) in - let requires = List.rev_map map st.files in - {st with requires = requires} - -let init () = - let transcript_dir = Filename.dirname Sys.argv.(0) in - let default_registry = Filename.concat transcript_dir "transcript" in - let matita_registry = Filename.concat !O.cwd "matita" in - load_registry default_registry; - load_registry matita_registry; - HG.init () - -let make registry = - let id x = x in - let get_pairs = R.get_list (R.pair id id) in - let get_input_type key1 key2 = - match R.get_string key1, R.get_string key2 with - | "gallina8", _ -> T.Gallina8, ".v", [] - | "grafite", "" -> T.Grafite "", ".ma", [] - | "grafite", s -> T.Grafite s, ".ma", [s] - | s, _ -> failwith ("unknown input type: " ^ s) - in - let get_output_type key = - match R.get_string key with - | "procedural" -> T.Procedural - | "declarative" -> T.Declarative - | s -> failwith ("unknown output type: " ^ s) - in - load_registry registry; - let input_type, input_ext, excludes = - get_input_type "package.input_type" "package.theory_file" - in - let st = { - 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_package = R.get_string "package.output_name"; - input_base_uri = R.get_string "package.input_base_uri"; - 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"; - input_type = input_type; - output_type = get_output_type "package.output_type"; - input_ext = input_ext; - remove_lines = R.get_int "package.heading_lines"; - excludes = excludes; - includes = get_pairs "package.include"; - iparams = get_pairs "package.inline"; - coercions = get_pairs "package.coercion"; - files = []; - requires = []; - scripts = Array.make default_scripts default_script - } in - let st = {st with - heading_path = Filename.concat !O.cwd st.heading_path; - input_path = Filename.concat !O.cwd st.input_path; - output_path = Filename.concat !O.cwd st.output_path - } in - prerr_endline "reading file names ..."; - let st = set_files st in - let st = set_requires st in - st - -let get_index st name = - let rec get_index name i = - if i >= Array.length st.scripts then None else - if st.scripts.(i).name = name then Some i else - get_index name (succ i) - in - match get_index name 0, get_index "" 0 with - | Some i, _ | _, Some i -> i - | None, None -> failwith "not enought script entries" - -let is_ma st name = - let i = get_index st name in - let script = st.scripts.(i) in - st.scripts.(i) <- {script with is_ma = true} - -let set_items st name items = - let i = get_index st name in - let script = st.scripts.(i) in - let contents = List.rev_append (X.list_uniq items) script.contents in - st.scripts.(i) <- {script with name = name; contents = contents} - -let set_heading st name = - let heading = st.heading_path, st.heading_lines in - set_items st name [T.Heading heading] - -let require st name moo inc = - set_items st name [T.Include (moo, inc)] - -let get_coercion st str = - try List.assoc str st.coercions with Not_found -> "" - -let make_path path = - List.fold_left Filename.concat "" (List.rev path) - -let make_prefix path = - String.concat "__" (List.rev path) ^ "__" - -let make_script_name st script name = - let ext = if script.is_ma then ".ma" else ".mma" in - Filename.concat st.output_path (name ^ ext) - -let commit st name = - let i = get_index st name in - let script = st.scripts.(i) in - let path = Filename.concat st.output_path (Filename.dirname name) in - let name = make_script_name st script name in - let cmd = Printf.sprintf "mkdir -p %s" path in - let _ = Sys.command cmd in - let och = open_out name in - G.commit st.output_type och script.contents; - close_out och; - st.scripts.(i) <- default_script - -let produce st = - let init name = set_heading st name in - let partition = function - | T.Coercion (false, _) - | T.Notation (false, _) -> false - | _ -> true - in - let get_items = match st.input_type with - | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token - | T.Grafite _ -> GrafiteParser.items GrafiteLexer.token - in - let produce st name = - let in_base_uri = Filename.concat st.input_base_uri name in - let out_base_uri = Filename.concat st.output_base_uri name in - let filter path = function - | T.Inline (b, k, obj, p, f) -> - let obj, p = - if b then Filename.concat (make_path path) obj, make_prefix path - else obj, p - in - let ext = G.string_of_inline_kind k in - let s = Filename.concat in_base_uri (obj ^ ext) in - path, Some (T.Inline (b, k, s, p, f)) - | T.Include (moo, s) -> - begin - try path, Some (T.Include (moo, List.assoc s st.requires)) - with Not_found -> path, None - end - | T.Coercion (b, obj) -> - let str = get_coercion st obj in - if str <> "" then path, Some (T.Coercion (b, str)) else - let base_uri = if b then out_base_uri else in_base_uri in - let s = obj ^ G.string_of_inline_kind T.Con in - path, Some (T.Coercion (b, Filename.concat base_uri s)) - | T.Section (b, id, _) as item -> - let path = if b then id :: path else List.tl path in - path, Some item - | T.Verbatim s -> - let pat, templ = st.input_base_uri, st.output_base_uri in - path, Some (T.Verbatim (Pcre.replace ~pat ~templ s)) - | item -> path, Some item - in - let set_includes st name = - try require st name true (List.assoc name st.includes) - with Not_found -> () - in - let rec remove_lines ich n = - if n > 0 then let _ = input_line ich in remove_lines ich (pred n) - in - Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path name in - let ich = open_in (file ^ st.input_ext) in - begin try remove_lines ich st.remove_lines with End_of_file -> () end; - let lexbuf = Lexing.from_channel ich in - try - let items = get_items lexbuf in close_in ich; - let _, rev_items = X.list_rev_map_filter_fold filter [] items in - let items = List.rev rev_items in - let local_items, global_items = List.partition partition items in - let comment = T.Line (Printf.sprintf "From %s" name) in - if global_items <> [] then - set_items st st.input_package (comment :: global_items); - init name; - begin match st.input_type with - | T.Grafite "" -> require st name false file - | _ -> require st name false st.input_package - end; - set_includes st name; set_items st name local_items; commit st name - with e -> - prerr_endline (Printexc.to_string e); close_in ich - in - is_ma st st.input_package; - init st.input_package; require st st.input_package false "preamble"; - match st.input_type with - | T.Grafite "" -> - List.iter (produce st) st.files - | T.Grafite s -> - let theory = Filename.concat st.input_path s in - require st st.input_package false theory; - List.iter (produce st) st.files; - commit st st.input_package - | _ -> - List.iter (produce st) st.files; - commit st st.input_package diff --git a/matita/components/binaries/transcript/engine.mli b/matita/components/binaries/transcript/engine.mli deleted file mode 100644 index fb80abbb0..000000000 --- a/matita/components/binaries/transcript/engine.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -type status - -val suffix: string - -val init: unit -> unit - -val make: string -> status - -val produce: status -> unit diff --git a/matita/components/binaries/transcript/gallina8Lexer.mll b/matita/components/binaries/transcript/gallina8Lexer.mll deleted file mode 100644 index 586bab472..000000000 --- a/matita/components/binaries/transcript/gallina8Lexer.mll +++ /dev/null @@ -1,129 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -{ - module O = Options - module P = Gallina8Parser - - let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) - - let check s = - let c = Char.code s.[0] in - if c <= 127 then s else - let escaped = Printf.sprintf "\\%3u\\" c in - begin - if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped; - escaped - end -} - -let QT = '"' -let SPC = [' ' '\t' '\n' '\r']+ -let ALPHA = ['A'-'Z' 'a'-'z' '_'] -let FIG = ['0'-'9'] -let ID = ALPHA (ALPHA | FIG | "\'")* -let RAWID = QT [^ '"']* QT -let NUM = "-"? FIG+ - -rule token = parse - | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } - | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "CoFixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Save" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s } - | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Parameter" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Parameters" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "Scheme" { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s } - | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s } - | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Hints" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s } - | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } - | "Import" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } - | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s } - | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Reset" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Delimit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Bind" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Arguments" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Open" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "V7only" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Reserved" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Grammar" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Syntax" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Add" SPC "Morphism" - { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s } - | "Add" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } - | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s } - | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s } - | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s } - | "with" { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s } - | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } - | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s } - | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s } - | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s } - | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s } - | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s } - | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s } - | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s } - | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s } - | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s } - | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s } - | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s } - | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s } - | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s } - | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s } - | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s } - | _ - { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s } - | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/matita/components/binaries/transcript/gallina8Parser.mly b/matita/components/binaries/transcript/gallina8Parser.mly deleted file mode 100644 index baacd3f40..000000000 --- a/matita/components/binaries/transcript/gallina8Parser.mly +++ /dev/null @@ -1,611 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -%{ - module T = Types - module O = Options - - let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s) - - let trim = HExtlib.trim_blanks - - let hd = List.hd - - let cat x = String.concat " " x - - let mk_vars local idents = - let kind = if local then T.Var else T.Con in - let map ident = T.Inline (local, kind, trim ident, "", None) in - List.map map idents - - let strip2 s = - String.sub s 1 (String.length s - 2) - - let strip1 s = - String.sub s 1 (String.length s - 1) - - let coercion str = - [T.Coercion (false, str); T.Coercion (true, str)] - - let notation str = - [T.Notation (false, str); T.Notation (true, str)] - - let mk_flavour str = - match trim str with - | "Remark" -> Some `Remark - | "Lemma" -> Some `Lemma - | "Theorem" -> Some `Theorem - | "Definition" -> Some `Definition - | "Fixpoint" -> Some `Definition - | "CoFixpoint" -> Some `Definition - | "Let" -> Some `Definition - | "Scheme" -> Some `Theorem - | _ -> assert false - - let mk_morphism ext = - let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in - List.rev_map generate ["2"; "1"] - -%} - %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM - %token WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR - %token EOF - - %start items - %type items -%% -/* SPACED TOKENS ************************************************************/ - - ident: xident spcs { $1 ^ $2 }; - fs: FS spcs { $1 ^ $2 }; - mor: MOR spcs { $1 ^ $2 }; - th: TH spcs { $1 ^ $2 }; - xlet: LET spcs { $1 ^ $2 }; - proof: PROOF spcs { $1 ^ $2 }; - qed: QED spcs { $1 ^ $2 }; - gen: GEN spcs { $1 ^ $2 }; - sec: SEC spcs { $1 ^ $2 }; - xend: END spcs { $1 ^ $2 }; - unx: UNX spcs { $1 ^ $2 }; - def: DEF spcs { $1 ^ $2 }; - op: OP spcs { $1 ^ $2 }; - abbr: ABBR spcs { $1 ^ $2 }; - var: VAR spcs { $1 ^ $2 }; - ax: AX spcs { $1 ^ $2 }; - req: REQ spcs { $1 ^ $2 }; - load: LOAD spcs { $1 ^ $2 }; - xp: XP spcs { $1 ^ $2 }; - ind: IND spcs { $1 ^ $2 }; - set: SET spcs { $1 ^ $2 }; - notation: NOT spcs { $1 ^ $2 }; - cn: CN spcs { $1 ^ $2 }; - str: STR spcs { $1 ^ $2 }; - id: ID spcs { $1 ^ $2 }; - coerc: COERC spcs { $1 ^ $2 }; - cm: CM spcs { $1 ^ $2 } | { "" } - wh: WITH spcs { $1 ^ $2 }; - -/* SPACES *******************************************************************/ - - comment: - | OQ verbatims CQ { $1 ^ $2 ^ $3 } - ; - spc: - | SPC { $1 } - | comment { $1 } - ; - spcs: - | { "" } - | spc spcs { $1 ^ $2 } - ; - rspcs: - | { "" } - | SPC rspcs { $1 ^ $2 } - ; - -/* IDENTIFIERS **************************************************************/ - - outer_keyword: - | LET { $1 } - | TH { $1 } - | VAR { $1 } - | AX { $1 } - | IND { $1 } - | GEN { $1 } - | SEC { $1 } - | END { $1 } - | UNX { $1 } - | REQ { $1 } - | LOAD { $1 } - | SET { $1 } - | NOT { $1 } - | ID { $1 } - | COERC { $1 } - | MOR { $1 } - ; - inner_keyword: - | XP { $1 } - ; - xident: - | IDENT { $1 } - | outer_keyword { $1 } - | WITH { $1 } - ; - qid: - | xident { [$1] } - | qid AC { strip1 $2 :: $1 } - ; - idents: - | ident { [$1] } - | ident cm idents { $1 :: $3 } - ; - -/* PLAIN SKIP ***************************************************************/ - - plain_skip: - | IDENT { $1 } - | inner_keyword { $1 } - | STR { $1 } - | INT { $1 } - | COE { $1 } - | OC { $1 } - | CC { $1 } - | SC { $1 } - | CN { $1 } - | CM { $1 } - | EXTRA { $1 } - ; - inner_skip: - | plain_skip { $1 } - | outer_keyword { $1 } - | AC { $1 } - | DEF { $1 } - | PROOF { $1 } - | QED { $1 } - | FS { $1 } - | WITH { $1 } - ; - -/* LEFT SKIP ****************************************************************/ - - rlskip: - | plain_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - | IN { $1, [] } - | CP { $1, [] } - ; - xlskip: - | outer_keyword { $1, [] } - | AC { $1, [] } - | WITH { $1, [] } - | rlskip { $1 } - ; - xlskips: - | xlskip spcs { fst $1 ^ $2, snd $1 } - | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - lskips: - | rlskip spcs { fst $1 ^ $2, snd $1 } - | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - opt_lskips: - | lskips { $1 } - | { "", [] } - ; - -/* GENERAL SKIP *************************************************************/ - - rskip: - | rlskip { $1 } - | DEF { $1, [] } - ; - xskip: - | outer_keyword { $1, [] } - | AC { $1, [] } - | WITH { $1, [] } - | rskip { $1 } - ; - xskips: - | xskip spcs { fst $1 ^ $2, snd $1 } - | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - skips: - | rskip spcs { fst $1 ^ $2, snd $1 } - | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* ABBREVIATION SKIP ********************************************************/ - - li_skip: - | inner_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - ; - li_skips: - | li_skip spcs { fst $1 ^ $2, snd $1 } - | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* PARENTETIC SKIP **********************************************************/ - - ocp_skip: - | inner_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - | IN { $1, [] } - ; - ocp_skips: - | ocp_skip spcs { fst $1 ^ $2, snd $1 } - | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* VERBATIM SKIP ************************************************************/ - - verbatim: - | comment { $1 } - | inner_skip { $1 } - | ABBR { $1 } - | IN { $1 } - | OP { $1 } - | CP { $1 } - | SPC { $1 } - ; - verbatims: - | { "" } - | verbatim verbatims { $1 ^ $2 } - ; - -/* PROOF STEPS **************************************************************/ - - step: - | macro_step { $1 } - | skips FS { snd $1 } - ; - steps: - | step spcs { $1 } - | step spcs steps { $1 @ $3 } - ; - just: - | steps qed { $1 } - | proof fs steps qed { $3 } - | proof skips { snd $2 } - | proof wh skips fs steps qed { snd $3 @ $5 } - ; - macro_step: - | th ident opt_lskips def xskips FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident lskips fs just FS - { out "TH" $2; - $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | gen ident def xskips FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | mor ident cn ident fs just FS - { out "MOR" $4; $6 @ mk_morphism (trim $4) } - | xlet ident opt_lskips def xskips FS - { out "TH" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident lskips fs just FS - { out "TH" $2; - $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | var idents cn xskips FS - { out "VAR" (cat $2); mk_vars true $2 } - | ax idents cn xskips FS - { out "AX" (cat $2); mk_vars false $2 } - | ind ident skips FS - { out "IND" $2; - T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 - } - | sec ident FS - { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } - | xend ident FS - { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } - | unx xskips FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | req xp ident FS - { out "REQ" $3; [T.Include (true, trim $3)] } - | req ident FS - { out "REQ" $2; [T.Include (true, trim $2)] } - | load str FS - { out "REQ" $2; [T.Include (true, strip2 (trim $2))] } - | coerc qid spcs skips FS - { out "COERCE" (hd $2); coercion (hd $2) } - | id coerc qid spcs skips FS - { out "COERCE" (hd $3); coercion (hd $3) } - | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | var idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - | ax idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - ; - -/* VERNACULAR ITEMS *********************************************************/ - - item: - | OQ verbatims CQ { [T.Comment $2] } - | macro_step { $1 } - | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) } - | error { out "ERROR" "item"; failwith "item" } - ; - items: - | rspcs EOF { [] } - | rspcs item items { $2 @ $3 } - ; - - -/* - oc: OC spcs { $1 ^ $2 }; - coe: COE spcs { $1 ^ $2 }; - sc: SC spcs { $1 ^ $2 }; - - cnot: - | EXTRA { $1 } - | INT { $1 } - ; - cnots: - | cnot spcs { $1 ^ $2 } - | cnot spcs cnots { $1 ^ $2 ^ $3 } - ; - - xstrict: - | AC { $1 } - | INT { $1 } - | EXTRA { $1 } - | CN { $1 } - | SC { $1 } - | OC { $1 } - | CC { $1 } - | COE { $1 } - | STR { $1 } - | abbr extends0 IN { $1 ^ $2 ^ $3 } - | op extends1 CP { $1 ^ $2 ^ $3 } - ; - strict: - | xstrict { $1 } - | IDENT { $1 } - | SET { $1 } - | NOT { $1 } - ; - restrict: - | strict { $1 } - | IN { $1 } - | CP { $1 } - ; - xre: - | xstrict { $1 } - | IN { $1 } - | CP { $1 } - ; - restricts: - | restrict spcs { $1 ^ $2 } - | restrict spcs restricts { $1 ^ $2 ^ $3 } - ; - xres: - | xre spcs { $1 ^ $2 } - | xre spcs restricts { $1 ^ $2 ^ $3 } - ; - extend0: - | strict { $1 } - | DEF { $1 } - ; - extends0: - | extend0 spcs { $1 ^ $2 } - | extend0 spcs extends0 { $1 ^ $2 ^ $3 } - ; - extend1: - | strict { $1 } - | DEF { $1 } - | IN { $1 } - ; - extends1: - | extend1 spcs { $1 ^ $2 } - | extend1 spcs extends1 { $1 ^ $2 ^ $3 } - ; - unexport_ff: - | IDENT { $1 } - | AC { $1 } - | STR { $1 } - | OP { $1 } - | ABBR { $1 } - | IN { $1 } - | CP { $1 } - | SET { $1 } - ; - unexport_rr: - | unexport_ff { $1 } - | INT { $1 } - | EXTRA { $1 } - | CN { $1 } - | COE { $1 } - | DEF { $1 } - ; - unexport_r: - | unexport_rr { $1, [] } - | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 } - | oc unexport_ff CC { $1, [] } - ; - unexports_r: - | unexport_r spcs { fst $1 ^ $2, snd $1 } - | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - field: - | ident cn unexports_r - { $1 ^ $2 ^ fst $3, snd $3 } - | ident def unexports_r - { $1 ^ $2 ^ fst $3, snd $3 } - | ident coe unexports_r - { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) } - ; - fields: - | field { $1 } - | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - | cnots { $1, [] } - | error { out "ERROR" "fields"; failwith "fields" } - ; - unexport: - | unexport_r { $1 } - | SC { $1, [] } - | CC { $1, [] } - | IP { $1, [] } - | LET { $1, [] } - | VAR { $1, [] } - - ; - unexports: - | unexport spcs { fst $1 ^ $2, snd $1 } - | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - verbatim: - | unexport_rr { $1 } - | reserved_ident { $1 } - | comment { $1 } - | OC { $1 } - | CC { $1 } - | SC { $1 } - | XP { $1 } - | IP { $1 } - | FS { $1 } - | SPC { $1 } - ; - verbatims: - | { "" } - | verbatim verbatims { $1 ^ $2 } - ; - step: - | macro_step { $1 } - | restricts FS { [] } - ; - steps: - | step spcs { [] } - | step spcs steps { $1 @ $3 } - ; - - macro_step: - | th ident restricts fs proof FS steps qed FS - { out "TH" $2; - $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts fs proof restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts fs steps qed FS - { out "TH" $2; - $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | gen ident def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs proof FS steps qed FS - { out "LET" $2; - $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs proof restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs steps qed FS - { out "LET" $2; - $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts def restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident def restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | var idents xres FS - { out "VAR" (cat $2); mk_vars true $2 } - | ax idents xres FS - { out "AX" (cat $2); mk_vars false $2 } - | ind ident unexports FS - { out "IND" $2; - T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 - } - | sec ident FS - { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } - | xend ident FS - { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } - | unx unexports FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | req xp ident FS - { out "REQ" $3; [T.Include (trim $3)] } - | req ip ident FS - { out "REQ" $3; [T.Include (trim $3)] } - | req ident FS - { out "REQ" $2; [T.Include (trim $2)] } - | load str FS - { out "REQ" $2; [T.Include (strip2 (trim $2))] } - | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); coercion (hd $2) } - | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); coercion (hd $3) } - | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | var idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - | ax idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - ; - item: - | OQ verbatims CQ { [T.Comment $2] } - | macro_step { $1 } - | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) } - | error { out "ERROR" "item"; failwith "item" } - ; - items: - | rspcs EOF { [] } - | rspcs item items { $2 @ $3 } - ; -*/ diff --git a/matita/components/binaries/transcript/grafite.ml b/matita/components/binaries/transcript/grafite.ml deleted file mode 100644 index 8d4e71174..000000000 --- a/matita/components/binaries/transcript/grafite.ml +++ /dev/null @@ -1,113 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -module T = Types -module O = Options - -module UM = UriManager -module NP = NotationPp -module GP = GrafiteAstPp -module G = GrafiteAst -module H = HExtlib - -let floc = H.dummy_floc - -let out_verbatim och s = - Printf.fprintf och "%s" s - -let out_comment och s = - let s = if s <> "" && s.[0] = '*' then "#" ^ s else s in - Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" - -let out_unexported och head s = - let s = Printf.sprintf " %s\n%s\n" head s in - out_comment och s - -let out_line_comment och s = - let l = 70 - String.length s in - let l = if l < 0 then 0 else l in - let s = Printf.sprintf " %s %s" s (String.make l '*') in - out_comment och s - -let out_preamble och (path, lines) = - let ich = open_in path in - let rec print i = - if i > 0 then - let s = input_line ich in - begin Printf.fprintf och "%s\n" s; print (pred i) end - in - print lines; - out_line_comment och "This file was automatically generated: do not edit" - -let out_command och cmd = - let term_pp = NP.pp_term in - let lazy_term_pp = NP.pp_term in - let obj_pp = NP.pp_obj NP.pp_term in - let s = GP.pp_statement cmd ~map_unicode_to_tex:false in - Printf.fprintf och "%s\n\n" s - -let command_of_obj obj = - G.Executable (floc, G.Command (floc, obj)) - -let require moo value = - command_of_obj (G.Include (floc, value ^ ".ma")) - -let out_alias och name uri = - Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri - -let check och src = - if Http_getter.exists ~local:false src then () else - let msg = "UNAVAILABLE OBJECT: " ^ src in - out_line_comment och msg; - prerr_endline msg - -let commit kind och items = - let trd (_, _, x) = x in - let commit = function - | T.Heading heading -> out_preamble och heading - | T.Line line -> - if !O.comments then out_line_comment och line - | T.Include (moo, script) -> out_command och (require moo script) - | T.Coercion specs -> - if !O.comments then out_unexported och "COERCION" (snd specs) - | T.Notation specs -> - if !O.comments then out_unexported och "NOTATION" (snd specs) (**) - | T.Inline (_, T.Var, src, _, _) -> - if !O.comments then out_unexported och "UNEXPORTED" src - | T.Section specs -> - if !O.comments then out_unexported och "UNEXPORTED" (trd specs) - | T.Comment comment -> - if !O.comments then out_comment och comment - | T.Unexport unexport -> - if !O.comments then out_unexported och "UNEXPORTED" unexport - | T.Verbatim verbatim -> out_verbatim och verbatim - | T.Discard _ -> () - in - List.iter commit (List.rev items) - -let string_of_inline_kind = function - | T.Con -> ".con" - | T.Var -> ".var" - | T.Ind -> ".ind" diff --git a/matita/components/binaries/transcript/grafite.mli b/matita/components/binaries/transcript/grafite.mli deleted file mode 100644 index 3bbd35c7b..000000000 --- a/matita/components/binaries/transcript/grafite.mli +++ /dev/null @@ -1,28 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -val commit: Types.output_kind -> out_channel -> Types.items -> unit - -val string_of_inline_kind: Types.inline_kind -> string diff --git a/matita/components/binaries/transcript/grafiteLexer.mll b/matita/components/binaries/transcript/grafiteLexer.mll deleted file mode 100644 index ac3055bc5..000000000 --- a/matita/components/binaries/transcript/grafiteLexer.mll +++ /dev/null @@ -1,77 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -{ - module O = Options - module P = GrafiteParser - - let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) -} - -let SPC = [' ' '\t' '\n' '\r']+ -let ALPHA = ['A'-'Z' 'a'-'z'] -let FIG = ['0'-'9'] -let DECOR = "?" | "'" | "`" -let IDENT = ALPHA (ALPHA | '_' | FIG )* DECOR* - -rule token = parse - | "(*" { let s = Lexing.lexeme lexbuf in out "OK" s; P.OK s } - | "*)" { let s = Lexing.lexeme lexbuf in out "CK" s; P.CK s } - | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } - | "axiom" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } -(* - | "fact" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } -*) - | "remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "variant" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "inductive" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "coinductive" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "record" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "let rec" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "let corec" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "notation" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "interpretation" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "alias" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "coercion" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "prefer coercion" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "default" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "include" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "inline" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "pump" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "elim" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | "apply" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | "intros" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | "assume" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | "the" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | "rewrite" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } - | IDENT { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } - | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | "." { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | _ { let s = Lexing.lexeme lexbuf in out "RAW" s; P.RAW s } - | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/matita/components/binaries/transcript/grafiteParser.mly b/matita/components/binaries/transcript/grafiteParser.mly deleted file mode 100644 index 2f4d1e264..000000000 --- a/matita/components/binaries/transcript/grafiteParser.mly +++ /dev/null @@ -1,140 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -%{ - module T = Types - module O = Options - - let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s) - - let mk_flavour str = - match str with - | "record" -> T.Ind, None - | "inductive" -> T.Ind, None - | "coinductive" -> T.Ind, None - | "axiom" -> T.Con, None - | "definition" -> T.Con, Some `Definition - | "let rec" -> T.Con, Some `Definition - | "let corec" -> T.Con, Some `Definition - | "theorem" -> T.Con, Some `Theorem - | "lemma" -> T.Con, Some `Lemma - | "fact" -> T.Con, Some `Fact - | "remark" -> T.Con, Some `Remark - | "variant" -> T.Con, Some `Variant - | _ -> assert false - -%} - %token SPC OK CK FS QED TH UNX PS ID RAW - %token EOF - - %start items - %type items -%% - -/* LINES ITEMS ***************************************************************/ - - extra: - | ID { $1 } - | QED { $1 } - | RAW { $1 } - ; - text: - | extra { $1 } - | TH { $1 } - | UNX { $1 } - | PS { $1 } - | comment { $1 } - ; - texts: - | { "" } - | text texts { $1 ^ $2 } - ; - line: - | texts FS { $1 ^ $2 } - ; - drop: - | extra line { $1 ^ $2 } - ; - drops: - | { "" } - | drop drops { $1 ^ $2 } - ; - -/* SPACE ITEMS *************************************************************/ - - verbatim: - | text { $1 } - | FS { $1 } - ; - verbatims: - | { "" } - | verbatim verbatims { $1 ^ $2 } - ; - comment: - | SPC { $1 } - | OK verbatims CK { $1 ^ $2 ^ $3 } - ; - -/* STEPS ********************************************************************/ - - step: - | comment { $1 } - | FS { $1 } - | TH { $1 } - | UNX { $1 } - | PS { $1 } - | ID { $1 } - | RAW { $1 } - ; - steps: - | QED FS { $1 ^ $2 } - | step steps { $1 ^ $2 } - ; - -/* ITEMS ********************************************************************/ - - id: - | ID { $1 } - | TH { $1 } - | UNX { $1 } - | PS { $1 } - ; - - item: - | comment - { out "OK" $1; [T.Verbatim $1] } - | TH SPC id line drops - { out "TH" $3; - let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b)] - } - | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } - | PS steps { out "PS" $2; [] } - | QED FS { [] } - ; - items: - | EOF { [] } - | item items { $1 @ $2 } -/* | error { out "ERROR" ""; failwith ("item id " ^ "") } */ - ; diff --git a/matita/components/binaries/transcript/options.ml b/matita/components/binaries/transcript/options.ml deleted file mode 100644 index eab659faf..000000000 --- a/matita/components/binaries/transcript/options.ml +++ /dev/null @@ -1,38 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -let cwd = ref Filename.current_dir_name - -let verbose_parser = ref false - -let verbose_lexer = ref false - -let verbose_escape = ref false - -let comments = ref true - -let getter = ref false - -let sources = ref ([]: string list) diff --git a/matita/components/binaries/transcript/top.ml b/matita/components/binaries/transcript/top.ml deleted file mode 100644 index b66146b2e..000000000 --- a/matita/components/binaries/transcript/top.ml +++ /dev/null @@ -1,48 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -let main = - let help = "Usage: transcript [ -glmpx | -C ] [ | ]*" in - let help_C = " set working directory to " in - let help_g = " check for non existing objects" in - let help_l = " verbose lexing" in - let help_m = " minimal output generation" in - let help_p = " verbose parsing" in - let help_x = " verbose character escaping" in - let set_cwd dir = Options.cwd := dir; Engine.init () in - let process_file file = - if Sys.file_exists file || Sys.file_exists (file ^ Engine.suffix) then - begin Engine.produce (Engine.make file); Options.sources := [] end - else - Options.sources := file :: !Options.sources - in - Arg.parse [ - ("-C", Arg.String set_cwd, help_C); - ("-g", Arg.Set Options.getter, help_g); - ("-l", Arg.Set Options.verbose_lexer, help_l); - ("-m", Arg.Clear Options.comments, help_m); - ("-p", Arg.Set Options.verbose_parser, help_p); - ("-x", Arg.Set Options.verbose_escape, help_x); - ] process_file help diff --git a/matita/components/binaries/transcript/transcript.conf.xml b/matita/components/binaries/transcript/transcript.conf.xml deleted file mode 100644 index ba028de36..000000000 --- a/matita/components/binaries/transcript/transcript.conf.xml +++ /dev/null @@ -1,7 +0,0 @@ - - -
- matita.ma.templ - 14 -
- diff --git a/matita/components/binaries/transcript/types.ml b/matita/components/binaries/transcript/types.ml deleted file mode 100644 index ba1619641..000000000 --- a/matita/components/binaries/transcript/types.ml +++ /dev/null @@ -1,54 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -type local = bool - -type inline_kind = Con | Ind | Var - -type input_kind = Gallina8 | Grafite of string - -type output_kind = Declarative | Procedural - -type source = string - -type prefix = string - -type flavour = Cic.object_flavour option - -(* type params = GrafiteAst.inline_param list *) - -type item = Heading of (string * int) - | Line of string - | Comment of string - | Unexport of string - | Include of (bool * string) - | Coercion of (local * string) - | Notation of (local * string) - | Section of (local * string * string) - | Inline of (local * inline_kind * source * prefix * flavour) - | Verbatim of string - | Discard of string - -type items = item list