/[mojave]/metaprl/editor/ml/nuprl_eval.ml
ViewVC logotype

Annotation of /metaprl/editor/ml/nuprl_eval.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (hide annotations) (download)
Thu Mar 16 19:52:02 2000 UTC (21 years, 4 months ago) by lolorigo
File size: 21536 byte(s)
added/improved functionality for metaprl/jprover/nuprl5 io

1 lolorigo 2922 (*
2     * This file is part of MetaPRL, a modular, higher order
3     * logical framework that provides a logical programming
4     * environment for OCaml and other languages.
5     *
6     * See the file doc/index.html for information on Nuprl,
7     * OCaml, and more information about this system.
8     *
9     * Copyright (C) 1998 Lori Lorigo, Richard Eaton, Cornell University
10     *
11     * This program is free software; you can redistribute it and/or
12     * modify it under the terms of the GNU General Public License
13     * as published by the Free Software Foundation; either version 2
14     * of the License, or (at your option) any later version.
15     *
16     * This program is distributed in the hope that it will be useful,
17     * but WITHOUT ANY WARRANTY; without even the implied warranty of
18     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19     * GNU General Public License for more details.
20     *
21     * You should have received a copy of the GNU General Public License
22     * along with this program; if not, write to the Free Software
23     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
24     *
25     * Authors: Lori Lorigo, Richard Eaton
26     *
27     *)
28    
29     (*
30     * This implements a filesystem interface to the library.
31     *)
32    
33    
34     open Refiner.Refiner.Term
35     open Refiner.Refiner.TermType
36     open Refiner.Refiner.Refine
37     open Basic
38    
39     open Utils
40     open Library
41     open Nuprl5
42    
43     open Printf
44     open Mp_debug
45     open Mp_num
46    
47     open Shell_sig
48    
49     module Shell = Shell.Shell (Shell_mp.ShellP4 (Shell_state.ShellState))
50     open Shell
51    
52     module Nuprl (*(Shell: Shell_sig.ShellSig)*) = struct
53    
54     exception LibraryException of string
55    
56     let itt_bug = ref true
57    
58     let _ =
59     show_loading "Loading Library_eval%t"
60    
61     let library = null_oref()
62     let connection = null_oref()
63    
64     let library_close () =
65     if oref_p library
66     then (leave (oref_val library);
67     disconnect (oref_val connection);
68     oref_nullify library
69     )
70     else raise (LibraryException "Close: No library open.")
71    
72     let lib_open_eval env ehook host localport remoteport =
73    
74     (* eprintf "%s %d %d %t" host localport remoteport eflush; *)
75    
76     if oref_p library
77     then raise (LibraryException "Open: Library already open.")
78     else let _ = oref_set library (join_eval (oref_set connection (connect host localport remoteport))
79     [env]
80     ehook) in
81     print_string "after join";
82     at_exit library_close (* jyh: something is strange here *)
83    
84     (*
85     *
86     * MetaPRL cmd syntax
87     *
88     * !mp_list_root{}() returns !tok_cons
89     * !mp_list_module_all{}(tok_cons) returns !cons{}(!cons(!token{thm:t}(); sequent); !cons ...
90     * !mp_list_module{}(tok_cons) returns !mp_edit{}(!cons(!token{thm:t}(); sequent); !cons ...
91     * !mp_thm_create{}(!msequent) returns !void()
92     * !mp_create_set{}(!tok_cons; sequent) returns !void()
93     * !mp_set_goal{}(!tok_cons; sequent) returns !void()
94     * !mp_lookup_proof{}(symaddr) returns !mp_prf(goal; tactic; children; extras) g and ex are sequent, ch are mp_prf
95     * !mp_refine{}(symaddr; address; tactic) returns !mp_ref(goal; subgoals; extras) g, subs and ex are sequent terms
96     * !mp_undo{}(symb) returns !mp_prf(goal; tactic; children; extras)
97     * !mp_save{}(symb) returns !void()
98     *
99     *)
100    
101     let mp_list_root_op = mk_nuprl5_op [ make_param (Token "!mp_list_root")]
102     let mp_list_display_op = mk_nuprl5_op [ make_param (Token "!mp_list_display")]
103     let mp_list_module_all_op = mk_nuprl5_op [ make_param (Token "!mp_list_module_all")]
104     let mp_list_module_op = mk_nuprl5_op [ make_param (Token "!mp_list_module")]
105     let mp_create_op = mk_nuprl5_op [ make_param (Token "!mp_create")]
106     let mp_create_rw_op = mk_nuprl5_op [ make_param (Token "!mp_create_rw")]
107     let mp_create_set_op = mk_nuprl5_op [ make_param (Token "!mp_create_set")]
108     let mp_set_goal_op = mk_nuprl5_op [ make_param (Token "!mp_set_goal")]
109     let mp_set_thm_op = mk_nuprl5_op [ make_param (Token "!mp_set_thm")]
110     let mp_set_rw_op = mk_nuprl5_op [ make_param (Token "!mp_set_rw")]
111     let mp_lookup_op = mk_nuprl5_op [ make_param (Token "!mp_lookup_proof")]
112     let mp_refine_op = mk_nuprl5_op [ make_param (Token "!mp_refine")]
113     let mp_undo_op = mk_nuprl5_op [ make_param (Token "!mp_undo")]
114     let mp_save_op = mk_nuprl5_op [ make_param (Token "!mp_save")]
115     let mp_save_thy_op = mk_nuprl5_op [ make_param (Token "!mp_save_thy")]
116     let mp_node_op = mk_nuprl5_op [ make_param (Token "!mp_node")]
117     let refiner_op = mk_nuprl5_op [ make_param (Token "!refine")]
118     let mp_compile_op = mk_nuprl5_op [ make_param (Token "!mp_compile")]
119    
120     let refine_req_p t = opeq refiner_op (operator_of_term t)
121    
122     let current_symaddr = ref []
123     let current_pair = ref ("foo", "foo")
124    
125     let refine_args t =
126     match dest_term t with
127     {term_op = op; term_terms = goal :: tac :: r } when (opeq op refiner_op)
128    
129     -> (term_of_unbound_term goal, term_of_unbound_term tac)
130    
131     | _ -> error ["eval"; "op"; "unrecognized"] [] [t]
132    
133     let iinf_sequent_op = mk_nuprl5_op [make_param (Token "!inf_sequent"); Basic.inil_parameter]
134     let iinf_sequent_term hyp term = mk_term iinf_sequent_op [(mk_bterm [] hyp); (mk_bterm [""] term)]
135    
136     let mp_prf_term g tac s e =
137     mk_term (mk_nuprl5_op [make_param (Token "!mp_prf")])
138     [(mk_bterm [] g); (mk_bterm [] tac); (mk_bterm [] s); (mk_bterm [] e)]
139    
140     let mp_edit_term w c a r =
141     mk_term (mk_nuprl5_op [make_param (Token "!mp_edit")])
142     [(mk_bterm [] w); (mk_bterm [] c); (mk_bterm [] a); (mk_bterm [] r)]
143    
144     let mp_ref_term g s e =
145     mk_term (mk_nuprl5_op [make_param (Token "!mp_ref")])
146     [(mk_bterm [] g); (mk_bterm [] s); (mk_bterm [] e)]
147    
148     let inatural_cons_op = (mk_nuprl5_op [make_param (Token "!natural_cons")])
149     let int_list_of_term_old t =
150     map_isexpr_to_list_by_op inatural_cons_op number_of_inatural_term t
151    
152     let ipui_addr_cons_op = mk_nuprl5_op [make_param (Token "!pui_addr_cons")]
153    
154     let int_list_of_term t =
155     map_isexpr_to_list_by_op ipui_addr_cons_op number_of_ipui_addr_term t
156    
157     let string_list_of_term t =
158     map_isexpr_to_list_by_op icons_op string_of_itoken_term t
159    
160     let imp_msequent_op = (mk_nuprl5_op [make_param (Token "!mp_msequent")])
161     let imp_msequent_term a g = mk_term imp_msequent_op [(mk_bterm [] a); (mk_bterm [] g)]
162     let imcons_op = (mk_nuprl5_op [make_param (Token "!mcons")])
163     let ianno_arg_cons_op = (mk_nuprl5_op [make_param (Token "!anno_arg_cons")])
164    
165     let msequent_to_term mseq =
166     let (goal, hyps) = dest_msequent mseq
167     in imp_msequent_term (list_to_ilist_by_op imcons_op hyps) goal
168    
169     let term_to_msequent t =
170     match dest_term t with
171     { term_op = imp_msequent_op; term_terms = [assums; goal]} ->
172     (map_isexpr_to_list_by_op imcons_op (let f x = x in f) (term_of_unbound_term assums),
173     (term_of_unbound_term goal))
174     | _ ->
175     raise (Refiner.Refiner.RefineError.RefineError
176     ("term_to_msequent", (Refiner.Refiner.RefineError.TermMatchError
177     (t, "malformed metasequent"))))
178    
179     let term_to_symaddr t =
180     match string_list_of_term t with
181     a::b::c::tl -> (b, c)
182     | _ ->
183     raise (Refiner.Refiner.RefineError.RefineError
184     ("term_to_symaddr", (Refiner.Refiner.RefineError.TermMatchError
185     (t, "malformed msequent"))))
186    
187     let ilist_op = (mk_nuprl5_op [make_param (Token "!list")])
188    
189     let ipair_op = (mk_nuprl5_op [make_param (Token "!pair")])
190     let ipair_term h t = mk_term ipair_op [(mk_bterm [] h); (mk_bterm [] t)]
191    
192     let list_of_ints length =
193     let rec ll len =
194     if len = 0 then []
195     else len::(ll (len - 1))
196     in List.rev (ll length)
197    
198     open List
199     open List_util
200    
201     let get_fl name shell=
202     let rec lp ls lf =
203     if ls = [] then lf
204     (*lal mapping is a hack, inneficient, but needed so union does not produce dups*)
205     else let el = List.map String.uncapitalize (edit_list_parents shell (hd ls)) in
206     lp (union el (tl ls)) (union el lf) in
207     lp [name] [name]
208    
209     let idform_op = (mk_nuprl5_op [make_param (Token "!dform")])
210     let idform_term attr lhs rhs =
211     mk_term idform_op [mk_bterm [] attr; mk_bterm [] lhs; mk_bterm [] rhs]
212    
213     let imp_prec_pair_op = (mk_nuprl5_op [make_param (Token "!mp_prec_pair")])
214     let imp_prec_pair_term lhs rhs =
215     mk_term imp_prec_pair_op [mk_bterm [] lhs; mk_bterm [] rhs]
216     let imp_prec_rel_op r = (mk_nuprl5_op [make_param (Token "!mp_prec_rel"); make_param (Token r)])
217     let imp_prec_rel_term r lhs rhs =
218     mk_term (imp_prec_rel_op r) [mk_bterm [] lhs; mk_bterm [] rhs]
219    
220     let idform_attr_op = (mk_nuprl5_op [make_param (Token "!dform_attr_cons")])
221     let imode_cons_op = (mk_nuprl5_op [make_param (Token "!mode_cons")])
222     let imp_prec_cons_op = (mk_nuprl5_op [make_param (Token "!mp_prec_cons")])
223     let imp_prec_rel_cons_op = (mk_nuprl5_op [make_param (Token "!mp_prec_rel_cons")])
224    
225     let ifail_parameter = make_param (Token "!fail")
226     let ifail_op = mk_nuprl5_op [ifail_parameter]
227     let ifail_term t = mk_term ifail_op [mk_bterm [] t]
228    
229     (*
230     let dest_rw_term t =
231     match dest_term t with
232     { term_op = imp_rw_op; term_terms = [redex; contract]} ->
233     ((term_of_unbound_term redex), (term_of_unbound_term contract))
234     | _ ->
235     raise (Refiner.Refiner.RefineError.RefineError
236     ("dest_rw_term", (Refiner.Refiner.RefineError.TermMatchError
237     (t, "malformed rw"))))
238    
239     let dest_rw_term t =
240     match dest_term t with
241     { term_op = imp_msequent_op; term_terms = [assums; goal]} ->
242     (match dest_term (term_of_unbound_term goal) with
243     { term_op = op ; term_terms = [redex; contract]} ->
244     ((term_of_unbound_term redex), (term_of_unbound_term contract))
245     | _ ->
246     raise (Refiner.Refiner.RefineError.RefineError
247     ("dest_rw_term", (Refiner.Refiner.RefineError.TermMatchError
248     ((term_of_unbound_term goal), "malformed rw")))))
249     | _ ->
250     raise (Refiner.Refiner.RefineError.RefineError
251     ("term_to_msequent", (Refiner.Refiner.RefineError.TermMatchError
252     (t, "malformed metasequent"))))
253    
254     this one if treated as proof
255     let dest_rw_term t =
256     match dest_term t with
257     { term_op = imp_msequent_op; term_terms = [assums; goal]} ->
258     (match dest_term (term_of_unbound_term goal) with
259     { term_op = op ; term_terms = [seq]} ->
260     (match dest_term (term_of_unbound_term seq) with
261     { term_op = op ; term_terms = [h]} ->
262     (match dest_term (term_of_unbound_term h) with
263     { term_op = op ; term_terms = [concl]} ->
264     (match dest_term (term_of_unbound_term concl) with
265     { term_op = op ; term_terms = [rw]} ->
266     (match dest_term (term_of_unbound_term rw) with
267     { term_op = op ; term_terms = [redex; contract]} ->
268     ((term_of_unbound_term redex), (term_of_unbound_term contract))))))
269     | _ ->
270     raise (Refiner.Refiner.RefineError.RefineError
271     ("dest_rw_term", (Refiner.Refiner.RefineError.TermMatchError
272     ((term_of_unbound_term goal), "malformed rw")))))
273     | _ ->
274     raise (Refiner.Refiner.RefineError.RefineError
275     ("term_to_msequent", (Refiner.Refiner.RefineError.TermMatchError
276     (t, "malformed metasequent"))))
277    
278     *)
279     let dest_rw_term t =
280     match dest_term t with
281     { term_op = imp_msequent_op; term_terms = [assums; goal]} ->
282     (match dest_term (term_of_unbound_term goal) with
283     { term_op = op ; term_terms = [redex; contract]} ->
284     ((term_of_unbound_term redex), (term_of_unbound_term contract))
285     | _ ->
286     raise (Refiner.Refiner.RefineError.RefineError
287     ("dest_rw_term", (Refiner.Refiner.RefineError.TermMatchError
288     ((term_of_unbound_term goal), "malformed rw")))))
289     | _ ->
290     raise (Refiner.Refiner.RefineError.RefineError
291     ("term_to_msequent", (Refiner.Refiner.RefineError.TermMatchError
292     (t, "malformed metasequent"))))
293    
294    
295    
296     let refine_ehook =
297     unconditional_error_handler
298     (function () ->
299     (function t ->
300     (* used in undo and lookup cmds *)
301    
302     let current_shell = ref (get_current_shell ()) in
303    
304     let rec visit_proof root_il =
305     let (tac, goal, subgoals, extras) = edit_node !current_shell root_il
306     in
307     (match tac with
308     Some s -> let length = List.length subgoals in
309     let vps i = visit_proof (i :: root_il) in
310     (mp_prf_term (msequent_to_term goal) (itext_term s)
311     (list_to_ilist (List.map vps (list_of_ints length)))
312     (list_to_ilist (List.map msequent_to_term extras)))
313     | None -> (mp_prf_term (msequent_to_term goal) ivoid_term inil_term
314     (list_to_ilist (List.map msequent_to_term extras))))
315     in
316     (match dest_term t with
317     {term_op = op; term_terms = symaddr :: addr :: tac :: r } when (opeq op mp_refine_op) ->
318     (let l = string_list_of_term (term_of_unbound_term symaddr)
319     in if l = !current_symaddr then ()
320     else (current_symaddr := l; edit_cd_thm !current_shell (hd (tl l)) (hd (tl (tl l))));
321     let tactic = string_of_itext_term (term_of_unbound_term tac) in
322     eprintf "%s %t" tactic eflush;
323    
324     let (gg, subgoals, extras) =
325     edit_refine !current_shell (int_list_of_term (term_of_unbound_term addr)) tactic in
326     (eprintf "after edit_refine %t" eflush;
327     mp_ref_term (msequent_to_term gg)
328     (list_to_ilist (List.map msequent_to_term subgoals))
329     (list_to_ilist_by_op ianno_arg_cons_op (List.map msequent_to_term extras))))
330    
331     (* node not needed at command call level*)
332     (*| {term_op = op; term_terms = addr :: tac :: r } when (opeq op mp_node_op) ->
333     let (goal, subgoals, extras) =
334     edit_refine !current_shell
335     (int_list_of_term (term_of_unbound_term addr))
336     (string_of_itext_term tac)
337     in
338     icons_term icons_op (msequent_to_term goal)
339     (icons_term icons_op (list_to_ilist (map msequent_to_term subgoals))
340     (list_to_ilist (List.map msequent_to_term extras)))
341     *)
342    
343     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_undo_op) ->
344     (let l = string_list_of_term (term_of_unbound_term symaddr) in
345     if l = !current_symaddr then ()
346     else (current_symaddr := l; edit_cd_thm !current_shell (hd (tl l)) (hd (tl (tl l))));
347     edit_undo !current_shell;
348     visit_proof [])
349    
350     | {term_op = op; term_terms = text :: mli_text :: r } when (opeq op mp_compile_op) ->
351     (*(Hashtbl.add Toploop.directive_table "natp1" (Toploop.Directive_int (let natp1 d = returnval := inatural_term (1 + d) in natp1)) [])*)
352     (* could have library write to file since coding for pretty printing
353     already exists *)
354     (* (output_to_file mp_compile_ml_file text;
355     output_to_file mp_compile_ml_file mli_text;
356     Unix.system "sh -c make";
357     *)
358     ivoid_term
359     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_save_op) ->
360     ((*let (b, c) = term_to_symaddr (term_of_unbound_term symaddr) in
361     if (b, c) = !current_pair then ()
362     else (current_pair := (b, c); edit_cd_thm !current_shell b c);*)
363     let l = string_list_of_term (term_of_unbound_term symaddr) in
364     if l = !current_symaddr then () else
365     (current_symaddr := l; edit_cd_thm !current_shell (hd (tl l)) (hd (tl (tl l))));
366     eprintf "saving thm %s %t" (hd (tl (tl l))) eflush;
367     save !current_shell;
368     current_shell := get_current_shell ();
369     ivoid_term)
370    
371     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_save_thy_op) ->
372     ((*let l = string_list_of_term (term_of_unbound_term symaddr) in
373     edit_save_thy !current_shell (hd (tl l));*)
374     ivoid_term)
375    
376     | {term_op = op; term_terms = [] } when (opeq op mp_list_root_op) ->
377     list_to_ilist (map itoken_term (edit_list_modules !current_shell))
378    
379     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_list_module_all_op) ->
380     let name = (hd (map_isexpr_to_list string_of_itoken_term
381     (term_of_unbound_term symaddr))) in
382     let f x = (edit_cd_thm !current_shell name x;
383     let (tac, goal, subgoals, extras) = edit_node !current_shell [] in
384     ipair_term (itoken_term x) (msequent_to_term goal))
385    
386     and flat_list = get_fl name !current_shell
387     in icons_term icons_op
388     (list_to_ilist_map itoken_term flat_list)
389     (list_to_ilist_map f (edit_list_module_all !current_shell name))
390    
391     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_list_module_op) ->
392     let name = (hd (map_isexpr_to_list string_of_itoken_term
393     (term_of_unbound_term symaddr))) in
394     let f x = (edit_cd_thm !current_shell name x;
395     let (tac, goal, subgoals, extras) = edit_node !current_shell [] in
396     ipair_term (itoken_term x) (msequent_to_term goal))
397    
398     and flat_list = get_fl name !current_shell
399     in icons_term icons_op
400     (list_to_ilist_map itoken_term flat_list)
401     (let (w, c, a, rl) = edit_list_module !current_shell name in
402     mp_edit_term (list_to_ilist_map f w) (list_to_ilist_map f c) (list_to_ilist_map f a) (list_to_ilist_map f rl))
403    
404     | {term_op = op; term_terms = symaddr :: r } when (opeq op mp_list_display_op) ->
405     let ff name =
406     let f = function (n, modes, attr, model, formats) ->
407     (ipair_term (itoken_term n)
408     (idform_term (list_to_ilist_by_op idform_attr_op
409     ((list_to_ilist_by_op imode_cons_op (map itoken_term modes)) :: attr))
410     formats
411     model))
412     in
413     ipair_term (imp_prec_pair_term (list_to_ilist_by_op imp_prec_cons_op
414     (edit_list_precs !current_shell name))
415     (list_to_ilist_by_op_map imp_prec_rel_cons_op
416     (function (r, t1, t2) -> imp_prec_rel_term r t1 t2)
417     (edit_list_prec_rels !current_shell name)))
418     (list_to_ilist (List.map f (edit_list_dforms !current_shell name)))
419     in list_to_ilist_map ff (map (function x -> hd (map_isexpr_to_list string_of_itoken_term x))
420     (map_isexpr_to_list_by_op ilist_op
421     (function x -> x) (term_of_unbound_term symaddr)))
422    
423     | {term_op = op; term_terms = symaddr :: mseq :: r} when (opeq op mp_set_thm_op) ->
424     let l = string_list_of_term (term_of_unbound_term symaddr)
425     in
426     (if l = !current_symaddr then () else edit_cd_thm !current_shell (hd (tl l)) (hd (tl (tl l)));
427     let (assums, goal) = term_to_msequent (term_of_unbound_term mseq) in
428     (eprintf "setting goal %s %s %t" (hd (tl l)) (hd (tl (tl l))) eflush;
429     eprintf "TO: %a/%t" print_term goal eflush;
430     edit_set_goal !current_shell (hd (tl l)) (hd (tl (tl l))) goal;
431     set_assumptions !current_shell assums;
432     current_shell := get_current_shell ();
433     save !current_shell;
434     current_shell := get_current_shell ();
435     ivoid_term))
436    
437     | {term_op = op; term_terms = symaddr :: rw :: r} when (opeq op mp_set_rw_op) ->
438     let l = string_list_of_term (term_of_unbound_term symaddr)
439     in
440     (if l = !current_symaddr then () else edit_cd_thm !current_shell (hd (tl l)) (hd (tl (tl l)));
441     let (redex, contract) = dest_rw_term (term_of_unbound_term rw) in
442     (eprintf "setting redex %s %s %t" (hd (tl l)) (hd (tl (tl l))) eflush;
443     eprintf "TO: %a/%a%t" print_term redex print_term contract eflush;
444     set_redex !current_shell redex; set_contractum !current_shell contract; ivoid_term)) (*use edit_set?*)
445    
446    
447     (* cd not needed at command call level*)
448     (*
449     | {term_op = op; term_terms = symaddr :: r} when (opeq op mp_cd_thm_op) ->
450     let l = string_list_of_term (term_of_unbound_term symaddr)
451     in
452     (current_symaddr := l; Shell.edit_cd_thm (hd (tl l)) (hd (tl (tl l))); ivoid_term)
453     *)
454     | {term_op = op; term_terms = mname :: name :: r} when (opeq op mp_create_op) ->
455     (edit_create_thm !current_shell (string_of_itoken_term (term_of_unbound_term mname))
456     (string_of_itoken_term (term_of_unbound_term name));
457     ivoid_term)
458    
459     | {term_op = op; term_terms = mname :: name :: r} when (opeq op mp_create_rw_op) ->
460     (edit_create_rw !current_shell (string_of_itoken_term (term_of_unbound_term mname))
461     (string_of_itoken_term (term_of_unbound_term name));
462     ivoid_term)
463    
464     | {term_op = op; term_terms = symaddr :: r} when (opeq op mp_lookup_op) ->
465     let l = string_list_of_term (term_of_unbound_term symaddr)
466     in
467     (if l = !current_symaddr then ()
468     else edit_cd_thm !current_shell (hd l) (hd (tl l));
469     visit_proof [])
470    
471    
472     (* step refine ie for rewrite tactic *)
473     (*
474     | {term_op = op; term_terms = goal :: tac :: r} when (opeq op mp_step_refine_op) ->
475     let subgoals, _ = refine (term_of_unbound_term tac) (term_of_unbound_term goal)
476     in list_to_ilist_map id subgoals
477     *)
478     | _ -> error ["eval"; "op"; "unrecognized"] [] [t])))
479    
480     (function term -> (function t -> (ifail_term term)))
481    
482    
483    
484     let library_open_eval name rhook =
485    
486     if not (oref_p library)
487     then let host = Sys.getenv "NUPRLLIB_HOST"
488     and port = int_of_string (Sys.getenv "NUPRLLIB_PORT")
489     and mport = int_of_string (Sys.getenv "MPLIB_PORT")
490     in
491     print_string "before lib_open_eval";
492     try (lib_open_eval name rhook host port mport); ()
493     with e -> (lib_open_eval name rhook host port (mport+2)); ()
494    
495    
496     let library_open_eval' port mport host name rhook =
497    
498     if not (oref_p library)
499     then lib_open_eval name rhook host port mport
500     ; ()
501    
502    
503     let library_loop_eval () =
504    
505     let lib = oref_val library in
506    
507     (with_transaction lib
508     (function t ->
509     (Library.eval t
510     (null_ap (itext_term "\l. inform_message nil ``MetaPRL Loop Start`` nil")))))
511    
512     ; server_loop lib
513    
514    
515     let library_open_and_loop_eval name rhook =
516     library_open_eval name rhook;
517     print_string "after open_eval";
518     (unwind_error
519     (function () -> library_loop_eval ();
520     library_close ())
521     (function () -> library_close ()))
522    
523    
524     let library_open_and_loop_eval' port mport host name rhook =
525    
526     library_open_eval' port mport host name rhook;
527    
528     (unwind_error
529     (function () -> library_loop_eval ();
530     library_close ())
531     (function () -> library_close ()))
532    
533    
534     let faux_refine g t =
535     print_newline();
536     Mbterm.print_term g;
537     Mbterm.print_term t;
538     print_newline();
539     [g; g]
540    
541     end
542    

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26