]> matita.cs.unibo.it Git - helm.git/commitdiff
transcript: very alpha version.
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 15 Nov 2006 14:10:33 +0000 (14:10 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 15 Nov 2006 14:10:33 +0000 (14:10 +0000)
parser for Coq V8 works fine on CoRN contribution scripts.

14 files changed:
components/binaries/Makefile
components/binaries/transcript/.depend [new file with mode: 0644]
components/binaries/transcript/CoRN-2.conf.xml [new file with mode: 0644]
components/binaries/transcript/CoRN.conf.xml [new file with mode: 0644]
components/binaries/transcript/Makefile [new file with mode: 0644]
components/binaries/transcript/engine.ml [new file with mode: 0644]
components/binaries/transcript/engine.mli [new file with mode: 0644]
components/binaries/transcript/grafite.ml [new file with mode: 0644]
components/binaries/transcript/grafite.mli [new file with mode: 0644]
components/binaries/transcript/top.ml [new file with mode: 0644]
components/binaries/transcript/transcript.conf.xml [new file with mode: 0644]
components/binaries/transcript/types.ml [new file with mode: 0644]
components/binaries/transcript/v8Lexer.mll [new file with mode: 0644]
components/binaries/transcript/v8Parser.mly [new file with mode: 0644]

index 9dd295fb40dc83cb96502cad036655e0df64f748..db074309d2e221c6edbc50380af1374b3124c8bc 100644 (file)
@@ -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 (file)
index 0000000..5e737a1
--- /dev/null
@@ -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 (file)
index 0000000..6e39584
--- /dev/null
@@ -0,0 +1,10 @@
+<?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>
diff --git a/components/binaries/transcript/CoRN.conf.xml b/components/binaries/transcript/CoRN.conf.xml
new file mode 100644 (file)
index 0000000..e952b23
--- /dev/null
@@ -0,0 +1,10 @@
+<?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>
diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile
new file mode 100644 (file)
index 0000000..87f9ea0
--- /dev/null
@@ -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 (file)
index 0000000..92c3c73
--- /dev/null
@@ -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 (file)
index 0000000..8016d71
--- /dev/null
@@ -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 (file)
index 0000000..9900b8b
--- /dev/null
@@ -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 (file)
index 0000000..b0b5fca
--- /dev/null
@@ -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 (file)
index 0000000..387d47f
--- /dev/null
@@ -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 [ <package> | <conf_file> ]*" 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 (file)
index 0000000..d79636f
--- /dev/null
@@ -0,0 +1,8 @@
+<?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>
diff --git a/components/binaries/transcript/types.ml b/components/binaries/transcript/types.ml
new file mode 100644 (file)
index 0000000..d7770ad
--- /dev/null
@@ -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 (file)
index 0000000..cddb728
--- /dev/null
@@ -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 (file)
index 0000000..9529bfb
--- /dev/null
@@ -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 <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 }
+    ;