%{
 open Cic;;
 module U = UriManager;;

 exception InvalidSuffix of string;;
 exception InductiveTypeURIExpected;;
 
 let uri_of_id_map = Hashtbl.create 53;;

 let binders = ref [];;

 let get_index_in_list e =
  let rec aux i =
   function
      [] -> raise Not_found
    | he::_ when he = e -> i
    | _::tl -> aux (i+1) tl
  in
   aux 1
;;
%}
%token <string> ID
%token <int> META
%token <int> NUM
%token <UriManager.uri> CONURI
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> INDCONURI
%token ALIAS
%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE EOF
%start main
%type <Cic.term option> main
%%
main:
   expr  { Some $1 }
 | alias { None }
 | EOF   { raise CicTextualParser0.Eof }
;
expr:
   CONURI
   { let uri = UriManager.string_of_uri $1 in
     let suff = (String.sub uri (String.length uri - 3) 3) in
      match suff with
         "con" -> Const ($1,0)
       | "var" -> Var $1
       | _ -> raise (InvalidSuffix suff)
   }
 | INDTYURI { MutInd (fst $1, 0, snd $1) }
 | INDCONURI
   { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) }
 | ID
   { try
       Rel (get_index_in_list (Name $1) !binders)
     with
      Not_found ->
       Hashtbl.find uri_of_id_map $1
   }
 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
    { MutCase (fst $5, 0, snd $5, $7, $3, $10) }
 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
    { try
       let _ = get_index_in_list (Name $5) !binders in
        raise InductiveTypeURIExpected
      with
       Not_found ->
        match Hashtbl.find uri_of_id_map $5 with
           MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10)
         | _ -> raise InductiveTypeURIExpected
    }
 | FIX ID LCURLY fixfuns RCURLY
    { let fixfuns = $4 in
       let idx =
        let rec find idx =
         function
            [] -> raise Not_found
          | (name,_,_,_)::_  when name = $2 -> idx
          | _::tl -> find (idx+1) tl
        in
         find 0 fixfuns
       in
        Fix (idx,fixfuns)
    }
 | COFIX ID LCURLY cofixfuns RCURLY
    { let cofixfuns = $4 in
       let idx =
        let rec find idx =
         function
            [] -> raise Not_found
          | (name,_,_)::_  when name = $2 -> idx
          | _::tl -> find (idx+1) tl
        in
         find 0 cofixfuns
       in
        CoFix (idx,cofixfuns)
    }
 | IMPLICIT { Implicit }
 | SET { Sort Set }
 | PROP { Sort Prop }
 | TYPE { Sort Type }
 | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
 | META { Meta $1 }
 | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 | pihead expr 
    { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) }
 | lambdahead expr 
    { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) }
 | letinhead expr 
    { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
;
fixfuns:
   ID LPAREN NUM RPAREN COLON expr LETIN expr
    { [$1,$3,$6,$8] }
 | ID LPAREN NUM RPAREN COLON expr LETIN expr SEMICOLON fixfuns
    { ($1,$3,$6,$8)::$10 }
;
cofixfuns:
   ID COLON expr LETIN expr
    { [$1,$3,$5] }
 | ID COLON expr LETIN expr SEMICOLON cofixfuns
    { ($1,$3,$5)::$7 }
;
pihead:
  PROD ID COLON expr DOT
   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
;
lambdahead:
  LAMBDA ID COLON expr DOT
   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
;
letinhead:
  LAMBDA ID LETIN expr DOT
   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
;
branches:
                            { [] }
 | expr SEMICOLON branches  { $1::$3 }
 | expr                     { [$1] }
;
exprlist:
                  { [] }
 | expr exprlist  { $1::$2 }
;
alias:
   ALIAS ID CONURI
    { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }
 | ALIAS ID INDTYURI
    { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) }
 | ALIAS ID INDCONURI
    { let uri,indno,consno = $3 in
       Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno))
    }