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,!TexCicTextualParser0.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 =
122 let module CTP0 = CicTextualParser0 in
123 match interp (CicTextualParser0.Id id) with
124 None -> raise (UnknownIdentifier id)
125 | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
126 | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
129 let indty_uri_of_id id interp =
130 let module CTP0 = CicTextualParser0 in
131 match interp (CicTextualParser0.Id id) with
132 None -> raise (UnknownIdentifier id)
133 | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
134 | Some _ -> raise InductiveTypeURIExpected
138 let newmeta = new_meta () in
139 let new_canonical_context = [] in
141 identity_relocation_list_for_metavariable new_canonical_context
143 TexCicTextualParser0.metasenv :=
144 [newmeta, new_canonical_context, Sort Type ;
145 newmeta+1, new_canonical_context, Meta (newmeta,irl);
146 newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
147 ] @ !TexCicTextualParser0.metasenv ;
148 [], function _ -> Meta (newmeta+2,irl)
154 %token <UriManager.uri> CONURI
155 %token <UriManager.uri> VARURI
156 %token <UriManager.uri * int> INDTYURI
157 %token <UriManager.uri * int * int> INDCONURI
158 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
159 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
167 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
170 | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
171 | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
172 | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
174 | DOLLAR expr DOLLAR EOF { $2 }
175 | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 }
176 | expr SEMICOLON { $1 } /* FG: to read several terms in a row
177 * Do we need to clear some static variables?
182 { [], function interp ->
183 let rec cic_int_of_int =
187 (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
192 (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
194 cic_int_of_int (n - 1)
200 { let dom1,mk_expr1 = $1 in
201 let dom2,mk_expr2 = $3 in
202 let dom = union dom1 dom2 in
203 dom, function interp ->
206 (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
212 { let dom1,mk_expr1 = $1 in
213 let dom2,mk_expr2 = $3 in
214 let dom = union dom1 dom2 in
215 dom, function interp ->
218 (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
224 { let dom1,mk_expr1 = $1 in
225 let dom2,mk_expr2 = $3 in
226 let dom3,mk_expr3 = mk_implicit () in
227 let dom = union dom1 (union dom2 dom3) in
228 dom, function interp ->
231 (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
237 | CONURI exp_named_subst
238 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
239 dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
241 | VARURI exp_named_subst
242 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
243 dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
245 | INDTYURI exp_named_subst
246 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
247 dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
249 | INDCONURI exp_named_subst
250 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
251 dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
256 Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders)
259 None -> ([], function _ -> res)
260 | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
264 let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
265 let dom = union dom1 [CicTextualParser0.Id $1] in
268 match interp (CicTextualParser0.Id $1) with
269 None -> raise (UnknownIdentifier $1)
270 | Some (CicTextualParser0.Uri uri) ->
271 term_of_uri uri (mk_exp_named_subst interp)
272 | Some CicTextualParser0.Implicit ->
273 (*CSC: not very clean; to maximize code reusage *)
274 snd (mk_implicit ()) ""
275 | Some (CicTextualParser0.Term mk_term) ->
278 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
279 { let dom1,mk_expr1 = $3 in
280 let dom2,mk_expr2 = $7 in
281 let dom3,mk_expr3 = $10 in
282 let dom = union dom1 (union dom2 dom3) in
286 (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
288 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
289 { let dom1,mk_expr1 = $3 in
290 let dom2,mk_expr2 = $7 in
291 let dom3,mk_expr3 = $10 in
293 union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3))
297 let uri,typeno = indty_uri_of_id $5 interp in
299 (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
302 | fixheader LCURLY exprseplist RCURLY
303 { let dom1,foo,ids_and_indexes,mk_types = $1 in
304 let dom2,mk_exprseplist = $3 in
305 let dom = union dom1 dom2 in
306 for i = 1 to List.length ids_and_indexes do
307 TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders
311 let types = mk_types interp in
312 let fixfunsbodies = (mk_exprseplist interp) in
316 [] -> raise Not_found
317 | (name,_)::_ when name = foo -> idx
318 | _::tl -> find (idx+1) tl
320 find 0 ids_and_indexes
323 List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
324 (List.combine ids_and_indexes types) fixfunsbodies
328 | cofixheader LCURLY exprseplist RCURLY
329 { let dom1,foo,ids,mk_types = $1 in
330 let dom2,mk_exprseplist = $3 in
331 let dom = union dom1 dom2 in
334 let types = mk_types interp in
335 let fixfunsbodies = (mk_exprseplist interp) in
339 [] -> raise Not_found
340 | name::_ when name = foo -> idx
341 | _::tl -> find (idx+1) tl
346 List.map2 (fun (name,ty) bo -> (name,ty,bo))
347 (List.combine ids types) fixfunsbodies
349 for i = 1 to List.length fixfuns do
350 TexCicTextualParser0.binders :=
351 List.tl !TexCicTextualParser0.binders
357 | SET { [], function _ -> Sort Set }
358 | PROP { [], function _ -> Sort Prop }
359 | TYPE { [], function _ -> Sort Type }
360 | LPAREN expr CAST expr RPAREN
361 { let dom1,mk_expr1 = $2 in
362 let dom2,mk_expr2 = $4 in
363 let dom = union dom1 dom2 in
364 dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
366 | META LBRACKET substitutionlist RBRACKET
367 { let dom,mk_substitutionlist = $3 in
368 dom, function interp -> Meta ($1, mk_substitutionlist interp)
370 | LPAREN expr exprlist RPAREN
371 { let length,dom2,mk_exprlist = $3 in
375 let dom1,mk_expr1 = $2 in
376 let dom = union dom1 dom2 in
379 Appl ((mk_expr1 interp)::(mk_exprlist interp))
384 | LCURLY named_substs RCURLY
389 { let dom,mk_expr = $3 in
390 dom, function interp -> [$1, mk_expr interp] }
392 { let dom1,mk_expr = $3 in
393 let dom = union [CicTextualParser0.Id $1] dom1 in
394 dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
395 | VARURI LETIN expr2 SEMICOLON named_substs
396 { let dom1,mk_expr = $3 in
397 let dom2,mk_named_substs = $5 in
398 let dom = union dom1 dom2 in
399 dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
401 | ID LETIN expr2 SEMICOLON named_substs
402 { let dom1,mk_expr = $3 in
403 let dom2,mk_named_substs = $5 in
404 let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
407 (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
412 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
413 let dom1,mk_expr1 = snd $1 in
414 let dom2,mk_expr2 = $2 in
415 let dom = union dom1 dom2 in
416 dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
419 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
420 let dom1,mk_expr1 = snd $1 in
421 let dom2,mk_expr2 = $2 in
422 let dom = union dom1 dom2 in
423 dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
426 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
427 let dom1,mk_expr1 = snd $1 in
428 let dom2,mk_expr2 = $2 in
429 let dom = union dom1 dom2 in
430 dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
436 FIX ID LCURLY fixfunsdecl RCURLY
437 { let dom,ids_and_indexes,mk_types = $4 in
439 List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
441 TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
442 dom, $2, ids_and_indexes, mk_types
446 ID LPAREN NUM RPAREN COLON expr
447 { let dom,mk_expr = $6 in
448 dom, [$1,$3], function interp -> [mk_expr interp]
450 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
451 { let dom1,mk_expr = $6 in
452 let dom2,ids_and_indexes,mk_types = $8 in
453 let dom = union dom1 dom2 in
454 dom, ($1,$3)::ids_and_indexes,
455 function interp -> (mk_expr interp)::(mk_types interp)
459 COFIX ID LCURLY cofixfunsdecl RCURLY
460 { let dom,ids,mk_types = $4 in
462 List.rev_map (function name -> Some (Name name)) ids
464 TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
465 dom, $2, ids, mk_types
470 { let dom,mk_expr = $3 in
471 dom, [$1], function interp -> [mk_expr interp]
473 | ID COLON expr SEMICOLON cofixfunsdecl
474 { let dom1,mk_expr = $3 in
475 let dom2,ids,mk_types = $5 in
476 let dom = union dom1 dom2 in
478 function interp -> (mk_expr interp)::(mk_types interp)
482 PROD ID COLON expr DOT
483 { TexCicTextualParser0.binders :=
484 (Some (Name $2))::!TexCicTextualParser0.binders;
485 let dom,mk_expr = $4 in
486 Cic.Name $2, (dom, function interp -> mk_expr interp)
489 { TexCicTextualParser0.binders :=
490 (Some Anonymous)::!TexCicTextualParser0.binders ;
491 let dom,mk_expr = $1 in
492 Anonymous, (dom, function interp -> mk_expr interp)
495 { TexCicTextualParser0.binders :=
496 (Some (Name $2))::!TexCicTextualParser0.binders;
497 let newmeta = new_meta () in
498 let new_canonical_context = [] in
500 identity_relocation_list_for_metavariable new_canonical_context
502 TexCicTextualParser0.metasenv :=
503 [newmeta, new_canonical_context, Sort Type ;
504 newmeta+1, new_canonical_context, Meta (newmeta,irl)
505 ] @ !TexCicTextualParser0.metasenv ;
506 Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
510 LAMBDA ID COLON expr DOT
511 { TexCicTextualParser0.binders :=
512 (Some (Name $2))::!TexCicTextualParser0.binders;
513 let dom,mk_expr = $4 in
514 Cic.Name $2, (dom, function interp -> mk_expr interp)
517 { TexCicTextualParser0.binders :=
518 (Some (Name $2))::!TexCicTextualParser0.binders;
519 let newmeta = new_meta () in
520 let new_canonical_context = [] in
522 identity_relocation_list_for_metavariable new_canonical_context
524 TexCicTextualParser0.metasenv :=
525 [newmeta, new_canonical_context, Sort Type ;
526 newmeta+1, new_canonical_context, Meta (newmeta,irl)
527 ] @ !TexCicTextualParser0.metasenv ;
528 Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
532 LAMBDA ID LETIN expr DOT
533 { TexCicTextualParser0.binders :=
534 (Some (Name $2))::!TexCicTextualParser0.binders ;
535 let dom,mk_expr = $4 in
536 Cic.Name $2, (dom, function interp -> mk_expr interp)
540 { [], function _ -> [] }
541 | expr SEMICOLON branches
542 { let dom1,mk_expr = $1 in
543 let dom2,mk_branches = $3 in
544 let dom = union dom1 dom2 in
545 dom, function interp -> (mk_expr interp)::(mk_branches interp)
548 { let dom,mk_expr = $1 in
549 dom, function interp -> [mk_expr interp]
554 { 0, [], function _ -> [] }
556 { let dom1,mk_expr = $1 in
557 let length,dom2,mk_exprlist = $2 in
558 let dom = union dom1 dom2 in
559 length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
564 { let dom,mk_expr = $1 in
565 dom, function interp -> [mk_expr interp]
567 | expr SEMICOLON exprseplist
568 { let dom1,mk_expr = $1 in
569 let dom2,mk_exprseplist = $3 in
570 let dom = union dom1 dom2 in
571 dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
575 { [], function _ -> [] }
576 | expr SEMICOLON substitutionlist
577 { let dom1,mk_expr = $1 in
578 let dom2,mk_substitutionlist = $3 in
579 let dom = union dom1 dom2 in
581 function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
583 | NONE SEMICOLON substitutionlist
584 { let dom,mk_exprsubstitutionlist = $3 in
585 dom, function interp -> None::(mk_exprsubstitutionlist interp)