diff options
| author | Enrico Tassi | 2013-11-25 10:13:32 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2013-11-27 15:12:45 +0100 |
| commit | d5451ad4fc55c38ea0a7a1687dfc80c2bb0f9d13 (patch) | |
| tree | 49eabbe2d581daff058760b86708395ad997e9e4 /lib/serialize.ml | |
| parent | 217793d60211c88dbeb565a3fc62994a96a062ef (diff) | |
First stab at retrocompatible INTERP message
Diffstat (limited to 'lib/serialize.ml')
| -rw-r--r-- | lib/serialize.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index 743247faf6..37856b5279 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -572,6 +572,8 @@ type 'a call = | Quit of quit_sty | About of about_sty | Init of init_sty + (* retrocompatibility *) + | Interp of interp_sty let str_of_call = function | Add _ -> "Add" @@ -589,6 +591,7 @@ let str_of_call = function | Quit _ -> "Quit" | About _ -> "About" | Init _ -> "Init" + | Interp _ -> "Interp" type unknown @@ -607,6 +610,7 @@ let mkcases x : mkcases_rty call = MkCases x let search x : search_rty call = Search x let quit x : quit_rty call = Quit x let init x : init_rty call = Init x +let interp x : interp_rty call = Interp x let abstract_eval_call handler (c : 'a call) : 'a value = let mkGood x : 'a value = Good (Obj.magic x) in @@ -627,6 +631,7 @@ let abstract_eval_call handler (c : 'a call) : 'a value = | Quit x -> mkGood (handler.quit x) | About x -> mkGood (handler.about x) | Init x -> mkGood (handler.init x) + | Interp x -> mkGood (handler.interp x) with any -> Fail (handler.handle_exn any) @@ -648,6 +653,7 @@ let mkcases_sty_t : mkcases_sty val_t = string_t let quit_sty_t : quit_sty val_t = unit_t let about_sty_t : about_sty val_t = unit_t let init_sty_t : init_sty val_t = unit_t +let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t let add_rty_t : add_rty val_t = pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) @@ -669,6 +675,7 @@ let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) let quit_rty_t : quit_rty val_t = unit_t let about_rty_t : about_rty val_t = coq_info_t let init_rty_t : init_rty val_t = state_id_t +let interp_rty_t : interp_rty val_t = union_t string_t string_t (** brain dead code, edit if protocol messages are added/removed {{{ *) let of_answer (q : 'a call) (v : 'a value) : xml = match q with @@ -687,6 +694,7 @@ let of_answer (q : 'a call) (v : 'a value) : xml = match q with | Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v) | About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v) | Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v) + | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v) let to_answer (q : 'a call) (x : xml) : 'a value = match q with | Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x) @@ -704,6 +712,7 @@ let to_answer (q : 'a call) (x : xml) : 'a value = match q with | Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x) | About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x) | Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x) + | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x) let of_call (q : 'a call) : xml = let mkCall x = constructor "call" (str_of_call q) [x] in @@ -723,6 +732,7 @@ let of_call (q : 'a call) : xml = | Quit x -> mkCall (of_value_type quit_sty_t x) | About x -> mkCall (of_value_type about_sty_t x) | Init x -> mkCall (of_value_type init_sty_t x) + | Interp x -> mkCall (of_value_type interp_sty_t x) let to_call : xml -> unknown call = do_match "call" (fun s a -> @@ -743,6 +753,7 @@ let to_call : xml -> unknown call = | "Quit" -> Quit (mkCallArg quit_sty_t a) | "About" -> About (mkCallArg about_sty_t a) | "Init" -> Init (mkCallArg init_sty_t a) + | "Interp" -> Interp (mkCallArg interp_sty_t a) | _ -> raise Marshal_error) (* }}} *) @@ -777,6 +788,7 @@ let pr_full_value call value = match call with | Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value) | About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value) | Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value) + | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value) let pr_call call = match call with | Add x -> str_of_call call ^ " " ^ print add_sty_t x | Edit_at x -> str_of_call call ^ " " ^ print edit_at_sty_t x @@ -793,6 +805,7 @@ let pr_call call = match call with | Quit x -> str_of_call call ^ " " ^ print quit_sty_t x | About x -> str_of_call call ^ " " ^ print about_sty_t x | Init x -> str_of_call call ^ " " ^ print init_sty_t x + | Interp x -> str_of_call call ^ " " ^ print interp_sty_t x (* }}} *) |
