Source file interactive.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
open Ast
open Ast_defs
open Ast_util
open Printf
let opt_interactive = ref false
module State = struct
type istate = {
ctx : Initial_check.ctx;
ast : Type_check.typed_ast;
effect_info : Effects.side_effect_info;
env : Type_check.Env.t;
default_sail_dir : string;
config : Yojson.Safe.t option;
}
let initial_istate config default_sail_dir =
{
ctx = Initial_check.initial_ctx;
ast = empty_ast;
effect_info = Effects.empty_side_effect_info;
env = Type_check.initial_env;
default_sail_dir;
config;
}
end
open State
let arg str = "<" ^ str ^ ">" |> Util.yellow |> Util.clear
let command str = str |> Util.green |> Util.clear
type action =
| ArgString of string * (string -> action)
| ArgInt of string * (int -> action)
| Action of (State.istate -> State.istate)
| ActionUnit of (State.istate -> unit)
let commands = ref []
let get_command cmd = List.assoc_opt cmd !commands
let all_commands () = !commands
let reflect_typ action =
let open Type_check in
let rec arg_typs = function
| ArgString (_, next) -> string_typ :: arg_typs (next "")
| ArgInt (_, next) -> int_typ :: arg_typs (next 0)
| Action _ -> []
| ActionUnit _ -> []
in
match action with Action _ -> function_typ [unit_typ] unit_typ | _ -> function_typ (arg_typs action) unit_typ
let generate_help name help action =
let rec args = function
| ArgString (hint, next) -> arg hint :: args (next "")
| ArgInt (hint, next) -> arg hint :: args (next 0)
| Action _ -> []
| ActionUnit _ -> []
in
let args = args action in
let help =
match String.split_on_char ':' help with
| [] -> assert false
| prefix :: splits ->
List.map
(fun split ->
match String.split_on_char ' ' split with
| [] -> assert false
| subst :: rest ->
if Str.string_match (Str.regexp "^[0-9]+") subst 0 then (
let num_str = Str.matched_string subst in
let num_end = Str.match_end () in
let punct = String.sub subst num_end (String.length subst - num_end) in
List.nth args (int_of_string num_str) ^ punct ^ " " ^ String.concat " " rest
)
else command (":" ^ subst) ^ " " ^ String.concat " " rest
)
splits
|> String.concat ""
|> fun rest -> prefix ^ rest
in
sprintf "%s %s - %s" Util.(name |> green |> clear) (String.concat ", " args) help
let run_action istate cmd argument action =
let args = String.split_on_char ',' argument in
let rec call args action =
match (args, action) with
| x :: xs, ArgString (hint, next) -> call xs (next (String.trim x))
| x :: xs, ArgInt (hint, next) ->
let x = String.trim x in
if Str.string_match (Str.regexp "^[0-9]+$") x 0 then call xs (next (int_of_string x))
else failwith (sprintf "%s argument %s must be an non-negative integer" (command cmd) (arg hint))
| _, Action act -> act istate
| _, ActionUnit act ->
act istate;
istate
| _, _ -> failwith (sprintf "Bad arguments for %s, see (%s %s)" (command cmd) (command ":help") (command cmd))
in
call args action
let register_command ~name ~help action = commands := (":" ^ name, (help, action)) :: !commands