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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2743 - (show 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 (*
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