parser for Coq V8 works fine on CoRN contribution scripts.
#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@%)
--- /dev/null
+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
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="package">
+ <key name="name">CoRN</key>
+ <key name="base_uri">cic:/matita/CoRN-Decl</key>
+ <key name="input_path">/home/fguidi/CoRN-2</key>
+ <key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
+ <key name="script_ext">.v</key>
+ </section>
+</helm_registry>
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="package">
+ <key name="name">CoRN</key>
+ <key name="base_uri">cic:/matita/CoRN-Decl</key>
+ <key name="input_path">/projects/helm/exportation/CoRN</key>
+ <key name="output_path">$(transcript.helm_dir)/matita/contribs/CoRN-Decl</key>
+ <key name="script_type">.v</key>
+ </section>
+</helm_registry>
--- /dev/null
+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
--- /dev/null
+(* 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
--- /dev/null
+(* 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
--- /dev/null
+(* 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)
--- /dev/null
+(* 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
--- /dev/null
+(* 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 [ <package> | <conf_file> ]*" in
+ let process_package package = Engine.produce (Engine.make package) in
+ Engine.init ();
+ Arg.parse [
+ ] process_package help
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="transcript">
+ <key name="helm_dir">/home/fguidi/svn/software</key>
+ <key name="heading_path">matita/matita.ma.templ</key>
+ <key name="heading_lines">14</key>
+ </section>
+</helm_registry>
--- /dev/null
+(* 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
--- /dev/null
+{
+ 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 }
--- /dev/null
+/* 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 <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
+ %token <string> LET IN TH PROOF QED VAR IND SEC REQ XP IP SET NOT LOAD ID COERC
+ %token EOF
+
+ %start items
+ %type <Types.items> 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 }
+ ;
projects / helm.git / commitdiff