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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2811 - (show annotations) (download)
Fri Sep 3 23:41:50 1999 UTC (21 years, 10 months ago) by jyh
File size: 21374 byte(s)
Rules are automatically added to mptop toploop.  This just means
that you can use a rule directly in a tactic without having to wrap
it.  Rules require addresses, so they are still hard to use, but
at least they are accessible.

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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26