+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /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
-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
+++ /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 suffix: string
-
-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 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 }
+++ /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 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 <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM
- %token <string> 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 <Types.items> 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 }
- ;
-*/
+++ /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 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"
+++ /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: Types.output_kind -> out_channel -> Types.items -> unit
-
-val string_of_inline_kind: Types.inline_kind -> string
+++ /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 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 }
+++ /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 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 <string> SPC OK CK FS QED TH UNX PS ID RAW
- %token EOF
-
- %start items
- %type <Types.items> 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 " ^ "") } */
- ;
+++ /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 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)
+++ /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 [ -glmpx | -C <dir> ] [ <package> | <conf_file> ]*" in
- let help_C = " set working directory to <dir>" 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
+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="transcript">
- <key name="heading_path">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 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
projects / helm.git / commitdiff