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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2549 - (show annotations) (download)
Fri Jan 1 20:14:13 1999 UTC (22 years, 7 months ago) by jyh
File size: 22187 byte(s)
Fixed up "make clean" to remove more files.
The directory should be like a new checkout afterwards.
Enabled set_debug function in toploop.  You can
turn on debugging with

# set_debug "xxx" true;;

for some debug variable xxx.

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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26