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 list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
153 CONURI exp_named_subst
154 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
155 dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
157 | VARURI exp_named_subst
158 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
159 dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
161 | INDTYURI exp_named_subst
162 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
163 dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
165 | INDCONURI exp_named_subst
166 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
167 dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
172 Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
175 None -> ([], function _ -> res)
176 | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
180 let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
181 let dom = union dom1 [$1] in
185 None -> raise (UnknownIdentifier $1)
186 | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
188 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
189 { let dom1,mk_expr1 = $3 in
190 let dom2,mk_expr2 = $7 in
191 let dom3,mk_expr3 = $10 in
192 let dom = union dom1 (union dom2 dom3) in
196 (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
198 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
199 { let dom1,mk_expr1 = $3 in
200 let dom2,mk_expr2 = $7 in
201 let dom3,mk_expr3 = $10 in
202 let dom = union [$5] (union dom1 (union dom2 dom3)) in
205 let uri,typeno = indty_uri_of_id $5 interp in
207 (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
210 | fixheader LCURLY exprseplist RCURLY
211 { let dom1,mk_fixheader = $1 in
212 let dom2,mk_exprseplist = $3 in
213 let dom = union dom1 dom2 in
216 let fixfunsdecls = snd (mk_fixheader interp) in
217 let fixfunsbodies = (mk_exprseplist interp) in
221 [] -> raise Not_found
222 | (name,_,_)::_ when name = (fst (mk_fixheader interp)) -> idx
223 | _::tl -> find (idx+1) tl
228 List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
229 fixfunsdecls fixfunsbodies
231 for i = 1 to List.length fixfuns do
232 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
236 | cofixheader LCURLY exprseplist RCURLY
237 { let dom1,mk_cofixheader = $1 in
238 let dom2,mk_exprseplist = $3 in
239 let dom = union dom1 dom2 in
242 let cofixfunsdecls = (snd (mk_cofixheader interp)) in
243 let cofixfunsbodies = mk_exprseplist interp in
247 [] -> raise Not_found
248 | (name,_)::_ when name = (fst (mk_cofixheader interp)) -> idx
249 | _::tl -> find (idx+1) tl
251 find 0 cofixfunsdecls
254 List.map2 (fun (name,ty) bo -> (name,ty,bo))
255 cofixfunsdecls cofixfunsbodies
257 for i = 1 to List.length cofixfuns do
258 CicTextualParser0.binders := List.tl !CicTextualParser0.binders
260 CoFix (idx,cofixfuns)
263 { let newmeta = new_meta () in
264 let new_canonical_context = [] in
266 identity_relocation_list_for_metavariable new_canonical_context
268 CicTextualParser0.metasenv :=
269 [newmeta, new_canonical_context, Sort Type ;
270 newmeta+1, new_canonical_context, Meta (newmeta,irl);
271 newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
272 ] @ !CicTextualParser0.metasenv ;
273 [], function _ -> Meta (newmeta+2,irl)
275 | SET { [], function _ -> Sort Set }
276 | PROP { [], function _ -> Sort Prop }
277 | TYPE { [], function _ -> Sort Type }
278 | LPAREN expr CAST expr RPAREN
279 { let dom1,mk_expr1 = $2 in
280 let dom2,mk_expr2 = $4 in
281 let dom = union dom1 dom2 in
282 dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
284 | META LBRACKET substitutionlist RBRACKET
285 { let dom,mk_substitutionlist = $3 in
286 dom, function interp -> Meta ($1, mk_substitutionlist interp)
288 | LPAREN expr expr exprlist RPAREN
289 { let dom1,mk_expr1 = $2 in
290 let dom2,mk_expr2 = $3 in
291 let dom3,mk_exprlist = $4 in
292 let dom = union dom1 (union dom2 dom3) in
295 Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
300 | LCURLY named_substs RCURLY
305 { let dom,mk_expr = $3 in
306 dom, function interp -> [$1, mk_expr interp] }
308 { let dom1,mk_expr = $3 in
309 let dom = union [$1] dom1 in
310 dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
311 | VARURI LETIN expr2 SEMICOLON named_substs
312 { let dom1,mk_expr = $3 in
313 let dom2,mk_named_substs = $5 in
314 let dom = union dom1 dom2 in
315 dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
317 | ID LETIN expr2 SEMICOLON named_substs
318 { let dom1,mk_expr = $3 in
319 let dom2,mk_named_substs = $5 in
320 let dom = union [$1] (union dom1 dom2) in
323 (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
328 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
329 let dom1,mk_expr1 = snd $1 in
330 let dom2,mk_expr2 = $2 in
331 let dom = union dom1 dom2 in
332 dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
335 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
336 let dom1,mk_expr1 = snd $1 in
337 let dom2,mk_expr2 = $2 in
338 let dom = union dom1 dom2 in
339 dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
342 { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
343 let dom1,mk_expr1 = snd $1 in
344 let dom2,mk_expr2 = $2 in
345 let dom = union dom1 dom2 in
346 dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
352 FIX ID LCURLY fixfunsdecl RCURLY
353 { let dom,mk_fixfunsdecl = $4 in
358 (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
360 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
361 $2,(mk_fixfunsdecl interp)
365 ID LPAREN NUM RPAREN COLON expr
366 { let dom,mk_expr = $6 in
367 dom, function interp -> [$1,$3,mk_expr interp]
369 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
370 { let dom1,mk_expr = $6 in
371 let dom2,mk_fixfunsdecl = $8 in
372 let dom = union dom1 dom2 in
373 dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
377 COFIX ID LCURLY cofixfunsdecl RCURLY
378 { let dom,mk_cofixfunsdecl = $4 in
383 (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
385 CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
386 $2,(mk_cofixfunsdecl interp)
391 { let dom,mk_expr = $3 in
392 dom, function interp -> [$1,(mk_expr interp)]
394 | ID COLON expr SEMICOLON cofixfunsdecl
395 { let dom1,mk_expr = $3 in
396 let dom2,mk_cofixfunsdecl = $5 in
397 let dom = union dom1 dom2 in
398 dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
402 PROD ID COLON expr DOT
403 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
404 let dom,mk_expr = $4 in
405 Cic.Name $2, (dom, function interp -> mk_expr interp)
408 { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
409 let dom,mk_expr = $1 in
410 Anonymous, (dom, function interp -> mk_expr interp)
412 | LPAREN expr RPAREN ARROW
413 { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
414 let dom,mk_expr = $2 in
415 Anonymous, (dom, function interp -> mk_expr interp)
419 LAMBDA ID COLON expr DOT
420 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
421 let dom,mk_expr = $4 in
422 Cic.Name $2, (dom, function interp -> mk_expr interp)
426 LAMBDA ID LETIN expr DOT
427 { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
428 let dom,mk_expr = $4 in
429 Cic.Name $2, (dom, function interp -> mk_expr interp)
433 { [], function _ -> [] }
434 | expr SEMICOLON branches
435 { let dom1,mk_expr = $1 in
436 let dom2,mk_branches = $3 in
437 let dom = union dom1 dom2 in
438 dom, function interp -> (mk_expr interp)::(mk_branches interp)
441 { let dom,mk_expr = $1 in
442 dom, function interp -> [mk_expr interp]
447 { [], function _ -> [] }
449 { let dom1,mk_expr = $1 in
450 let dom2,mk_exprlist = $2 in
451 let dom = union dom1 dom2 in
452 dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
457 { let dom,mk_expr = $1 in
458 dom, function interp -> [mk_expr interp]
460 | expr SEMICOLON exprseplist
461 { let dom1,mk_expr = $1 in
462 let dom2,mk_exprseplist = $3 in
463 let dom = union dom1 dom2 in
464 dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
468 { [], function _ -> [] }
469 | expr SEMICOLON substitutionlist
470 { let dom1,mk_expr = $1 in
471 let dom2,mk_substitutionlist = $3 in
472 let dom = union dom1 dom2 in
474 function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
476 | NONE SEMICOLON substitutionlist
477 { let dom,mk_exprsubstitutionlist = $3 in
478 dom, function interp -> None::(mk_exprsubstitutionlist interp)