(* Copyright (C) 2004, 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 debug = false
let debug_print s =
  if debug then begin
    prerr_endline "<NEW_TEXTUAL_PARSER>";
    prerr_endline s;
    prerr_endline "</NEW_TEXTUAL_PARSER>"
  end

  (** if set to true each number will have a different insance number and can
  * thus be interpreted differently than others *)
let use_fresh_num_instances = false

  (** does the lexer return COMMENT tokens? *)
let return_comments = false

open Printf

open DisambiguateTypes

exception Parse_error of Token.flocation * string

let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments ()

let fresh_num_instance =
  let n = ref 0 in
  if use_fresh_num_instances then
    (fun () -> incr n; !n)
  else
    (fun () -> 0)

let choice_of_uri suri =
  let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in
  (suri, (fun _ _ _ -> term))

let grammar = Grammar.gcreate cic_lexer

let term = Grammar.Entry.create grammar "term"
let term0 = Grammar.Entry.create grammar "term0"
let tactic = Grammar.Entry.create grammar "tactic"
let tactical = Grammar.Entry.create grammar "tactical"
let tactical0 = Grammar.Entry.create grammar "tactical0"
let command = Grammar.Entry.create grammar "command"
let alias_spec = Grammar.Entry.create grammar "alias_spec"
let macro = Grammar.Entry.create grammar "macro"
let script = Grammar.Entry.create grammar "script"
let statement = Grammar.Entry.create grammar "statement"
let statements = Grammar.Entry.create grammar "statements"

let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)

let fail floc msg =
  let (x, y) = CicAst.loc_of_floc floc in
  failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)

let name_of_string = function
  | "_" -> Cic.Anonymous
  | s -> Cic.Name s

let string_of_name = function
  | Cic.Anonymous -> "_"
  | Cic.Name s -> s
  
let int_opt = function
  | None -> None
  | Some lexeme -> Some (int_of_string lexeme)

let int_of_string s =
  try
    Pervasives.int_of_string s
  with Failure _ ->
    failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)

  (** the uri of an inductive type (a ".ind" uri) is not meaningful without an
  * xpointer. Still, it's likely that an user who wrote "cic:/blabla/foo.ind"
  * actually meant "cic:/blabla/foo.ind#xpointer(1/1)", i.e. the first inductive
  * type in a block of mutual inductive types.
  *
  * This function performs the expansion foo.ind -> foo#xpointer..., if needed
  *)
let ind_expansion uri =
  let len = String.length uri in
  if len >= 4 && String.sub uri (len - 4) 4 = ".ind" then
    uri ^ "#xpointer(1/1)"
  else
    uri

let mk_binder_ast binder typ vars body =
  List.fold_right
    (fun var body ->
       let name = name_of_string var in
       CicAst.Binder (binder, (name, typ), body))
    vars body

