+%{
+ 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))
+ }