diff --git a/simplest_model/analyzer.ml b/simplest_model/analyzer.ml index e0a9c1e..2480d75 100644 --- a/simplest_model/analyzer.ml +++ b/simplest_model/analyzer.ml @@ -37,59 +37,61 @@ struct | ([], _) -> raise Not_found - let env_get state id = match state with + let env_get (state : state) (id : data) : data = match state with (env, _mem, _mem_len, _assignments) -> List.assoc id env - let env_add state id mem_id = match state with + let env_add (state : state) (id : data) (mem_id : data) : state = match state with (env, mem, mem_len, assignments) -> let env = (id, mem_id) :: env in (env, mem, mem_len, assignments) - let inv_id mem_len id = mem_len - id - 1 + let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1 - let mem_get state id = match state with + let mem_get (state : state) (id : data) : value = match state with (_env, mem, mem_len, _assignments) -> List.nth mem @@ inv_id mem_len @@ env_get state id - let mem_set state id value= match state with + let mem_set (state : state) (id : data) (value : value) : state = match state with (env, mem, mem_len, assignments) -> let mem_id = inv_id mem_len @@ env_get state id in let mem = list_replace mem mem_id value in (env, mem, mem_len, id :: assignments) - let mem_add state value = match state with + let mem_add (state : state) (value : value) : state = match state with (env, mem, mem_len, assignments) -> let mem = value :: mem in (env, mem, mem_len + 1, assignments) - let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state + let mem_check (state : state) (id : data) : state = + if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state - let arg_to_value state arg = match arg with + let arg_to_value (state : state) (arg : arg) : value = match arg with | RValue -> UnitV | LValue id -> mem_get state id - let st_mem_len state = + let st_mem_len (state : state) : int = match state with (_, _, mem_len, _) -> mem_len - let st_add_arg state state_before id arg_tag arg = + let st_add_arg (state : state) (state_before : state) + (id : data) (arg_tag : tag) (arg : arg) : state = match (arg_tag, arg) with | (Ref, RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *) | (Ref, LValue arg) -> env_add state id (env_get state_before arg) | (Value, arg) -> let state = mem_add state (arg_to_value state_before arg) in env_add state id (st_mem_len state - 1) - let st_spoil_assignments state = + let st_spoil_assignments (state : state) : state = match state with (env, mem, mem_len, assignments) -> (* TODO: use env var ids instead of mem_ids ?? *) (env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, []) let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs - let rec eval_stmt state prog stmt = + let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state = match stmt with | Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args) | Read id -> mem_check state id | Write id -> mem_set state id UnitV - and eval_body state prog body = + and eval_body (state : state) (prog : fun_decl list) (body : body) : state = List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body - and eval_fun state prog decl args = + and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state = match decl with (arg_tags, body) -> match state with (env_before, mem_before, len_before, assignments_before) as state_before -> let state = ([], mem_before, len_before, []) in @@ -99,14 +101,14 @@ struct match state with (_env, mem, len, _assignments) -> (env_before, list_drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *) - and eval_fun_empty_args state prog decl = + and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state = match decl with (arg_tags, _) -> let args = List.map (fun _ -> RValue) arg_tags in eval_fun state prog decl args - let empty_state = ([], [], 0, []) + let empty_state : state = ([], [], 0, []) - let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl + let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl (* tests *) diff --git a/simplest_model_with_mods/analyzer.ml b/simplest_model_with_mods/analyzer.ml index e0a9c1e..fd774f4 100644 --- a/simplest_model_with_mods/analyzer.ml +++ b/simplest_model_with_mods/analyzer.ml @@ -6,6 +6,7 @@ struct type data = int type tag = Ref | Value + type mode = Const | Mut (* TODO: add mode to func decl *) type stmt = Call of data * data list | Read of data | Write of data type body = stmt list @@ -37,59 +38,61 @@ struct | ([], _) -> raise Not_found - let env_get state id = match state with + let env_get (state : state) (id : data) : data = match state with (env, _mem, _mem_len, _assignments) -> List.assoc id env - let env_add state id mem_id = match state with + let env_add (state : state) (id : data) (mem_id : data) : state = match state with (env, mem, mem_len, assignments) -> let env = (id, mem_id) :: env in (env, mem, mem_len, assignments) - let inv_id mem_len id = mem_len - id - 1 + let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1 - let mem_get state id = match state with + let mem_get (state : state) (id : data) : value = match state with (_env, mem, mem_len, _assignments) -> List.nth mem @@ inv_id mem_len @@ env_get state id - let mem_set state id value= match state with + let mem_set (state : state) (id : data) (value : value) : state = match state with (env, mem, mem_len, assignments) -> let mem_id = inv_id mem_len @@ env_get state id in let mem = list_replace mem mem_id value in (env, mem, mem_len, id :: assignments) - let mem_add state value = match state with + let mem_add (state : state) (value : value) : state = match state with (env, mem, mem_len, assignments) -> let mem = value :: mem in (env, mem, mem_len + 1, assignments) - let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state + let mem_check (state : state) (id : data) : state = + if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state - let arg_to_value state arg = match arg with + let arg_to_value (state : state) (arg : arg) : value = match arg with | RValue -> UnitV | LValue id -> mem_get state id - let st_mem_len state = + let st_mem_len (state : state) : int = match state with (_, _, mem_len, _) -> mem_len - let st_add_arg state state_before id arg_tag arg = + let st_add_arg (state : state) (state_before : state) + (id : data) (arg_tag : tag) (arg : arg) : state = match (arg_tag, arg) with | (Ref, RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *) | (Ref, LValue arg) -> env_add state id (env_get state_before arg) | (Value, arg) -> let state = mem_add state (arg_to_value state_before arg) in env_add state id (st_mem_len state - 1) - let st_spoil_assignments state = + let st_spoil_assignments (state : state) : state = match state with (env, mem, mem_len, assignments) -> (* TODO: use env var ids instead of mem_ids ?? *) (env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, []) let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs - let rec eval_stmt state prog stmt = + let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state = match stmt with | Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args) | Read id -> mem_check state id | Write id -> mem_set state id UnitV - and eval_body state prog body = + and eval_body (state : state) (prog : fun_decl list) (body : body) : state = List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body - and eval_fun state prog decl args = + and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state = match decl with (arg_tags, body) -> match state with (env_before, mem_before, len_before, assignments_before) as state_before -> let state = ([], mem_before, len_before, []) in @@ -99,14 +102,14 @@ struct match state with (_env, mem, len, _assignments) -> (env_before, list_drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *) - and eval_fun_empty_args state prog decl = + and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state = match decl with (arg_tags, _) -> let args = List.map (fun _ -> RValue) arg_tags in eval_fun state prog decl args - let empty_state = ([], [], 0, []) + let empty_state : state = ([], [], 0, []) - let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl + let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl (* tests *)