path: root/abstract/interpret.ml

open Abstract_syntax_tree
open Environment_domain
open Util

module Make (E : ENVIRONMENT_DOMAIN) = struct

	let neg (e, l) =
		(AST_unary(AST_NOT, (e, l))), l

	let rec condition cond env =
		begin match fst cond with
		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
			E.compare env e1 e2
		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
			E.compare env e2 e1
		| AST_binary (AST_AND, e1, e2) ->
			E.meet (condition e1 env) (condition e2 env)
		| AST_binary (AST_OR, e1, e2) ->
			E.join (condition e1 env) (condition e2 env)
		| _ -> env (* TODO : encode some transformations *)
		end

	let rec interp_stmt env stat =
		begin match fst stat with
		| AST_block b ->
			List.fold_left interp_stmt env b
		| AST_assign ((id, _), exp) ->
			E.assign env id exp
		| AST_if (cond, tb, None) ->
			E.join
				(interp_stmt (condition cond env) tb)
				(condition (neg cond) env)
		| AST_if (cond, tb, Some eb) ->
			E.join
				(interp_stmt (condition cond env) tb)
				(interp_stmt (condition (neg cond) env) eb)
		| AST_while (cond, (body, _)) ->
			(* TODO *)
			env
		| AST_HALT -> E.bottom
		| AST_assert (cond, l) ->
			(* TODO *)
			env
		| AST_print items ->
			(* TODO *)
			env
		| _ -> assert false (* not implemented *)
		end
	
	let interpret prog =
		List.fold_left
			(fun env x -> match x with
				| AST_stat st -> interp_stmt env st
				| _ -> env)
			E.init
			(fst prog)
end