(* 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/
 *)

(* $Id$ *)

let out = ref ignore
let set_callback f = out := f

module Ast = CicNotationPt

exception NoInclusionPerformed of string (* full path *)

type 'a localized_option =
   LSome of 'a
 | LNone of GrafiteAst.loc

type ast_statement =
  (CicNotationPt.term, CicNotationPt.term,
   CicNotationPt.term GrafiteAst.reduction, 
   CicNotationPt.term CicNotationPt.obj, string)
    GrafiteAst.statement

type statement =
  ?never_include:bool -> 
  include_paths:string list ->
  LexiconEngine.status ->
    LexiconEngine.status * ast_statement localized_option

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
        
let mk_rec_corec ind_kind defs loc = 
 (* In case of mutual definitions here we produce just
    the syntax tree for the first one. The others will be
    generated from the completely specified term just before
    insertion in the environment. We use the flavour
    `MutualDefinition to rememer this. *)
  let name,ty = 
    match defs with
    | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
        let ty =
         List.fold_right
          (fun var ty -> Ast.Binder (`Pi,var,ty)
          ) params ty
        in
         name,ty
    | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
        name, Ast.Implicit
    | _ -> assert false 
  in
  let body = Ast.Ident (name,None) in
  let flavour =
   if List.length defs = 1 then
    `Definition
   else
    `MutualDefinition
  in
   GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
     Some (Ast.LetRec (ind_kind, defs, body))))

type by_continuation =
   BYC_done
 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term

