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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2772 - (hide 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 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    
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 jyh 2630 resource (string * expr, top_table, top_data, unit) toploop_resource
94 jyh 2494
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 jyh 2577 let _ = collect "." [] data in
123 jyh 2494 hash
124    
125     (*
126     * Wrap up the joiner.
127     *)
128 jyh 2629 let join_resource base1 base2 =
129     Join (base1, base2)
130 jyh 2494
131 jyh 2629 let extract_resource data =
132 jyh 2494 collect_table data
133    
134 jyh 2629 let improve_resource data (name, expr) =
135     Expr (name, expr, data)
136 jyh 2494
137 jyh 2629 let close_resource data mod_name =
138     Label (String.capitalize mod_name, data)
139 jyh 2494
140     (************************************************************************
141     * COMPILING *
142     ************************************************************************)
143    
144     (*
145     * Right now most things are not supported.
146     *)
147     let not_supported loc str =
148 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
149 jyh 2494
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 nogin 2772 collect (name :: names) e2
250 jyh 2494 | (<: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 jyh 2525 mk_var_expr base loc s
428 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
429     not_supported loc "while"
430     | MLast.ExAnt (_, e) ->
431     not_supported loc "ExAnt"
432 jyh 2629 | MLast.ExXnd (_, _, e) ->
433     mk_expr base e
434 jyh 2494
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 jyh 2629 | MLast.PaXnd _ ->
471     not_supported loc "patterm PaXnd"
472 jyh 2494
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 jyh 2577 (*
498 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
499 jyh 2577 *)
500     | MLast.TyObj (loc, _, _) ->
501 jyh 2494 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 jyh 2629 | MLast.TyXnd (_, _, t) ->
511     mk_type base t
512 jyh 2494
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 jyh 2525 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 jyh 2494 let values =
629     ["+", int_int_fun_int_expr ( + );
630     "-", int_int_fun_int_expr ( - );
631     "*", int_int_fun_int_expr ( * );
632 jyh 2525 "/", int_int_fun_int_expr ( / );
633     "::", cons_expr;
634     "()", UnitExpr ();
635     "[]", ListExpr [];
636 jyh 2549 "True", BoolExpr true;
637     "False", BoolExpr false]
638 jyh 2494
639 jyh 2525
640 jyh 2494 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 jyh 2629 Mp_resource.create (**)
648     { resource_join = join_resource;
649     resource_extract = extract_resource;
650     resource_improve = improve_resource;
651 jyh 2630 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
652 jyh 2629 resource_close = close_resource
653     }
654     (add_resources Empty values)
655 jyh 2494
656 jyh 2629 let get_resource modname =
657     Mp_resource.find toploop_resource modname
658 jyh 2494
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