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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2772 - (show annotations) (download)
Sun Jul 4 00:42:06 1999 UTC (22 years, 1 month ago) by nogin
File size: 21048 byte(s)
Small changes

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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26