+++ /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, GrafiteAst.reduction,
- GrafiteAst.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,
- GrafiteAst.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,GrafiteAst.Theorem (flavour, name, typ, body))
- | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
- body = term ->
- GrafiteAst.Obj (loc,
- GrafiteAst.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,GrafiteAst.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,GrafiteAst.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,GrafiteAst.Inductive (params, ind_types))
- | IDENT "coercion" ; name = IDENT ->
- GrafiteAst.Coercion (loc, Ast.Ident (name,Some []))
- | IDENT "coercion" ; name = URI ->
- GrafiteAst.Coercion (loc, Ast.Uri (name,Some []))
- | IDENT "alias" ; spec = alias_spec ->
- GrafiteAst.Alias (loc, spec)
- | IDENT "record" ; (params,name,ty,fields) = record_spec ->
- GrafiteAst.Obj (loc,GrafiteAst.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 "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI ->
- (** metadata commands lives only in .moo, where they are in marshalled
- * form *)
- raise (HExtlib.Localized (loc,CicNotationParser.Parse_error "metadata not allowed here"))
-
- | 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 [])
-
projects / helm.git / blobdiff