From 3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 14 Apr 2009 20:06:32 +0000 Subject: [PATCH] - 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" --- .../components/acic_procedural/procedural1.ml | 20 +-- .../acic_procedural/proceduralTypes.ml | 17 ++- .../components/binaries/transcript/.depend | 28 ++-- .../binaries/transcript/.depend.opt | 28 ++-- .../components/binaries/transcript/Makefile | 10 +- .../components/binaries/transcript/engine.ml | 37 +++-- .../{v8Lexer.mll => gallina8Lexer.mll} | 29 +++- .../{v8Parser.mly => gallina8Parser.mly} | 0 .../binaries/transcript/grafiteLexer.mll | 75 ++++++++++ .../binaries/transcript/grafiteParser.mly | 141 ++++++++++++++++++ .../components/binaries/transcript/types.ml | 2 + .../components/syntax_extensions/.depend | 3 - .../components/tactics/primitiveTactics.ml | 22 +-- .../contribs/procedural/library/Makefile | 3 + .../procedural/library/library.conf.xml | 13 ++ .../contribs/procedural/library/preamble.ma | 49 ++++++ .../matita/contribs/procedural/library/root | 1 + 17 files changed, 398 insertions(+), 80 deletions(-) rename helm/software/components/binaries/transcript/{v8Lexer.mll => gallina8Lexer.mll} (86%) rename helm/software/components/binaries/transcript/{v8Parser.mly => gallina8Parser.mly} (100%) create mode 100644 helm/software/components/binaries/transcript/grafiteLexer.mll create mode 100644 helm/software/components/binaries/transcript/grafiteParser.mly create mode 100644 helm/software/matita/contribs/procedural/library/Makefile create mode 100644 helm/software/matita/contribs/procedural/library/library.conf.xml create mode 100644 helm/software/matita/contribs/procedural/library/preamble.ma create mode 100644 helm/software/matita/contribs/procedural/library/root 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/v8Lexer.mll b/helm/software/components/binaries/transcript/gallina8Lexer.mll similarity index 86% rename from helm/software/components/binaries/transcript/v8Lexer.mll rename to helm/software/components/binaries/transcript/gallina8Lexer.mll index 0ef38a919..586bab472 100644 --- a/helm/software/components/binaries/transcript/v8Lexer.mll +++ b/helm/software/components/binaries/transcript/gallina8Lexer.mll @@ -1,7 +1,32 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + { module O = Options - module P = V8Parser - + module P = Gallina8Parser + let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s) let check s = diff --git a/helm/software/components/binaries/transcript/v8Parser.mly b/helm/software/components/binaries/transcript/gallina8Parser.mly similarity index 100% rename from helm/software/components/binaries/transcript/v8Parser.mly rename to helm/software/components/binaries/transcript/gallina8Parser.mly 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/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 -- 2.39.2