1 /* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 module U = UriManager;;
30 exception InvalidSuffix of string;;
31 exception InductiveTypeURIExpected;;
32 exception UnknownIdentifier of string;;
34 let uri_of_id_map = Hashtbl.create 53;;
36 let get_index_in_list e =
40 | he::_ when he = e -> i
41 | _::tl -> aux (i+1) tl
46 let get_cookingno uri =
47 UriManager.relative_depth !CicTextualParser0.current_uri uri 0
54 %token <UriManager.uri> CONURI
55 %token <UriManager.uri * int> INDTYURI
56 %token <UriManager.uri * int * int> INDCONURI
58 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
59 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
62 %type <Cic.term option> main
67 | EOF { raise CicTextualParser0.Eof }
71 { let uri = UriManager.string_of_uri $1 in
72 let suff = (String.sub uri (String.length uri - 3) 3) in
75 let cookingno = get_cookingno $1 in
78 | _ -> raise (InvalidSuffix suff)
81 { let cookingno = get_cookingno (fst $1) in
82 MutInd (fst $1, cookingno, snd $1) }
84 { let (uri,tyno,consno) = $1 in
85 let cookingno = get_cookingno uri in
86 MutConstruct (uri, cookingno, tyno, consno) }
89 Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
93 Hashtbl.find uri_of_id_map $1
96 raise (UnknownIdentifier $1)
98 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
99 { let cookingno = get_cookingno (fst $5) in
100 MutCase (fst $5, cookingno, snd $5, $7, $3, $10) }
101 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
103 let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
104 raise InductiveTypeURIExpected
107 match Hashtbl.find uri_of_id_map $5 with
108 MutInd (uri,cookingno,typeno) ->
109 MutCase (uri, cookingno, typeno, $7, $3, $10)
110 | _ -> raise InductiveTypeURIExpected
112 | fixheader LCURLY exprseplist RCURLY
113 { let fixfunsdecls = snd $1 in
114 let fixfunsbodies = $3 in
118 [] -> raise Not_found
119 | (name,_,_)::_ when name = (fst $1) -> idx
120 | _::tl -> find (idx+1) tl
125 List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
126 fixfunsdecls fixfunsbodies
128 for i = 1 to List.length fixfuns do
129 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
133 | cofixheader LCURLY exprseplist RCURLY
134 { let cofixfunsdecls = (snd $1) in
135 let cofixfunsbodies = $3 in
139 [] -> raise Not_found
140 | (name,_)::_ when name = (fst $1) -> idx
141 | _::tl -> find (idx+1) tl
143 find 0 cofixfunsdecls
146 List.map2 (fun (name,ty) bo -> (name,ty,bo))
147 cofixfunsdecls cofixfunsbodies
149 for i = 1 to List.length cofixfuns do
150 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
152 CoFix (idx,cofixfuns)
154 | IMPLICIT { Implicit }
158 | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
160 | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
164 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
165 Prod (fst $1, snd $1,$2) }
167 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
168 Lambda (fst $1, snd $1,$2) }
170 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
171 LetIn (fst $1, snd $1,$2) }
176 FIX ID LCURLY fixfunsdecl RCURLY
177 { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
178 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
183 ID LPAREN NUM RPAREN COLON expr
185 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
189 COFIX ID LCURLY cofixfunsdecl RCURLY
190 { let bs = List.rev_map (function (name,_) -> Name name) $4 in
191 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
198 | ID COLON expr SEMICOLON cofixfunsdecl
202 PROD ID COLON expr DOT
203 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
206 { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
208 | LPAREN expr RPAREN ARROW
209 { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
213 LAMBDA ID COLON expr DOT
214 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
218 LAMBDA ID LETIN expr DOT
219 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
224 | expr SEMICOLON branches { $1::$3 }
229 | expr exprlist { $1::$2 }
233 | expr SEMICOLON exprseplist { $1::$3 }
237 { let cookingno = get_cookingno $3 in
238 Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) }
240 { let cookingno = get_cookingno (fst $3) in
241 Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) }
243 { let uri,indno,consno = $3 in
244 let cookingno = get_cookingno uri in
245 Hashtbl.add uri_of_id_map $2
246 (Cic.MutConstruct (uri, cookingno, indno ,consno))