/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Contents of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2911 - (show annotations) (download)
Thu Feb 24 01:42:53 2000 UTC (21 years, 5 months ago) by jyh
File size: 21399 byte(s)
Planning for update to .prla files.

1 (*
2 * Define a resource to evaluate toplevel expressions.
3 *
4 * ----------------------------------------------------------------
5 *
6 * This file is part of MetaPRL, a modular, higher order
7 * logical framework that provides a logical programming
8 * environment for OCaml and other languages.
9 *
10 * See the file doc/index.html for information on Nuprl,
11 * OCaml, and more information about this system.
12 *
13 * Copyright (C) 1998 Jason Hickey, Cornell University
14 *
15 * This program is free software; you can redistribute it and/or
16 * modify it under the terms of the GNU General Public License
17 * as published by the Free Software Foundation; either version 2
18 * of the License, or (at your option) any later version.
19 *
20 * This program is distributed in the hope that it will be useful,
21 * but WITHOUT ANY WARRANTY; without even the implied warranty of
22 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23 * GNU General Public License for more details.
24 *
25 * You should have received a copy of the GNU General Public License
26 * along with this program; if not, write to the Free Software
27 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28 *
29 * Author: Jason Hickey
30 * jyh@cs.cornell.edu
31 *)
32
33 open MLast
34
35 open Refiner.Refiner.TermType
36 open Refiner.Refiner.TermAddr
37 open Refiner.Refiner.RefineError
38 open Mp_resource
39
40 open Tactic_type.Tacticals
41 open Tactic_type.Conversionals
42
43 (************************************************************************
44 * TYPES *
45 ************************************************************************)
46
47 (*
48 * These are the values that we recognize.
49 *)
50 type expr =
51 (* Base types *)
52 UnitExpr of unit
53 | BoolExpr of bool
54 | IntExpr of int
55 | StringExpr of string
56 | TermExpr of term
57 | TacticExpr of tactic
58 | ConvExpr of conv
59 | AddressExpr of address
60
61 (* Uptyped tuples and functions *)
62 | ListExpr of expr list
63 | TupleExpr of expr list
64 | FunExpr of (expr -> expr)
65
66 (* Common cases are typed *)
67 | UnitFunExpr of (unit -> expr)
68 | BoolFunExpr of (bool -> expr)
69 | IntFunExpr of (int -> expr)
70 | StringFunExpr of (string -> expr)
71 | TermFunExpr of (term -> expr)
72 | TacticFunExpr of (tactic -> expr)
73 | IntTacticFunExpr of ((int -> tactic) -> expr)
74 | ConvFunExpr of (conv -> expr)
75 | AddressFunExpr of (address -> expr)
76
77 (* These functions take lists *)
78 | AddrFunExpr of (int list -> expr)
79 | StringListFunExpr of (string list -> expr)
80 | TermListFunExpr of (term list -> expr)
81 | TacticListFunExpr of (tactic list -> expr)
82 | ConvListFunExpr of (conv list -> expr)
83
84 (*
85 * The resource maps strings to values.
86 *)
87 type top_data =
88 Empty
89 | Label of string * top_data
90 | Expr of string * expr * top_data
91 | Join of top_data * top_data
92
93 type top_table =
94 (string, string * expr) Hashtbl.t
95
96 resource (string * expr, top_table, top_data, unit) toploop_resource
97
98 (************************************************************************
99 * IMPLEMENTATION *
100 ************************************************************************)
101
102 (*
103 * Construct a hash table of all the values.
104 * As in ML, the newer values override the previous.
105 *)
106 let collect_table data =
107 let hash = Hashtbl.create 201 in
108 let rec collect mod_name labels = function
109 Empty ->
110 labels
111 | (Label (mod_name, next)) as label ->
112 if List.memq label labels then
113 labels
114 else
115 collect mod_name (label :: labels) next
116 | Expr (name, expr, next) ->
117 let labels = collect mod_name labels next in
118 Hashtbl.add hash name (mod_name, expr);
119 labels
120
121 | Join (next1, next2) ->
122 let labels = collect mod_name labels next1 in
123 collect mod_name labels next2
124 in
125 let _ = collect "." [] data in
126 hash
127
128 (*
129 * Wrap up the joiner.
130 *)
131 let join_resource base1 base2 =
132 Join (base1, base2)
133
134 let extract_resource data =
135 collect_table data
136
137 let improve_resource data (name, expr) =
138 Expr (name, expr, data)
139
140 let close_resource data mod_name =
141 Label (String.capitalize mod_name, data)
142
143 (************************************************************************
144 * COMPILING *
145 ************************************************************************)
146
147 (*
148 * Right now most things are not supported.
149 *)
150 let not_supported loc str =
151 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
152
153 let type_error loc str =
154 Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))
155
156 (*
157 * Convert a list to a term list.
158 *)
159 let some_list_of_list f loc = function
160 ListExpr l ->
161 List.map f l
162 | _ ->
163 type_error loc "expr should be a list"
164
165 let term_expr loc = function
166 TermExpr t ->
167 t
168 | _ ->
169 type_error loc "expr should be a term"
170
171 let int_expr loc = function
172 IntExpr t ->
173 t
174 | _ ->
175 type_error loc "expr should be an int"
176
177 let string_expr loc = function
178 StringExpr t ->
179 t
180 | _ ->
181 type_error loc "expr should be a string"
182
183 let tactic_expr loc = function
184 TacticExpr t ->
185 t
186 | _ ->
187 type_error loc "expr should be a tactic"
188
189 let conv_expr loc = function
190 ConvExpr t ->
191 t
192 | _ ->
193 type_error loc "expr should be a conv"
194
195 let term_list_of_list loc = some_list_of_list (term_expr loc) loc
196 let int_list_of_list loc = some_list_of_list (int_expr loc) loc
197 let string_list_of_list loc = some_list_of_list (string_expr loc) loc
198 let tactic_list_of_list loc = some_list_of_list (tactic_expr loc) loc
199 let conv_list_of_list loc = some_list_of_list (conv_expr loc) loc
200
201 (*
202 * Want an int tactic.
203 *)
204 let int_tactic_expr loc = function
205 IntFunExpr f ->
206 (fun i ->
207 match f i with
208 TacticExpr tac ->
209 tac
210 | _ ->
211 type_error loc "int tactic expected")
212 | _ ->
213 type_error loc "int tactic expected"
214
215 (*
216 * Lookup a variable from the table.
217 *)
218 let rec mk_var_expr base loc v =
219 try snd (Hashtbl.find base v) with
220 Not_found ->
221 Stdpp.raise_with_loc loc (RefineError ("mk_var_expr", StringStringError ("undefined variable", v)))
222
223 and mk_proj_expr base loc expr =
224 let rec search modname v = function
225 (modname', expr) :: tl ->
226 if modname' = modname then
227 expr
228 else
229 search modname v tl
230 | [] ->
231 Stdpp.raise_with_loc loc (**)
232 (RefineError ("mk_proj_expr",
233 StringStringError ("undefined variable", modname ^ "." ^ v)))
234 in
235 let lookup names v =
236 match names with
237 [modname] ->
238 begin
239 try search modname v (Hashtbl.find_all base v) with
240 Not_found ->
241 Stdpp.raise_with_loc loc (**)
242 (RefineError ("mk_proj_expr",
243 StringStringError ("undefined variable", modname ^ "." ^ v)))
244 end
245 | _ ->
246 Stdpp.raise_with_loc loc (**)
247 (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
248 in
249 let rec collect names expr =
250 match expr with
251 (<:expr< $uid: name$ . $e2$ >>) ->
252 collect (name :: names) e2
253 | (<:expr< $lid: v$ >>) ->
254 lookup names v
255 | _ ->
256 not_supported loc "expr projection"
257 in
258 collect [] expr
259
260 (*
261 * For an application, we lookup the function and try to
262 * specialize the argument.
263 *)
264 and mk_apply_expr base loc f a =
265 let a = mk_expr base a in
266 match mk_expr base f with
267 FunExpr f ->
268 f a
269 | UnitFunExpr f ->
270 begin
271 match a with
272 UnitExpr () ->
273 f ()
274 | _ ->
275 type_error loc "expr should be unit"
276 end
277 | BoolFunExpr f ->
278 begin
279 match a with
280 BoolExpr a ->
281 f a
282 | _ ->
283 type_error loc "expr should be a bool"
284 end
285 | IntFunExpr f ->
286 begin
287 match a with
288 IntExpr a ->
289 f a
290 | _ ->
291 type_error loc "expr should be int"
292 end
293 | StringFunExpr f ->
294 begin
295 match a with
296 StringExpr a ->
297 f a
298 | _ ->
299 type_error loc "expr should be a string"
300 end
301 | TermFunExpr f ->
302 begin
303 match a with
304 TermExpr a ->
305 f a
306 | _ ->
307 type_error loc "expr should be a term"
308 end
309 | TacticFunExpr f ->
310 begin
311 match a with
312 TacticExpr a ->
313 f a
314 | _ ->
315 type_error loc "expr should be a tactic"
316 end
317 | IntTacticFunExpr f ->
318 f (int_tactic_expr loc a)
319 | ConvFunExpr f ->
320 begin
321 match a with
322 ConvExpr a ->
323 f a
324 | _ ->
325 type_error loc "expr should be a conversion"
326 end
327 | AddressFunExpr f ->
328 begin
329 match a with
330 AddressExpr a ->
331 f a
332 | _ ->
333 f (make_address (int_list_of_list loc a))
334 end
335
336 | AddrFunExpr f ->
337 f (int_list_of_list loc a)
338 | StringListFunExpr f ->
339 f (string_list_of_list loc a)
340 | TermListFunExpr f ->
341 f (term_list_of_list loc a)
342 | TacticListFunExpr f ->
343 f (tactic_list_of_list loc a)
344 | ConvListFunExpr f ->
345 f (conv_list_of_list loc a)
346 | UnitExpr _
347 | BoolExpr _
348 | IntExpr _
349 | StringExpr _
350 | TermExpr _
351 | TacticExpr _
352 | ConvExpr _
353 | AddressExpr _
354 | ListExpr _
355 | TupleExpr _ ->
356 type_error loc "expr should be a function"
357
358 (*
359 * A tuple of expressions.
360 * We only support unit for now.
361 *)
362 and mk_tuple_expr base loc = function
363 [] ->
364 UnitExpr ()
365 | _ ->
366 not_supported loc "tuple expression"
367
368 and mk_expr base expr =
369 let loc = loc_of_expr expr in
370 match expr with
371 (<:expr< $e1$ . $e2$ >> as expr) ->
372 mk_proj_expr base loc expr
373 | (<:expr< $e1$ $e2$ >>) ->
374 mk_apply_expr base loc e1 e2
375 | (<:expr< $e1$ .( $e2$ ) >>) ->
376 not_supported loc "array subscript"
377 | (<:expr< [| $list:el$ |] >>) ->
378 not_supported loc "array"
379 | (<:expr< $e1$ := $e2$ >>) ->
380 not_supported loc "assignment"
381 | (<:expr< $chr:c$ >>) ->
382 not_supported loc "char"
383 (*
384 | (<:expr< ( $e$ :> $t$ ) >>) ->
385 *)
386 | MLast.ExCoe (_, e, t) ->
387 not_supported loc "class coercion"
388 | (<:expr< $flo:s$ >>) ->
389 not_supported loc "float"
390 | (<:expr< for $s$ = $e1$ $to:b$ $e2$ do $list:el$ done >>) ->
391 not_supported loc "for loop"
392 | (<:expr< fun [ $list:pwel$ ] >>) ->
393 not_supported loc "fun"
394 | (<:expr< if $e1$ then $e2$ else $e3$ >>) ->
395 not_supported loc "ifthenelse"
396 | (<:expr< $int:s$ >>) ->
397 IntExpr (int_of_string s)
398 | (<:expr< let $rec:b$ $list:pel$ in $e$ >>) ->
399 not_supported loc "let"
400 | (<:expr< $lid:s$ >>) ->
401 mk_var_expr base loc s
402 | MLast.ExLmd _ ->
403 not_supported loc "local module"
404 | (<:expr< match $e$ with [ $list:pwel$ ] >>) ->
405 not_supported loc "match"
406 (*
407 | (<:expr< new $e$ >>) ->
408 *)
409 | MLast.ExNew _ ->
410 not_supported loc "new"
411 (*
412 | (<:expr< {< $list:sel$ >} >>) ->
413 *)
414 | MLast.ExOvr _ ->
415 not_supported loc "stream"
416 (*
417 | (<:expr< { $list:eel$ } >>) ->
418 *)
419 | MLast.ExRec _ ->
420 not_supported loc "record"
421 | (<:expr< do $list:el$ return $e$ >>) ->
422 not_supported loc "do"
423 (*
424 | (<:expr< $e$ # $i$ >>) ->
425 *)
426 | MLast.ExSnd _ ->
427 not_supported loc "class projection"
428 | (<:expr< $e1$ .[ $e2$ ] >>) ->
429 not_supported loc "string subscript"
430 | (<:expr< $str:s$ >>) ->
431 StringExpr s
432 | (<:expr< try $e$ with [ $list:pwel$ ] >>) ->
433 not_supported loc "try"
434 | (<:expr< ( $list:el$ ) >>) ->
435 mk_tuple_expr base loc el
436 | (<:expr< ( $e$ : $t$ ) >>) ->
437 mk_expr base e
438 | (<:expr< $uid:s$ >>) ->
439 mk_var_expr base loc s
440 | (<:expr< while $e$ do $list:el$ done >>) ->
441 not_supported loc "while"
442 | MLast.ExAnt (_, e) ->
443 not_supported loc "ExAnt"
444 | MLast.ExXnd (_, _, e) ->
445 mk_expr base e
446
447 and mk_patt base patt =
448 let loc = loc_of_patt patt in
449 match patt with
450 (<:patt< $p1$ . $p2$ >>) ->
451 not_supported loc "patt projection"
452 | (<:patt< ( $p1$ as $p2$ ) >>) ->
453 not_supported loc "patt"
454 | (<:patt< _ >>) ->
455 not_supported loc "wild pattern"
456 | (<:patt< $p1$ $p2$ >>) ->
457 not_supported loc "pattern application"
458 | (<:patt< [| $list: pl$ |] >>) ->
459 not_supported loc "array patterns"
460 | (<:patt< $chr:c$ >>) ->
461 not_supported loc "pattern char"
462 | (<:patt< $int:s$ >>) ->
463 not_supported loc "pattern int"
464 | (<:patt< $lid:v$ >>) ->
465 not_supported loc "pattern var"
466 | (<:patt< $p1$ | $p2$ >>) ->
467 not_supported loc "pattern choice"
468 | (<:patt< $p1$ .. $p2$ >>) ->
469 not_supported loc "pattern range"
470 | (<:patt< { $list:ppl$ } >>) ->
471 not_supported loc "pattern list"
472 | (<:patt< $str:s$ >>) ->
473 not_supported loc "pattern string"
474 | (<:patt< ( $list:pl$ ) >>) ->
475 not_supported loc "pattern list"
476 | (<:patt< ( $p$ : $t'$ ) >>) ->
477 not_supported loc "pattern cast"
478 | (<:patt< $uid:s$ >>) ->
479 not_supported loc "pattern uid"
480 | MLast.PaAnt (_, p) ->
481 not_supported loc "pattern PaAnt"
482 | MLast.PaXnd _ ->
483 not_supported loc "patterm PaXnd"
484
485 and mk_type base t =
486 let loc = loc_of_ctyp t in
487 match t with
488 (<:ctyp< $t1$ . $t2$ >>) ->
489 not_supported loc "type projection"
490 | (<:ctyp< $t1$ as $t2$ >>) ->
491 not_supported loc "type"
492 | (<:ctyp< _ >>) ->
493 not_supported loc "type wildcard"
494 | (<:ctyp< $t1$ $t2$ >>) ->
495 not_supported loc "type application"
496 | (<:ctyp< $t1$ -> $t2$ >>) ->
497 not_supported loc "type function"
498 (*
499 | (<:ctyp< # $i$ >>) ->
500 *)
501 | MLast.TyCls _ ->
502 not_supported loc "type method"
503 | (<:ctyp< $lid:s$ >>) ->
504 not_supported loc "type var"
505 | (<:ctyp< '$s$ >>) ->
506 not_supported loc "type param"
507 | (<:ctyp< $t1$ == $t2$ >>) ->
508 not_supported loc "type equality"
509 (*
510 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
511 *)
512 | MLast.TyObj (loc, _, _) ->
513 not_supported loc "type class"
514 | (<:ctyp< { $list:sbtl$ } >>) ->
515 not_supported loc "type record"
516 | (<:ctyp< [ $list:stll$ ] >>) ->
517 not_supported loc "type list"
518 | (<:ctyp< ( $list:tl$ ) >>) ->
519 not_supported loc "type product"
520 | (<:ctyp< $uid:s$ >>) ->
521 not_supported loc "type constructor var"
522 | MLast.TyXnd (_, _, t) ->
523 mk_type base t
524
525 and mk_sig_item base si =
526 let loc = loc_of_sig_item si in
527 match si with
528 (*
529 (<:sig_item< class $list:ctl$ >>) ->
530 *)
531 MLast.SgCls _
532 | MLast.SgClt _ ->
533 not_supported loc "sig class"
534 | (<:sig_item< declare $list:sil$ end >>) ->
535 mk_sig_item base (List_util.last sil)
536 | (<:sig_item< exception $s$ of $list:tl$ >>) ->
537 not_supported loc "sig exception"
538 | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
539 not_supported loc "sig external"
540 | SgInc (_, mt) ->
541 not_supported loc "sig SgInc"
542 | (<:sig_item< module $s$ : $mt$ >>) ->
543 not_supported loc "sig module"
544 | (<:sig_item< module type $s$ = $mt$ >>) ->
545 not_supported loc "sig module type"
546 | (<:sig_item< open $sl$ >>) ->
547 not_supported loc "sig open"
548 | (<:sig_item< type $list:tdl$ >>) ->
549 not_supported loc "sig type"
550 | (<:sig_item< value $s$ : $t$ >>) ->
551 not_supported loc "sig value"
552
553 and mk_str_item base si =
554 let loc = loc_of_str_item si in
555 match si with
556 (*
557 (<:str_item< class $list:cdl$ >>) ->
558 *)
559 MLast.StCls _
560 | MLast.StClt _ ->
561 not_supported loc "str class"
562 | (<:str_item< declare $list:stl$ end >>) ->
563 mk_str_item base (List_util.last stl)
564 | (<:str_item< exception $s$ of $list:tl$ >>) ->
565 not_supported loc "str exception"
566 | (<:str_item< $exp:e$ >>) ->
567 mk_expr base e
568 | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
569 not_supported loc "str external"
570 | (<:str_item< module $s$ = $me$ >>) ->
571 not_supported loc "str module"
572 | (<:str_item< module type $s$ = $mt$ >>) ->
573 not_supported loc "str module type"
574 | (<:str_item< open $sl$ >>) ->
575 not_supported loc "str module open"
576 | (<:str_item< type $list:tdl$ >>) ->
577 not_supported loc "str type"
578 | (<:str_item< value $rec:b$ $list:pel$ >>) ->
579 not_supported loc "str let"
580
581 and mk_module_type base mt =
582 let loc = loc_of_module_type mt in
583 match mt with
584 (<:module_type< $mt1$ . $mt2$ >>) ->
585 not_supported loc "module type projection"
586 | (<:module_type< $mt1$ $mt2$ >>) ->
587 not_supported loc "module type application"
588 | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
589 not_supported loc "module type functor"
590 | (<:module_type< $lid:i$ >>) ->
591 not_supported loc "module type var"
592 | (<:module_type< sig $list:sil$ end >>) ->
593 not_supported loc "module type sig"
594 | (<:module_type< $uid:i$ >>) ->
595 not_supported loc "module type var"
596 | (<:module_type< $mt$ with $list:wcl$ >>) ->
597 not_supported loc "module type constraint"
598
599 and mk_wc base = function
600 WcTyp (loc, sl1, sl2, t) ->
601 not_supported loc "with clause type"
602 | WcMod (loc, sl1, mt) ->
603 not_supported loc "with clause module"
604
605 and mk_module_expr base me =
606 let loc = loc_of_module_expr me in
607 match me with
608 (<:module_expr< $me1$ . $me2$ >>) ->
609 not_supported loc "module expr projection"
610 | (<:module_expr< $me1$ $me2$ >>) ->
611 not_supported loc "module expr application"
612 | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
613 not_supported loc "module expr functor"
614 | (<:module_expr< struct $list:sil$ end >>) ->
615 not_supported loc "module expr struct"
616 | (<:module_expr< ( $me$ : $mt$) >>) ->
617 not_supported loc "module expr type"
618 | (<:module_expr< $uid:i$ >>) ->
619 not_supported loc "module expr id"
620
621 (************************************************************************
622 * RESOURCES *
623 ************************************************************************)
624
625 (*
626 * Include the common library functions.
627 *)
628 let int_int_fun_int_expr f =
629 IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
630
631 let cons_expr =
632 FunExpr (fun e1 ->
633 FunExpr (fun e2 ->
634 match e2 with
635 ListExpr e2 ->
636 ListExpr (e1 :: e2)
637 | _ ->
638 raise (RefineError ("cons_expr", StringError "type mismatch"))))
639
640 let values =
641 ["+", int_int_fun_int_expr ( + );
642 "-", int_int_fun_int_expr ( - );
643 "*", int_int_fun_int_expr ( * );
644 "/", int_int_fun_int_expr ( / );
645 "::", cons_expr;
646 "()", UnitExpr ();
647 "[]", ListExpr [];
648 "True", BoolExpr true;
649 "False", BoolExpr false]
650
651
652 let rec add_resources base = function
653 (name, expr) :: tl ->
654 add_resources (Expr (name, expr, base)) tl
655 | [] ->
656 base
657
658 let toploop_resource =
659 Mp_resource.create (**)
660 { resource_join = join_resource;
661 resource_extract = extract_resource;
662 resource_improve = improve_resource;
663 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
664 resource_close = close_resource
665 }
666 (add_resources Empty values)
667
668 let get_resource modname =
669 Mp_resource.find toploop_resource modname
670
671 let expr_of_ocaml_expr = mk_expr
672 let expr_of_ocaml_str_item = mk_str_item
673
674 (*
675 * -*-
676 * Local Variables:
677 * Caml-master: "refiner"
678 * End:
679 * -*-
680 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26