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;;
33 exception ExplicitNamedSubstitutionAppliedToRel;;
34 exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
36 (* merge removing duplicates of two lists free of duplicates *)
42 if List.mem he dom1 then filter tl else he::(filter tl)
47 let get_index_in_list e =
51 | (Some he)::_ when he = e -> i
52 | _::tl -> aux (i+1) tl
57 (* Returns the first meta whose number is above the *)
58 (* number of the higher meta. *)
59 (*CSC: cut&pasted from proofEngine.ml *)
65 | None,(n,_,_)::tl -> aux (Some n,tl)
66 | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
68 1 + aux (None,!CicTextualParser0.metasenv)
71 (* identity_relocation_list_for_metavariable i canonical_context *)
72 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
73 (* where n = List.length [canonical_context] *)
74 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
75 (*CSC: cut&pasted from proofEngine.ml *)
76 let identity_relocation_list_for_metavariable canonical_context =
77 let canonical_context_length = List.length canonical_context in
81 | (n,None::tl) -> None::(aux ((n+1),tl))
82 | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
84 aux (1,canonical_context)
87 let deoptionize_exp_named_subst =
89 None -> [], (function _ -> [])
90 | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
93 let term_of_con_uri uri exp_named_subst =
94 Const (uri,exp_named_subst)
97 let term_of_var_uri uri exp_named_subst =
98 Var (uri,exp_named_subst)
101 let term_of_indty_uri (uri,tyno) exp_named_subst =
102 MutInd (uri, tyno, exp_named_subst)
105 let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
106 MutConstruct (uri, tyno, consno, exp_named_subst)
109 let term_of_uri uri =
111 CicTextualParser0.ConUri uri ->
113 | CicTextualParser0.VarUri uri ->
115 | CicTextualParser0.IndTyUri (uri,tyno) ->
116 term_of_indty_uri (uri,tyno)
117 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
118 term_of_indcon_uri (uri,tyno,consno)
121 let var_uri_of_id id interp =
123 None -> raise (UnknownIdentifier id)
124 | Some (CicTextualParser0.VarUri uri) -> uri
125 | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
128 let indty_uri_of_id id interp =
130 None -> raise (UnknownIdentifier id)
131 | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
132 | Some _ -> raise InductiveTypeURIExpected
138 %token <UriManager.uri> CONURI
139 %token <UriManager.uri> VARURI
140 %token <UriManager.uri * int> INDTYURI
141 %token <UriManager.uri * int * int> INDCONURI
143 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
144 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
147 %type <((string * CicTextualParser0.uri) -> unit) -> (string list * ((string -> CicTextualParser0.uri option) -> Cic.term)) option> main
150 expr { function _ -> Some $1 }
151 | alias { function register -> register $1 ; None }
152 | EOF { raise CicTextualParser0.Eof }
155 CONURI exp_named_subst
156 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
157 dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
159 | VARURI exp_named_subst
160 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
161 dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
163 | INDTYURI exp_named_subst
164 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
165 dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
167 | INDCONURI exp_named_subst
168 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
169 dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
174 Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
177 None -> ([], function _ -> res)
178 | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
182 let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
183 let dom = union dom1 [$1] in
187 None -> raise (UnknownIdentifier $1)
188 | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
190 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
191 { let dom1,mk_expr1 = $3 in
192 let dom2,mk_expr2 = $7 in
193 let dom3,mk_expr3 = $10 in
194 let dom = union dom1 (union dom2 dom3) in
198 (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
200 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
201 { let dom1,mk_expr1 = $3 in
202 let dom2,mk_expr2 = $7 in
203 let dom3,mk_expr3 = $10 in
204 let dom = union [$5] (union dom1 (union dom2 dom3)) in
207 let uri,typeno = indty_uri_of_id $5 interp in
209 (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
212 | fixheader LCURLY exprseplist RCURLY
213 { let dom1,mk_fixheader = $1 in
214 let dom2,mk_exprseplist = $3 in
215 let dom = union dom1 dom2 in
218 let fixfunsdecls = snd (mk_fixheader interp) in
219 let fixfunsbodies = (mk_exprseplist interp) in
223 [] -> raise Not_found
224 | (name,_,_)::_ when name = (fst (mk_fixheader interp)) -> idx
225 | _::tl -> find (idx+1) tl
230 List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
231 fixfunsdecls fixfunsbodies
233 for i = 1 to List.length fixfuns do
234 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
238 | cofixheader LCURLY exprseplist RCURLY
239 { let dom1,mk_cofixheader = $1 in
240 let dom2,mk_exprseplist = $3 in
241 let dom = union dom1 dom2 in
244 let cofixfunsdecls = (snd (mk_cofixheader interp)) in
245 let cofixfunsbodies = mk_exprseplist interp in
249 [] -> raise Not_found
250 | (name,_)::_ when name = (fst (mk_cofixheader interp)) -> idx
251 | _::tl -> find (idx+1) tl
253 find 0 cofixfunsdecls
256 List.map2 (fun (name,ty) bo -> (name,ty,bo))
257 cofixfunsdecls cofixfunsbodies
259 for i = 1 to List.length cofixfuns do
260 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
262 CoFix (idx,cofixfuns)
265 { let newmeta = new_meta () in
266 let new_canonical_context = [] in
268 identity_relocation_list_for_metavariable new_canonical_context
270 CicTextualParser0.metasenv :=
271 [newmeta, new_canonical_context, Sort Type ;
272 newmeta+1, new_canonical_context, Meta (newmeta,irl);
273 newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
274 ] @ !CicTextualParser0.metasenv ;
275 [], function _ -> Meta (newmeta+2,irl)
277 | SET { [], function _ -> Sort Set }
278 | PROP { [], function _ -> Sort Prop }
279 | TYPE { [], function _ -> Sort Type }
280 | LPAREN expr CAST expr RPAREN
281 { let dom1,mk_expr1 = $2 in
282 let dom2,mk_expr2 = $4 in
283 let dom = union dom1 dom2 in
284 dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
286 | META LBRACKET substitutionlist RBRACKET
287 { let dom,mk_substitutionlist = $3 in
288 dom, function interp -> Meta ($1, mk_substitutionlist interp)
290 | LPAREN expr expr exprlist RPAREN
291 { let dom1,mk_expr1 = $2 in
292 let dom2,mk_expr2 = $3 in
293 let dom3,mk_exprlist = $4 in
294 let dom = union dom1 (union dom2 dom3) in
297 Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
302 | LCURLY named_substs RCURLY
307 { let dom,mk_expr = $3 in
308 dom, function interp -> [$1, mk_expr interp] }
310 { let dom1,mk_expr = $3 in
311 let dom = union [$1] dom1 in
312 dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
313 | VARURI LETIN expr2 SEMICOLON named_substs
314 { let dom1,mk_expr = $3 in
315 let dom2,mk_named_substs = $5 in
316 let dom = union dom1 dom2 in
317 dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
319 | ID LETIN expr2 SEMICOLON named_substs
320 { let dom1,mk_expr = $3 in
321 let dom2,mk_named_substs = $5 in
322 let dom = union [$1] (union dom1 dom2) in
325 (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
330 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
331 let dom1,mk_expr1 = snd $1 in
332 let dom2,mk_expr2 = $2 in
333 let dom = union dom1 dom2 in
334 dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
337 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
338 let dom1,mk_expr1 = snd $1 in
339 let dom2,mk_expr2 = $2 in
340 let dom = union dom1 dom2 in
341 dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
344 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
345 let dom1,mk_expr1 = snd $1 in
346 let dom2,mk_expr2 = $2 in
347 let dom = union dom1 dom2 in
348 dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
354 FIX ID LCURLY fixfunsdecl RCURLY
355 { let dom,mk_fixfunsdecl = $4 in
360 (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
362 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
363 $2,(mk_fixfunsdecl interp)
367 ID LPAREN NUM RPAREN COLON expr
368 { let dom,mk_expr = $6 in
369 dom, function interp -> [$1,$3,mk_expr interp]
371 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
372 { let dom1,mk_expr = $6 in
373 let dom2,mk_fixfunsdecl = $8 in
374 let dom = union dom1 dom2 in
375 dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
379 COFIX ID LCURLY cofixfunsdecl RCURLY
380 { let dom,mk_cofixfunsdecl = $4 in
385 (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
387 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
388 $2,(mk_cofixfunsdecl interp)
393 { let dom,mk_expr = $3 in
394 dom, function interp -> [$1,(mk_expr interp)]
396 | ID COLON expr SEMICOLON cofixfunsdecl
397 { let dom1,mk_expr = $3 in
398 let dom2,mk_cofixfunsdecl = $5 in
399 let dom = union dom1 dom2 in
400 dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
404 PROD ID COLON expr DOT
405 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
406 let dom,mk_expr = $4 in
407 Cic.Name $2, (dom, function interp -> mk_expr interp)
410 { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
411 let dom,mk_expr = $1 in
412 Anonymous, (dom, function interp -> mk_expr interp)
414 | LPAREN expr RPAREN ARROW
415 { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
416 let dom,mk_expr = $2 in
417 Anonymous, (dom, function interp -> mk_expr interp)
421 LAMBDA ID COLON expr DOT
422 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
423 let dom,mk_expr = $4 in
424 Cic.Name $2, (dom, function interp -> mk_expr interp)
428 LAMBDA ID LETIN expr DOT
429 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
430 let dom,mk_expr = $4 in
431 Cic.Name $2, (dom, function interp -> mk_expr interp)
435 { [], function _ -> [] }
436 | expr SEMICOLON branches
437 { let dom1,mk_expr = $1 in
438 let dom2,mk_branches = $3 in
439 let dom = union dom1 dom2 in
440 dom, function interp -> (mk_expr interp)::(mk_branches interp)
443 { let dom,mk_expr = $1 in
444 dom, function interp -> [mk_expr interp]
449 { [], function _ -> [] }
451 { let dom1,mk_expr = $1 in
452 let dom2,mk_exprlist = $2 in
453 let dom = union dom1 dom2 in
454 dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
459 { let dom,mk_expr = $1 in
460 dom, function interp -> [mk_expr interp]
462 | expr SEMICOLON exprseplist
463 { let dom1,mk_expr = $1 in
464 let dom2,mk_exprseplist = $3 in
465 let dom = union dom1 dom2 in
466 dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
470 { [], function _ -> [] }
471 | expr SEMICOLON substitutionlist
472 { let dom1,mk_expr = $1 in
473 let dom2,mk_substitutionlist = $3 in
474 let dom = union dom1 dom2 in
476 function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
478 | NONE SEMICOLON substitutionlist
479 { let dom,mk_exprsubstitutionlist = $3 in
480 dom, function interp -> None::(mk_exprsubstitutionlist interp)
485 { $2,(CicTextualParser0.ConUri $3) }
487 { $2,(CicTextualParser0.VarUri $3) }
489 { $2,(CicTextualParser0.IndTyUri (fst $3, snd $3)) }
491 { let uri,indno,consno = $3 in
492 $2,(CicTextualParser0.IndConUri (uri, indno, consno))