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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2811 - (hide 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 jyh 2494 (*
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 jyh 2525 *
15 jyh 2494 * 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 jyh 2525 *
20 jyh 2494 * 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 jyh 2525 *
25 jyh 2494 * 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 jyh 2525 *
29 jyh 2494 * 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 jyh 2743 open Tactic_type.Tacticals
40     open Tactic_type.Conversionals
41 jyh 2494
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 jyh 2811 | AddressExpr of address
59 jyh 2494
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 jyh 2811 | AddressFunExpr of (address -> expr)
75 jyh 2494
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 jyh 2630 resource (string * expr, top_table, top_data, unit) toploop_resource
96 jyh 2494
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 jyh 2577 let _ = collect "." [] data in
125 jyh 2494 hash
126    
127     (*
128     * Wrap up the joiner.
129     *)
130 jyh 2629 let join_resource base1 base2 =
131     Join (base1, base2)
132 jyh 2494
133 jyh 2629 let extract_resource data =
134 jyh 2494 collect_table data
135    
136 jyh 2629 let improve_resource data (name, expr) =
137     Expr (name, expr, data)
138 jyh 2494
139 jyh 2629 let close_resource data mod_name =
140     Label (String.capitalize mod_name, data)
141 jyh 2494
142     (************************************************************************
143     * COMPILING *
144     ************************************************************************)
145    
146     (*
147     * Right now most things are not supported.
148     *)
149     let not_supported loc str =
150 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
151 jyh 2494
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 nogin 2772 collect (name :: names) e2
252 jyh 2494 | (<: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 jyh 2811 | 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 jyh 2494
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 jyh 2811 | AddressExpr _
353 jyh 2494 | 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 jyh 2525 mk_var_expr base loc s
439 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
440     not_supported loc "while"
441     | MLast.ExAnt (_, e) ->
442     not_supported loc "ExAnt"
443 jyh 2629 | MLast.ExXnd (_, _, e) ->
444     mk_expr base e
445 jyh 2494
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 jyh 2629 | MLast.PaXnd _ ->
482     not_supported loc "patterm PaXnd"
483 jyh 2494
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 jyh 2577 (*
509 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
510 jyh 2577 *)
511     | MLast.TyObj (loc, _, _) ->
512 jyh 2494 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 jyh 2629 | MLast.TyXnd (_, _, t) ->
522     mk_type base t
523 jyh 2494
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 jyh 2525 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 jyh 2494 let values =
640     ["+", int_int_fun_int_expr ( + );
641     "-", int_int_fun_int_expr ( - );
642     "*", int_int_fun_int_expr ( * );
643 jyh 2525 "/", int_int_fun_int_expr ( / );
644     "::", cons_expr;
645     "()", UnitExpr ();
646     "[]", ListExpr [];
647 jyh 2549 "True", BoolExpr true;
648     "False", BoolExpr false]
649 jyh 2494
650 jyh 2525
651 jyh 2494 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 jyh 2629 Mp_resource.create (**)
659     { resource_join = join_resource;
660     resource_extract = extract_resource;
661     resource_improve = improve_resource;
662 jyh 2630 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
663 jyh 2629 resource_close = close_resource
664     }
665     (add_resources Empty values)
666 jyh 2494
667 jyh 2629 let get_resource modname =
668     Mp_resource.find toploop_resource modname
669 jyh 2494
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