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

Contents of /metaprl/editor/ml/nuprl_eval.ml

Parent Directory Parent Directory | Revision Log Revision Log


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