3 module U = UriManager;;
5 exception InvalidSuffix of string;;
6 exception InductiveTypeURIExpected;;
8 let uri_of_id_map = Hashtbl.create 53;;
10 let binders = ref [];;
12 let get_index_in_list e =
16 | he::_ when he = e -> i
17 | _::tl -> aux (i+1) tl
25 %token <UriManager.uri> CONURI
26 %token <UriManager.uri * int> INDTYURI
27 %token <UriManager.uri * int * int> INDCONURI
29 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
30 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE EOF
32 %type <Cic.term option> main
37 | EOF { raise CicTextualParser0.Eof }
41 { let uri = UriManager.string_of_uri $1 in
42 let suff = (String.sub uri (String.length uri - 3) 3) in
46 | _ -> raise (InvalidSuffix suff)
48 | INDTYURI { MutInd (fst $1, 0, snd $1) }
50 { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) }
53 Rel (get_index_in_list (Name $1) !binders)
56 Hashtbl.find uri_of_id_map $1
58 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
59 { MutCase (fst $5, 0, snd $5, $7, $3, $10) }
60 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
62 let _ = get_index_in_list (Name $5) !binders in
63 raise InductiveTypeURIExpected
66 match Hashtbl.find uri_of_id_map $5 with
67 MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10)
68 | _ -> raise InductiveTypeURIExpected
70 | fixheader LCURLY exprseplist RCURLY
71 { let fixfunsdecls = snd $1 in
72 let fixfunsbodies = $3 in
77 | (name,_,_)::_ when name = (fst $1) -> idx
78 | _::tl -> find (idx+1) tl
83 List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
84 fixfunsdecls fixfunsbodies
86 for i = 1 to List.length fixfuns do
87 binders := List.tl !binders
91 | cofixheader LCURLY exprseplist RCURLY
92 { let cofixfunsdecls = (snd $1) in
93 let cofixfunsbodies = $3 in
98 | (name,_)::_ when name = (fst $1) -> idx
99 | _::tl -> find (idx+1) tl
101 find 0 cofixfunsdecls
104 List.map2 (fun (name,ty) bo -> (name,ty,bo))
105 cofixfunsdecls cofixfunsbodies
107 for i = 1 to List.length cofixfuns do
108 binders := List.tl !binders
110 CoFix (idx,cofixfuns)
112 | IMPLICIT { Implicit }
116 | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
118 | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
120 { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) }
122 { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) }
124 { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
127 FIX ID LCURLY fixfunsdecl RCURLY
128 { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
129 binders := bs@(!binders) ;
134 ID LPAREN NUM RPAREN COLON expr
136 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
140 COFIX ID LCURLY cofixfunsdecl RCURLY
141 { let bs = List.rev_map (function (name,_) -> Name name) $4 in
142 binders := bs@(!binders) ;
149 | ID COLON expr SEMICOLON cofixfunsdecl
153 PROD ID COLON expr DOT
154 { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
157 LAMBDA ID COLON expr DOT
158 { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
161 LAMBDA ID LETIN expr DOT
162 { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
166 | expr SEMICOLON branches { $1::$3 }
171 | expr exprlist { $1::$2 }
175 | expr SEMICOLON exprseplist { $1::$3 }
179 { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }
181 { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) }
183 { let uri,indno,consno = $3 in
184 Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno))