-requires="helm-grafite2"
+requires="helm-grafite2 ulex"
version="0.0.1"
archive(byte)="grafite_parser.cma"
archive(native)="grafite_parser.cmxa"
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
INTERFACE_FILES = \
grafiteAstPp.mli \
- grafiteParser.mli \
cicNotation.mli \
grafiteMarshal.mli \
$(NULL)
grafiteAst.ml \
$(INTERFACE_FILES:%.mli=%.ml)
-all: test_parser print_grammar test_dep
-clean: clean_tests
-
-# <cross> 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)
-# </cross>
-#
-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> 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)
-# </cross>
-
| 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) ->
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
+++ /dev/null
-(* 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<vdash>>; 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<def>> ; 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<def>>; OPT SYMBOL "|";
- fst_constructors = LIST0 constructor SEP SYMBOL "|";
- tl = OPT [ "with";
- types = LIST1 [
- name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
- 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<def>>; 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<eta>> (* η *); 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<def>> ; 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<def>> (* ≝ *); body = term -> body ] ->
- GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
- | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
- 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 [])
-
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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 "@[<hov2>";
- 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 "{@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting+1) in
- Format.fprintf fmt "@]} @ ";
- todo
- | Slist0sep (symbol,sep) ->
- Format.fprintf fmt "[@[<hov2> ";
- let todo = visit_symbol symbol todo is_son (nesting + 1) in
- Format.fprintf fmt "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "{@[<hov2> ";
- 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 "[@[<hov2> ";
- 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 "@[<hov2>( ";
- 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 "@[<hv2>%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] []
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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\e[01;31m%s\e[00m%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)
-
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)
* 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
*)
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
}
type eval_ast =
{ea_go:
'term 'lazy_term 'reduction 'obj 'ident.
+ baseuri_of_script:(string -> string) ->
disambiguate_tactic:
(GrafiteTypes.status ->
ProofEngineTypes.goal ->
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 ->
type 'a eval_command =
{ec_go: 'term 'obj.
+ baseuri_of_script:(string -> string) ->
disambiguate_command:
(GrafiteTypes.status ->
('term,'obj) GrafiteAst.command ->
type 'a eval_executable =
{ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
+ baseuri_of_script:(string -> string) ->
disambiguate_tactic:
(GrafiteTypes.status ->
ProofEngineTypes.goal ->
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 =
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 =
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
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
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
}
*)
exception Drop
-exception UnableToInclude of string
exception IncludedFileNotCompiled of string
val eval_ast :
+ baseuri_of_script:(string -> string) ->
+
disambiguate_tactic:
(GrafiteTypes.status ->
ProofEngineTypes.goal ->
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 ->
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
-
* 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
+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
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> 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)
+# </cross>
+#
+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
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
--- /dev/null
+(* 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<vdash>>; 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<def>> ; 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<def>>; OPT SYMBOL "|";
+ fst_constructors = LIST0 constructor SEP SYMBOL "|";
+ tl = OPT [ "with";
+ types = LIST1 [
+ name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
+ 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<def>>; 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<eta>> (* η *); 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<def>> ; 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<def>> (* ≝ *); body = term -> body ] ->
+ GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
+ | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
+ 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 [])
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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)
--- /dev/null
+(* 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
--- /dev/null
+(* 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 "@[<hov2>";
+ 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 "{@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son (nesting+1) in
+ Format.fprintf fmt "@]} @ ";
+ todo
+ | Slist0sep (symbol,sep) ->
+ Format.fprintf fmt "[@[<hov2> ";
+ let todo = visit_symbol symbol todo is_son (nesting + 1) in
+ Format.fprintf fmt "{@[<hov2> ";
+ 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 "{@[<hov2> ";
+ 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 "{@[<hov2> ";
+ 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 "[@[<hov2> ";
+ 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 "@[<hov2>( ";
+ 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 "@[<hv2>%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] []
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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\e[01;31m%s\e[00m%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)
+
projects / helm.git / commitdiff