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)
155 %token <UriManager.uri> CONURI
156 %token <UriManager.uri> VARURI
157 %token <UriManager.uri * int> INDTYURI
158 %token <UriManager.uri * int * int> INDCONURI
159 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
160 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
162 %token RPLUS RMINUS RTIMES RDIV
163 %token PLUS MINUS TIMES EQT EQ NEQT
165 %nonassoc EQ EQT NEQT
166 %left PLUS MINUS RPLUS RMINUS
167 %left TIMES RTIMES RDIV
169 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
172 | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
173 | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
174 | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
176 | DOLLAR expr DOLLAR EOF { $2 }
177 | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 }
178 | expr SEMICOLON { $1 } /* FG: to read several terms in a row
179 * Do we need to clear some static variables?
184 { [], function interp ->
185 let rec cic_real_of_real =
189 (UriManager.uri_of_string
190 "cic:/Coq/Reals/Rdefinitions/R0.con",[])
193 (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con",[])
197 (UriManager.uri_of_string
198 "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
199 Cic.Const (UriManager.uri_of_string
200 "cic:/Coq/Reals/Rdefinitions/R1.con",[]);
201 cic_real_of_real (n - 1)
207 { [], function interp ->
208 let rec cic_int_of_int =
212 (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
217 (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
219 cic_int_of_int (n - 1)
225 { let dom1,mk_expr1 = $1 in
226 let dom2,mk_expr2 = $3 in
227 let dom = union dom1 dom2 in
228 dom, function interp ->
231 (UriManager.uri_of_string
232 "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
238 { let dom1,mk_expr1 = $1 in
239 let dom2,mk_expr2 = $3 in
240 let dom = union dom1 dom2 in
241 dom, function interp ->
244 (UriManager.uri_of_string
245 "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ;
251 { let dom1,mk_expr1 = $1 in
252 let dom2,mk_expr2 = $3 in
253 let dom = union dom1 dom2 in
254 dom, function interp ->
257 (UriManager.uri_of_string
258 "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ;
264 { let dom1,mk_expr1 = $1 in
265 let dom2,mk_expr2 = $3 in
266 let dom = union dom1 dom2 in
267 dom, function interp ->
270 (UriManager.uri_of_string
271 "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ;
277 { let dom1,mk_expr1 = $1 in
278 let dom2,mk_expr2 = $3 in
279 let dom = union dom1 dom2 in
280 dom, function interp ->
283 (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
289 { let dom1,mk_expr1 = $1 in
290 let dom2,mk_expr2 = $3 in
291 let dom = union dom1 dom2 in
292 dom, function interp ->
295 (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
301 { let dom1,mk_expr1 = $1 in
302 let dom2,mk_expr2 = $3 in
303 let dom = union dom1 dom2 in
304 dom, function interp ->
307 (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
313 { let dom1,mk_expr1 = $1 in
314 let dom2,mk_expr2 = $3 in
315 let dom3,mk_expr3 = mk_implicit () in
316 let dom = union dom1 (union dom2 dom3) in
317 dom, function interp ->
320 (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
327 { let dom1,mk_expr1 = $1 in
328 let dom2,mk_expr2 = $3 in
329 let dom3,mk_expr3 = mk_implicit () in
330 let dom = union dom1 (union dom2 dom3) in
331 dom, function interp ->
333 Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]);
336 (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
343 { let dom1,mk_expr1 = $1 in
344 let dom2,mk_expr2 = $3 in
345 let dom3,mk_expr3 = mk_implicit () in
346 let dom = union dom1 (union dom2 dom3) in
347 dom, function interp ->
350 (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
356 | CONURI exp_named_subst
357 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
358 dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
360 | VARURI exp_named_subst
361 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
362 dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
364 | INDTYURI exp_named_subst
365 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
366 dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
368 | INDCONURI exp_named_subst
369 { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
370 dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
375 Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders)
378 None -> ([], function _ -> res)
379 | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
383 let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
384 let dom = union dom1 [CicTextualParser0.Id $1] in
387 match interp (CicTextualParser0.Id $1) with
388 None -> raise (UnknownIdentifier $1)
389 | Some (CicTextualParser0.Uri uri) ->
390 term_of_uri uri (mk_exp_named_subst interp)
391 | Some CicTextualParser0.Implicit ->
392 (*CSC: not very clean; to maximize code reusage *)
393 snd (mk_implicit ()) ""
394 | Some (CicTextualParser0.Term mk_term) ->
397 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
398 { let dom1,mk_expr1 = $3 in
399 let dom2,mk_expr2 = $7 in
400 let dom3,mk_expr3 = $10 in
401 let dom = union dom1 (union dom2 dom3) in
405 (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
407 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
408 { let dom1,mk_expr1 = $3 in
409 let dom2,mk_expr2 = $7 in
410 let dom3,mk_expr3 = $10 in
412 union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3))
416 let uri,typeno = indty_uri_of_id $5 interp in
418 (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
421 | fixheader LCURLY exprseplist RCURLY
422 { let dom1,foo,ids_and_indexes,mk_types = $1 in
423 let dom2,mk_exprseplist = $3 in
424 let dom = union dom1 dom2 in
425 for i = 1 to List.length ids_and_indexes do
426 TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders
430 let types = mk_types interp in
431 let fixfunsbodies = (mk_exprseplist interp) in
435 [] -> raise Not_found
436 | (name,_)::_ when name = foo -> idx
437 | _::tl -> find (idx+1) tl
439 find 0 ids_and_indexes
442 List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
443 (List.combine ids_and_indexes types) fixfunsbodies
447 | cofixheader LCURLY exprseplist RCURLY
448 { let dom1,foo,ids,mk_types = $1 in
449 let dom2,mk_exprseplist = $3 in
450 let dom = union dom1 dom2 in
453 let types = mk_types interp in
454 let fixfunsbodies = (mk_exprseplist interp) in
458 [] -> raise Not_found
459 | name::_ when name = foo -> idx
460 | _::tl -> find (idx+1) tl
465 List.map2 (fun (name,ty) bo -> (name,ty,bo))
466 (List.combine ids types) fixfunsbodies
468 for i = 1 to List.length fixfuns do
469 TexCicTextualParser0.binders :=
470 List.tl !TexCicTextualParser0.binders
476 | SET { [], function _ -> Sort Set }
477 | PROP { [], function _ -> Sort Prop }
478 | TYPE { [], function _ -> Sort Type }
479 | LPAREN expr CAST expr RPAREN
480 { let dom1,mk_expr1 = $2 in
481 let dom2,mk_expr2 = $4 in
482 let dom = union dom1 dom2 in
483 dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
485 | META LBRACKET substitutionlist RBRACKET
486 { let dom,mk_substitutionlist = $3 in
487 dom, function interp -> Meta ($1, mk_substitutionlist interp)
489 | LPAREN expr exprlist RPAREN
490 { let length,dom2,mk_exprlist = $3 in
494 let dom1,mk_expr1 = $2 in
495 let dom = union dom1 dom2 in
498 Appl ((mk_expr1 interp)::(mk_exprlist interp))
503 | LCURLY named_substs RCURLY
508 { let dom,mk_expr = $3 in
509 dom, function interp -> [$1, mk_expr interp] }
511 { let dom1,mk_expr = $3 in
512 let dom = union [CicTextualParser0.Id $1] dom1 in
513 dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
514 | VARURI LETIN expr2 SEMICOLON named_substs
515 { let dom1,mk_expr = $3 in
516 let dom2,mk_named_substs = $5 in
517 let dom = union dom1 dom2 in
518 dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
520 | ID LETIN expr2 SEMICOLON named_substs
521 { let dom1,mk_expr = $3 in
522 let dom2,mk_named_substs = $5 in
523 let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
526 (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
531 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
532 let dom1,mk_expr1 = snd $1 in
533 let dom2,mk_expr2 = $2 in
534 let dom = union dom1 dom2 in
535 dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
538 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
539 let dom1,mk_expr1 = snd $1 in
540 let dom2,mk_expr2 = $2 in
541 let dom = union dom1 dom2 in
542 dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
545 { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
546 let dom1,mk_expr1 = snd $1 in
547 let dom2,mk_expr2 = $2 in
548 let dom = union dom1 dom2 in
549 dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
555 FIX ID LCURLY fixfunsdecl RCURLY
556 { let dom,ids_and_indexes,mk_types = $4 in
558 List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
560 TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
561 dom, $2, ids_and_indexes, mk_types
565 ID LPAREN NUM RPAREN COLON expr
566 { let dom,mk_expr = $6 in
567 dom, [$1,$3], function interp -> [mk_expr interp]
569 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
570 { let dom1,mk_expr = $6 in
571 let dom2,ids_and_indexes,mk_types = $8 in
572 let dom = union dom1 dom2 in
573 dom, ($1,$3)::ids_and_indexes,
574 function interp -> (mk_expr interp)::(mk_types interp)
578 COFIX ID LCURLY cofixfunsdecl RCURLY
579 { let dom,ids,mk_types = $4 in
581 List.rev_map (function name -> Some (Name name)) ids
583 TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
584 dom, $2, ids, mk_types
589 { let dom,mk_expr = $3 in
590 dom, [$1], function interp -> [mk_expr interp]
592 | ID COLON expr SEMICOLON cofixfunsdecl
593 { let dom1,mk_expr = $3 in
594 let dom2,ids,mk_types = $5 in
595 let dom = union dom1 dom2 in
597 function interp -> (mk_expr interp)::(mk_types interp)
601 PROD ID COLON expr DOT
602 { TexCicTextualParser0.binders :=
603 (Some (Name $2))::!TexCicTextualParser0.binders;
604 let dom,mk_expr = $4 in
605 Cic.Name $2, (dom, function interp -> mk_expr interp)
608 { TexCicTextualParser0.binders :=
609 (Some Anonymous)::!TexCicTextualParser0.binders ;
610 let dom,mk_expr = $1 in
611 Anonymous, (dom, function interp -> mk_expr interp)
614 { TexCicTextualParser0.binders :=
615 (Some (Name $2))::!TexCicTextualParser0.binders;
616 let newmeta = new_meta () in
617 let new_canonical_context = [] in
619 identity_relocation_list_for_metavariable new_canonical_context
621 TexCicTextualParser0.metasenv :=
622 [newmeta, new_canonical_context, Sort Type ;
623 newmeta+1, new_canonical_context, Meta (newmeta,irl)
624 ] @ !TexCicTextualParser0.metasenv ;
625 Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
629 LAMBDA ID COLON expr DOT
630 { TexCicTextualParser0.binders :=
631 (Some (Name $2))::!TexCicTextualParser0.binders;
632 let dom,mk_expr = $4 in
633 Cic.Name $2, (dom, function interp -> mk_expr interp)
636 { TexCicTextualParser0.binders :=
637 (Some (Name $2))::!TexCicTextualParser0.binders;
638 let newmeta = new_meta () in
639 let new_canonical_context = [] in
641 identity_relocation_list_for_metavariable new_canonical_context
643 TexCicTextualParser0.metasenv :=
644 [newmeta, new_canonical_context, Sort Type ;
645 newmeta+1, new_canonical_context, Meta (newmeta,irl)
646 ] @ !TexCicTextualParser0.metasenv ;
647 Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
651 LAMBDA ID LETIN expr DOT
652 { TexCicTextualParser0.binders :=
653 (Some (Name $2))::!TexCicTextualParser0.binders ;
654 let dom,mk_expr = $4 in
655 Cic.Name $2, (dom, function interp -> mk_expr interp)
659 { [], function _ -> [] }
660 | expr SEMICOLON branches
661 { let dom1,mk_expr = $1 in
662 let dom2,mk_branches = $3 in
663 let dom = union dom1 dom2 in
664 dom, function interp -> (mk_expr interp)::(mk_branches interp)
667 { let dom,mk_expr = $1 in
668 dom, function interp -> [mk_expr interp]
673 { 0, [], function _ -> [] }
675 { let dom1,mk_expr = $1 in
676 let length,dom2,mk_exprlist = $2 in
677 let dom = union dom1 dom2 in
678 length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
683 { let dom,mk_expr = $1 in
684 dom, function interp -> [mk_expr interp]
686 | expr SEMICOLON exprseplist
687 { let dom1,mk_expr = $1 in
688 let dom2,mk_exprseplist = $3 in
689 let dom = union dom1 dom2 in
690 dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
694 { [], function _ -> [] }
695 | expr SEMICOLON substitutionlist
696 { let dom1,mk_expr = $1 in
697 let dom2,mk_substitutionlist = $3 in
698 let dom = union dom1 dom2 in
700 function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
702 | NONE SEMICOLON substitutionlist
703 { let dom,mk_exprsubstitutionlist = $3 in
704 dom, function interp -> None::(mk_exprsubstitutionlist interp)