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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2743 - (hide annotations) (download)
Wed Jun 23 04:50:29 1999 UTC (22 years, 1 month ago) by jyh
File size: 21047 byte(s)
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

Changes:
   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or
      otherwise.

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).

Jason

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     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 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