]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_textual_parser/cicTextualParser.mly
added generation of LaTeX documentation
[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly
1 /* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  */
25
26 %{
27  open Cic;;
28  module U = UriManager;;
29
30  exception InvalidSuffix of string;;
31  exception InductiveTypeURIExpected;;
32  exception UnknownIdentifier of string;;
33  
34  let uri_of_id_map = Hashtbl.create 53;;
35
36  let get_index_in_list e =
37   let rec aux i =
38    function
39       [] -> raise Not_found
40     | (Some he)::_ when he = e -> i
41     | _::tl -> aux (i+1) tl
42   in
43    aux 1
44 ;;
45
46  let get_cookingno uri =
47   UriManager.relative_depth !CicTextualParser0.current_uri uri 0
48  ;;
49
50  (* Returns the first meta whose number is above the *)
51  (* number of the higher meta.                       *)
52  (*CSC: cut&pasted from proofEngine.ml *)
53  let new_meta () =
54   let rec aux =
55    function
56       None,[] -> 1
57     | Some n,[] -> n
58     | None,(n,_,_)::tl -> aux (Some n,tl)
59     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
60   in
61    1 + aux (None,!CicTextualParser0.metasenv)
62  ;;
63
64  (* identity_relocation_list_for_metavariable i canonical_context         *)
65  (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
66  (* where n = List.length [canonical_context]                             *)
67  (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
68  (*CSC: cut&pasted from proofEngine.ml *)
69  let identity_relocation_list_for_metavariable canonical_context =
70   let canonical_context_length = List.length canonical_context in
71    let rec aux =
72     function
73        (_,[]) -> []
74      | (n,None::tl) -> None::(aux ((n+1),tl))
75      | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
76    in
77     aux (1,canonical_context)
78  ;;
79
80 %}
81 %token <string> ID
82 %token <int> META
83 %token <int> NUM
84 %token <UriManager.uri> CONURI
85 %token <UriManager.uri * int> INDTYURI
86 %token <UriManager.uri * int * int> INDCONURI
87 %token ALIAS
88 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
89 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
90 %right ARROW
91 %start main
92 %type <Cic.term option> main
93 %%
94 main:
95    expr  { Some $1 }
96  | alias { None }
97  | EOF   { raise CicTextualParser0.Eof }
98 ;
99 expr2:
100    CONURI
101    { let uri = UriManager.string_of_uri $1 in
102      let suff = (String.sub uri (String.length uri - 3) 3) in
103       match suff with
104          "con" ->
105            let cookingno = get_cookingno $1 in
106             Const ($1,cookingno)
107        | "var" -> Var $1
108        | _ -> raise (InvalidSuffix suff)
109    }
110  | INDTYURI
111     { let cookingno = get_cookingno (fst $1) in
112        MutInd (fst $1, cookingno, snd $1) }
113  | INDCONURI
114    { let (uri,tyno,consno) = $1 in
115       let cookingno = get_cookingno uri in
116        MutConstruct (uri, cookingno, tyno, consno) }
117  | ID
118    { try
119        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
120      with
121       Not_found ->
122        try
123         Hashtbl.find uri_of_id_map $1
124        with
125         Not_found ->
126          match ! CicTextualParser0.locate_object $1 with
127           | None      -> raise (UnknownIdentifier $1)
128           | Some term -> Hashtbl.add uri_of_id_map $1 term; term  
129    }
130  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
131     { let cookingno = get_cookingno (fst $5) in
132        MutCase (fst $5, cookingno, snd $5, $7, $3, $10) }
133  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
134     { try
135        let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
136         raise InductiveTypeURIExpected
137       with
138        Not_found ->
139         match Hashtbl.find uri_of_id_map $5 with
140            MutInd (uri,cookingno,typeno) ->
141             MutCase (uri, cookingno, typeno, $7, $3, $10)
142          | _ -> raise InductiveTypeURIExpected
143     }
144  | fixheader LCURLY exprseplist RCURLY
145     { let fixfunsdecls = snd $1 in
146       let fixfunsbodies = $3 in
147        let idx =
148         let rec find idx =
149          function
150             [] -> raise Not_found
151           | (name,_,_)::_  when name = (fst $1) -> idx
152           | _::tl -> find (idx+1) tl
153         in
154          find 0 fixfunsdecls
155        in
156         let fixfuns =
157          List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
158           fixfunsdecls fixfunsbodies
159         in
160          for i = 1 to List.length fixfuns do
161           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
162          done ;
163          Fix (idx,fixfuns)
164     }
165  | cofixheader LCURLY exprseplist RCURLY
166     { let cofixfunsdecls = (snd $1) in
167       let cofixfunsbodies = $3 in
168        let idx =
169         let rec find idx =
170          function
171             [] -> raise Not_found
172           | (name,_)::_  when name = (fst $1) -> idx
173           | _::tl -> find (idx+1) tl
174         in
175          find 0 cofixfunsdecls
176        in
177         let cofixfuns =
178          List.map2 (fun (name,ty) bo -> (name,ty,bo))
179           cofixfunsdecls cofixfunsbodies
180         in
181          for i = 1 to List.length cofixfuns do
182           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
183          done ;
184          CoFix (idx,cofixfuns)
185     }
186  | IMPLICIT
187     { let newmeta = new_meta () in
188        let new_canonical_context = [] in
189         let irl =
190          identity_relocation_list_for_metavariable new_canonical_context
191         in
192          CicTextualParser0.metasenv :=
193           [newmeta, new_canonical_context, Sort Type ;
194            newmeta+1, new_canonical_context, Meta (newmeta,irl);
195            newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
196           ] @ !CicTextualParser0.metasenv ;
197          Meta (newmeta+2,irl)
198     }
199  | SET { Sort Set }
200  | PROP { Sort Prop }
201  | TYPE { Sort Type }
202  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
203  | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) } 
204  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
205 ;
206 expr :
207    pihead expr
208     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
209       Prod (fst $1, snd $1,$2) }
210  | lambdahead expr
211     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
212       Lambda (fst $1, snd $1,$2) }
213  | letinhead expr
214     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
215       LetIn (fst $1, snd $1,$2) }
216  | expr2
217     { $1 }
218 ;
219 fixheader:
220    FIX ID LCURLY fixfunsdecl RCURLY
221     { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
222        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
223        $2,$4
224     }
225 ;
226 fixfunsdecl:
227    ID LPAREN NUM RPAREN COLON expr
228     { [$1,$3,$6] }
229  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
230     { ($1,$3,$6)::$8 }
231 ;
232 cofixheader:
233    COFIX ID LCURLY cofixfunsdecl RCURLY
234     { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
235        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
236        $2,$4
237     }
238 ;
239 cofixfunsdecl:
240    ID COLON expr
241     { [$1,$3] }
242  | ID COLON expr SEMICOLON cofixfunsdecl
243     { ($1,$3)::$5 }
244 ;
245 pihead:
246    PROD ID COLON expr DOT
247     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
248       (Cic.Name $2, $4) }
249  | expr2 ARROW
250    { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
251      (Anonimous, $1) }
252  | LPAREN expr RPAREN ARROW
253    { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
254      (Anonimous, $2) }
255 ;
256 lambdahead:
257   LAMBDA ID COLON expr DOT
258    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
259      (Cic.Name $2, $4) }
260 ;
261 letinhead:
262   LAMBDA ID LETIN expr DOT
263    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
264      (Cic.Name $2, $4) }
265 ;
266 branches:
267                             { [] }
268  | expr SEMICOLON branches  { $1::$3 }
269  | expr                     { [$1] }
270 ;
271 exprlist:
272                   { [] }
273  | expr exprlist  { $1::$2 }
274 ;
275 exprseplist:
276    expr                        { [$1] }
277  | expr SEMICOLON exprseplist  { $1::$3 }
278 ;
279 substitutionlist:
280                                      { [] }
281  | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
282  | NONE SEMICOLON substitutionlist   { None::$3 }
283 ;
284 alias:
285    ALIAS ID CONURI
286     { let cookingno = get_cookingno $3 in
287        Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) }
288  | ALIAS ID INDTYURI
289     { let cookingno = get_cookingno (fst $3) in
290        Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) }
291  | ALIAS ID INDCONURI
292     { let uri,indno,consno = $3 in
293        let cookingno = get_cookingno uri in
294         Hashtbl.add uri_of_id_map $2
295          (Cic.MutConstruct (uri, cookingno, indno ,consno))
296     }
297
298
299