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;;
33 let uri_of_id_map = Hashtbl.create 53;;
35 let get_index_in_list e =
39 | he::_ when he = e -> i
40 | _::tl -> aux (i+1) tl
45 let get_cookingno uri =
46 UriManager.relative_depth !CicTextualParser0.current_uri uri 0
53 %token <UriManager.uri> CONURI
54 %token <UriManager.uri * int> INDTYURI
55 %token <UriManager.uri * int * int> INDCONURI
57 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
58 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
60 %type <Cic.term option> main
65 | EOF { raise CicTextualParser0.Eof }
69 { let uri = UriManager.string_of_uri $1 in
70 let suff = (String.sub uri (String.length uri - 3) 3) in
73 let cookingno = get_cookingno $1 in
76 | _ -> raise (InvalidSuffix suff)
79 { let cookingno = get_cookingno (fst $1) in
80 MutInd (fst $1, cookingno, snd $1) }
82 { let (uri,tyno,consno) = $1 in
83 let cookingno = get_cookingno uri in
84 MutConstruct (uri, cookingno, tyno, consno) }
87 Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
90 Hashtbl.find uri_of_id_map $1
92 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
93 { let cookingno = get_cookingno (fst $5) in
94 MutCase (fst $5, cookingno, snd $5, $7, $3, $10) }
95 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
97 let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
98 raise InductiveTypeURIExpected
101 match Hashtbl.find uri_of_id_map $5 with
102 MutInd (uri,cookingno,typeno) ->
103 MutCase (uri, cookingno, typeno, $7, $3, $10)
104 | _ -> raise InductiveTypeURIExpected
106 | fixheader LCURLY exprseplist RCURLY
107 { let fixfunsdecls = snd $1 in
108 let fixfunsbodies = $3 in
112 [] -> raise Not_found
113 | (name,_,_)::_ when name = (fst $1) -> idx
114 | _::tl -> find (idx+1) tl
119 List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
120 fixfunsdecls fixfunsbodies
122 for i = 1 to List.length fixfuns do
123 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
127 | cofixheader LCURLY exprseplist RCURLY
128 { let cofixfunsdecls = (snd $1) in
129 let cofixfunsbodies = $3 in
133 [] -> raise Not_found
134 | (name,_)::_ when name = (fst $1) -> idx
135 | _::tl -> find (idx+1) tl
137 find 0 cofixfunsdecls
140 List.map2 (fun (name,ty) bo -> (name,ty,bo))
141 cofixfunsdecls cofixfunsbodies
143 for i = 1 to List.length cofixfuns do
144 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
146 CoFix (idx,cofixfuns)
148 | IMPLICIT { Implicit }
152 | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
154 | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
156 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
157 Prod (fst $1, snd $1,$2) }
159 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
160 Lambda (fst $1, snd $1,$2) }
162 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
163 LetIn (fst $1, snd $1,$2) }
166 FIX ID LCURLY fixfunsdecl RCURLY
167 { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
168 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
173 ID LPAREN NUM RPAREN COLON expr
175 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
179 COFIX ID LCURLY cofixfunsdecl RCURLY
180 { let bs = List.rev_map (function (name,_) -> Name name) $4 in
181 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
188 | ID COLON expr SEMICOLON cofixfunsdecl
192 PROD ID COLON expr DOT
193 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
196 { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
198 | LPAREN expr RPAREN ARROW
199 { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
203 LAMBDA ID COLON expr DOT
204 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
208 LAMBDA ID LETIN expr DOT
209 { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
214 | expr SEMICOLON branches { $1::$3 }
219 | expr exprlist { $1::$2 }
223 | expr SEMICOLON exprseplist { $1::$3 }
227 { let cookingno = get_cookingno $3 in
228 Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) }
230 { let cookingno = get_cookingno (fst $3) in
231 Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) }
233 { let uri,indno,consno = $3 in
234 let cookingno = get_cookingno uri in
235 Hashtbl.add uri_of_id_map $2
236 (Cic.MutConstruct (uri, cookingno, indno ,consno))