EXTEND
  GLOBAL: term term0 statement statements;
  int: [
    [ num = NUM ->
        try
          int_of_string num
        with Failure _ -> raise (Parse_error (loc, "integer literal expected"))
    ]
  ];
  meta_subst: [
    [ s = SYMBOL "_" -> None
    | t = term -> Some t ]
  ];
  binder_low: [
    [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
    | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
    | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
  ];
  binder_high: [ [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda ] ];
  sort: [
    [ "Prop" -> `Prop
    | "Set" -> `Set
    | "Type" -> `Type
    | "CProp" -> `CProp ]
  ];
  typed_name: [
    [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
        (Cic.Name i, Some typ)
    | i = IDENT -> (Cic.Name i, None)
    ]
  ];
  subst: [
    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
      PAREN "[";
      substs = LIST1 [
        i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
      ] SEP SYMBOL ";";
      PAREN "]" ->
        substs
    ]
  ];
  substituted_name: [ (* a subs.name is an explicit substitution subject *)
    [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst)
    | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst)
    ]
  ];
  name: [ (* as substituted_name with no explicit substitution *)
    [ s = [ IDENT | SYMBOL ] -> s ]
  ];
  pattern: [
    [ n = name -> (n, [])
    | PAREN "("; head = name; vars = LIST1 typed_name; PAREN ")" ->
        (head, vars)
    ]
  ];
  arg: [
   [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
      SYMBOL ":"; ty = term; PAREN ")" -> names,ty
   | name = IDENT -> [name],CicAst.Implicit
   ]
  ];
  let_defs:[
    [ defs = LIST1 [
        name = IDENT;
        args = LIST1 [arg = arg -> arg];
        index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
        ty = OPT [ SYMBOL ":" ; t = term -> t ];
        SYMBOL <:unicode<def>> (* ≝ *);
        t1 = term ->
          let rec list_of_binder binder ty final_term = function
            | [] -> final_term
            | name::tl -> 
                CicAst.Binder (binder, (Cic.Name name, Some ty), 
                  list_of_binder binder ty final_term tl)
          in
          let rec binder_of_arg_list binder final_term = function
            | [] -> final_term
            | (l,ty)::tl ->  
                list_of_binder binder ty 
                  (binder_of_arg_list binder final_term tl) l
          in
          let t1' = binder_of_arg_list `Lambda t1 args in
          let ty' = 
            match ty with 
            | None -> None
            | Some ty -> Some (binder_of_arg_list `Pi ty args)
          in
          let rec get_position_of name n = function 
            | [] -> (None,n)
            | nam::tl -> 
                if nam = name then 
                  (Some n,n) 
                else 
                  (get_position_of name (n+1) tl)
          in
          let rec find_arg name n = function 
            | [] -> (fail loc (sprintf "Argument %s not found" name))
            | (l,_)::tl -> 
                let (got,len) = get_position_of name 0 l in
                (match got with 
                | None -> (find_arg name (n+len) tl)
                | Some where -> n + where)
          in
          let index = 
            (match index_name with 
             | None -> 0 
             | (Some name) -> find_arg name 0 args)
          in
          ((Cic.Name name,ty'), t1', index)
      ] SEP "and" -> defs
    ]];
  constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
  binder_vars: [
      [ vars = LIST1 IDENT SEP SYMBOL ",";
        typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
      | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
        typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
      ]
  ];
  term0: [ [ t = term; EOI -> return_term loc t ] ];
  term:
    [ "letin" NONA
      [ "let"; var = typed_name;
        SYMBOL <:unicode<def>> (* ≝ *);
        t1 = term; "in"; t2 = term ->
          return_term loc (CicAst.LetIn (var, t1, t2))
      | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
        defs = let_defs; "in"; body = term ->
            return_term loc (CicAst.LetRec (ind_kind, defs, body))
      ]
    | "binder" RIGHTA
      [
        b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
          let binder = mk_binder_ast b typ vars body in
          return_term loc binder
      | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
          let binder = mk_binder_ast b typ vars body in
          return_term loc binder
      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
      ]
    | "logic_add" LEFTA   [ (* nothing here by default *) ]
    | "logic_mult" LEFTA  [ (* nothing here by default *) ]
    | "logic_inv" NONA    [ (* nothing here by default *) ]
    | "relop" LEFTA
      [ t1 = term; SYMBOL "="; t2 = term ->
        return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
      ]
    | "add" LEFTA     [ (* nothing here by default *) ]
    | "mult" LEFTA    [ (* nothing here by default *) ]
    | "power" LEFTA   [ (* nothing here by default *) ]
    | "inv" NONA      [ (* nothing here by default *) ]
    | "apply" LEFTA
      [ t1 = term; t2 = term ->
        let rec aux = function
          | CicAst.Appl (hd :: tl) -> aux hd @ tl
          | term -> [term]
        in
        CicAst.Appl (aux t1 @ [t2])
      ]
    | "simple" NONA
      [ sort = sort -> CicAst.Sort sort
      | n = substituted_name -> return_term loc n
      | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
      | IMPLICIT -> return_term loc CicAst.Implicit
      | PLACEHOLDER -> return_term loc CicAst.UserInput
      | m = META;
        substs = [
          PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
            substs
        ] ->
            let index =
              try
                int_of_string (String.sub m 1 (String.length m - 1))
              with Failure "int_of_string" ->
                fail loc ("Invalid meta variable number: " ^ m)
            in
            return_term loc (CicAst.Meta (index, substs))
      | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
        "match"; t = term;
        indty_ident = OPT ["in" ; id = IDENT -> id ];
        "with";
        PAREN "[";
        patterns = LIST0 [
          lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term
          ->
            ((lhs: CicAst.case_pattern), rhs)
        ] SEP SYMBOL "|";
        PAREN "]" ->
          return_term loc
            (CicAst.Case (t, indty_ident, outtyp, patterns))
      | PAREN "("; t1 = term; SYMBOL ":"; t2 = term; PAREN ")" ->
          return_term loc (CicAst.Appl [CicAst.Symbol ("cast", 0); t1; t2])
      | PAREN "("; t = term; PAREN ")" -> return_term loc t
      ]
    ];
  tactic_where: [
    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
  ];
  tactic_term: [ [ t = term -> t ] ];
  ident_list0: [
    [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
  ];
  ident_list1: [
    [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
  ];
  reduction_kind: [
    [ [ IDENT "reduce" ] -> `Reduce
    | [ IDENT "simplify" ] -> `Simpl
    | [ IDENT "whd" ] -> `Whd 
    | [ IDENT "normalize" ] -> `Normalize ]
  ];
  pattern_spec: [
    [ "in";
      hyp_paths =
       LIST0
        [ id = IDENT ;
          path = OPT [SYMBOL ":" ; path = term -> path ] ->
          (id,match path with Some p -> p | None -> CicAst.UserInput) ]
        SEP SYMBOL ";";
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
        (hyp_paths, goal_path) ]
  ];
  direction: [
    [ IDENT "left" -> `Left
    | SYMBOL ">" -> `Left
    | IDENT "right" -> `Right
    | SYMBOL "<" -> `Right ]
  ];
  tactic: [
    [ [ IDENT "absurd" ]; t = tactic_term ->
        TacticAst.Absurd (loc, t)
    | [ IDENT "apply" ]; t = tactic_term ->
        TacticAst.Apply (loc, t)
    | [ IDENT "assumption" ] ->
        TacticAst.Assumption loc
    | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> 
          TacticAst.Auto (loc,num)
    | [ IDENT "change" ];
      t1 = tactic_term; "with"; t2 = tactic_term;
      where = tactic_where ->
        TacticAst.Change (loc, t1, t2, where)
    (* TODO Change_pattern *)
    | [ IDENT "contradiction" ] ->
        TacticAst.Contradiction loc
    | [ IDENT "cut" ];
      t = tactic_term ->
        TacticAst.Cut (loc, t)
    | [ IDENT "decompose" ];
      principles = ident_list1; where = IDENT ->
        TacticAst.Decompose (loc, where, principles)
    | [ IDENT "discriminate" ];
      t = tactic_term ->
        TacticAst.Discriminate (loc, t)
    | [ IDENT "elimType" ]; t = tactic_term ->
        TacticAst.ElimType (loc, t)
    | [ IDENT "elim" ];
      t1 = tactic_term;
      using = OPT [ "using"; using = tactic_term -> using ] ->
        TacticAst.Elim (loc, t1, using)
    | [ IDENT "exact" ]; t = tactic_term ->
        TacticAst.Exact (loc, t)
    | [ IDENT "exists" ] ->
        TacticAst.Exists loc
    | [ IDENT "fold" ];
      kind = reduction_kind; t = tactic_term ->
        TacticAst.Fold (loc, kind, t)
    | [ IDENT "fourier" ] ->
        TacticAst.Fourier loc
    | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n)
    | [ IDENT "injection" ]; ident = IDENT ->
        TacticAst.Injection (loc, ident)
    | [ IDENT "intros" ];
      num = OPT [ num = int -> num ];
      idents = OPT ident_list0 ->
        let idents = match idents with None -> [] | Some idents -> idents in
        TacticAst.Intros (loc, num, idents)
    | [ IDENT "intro" ] ->
        TacticAst.Intros (loc, Some 1, [])
    | [ IDENT "left" ] -> TacticAst.Left loc
    | [ IDENT "letin" ];
       where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
        TacticAst.LetIn (loc, t, where)
    | kind = reduction_kind;
      p = OPT [ pattern_spec ] ->
        let p = match p with None -> [], None | Some p -> p in
        TacticAst.Reduce (loc, kind, p)
    | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] ->
       let p = match p with None -> [], None | Some p -> p in
       TacticAst.Generalize (loc,t,p)
    | [ IDENT "reflexivity" ] ->
        TacticAst.Reflexivity loc
    | [ IDENT "replace" ];
      t1 = tactic_term; "with"; t2 = tactic_term ->
        TacticAst.Replace (loc, t1, t2)
    | IDENT "rewrite" ; d = direction; t = term ;
      p = OPT [ pattern_spec ] ->
        let p = match p with None -> [], None | Some p -> p in
        TacticAst.Rewrite (loc, d, t, p)
    | [ IDENT "right" ] -> TacticAst.Right loc
    | [ IDENT "ring" ] -> TacticAst.Ring loc
    | [ IDENT "split" ] -> TacticAst.Split loc
    | [ IDENT "symmetry" ] ->
        TacticAst.Symmetry loc
    | [ IDENT "transitivity" ];
      t = tactic_term ->
        TacticAst.Transitivity (loc, t)
    | [ IDENT "fwd" ]; name = IDENT ->
        TacticAst.FwdSimpl (loc, name)
    | [ IDENT "lapply" ]; t = term ->
        TacticAst.LApply (loc, t, [])
    ]
  ];
  tactical:
    [ "sequence" LEFTA
      [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
          TacticAst.Seq (loc, tacticals)
      ]
    | "then" NONA
      [ tac = tactical;
        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
          (TacticAst.Then (loc, tac, tacs))
      ]
    | "loops" RIGHTA
      [ [ IDENT "do" ]; count = int; tac = tactical ->
          TacticAst.Do (loc, count, tac)
      | [ IDENT "repeat" ]; tac = tactical ->
          TacticAst.Repeat (loc, tac)
      ]
    | "simple" NONA
      [ IDENT "tries";
        PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
          TacticAst.Tries (loc, tacs)
      | IDENT "try"; tac = NEXT ->
          TacticAst.Try (loc, tac)
      | IDENT "fail" -> TacticAst.Fail loc
      | IDENT "id" -> TacticAst.IdTac loc
      | PAREN "("; tac = tactical; PAREN ")" -> tac
      | tac = tactic -> TacticAst.Tactic (loc, 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>>; PAREN "{" ; 
     fields = LIST0 [ 
       name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) 
     ] SEP SYMBOL ";"; PAREN "}" -> 
      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"  ] -> TacticAst.Quit loc
(*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
    | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
(*     | [ IDENT "undo"   ]; steps = OPT NUM ->
        TacticAst.Undo (loc, int_opt steps)
    | [ IDENT "redo"   ]; steps = OPT NUM ->
        TacticAst.Redo (loc, int_opt steps) *)
    | [ IDENT "check"   ]; t = term ->
        TacticAst.Check (loc, t)
    | [ IDENT "hint" ] -> TacticAst.Hint loc
    | [ IDENT "whelp"; "match" ] ; t = term -> 
        TacticAst.WMatch (loc,t)
    | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
        TacticAst.WInstance (loc,t)
    | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT -> 
        TacticAst.WLocate (loc,id)
    | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
        TacticAst.WElim (loc, t)
    | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
        TacticAst.WHint (loc,t)
    | [ IDENT "print" ]; name = QSTRING -> TacticAst.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
        let rex = Str.regexp 
          ("^\\(cic:/\\|theory:/\\)"^ident^
           "\\(/"^ident^"+\\)*\\(\\."^ident^"\\)+"^
           "\\(#xpointer("^ num^"\\(/"^num^"\\)+)\\)?$") 
        in
        if Str.string_match rex uri 0 then
          TacticAst.Ident_alias (id, uri)
        else 
          raise (Parse_error (loc,sprintf "Not a valid uri: %s" uri))
      else
        raise (Parse_error (loc,sprintf "Not a valid identifier: %s" id))
    | IDENT "symbol"; symbol = QSTRING;
      instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
      SYMBOL "="; dsc = QSTRING ->
        let instance =
          match instance with Some i -> int_of_string i | None -> 0
        in
        TacticAst.Symbol_alias (symbol, instance, dsc)
    | IDENT "num";
      instance = OPT [ PAREN "("; IDENT "instance"; n = NUM; PAREN ")" -> n ];
      SYMBOL "="; dsc = QSTRING ->
        let instance =
          match instance with Some i -> int_of_string i | None -> 0
        in
        TacticAst.Number_alias (instance, dsc)
    ]
  ];
  
  command: [[
      [ IDENT "set"    ]; n = QSTRING; v = QSTRING ->
        TacticAst.Set (loc, n, v)
    | [ IDENT "qed"   ] -> TacticAst.Qed loc
    | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, typ, body))
    | flavour = theorem_flavour; name = IDENT;
      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
        TacticAst.Obj (loc,TacticAst.Theorem (flavour, name, CicAst.Implicit, body))
    | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
        defs = let_defs -> 
          let name,ty = 
            match defs with
            | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
            | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
            | _ -> assert false 
          in
          let body = CicAst.Ident (name,None) in
          TacticAst.Obj (loc,TacticAst.Theorem(`Definition, name, ty,
            Some (CicAst.LetRec (ind_kind, defs, body))))
          
    | [ IDENT "inductive" ]; spec = inductive_spec ->
        let (params, ind_types) = spec in
        TacticAst.Obj (loc,TacticAst.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
        TacticAst.Obj (loc,TacticAst.Inductive (params, ind_types))
    | [ IDENT "coercion" ] ; name = IDENT -> 
        TacticAst.Coercion (loc, CicAst.Ident (name,Some []))
    | [ IDENT "coercion" ] ; name = URI -> 
        TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
    | [ IDENT "alias"   ]; spec = alias_spec ->
        TacticAst.Alias (loc, spec)
    | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
        TacticAst.Obj (loc,TacticAst.Record (params,name,ty,fields))
  ]];

  executable: [
    [ cmd = command; SYMBOL "." -> TacticAst.Command (loc, cmd)
    | tac = tactical; SYMBOL "." -> TacticAst.Tactical (loc, tac)
    | mac = macro; SYMBOL "." -> TacticAst.Macro (loc, mac)
    ]
  ];
  
  comment: [
    [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> 
       TacticAst.Code (loc, ex)
    | str = NOTE -> 
       TacticAst.Note (loc, str)
    ]
  ];
  
  statement: [
    [ ex = executable -> TacticAst.Executable (loc,ex)
    | com = comment -> TacticAst.Comment (loc, com)
    ]
  ];
  statements: [
    [ l = LIST0 statement ; EOI -> l 
    ]  
  ];
END

let exc_located_wrapper f =
  try
    f ()
  with
  | Stdpp.Exc_located (floc, Stream.Error msg) ->
      raise (Parse_error (floc, msg))
  | Stdpp.Exc_located (floc, exn) ->
      raise (Parse_error (floc, (Printexc.to_string exn)))

let parse_term stream =
  exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
let parse_statement stream =
  exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
let parse_statements stream =
  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
  

(**/**)

(** {2 Interface for gTopLevel} *)

module EnvironmentP3 =
  struct
    type t = environment

    let empty = ""

    let aliases_grammar = Grammar.gcreate cic_lexer
    let aliases = Grammar.Entry.create aliases_grammar "aliases"

    let to_string env =
      let aliases =
        Environment.fold
          (fun domain_item (dsc, _) acc ->
            let s =
              match domain_item with
              | Id id ->
                  TacticAstPp.pp_alias (TacticAst.Ident_alias (id, dsc)) ^ "."
              | Symbol (symb, i) ->
                  TacticAstPp.pp_alias (TacticAst.Symbol_alias (symb, i, dsc))
                  ^ "."
              | Num i ->
                  TacticAstPp.pp_alias (TacticAst.Number_alias (i, dsc)) ^ "."
            in
            s :: acc)
          env []
      in
      String.concat "\n" (List.sort compare aliases)

    EXTEND
      GLOBAL: aliases;
      aliases: [  (* build an environment from an aliases list *)
        [ aliases = LIST0 alias; EOI ->
            List.fold_left
              (fun env (domain_item, codomain_item) ->
                Environment.add domain_item codomain_item env)
              Environment.empty aliases
        ]
      ];
      alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
        [ IDENT "alias";
          choice =
            [ IDENT "id"; id = IDENT; SYMBOL "="; suri = URI ->
                (Id id, choice_of_uri suri)
            | IDENT "symbol"; symbol = QSTRING;
              PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
              SYMBOL "="; dsc = QSTRING ->
                (Symbol (symbol, int_of_string instance),
                 DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
            | IDENT "num";
              PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
              SYMBOL "="; dsc = QSTRING ->
                (Num (int_of_string instance),
                 DisambiguateChoices.lookup_num_by_dsc dsc)
            ] -> choice ]
      ];
    END

    let of_string s =
      if s = empty then
        Environment.empty
      else
        exc_located_wrapper
          (fun () -> Grammar.Entry.parse aliases (Stream.of_string s))
  end

(* vim:set encoding=utf8: *)