EXTEND
  GLOBAL: term statement;
  constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
  new_name: [
    [ id = IDENT -> Some id
    | SYMBOL "_" -> None ]
    ];
  ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
  tactic_term_list1: [
    [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
  ];
  reduction_kind: [
    [ IDENT "normalize" -> `Normalize
    | IDENT "simplify" -> `Simpl
    | IDENT "unfold"; t = OPT tactic_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, [] -> Some Ast.UserInput
        | None, _::_ -> None
        | Some goal_path, _ -> Some 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, [], Some Ast.UserInput
           | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
         in
          wanted, hyp_paths, goal_path ] ->
      match res with
         None -> None,[],Some Ast.UserInput
       | Some ps -> ps]
  ];
  direction: [
    [ SYMBOL ">" -> `LeftToRight
    | SYMBOL "<" -> `RightToLeft ]
  ];
  int: [ [ num = NUMBER -> int_of_string num ] ];
  intros_names: [
   [ idents = OPT ident_list0 ->
      match idents with None -> [] | Some idents -> idents
   ]
  ];
  intros_spec: [
    [ OPT [ IDENT "names" ]; 
      num = OPT [ num = int -> num ]; 
      idents = intros_names ->
        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 "applyS"; t = tactic_term ; params = auto_params ->
        GrafiteAst.ApplyS (loc, t, params)
    | IDENT "assumption" ->
        GrafiteAst.Assumption loc
    | IDENT "autobatch";  params = auto_params ->
        GrafiteAst.AutoBatch (loc,params)
    | IDENT "cases"; what = tactic_term;
      specs = intros_spec ->
        GrafiteAst.Cases (loc, what, specs)
    | IDENT "clear"; ids = LIST1 IDENT ->
        GrafiteAst.Clear (loc, ids)
    | IDENT "clearbody"; id = IDENT ->
        GrafiteAst.ClearBody (loc,id)
    | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
        GrafiteAst.Change (loc, what, t)
    | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
      OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
        let times = match times with None -> 1 | Some i -> i in
        GrafiteAst.Compose (loc, t1, t2, times, specs)
    | 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 "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
    | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
    | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
        GrafiteAst.Destruct (loc, xts)
    | IDENT "elim"; what = tactic_term; using = using; 
       pattern = OPT pattern_spec;
       (num, idents) = intros_spec ->
        let pattern = match pattern with
           | None         -> None, [], Some Ast.UserInput
           | Some pattern -> pattern   
        in
        GrafiteAst.Elim (loc, what, using, pattern, (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 [ "as"; idents = LIST1 new_name -> idents ] ->
        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 "id" -> GrafiteAst.IdTac loc
    | IDENT "intro"; ident = OPT IDENT ->
        let idents = match ident with None -> [] | Some id -> [Some id] in
        GrafiteAst.Intros (loc, (Some 1, idents))
    | IDENT "intros"; specs = intros_spec ->
        GrafiteAst.Intros (loc, specs)
    | IDENT "inversion"; t = tactic_term ->
        GrafiteAst.Inversion (loc, t)
    | IDENT "lapply"; 
      linear = OPT [ IDENT "linear" ];
      depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
      what = tactic_term; 
      to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
      ident = OPT [ "as" ; ident = IDENT -> ident ] ->
        let linear = match linear with None -> false | Some _ -> true in 
        let to_what = match to_what with None -> [] | Some to_what -> to_what in
        GrafiteAst.LApply (loc, linear, 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;
       xnames = OPT [ "as"; n = ident_list0 -> n ] ->
       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
         let n = match xnames with None -> [] | Some names -> names in 
         GrafiteAst.Rewrite (loc, d, t, p, n)
    | 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)
     (* Produzioni Aggiunte *)
    | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
        GrafiteAst.Assume (loc, id, t)
    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; 
      t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; 
                t' = tactic_term -> t']->
        GrafiteAst.Suppose (loc, t, id, t1)
    | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; 
      id2 = IDENT ; RPAREN -> 
        GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
    | just =
       [ IDENT "using"; t=tactic_term -> `Term t
       | params = auto_params -> `Auto params] ;
      cont=by_continuation ->
       (match cont with
           BYC_done -> GrafiteAst.Bydone (loc, just)
         | BYC_weproved (ty,id,t1) ->
            GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
         | BYC_letsuchthat (id1,t1,id2,t2) ->
            GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
         | BYC_wehaveand (id1,t1,id2,t2) ->
            GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
        GrafiteAst.We_need_to_prove (loc, t, id, t1)
    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
        GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
        GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
    | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
        GrafiteAst.Byinduction(loc, t, id)
    | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
        GrafiteAst.Thesisbecomes(loc, t)
    | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
        SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
         GrafiteAst.Case(loc,id,params)
      (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
    | IDENT "conclude"; 
      termine = tactic_term;
      SYMBOL "=" ;
      t1=tactic_term ;
      t2 =
       [ IDENT "using"; t=tactic_term -> `Term t
       | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
       | IDENT "proof" -> `Proof
       | params = auto_params -> `Auto params];
      cont = rewriting_step_continuation ->
       GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
    | IDENT "obtain" ; name = IDENT;
      termine = tactic_term;
      SYMBOL "=" ;
      t1=tactic_term ;
      t2 =
       [ IDENT "using"; t=tactic_term -> `Term t
       | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
       | IDENT "proof" -> `Proof
       | params = auto_params -> `Auto params];
      cont = rewriting_step_continuation ->
       GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
    | SYMBOL "=" ;
      t1=tactic_term ;
      t2 =
       [ IDENT "using"; t=tactic_term -> `Term t
       | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
       | IDENT "proof" -> `Proof
       | params = auto_params -> `Auto params];
      cont = rewriting_step_continuation ->
       GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
  ]
];
  auto_fixed_param: [
   [ IDENT "paramodulation"
   | IDENT "depth"
   | IDENT "width"
   | IDENT "size"
   | IDENT "timeout"
   | IDENT "library"
   | IDENT "type"
   ]
];
  auto_params: [
   [ params =
      LIST0 [
         i = auto_fixed_param -> i,""
       | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
              string_of_int v | v = IDENT -> v ] -> i,v ]; 
      tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
      (match tl with Some l -> l | None -> []),
      params
   ]
];
  by_continuation: [
    [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
    | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; 
            "done" -> BYC_weproved (ty,None,t1)
    | "done" -> BYC_done
    | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; 
      id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
    | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
              BYC_wehaveand (id1,t1,id2,t2)
    ]
];
  rewriting_step_continuation : [
    [ "done" -> true
    | -> false
    ]
];
  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 ->
          GrafiteAst.Do (loc, count, tac)
      | IDENT "repeat"; tac = SELF -> 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)
      | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
      | LPAREN; tac = SELF; RPAREN -> tac
      | tac = tactic -> tac
      ]
    ];
  punctuation_tactical:
    [
      [ SYMBOL "[" -> GrafiteAst.Branch loc
      | SYMBOL "|" -> GrafiteAst.Shift loc
      | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
      | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
      | SYMBOL "]" -> GrafiteAst.Merge loc
      | SYMBOL ";" -> GrafiteAst.Semicolon loc
      | SYMBOL "." -> GrafiteAst.Dot loc
      ]
    ];
  non_punctuation_tactical:
    [ "simple" NONA
      [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
      | IDENT "unfocus" -> GrafiteAst.Unfocus loc
      | IDENT "skip" -> GrafiteAst.Skip loc
      ]
    ];
  theorem_flavour: [
    [ [ IDENT "definition"  ] -> `Definition
    | [ IDENT "fact"        ] -> `Fact
    | [ IDENT "lemma"       ] -> `Lemma
    | [ IDENT "remark"      ] -> `Remark
    | [ IDENT "theorem"     ] -> `Theorem
    ]
  ];
  inductive_spec: [ [
    fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
    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 CicNotationParser.protected_binder_vars ;
     SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
     fields = LIST0 [ 
       name = IDENT ; 
       coercion = [ 
           SYMBOL ":" -> false,0 
         | SYMBOL ":"; SYMBOL ">" -> true,0
         | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
       ]; 
       ty = term -> 
         let b,n = coercion in 
         (name,ty,b,n) 
     ] 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 "check"   ]; t = term ->
        GrafiteAst.Check (loc, t)
    | [ IDENT "inline"]; 
        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
        suri = QSTRING; prefix = OPT QSTRING ->
         let style = match style with 
            | None       -> GrafiteAst.Declarative
            | Some depth -> GrafiteAst.Procedural depth
         in
         let prefix = match prefix with None -> "" | Some prefix -> prefix in
         GrafiteAst.Inline (loc,style,suri,prefix)
    | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
         if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
    | IDENT "auto"; params = auto_params ->
        GrafiteAst.AutoInteractive (loc,params)
    | [ IDENT "whelp"; "match" ] ; t = term -> 
        GrafiteAst.WMatch (loc,t)
    | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
        GrafiteAst.WInstance (loc,t)
    | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
        GrafiteAst.WLocate (loc,id)
    | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
        GrafiteAst.WElim (loc, t)
    | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
        GrafiteAst.WHint (loc,t)
    ]
  ];
  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
          LexiconAst.Ident_alias (id, uri)
        else 
          raise
           (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
      else
        raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
          Printf.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
        LexiconAst.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
        LexiconAst.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:(Printf.sprintf "@{%s}" blob)
              (CicNotationParser.parse_level2_ast
                (Ulexing.from_utf8_string blob))
        | blob = UNPARSED_META ->
            add_raw_attribute ~text:(Printf.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)
    ]
  ];
  
  include_command: [ [
      IDENT "include" ; path = QSTRING -> 
        loc,path,LexiconAst.WithPreferences
    | IDENT "include'" ; path = QSTRING -> 
        loc,path,LexiconAst.WithoutPreferences
   ]];

  grafite_command: [ [
      IDENT "set"; n = QSTRING; v = QSTRING ->
        GrafiteAst.Set (loc, n, v)
    | IDENT "drop" -> GrafiteAst.Drop loc
    | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
    | 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))
    | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
        GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
    | LETCOREC ; defs = CicNotationParser.let_defs -> 
        mk_rec_corec `CoInductive defs loc
    | LETREC ; defs = CicNotationParser.let_defs -> 
        mk_rec_corec `Inductive defs loc
    | 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" ; suri = URI ; arity = OPT int ; 
      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
        let arity = match arity with None -> 0 | Some x -> x in
        let saturations = match saturations with None -> 0 | Some x -> x in
        let composites = match composites with None -> true | Some _ -> false in
        GrafiteAst.Coercion
         (loc, UriManager.uri_of_string suri, composites, arity, saturations)
    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
        GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
    | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
       let uris = List.map UriManager.uri_of_string uris in
        GrafiteAst.Default (loc,what,uris)
    | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
      refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
                   refl = tactic_term -> refl ] ;
      sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
                   sym = tactic_term -> sym ] ;
      trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
                   trans = tactic_term -> trans ] ;
      "as" ; id = IDENT ->
       GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
  ]];
  lexicon_command: [ [
      IDENT "alias" ; spec = alias_spec ->
        LexiconAst.Alias (loc, spec)
    | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
        LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
    | IDENT "interpretation"; id = QSTRING;
      (symbol, args, l3) = interpretation ->
        LexiconAst.Interpretation (loc, id, (symbol, args), l3)
  ]];
  executable: [
    [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
    | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
        GrafiteAst.Tactic (loc, Some tac, punct)
    | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
    | tac = non_punctuation_tactical; punct = punctuation_tactical ->
        GrafiteAst.NonPunctuationTactical (loc, tac, punct)
    | 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 ->
       fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
    | com = comment ->
       fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
    | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
       fun ?(never_include=false) ~include_paths status ->
        let _root, buri, fullpath, _rrelpath = 
          Librarian.baseuri_of_script ~include_paths fname 
        in
        let status =
         if never_include then raise (NoInclusionPerformed fullpath)
         else LexiconEngine.eval_command status 
                (LexiconAst.Include (iloc,buri,mode,fullpath))
        in
         !out fname;
         status,
          LSome
          (GrafiteAst.Executable
           (loc,GrafiteAst.Command
            (loc,GrafiteAst.Include (iloc,buri))))
    | scom = lexicon_command ; SYMBOL "." ->
       fun ?(never_include=false) ~include_paths status ->
        let status = LexiconEngine.eval_command status scom in
         status,LNone loc
    | 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)))