From: Ferruccio Guidi Date: Wed, 15 Nov 2006 14:10:33 +0000 (+0000) Subject: transcript: very alpha version. X-Git-Tag: 0.4.95@7852~807 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0dfad591e92a2c1174313ed7be80da0084b618b3;p=helm.git transcript: very alpha version. parser for Coq V8 works fine on CoRN contribution scripts. --- diff --git a/components/binaries/Makefile b/components/binaries/Makefile index 9dd295fb4..db074309d 100644 --- a/components/binaries/Makefile +++ b/components/binaries/Makefile @@ -3,7 +3,7 @@ H=@ #CSC: saturate is broken after the huge refactoring of auto/paramodulation #CSC: by Andrea #BINARIES=extractor table_creator utilities saturate -BINARIES=extractor table_creator utilities +BINARIES=extractor table_creator utilities transcript all: $(BINARIES:%=rec@all@%) opt: $(BINARIES:%=rec@opt@%) diff --git a/components/binaries/transcript/.depend b/components/binaries/transcript/.depend new file mode 100644 index 000000000..5e737a14a --- /dev/null +++ b/components/binaries/transcript/.depend @@ -0,0 +1,12 @@ +v8Parser.cmi: types.cmo +grafite.cmi: types.cmo +v8Parser.cmo: types.cmo v8Parser.cmi +v8Parser.cmx: types.cmx v8Parser.cmi +v8Lexer.cmo: v8Parser.cmi +v8Lexer.cmx: v8Parser.cmx +grafite.cmo: types.cmo grafite.cmi +grafite.cmx: types.cmx grafite.cmi +engine.cmo: v8Parser.cmi v8Lexer.cmo types.cmo grafite.cmi engine.cmi +engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx grafite.cmx engine.cmi +top.cmo: engine.cmi +top.cmx: engine.cmx diff --git a/components/binaries/transcript/CoRN-2.conf.xml b/components/binaries/transcript/CoRN-2.conf.xml new file mode 100644 index 000000000..6e3958459 --- /dev/null +++ b/components/binaries/transcript/CoRN-2.conf.xml @@ -0,0 +1,10 @@ + + +
+ CoRN + cic:/matita/CoRN-Decl + /home/fguidi/CoRN-2 + $(transcript.helm_dir)/matita/contribs/CoRN-Decl + .v +
+ diff --git a/components/binaries/transcript/CoRN.conf.xml b/components/binaries/transcript/CoRN.conf.xml new file mode 100644 index 000000000..e952b23e4 --- /dev/null +++ b/components/binaries/transcript/CoRN.conf.xml @@ -0,0 +1,10 @@ + + +
+ CoRN + cic:/matita/CoRN-Decl + /projects/helm/exportation/CoRN + $(transcript.helm_dir)/matita/contribs/CoRN-Decl + .v +
+ diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile new file mode 100644 index 000000000..87f9ea0a3 --- /dev/null +++ b/components/binaries/transcript/Makefile @@ -0,0 +1,82 @@ +H=@ + +REQUIRES = unix str helm-grafite_parser + +MLS = types.ml v8Parser.ml v8Lexer.ml grafite.ml engine.ml top.ml +MLIS = v8Parser.mli grafite.mli engine.mli +CLEAN = v8Parser.ml v8Parser.mli v8Lexer.ml + +PACKAGES = CoRN + +CMOS = $(MLS:%.ml=%.cmo) +CMXS = $(MLS:%.ml=%.cmx) +CMIS = $(MLIS:%.mli=%.cmi) +EXTRAS = + +OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg +OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg +OCAMLDEP = $(OCAMLFIND) ocamldep +OCAMLYACC = ocamlyacc +OCAMLLEX = ocamllex + +all: transcript .depend + @echo -n +opt: transcript.opt $(EXTRAS) .depend + #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 + +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 + +%.cmi: %.mli $(EXTRAS) + @echo " OCAMLC $<" + $(H)$(OCAMLC) -c $< +%.cmo %.cmi: %.ml $(EXTRAS) + @echo " OCAMLC $<" + $(H)$(OCAMLC) -c $< +%.cmx: %.ml $(EXTRAS) + @echo " OCAMLOPT $<" + $(H)$(OCAMLOPT) -c $< +%.ml %.mli: %.mly $(EXTRAS) + @echo " OCAMLYACC $<" + $(H)$(OCAMLYACC) -v $< +%.ml: %.mll $(EXTRAS) + @echo " OCAMLLEX $<" + $(H)$(OCAMLLEX) $< + +include ../../../Makefile.defs + +ifeq ($(MAKECMDGOALS), all) + include .depend +endif + +ifeq ($(MAKECMDGOALS),) + include .depend +endif diff --git a/components/binaries/transcript/engine.ml b/components/binaries/transcript/engine.ml new file mode 100644 index 000000000..92c3c73b4 --- /dev/null +++ b/components/binaries/transcript/engine.ml @@ -0,0 +1,155 @@ +(* 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 + +type script = { + name: string; + contents: Types.items +} + +type status = { + helm_dir: string; + heading_path: string; + heading_lines: int; + package: string; + base_uri: string; + input_path: string; + output_path: string; + script_ext: string; + files: string list; + requires: (string * string) list; + scripts: script array +} + +let default_script = { + name = ""; contents = [] +} + +let default_scripts = 2 + +let load_registry registry = + let suffix = ".conf.xml" in + 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.script_ext in + let ich = Unix.open_process_in cmd in + let rec aux files = + match eof ich with + | None -> List.rev files + | Some l -> aux (trim l :: 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 default_registry = "transcript" in + load_registry default_registry + +let make registry = + 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"; + package = R.get_string "package.name"; + base_uri = R.get_string "package.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"; + files = []; + requires = []; + scripts = Array.make default_scripts default_script + } 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 set_items st name items = + let i = get_index st name in + let script = st.scripts.(i) in + let contents = List.rev_append items script.contents 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 + set_items st name [Types.Heading heading] + +let set_baseuri st name = + let baseuri = Filename.concat st.base_uri name in + set_items st name [Types.BaseUri baseuri] + +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 = Filename.concat st.output_path (name ^ ".ma") in + let cmd = Printf.sprintf "mkdir -p %s" path in + let _ = Sys.command cmd in + let och = open_out name in + Grafite.commit och script.contents; + close_out och; + st.scripts.(i) <- default_script + +let produce st = + let init name = set_heading st name; set_baseuri st name in + let produce st name = + Printf.eprintf "processing file name: %s ...\n" name; flush stderr; + let file = Filename.concat st.input_path (name ^ st.script_ext) in + let ich = open_in file in + let lexbuf = Lexing.from_channel ich in + try + let items = V8Parser.items V8Lexer.token lexbuf in + close_in ich; + init name; set_items st name items; commit st name + with e -> + prerr_endline (Printexc.to_string e); close_in ich + in + init st.package; List.iter (produce st) st.files; commit st st.package diff --git a/components/binaries/transcript/engine.mli b/components/binaries/transcript/engine.mli new file mode 100644 index 000000000..8016d71cf --- /dev/null +++ b/components/binaries/transcript/engine.mli @@ -0,0 +1,32 @@ +(* 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 init: unit -> unit + +val make: string -> status + +val produce: status -> unit diff --git a/components/binaries/transcript/grafite.ml b/components/binaries/transcript/grafite.ml new file mode 100644 index 000000000..9900b8bc8 --- /dev/null +++ b/components/binaries/transcript/grafite.ml @@ -0,0 +1,84 @@ +(* 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 NP = CicNotationPp +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 = + Printf.fprintf och "%s%s%s\n\n" "(*" s "*)" + +let out_line_comment och s = + let l = 70 - String.length s in + Printf.fprintf och "%s %s %s%s\n\n" "(*" s (String.make l '*') "*)" + +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 in + let s = GP.pp_statement ~term_pp ~lazy_term_pp ~obj_pp cmd in + Printf.fprintf och "%s\n\n" s + +let command_of_obj obj = + G.Executable (floc, G.Command (floc, obj)) + +let set key value = + command_of_obj (G.Set (floc, key, value)) + +let require value = + command_of_obj (G.Include (floc, value ^ ".ma")) + +let commit och items = + let commit = function + | T.Heading heading -> out_preamble och heading + | T.BaseUri baseuri -> out_command och (set "baseuri" baseuri) + | T.Include inc -> () (* *) + | T.Coercion coercion -> () (* *) + | T.Notation notation -> () (* *) + | T.Inline iniline -> () (* *) + | T.Comment comment -> () (* out_comment och comment *) + | T.Unexport unexport -> () (* *) + | T.Verbatim verbatim -> out_verbatim och verbatim + | T.Discard _ -> () + in + List.iter commit (List.rev items) diff --git a/components/binaries/transcript/grafite.mli b/components/binaries/transcript/grafite.mli new file mode 100644 index 000000000..b0b5fcafc --- /dev/null +++ b/components/binaries/transcript/grafite.mli @@ -0,0 +1,26 @@ +(* 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: out_channel -> Types.items -> unit diff --git a/components/binaries/transcript/top.ml b/components/binaries/transcript/top.ml new file mode 100644 index 000000000..387d47f12 --- /dev/null +++ b/components/binaries/transcript/top.ml @@ -0,0 +1,31 @@ +(* 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 [ | ]*" in + let process_package package = Engine.produce (Engine.make package) in + Engine.init (); + Arg.parse [ + ] process_package help diff --git a/components/binaries/transcript/transcript.conf.xml b/components/binaries/transcript/transcript.conf.xml new file mode 100644 index 000000000..d79636f39 --- /dev/null +++ b/components/binaries/transcript/transcript.conf.xml @@ -0,0 +1,8 @@ + + +
+ /home/fguidi/svn/software + matita/matita.ma.templ + 14 +
+ diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml new file mode 100644 index 000000000..d7770ade7 --- /dev/null +++ b/components/binaries/transcript/types.ml @@ -0,0 +1,39 @@ +(* 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 inline_kind = Con | Ind | Var + +type item = Heading of (string * int) + | Comment of string + | Unexport of string + | BaseUri of string + | Include of string + | Coercion of string + | Notation of string + | Inline of (inline_kind * string) + | Verbatim of string + | Discard of string + +type items = item list diff --git a/components/binaries/transcript/v8Lexer.mll b/components/binaries/transcript/v8Lexer.mll new file mode 100644 index 000000000..cddb728bd --- /dev/null +++ b/components/binaries/transcript/v8Lexer.mll @@ -0,0 +1,71 @@ +{ + module P = V8Parser + + let out t s = () (* prerr_endline (t ^ " " ^ s) *) +} + +let QT = '"' +let SPC = [' ' '\t' '\n']+ +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 "TH" s; P.TH 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 } + | "Qed" { 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 "VAR" s; P.VAR s } + | "Inductive" { 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 } + | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "End" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Hint" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Unset" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Print" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Opaque" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Transparent" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Ltac" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Tactic" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "Declare" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC 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 "IP" s; P.IP 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 } + | "Implicit" { 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 } + | "Infix" { 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 "LET" s; P.LET s } + | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN 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 } + | "." 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 "SPEC" s; P.EXTRA s } + | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/components/binaries/transcript/v8Parser.mly b/components/binaries/transcript/v8Parser.mly new file mode 100644 index 000000000..9529bfb62 --- /dev/null +++ b/components/binaries/transcript/v8Parser.mly @@ -0,0 +1,290 @@ +/* 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 + + let out t s = () (* prerr_endline ("-- " ^ t ^ " " ^ s) *) + + let cat x = String.concat " " x + + let mk_vars idents = + let map ident = T.Inline (T.Var, ident) 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 hd = List.hd +%} + %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC + %token LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC + %token EOF + + %start items + %type items +%% + comment: + | OQ verbatims CQ { $1 ^ $2 ^ $3 } + ; + spc: + | SPC { $1 } + | comment { $1 } + ; + spcs: + | { "" } + | spc spcs { $1 ^ $2 } + ; + rspcs: + | { "" } + | SPC rspcs { $1 ^ $2 } + ; + fs: FS spcs { $1 ^ $2 }; + ident: IDENT spcs { $1 ^ $2 }; + th: TH spcs { $1 ^ $2 }; + proof: PROOF spcs { $1 ^ $2 }; + qed: QED spcs { $1 ^ $2 }; + sec: SEC spcs { $1 ^ $2 }; + def: DEF spcs { $1 ^ $2 }; + op: OP spcs { $1 ^ $2 }; + xlet: LET spcs { $1 ^ $2 }; + var: VAR spcs { $1 ^ $2 }; + req: REQ spcs { $1 ^ $2 }; + load: LOAD spcs { $1 ^ $2 }; + xp: XP spcs { $1 ^ $2 }; + ip: IP spcs { $1 ^ $2 }; + ind: IND spcs { $1 ^ $2 }; + set: SET spcs { $1 ^ $2 }; + notation: NOT spcs { $1 ^ $2 }; + oc: OC spcs { $1 ^ $2 }; + coe: COE spcs { $1 ^ $2 }; + cn: CN spcs { $1 ^ $2 }; + sc: SC spcs { $1 ^ $2 }; + str: STR spcs { $1 ^ $2 }; + id: ID spcs { $1 ^ $2 }; + coerc: COERC spcs { $1 ^ $2 }; + + + idents: + | ident { [$1] } + | ident idents { $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 } + | xlet 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_rr: + | AC { $1 } + | INT { $1 } + | IDENT { $1 } + | EXTRA { $1 } + | CN { $1 } + | COE { $1 } + | STR { $1 } + | OP { $1 } + | LET { $1 } + | IN { $1 } + | CP { $1 } + | DEF { $1 } + | SET { $1 } + | NOT { $1 } + | LOAD { $1 } + | ID { $1 } + | COERC { $1 } + ; + unexport_r: + | unexport_rr { $1, [] } + | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 } + ; + 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 coe unexports_r { $1 ^ $2 ^ fst $3, snd $3 @ [T.Coercion $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, [] } + ; + unexports: + | unexport spcs { fst $1 ^ $2, snd $1 } + | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + verbatim: + | unexport_rr { $1 } + | OC { $1 } + | CC { $1 } + | SC { $1 } + | TH { $1 } + | VAR { $1 } + | IND { $1 } + | SEC { $1 } + | REQ { $1 } + | XP { $1 } + | IP { $1 } + | QED { $1 } + | PROOF { $1 } + | FS { $1 } + | SPC { $1 } + ; + verbatims: + | { "" } + | verbatim verbatims { $1 ^ $2 } + ; + step: + | macro_step { $1 } + | restricts FS { [] } + ; + steps: + | step spcs { [] } + | step spcs steps { $1 @ $3 } + ; + + qid: + | IDENT { [$1] } + | qid AC { strip1 $2 :: $1 } + ; + + macro_step: + | th ident restricts fs proof FS steps qed FS + { out "TH" $2; $7 @ [T.Inline (T.Con, $2)] } + | th ident restricts fs proof restricts FS + { out "TH" $2; [T.Inline (T.Con, $2)] } + | th ident restricts fs steps qed FS + { out "TH" $2; $5 @ [T.Inline (T.Con, $2)] } + | th ident restricts def restricts FS + { out "TH" $2; [T.Inline (T.Con, $2)] } + | th ident def restricts FS + { out "TH" $2; [T.Inline (T.Con, $2)] } + | var idents xres FS + { out "VAR" (cat $2); mk_vars $2 } + | ind ident unexports FS + { out "IND" $2; snd $3 @ [T.Inline (T.Ind, $2)] } + | sec unexports FS + { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ $3)] } + | req xp ident FS + { out "REQ" $3; [T.Include $3] } + | req ip ident FS + { out "REQ" $3; [T.Include $3] } + | req ident FS + { out "REQ" $2; [T.Include $2] } + | load str FS + { out "REQ" $2; [T.Include (strip2 $2)] } + | coerc qid spcs cn unexports FS + { out "COERCE" (hd $2); [T.Coercion (hd $2)] } + | id coerc qid spcs cn unexports FS + { out "COERCE" (hd $3); [T.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) } + ; + item: + | comment { [T.Comment $1] } + | macro_step { $1 } + | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ $3)] } + | notation unexports FS { [T.Notation ($1 ^ fst $2 ^ $3)] } + | error { out "ERROR" "item"; failwith "item" } + ; + items: + | rspcs EOF { [] } + | rspcs item items { $2 @ $3 } + ;