From: Claudio Sacerdoti Coen Date: Mon, 5 Dec 2005 14:09:31 +0000 (+0000) Subject: 1. Several files in grafite that should be in grafite_parser moved there. X-Git-Tag: make_still_working~8047 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a696aae5ea794cd43fd3d83d37a0345d2a1387b3;p=helm.git 1. Several files in grafite that should be in grafite_parser moved there. 2. grafiteEngine is now generalized over the function baseuri_of_script (that associates the baseuri to a .ma file). This function is used to execute the Include statement. However, it seems to me that this shows a problem in the architecture (since the only possible implementation of the function involves using the grafie_parser right now). Modified Files in ocaml: METAS/meta.helm-grafite_parser.src grafite/.depend grafite/Makefile grafite/cicNotation.ml grafite/cicNotation.mli grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite_parser/.depend grafite_parser/Makefile Modified Files in matita: matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml Added Files in ocaml: grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli grafite_parser/grafiteParser.ml grafite_parser/grafiteParser.mli grafite_parser/grafiteParserMisc.ml grafite_parser/grafiteParserMisc.mli grafite_parser/print_grammar.ml grafite_parser/test_dep.ml grafite_parser/test_parser.ml Removed Files in ocaml: grafite/grafiteParser.ml grafite/grafiteParser.mli grafite/print_grammar.ml grafite/test_dep.ml grafite/test_parser.ml --- diff --git a/helm/ocaml/METAS/meta.helm-grafite_parser.src b/helm/ocaml/METAS/meta.helm-grafite_parser.src index 389007b5b..cba4c171b 100644 --- a/helm/ocaml/METAS/meta.helm-grafite_parser.src +++ b/helm/ocaml/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-grafite2" +requires="helm-grafite2 ulex" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/helm/ocaml/grafite/.depend b/helm/ocaml/grafite/.depend index c5774b069..a6c70afc7 100644 --- a/helm/ocaml/grafite/.depend +++ b/helm/ocaml/grafite/.depend @@ -1,12 +1,9 @@ grafiteAstPp.cmi: grafiteAst.cmo -grafiteParser.cmi: grafiteAst.cmo cicNotation.cmi: grafiteAst.cmo grafiteMarshal.cmi: grafiteAst.cmo grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi -grafiteParser.cmo: grafiteAst.cmo grafiteParser.cmi -grafiteParser.cmx: grafiteAst.cmx grafiteParser.cmi -cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotation.cmi -cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotation.cmi -grafiteMarshal.cmo: grafiteAst.cmo grafiteMarshal.cmi -grafiteMarshal.cmx: grafiteAst.cmx grafiteMarshal.cmi +cicNotation.cmo: grafiteAst.cmo cicNotation.cmi +cicNotation.cmx: grafiteAst.cmx cicNotation.cmi +grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmo grafiteMarshal.cmi +grafiteMarshal.cmx: grafiteAstPp.cmx grafiteAst.cmx grafiteMarshal.cmi diff --git a/helm/ocaml/grafite/Makefile b/helm/ocaml/grafite/Makefile index 0ce510b20..b16d7b7dd 100644 --- a/helm/ocaml/grafite/Makefile +++ b/helm/ocaml/grafite/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ grafiteAstPp.mli \ - grafiteParser.mli \ cicNotation.mli \ grafiteMarshal.mli \ $(NULL) @@ -11,47 +10,5 @@ IMPLEMENTATION_FILES = \ grafiteAst.ml \ $(INTERFACE_FILES:%.mli=%.ml) -all: test_parser print_grammar test_dep -clean: clean_tests - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# -# -grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) -grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) - -clean_tests: - rm -f test_parser{,.opt} test_dep{,.opt} print_grammar{,.opt} - -LOCAL_LINKOPTS = -package helm-grafite -linkpkg -test: test_parser print_grammar test_dep -test_parser: test_parser.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -print_grammar: print_grammar.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -test_dep: test_dep.ml $(PACKAGE).cma - $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< include ../Makefile.common - -# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as -# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by -# "_loc" occurrences -UTF8DIR := $(shell $(OCAMLFIND) query helm-utf8_macros) -ULEXDIR := $(shell $(OCAMLFIND) query ulex) -MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" -cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) -# - diff --git a/helm/ocaml/grafite/cicNotation.ml b/helm/ocaml/grafite/cicNotation.ml index 30dd5f4d1..9500a8e11 100644 --- a/helm/ocaml/grafite/cicNotation.ml +++ b/helm/ocaml/grafite/cicNotation.ml @@ -61,17 +61,6 @@ let remove_notation = function | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id | InterpretationId id -> TermAcicContent.remove_interpretation id -let load_notation fname = - let ic = open_in fname in - let lexbuf = Ulexing.from_utf8_channel ic in - try - while true do - match GrafiteParser.parse_statement lexbuf with - | Executable (_, Command (_, cmd)) -> ignore (process_notation cmd) - | _ -> () - done - with End_of_file -> close_in ic - let get_all_notations () = List.map (fun (interp_id, dsc) -> diff --git a/helm/ocaml/grafite/cicNotation.mli b/helm/ocaml/grafite/cicNotation.mli index 1c6e95385..41b775562 100644 --- a/helm/ocaml/grafite/cicNotation.mli +++ b/helm/ocaml/grafite/cicNotation.mli @@ -30,9 +30,6 @@ val process_notation: val remove_notation: notation_id -> unit -(** @param fname file from which load notation *) -val load_notation: string -> unit - (** {2 Notation enabling/disabling} * Right now, only disabling of notation during pretty printing is supporting. * If it is useful to disable it also for the input phase is still to be diff --git a/helm/ocaml/grafite/grafiteParser.ml b/helm/ocaml/grafite/grafiteParser.ml deleted file mode 100644 index 64db52295..000000000 --- a/helm/ocaml/grafite/grafiteParser.ml +++ /dev/null @@ -1,555 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -open Printf - -module Ast = CicNotationPt - -type statement = - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) - GrafiteAst.statement - -let grammar = CicNotationParser.level2_ast_grammar - -let term = CicNotationParser.term -let statement = Grammar.Entry.create grammar "statement" - -let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) - -let default_precedence = 50 -let default_associativity = Gramext.NonA - -EXTEND - GLOBAL: term statement; - arg: [ - [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; - SYMBOL ":"; ty = term; RPAREN -> names,ty - | name = IDENT -> [name],Ast.Implicit - ] - ]; - constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; - tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; - ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ]; - tactic_term_list1: [ - [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] - ]; - reduction_kind: [ - [ IDENT "normalize" -> `Normalize - | IDENT "reduce" -> `Reduce - | IDENT "simplify" -> `Simpl - | IDENT "unfold"; t = OPT term -> `Unfold t - | IDENT "whd" -> `Whd ] - ]; - sequent_pattern_spec: [ - [ hyp_paths = - LIST0 - [ id = IDENT ; - path = OPT [SYMBOL ":" ; path = tactic_term -> path ] -> - (id,match path with Some p -> p | None -> Ast.UserInput) ]; - goal_path = OPT [ SYMBOL <:unicode>; term = tactic_term -> term ] -> - let goal_path = - match goal_path, hyp_paths with - None, [] -> Ast.UserInput - | None, _::_ -> Ast.Implicit - | Some goal_path, _ -> goal_path - in - hyp_paths,goal_path - ] - ]; - pattern_spec: [ - [ res = OPT [ - "in"; - wanted_and_sps = - [ "match" ; wanted = tactic_term ; - sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> - Some wanted,sps - | sps = sequent_pattern_spec -> - None,Some sps - ] -> - let wanted,hyp_paths,goal_path = - match wanted_and_sps with - wanted,None -> wanted, [], Ast.UserInput - | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path - in - wanted, hyp_paths, goal_path ] -> - match res with - None -> None,[],Ast.UserInput - | Some ps -> ps] - ]; - direction: [ - [ SYMBOL ">" -> `LeftToRight - | SYMBOL "<" -> `RightToLeft ] - ]; - int: [ [ num = NUMBER -> int_of_string num ] ]; - intros_spec: [ - [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - num, idents - ] - ]; - using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; - tactic: [ - [ IDENT "absurd"; t = tactic_term -> - GrafiteAst.Absurd (loc, t) - | IDENT "apply"; t = tactic_term -> - GrafiteAst.Apply (loc, t) - | IDENT "assumption" -> - GrafiteAst.Assumption loc - | IDENT "auto"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; - paramodulation = OPT [ IDENT "paramodulation" ]; - full = OPT [ IDENT "full" ] -> (* ALB *) - GrafiteAst.Auto (loc,depth,width,paramodulation,full) - | IDENT "clear"; id = IDENT -> - GrafiteAst.Clear (loc,id) - | IDENT "clearbody"; id = IDENT -> - GrafiteAst.ClearBody (loc,id) - | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> - GrafiteAst.Change (loc, what, t) - | IDENT "compare"; t = tactic_term -> - GrafiteAst.Compare (loc,t) - | IDENT "constructor"; n = int -> - GrafiteAst.Constructor (loc, n) - | IDENT "contradiction" -> - GrafiteAst.Contradiction loc - | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> - GrafiteAst.Cut (loc, ident, t) - | IDENT "decide"; IDENT "equality" -> - GrafiteAst.DecideEquality loc - | IDENT "decompose"; types = OPT ident_list0; what = IDENT; - (num, idents) = intros_spec -> - let types = match types with None -> [] | Some types -> types in - let to_spec id = GrafiteAst.Ident id in - GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) - | IDENT "discriminate"; t = tactic_term -> - GrafiteAst.Discriminate (loc, t) - | IDENT "elim"; what = tactic_term; using = using; - (num, idents) = intros_spec -> - GrafiteAst.Elim (loc, what, using, num, idents) - | IDENT "elimType"; what = tactic_term; using = using; - (num, idents) = intros_spec -> - GrafiteAst.ElimType (loc, what, using, num, idents) - | IDENT "exact"; t = tactic_term -> - GrafiteAst.Exact (loc, t) - | IDENT "exists" -> - GrafiteAst.Exists loc - | IDENT "fail" -> GrafiteAst.Fail loc - | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> - let (pt,_,_) = p in - if pt <> None then - raise (HExtlib.Localized (loc, CicNotationParser.Parse_error - ("the pattern cannot specify the term to replace, only its" - ^ " paths in the hypotheses and in the conclusion"))) - else - GrafiteAst.Fold (loc, kind, t, p) - | IDENT "fourier" -> - GrafiteAst.Fourier loc - | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - GrafiteAst.FwdSimpl (loc, hyp, idents) - | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> - GrafiteAst.Generalize (loc,p,id) - | IDENT "goal"; n = int -> - GrafiteAst.Goal (loc, n) - | IDENT "id" -> GrafiteAst.IdTac loc - | IDENT "injection"; t = tactic_term -> - GrafiteAst.Injection (loc, t) - | IDENT "intro"; ident = OPT IDENT -> - let idents = match ident with None -> [] | Some id -> [id] in - GrafiteAst.Intros (loc, Some 1, idents) - | IDENT "intros"; (num, idents) = intros_spec -> - GrafiteAst.Intros (loc, num, idents) - | IDENT "lapply"; - depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; - what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; - ident = OPT [ IDENT "using" ; ident = IDENT -> ident ] -> - let to_what = match to_what with None -> [] | Some to_what -> to_what in - GrafiteAst.LApply (loc, depth, to_what, what, ident) - | IDENT "left" -> GrafiteAst.Left loc - | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> - GrafiteAst.LetIn (loc, t, where) - | kind = reduction_kind; p = pattern_spec -> - GrafiteAst.Reduce (loc, kind, p) - | IDENT "reflexivity" -> - GrafiteAst.Reflexivity loc - | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> - GrafiteAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> - let (pt,_,_) = p in - if pt <> None then - raise - (HExtlib.Localized (loc, - (CicNotationParser.Parse_error - "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) - else - GrafiteAst.Rewrite (loc, d, t, p) - | IDENT "right" -> - GrafiteAst.Right loc - | IDENT "ring" -> - GrafiteAst.Ring loc - | IDENT "split" -> - GrafiteAst.Split loc - | IDENT "symmetry" -> - GrafiteAst.Symmetry loc - | IDENT "transitivity"; t = tactic_term -> - GrafiteAst.Transitivity (loc, t) - ] - ]; - atomic_tactical: - [ "sequence" LEFTA - [ t1 = SELF; SYMBOL ";"; t2 = SELF -> - let ts = - match t1 with - | GrafiteAst.Seq (_, l) -> l @ [ t2 ] - | _ -> [ t1; t2 ] - in - GrafiteAst.Seq (loc, ts) - ] - | "then" NONA - [ tac = SELF; SYMBOL ";"; - SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> - (GrafiteAst.Then (loc, tac, tacs)) - ] - | "loops" RIGHTA - [ IDENT "do"; count = int; tac = SELF; IDENT "end" -> - GrafiteAst.Do (loc, count, tac) - | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac) - ] - | "simple" NONA - [ IDENT "first"; - SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> - GrafiteAst.First (loc, tacs) - | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac) - | IDENT "solve"; - SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> - GrafiteAst.Solve (loc, tacs) - | LPAREN; tac = SELF; RPAREN -> tac - | tac = tactic -> GrafiteAst.Tactic (loc, tac) - ] - ]; - punctuation_tactical: - [ - [ SYMBOL "[" -> GrafiteAst.Branch loc - | SYMBOL "|" -> GrafiteAst.Shift loc - | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i) - | SYMBOL "]" -> GrafiteAst.Merge loc - | SYMBOL ";" -> GrafiteAst.Semicolon loc - | SYMBOL "." -> GrafiteAst.Dot loc - ] - ]; - tactical: - [ "simple" NONA - [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals) - | IDENT "unfocus" -> GrafiteAst.Unfocus loc - | IDENT "skip" -> GrafiteAst.Skip loc - | tac = atomic_tactical LEVEL "loops" -> tac - ] - ]; - theorem_flavour: [ - [ [ IDENT "definition" ] -> `Definition - | [ IDENT "fact" ] -> `Fact - | [ IDENT "lemma" ] -> `Lemma - | [ IDENT "remark" ] -> `Remark - | [ IDENT "theorem" ] -> `Theorem - ] - ]; - inductive_spec: [ [ - fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; - SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; - fst_constructors = LIST0 constructor SEP SYMBOL "|"; - tl = OPT [ "with"; - types = LIST1 [ - name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; - OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> - (name, true, typ, constructors) ] SEP "with" -> types - ] -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in - let tl_ind_types = match tl with None -> [] | Some types -> types in - let ind_types = fst_ind_type :: tl_ind_types in - (params, ind_types) - ] ]; - - record_spec: [ [ - name = IDENT; params = LIST0 [ arg = arg -> arg ] ; - SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; - fields = LIST0 [ - name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) - ] SEP SYMBOL ";"; SYMBOL "}" -> - let params = - List.fold_right - (fun (names, typ) acc -> - (List.map (fun name -> (name, typ)) names) @ acc) - params [] - in - (params,name,typ,fields) - ] ]; - - macro: [ - [ [ IDENT "quit" ] -> GrafiteAst.Quit loc -(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *) -(* | [ IDENT "undo" ]; steps = OPT NUMBER -> - GrafiteAst.Undo (loc, int_opt steps) - | [ IDENT "redo" ]; steps = OPT NUMBER -> - GrafiteAst.Redo (loc, int_opt steps) *) - | [ IDENT "check" ]; t = term -> - GrafiteAst.Check (loc, t) - | [ IDENT "hint" ] -> GrafiteAst.Hint loc - | [ IDENT "whelp"; "match" ] ; t = term -> - GrafiteAst.WMatch (loc,t) - | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> - GrafiteAst.WInstance (loc,t) - | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> - GrafiteAst.WLocate (loc,id) - | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> - GrafiteAst.WElim (loc, t) - | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> - GrafiteAst.WHint (loc,t) - | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) - ] - ]; - alias_spec: [ - [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> - let alpha = "[a-zA-Z]" in - let num = "[0-9]+" in - let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in - let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in - let rex = Str.regexp ("^"^ident^"$") in - if Str.string_match rex id 0 then - if (try ignore (UriManager.uri_of_string uri); true - with UriManager.IllFormedUri _ -> false) - then - GrafiteAst.Ident_alias (id, uri) - else - raise - (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) - else - raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( - sprintf "Not a valid identifier: %s" id))) - | IDENT "symbol"; symbol = QSTRING; - instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> i | None -> 0 - in - GrafiteAst.Symbol_alias (symbol, instance, dsc) - | IDENT "num"; - instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; - SYMBOL "="; dsc = QSTRING -> - let instance = - match instance with Some i -> i | None -> 0 - in - GrafiteAst.Number_alias (instance, dsc) - ] - ]; - argument: [ - [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; - id = IDENT -> - Ast.IdentArg (List.length l, id) - ] - ]; - associativity: [ - [ IDENT "left"; IDENT "associative" -> Gramext.LeftA - | IDENT "right"; IDENT "associative" -> Gramext.RightA - | IDENT "non"; IDENT "associative" -> Gramext.NonA - ] - ]; - precedence: [ - [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] - ]; - notation: [ - [ dir = OPT direction; s = QSTRING; - assoc = OPT associativity; prec = OPT precedence; - IDENT "for"; - p2 = - [ blob = UNPARSED_AST -> - add_raw_attribute ~text:(sprintf "@{%s}" blob) - (CicNotationParser.parse_level2_ast - (Ulexing.from_utf8_string blob)) - | blob = UNPARSED_META -> - add_raw_attribute ~text:(sprintf "${%s}" blob) - (CicNotationParser.parse_level2_meta - (Ulexing.from_utf8_string blob)) - ] -> - let assoc = - match assoc with - | None -> default_associativity - | Some assoc -> assoc - in - let prec = - match prec with - | None -> default_precedence - | Some prec -> prec - in - let p1 = - add_raw_attribute ~text:s - (CicNotationParser.parse_level1_pattern - (Ulexing.from_utf8_string s)) - in - (dir, p1, assoc, prec, p2) - ] - ]; - level3_term: [ - [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u) - | id = IDENT -> Ast.VarPattern id - | SYMBOL "_" -> Ast.ImplicitPattern - | LPAREN; terms = LIST1 SELF; RPAREN -> - (match terms with - | [] -> assert false - | [term] -> term - | terms -> Ast.ApplPattern terms) - ] - ]; - interpretation: [ - [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> - (s, args, t) - ] - ]; - command: [ [ - IDENT "set"; n = QSTRING; v = QSTRING -> - GrafiteAst.Set (loc, n, v) - | IDENT "drop" -> GrafiteAst.Drop loc - | IDENT "qed" -> GrafiteAst.Qed loc - | IDENT "variant" ; name = IDENT; SYMBOL ":"; - typ = term; SYMBOL <:unicode> ; newname = IDENT -> - GrafiteAst.Obj (loc, - Ast.Theorem - (`Variant,name,typ,Some (Ast.Ident (newname, None)))) - | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body)) - | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); - body = term -> - GrafiteAst.Obj (loc, - Ast.Theorem (flavour, name, Ast.Implicit, Some body)) - | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = CicNotationParser.let_defs -> - let name,ty = - match defs with - | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty - | ((Ast.Ident (name, None), None),_,_) :: _ -> - name, Ast.Implicit - | _ -> assert false - in - let body = Ast.Ident (name,None) in - GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty, - Some (Ast.LetRec (ind_kind, defs, body)))) - | IDENT "inductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coinductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - let ind_types = (* set inductive flags to false (coinductive) *) - List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) - ind_types - in - GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) - | IDENT "coercion" ; name = IDENT -> - GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true) - | IDENT "coercion" ; name = URI -> - GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true) - | IDENT "alias" ; spec = alias_spec -> - GrafiteAst.Alias (loc, spec) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> - GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) - | IDENT "include" ; path = QSTRING -> - GrafiteAst.Include (loc,path) - | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> - let uris = List.map UriManager.uri_of_string uris in - GrafiteAst.Default (loc,what,uris) - | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation -> - GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2) - | IDENT "interpretation"; id = QSTRING; - (symbol, args, l3) = interpretation -> - GrafiteAst.Interpretation (loc, id, (symbol, args), l3) - - | IDENT "dump" -> GrafiteAst.Dump loc - | IDENT "render"; u = URI -> - GrafiteAst.Render (loc, UriManager.uri_of_string u) - ]]; - executable: [ - [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) - | tac = tactical; punct = punctuation_tactical -> - GrafiteAst.Tactical (loc, tac, Some punct) - | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) - | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) - ] - ]; - comment: [ - [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> - GrafiteAst.Code (loc, ex) - | str = NOTE -> - GrafiteAst.Note (loc, str) - ] - ]; - statement: [ - [ ex = executable -> GrafiteAst.Executable (loc,ex) - | com = comment -> GrafiteAst.Comment (loc, com) - | EOI -> raise End_of_file - ] - ]; -END - -let exc_located_wrapper f = - try - f () - with - | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file - | Stdpp.Exc_located (floc, Stream.Error msg) -> - raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg)) - | Stdpp.Exc_located (floc, exn) -> - raise - (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) - -let parse_statement lexbuf = - exc_located_wrapper - (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf))) - -let parse_dependencies lexbuf = - let tok_stream,_ = - CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) - in - let rec parse acc = - (parser - | [< '("URI", u) >] -> - parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc) - | [< '("IDENT", "include"); '("QSTRING", fname) >] -> - parse (GrafiteAst.IncludeDep fname :: acc) - | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] -> - parse (GrafiteAst.BaseuriDep baseuri :: acc) - | [< '("EOI", _) >] -> acc - | [< 'tok >] -> parse acc - | [< >] -> acc) tok_stream - in - List.rev (parse []) - diff --git a/helm/ocaml/grafite/grafiteParser.mli b/helm/ocaml/grafite/grafiteParser.mli deleted file mode 100644 index 7b33c6e42..000000000 --- a/helm/ocaml/grafite/grafiteParser.mli +++ /dev/null @@ -1,37 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -type statement = - (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.obj, string) - GrafiteAst.statement - -val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) - - (** @raise End_of_file *) -val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list - -val statement: statement Grammar.Entry.e - diff --git a/helm/ocaml/grafite/print_grammar.ml b/helm/ocaml/grafite/print_grammar.ml deleted file mode 100644 index d7d6f3c96..000000000 --- a/helm/ocaml/grafite/print_grammar.ml +++ /dev/null @@ -1,285 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -open Gramext - -let tex_of_unicode s = - let contractions = ("\\Longrightarrow","=>") :: [] in - if String.length s <= 1 then s - else (* probably an extended unicode symbol *) - let s = Utf8Macro.tex_of_unicode s in - try List.assoc s contractions with Not_found -> s - -let needs_brackets t = - let rec count_brothers = function - | Node {brother = brother} -> 1 + count_brothers brother - | _ -> 0 - in - count_brothers t > 1 - -let visit_description desc fmt self = - let skip s = List.mem s [ ] in - let inline s = List.mem s [ "int" ] in - - let rec visit_entry e todo is_son nesting = - let { ename = ename; edesc = desc } = e in - if inline ename then - visit_desc desc todo is_son nesting - else - begin - Format.fprintf fmt "%s " ename; - if skip ename then - todo - else - todo @ [e] - end - - and visit_desc d todo is_son nesting = - match d with - | Dlevels [] -> todo - | Dlevels [lev] -> visit_level lev todo is_son nesting - | Dlevels (lev::levels) -> - let todo = visit_level lev todo is_son nesting in - List.fold_left - (fun acc l -> - Format.fprintf fmt "@ | "; - visit_level l acc is_son nesting) - todo levels; - | _ -> todo - - and visit_level l todo is_son nesting = - let { lsuffix = suff ; lprefix = pref } = l in - let todo = visit_tree suff todo is_son nesting in - visit_tree pref todo is_son nesting - - and visit_tree t todo is_son nesting = - match t with - | Node node -> visit_node node todo is_son nesting - | _ -> todo - - and visit_node n todo is_son nesting = - let is_tree_printable t = - match t with - | Node _ -> true - | _ -> false - in - let { node = symbol; son = son ; brother = brother } = n in - let todo = visit_symbol symbol todo is_son nesting in - let todo = - if is_tree_printable son then - begin - let need_b = needs_brackets son in - if not is_son then - Format.fprintf fmt "@["; - if need_b then - Format.fprintf fmt "( "; - let todo = visit_tree son todo true nesting in - if need_b then - Format.fprintf fmt ")"; - if not is_son then - Format.fprintf fmt "@]"; - todo - end - else - todo - in - if is_tree_printable brother then - begin - Format.fprintf fmt "@ | "; - visit_tree brother todo is_son nesting - end - else - todo - - and visit_symbol s todo is_son nesting = - match s with - | Smeta (name, sl, _) -> - Format.fprintf fmt "%s " name; - List.fold_left ( - fun acc s -> - let todo = visit_symbol s acc is_son nesting in - if is_son then - Format.fprintf fmt "@ "; - todo) - todo sl - | Snterm entry -> visit_entry entry todo is_son nesting - | Snterml (entry,_) -> visit_entry entry todo is_son nesting - | Slist0 symbol -> - Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting+1) in - Format.fprintf fmt "@]} @ "; - todo - | Slist0sep (symbol,sep) -> - Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son (nesting + 2) in - Format.fprintf fmt " "; - let todo = visit_symbol symbol todo is_son (nesting + 2) in - Format.fprintf fmt "@]} @]] @ "; - todo - | Slist1 symbol -> - Format.fprintf fmt "{@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "@]}+ @ "; - todo - | Slist1sep (symbol,sep) -> - let todo = visit_symbol symbol todo is_son nesting in - Format.fprintf fmt "{@[ "; - let todo = visit_symbol sep todo is_son (nesting + 1) in - let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "@]} @ "; - todo - | Sopt symbol -> - Format.fprintf fmt "[@[ "; - let todo = visit_symbol symbol todo is_son (nesting + 1) in - Format.fprintf fmt "@]] @ "; - todo - | Sself -> Format.fprintf fmt "%s " self; todo - | Snext -> Format.fprintf fmt "next "; todo - | Stoken pattern -> - let constructor, keyword = pattern in - if keyword = "" then - Format.fprintf fmt "`%s' " constructor - else - Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); - todo - | Stree tree -> - if needs_brackets tree then - begin - Format.fprintf fmt "@[( "; - let todo = visit_tree tree todo is_son (nesting + 1) in - Format.fprintf fmt ")@] @ "; - todo - end - else - visit_tree tree todo is_son (nesting + 1) - in - visit_desc desc [] false 0 -;; - -let rec clean_dummy_desc = function - | Dlevels l -> Dlevels (clean_levels l) - | x -> x - -and clean_levels = function - | [] -> [] - | l :: tl -> clean_level l @ clean_levels tl - -and clean_level = function - | x -> - let pref = clean_tree x.lprefix in - let suff = clean_tree x.lsuffix in - match pref,suff with - | DeadEnd, DeadEnd -> [] - | _ -> [{x with lprefix = pref; lsuffix = suff}] - -and clean_tree = function - | Node n -> clean_node n - | x -> x - -and clean_node = function - | {node=node;son=son;brother=brother} -> - let bn = is_symbol_dummy node in - let bs = is_tree_dummy son in - let bb = is_tree_dummy brother in - let son = if bs then DeadEnd else son in - let brother = if bb then DeadEnd else brother in - if bb && bs && bn then - DeadEnd - else - if bn then - Node {node=Sself;son=son;brother=brother} - else - Node {node=node;son=son;brother=brother} - -and is_level_dummy = function - | {lsuffix=lsuffix;lprefix=lprefix} -> - is_tree_dummy lsuffix && is_tree_dummy lprefix - -and is_desc_dummy = function - | Dlevels l -> List.for_all is_level_dummy l - | Dparser _ -> true - -and is_entry_dummy = function - | {edesc=edesc} -> is_desc_dummy edesc - -and is_symbol_dummy = function - | Stoken ("DUMMY", _) -> true - | Stoken _ -> false - | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt - | Snterm e | Snterml (e, _) -> is_entry_dummy e - | Slist1 x | Slist0 x -> is_symbol_dummy x - | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y - | Sopt x -> is_symbol_dummy x - | Sself | Snext -> false - | Stree t -> is_tree_dummy t - -and is_tree_dummy = function - | Node {node=node} -> is_symbol_dummy node - | _ -> true -;; - - -let rec visit_entries todo pped = - let fmt = Format.std_formatter in - match todo with - | [] -> () - | hd :: tl -> - let todo = - if not (List.memq hd pped) then - begin - let { ename = ename; edesc = desc } = hd in - Format.fprintf fmt "@[%s ::=@ " ename; - let desc = clean_dummy_desc desc in - let todo = visit_description desc fmt ename @ todo in - Format.fprintf fmt "@]"; - Format.pp_print_newline fmt (); - Format.pp_print_newline fmt (); - todo - end - else - todo - in - let clean_todo todo = - let name_of_entry e = e.ename in - let pped = hd :: pped in - let todo = tl @ todo in - let todo = List.filter (fun e -> not(List.memq e pped)) todo in - HExtlib.list_uniq - ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) - (List.sort - (fun e1 e2 -> - Pervasives.compare (name_of_entry e1) (name_of_entry e2)) - todo), - pped - in - let todo,pped = clean_todo todo in - visit_entries todo pped -;; - -let _ = - let g_entry = Grammar.Entry.obj GrafiteParser.statement in - visit_entries [g_entry] [] diff --git a/helm/ocaml/grafite/test_dep.ml b/helm/ocaml/grafite/test_dep.ml deleted file mode 100644 index a2c7e392e..000000000 --- a/helm/ocaml/grafite/test_dep.ml +++ /dev/null @@ -1,38 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -let _ = - let ic = ref stdin in - let usage = "test_coarse_parser [ file ]" in - let open_file fname = - if !ic <> stdin then close_in !ic; - ic := open_in fname - in - Arg.parse [] open_file usage; - let deps = - GrafiteParser.parse_dependencies (Ulexing.from_utf8_channel !ic) - in - List.iter (fun dep -> print_endline (GrafiteAstPp.pp_dependency dep)) deps - diff --git a/helm/ocaml/grafite/test_parser.ml b/helm/ocaml/grafite/test_parser.ml deleted file mode 100644 index d5edf50c9..000000000 --- a/helm/ocaml/grafite/test_parser.ml +++ /dev/null @@ -1,161 +0,0 @@ -(* Copyright (C) 2005, 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://helm.cs.unibo.it/ - *) - -open Printf - -let _ = Helm_registry.load_from "test_parser.conf.xml" - -let xml_stream_of_markup = - let rec print_box (t: CicNotationPres.boxml_markup) = - Box.box2xml print_mpres t - and print_mpres (t: CicNotationPres.mathml_markup) = - Mpresentation.print_mpres print_box t - in - print_mpres - -let dump_xml t id_to_uri fname = - prerr_endline (sprintf "dumping MathML to %s ..." fname); - flush stdout; - let oc = open_out fname in - let markup = CicNotationPres.render id_to_uri t in - let xml_stream = CicNotationPres.print_xml markup in - Xml.pp_to_outchan xml_stream oc; - close_out oc - -let extract_loc = - function - | GrafiteAst.Executable (loc, _) - | GrafiteAst.Comment (loc, _) -> loc - -let pp_associativity = function - | Gramext.LeftA -> "left" - | Gramext.RightA -> "right" - | Gramext.NonA -> "non" - -let pp_precedence = string_of_int - -(* let last_rule_id = ref None *) - -let process_stream istream = - let char_count = ref 0 in - let module P = CicNotationPt in - let module G = GrafiteAst in - try - while true do - try - let statement = GrafiteParser.parse_statement istream in - let floc = extract_loc statement in - let (_, y) = HExtlib.loc_of_floc floc in - char_count := y + !char_count; - match statement with -(* | G.Executable (_, G.Macro (_, G.Check (_, - P.AttributedTerm (_, P.Ident _)))) -> - prerr_endline "mega hack"; - (match !last_rule_id with - | None -> () - | Some id -> - prerr_endline "removing last notation rule ..."; - CicNotationParser.delete id) *) - | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); - let t' = TermContentPres.pp_ast t in - prerr_endline (sprintf "rendered ast: %s" - (CicNotationPp.pp_term t')); - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" - | G.Executable (_, G.Command (_, - G.Notation (_, dir, l1, associativity, precedence, l2))) -> - prerr_endline "notation"; - prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); - prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); - prerr_endline (sprintf "prec: %s" (pp_precedence precedence)); - prerr_endline (sprintf "assoc: %s" (pp_associativity associativity)); - let keywords = CicNotationUtil.keywords_of_term l1 in - if keywords <> [] then - prerr_endline (sprintf "keywords: %s" - (String.concat " " keywords)); - if dir <> Some `RightToLeft then - ignore - (CicNotationParser.extend l1 ?precedence ?associativity - (fun env loc -> TermContentPres.instantiate_level2 env l2)); -(* last_rule_id := Some rule_id; *) - if dir <> Some `LeftToRight then - ignore (TermContentPres.add_pretty_printer - ?precedence ?associativity l2 l1) - | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> - prerr_endline "interpretation"; - prerr_endline (sprintf "dsc: %s" id); - ignore (TermAcicContent.add_interpretation id l2 l3); - flush stdout - | G.Executable (_, G.Command (_, G.Dump _)) -> - CicNotationParser.print_l2_pattern (); print_newline () - | G.Executable (_, G.Command (_, G.Render (_, uri))) -> - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - let annobj, _, _, id_to_sort, _, _, _ = - Cic2acic.acic_object_of_cic_object obj - in - let annterm = - match annobj with - | Cic.AConstant (_, _, _, _, ty, _, _) - | Cic.AVariable (_, _, _, ty, _, _) -> ty - | _ -> assert false - in - let t, id_to_uri = - TermAcicContent.ast_of_acic id_to_sort annterm - in - prerr_endline "Raw AST"; - prerr_endline (CicNotationPp.pp_term t); - let t' = TermContentPres.pp_ast t in - prerr_endline "Rendered AST"; - prerr_endline (CicNotationPp.pp_term t'); - dump_xml t' id_to_uri "out.xml" - | _ -> prerr_endline "Unsupported statement" - with - | End_of_file -> raise End_of_file - | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> - let (x, y) = HExtlib.loc_of_floc floc in -(* let before = String.sub line 0 x in - let error = String.sub line x (y - x) in - let after = String.sub line y (String.length line - y) in - eprintf "%s%s%s\n" before error after; - prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) - prerr_endline (sprintf "Parse error at character %d-%d: %s" - (!char_count + x) (!char_count + y) msg) - | exn -> - prerr_endline - (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) - done - with End_of_file -> () - -let _ = - let arg_spec = [ ] in - let usage = "" in - Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; - print_endline "Loading builtin notation ..."; - CicNotation.load_notation (Helm_registry.get "notation.core_file"); - print_endline "done."; - flush stdout; - process_stream (Ulexing.from_utf8_channel stdin) - diff --git a/helm/ocaml/grafite2/disambiguatePp.ml b/helm/ocaml/grafite2/disambiguatePp.ml index c3a48e409..733179589 100644 --- a/helm/ocaml/grafite2/disambiguatePp.ml +++ b/helm/ocaml/grafite2/disambiguatePp.ml @@ -25,38 +25,6 @@ open DisambiguateTypes -let parse_environment str = - let stream = Ulexing.from_utf8_string str in - let environment = ref Environment.empty in - let multiple_environment = ref Environment.empty in - try - while true do - let alias = - match GrafiteParser.parse_statement stream with - GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias))) - -> alias - | _ -> assert false in - let key,value = - (*CSC: Warning: this code should be factorized with the corresponding - code in MatitaEngine *) - match alias with - GrafiteAst.Ident_alias (id,uri) -> - Id id, - (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) - | GrafiteAst.Symbol_alias (symb,instance,desc) -> - Symbol (symb,instance), - DisambiguateChoices.lookup_symbol_by_dsc symb desc - | GrafiteAst.Number_alias (instance,desc) -> - Num instance, - DisambiguateChoices.lookup_num_by_dsc desc - in - environment := Environment.add key value !environment; - multiple_environment := Environment.cons key value !multiple_environment; - done; - assert false - with End_of_file -> - !environment, !multiple_environment - let alias_of_domain_and_codomain_items domain_item (dsc,_) = match domain_item with Id id -> GrafiteAst.Ident_alias (id, dsc) diff --git a/helm/ocaml/grafite2/disambiguatePp.mli b/helm/ocaml/grafite2/disambiguatePp.mli index 69b6e8451..516dfee17 100644 --- a/helm/ocaml/grafite2/disambiguatePp.mli +++ b/helm/ocaml/grafite2/disambiguatePp.mli @@ -23,10 +23,6 @@ * http://helm.cs.unibo.it/ *) -val parse_environment: - string -> - DisambiguateTypes.environment * DisambiguateTypes.multiple_environment - val aliases_of_domain_and_codomain_items_list: (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list -> GrafiteAst.alias_spec list diff --git a/helm/ocaml/grafite2/grafiteEngine.ml b/helm/ocaml/grafite2/grafiteEngine.ml index 70fb767a8..00470b9fc 100644 --- a/helm/ocaml/grafite2/grafiteEngine.ml +++ b/helm/ocaml/grafite2/grafiteEngine.ml @@ -24,13 +24,11 @@ *) exception Drop -exception UnableToInclude of string exception IncludedFileNotCompiled of string (* file name *) exception MetadataNotFound of string (* file name *) type options = { do_heavy_checks: bool ; - include_paths: string list ; clean_baseuri: bool } @@ -319,6 +317,7 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos type eval_ast = {ea_go: 'term 'lazy_term 'reduction 'obj 'ident. + baseuri_of_script:(string -> string) -> disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -332,7 +331,6 @@ type eval_ast = GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> ?do_heavy_checks:bool -> - ?include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> @@ -341,6 +339,7 @@ type eval_ast = type 'a eval_command = {ec_go: 'term 'obj. + baseuri_of_script:(string -> string) -> disambiguate_command: (GrafiteTypes.status -> ('term,'obj) GrafiteAst.command -> @@ -351,6 +350,7 @@ type 'a eval_command = type 'a eval_executable = {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. + baseuri_of_script:(string -> string) -> disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -446,23 +446,9 @@ let eval_tactical ~disambiguate_tactic status tac = in status -let make_absolute paths path = - let rec aux = function - | [] -> ignore (Unix.stat path); path - | p :: tl -> - let path = p ^ "/" ^ path in - try - ignore (Unix.stat path); path - with Unix.Unix_error _ -> aux tl - in - try - aux paths - with Unix.Unix_error _ -> raise (UnableToInclude path) -;; - let eval_comment status c = status -let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> +let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd -> let status,cmd = disambiguate_command status cmd in let cmd,notation_ids' = CicNotation.process_notation cmd in let status = @@ -475,10 +461,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status | GrafiteAst.Include (loc, path) -> - let absolute_path = make_absolute opts.include_paths path in - let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in - let metadatapath = - GrafiteMisc.metadata_file_of_script ~basedir absolute_path in + let baseuri = baseuri_of_script path in + let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in if not (Sys.file_exists moopath) then raise (IncludedFileNotCompiled moopath); let status = @@ -634,7 +619,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> MatitaSync.add_obj uri obj {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof} -} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex -> +} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex -> match ex with | GrafiteAst.Tactical (_, tac, None) -> eval_tactical ~disambiguate_tactic status tac @@ -642,7 +627,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> let status = eval_tactical ~disambiguate_tactic status tac in eval_tactical ~disambiguate_tactic status punct | GrafiteAst.Command (_, cmd) -> - eval_command.ec_go ~disambiguate_command opts status cmd + eval_command.ec_go ~baseuri_of_script ~disambiguate_command + opts status cmd | GrafiteAst.Macro (_, mac) -> (*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO raise (Command_error @@ -662,21 +648,23 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd -> let ast = ast_of_cmd ast in status := eval_ast.ea_go + ~baseuri_of_script:(fun _ -> assert false) ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic) ~disambiguate_command:(fun status cmd -> status,cmd) !status ast) moo -} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command - ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st +} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic + ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status + st -> let opts = { do_heavy_checks = do_heavy_checks ; - include_paths = include_paths; clean_baseuri = clean_baseuri } in match st with | GrafiteAst.Executable (_,ex) -> - eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex + eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic + ~disambiguate_command opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c } diff --git a/helm/ocaml/grafite2/grafiteEngine.mli b/helm/ocaml/grafite2/grafiteEngine.mli index efebbf048..e317060b5 100644 --- a/helm/ocaml/grafite2/grafiteEngine.mli +++ b/helm/ocaml/grafite2/grafiteEngine.mli @@ -24,10 +24,11 @@ *) exception Drop -exception UnableToInclude of string exception IncludedFileNotCompiled of string val eval_ast : + baseuri_of_script:(string -> string) -> + disambiguate_tactic: (GrafiteTypes.status -> ProofEngineTypes.goal -> @@ -41,7 +42,6 @@ val eval_ast : GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> ?do_heavy_checks:bool -> - ?include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status -> ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> diff --git a/helm/ocaml/grafite2/grafiteMisc.ml b/helm/ocaml/grafite2/grafiteMisc.ml index 8739b7a07..227cd382b 100644 --- a/helm/ocaml/grafite2/grafiteMisc.ml +++ b/helm/ocaml/grafite2/grafiteMisc.ml @@ -29,51 +29,3 @@ let is_empty buri = Http_getter_types.Ls_section _ -> true | Http_getter_types.Ls_object _ -> false) (Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/")) - -let baseuri_of_baseuri_decl st = - match st with - | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None - -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Ulexing.from_utf8_channel ic in - (try - while true do - try - let stm = GrafiteParser.parse_statement istream in - match baseuri_of_baseuri_decl stm with - | Some buri -> - let u = Http_getter_misc.strip_trailing_slash buri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then - HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); - (try - ignore(Http_getter.resolve u) - with - | Http_getter_types.Unresolvable_URI _ -> - HLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | Http_getter_types.Key_not_found _ -> ()); - uri := Some u; - raise End_of_file - | None -> () - with - CicNotationParser.Parse_error err -> - HLog.error ("Unable to parse: " ^ file); - HLog.error ("Parse error: " ^ err); - () - done - with End_of_file -> close_in ic); - match !uri with - | Some uri -> uri - | None -> failwith ("No baseuri defined in " ^ file) - -let obj_file_of_script ~basedir f = - let baseuri = baseuri_of_file f in - LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri - -let metadata_file_of_script ~basedir f = - let baseuri = baseuri_of_file f in - LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri - diff --git a/helm/ocaml/grafite2/grafiteMisc.mli b/helm/ocaml/grafite2/grafiteMisc.mli index 9f1486b0b..833bb6360 100644 --- a/helm/ocaml/grafite2/grafiteMisc.mli +++ b/helm/ocaml/grafite2/grafiteMisc.mli @@ -23,14 +23,5 @@ * http://helm.cs.unibo.it/ *) -val baseuri_of_baseuri_decl : - ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> - string option - (** check whether no objects are defined below a given baseuri *) val is_empty: string -> bool - -val baseuri_of_file : string -> string - -val obj_file_of_script : basedir:string -> string -> string -val metadata_file_of_script : basedir:string -> string -> string diff --git a/helm/ocaml/grafite_parser/.depend b/helm/ocaml/grafite_parser/.depend index 8baa095bc..6d2222906 100644 --- a/helm/ocaml/grafite_parser/.depend +++ b/helm/ocaml/grafite_parser/.depend @@ -1,4 +1,10 @@ +grafiteParser.cmo: grafiteParser.cmi +grafiteParser.cmx: grafiteParser.cmi +cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi +cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi matitaDisambiguator.cmo: matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaDisambiguator.cmi grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi +grafiteParserMisc.cmo: grafiteParserMisc.cmi +grafiteParserMisc.cmx: grafiteParserMisc.cmi diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile index afb05493e..d569dd41d 100644 --- a/helm/ocaml/grafite_parser/Makefile +++ b/helm/ocaml/grafite_parser/Makefile @@ -2,9 +2,41 @@ PACKAGE = grafite_parser PREDICATES = INTERFACE_FILES = \ + grafiteParser.mli \ + cicNotation2.mli \ matitaDisambiguator.mli \ grafiteDisambiguate.mli \ + grafiteParserMisc.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +all: test_parser print_grammar test_dep +clean: clean_tests + +# cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as +# soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by +# "_loc" occurrences +UTF8DIR = $(shell $(OCAMLFIND) query helm-utf8_macros) +ULEXDIR = $(shell $(OCAMLFIND) query ulex) +MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" +grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +# +# +grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) +grafiteParser.cmx: OCAMLOPT = $(OCAMLOPT_P4) + +clean_tests: + rm -f test_parser{,.opt} test_dep{,.opt} print_grammar{,.opt} + +LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg +test: test_parser print_grammar test_dep +test_parser: test_parser.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +print_grammar: print_grammar.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< +test_dep: test_dep.ml $(PACKAGE).cma + $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< + include ../Makefile.common diff --git a/helm/ocaml/grafite_parser/cicNotation2.ml b/helm/ocaml/grafite_parser/cicNotation2.ml new file mode 100644 index 000000000..2ce3f012f --- /dev/null +++ b/helm/ocaml/grafite_parser/cicNotation2.ml @@ -0,0 +1,69 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +let load_notation fname = + let ic = open_in fname in + let lexbuf = Ulexing.from_utf8_channel ic in + try + while true do + match GrafiteParser.parse_statement lexbuf with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, cmd)) -> + ignore (CicNotation.process_notation cmd) + | _ -> () + done + with End_of_file -> close_in ic + +let parse_environment str = + let stream = Ulexing.from_utf8_string str in + let environment = ref DisambiguateTypes.Environment.empty in + let multiple_environment = ref DisambiguateTypes.Environment.empty in + try + while true do + let alias = + match GrafiteParser.parse_statement stream with + GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias))) + -> alias + | _ -> assert false in + let key,value = + (*CSC: Warning: this code should be factorized with the corresponding + code in MatitaEngine *) + match alias with + GrafiteAst.Ident_alias (id,uri) -> + DisambiguateTypes.Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) + | GrafiteAst.Symbol_alias (symb,instance,desc) -> + DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc + | GrafiteAst.Number_alias (instance,desc) -> + DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc + in + environment := DisambiguateTypes.Environment.add key value !environment; + multiple_environment := DisambiguateTypes.Environment.cons key value !multiple_environment; + done; + assert false + with End_of_file -> + !environment, !multiple_environment + diff --git a/helm/ocaml/grafite_parser/cicNotation2.mli b/helm/ocaml/grafite_parser/cicNotation2.mli new file mode 100644 index 000000000..2d8c4b3c8 --- /dev/null +++ b/helm/ocaml/grafite_parser/cicNotation2.mli @@ -0,0 +1,31 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +val parse_environment: + string -> + DisambiguateTypes.environment * DisambiguateTypes.multiple_environment + +(** @param fname file from which load notation *) +val load_notation: string -> unit diff --git a/helm/ocaml/grafite_parser/grafiteParser.ml b/helm/ocaml/grafite_parser/grafiteParser.ml new file mode 100644 index 000000000..64db52295 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParser.ml @@ -0,0 +1,555 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +open Printf + +module Ast = CicNotationPt + +type statement = + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.obj, string) + GrafiteAst.statement + +let grammar = CicNotationParser.level2_ast_grammar + +let term = CicNotationParser.term +let statement = Grammar.Entry.create grammar "statement" + +let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t) + +let default_precedence = 50 +let default_associativity = Gramext.NonA + +EXTEND + GLOBAL: term statement; + arg: [ + [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; RPAREN -> names,ty + | name = IDENT -> [name],Ast.Implicit + ] + ]; + constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; + tactic_term: [ [ t = term LEVEL "90N" -> t ] ]; + ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ]; + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] + ]; + reduction_kind: [ + [ IDENT "normalize" -> `Normalize + | IDENT "reduce" -> `Reduce + | IDENT "simplify" -> `Simpl + | IDENT "unfold"; t = OPT term -> `Unfold t + | IDENT "whd" -> `Whd ] + ]; + sequent_pattern_spec: [ + [ hyp_paths = + LIST0 + [ id = IDENT ; + path = OPT [SYMBOL ":" ; path = tactic_term -> path ] -> + (id,match path with Some p -> p | None -> Ast.UserInput) ]; + goal_path = OPT [ SYMBOL <:unicode>; term = tactic_term -> term ] -> + let goal_path = + match goal_path, hyp_paths with + None, [] -> Ast.UserInput + | None, _::_ -> Ast.Implicit + | Some goal_path, _ -> goal_path + in + hyp_paths,goal_path + ] + ]; + pattern_spec: [ + [ res = OPT [ + "in"; + wanted_and_sps = + [ "match" ; wanted = tactic_term ; + sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> + Some wanted,sps + | sps = sequent_pattern_spec -> + None,Some sps + ] -> + let wanted,hyp_paths,goal_path = + match wanted_and_sps with + wanted,None -> wanted, [], Ast.UserInput + | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path + in + wanted, hyp_paths, goal_path ] -> + match res with + None -> None,[],Ast.UserInput + | Some ps -> ps] + ]; + direction: [ + [ SYMBOL ">" -> `LeftToRight + | SYMBOL "<" -> `RightToLeft ] + ]; + int: [ [ num = NUMBER -> int_of_string num ] ]; + intros_spec: [ + [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + num, idents + ] + ]; + using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ]; + tactic: [ + [ IDENT "absurd"; t = tactic_term -> + GrafiteAst.Absurd (loc, t) + | IDENT "apply"; t = tactic_term -> + GrafiteAst.Apply (loc, t) + | IDENT "assumption" -> + GrafiteAst.Assumption loc + | IDENT "auto"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; + width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ]; + paramodulation = OPT [ IDENT "paramodulation" ]; + full = OPT [ IDENT "full" ] -> (* ALB *) + GrafiteAst.Auto (loc,depth,width,paramodulation,full) + | IDENT "clear"; id = IDENT -> + GrafiteAst.Clear (loc,id) + | IDENT "clearbody"; id = IDENT -> + GrafiteAst.ClearBody (loc,id) + | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> + GrafiteAst.Change (loc, what, t) + | IDENT "compare"; t = tactic_term -> + GrafiteAst.Compare (loc,t) + | IDENT "constructor"; n = int -> + GrafiteAst.Constructor (loc, n) + | IDENT "contradiction" -> + GrafiteAst.Contradiction loc + | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> + GrafiteAst.Cut (loc, ident, t) + | IDENT "decide"; IDENT "equality" -> + GrafiteAst.DecideEquality loc + | IDENT "decompose"; types = OPT ident_list0; what = IDENT; + (num, idents) = intros_spec -> + let types = match types with None -> [] | Some types -> types in + let to_spec id = GrafiteAst.Ident id in + GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) + | IDENT "discriminate"; t = tactic_term -> + GrafiteAst.Discriminate (loc, t) + | IDENT "elim"; what = tactic_term; using = using; + (num, idents) = intros_spec -> + GrafiteAst.Elim (loc, what, using, num, idents) + | IDENT "elimType"; what = tactic_term; using = using; + (num, idents) = intros_spec -> + GrafiteAst.ElimType (loc, what, using, num, idents) + | IDENT "exact"; t = tactic_term -> + GrafiteAst.Exact (loc, t) + | IDENT "exists" -> + GrafiteAst.Exists loc + | IDENT "fail" -> GrafiteAst.Fail loc + | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise (HExtlib.Localized (loc, CicNotationParser.Parse_error + ("the pattern cannot specify the term to replace, only its" + ^ " paths in the hypotheses and in the conclusion"))) + else + GrafiteAst.Fold (loc, kind, t, p) + | IDENT "fourier" -> + GrafiteAst.Fourier loc + | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + GrafiteAst.FwdSimpl (loc, hyp, idents) + | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> + GrafiteAst.Generalize (loc,p,id) + | IDENT "goal"; n = int -> + GrafiteAst.Goal (loc, n) + | IDENT "id" -> GrafiteAst.IdTac loc + | IDENT "injection"; t = tactic_term -> + GrafiteAst.Injection (loc, t) + | IDENT "intro"; ident = OPT IDENT -> + let idents = match ident with None -> [] | Some id -> [id] in + GrafiteAst.Intros (loc, Some 1, idents) + | IDENT "intros"; (num, idents) = intros_spec -> + GrafiteAst.Intros (loc, num, idents) + | IDENT "lapply"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ]; + what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; + ident = OPT [ IDENT "using" ; ident = IDENT -> ident ] -> + let to_what = match to_what with None -> [] | Some to_what -> to_what in + GrafiteAst.LApply (loc, depth, to_what, what, ident) + | IDENT "left" -> GrafiteAst.Left loc + | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + GrafiteAst.LetIn (loc, t, where) + | kind = reduction_kind; p = pattern_spec -> + GrafiteAst.Reduce (loc, kind, p) + | IDENT "reflexivity" -> + GrafiteAst.Reflexivity loc + | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> + GrafiteAst.Replace (loc, p, t) + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> + let (pt,_,_) = p in + if pt <> None then + raise + (HExtlib.Localized (loc, + (CicNotationParser.Parse_error + "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion"))) + else + GrafiteAst.Rewrite (loc, d, t, p) + | IDENT "right" -> + GrafiteAst.Right loc + | IDENT "ring" -> + GrafiteAst.Ring loc + | IDENT "split" -> + GrafiteAst.Split loc + | IDENT "symmetry" -> + GrafiteAst.Symmetry loc + | IDENT "transitivity"; t = tactic_term -> + GrafiteAst.Transitivity (loc, t) + ] + ]; + atomic_tactical: + [ "sequence" LEFTA + [ t1 = SELF; SYMBOL ";"; t2 = SELF -> + let ts = + match t1 with + | GrafiteAst.Seq (_, l) -> l @ [ t2 ] + | _ -> [ t1; t2 ] + in + GrafiteAst.Seq (loc, ts) + ] + | "then" NONA + [ tac = SELF; SYMBOL ";"; + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> + (GrafiteAst.Then (loc, tac, tacs)) + ] + | "loops" RIGHTA + [ IDENT "do"; count = int; tac = SELF; IDENT "end" -> + GrafiteAst.Do (loc, count, tac) + | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac) + ] + | "simple" NONA + [ IDENT "first"; + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> + GrafiteAst.First (loc, tacs) + | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac) + | IDENT "solve"; + SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"-> + GrafiteAst.Solve (loc, tacs) + | LPAREN; tac = SELF; RPAREN -> tac + | tac = tactic -> GrafiteAst.Tactic (loc, tac) + ] + ]; + punctuation_tactical: + [ + [ SYMBOL "[" -> GrafiteAst.Branch loc + | SYMBOL "|" -> GrafiteAst.Shift loc + | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i) + | SYMBOL "]" -> GrafiteAst.Merge loc + | SYMBOL ";" -> GrafiteAst.Semicolon loc + | SYMBOL "." -> GrafiteAst.Dot loc + ] + ]; + tactical: + [ "simple" NONA + [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals) + | IDENT "unfocus" -> GrafiteAst.Unfocus loc + | IDENT "skip" -> GrafiteAst.Skip loc + | tac = atomic_tactical LEVEL "loops" -> tac + ] + ]; + theorem_flavour: [ + [ [ IDENT "definition" ] -> `Definition + | [ IDENT "fact" ] -> `Fact + | [ IDENT "lemma" ] -> `Lemma + | [ IDENT "remark" ] -> `Remark + | [ IDENT "theorem" ] -> `Theorem + ] + ]; + inductive_spec: [ [ + fst_name = IDENT; params = LIST0 [ arg=arg -> arg ]; + SYMBOL ":"; fst_typ = term; SYMBOL <:unicode>; OPT SYMBOL "|"; + fst_constructors = LIST0 constructor SEP SYMBOL "|"; + tl = OPT [ "with"; + types = LIST1 [ + name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode>; + OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" -> + (name, true, typ, constructors) ] SEP "with" -> types + ] -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in + let tl_ind_types = match tl with None -> [] | Some types -> types in + let ind_types = fst_ind_type :: tl_ind_types in + (params, ind_types) + ] ]; + + record_spec: [ [ + name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; SYMBOL "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] SEP SYMBOL ";"; SYMBOL "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + (params,name,typ,fields) + ] ]; + + macro: [ + [ [ IDENT "quit" ] -> GrafiteAst.Quit loc +(* | [ IDENT "abort" ] -> GrafiteAst.Abort loc *) +(* | [ IDENT "undo" ]; steps = OPT NUMBER -> + GrafiteAst.Undo (loc, int_opt steps) + | [ IDENT "redo" ]; steps = OPT NUMBER -> + GrafiteAst.Redo (loc, int_opt steps) *) + | [ IDENT "check" ]; t = term -> + GrafiteAst.Check (loc, t) + | [ IDENT "hint" ] -> GrafiteAst.Hint loc + | [ IDENT "whelp"; "match" ] ; t = term -> + GrafiteAst.WMatch (loc,t) + | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> + GrafiteAst.WInstance (loc,t) + | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> + GrafiteAst.WLocate (loc,id) + | [ IDENT "whelp"; IDENT "elim" ] ; t = term -> + GrafiteAst.WElim (loc, t) + | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> + GrafiteAst.WHint (loc,t) + | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name) + ] + ]; + alias_spec: [ + [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> + let alpha = "[a-zA-Z]" in + let num = "[0-9]+" in + let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in + let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in + let rex = Str.regexp ("^"^ident^"$") in + if Str.string_match rex id 0 then + if (try ignore (UriManager.uri_of_string uri); true + with UriManager.IllFormedUri _ -> false) + then + GrafiteAst.Ident_alias (id, uri) + else + raise + (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri))) + else + raise (HExtlib.Localized (loc, CicNotationParser.Parse_error ( + sprintf "Not a valid identifier: %s" id))) + | IDENT "symbol"; symbol = QSTRING; + instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> i | None -> 0 + in + GrafiteAst.Symbol_alias (symbol, instance, dsc) + | IDENT "num"; + instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ]; + SYMBOL "="; dsc = QSTRING -> + let instance = + match instance with Some i -> i | None -> 0 + in + GrafiteAst.Number_alias (instance, dsc) + ] + ]; + argument: [ + [ l = LIST0 [ SYMBOL <:unicode> (* η *); SYMBOL "." -> () ]; + id = IDENT -> + Ast.IdentArg (List.length l, id) + ] + ]; + associativity: [ + [ IDENT "left"; IDENT "associative" -> Gramext.LeftA + | IDENT "right"; IDENT "associative" -> Gramext.RightA + | IDENT "non"; IDENT "associative" -> Gramext.NonA + ] + ]; + precedence: [ + [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ] + ]; + notation: [ + [ dir = OPT direction; s = QSTRING; + assoc = OPT associativity; prec = OPT precedence; + IDENT "for"; + p2 = + [ blob = UNPARSED_AST -> + add_raw_attribute ~text:(sprintf "@{%s}" blob) + (CicNotationParser.parse_level2_ast + (Ulexing.from_utf8_string blob)) + | blob = UNPARSED_META -> + add_raw_attribute ~text:(sprintf "${%s}" blob) + (CicNotationParser.parse_level2_meta + (Ulexing.from_utf8_string blob)) + ] -> + let assoc = + match assoc with + | None -> default_associativity + | Some assoc -> assoc + in + let prec = + match prec with + | None -> default_precedence + | Some prec -> prec + in + let p1 = + add_raw_attribute ~text:s + (CicNotationParser.parse_level1_pattern + (Ulexing.from_utf8_string s)) + in + (dir, p1, assoc, prec, p2) + ] + ]; + level3_term: [ + [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u) + | id = IDENT -> Ast.VarPattern id + | SYMBOL "_" -> Ast.ImplicitPattern + | LPAREN; terms = LIST1 SELF; RPAREN -> + (match terms with + | [] -> assert false + | [term] -> term + | terms -> Ast.ApplPattern terms) + ] + ]; + interpretation: [ + [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term -> + (s, args, t) + ] + ]; + command: [ [ + IDENT "set"; n = QSTRING; v = QSTRING -> + GrafiteAst.Set (loc, n, v) + | IDENT "drop" -> GrafiteAst.Drop loc + | IDENT "qed" -> GrafiteAst.Qed loc + | IDENT "variant" ; name = IDENT; SYMBOL ":"; + typ = term; SYMBOL <:unicode> ; newname = IDENT -> + GrafiteAst.Obj (loc, + Ast.Theorem + (`Variant,name,typ,Some (Ast.Ident (newname, None)))) + | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; + body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> + GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body)) + | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); + body = term -> + GrafiteAst.Obj (loc, + Ast.Theorem (flavour, name, Ast.Implicit, Some body)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = CicNotationParser.let_defs -> + let name,ty = + match defs with + | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty + | ((Ast.Ident (name, None), None),_,_) :: _ -> + name, Ast.Implicit + | _ -> assert false + in + let body = Ast.Ident (name,None) in + GrafiteAst.Obj (loc, Ast.Theorem(`Definition, name, ty, + Some (Ast.LetRec (ind_kind, defs, body)))) + | IDENT "inductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) + | IDENT "coinductive"; spec = inductive_spec -> + let (params, ind_types) = spec in + let ind_types = (* set inductive flags to false (coinductive) *) + List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) + ind_types + in + GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types)) + | IDENT "coercion" ; name = IDENT -> + GrafiteAst.Coercion (loc, Ast.Ident (name,Some []), true) + | IDENT "coercion" ; name = URI -> + GrafiteAst.Coercion (loc, Ast.Uri (name,Some []), true) + | IDENT "alias" ; spec = alias_spec -> + GrafiteAst.Alias (loc, spec) + | IDENT "record" ; (params,name,ty,fields) = record_spec -> + GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields)) + | IDENT "include" ; path = QSTRING -> + GrafiteAst.Include (loc,path) + | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> + let uris = List.map UriManager.uri_of_string uris in + GrafiteAst.Default (loc,what,uris) + | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation -> + GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2) + | IDENT "interpretation"; id = QSTRING; + (symbol, args, l3) = interpretation -> + GrafiteAst.Interpretation (loc, id, (symbol, args), l3) + + | IDENT "dump" -> GrafiteAst.Dump loc + | IDENT "render"; u = URI -> + GrafiteAst.Render (loc, UriManager.uri_of_string u) + ]]; + executable: [ + [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) + | tac = tactical; punct = punctuation_tactical -> + GrafiteAst.Tactical (loc, tac, Some punct) + | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) + | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) + ] + ]; + comment: [ + [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> + GrafiteAst.Code (loc, ex) + | str = NOTE -> + GrafiteAst.Note (loc, str) + ] + ]; + statement: [ + [ ex = executable -> GrafiteAst.Executable (loc,ex) + | com = comment -> GrafiteAst.Comment (loc, com) + | EOI -> raise End_of_file + ] + ]; +END + +let exc_located_wrapper f = + try + f () + with + | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg)) + | Stdpp.Exc_located (floc, exn) -> + raise + (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn))) + +let parse_statement lexbuf = + exc_located_wrapper + (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf))) + +let parse_dependencies lexbuf = + let tok_stream,_ = + CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) + in + let rec parse acc = + (parser + | [< '("URI", u) >] -> + parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc) + | [< '("IDENT", "include"); '("QSTRING", fname) >] -> + parse (GrafiteAst.IncludeDep fname :: acc) + | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] -> + parse (GrafiteAst.BaseuriDep baseuri :: acc) + | [< '("EOI", _) >] -> acc + | [< 'tok >] -> parse acc + | [< >] -> acc) tok_stream + in + List.rev (parse []) + diff --git a/helm/ocaml/grafite_parser/grafiteParser.mli b/helm/ocaml/grafite_parser/grafiteParser.mli new file mode 100644 index 000000000..7b33c6e42 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParser.mli @@ -0,0 +1,37 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +type statement = + (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, + CicNotationPt.obj, string) + GrafiteAst.statement + +val parse_statement: Ulexing.lexbuf -> statement (** @raise End_of_file *) + + (** @raise End_of_file *) +val parse_dependencies: Ulexing.lexbuf -> GrafiteAst.dependency list + +val statement: statement Grammar.Entry.e + diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.ml b/helm/ocaml/grafite_parser/grafiteParserMisc.ml new file mode 100644 index 000000000..1b77da7cb --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParserMisc.ml @@ -0,0 +1,80 @@ +(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ + *) + +exception UnableToInclude of string + +let baseuri_of_baseuri_decl st = + match st with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> + Some buri + | _ -> None + +let make_absolute paths path = + let rec aux = function + | [] -> ignore (Unix.stat path); path + | p :: tl -> + let path = p ^ "/" ^ path in + try + ignore (Unix.stat path); path + with Unix.Unix_error _ -> aux tl + in + try + aux paths + with Unix.Unix_error _ -> raise (UnableToInclude path) +;; + +let baseuri_of_script ~include_paths file = + let file = make_absolute include_paths file in + let uri = ref None in + let ic = open_in file in + let istream = Ulexing.from_utf8_channel ic in + (try + while true do + try + let stm = GrafiteParser.parse_statement istream in + match baseuri_of_baseuri_decl stm with + | Some buri -> + let u = Http_getter_misc.strip_trailing_slash buri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then + HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); + (try + ignore(Http_getter.resolve u) + with + | Http_getter_types.Unresolvable_URI _ -> + HLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | Http_getter_types.Key_not_found _ -> ()); + uri := Some u; + raise End_of_file + | None -> () + with + CicNotationParser.Parse_error err -> + HLog.error ("Unable to parse: " ^ file); + HLog.error ("Parse error: " ^ err); + () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) diff --git a/helm/ocaml/grafite_parser/grafiteParserMisc.mli b/helm/ocaml/grafite_parser/grafiteParserMisc.mli new file mode 100644 index 000000000..74f60ec04 --- /dev/null +++ b/helm/ocaml/grafite_parser/grafiteParserMisc.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/ + *) + +exception UnableToInclude of string + +val baseuri_of_baseuri_decl : + ('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement -> + string option + +val baseuri_of_script : include_paths:string list -> string -> string diff --git a/helm/ocaml/grafite_parser/print_grammar.ml b/helm/ocaml/grafite_parser/print_grammar.ml new file mode 100644 index 000000000..d7d6f3c96 --- /dev/null +++ b/helm/ocaml/grafite_parser/print_grammar.ml @@ -0,0 +1,285 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +open Gramext + +let tex_of_unicode s = + let contractions = ("\\Longrightarrow","=>") :: [] in + if String.length s <= 1 then s + else (* probably an extended unicode symbol *) + let s = Utf8Macro.tex_of_unicode s in + try List.assoc s contractions with Not_found -> s + +let needs_brackets t = + let rec count_brothers = function + | Node {brother = brother} -> 1 + count_brothers brother + | _ -> 0 + in + count_brothers t > 1 + +let visit_description desc fmt self = + let skip s = List.mem s [ ] in + let inline s = List.mem s [ "int" ] in + + let rec visit_entry e todo is_son nesting = + let { ename = ename; edesc = desc } = e in + if inline ename then + visit_desc desc todo is_son nesting + else + begin + Format.fprintf fmt "%s " ename; + if skip ename then + todo + else + todo @ [e] + end + + and visit_desc d todo is_son nesting = + match d with + | Dlevels [] -> todo + | Dlevels [lev] -> visit_level lev todo is_son nesting + | Dlevels (lev::levels) -> + let todo = visit_level lev todo is_son nesting in + List.fold_left + (fun acc l -> + Format.fprintf fmt "@ | "; + visit_level l acc is_son nesting) + todo levels; + | _ -> todo + + and visit_level l todo is_son nesting = + let { lsuffix = suff ; lprefix = pref } = l in + let todo = visit_tree suff todo is_son nesting in + visit_tree pref todo is_son nesting + + and visit_tree t todo is_son nesting = + match t with + | Node node -> visit_node node todo is_son nesting + | _ -> todo + + and visit_node n todo is_son nesting = + let is_tree_printable t = + match t with + | Node _ -> true + | _ -> false + in + let { node = symbol; son = son ; brother = brother } = n in + let todo = visit_symbol symbol todo is_son nesting in + let todo = + if is_tree_printable son then + begin + let need_b = needs_brackets son in + if not is_son then + Format.fprintf fmt "@["; + if need_b then + Format.fprintf fmt "( "; + let todo = visit_tree son todo true nesting in + if need_b then + Format.fprintf fmt ")"; + if not is_son then + Format.fprintf fmt "@]"; + todo + end + else + todo + in + if is_tree_printable brother then + begin + Format.fprintf fmt "@ | "; + visit_tree brother todo is_son nesting + end + else + todo + + and visit_symbol s todo is_son nesting = + match s with + | Smeta (name, sl, _) -> + Format.fprintf fmt "%s " name; + List.fold_left ( + fun acc s -> + let todo = visit_symbol s acc is_son nesting in + if is_son then + Format.fprintf fmt "@ "; + todo) + todo sl + | Snterm entry -> visit_entry entry todo is_son nesting + | Snterml (entry,_) -> visit_entry entry todo is_son nesting + | Slist0 symbol -> + Format.fprintf fmt "{@[ "; + let todo = visit_symbol symbol todo is_son (nesting+1) in + Format.fprintf fmt "@]} @ "; + todo + | Slist0sep (symbol,sep) -> + Format.fprintf fmt "[@[ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "{@[ "; + let todo = visit_symbol sep todo is_son (nesting + 2) in + Format.fprintf fmt " "; + let todo = visit_symbol symbol todo is_son (nesting + 2) in + Format.fprintf fmt "@]} @]] @ "; + todo + | Slist1 symbol -> + Format.fprintf fmt "{@[ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "@]}+ @ "; + todo + | Slist1sep (symbol,sep) -> + let todo = visit_symbol symbol todo is_son nesting in + Format.fprintf fmt "{@[ "; + let todo = visit_symbol sep todo is_son (nesting + 1) in + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "@]} @ "; + todo + | Sopt symbol -> + Format.fprintf fmt "[@[ "; + let todo = visit_symbol symbol todo is_son (nesting + 1) in + Format.fprintf fmt "@]] @ "; + todo + | Sself -> Format.fprintf fmt "%s " self; todo + | Snext -> Format.fprintf fmt "next "; todo + | Stoken pattern -> + let constructor, keyword = pattern in + if keyword = "" then + Format.fprintf fmt "`%s' " constructor + else + Format.fprintf fmt "\"%s\" " (tex_of_unicode keyword); + todo + | Stree tree -> + if needs_brackets tree then + begin + Format.fprintf fmt "@[( "; + let todo = visit_tree tree todo is_son (nesting + 1) in + Format.fprintf fmt ")@] @ "; + todo + end + else + visit_tree tree todo is_son (nesting + 1) + in + visit_desc desc [] false 0 +;; + +let rec clean_dummy_desc = function + | Dlevels l -> Dlevels (clean_levels l) + | x -> x + +and clean_levels = function + | [] -> [] + | l :: tl -> clean_level l @ clean_levels tl + +and clean_level = function + | x -> + let pref = clean_tree x.lprefix in + let suff = clean_tree x.lsuffix in + match pref,suff with + | DeadEnd, DeadEnd -> [] + | _ -> [{x with lprefix = pref; lsuffix = suff}] + +and clean_tree = function + | Node n -> clean_node n + | x -> x + +and clean_node = function + | {node=node;son=son;brother=brother} -> + let bn = is_symbol_dummy node in + let bs = is_tree_dummy son in + let bb = is_tree_dummy brother in + let son = if bs then DeadEnd else son in + let brother = if bb then DeadEnd else brother in + if bb && bs && bn then + DeadEnd + else + if bn then + Node {node=Sself;son=son;brother=brother} + else + Node {node=node;son=son;brother=brother} + +and is_level_dummy = function + | {lsuffix=lsuffix;lprefix=lprefix} -> + is_tree_dummy lsuffix && is_tree_dummy lprefix + +and is_desc_dummy = function + | Dlevels l -> List.for_all is_level_dummy l + | Dparser _ -> true + +and is_entry_dummy = function + | {edesc=edesc} -> is_desc_dummy edesc + +and is_symbol_dummy = function + | Stoken ("DUMMY", _) -> true + | Stoken _ -> false + | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt + | Snterm e | Snterml (e, _) -> is_entry_dummy e + | Slist1 x | Slist0 x -> is_symbol_dummy x + | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y + | Sopt x -> is_symbol_dummy x + | Sself | Snext -> false + | Stree t -> is_tree_dummy t + +and is_tree_dummy = function + | Node {node=node} -> is_symbol_dummy node + | _ -> true +;; + + +let rec visit_entries todo pped = + let fmt = Format.std_formatter in + match todo with + | [] -> () + | hd :: tl -> + let todo = + if not (List.memq hd pped) then + begin + let { ename = ename; edesc = desc } = hd in + Format.fprintf fmt "@[%s ::=@ " ename; + let desc = clean_dummy_desc desc in + let todo = visit_description desc fmt ename @ todo in + Format.fprintf fmt "@]"; + Format.pp_print_newline fmt (); + Format.pp_print_newline fmt (); + todo + end + else + todo + in + let clean_todo todo = + let name_of_entry e = e.ename in + let pped = hd :: pped in + let todo = tl @ todo in + let todo = List.filter (fun e -> not(List.memq e pped)) todo in + HExtlib.list_uniq + ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2)) + (List.sort + (fun e1 e2 -> + Pervasives.compare (name_of_entry e1) (name_of_entry e2)) + todo), + pped + in + let todo,pped = clean_todo todo in + visit_entries todo pped +;; + +let _ = + let g_entry = Grammar.Entry.obj GrafiteParser.statement in + visit_entries [g_entry] [] diff --git a/helm/ocaml/grafite_parser/test_dep.ml b/helm/ocaml/grafite_parser/test_dep.ml new file mode 100644 index 000000000..a2c7e392e --- /dev/null +++ b/helm/ocaml/grafite_parser/test_dep.ml @@ -0,0 +1,38 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +let _ = + let ic = ref stdin in + let usage = "test_coarse_parser [ file ]" in + let open_file fname = + if !ic <> stdin then close_in !ic; + ic := open_in fname + in + Arg.parse [] open_file usage; + let deps = + GrafiteParser.parse_dependencies (Ulexing.from_utf8_channel !ic) + in + List.iter (fun dep -> print_endline (GrafiteAstPp.pp_dependency dep)) deps + diff --git a/helm/ocaml/grafite_parser/test_parser.ml b/helm/ocaml/grafite_parser/test_parser.ml new file mode 100644 index 000000000..76463f814 --- /dev/null +++ b/helm/ocaml/grafite_parser/test_parser.ml @@ -0,0 +1,161 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +open Printf + +let _ = Helm_registry.load_from "test_parser.conf.xml" + +let xml_stream_of_markup = + let rec print_box (t: CicNotationPres.boxml_markup) = + Box.box2xml print_mpres t + and print_mpres (t: CicNotationPres.mathml_markup) = + Mpresentation.print_mpres print_box t + in + print_mpres + +let dump_xml t id_to_uri fname = + prerr_endline (sprintf "dumping MathML to %s ..." fname); + flush stdout; + let oc = open_out fname in + let markup = CicNotationPres.render id_to_uri t in + let xml_stream = CicNotationPres.print_xml markup in + Xml.pp_to_outchan xml_stream oc; + close_out oc + +let extract_loc = + function + | GrafiteAst.Executable (loc, _) + | GrafiteAst.Comment (loc, _) -> loc + +let pp_associativity = function + | Gramext.LeftA -> "left" + | Gramext.RightA -> "right" + | Gramext.NonA -> "non" + +let pp_precedence = string_of_int + +(* let last_rule_id = ref None *) + +let process_stream istream = + let char_count = ref 0 in + let module P = CicNotationPt in + let module G = GrafiteAst in + try + while true do + try + let statement = GrafiteParser.parse_statement istream in + let floc = extract_loc statement in + let (_, y) = HExtlib.loc_of_floc floc in + char_count := y + !char_count; + match statement with +(* | G.Executable (_, G.Macro (_, G.Check (_, + P.AttributedTerm (_, P.Ident _)))) -> + prerr_endline "mega hack"; + (match !last_rule_id with + | None -> () + | Some id -> + prerr_endline "removing last notation rule ..."; + CicNotationParser.delete id) *) + | G.Executable (_, G.Macro (_, G.Check (_, t))) -> + prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); + let t' = TermContentPres.pp_ast t in + prerr_endline (sprintf "rendered ast: %s" + (CicNotationPp.pp_term t')); + let tbl = Hashtbl.create 0 in + dump_xml t' tbl "out.xml" + | G.Executable (_, G.Command (_, + G.Notation (_, dir, l1, associativity, precedence, l2))) -> + prerr_endline "notation"; + prerr_endline (sprintf "l1: %s" (CicNotationPp.pp_term l1)); + prerr_endline (sprintf "l2: %s" (CicNotationPp.pp_term l2)); + prerr_endline (sprintf "prec: %s" (pp_precedence precedence)); + prerr_endline (sprintf "assoc: %s" (pp_associativity associativity)); + let keywords = CicNotationUtil.keywords_of_term l1 in + if keywords <> [] then + prerr_endline (sprintf "keywords: %s" + (String.concat " " keywords)); + if dir <> Some `RightToLeft then + ignore + (CicNotationParser.extend l1 ?precedence ?associativity + (fun env loc -> TermContentPres.instantiate_level2 env l2)); +(* last_rule_id := Some rule_id; *) + if dir <> Some `LeftToRight then + ignore (TermContentPres.add_pretty_printer + ?precedence ?associativity l2 l1) + | G.Executable (_, G.Command (_, G.Interpretation (_, id, l2, l3))) -> + prerr_endline "interpretation"; + prerr_endline (sprintf "dsc: %s" id); + ignore (TermAcicContent.add_interpretation id l2 l3); + flush stdout + | G.Executable (_, G.Command (_, G.Dump _)) -> + CicNotationParser.print_l2_pattern (); print_newline () + | G.Executable (_, G.Command (_, G.Render (_, uri))) -> + let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let annobj, _, _, id_to_sort, _, _, _ = + Cic2acic.acic_object_of_cic_object obj + in + let annterm = + match annobj with + | Cic.AConstant (_, _, _, _, ty, _, _) + | Cic.AVariable (_, _, _, ty, _, _) -> ty + | _ -> assert false + in + let t, id_to_uri = + TermAcicContent.ast_of_acic id_to_sort annterm + in + prerr_endline "Raw AST"; + prerr_endline (CicNotationPp.pp_term t); + let t' = TermContentPres.pp_ast t in + prerr_endline "Rendered AST"; + prerr_endline (CicNotationPp.pp_term t'); + dump_xml t' id_to_uri "out.xml" + | _ -> prerr_endline "Unsupported statement" + with + | End_of_file -> raise End_of_file + | HExtlib.Localized (floc,CicNotationParser.Parse_error msg) -> + let (x, y) = HExtlib.loc_of_floc floc in +(* let before = String.sub line 0 x in + let error = String.sub line x (y - x) in + let after = String.sub line y (String.length line - y) in + eprintf "%s%s%s\n" before error after; + prerr_endline (sprintf "at character %d-%d: %s" x y msg) *) + prerr_endline (sprintf "Parse error at character %d-%d: %s" + (!char_count + x) (!char_count + y) msg) + | exn -> + prerr_endline + (sprintf "Uncaught exception: %s" (Printexc.to_string exn)) + done + with End_of_file -> () + +let _ = + let arg_spec = [ ] in + let usage = "" in + Arg.parse arg_spec (fun _ -> raise (Arg.Bad usage)) usage; + print_endline "Loading builtin notation ..."; + CicNotation2.load_notation (Helm_registry.get "notation.core_file"); + print_endline "done."; + flush stdout; + process_stream (Ulexing.from_utf8_channel stdin) +