From: Ferruccio Guidi Date: Tue, 14 Apr 2009 20:06:32 +0000 (+0000) Subject: - Procedural: generation of "exact" is now complete X-Git-Tag: make_still_working~4083 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;p=helm.git - Procedural: generation of "exact" is now complete - relevant tactics are now counted correctly - PrimitiveTactics: we set exact_tac = apply_tac as in NTactics - transcript: the grafite parser is now working the "library" devel is parsed succesfully - procedural/library: new devel. Will contain the procedural reconstruction of "library" --- diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml index ad3152530..a0c0331f3 100644 --- a/helm/software/components/acic_procedural/procedural1.ml +++ b/helm/software/components/acic_procedural/procedural1.ml @@ -198,13 +198,14 @@ let mk_exp_args hd tl classes synth = let map v (cl, b) = if I.overlaps synth cl && b then v else meta "" in - let rec aux = function - | [] -> [] - | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl) + let rec aux b = function + | [] -> b, [] + | hd :: tl -> + if hd = meta "" then aux true tl else b, List.rev (hd :: tl) in let args = T.list_rev_map2 map tl classes in - let args = aux args in - if args = [] then hd else C.AAppl ("", hd :: args) + let b, args = aux false args in + if args = [] then b, hd else b, C.AAppl ("", hd :: args) let mk_convert st ?name sty ety note = let e = Cn.hole "" in @@ -365,6 +366,7 @@ and proc_appl st what hd tl = let synth = mk_synth I.S.empty decurry in let text = "" (* Printf.sprintf "%u %s" parsno (Cl.to_string h) *) in let script = List.rev (mk_arg st hd) in + let tactic b t n = if b then T.Apply (t, n) else T.Exact (t, n) in match rc with | Some (i, j, uri, tyno) -> let classes2, tl2, _, where = split2_last classes tl in @@ -374,8 +376,8 @@ and proc_appl st what hd tl = let qs = proc_bkd_proofs (next st) synth2 names classes2 tl2 in if List.length qs <> List.length names then let qs = proc_bkd_proofs (next st) synth [] classes tl in - let hd = mk_exp_args hd tl classes synth in - script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + let b, hd = mk_exp_args hd tl classes synth in + script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else if is_rewrite_right hd then script2 @ mk_rewrite st dtext where qs tl2 false what else if is_rewrite_left hd then @@ -389,8 +391,8 @@ and proc_appl st what hd tl = | None -> let names = get_sub_names hd tl in let qs = proc_bkd_proofs (next st) synth names classes tl in - let hd = mk_exp_args hd tl classes synth in - script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] + let b, hd = mk_exp_args hd tl classes synth in + script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else [T.Exact (what, dtext)] in diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index 75ce2ee64..b30d6e862 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -279,12 +279,19 @@ let render_steps a = render_steps mk_dot a let rec count_step a = function | Note _ - | Statement _ + | Statement _ + | Inductive _ + | Qed _ +(* level 0 *) + | Intros (Some 0, [], _) | Id _ | Exact _ - | Qed _ -> a - | Branch (pps, _) -> List.fold_left count_steps a pps - | _ -> succ a + | Change _ + | Clear _ + | ClearBody _ -> a + | Branch (pps, _) -> List.fold_left count_steps a pps +(* level 1 *) + | _ -> succ a and count_steps a = List.fold_left count_step a @@ -294,7 +301,7 @@ let rec count_node a = function | Note _ | Inductive _ | Statement _ - | Qed _ + | Qed _ | Id _ | Intros _ | Clear _ diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 8121968e9..e2fae069b 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,19 +1,19 @@ -v8Parser.cmi: types.cmo +gallina8Parser.cmi: types.cmo +grafiteParser.cmi: types.cmo grafite.cmi: types.cmo -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: -v8Parser.cmo: types.cmo options.cmo v8Parser.cmi -v8Parser.cmx: types.cmx options.cmx v8Parser.cmi -v8Lexer.cmo: v8Parser.cmi options.cmo -v8Lexer.cmx: v8Parser.cmx 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: v8Parser.cmi v8Lexer.cmo types.cmo options.cmo grafite.cmi \ - engine.cmi -engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx options.cmx grafite.cmx \ - engine.cmi +engine.cmo: types.cmo options.cmo grafite.cmi gallina8Parser.cmi \ + gallina8Lexer.cmo engine.cmi +engine.cmx: types.cmx options.cmx grafite.cmx gallina8Parser.cmx \ + gallina8Lexer.cmx engine.cmi top.cmo: options.cmo engine.cmi top.cmx: options.cmx engine.cmx diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index b64d148de..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,19 +1,19 @@ -v8Parser.cmi: types.cmx +gallina8Parser.cmi: types.cmx +grafiteParser.cmi: types.cmx grafite.cmi: types.cmx -engine.cmi: -types.cmo: -types.cmx: -options.cmo: -options.cmx: -v8Parser.cmo: types.cmx options.cmx v8Parser.cmi -v8Parser.cmx: types.cmx options.cmx v8Parser.cmi -v8Lexer.cmo: v8Parser.cmi options.cmx -v8Lexer.cmx: v8Parser.cmx 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: v8Parser.cmi v8Lexer.cmx types.cmx options.cmx grafite.cmi \ - engine.cmi -engine.cmx: v8Parser.cmx v8Lexer.cmx types.cmx options.cmx grafite.cmx \ - engine.cmi +engine.cmo: types.cmx options.cmx grafiteParser.cmi grafiteLexer.cmx \ + grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi +engine.cmx: types.cmx options.cmx grafiteParser.cmx grafiteLexer.cmx \ + grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi top.cmo: options.cmx engine.cmi top.cmx: options.cmx engine.cmx diff --git a/helm/software/components/binaries/transcript/Makefile b/helm/software/components/binaries/transcript/Makefile index 9ac3969b6..b3cc00a0c 100644 --- a/helm/software/components/binaries/transcript/Makefile +++ b/helm/software/components/binaries/transcript/Makefile @@ -4,9 +4,13 @@ H=@ REQUIRES = unix str helm-grafite_parser -MLS = types.ml options.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 +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 diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index ccf07423f..4504d2999 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -46,8 +46,9 @@ type status = { output_base_uri: string; input_path: string; output_path: string; - input_type: string; + input_type: T.input_kind; output_type: T.output_kind; + input_ext: string; includes: (string * string) list; coercions: (string * string) list; files: string list; @@ -72,8 +73,8 @@ let load_registry 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_type 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 @@ -100,6 +101,12 @@ let init () = let make registry = let id x = x in let get_pairs = R.get_list (R.pair id id) in + let get_input_type key = + match R.get_string key with + | "gallina8" -> T.Gallina8, ".v" + | "grafite" -> T.Grafite, ".ma" + | _ -> failwith "unknown input type" + in let get_output_type key = match R.get_string key with | "procedural" -> T.Procedural @@ -107,17 +114,23 @@ let make registry = | _ -> failwith "unknown output type" in load_registry registry; + let input_type, input_ext = get_input_type "package.input_type" in + let heading_lines = match input_type with + | T.Grafite -> 0 + | _ -> R.get_int "transcript.heading_lines" + in let st = { heading_path = R.get_string "transcript.heading_path"; - heading_lines = R.get_int "transcript.heading_lines"; + heading_lines = 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 = R.get_string "package.input_type"; + input_type = input_type; output_type = get_output_type "package.output_type"; + input_ext = input_ext; includes = get_pairs "package.include"; coercions = get_pairs "package.coercion"; files = []; @@ -126,7 +139,8 @@ let make registry = } in let st = {st with heading_path = Filename.concat !O.cwd st.heading_path; - output_path = Filename.concat !O.cwd st.output_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 @@ -154,7 +168,7 @@ let set_items st name items = let contents = List.rev_append items script.contents in st.scripts.(i) <- {script with name = name; contents = contents} -let set_heading st name = +let set_heading st name = let heading = st.heading_path, st.heading_lines in set_items st name [T.Heading heading] @@ -193,6 +207,10 @@ let produce st = | 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 @@ -225,12 +243,11 @@ let produce st = with Not_found -> () in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path (name ^ st.input_type) in + let file = Filename.concat st.input_path (name ^ st.input_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; + 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 diff --git a/helm/software/components/binaries/transcript/gallina8Lexer.mll b/helm/software/components/binaries/transcript/gallina8Lexer.mll new file mode 100644 index 000000000..586bab472 --- /dev/null +++ b/helm/software/components/binaries/transcript/gallina8Lexer.mll @@ -0,0 +1,129 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +{ + module O = Options + module P = Gallina8Parser + + let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) + + let check s = + let c = Char.code s.[0] in + if c <= 127 then s else + let escaped = Printf.sprintf "\\%3u\\" c in + begin + if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped; + escaped + end +} + +let QT = '"' +let SPC = [' ' '\t' '\n' '\r']+ +let ALPHA = ['A'-'Z' 'a'-'z' '_'] +let FIG = ['0'-'9'] +let ID = ALPHA (ALPHA | FIG | "\'")* +let RAWID = QT [^ '"']* QT +let NUM = "-"? FIG+ + +rule token = parse + | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } + | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "CoFixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } + | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } + | "Save" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } + | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } + | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s } + | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } + | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } + | "Parameter" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } + | "Parameters" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } + | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } + | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } + | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } + | "Scheme" { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s } + | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } + | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s } + | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Hints" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s } + | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } + | "Import" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } + | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s } + | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Reset" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Delimit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Bind" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Arguments" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Open" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "V7only" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } + | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Reserved" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Grammar" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Syntax" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Add" SPC "Morphism" + { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s } + | "Add" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } + | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } + | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s } + | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s } + | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s } + | "with" { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s } + | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } + | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s } + | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s } + | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s } + | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s } + | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s } + | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s } + | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } + | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } + | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s } + | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s } + | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s } + | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s } + | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s } + | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s } + | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s } + | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s } + | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s } + | _ + { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s } + | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/helm/software/components/binaries/transcript/gallina8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly new file mode 100644 index 000000000..8bba4fb0b --- /dev/null +++ b/helm/software/components/binaries/transcript/gallina8Parser.mly @@ -0,0 +1,611 @@ +/* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + */ + +%{ + module T = Types + module O = Options + + let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s) + + let trim = HExtlib.trim_blanks + + let hd = List.hd + + let cat x = String.concat " " x + + let mk_vars local idents = + let kind = if local then T.Var else T.Con in + let map ident = T.Inline (local, kind, trim ident, "", None) in + List.map map idents + + let strip2 s = + String.sub s 1 (String.length s - 2) + + let strip1 s = + String.sub s 1 (String.length s - 1) + + let coercion str = + [T.Coercion (false, str); T.Coercion (true, str)] + + let notation str = + [T.Notation (false, str); T.Notation (true, str)] + + let mk_flavour str = + match trim str with + | "Remark" -> Some `Remark + | "Lemma" -> Some `Lemma + | "Theorem" -> Some `Theorem + | "Definition" -> Some `Definition + | "Fixpoint" -> Some `Definition + | "CoFixpoint" -> Some `Definition + | "Let" -> Some `Definition + | "Scheme" -> Some `Theorem + | _ -> assert false + + let mk_morphism ext = + let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in + List.rev_map generate ["2"; "1"] + +%} + %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM + %token WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR + %token EOF + + %start items + %type items +%% +/* SPACED TOKENS ************************************************************/ + + ident: xident spcs { $1 ^ $2 }; + fs: FS spcs { $1 ^ $2 }; + mor: MOR spcs { $1 ^ $2 }; + th: TH spcs { $1 ^ $2 }; + xlet: LET spcs { $1 ^ $2 }; + proof: PROOF spcs { $1 ^ $2 }; + qed: QED spcs { $1 ^ $2 }; + gen: GEN spcs { $1 ^ $2 }; + sec: SEC spcs { $1 ^ $2 }; + xend: END spcs { $1 ^ $2 }; + unx: UNX spcs { $1 ^ $2 }; + def: DEF spcs { $1 ^ $2 }; + op: OP spcs { $1 ^ $2 }; + abbr: ABBR spcs { $1 ^ $2 }; + var: VAR spcs { $1 ^ $2 }; + ax: AX spcs { $1 ^ $2 }; + req: REQ spcs { $1 ^ $2 }; + load: LOAD spcs { $1 ^ $2 }; + xp: XP spcs { $1 ^ $2 }; + ind: IND spcs { $1 ^ $2 }; + set: SET spcs { $1 ^ $2 }; + notation: NOT spcs { $1 ^ $2 }; + cn: CN spcs { $1 ^ $2 }; + str: STR spcs { $1 ^ $2 }; + id: ID spcs { $1 ^ $2 }; + coerc: COERC spcs { $1 ^ $2 }; + cm: CM spcs { $1 ^ $2 } | { "" } + wh: WITH spcs { $1 ^ $2 }; + +/* SPACES *******************************************************************/ + + comment: + | OQ verbatims CQ { $1 ^ $2 ^ $3 } + ; + spc: + | SPC { $1 } + | comment { $1 } + ; + spcs: + | { "" } + | spc spcs { $1 ^ $2 } + ; + rspcs: + | { "" } + | SPC rspcs { $1 ^ $2 } + ; + +/* IDENTIFIERS **************************************************************/ + + outer_keyword: + | LET { $1 } + | TH { $1 } + | VAR { $1 } + | AX { $1 } + | IND { $1 } + | GEN { $1 } + | SEC { $1 } + | END { $1 } + | UNX { $1 } + | REQ { $1 } + | LOAD { $1 } + | SET { $1 } + | NOT { $1 } + | ID { $1 } + | COERC { $1 } + | MOR { $1 } + ; + inner_keyword: + | XP { $1 } + ; + xident: + | IDENT { $1 } + | outer_keyword { $1 } + | WITH { $1 } + ; + qid: + | xident { [$1] } + | qid AC { strip1 $2 :: $1 } + ; + idents: + | ident { [$1] } + | ident cm idents { $1 :: $3 } + ; + +/* PLAIN SKIP ***************************************************************/ + + plain_skip: + | IDENT { $1 } + | inner_keyword { $1 } + | STR { $1 } + | INT { $1 } + | COE { $1 } + | OC { $1 } + | CC { $1 } + | SC { $1 } + | CN { $1 } + | CM { $1 } + | EXTRA { $1 } + ; + inner_skip: + | plain_skip { $1 } + | outer_keyword { $1 } + | AC { $1 } + | DEF { $1 } + | PROOF { $1 } + | QED { $1 } + | FS { $1 } + | WITH { $1 } + ; + +/* LEFT SKIP ****************************************************************/ + + rlskip: + | plain_skip { $1, [] } + | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } + | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } + | IN { $1, [] } + | CP { $1, [] } + ; + xlskip: + | outer_keyword { $1, [] } + | AC { $1, [] } + | WITH { $1, [] } + | rlskip { $1 } + ; + xlskips: + | xlskip spcs { fst $1 ^ $2, snd $1 } + | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + lskips: + | rlskip spcs { fst $1 ^ $2, snd $1 } + | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + opt_lskips: + | lskips { $1 } + | { "", [] } + ; + +/* GENERAL SKIP *************************************************************/ + + rskip: + | rlskip { $1 } + | DEF { $1, [] } + ; + xskip: + | outer_keyword { $1, [] } + | AC { $1, [] } + | WITH { $1, [] } + | rskip { $1 } + ; + xskips: + | xskip spcs { fst $1 ^ $2, snd $1 } + | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + skips: + | rskip spcs { fst $1 ^ $2, snd $1 } + | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + +/* ABBREVIATION SKIP ********************************************************/ + + li_skip: + | inner_skip { $1, [] } + | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } + | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } + ; + li_skips: + | li_skip spcs { fst $1 ^ $2, snd $1 } + | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + +/* PARENTETIC SKIP **********************************************************/ + + ocp_skip: + | inner_skip { $1, [] } + | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } + | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } + | IN { $1, [] } + ; + ocp_skips: + | ocp_skip spcs { fst $1 ^ $2, snd $1 } + | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + +/* VERBATIM SKIP ************************************************************/ + + verbatim: + | comment { $1 } + | inner_skip { $1 } + | ABBR { $1 } + | IN { $1 } + | OP { $1 } + | CP { $1 } + | SPC { $1 } + ; + verbatims: + | { "" } + | verbatim verbatims { $1 ^ $2 } + ; + +/* PROOF STEPS **************************************************************/ + + step: + | macro_step { $1 } + | skips FS { snd $1 } + ; + steps: + | step spcs { $1 } + | step spcs steps { $1 @ $3 } + ; + just: + | steps qed { $1 } + | proof fs steps qed { $3 } + | proof skips { snd $2 } + | proof wh skips fs steps qed { snd $3 @ $5 } + ; + macro_step: + | th ident opt_lskips def xskips FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | th ident lskips fs just FS + { out "TH" $2; + $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | gen ident def xskips FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | mor ident cn ident fs just FS + { out "MOR" $4; $6 @ mk_morphism (trim $4) } + | xlet ident opt_lskips def xskips FS + { out "TH" $2; + [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident lskips fs just FS + { out "TH" $2; + $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | var idents cn xskips FS + { out "VAR" (cat $2); mk_vars true $2 } + | ax idents cn xskips FS + { out "AX" (cat $2); mk_vars false $2 } + | ind ident skips FS + { out "IND" $2; + T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 + } + | sec ident FS + { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } + | xend ident FS + { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } + | unx xskips FS + { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + | req xp ident FS + { out "REQ" $3; [T.Include (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 skips FS + { out "COERCE" (hd $2); coercion (hd $2) } + | id coerc qid spcs skips FS + { out "COERCE" (hd $3); coercion (hd $3) } + | th ident error + { out "ERROR" $2; failwith ("macro_step " ^ $2) } + | ind ident error + { out "ERROR" $2; failwith ("macro_step " ^ $2) } + | var idents error + { let vs = cat $2 in + out "ERROR" vs; failwith ("macro_step " ^ vs) } + | ax idents error + { let vs = cat $2 in + out "ERROR" vs; failwith ("macro_step " ^ vs) } + ; + +/* VERNACULAR ITEMS *********************************************************/ + + item: + | OQ verbatims CQ { [T.Comment $2] } + | macro_step { $1 } + | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) } + | error { out "ERROR" "item"; failwith "item" } + ; + items: + | rspcs EOF { [] } + | rspcs item items { $2 @ $3 } + ; + + +/* + oc: OC spcs { $1 ^ $2 }; + coe: COE spcs { $1 ^ $2 }; + sc: SC spcs { $1 ^ $2 }; + + cnot: + | EXTRA { $1 } + | INT { $1 } + ; + cnots: + | cnot spcs { $1 ^ $2 } + | cnot spcs cnots { $1 ^ $2 ^ $3 } + ; + + xstrict: + | AC { $1 } + | INT { $1 } + | EXTRA { $1 } + | CN { $1 } + | SC { $1 } + | OC { $1 } + | CC { $1 } + | COE { $1 } + | STR { $1 } + | abbr extends0 IN { $1 ^ $2 ^ $3 } + | op extends1 CP { $1 ^ $2 ^ $3 } + ; + strict: + | xstrict { $1 } + | IDENT { $1 } + | SET { $1 } + | NOT { $1 } + ; + restrict: + | strict { $1 } + | IN { $1 } + | CP { $1 } + ; + xre: + | xstrict { $1 } + | IN { $1 } + | CP { $1 } + ; + restricts: + | restrict spcs { $1 ^ $2 } + | restrict spcs restricts { $1 ^ $2 ^ $3 } + ; + xres: + | xre spcs { $1 ^ $2 } + | xre spcs restricts { $1 ^ $2 ^ $3 } + ; + extend0: + | strict { $1 } + | DEF { $1 } + ; + extends0: + | extend0 spcs { $1 ^ $2 } + | extend0 spcs extends0 { $1 ^ $2 ^ $3 } + ; + extend1: + | strict { $1 } + | DEF { $1 } + | IN { $1 } + ; + extends1: + | extend1 spcs { $1 ^ $2 } + | extend1 spcs extends1 { $1 ^ $2 ^ $3 } + ; + unexport_ff: + | IDENT { $1 } + | AC { $1 } + | STR { $1 } + | OP { $1 } + | ABBR { $1 } + | IN { $1 } + | CP { $1 } + | SET { $1 } + ; + unexport_rr: + | unexport_ff { $1 } + | INT { $1 } + | EXTRA { $1 } + | CN { $1 } + | COE { $1 } + | DEF { $1 } + ; + unexport_r: + | unexport_rr { $1, [] } + | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 } + | oc unexport_ff CC { $1, [] } + ; + unexports_r: + | unexport_r spcs { fst $1 ^ $2, snd $1 } + | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + field: + | ident cn unexports_r + { $1 ^ $2 ^ fst $3, snd $3 } + | ident def unexports_r + { $1 ^ $2 ^ fst $3, snd $3 } + | ident coe unexports_r + { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) } + ; + fields: + | field { $1 } + | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + | cnots { $1, [] } + | error { out "ERROR" "fields"; failwith "fields" } + ; + unexport: + | unexport_r { $1 } + | SC { $1, [] } + | CC { $1, [] } + | IP { $1, [] } + | LET { $1, [] } + | VAR { $1, [] } + + ; + unexports: + | unexport spcs { fst $1 ^ $2, snd $1 } + | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } + ; + verbatim: + | unexport_rr { $1 } + | reserved_ident { $1 } + | comment { $1 } + | OC { $1 } + | CC { $1 } + | SC { $1 } + | XP { $1 } + | IP { $1 } + | FS { $1 } + | SPC { $1 } + ; + verbatims: + | { "" } + | verbatim verbatims { $1 ^ $2 } + ; + step: + | macro_step { $1 } + | restricts FS { [] } + ; + steps: + | step spcs { [] } + | step spcs steps { $1 @ $3 } + ; + + macro_step: + | th ident restricts fs proof FS steps qed FS + { out "TH" $2; + $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | th ident restricts fs proof restricts FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | th ident restricts fs steps qed FS + { out "TH" $2; + $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | th ident restricts def restricts FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | th ident def restricts FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | gen ident def restricts FS + { out "TH" $2; + [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident restricts fs proof FS steps qed FS + { out "LET" $2; + $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident restricts fs proof restricts FS + { out "LET" $2; + [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident restricts fs steps qed FS + { out "LET" $2; + $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident restricts def restricts FS + { out "LET" $2; + [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | xlet ident def restricts FS + { out "LET" $2; + [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] + } + | var idents xres FS + { out "VAR" (cat $2); mk_vars true $2 } + | ax idents xres FS + { out "AX" (cat $2); mk_vars false $2 } + | ind ident unexports FS + { out "IND" $2; + T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 + } + | sec ident FS + { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } + | xend ident FS + { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } + | unx unexports FS + { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + | req xp ident FS + { out "REQ" $3; [T.Include (trim $3)] } + | req ip ident FS + { out "REQ" $3; [T.Include (trim $3)] } + | req ident FS + { out "REQ" $2; [T.Include (trim $2)] } + | load str FS + { out "REQ" $2; [T.Include (strip2 (trim $2))] } + | coerc qid spcs cn unexports FS + { out "COERCE" (hd $2); coercion (hd $2) } + | id coerc qid spcs cn unexports FS + { out "COERCE" (hd $3); coercion (hd $3) } + | th ident error + { out "ERROR" $2; failwith ("macro_step " ^ $2) } + | ind ident error + { out "ERROR" $2; failwith ("macro_step " ^ $2) } + | var idents error + { let vs = cat $2 in + out "ERROR" vs; failwith ("macro_step " ^ vs) } + | ax idents error + { let vs = cat $2 in + out "ERROR" vs; failwith ("macro_step " ^ vs) } + ; + item: + | OQ verbatims CQ { [T.Comment $2] } + | macro_step { $1 } + | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } + | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) } + | error { out "ERROR" "item"; failwith "item" } + ; + items: + | rspcs EOF { [] } + | rspcs item items { $2 @ $3 } + ; +*/ diff --git a/helm/software/components/binaries/transcript/grafiteLexer.mll b/helm/software/components/binaries/transcript/grafiteLexer.mll new file mode 100644 index 000000000..bfa818e30 --- /dev/null +++ b/helm/software/components/binaries/transcript/grafiteLexer.mll @@ -0,0 +1,75 @@ +(* 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 } + | "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 } + | IDENT { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } + | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } + | "." { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } + | _ { let s = Lexing.lexeme lexbuf in out "RAW" s; P.RAW s } + | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly new file mode 100644 index 000000000..3163a6a07 --- /dev/null +++ b/helm/software/components/binaries/transcript/grafiteParser.mly @@ -0,0 +1,141 @@ +/* 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, None + | _ -> assert false + +%} + %token SPC OK CK FS QED TH UNX PS ID RAW + %token EOF + + %start items + %type items +%% + +/* LINES ITEMS ***************************************************************/ + + extra: + | ID { $1 } + | QED { $1 } + | RAW { $1 } + ; + text: + | extra { $1 } + | TH { $1 } + | UNX { $1 } + | PS { $1 } + | comment { $1 } + ; + texts: + | { "" } + | text texts { $1 ^ $2 } + ; + line: + | texts FS { $1 ^ $2 } + ; + drop: + | extra line { $1 ^ $2 } + ; + drops: + | { "" } + | drop drops { $1 ^ $2 } + ; + +/* SPACE ITEMS *************************************************************/ + + verbatim: + | text { $1 } + | FS { $1 } + ; + verbatims: + | { "" } + | verbatim verbatims { $1 ^ $2 } + ; + comment: + | SPC { $1 } + | OK verbatims CK { $1 ^ $2 ^ $3 } + ; + +/* STEPS ********************************************************************/ + + step: + | comment { $1 } + | FS { $1 } + | TH { $1 } + | UNX { $1 } + | PS { $1 } + | ID { $1 } + | RAW { $1 } + ; + steps: + | QED FS { $1 ^ $2 } + | step steps { $1 ^ $2 } + ; + +/* ITEMS ********************************************************************/ + + id: + | ID { $1 } + | TH { $1 } + | UNX { $1 } + | PS { $1 } + ; + + item: + | comment + { out "OK" $1; [T.Verbatim $1] } + | TH SPC id line drops + { out "TH" $3; + let a, b = mk_flavour $1 in [T.Inline (true, a, $3, "", b)] + } + | UNX line drops + { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } + | PS steps + { [] } + ; + items: + | EOF { [] } + | item items { $1 @ $2 } +/* | error { out "ERROR" ""; failwith ("item id " ^ "") } */ + ; diff --git a/helm/software/components/binaries/transcript/types.ml b/helm/software/components/binaries/transcript/types.ml index fbe112a83..7b17db7b2 100644 --- a/helm/software/components/binaries/transcript/types.ml +++ b/helm/software/components/binaries/transcript/types.ml @@ -27,6 +27,8 @@ type local = bool type inline_kind = Con | Ind | Var +type input_kind = Gallina8 | Grafite + type output_kind = Declarative | Procedural type source = string diff --git a/helm/software/components/binaries/transcript/v8Lexer.mll b/helm/software/components/binaries/transcript/v8Lexer.mll deleted file mode 100644 index 0ef38a919..000000000 --- a/helm/software/components/binaries/transcript/v8Lexer.mll +++ /dev/null @@ -1,104 +0,0 @@ -{ - module O = Options - module P = V8Parser - - let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) - - let check s = - let c = Char.code s.[0] in - if c <= 127 then s else - let escaped = Printf.sprintf "\\%3u\\" c in - begin - if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped; - escaped - end -} - -let QT = '"' -let SPC = [' ' '\t' '\n' '\r']+ -let ALPHA = ['A'-'Z' 'a'-'z' '_'] -let FIG = ['0'-'9'] -let ID = ALPHA (ALPHA | FIG | "\'")* -let RAWID = QT [^ '"']* QT -let NUM = "-"? FIG+ - -rule token = parse - | "Let" { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s } - | "Remark" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Lemma" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Theorem" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Definition" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Fixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "CoFixpoint" { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s } - | "Qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Save" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Defined" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } - | "Proof" { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s } - | "Variable" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Variables" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Hypothesis" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Hypotheses" { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s } - | "Axiom" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Parameter" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Parameters" { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s } - | "Inductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "Record" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s } - | "Scheme" { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s } - | "Section" { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s } - | "End" { let s = Lexing.lexeme lexbuf in out "END" s; P.END s } - | "Hint" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Hints" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Unset" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Print" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Opaque" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Ltac" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Tactic" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Declare" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } - | "Require" { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s } - | "Export" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } - | "Import" { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s } - | "Load" { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s } - | "Set" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Reset" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Implicit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Delimit" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Bind" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Arguments" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Open" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "V7only" { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s } - | "Notation" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Reserved" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Infix" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Grammar" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Syntax" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Add" SPC "Morphism" - { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s } - | "Add" { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s } - | "Identity" { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } - | "Coercion" { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s } - | "let" { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s } - | "in" { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s } - | "with" { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s } - | SPC { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s } - | ID { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s } - | RAWID { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s } - | NUM { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s } - | ":=" { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s } - | ":>" { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s } - | "." ID { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s } - | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | "." eof { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } - | "(*" { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s } - | "*)" { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s } - | "(" { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s } - | ")" { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s } - | "{" { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s } - | "}" { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s } - | ";" { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s } - | ":" { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s } - | "," { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s } - | _ - { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s } - | eof { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF } diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/v8Parser.mly deleted file mode 100644 index 8bba4fb0b..000000000 --- a/helm/software/components/binaries/transcript/v8Parser.mly +++ /dev/null @@ -1,611 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -%{ - module T = Types - module O = Options - - let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s) - - let trim = HExtlib.trim_blanks - - let hd = List.hd - - let cat x = String.concat " " x - - let mk_vars local idents = - let kind = if local then T.Var else T.Con in - let map ident = T.Inline (local, kind, trim ident, "", None) in - List.map map idents - - let strip2 s = - String.sub s 1 (String.length s - 2) - - let strip1 s = - String.sub s 1 (String.length s - 1) - - let coercion str = - [T.Coercion (false, str); T.Coercion (true, str)] - - let notation str = - [T.Notation (false, str); T.Notation (true, str)] - - let mk_flavour str = - match trim str with - | "Remark" -> Some `Remark - | "Lemma" -> Some `Lemma - | "Theorem" -> Some `Theorem - | "Definition" -> Some `Definition - | "Fixpoint" -> Some `Definition - | "CoFixpoint" -> Some `Definition - | "Let" -> Some `Definition - | "Scheme" -> Some `Theorem - | _ -> assert false - - let mk_morphism ext = - let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in - List.rev_map generate ["2"; "1"] - -%} - %token SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM - %token WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR - %token EOF - - %start items - %type items -%% -/* SPACED TOKENS ************************************************************/ - - ident: xident spcs { $1 ^ $2 }; - fs: FS spcs { $1 ^ $2 }; - mor: MOR spcs { $1 ^ $2 }; - th: TH spcs { $1 ^ $2 }; - xlet: LET spcs { $1 ^ $2 }; - proof: PROOF spcs { $1 ^ $2 }; - qed: QED spcs { $1 ^ $2 }; - gen: GEN spcs { $1 ^ $2 }; - sec: SEC spcs { $1 ^ $2 }; - xend: END spcs { $1 ^ $2 }; - unx: UNX spcs { $1 ^ $2 }; - def: DEF spcs { $1 ^ $2 }; - op: OP spcs { $1 ^ $2 }; - abbr: ABBR spcs { $1 ^ $2 }; - var: VAR spcs { $1 ^ $2 }; - ax: AX spcs { $1 ^ $2 }; - req: REQ spcs { $1 ^ $2 }; - load: LOAD spcs { $1 ^ $2 }; - xp: XP spcs { $1 ^ $2 }; - ind: IND spcs { $1 ^ $2 }; - set: SET spcs { $1 ^ $2 }; - notation: NOT spcs { $1 ^ $2 }; - cn: CN spcs { $1 ^ $2 }; - str: STR spcs { $1 ^ $2 }; - id: ID spcs { $1 ^ $2 }; - coerc: COERC spcs { $1 ^ $2 }; - cm: CM spcs { $1 ^ $2 } | { "" } - wh: WITH spcs { $1 ^ $2 }; - -/* SPACES *******************************************************************/ - - comment: - | OQ verbatims CQ { $1 ^ $2 ^ $3 } - ; - spc: - | SPC { $1 } - | comment { $1 } - ; - spcs: - | { "" } - | spc spcs { $1 ^ $2 } - ; - rspcs: - | { "" } - | SPC rspcs { $1 ^ $2 } - ; - -/* IDENTIFIERS **************************************************************/ - - outer_keyword: - | LET { $1 } - | TH { $1 } - | VAR { $1 } - | AX { $1 } - | IND { $1 } - | GEN { $1 } - | SEC { $1 } - | END { $1 } - | UNX { $1 } - | REQ { $1 } - | LOAD { $1 } - | SET { $1 } - | NOT { $1 } - | ID { $1 } - | COERC { $1 } - | MOR { $1 } - ; - inner_keyword: - | XP { $1 } - ; - xident: - | IDENT { $1 } - | outer_keyword { $1 } - | WITH { $1 } - ; - qid: - | xident { [$1] } - | qid AC { strip1 $2 :: $1 } - ; - idents: - | ident { [$1] } - | ident cm idents { $1 :: $3 } - ; - -/* PLAIN SKIP ***************************************************************/ - - plain_skip: - | IDENT { $1 } - | inner_keyword { $1 } - | STR { $1 } - | INT { $1 } - | COE { $1 } - | OC { $1 } - | CC { $1 } - | SC { $1 } - | CN { $1 } - | CM { $1 } - | EXTRA { $1 } - ; - inner_skip: - | plain_skip { $1 } - | outer_keyword { $1 } - | AC { $1 } - | DEF { $1 } - | PROOF { $1 } - | QED { $1 } - | FS { $1 } - | WITH { $1 } - ; - -/* LEFT SKIP ****************************************************************/ - - rlskip: - | plain_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - | IN { $1, [] } - | CP { $1, [] } - ; - xlskip: - | outer_keyword { $1, [] } - | AC { $1, [] } - | WITH { $1, [] } - | rlskip { $1 } - ; - xlskips: - | xlskip spcs { fst $1 ^ $2, snd $1 } - | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - lskips: - | rlskip spcs { fst $1 ^ $2, snd $1 } - | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - opt_lskips: - | lskips { $1 } - | { "", [] } - ; - -/* GENERAL SKIP *************************************************************/ - - rskip: - | rlskip { $1 } - | DEF { $1, [] } - ; - xskip: - | outer_keyword { $1, [] } - | AC { $1, [] } - | WITH { $1, [] } - | rskip { $1 } - ; - xskips: - | xskip spcs { fst $1 ^ $2, snd $1 } - | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - skips: - | rskip spcs { fst $1 ^ $2, snd $1 } - | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* ABBREVIATION SKIP ********************************************************/ - - li_skip: - | inner_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - ; - li_skips: - | li_skip spcs { fst $1 ^ $2, snd $1 } - | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* PARENTETIC SKIP **********************************************************/ - - ocp_skip: - | inner_skip { $1, [] } - | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 } - | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 } - | IN { $1, [] } - ; - ocp_skips: - | ocp_skip spcs { fst $1 ^ $2, snd $1 } - | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - -/* VERBATIM SKIP ************************************************************/ - - verbatim: - | comment { $1 } - | inner_skip { $1 } - | ABBR { $1 } - | IN { $1 } - | OP { $1 } - | CP { $1 } - | SPC { $1 } - ; - verbatims: - | { "" } - | verbatim verbatims { $1 ^ $2 } - ; - -/* PROOF STEPS **************************************************************/ - - step: - | macro_step { $1 } - | skips FS { snd $1 } - ; - steps: - | step spcs { $1 } - | step spcs steps { $1 @ $3 } - ; - just: - | steps qed { $1 } - | proof fs steps qed { $3 } - | proof skips { snd $2 } - | proof wh skips fs steps qed { snd $3 @ $5 } - ; - macro_step: - | th ident opt_lskips def xskips FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident lskips fs just FS - { out "TH" $2; - $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | gen ident def xskips FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | mor ident cn ident fs just FS - { out "MOR" $4; $6 @ mk_morphism (trim $4) } - | xlet ident opt_lskips def xskips FS - { out "TH" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident lskips fs just FS - { out "TH" $2; - $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | var idents cn xskips FS - { out "VAR" (cat $2); mk_vars true $2 } - | ax idents cn xskips FS - { out "AX" (cat $2); mk_vars false $2 } - | ind ident skips FS - { out "IND" $2; - T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 - } - | sec ident FS - { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } - | xend ident FS - { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } - | unx xskips FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | req xp ident FS - { out "REQ" $3; [T.Include (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 skips FS - { out "COERCE" (hd $2); coercion (hd $2) } - | id coerc qid spcs skips FS - { out "COERCE" (hd $3); coercion (hd $3) } - | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | var idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - | ax idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - ; - -/* VERNACULAR ITEMS *********************************************************/ - - item: - | OQ verbatims CQ { [T.Comment $2] } - | macro_step { $1 } - | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) } - | error { out "ERROR" "item"; failwith "item" } - ; - items: - | rspcs EOF { [] } - | rspcs item items { $2 @ $3 } - ; - - -/* - oc: OC spcs { $1 ^ $2 }; - coe: COE spcs { $1 ^ $2 }; - sc: SC spcs { $1 ^ $2 }; - - cnot: - | EXTRA { $1 } - | INT { $1 } - ; - cnots: - | cnot spcs { $1 ^ $2 } - | cnot spcs cnots { $1 ^ $2 ^ $3 } - ; - - xstrict: - | AC { $1 } - | INT { $1 } - | EXTRA { $1 } - | CN { $1 } - | SC { $1 } - | OC { $1 } - | CC { $1 } - | COE { $1 } - | STR { $1 } - | abbr extends0 IN { $1 ^ $2 ^ $3 } - | op extends1 CP { $1 ^ $2 ^ $3 } - ; - strict: - | xstrict { $1 } - | IDENT { $1 } - | SET { $1 } - | NOT { $1 } - ; - restrict: - | strict { $1 } - | IN { $1 } - | CP { $1 } - ; - xre: - | xstrict { $1 } - | IN { $1 } - | CP { $1 } - ; - restricts: - | restrict spcs { $1 ^ $2 } - | restrict spcs restricts { $1 ^ $2 ^ $3 } - ; - xres: - | xre spcs { $1 ^ $2 } - | xre spcs restricts { $1 ^ $2 ^ $3 } - ; - extend0: - | strict { $1 } - | DEF { $1 } - ; - extends0: - | extend0 spcs { $1 ^ $2 } - | extend0 spcs extends0 { $1 ^ $2 ^ $3 } - ; - extend1: - | strict { $1 } - | DEF { $1 } - | IN { $1 } - ; - extends1: - | extend1 spcs { $1 ^ $2 } - | extend1 spcs extends1 { $1 ^ $2 ^ $3 } - ; - unexport_ff: - | IDENT { $1 } - | AC { $1 } - | STR { $1 } - | OP { $1 } - | ABBR { $1 } - | IN { $1 } - | CP { $1 } - | SET { $1 } - ; - unexport_rr: - | unexport_ff { $1 } - | INT { $1 } - | EXTRA { $1 } - | CN { $1 } - | COE { $1 } - | DEF { $1 } - ; - unexport_r: - | unexport_rr { $1, [] } - | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 } - | oc unexport_ff CC { $1, [] } - ; - unexports_r: - | unexport_r spcs { fst $1 ^ $2, snd $1 } - | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - field: - | ident cn unexports_r - { $1 ^ $2 ^ fst $3, snd $3 } - | ident def unexports_r - { $1 ^ $2 ^ fst $3, snd $3 } - | ident coe unexports_r - { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) } - ; - fields: - | field { $1 } - | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - | cnots { $1, [] } - | error { out "ERROR" "fields"; failwith "fields" } - ; - unexport: - | unexport_r { $1 } - | SC { $1, [] } - | CC { $1, [] } - | IP { $1, [] } - | LET { $1, [] } - | VAR { $1, [] } - - ; - unexports: - | unexport spcs { fst $1 ^ $2, snd $1 } - | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 } - ; - verbatim: - | unexport_rr { $1 } - | reserved_ident { $1 } - | comment { $1 } - | OC { $1 } - | CC { $1 } - | SC { $1 } - | XP { $1 } - | IP { $1 } - | FS { $1 } - | SPC { $1 } - ; - verbatims: - | { "" } - | verbatim verbatims { $1 ^ $2 } - ; - step: - | macro_step { $1 } - | restricts FS { [] } - ; - steps: - | step spcs { [] } - | step spcs steps { $1 @ $3 } - ; - - macro_step: - | th ident restricts fs proof FS steps qed FS - { out "TH" $2; - $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts fs proof restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts fs steps qed FS - { out "TH" $2; - $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident restricts def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | th ident def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | gen ident def restricts FS - { out "TH" $2; - [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs proof FS steps qed FS - { out "LET" $2; - $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs proof restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts fs steps qed FS - { out "LET" $2; - $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident restricts def restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | xlet ident def restricts FS - { out "LET" $2; - [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)] - } - | var idents xres FS - { out "VAR" (cat $2); mk_vars true $2 } - | ax idents xres FS - { out "AX" (cat $2); mk_vars false $2 } - | ind ident unexports FS - { out "IND" $2; - T.Inline (false, T.Ind, trim $2, "", None) :: snd $3 - } - | sec ident FS - { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] } - | xend ident FS - { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] } - | unx unexports FS - { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | req xp ident FS - { out "REQ" $3; [T.Include (trim $3)] } - | req ip ident FS - { out "REQ" $3; [T.Include (trim $3)] } - | req ident FS - { out "REQ" $2; [T.Include (trim $2)] } - | load str FS - { out "REQ" $2; [T.Include (strip2 (trim $2))] } - | coerc qid spcs cn unexports FS - { out "COERCE" (hd $2); coercion (hd $2) } - | id coerc qid spcs cn unexports FS - { out "COERCE" (hd $3); coercion (hd $3) } - | th ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | ind ident error - { out "ERROR" $2; failwith ("macro_step " ^ $2) } - | var idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - | ax idents error - { let vs = cat $2 in - out "ERROR" vs; failwith ("macro_step " ^ vs) } - ; - item: - | OQ verbatims CQ { [T.Comment $2] } - | macro_step { $1 } - | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] } - | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) } - | error { out "ERROR" "item"; failwith "item" } - ; - items: - | rspcs EOF { [] } - | rspcs item items { $2 @ $3 } - ; -*/ diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 70b82092c..0040d7ebf 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -462,26 +462,8 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: in PET.mk_tactic (letin_tac ~mk_fresh_name_callback term) - (** functional part of the "exact" tactic *) -let exact_tac ~term = - let exact_tac ~term (proof, goal) = - (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_subst,_,_, _) = proof in - let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let module T = CicTypeChecker in - let module R = CicReduction in - let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in - let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *) - if b then - begin - let (newproof, metasenv') = - ProofEngineHelpers.subst_meta_in_proof proof metano term [] in - (newproof, []) - end - else - raise (PET.Fail (lazy "The type of the provided term is not the one expected.")) - in - PET.mk_tactic (exact_tac ~term) +(* FG: exact_tac := apply_tac as in NTactics *) +let exact_tac ~term = apply_tac ~term (* not really "primitive" tactics .... *) diff --git a/helm/software/matita/contribs/procedural/library/Makefile b/helm/software/matita/contribs/procedural/library/Makefile new file mode 100644 index 000000000..bd75dbd6d --- /dev/null +++ b/helm/software/matita/contribs/procedural/library/Makefile @@ -0,0 +1,3 @@ +DEVEL = library + +include ../Makefile.common diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml new file mode 100644 index 000000000..8165072d9 --- /dev/null +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -0,0 +1,13 @@ + + +
+ library + library + cic:/matita + cic:/matita/procedural/library + library + contribs/procedural/library + grafite + procedural +
+ diff --git a/helm/software/matita/contribs/procedural/library/preamble.ma b/helm/software/matita/contribs/procedural/library/preamble.ma new file mode 100644 index 000000000..89ee1a360 --- /dev/null +++ b/helm/software/matita/contribs/procedural/library/preamble.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* + +default "equality" + cic:/Coq/Init/Logic/eq.ind + cic:/Coq/Init/Logic/sym_eq.con + cic:/Coq/Init/Logic/trans_eq.con + cic:/Coq/Init/Logic/eq_ind.con + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con + cic:/Coq/Init/Logic/f_equal.con + cic:/matita/procedural/Coq/preamble/f_equal1.con. + +default "true" + cic:/Coq/Init/Logic/True.ind. +default "false" + cic:/Coq/Init/Logic/False.ind. +default "absurd" + cic:/Coq/Init/Logic/absurd.con. + +interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y). + +theorem f_equal1 : \forall A,B:Type.\forall f:A\to B.\forall x,y:A. + x = y \to (f y) = (f x). + intros. + symmetry. + apply cic:/Coq/Init/Logic/f_equal.con. + assumption. +qed. + +alias id "land" = "cic:/matita/procedural/Coq/Init/Logic/and.ind#xpointer(1/1)". + +*) diff --git a/helm/software/matita/contribs/procedural/library/root b/helm/software/matita/contribs/procedural/library/root new file mode 100644 index 000000000..0b7bcc5ca --- /dev/null +++ b/helm/software/matita/contribs/procedural/library/root @@ -0,0 +1 @@ +baseuri=cic:/matita/procedural/library