mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Moving to Format.printf (instead of Printf and all string conversions)
This commit is contained in:
Raphaël Monat
parent
0ccae5d73b
commit
230cbada36
@ -50,11 +50,41 @@ module Variable (_ : sig end) = struct
|
||||
end
|
||||
|
||||
module BoolVariable = Variable ()
|
||||
module BoolVariableMap = Map.Make(BoolVariable)
|
||||
module BoolVariableMap =
|
||||
(struct
|
||||
include Map.Make(BoolVariable)
|
||||
|
||||
let map_printer key_printer value_printer fmt map =
|
||||
Format.fprintf fmt "{ %a }"
|
||||
(fun fmt -> iter (fun k v ->
|
||||
Format.fprintf fmt "%a ~> %a, " key_printer k value_printer v
|
||||
)) map
|
||||
end)
|
||||
module IntVariable = Variable ()
|
||||
module IntVariableMap = Map.Make(IntVariable)
|
||||
module IntVariableMap =
|
||||
(struct
|
||||
include Map.Make(IntVariable)
|
||||
|
||||
let map_printer key_printer value_printer fmt map =
|
||||
Format.fprintf fmt "{ %a }"
|
||||
(fun fmt -> iter (fun k v ->
|
||||
Format.fprintf fmt "%a ~> %a, " key_printer k value_printer v
|
||||
)) map
|
||||
end)
|
||||
|
||||
module FunctionVariable = Variable ()
|
||||
module FunctionVariableMap = Map.Make(FunctionVariable)
|
||||
module FunctionVariableMap =
|
||||
(struct
|
||||
include Map.Make(FunctionVariable)
|
||||
|
||||
let map_printer key_printer value_printer fmt map =
|
||||
Format.fprintf fmt "{ %a }"
|
||||
(fun fmt -> iter (fun k v ->
|
||||
Format.fprintf fmt "%a ~> %a, " key_printer k value_printer v
|
||||
)) map
|
||||
end)
|
||||
|
||||
|
||||
|
||||
type typ =
|
||||
| Int
|
||||
|
||||
@ -16,101 +16,115 @@ limitations under the License.
|
||||
|
||||
open Ast
|
||||
|
||||
let format_typ (t: typ) : string = match t with
|
||||
| Int -> "integer"
|
||||
| Bool -> "boolean"
|
||||
|
||||
let format_comparison_op (op : comparison_op) : string = match op with
|
||||
| Lt -> "<"
|
||||
| Lte -> "<="
|
||||
| Gt -> ">"
|
||||
| Gte -> ">="
|
||||
| Neq -> "!="
|
||||
| Eq -> "=="
|
||||
let pp_print_list_comma eldisplay fmt l =
|
||||
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ", ") eldisplay fmt l
|
||||
|
||||
let format_logical_binop (op: logical_binop) : string = match op with
|
||||
| And -> "&&"
|
||||
| Or -> "||"
|
||||
let pp_print_list_endline eldisplay fmt l =
|
||||
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n") eldisplay fmt l
|
||||
|
||||
let format_arithmetic_binop (op: arithmetic_binop) : string = match op with
|
||||
| Add -> "+"
|
||||
| Sub -> "-"
|
||||
| Mul -> "*"
|
||||
| Div -> "/"
|
||||
|
||||
let format_bool_var (b: BoolVariable.t) : string =
|
||||
Printf.sprintf "%s_%d"
|
||||
let format_typ fmt (t: typ) =
|
||||
Format.pp_print_string fmt
|
||||
(match t with
|
||||
| Int -> "integer"
|
||||
| Bool -> "boolean")
|
||||
|
||||
let format_comparison_op fmt (op : comparison_op) =
|
||||
Format.pp_print_string fmt
|
||||
(match op with
|
||||
| Lt -> "<"
|
||||
| Lte -> "<="
|
||||
| Gt -> ">"
|
||||
| Gte -> ">="
|
||||
| Neq -> "!="
|
||||
| Eq -> "==")
|
||||
|
||||
let format_logical_binop fmt (op: logical_binop) =
|
||||
Format.pp_print_string fmt
|
||||
(match op with
|
||||
| And -> "&&"
|
||||
| Or -> "||")
|
||||
|
||||
let format_arithmetic_binop fmt (op: arithmetic_binop) =
|
||||
Format.pp_print_string fmt
|
||||
(match op with
|
||||
| Add -> "+"
|
||||
| Sub -> "-"
|
||||
| Mul -> "*"
|
||||
| Div -> "/")
|
||||
|
||||
let format_bool_var fmt (b: BoolVariable.t) =
|
||||
Format.fprintf fmt "%s_%d"
|
||||
(Pos.unmark b.BoolVariable.name)
|
||||
b.BoolVariable.id
|
||||
|
||||
let format_int_var (b: IntVariable.t) : string =
|
||||
Printf.sprintf "%s_%d"
|
||||
let format_int_var fmt (b: IntVariable.t) =
|
||||
Format.fprintf fmt "%s_%d"
|
||||
(Pos.unmark b.IntVariable.name)
|
||||
b.IntVariable.id
|
||||
|
||||
let format_function_var (b: FunctionVariable.t) : string =
|
||||
Printf.sprintf "%s_%d"
|
||||
let format_function_var fmt (b: FunctionVariable.t) =
|
||||
Format.fprintf fmt "%s_%d"
|
||||
(Pos.unmark b.FunctionVariable.name)
|
||||
b.FunctionVariable.id
|
||||
|
||||
let rec format_logical_expression (e: logical_expression) : string = match e with
|
||||
let rec format_logical_expression fmt (e: logical_expression) = match e with
|
||||
| Comparison (op, e1, e2) ->
|
||||
Printf.sprintf "(%s %s %s)"
|
||||
(format_arithmetic_expression (Pos.unmark e1))
|
||||
(format_comparison_op (Pos.unmark op))
|
||||
(format_arithmetic_expression (Pos.unmark e2))
|
||||
Format.fprintf fmt "(%a %a %a)"
|
||||
format_arithmetic_expression (Pos.unmark e1)
|
||||
format_comparison_op (Pos.unmark op)
|
||||
format_arithmetic_expression (Pos.unmark e2)
|
||||
| LogicalBinop (op, e1, e2) ->
|
||||
Printf.sprintf "(%s %s %s)"
|
||||
(format_logical_expression (Pos.unmark e1))
|
||||
(format_logical_binop (Pos.unmark op))
|
||||
(format_logical_expression (Pos.unmark e2))
|
||||
Format.fprintf fmt "(%a %a %a)"
|
||||
format_logical_expression (Pos.unmark e1)
|
||||
format_logical_binop (Pos.unmark op)
|
||||
format_logical_expression (Pos.unmark e2)
|
||||
| LogicalNot e1 ->
|
||||
Printf.sprintf "!%s" (format_logical_expression (Pos.unmark e1))
|
||||
| BoolLiteral b -> string_of_bool b
|
||||
| BoolVar v -> format_bool_var v
|
||||
Format.fprintf fmt "!%a" format_logical_expression (Pos.unmark e1)
|
||||
| BoolLiteral b ->
|
||||
Format.fprintf fmt "%b" b
|
||||
| BoolVar v ->
|
||||
format_bool_var fmt v
|
||||
|
||||
and format_arithmetic_expression (e: arithmetic_expression) : string = match e with
|
||||
and format_arithmetic_expression fmt (e: arithmetic_expression) = match e with
|
||||
| ArithmeticBinop (op, e1, e2) ->
|
||||
Printf.sprintf "(%s %s %s)"
|
||||
(format_arithmetic_expression (Pos.unmark e1))
|
||||
(format_arithmetic_binop (Pos.unmark op))
|
||||
(format_arithmetic_expression (Pos.unmark e2))
|
||||
Format.fprintf fmt "(%a %a %a)"
|
||||
format_arithmetic_expression (Pos.unmark e1)
|
||||
format_arithmetic_binop (Pos.unmark op)
|
||||
format_arithmetic_expression (Pos.unmark e2)
|
||||
| Conditional (e1, e2, e3) ->
|
||||
Printf.sprintf "(if %s then %s else %s)"
|
||||
(format_logical_expression (Pos.unmark e1))
|
||||
(format_arithmetic_expression (Pos.unmark e2))
|
||||
(format_arithmetic_expression (Pos.unmark e3))
|
||||
Format.fprintf fmt "(if %a then %a else %a)"
|
||||
format_logical_expression (Pos.unmark e1)
|
||||
format_arithmetic_expression (Pos.unmark e2)
|
||||
format_arithmetic_expression (Pos.unmark e3)
|
||||
| ArithmeticMinus e1 ->
|
||||
Printf.sprintf "- %s" (format_arithmetic_expression (Pos.unmark e1))
|
||||
| IntLiteral i -> Int64.to_string i
|
||||
| IntVar v -> format_int_var v
|
||||
Format.fprintf fmt "- %a" format_arithmetic_expression (Pos.unmark e1)
|
||||
| IntLiteral i ->
|
||||
Format.pp_print_string fmt (Int64.to_string i)
|
||||
| IntVar v ->
|
||||
format_int_var fmt v
|
||||
|
||||
let format_command (c: command) : string = match c with
|
||||
let format_command fmt (c: command) = match c with
|
||||
| BoolDef (bv, e) ->
|
||||
Printf.sprintf "%s : bool := %s"
|
||||
(format_bool_var bv)
|
||||
(format_logical_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "%a : bool := %a"
|
||||
format_bool_var bv
|
||||
format_logical_expression (Pos.unmark e)
|
||||
| IntDef (iv, e) ->
|
||||
Printf.sprintf "%s : int := %s"
|
||||
(format_int_var iv)
|
||||
(format_arithmetic_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "%a : int := %a"
|
||||
format_int_var iv
|
||||
format_arithmetic_expression (Pos.unmark e)
|
||||
| Constraint e ->
|
||||
Printf.sprintf "assert(%s)"
|
||||
(format_logical_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "assert(%a)"
|
||||
format_logical_expression (Pos.unmark e)
|
||||
|
||||
let format_func (f: func) : string =
|
||||
Printf.sprintf "function(%s, %s) -> %s, %s\n%s"
|
||||
(String.concat "," (List.map (fun v -> format_int_var v) (fst f.inputs)))
|
||||
(String.concat "," (List.map (fun v -> format_bool_var v) (snd f.inputs)))
|
||||
(String.concat "," (List.map (fun v -> format_int_var v) (fst f.outputs)))
|
||||
(String.concat "," (List.map (fun v -> format_bool_var v) (snd f.outputs)))
|
||||
(String.concat "\n" (List.map (fun c -> format_command c) f.body))
|
||||
let format_func fmt (f: func) =
|
||||
Format.fprintf fmt "function(%a, %a) -> %a, %a\n%a"
|
||||
(pp_print_list_comma format_int_var) (fst f.inputs)
|
||||
(pp_print_list_comma format_bool_var) (snd f.inputs)
|
||||
(pp_print_list_comma format_int_var) (fst f.outputs)
|
||||
(pp_print_list_comma format_bool_var) (snd f.outputs)
|
||||
(pp_print_list_endline format_command) f.body
|
||||
|
||||
let format_program (p: program) : string =
|
||||
FunctionVariableMap.fold (fun fvar f acc ->
|
||||
acc ^ begin
|
||||
Printf.sprintf "%s ::= %s\n\n"
|
||||
(format_function_var fvar)
|
||||
(format_func f)
|
||||
end
|
||||
) p.program_functions ""
|
||||
let format_program fmt (p: program) =
|
||||
FunctionVariableMap.map_printer format_function_var format_func fmt p.program_functions
|
||||
|
||||
@ -35,12 +35,10 @@ let rec typecheck_logical_expression
|
||||
| BoolLiteral _ -> ()
|
||||
| BoolVar var ->
|
||||
if not (List.mem var (snd ctx.ctx_defined_variables)) then
|
||||
raise
|
||||
(Errors.VerifiscTypeError
|
||||
(Printf.sprintf "boolean variable %s used %s is undefined"
|
||||
(Pos.unmark var.BoolVariable.name)
|
||||
(Pos.format_position (Pos.get_position e))
|
||||
))
|
||||
Errors.verifisc_type_error
|
||||
"boolean variable %s used %a is undefined"
|
||||
(Pos.unmark var.BoolVariable.name)
|
||||
Pos.format_position (Pos.get_position e)
|
||||
|
||||
and typecheck_arithmetic_expression
|
||||
(e: arithmetic_expression Pos.marked)
|
||||
@ -58,12 +56,10 @@ and typecheck_arithmetic_expression
|
||||
| IntLiteral _ -> ()
|
||||
| IntVar var ->
|
||||
if not (List.mem var (fst ctx.ctx_defined_variables)) then
|
||||
raise
|
||||
(Errors.VerifiscTypeError
|
||||
(Printf.sprintf "integer variable %s used %s is undefined"
|
||||
(Pos.unmark var.IntVariable.name)
|
||||
(Pos.format_position (Pos.get_position e))
|
||||
))
|
||||
Errors.verifisc_type_error
|
||||
"integer variable %s used %a is undefined"
|
||||
(Pos.unmark var.IntVariable.name)
|
||||
Pos.format_position (Pos.get_position e)
|
||||
|
||||
let typecheck (program : program) : unit =
|
||||
FunctionVariableMap.iter (fun _ func ->
|
||||
@ -74,11 +70,10 @@ let typecheck (program : program) : unit =
|
||||
match cmd with
|
||||
| BoolDef (var, e) ->
|
||||
if List.mem var (snd ctx.ctx_defined_variables) then
|
||||
raise (Errors.VerifiscTypeError (
|
||||
Printf.sprintf "Forbidden variable redefiniton: %s %s"
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
(Pos.format_position (Pos.get_position e))
|
||||
));
|
||||
Errors.verifisc_type_error
|
||||
"Forbidden variable redefiniton: %s %a"
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
Pos.format_position (Pos.get_position e);
|
||||
typecheck_logical_expression e ctx;
|
||||
{
|
||||
ctx_defined_variables =
|
||||
@ -87,11 +82,10 @@ let typecheck (program : program) : unit =
|
||||
)}
|
||||
| IntDef (var, e) ->
|
||||
if List.mem var (fst ctx.ctx_defined_variables) then
|
||||
raise (Errors.VerifiscTypeError (
|
||||
Printf.sprintf "Forbidden variable redefiniton: %s %s"
|
||||
Errors.verifisc_type_error
|
||||
"Forbidden variable redefiniton: %s %a"
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
(Pos.format_position (Pos.get_position e))
|
||||
));
|
||||
Pos.format_position (Pos.get_position e);
|
||||
typecheck_arithmetic_expression e ctx;
|
||||
{
|
||||
ctx_defined_variables =
|
||||
@ -104,18 +98,12 @@ let typecheck (program : program) : unit =
|
||||
) ctx func.body in
|
||||
List.iter (fun output_var ->
|
||||
if not (List.mem output_var (fst ctx.ctx_defined_variables)) then
|
||||
raise
|
||||
(Errors.VerifiscTypeError
|
||||
(Printf.sprintf "integer output variable %s is undefined"
|
||||
(Pos.unmark output_var.IntVariable.name)
|
||||
))
|
||||
Errors.verifisc_type_error "integer output variable %s is undefined"
|
||||
(Pos.unmark output_var.IntVariable.name)
|
||||
) (fst func.outputs);
|
||||
List.iter (fun output_var ->
|
||||
if not (List.mem output_var (snd ctx.ctx_defined_variables)) then
|
||||
raise
|
||||
(Errors.VerifiscTypeError
|
||||
(Printf.sprintf "boolean output variable %s is undefined"
|
||||
Errors.verifisc_type_error "boolean output variable %s is undefined"
|
||||
(Pos.unmark output_var.BoolVariable.name)
|
||||
))
|
||||
) (snd func.outputs)
|
||||
) program.program_functions
|
||||
|
||||
@ -19,3 +19,11 @@ exception UnsupportedByVerifisc of string
|
||||
exception VerifiscTypeError of string
|
||||
|
||||
exception VerifiscRuntimeError of string
|
||||
|
||||
let verifisc_type_error kont =
|
||||
Format.kasprintf (fun str ->
|
||||
raise (VerifiscTypeError str)) kont
|
||||
|
||||
let verifisc_runtime_error kont =
|
||||
Format.kasprintf (fun str ->
|
||||
raise (VerifiscRuntimeError str)) kont
|
||||
|
||||
@ -16,72 +16,66 @@ limitations under the License.
|
||||
|
||||
open Ir
|
||||
|
||||
let format_int_literal (v: int_literal) : string =
|
||||
let format_int_literal fmt (v: int_literal) =
|
||||
match v with
|
||||
| Int i -> Int64.to_string i
|
||||
| IntVar var -> Format_ast.format_int_var var
|
||||
| Int i -> Format.fprintf fmt "%s" (Int64.to_string i)
|
||||
| IntVar var -> Format_ast.format_int_var fmt var
|
||||
|
||||
let format_bool_literal (v: bool_literal) : string =
|
||||
let format_bool_literal fmt (v: bool_literal) =
|
||||
match v with
|
||||
| Bool b -> string_of_bool b
|
||||
| BoolVar var -> Format_ast.format_bool_var var
|
||||
| Bool b -> Format.fprintf fmt "%b" b
|
||||
| BoolVar var -> Format_ast.format_bool_var fmt var
|
||||
|
||||
let format_logical_expression (e: logical_expression) : string = match e with
|
||||
let format_logical_expression fmt (e: logical_expression) = match e with
|
||||
| Comparison (op, v1, v2) ->
|
||||
Printf.sprintf "%s %s %s"
|
||||
(format_int_literal (Pos.unmark v1))
|
||||
(Format_ast.format_comparison_op (Pos.unmark op))
|
||||
(format_int_literal (Pos.unmark v2))
|
||||
Format.fprintf fmt "%a %a %a"
|
||||
format_int_literal (Pos.unmark v1)
|
||||
Format_ast.format_comparison_op (Pos.unmark op)
|
||||
format_int_literal (Pos.unmark v2)
|
||||
| LogicalBinop (op, v1, v2) ->
|
||||
Printf.sprintf "%s %s %s"
|
||||
(format_bool_literal (Pos.unmark v1))
|
||||
(Format_ast.format_logical_binop (Pos.unmark op))
|
||||
(format_bool_literal (Pos.unmark v2))
|
||||
Format.fprintf fmt "%a %a %a"
|
||||
format_bool_literal (Pos.unmark v1)
|
||||
Format_ast.format_logical_binop (Pos.unmark op)
|
||||
format_bool_literal (Pos.unmark v2)
|
||||
| LogicalNot v1 ->
|
||||
Printf.sprintf "!%s" (format_bool_literal (Pos.unmark v1))
|
||||
| BoolLiteral b -> format_bool_literal (Pos.unmark b)
|
||||
Format.fprintf fmt "!%a" format_bool_literal (Pos.unmark v1)
|
||||
| BoolLiteral b -> format_bool_literal fmt (Pos.unmark b)
|
||||
|
||||
let format_arithmetic_expression (e: arithmetic_expression) : string = match e with
|
||||
let format_arithmetic_expression fmt (e: arithmetic_expression) = match e with
|
||||
| ArithmeticBinop (op, v1, v2) ->
|
||||
Printf.sprintf "%s %s %s"
|
||||
(format_int_literal (Pos.unmark v1))
|
||||
(Format_ast.format_arithmetic_binop (Pos.unmark op))
|
||||
(format_int_literal (Pos.unmark v2))
|
||||
Format.fprintf fmt "%a %a %a"
|
||||
format_int_literal (Pos.unmark v1)
|
||||
Format_ast.format_arithmetic_binop (Pos.unmark op)
|
||||
format_int_literal (Pos.unmark v2)
|
||||
| Conditional (v1, v2, v3) ->
|
||||
Printf.sprintf "if %s then %s else %s"
|
||||
(format_bool_literal (Pos.unmark v1))
|
||||
(format_int_literal (Pos.unmark v2))
|
||||
(format_int_literal (Pos.unmark v3))
|
||||
Format.fprintf fmt "if %a then %a else %a"
|
||||
format_bool_literal (Pos.unmark v1)
|
||||
format_int_literal (Pos.unmark v2)
|
||||
format_int_literal (Pos.unmark v3)
|
||||
| ArithmeticMinus v1 ->
|
||||
Printf.sprintf "- %s" (format_int_literal (Pos.unmark v1))
|
||||
| IntLiteral v -> format_int_literal (Pos.unmark v)
|
||||
Format.fprintf fmt "- %a" format_int_literal (Pos.unmark v1)
|
||||
| IntLiteral v -> format_int_literal fmt (Pos.unmark v)
|
||||
|
||||
let format_command (c: command) : string = match c with
|
||||
let format_command fmt (c: command) = match c with
|
||||
| BoolDef (bv, e) ->
|
||||
Printf.sprintf "%s : bool := %s"
|
||||
(Format_ast.format_bool_var bv)
|
||||
(format_logical_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "%a : bool := %a"
|
||||
Format_ast.format_bool_var bv
|
||||
format_logical_expression (Pos.unmark e)
|
||||
| IntDef (iv, e) ->
|
||||
Printf.sprintf "%s : int := %s"
|
||||
(Format_ast.format_int_var iv)
|
||||
(format_arithmetic_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "%a : int := %a"
|
||||
Format_ast.format_int_var iv
|
||||
format_arithmetic_expression (Pos.unmark e)
|
||||
| Constraint e ->
|
||||
Printf.sprintf "assert(%s)"
|
||||
(format_logical_expression (Pos.unmark e))
|
||||
Format.fprintf fmt "assert(%a)"
|
||||
format_logical_expression (Pos.unmark e)
|
||||
|
||||
let format_func (f: func) : string =
|
||||
Printf.sprintf "function(%s, %s) -> %s, %s\n%s"
|
||||
(String.concat "," (List.map (fun v -> Format_ast.format_bool_var v) (snd f.inputs)))
|
||||
(String.concat "," (List.map (fun v -> Format_ast.format_int_var v) (fst f.inputs)))
|
||||
(String.concat "," (List.map (fun v -> Format_ast.format_int_var v) (fst f.outputs)))
|
||||
(String.concat "," (List.map (fun v -> Format_ast.format_bool_var v) (snd f.outputs)))
|
||||
(String.concat "\n" (List.map (fun c -> format_command c) f.body))
|
||||
let format_func fmt (f: func) =
|
||||
Format.fprintf fmt "function(%a, %a) -> %a, %a\n%a"
|
||||
(Format_ast.pp_print_list_comma Format_ast.format_int_var) (fst f.inputs)
|
||||
(Format_ast.pp_print_list_comma Format_ast.format_bool_var) (snd f.inputs)
|
||||
(Format_ast.pp_print_list_comma Format_ast.format_int_var) (fst f.outputs)
|
||||
(Format_ast.pp_print_list_comma Format_ast.format_bool_var) (snd f.outputs)
|
||||
(Format_ast.pp_print_list_endline format_command) f.body
|
||||
|
||||
let format_program (p: program) : string =
|
||||
Ast.FunctionVariableMap.fold (fun fvar f acc ->
|
||||
acc ^ begin
|
||||
Printf.sprintf "%s ::= %s\n\n"
|
||||
(Format_ast.format_function_var fvar)
|
||||
(format_func f)
|
||||
end
|
||||
) p.program_functions ""
|
||||
let format_program fmt (p: program) =
|
||||
Ast.FunctionVariableMap.map_printer Format_ast.format_function_var format_func fmt p.program_functions
|
||||
|
||||
@ -73,9 +73,8 @@ let interpret_arithmetic_expression (e: arithmetic_expression Pos.marked) (ctx:
|
||||
| Ast.Mul -> Int64.mul v1 v2
|
||||
| Ast.Div ->
|
||||
if v2 = Int64.zero then
|
||||
raise (Errors.VerifiscRuntimeError (
|
||||
Printf.sprintf "division by zero %s" (Pos.format_position (Pos.get_position e))
|
||||
));
|
||||
Errors.verifisc_runtime_error
|
||||
"division by zero %a" Pos.format_position (Pos.get_position e);
|
||||
Int64.div v1 v2
|
||||
end
|
||||
| ArithmeticMinus v1 ->
|
||||
@ -98,30 +97,22 @@ let interpret_command (cmd: command) (ctx: ctx) : ctx =
|
||||
{ ctx with int_values = Ast.IntVariableMap.add var v ctx.int_values }
|
||||
| Constraint e ->
|
||||
if not (interpret_logical_expression e ctx) then
|
||||
raise
|
||||
(Errors.VerifiscRuntimeError
|
||||
(Printf.sprintf "assertion violated %s"
|
||||
(Pos.format_position (Pos.get_position e))))
|
||||
Errors.verifisc_runtime_error "assertion violated %a"
|
||||
Pos.format_position (Pos.get_position e)
|
||||
else ctx
|
||||
|
||||
let interpret_function (f_var : Ast.FunctionVariable.t) (f: func) (ctx: ctx) : ctx =
|
||||
List.iter (fun var ->
|
||||
if not (Ast.IntVariableMap.mem var ctx.int_values) then
|
||||
raise
|
||||
(Errors.VerifiscRuntimeError
|
||||
(Printf.sprintf "missing input value for function %s: %s"
|
||||
(Pos.unmark f_var.Ast.FunctionVariable.name)
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
))
|
||||
Errors.verifisc_runtime_error "missing input value for function %s: %s"
|
||||
(Pos.unmark f_var.Ast.FunctionVariable.name)
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
) (fst f.inputs);
|
||||
List.iter (fun var ->
|
||||
if not (Ast.BoolVariableMap.mem var ctx.bool_values) then
|
||||
raise
|
||||
(Errors.VerifiscRuntimeError
|
||||
(Printf.sprintf "missing input value for function %s: %s"
|
||||
Errors.verifisc_runtime_error "missing input value for function %s: %s"
|
||||
(Pos.unmark f_var.Ast.FunctionVariable.name)
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
))
|
||||
) (snd f.inputs);
|
||||
let ctx = List.fold_left (fun ctx cmd ->
|
||||
interpret_command cmd ctx
|
||||
@ -129,33 +120,27 @@ let interpret_function (f_var : Ast.FunctionVariable.t) (f: func) (ctx: ctx) : c
|
||||
in
|
||||
List.iter (fun var ->
|
||||
if not (Ast.IntVariableMap.mem var ctx.int_values) then
|
||||
raise
|
||||
(Errors.VerifiscRuntimeError
|
||||
(Printf.sprintf "missing output value for function %s: %s"
|
||||
Errors.verifisc_runtime_error "missing output value for function %s: %s"
|
||||
(Pos.unmark f_var.Ast.FunctionVariable.name)
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
))
|
||||
) (fst f.outputs);
|
||||
List.iter (fun var ->
|
||||
if not (Ast.BoolVariableMap.mem var ctx.bool_values) then
|
||||
raise
|
||||
(Errors.VerifiscRuntimeError
|
||||
(Printf.sprintf "missing output value for function %s: %s"
|
||||
Errors.verifisc_runtime_error "missing output value for function %s: %s"
|
||||
(Pos.unmark f_var.Ast.FunctionVariable.name)
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
))
|
||||
) (snd f.outputs);
|
||||
ctx
|
||||
|
||||
let read_inputs_from_stdin (f: func) (mult_factor: int): ctx =
|
||||
Printf.printf "Enter the input values of the program and press [Enter]\n";
|
||||
Format.printf "Enter the input values of the program and press [Enter]@\n";
|
||||
let ctx = empty_ctx in
|
||||
let ctx = List.fold_left (fun ctx var ->
|
||||
Printf.printf "%s : float := " (Pos.unmark var.Ast.IntVariable.name);
|
||||
Format.printf "%s : float := " (Pos.unmark var.Ast.IntVariable.name);
|
||||
let input = ref None in
|
||||
while !input = None do
|
||||
match read_float_opt () with
|
||||
| None -> Printf.printf "Please enter an integer!\n"
|
||||
| None -> Format.printf "Please enter an integer!@\n"
|
||||
| Some f -> input := Some (Int64.of_float (f *. (float_of_int mult_factor)))
|
||||
done;
|
||||
match !input with
|
||||
@ -165,7 +150,7 @@ let read_inputs_from_stdin (f: func) (mult_factor: int): ctx =
|
||||
{ ctx with int_values = Ast.IntVariableMap.add var i ctx.int_values }
|
||||
) ctx (fst f.inputs) in
|
||||
let ctx = List.fold_left (fun ctx var ->
|
||||
Printf.printf "%s : bool := " (Pos.unmark var.Ast.BoolVariable.name);
|
||||
Format.printf "%s : bool := " (Pos.unmark var.Ast.BoolVariable.name);
|
||||
let input = ref None in
|
||||
while !input = None do
|
||||
let str = read_line () in
|
||||
@ -174,7 +159,7 @@ let read_inputs_from_stdin (f: func) (mult_factor: int): ctx =
|
||||
else if str = "false" then
|
||||
input := Some false
|
||||
else
|
||||
Printf.printf "Please enter an integer!\n"
|
||||
Format.printf "Please enter an integer!@\n"
|
||||
done;
|
||||
match !input with
|
||||
| None -> assert false (* should not happen *)
|
||||
@ -183,18 +168,20 @@ let read_inputs_from_stdin (f: func) (mult_factor: int): ctx =
|
||||
ctx
|
||||
|
||||
let repl_interpreter (p: program) : unit =
|
||||
Printf.printf "Here is the list of functions in the program:\n%s\n"
|
||||
(String.concat "\n" (List.map (fun (f, _) ->
|
||||
Printf.sprintf "[%d] %s (%s)"
|
||||
(f.Ast.FunctionVariable.id)
|
||||
(Pos.unmark f.Ast.FunctionVariable.name)
|
||||
(Pos.unmark f.Ast.FunctionVariable.descr)
|
||||
) (Ast.FunctionVariableMap.bindings p.program_functions)));
|
||||
Printf.printf "Please enter the number of the function you wish to execute and press [Enter]:\n";
|
||||
Format.printf "Here is the list of functions in the program:@\n%a@\n"
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
|
||||
(fun fmt (f, _) ->
|
||||
Format.fprintf fmt "[%d] %s (%s)"
|
||||
(f.Ast.FunctionVariable.id)
|
||||
(Pos.unmark f.Ast.FunctionVariable.name)
|
||||
(Pos.unmark f.Ast.FunctionVariable.descr)))
|
||||
(Ast.FunctionVariableMap.bindings p.program_functions);
|
||||
Format.printf "Please enter the number of the function you wish to execute and press [Enter]:\n";
|
||||
let input = ref None in
|
||||
while !input = None do
|
||||
match read_int_opt () with
|
||||
| None -> Printf.printf "Please enter an integer!\n"
|
||||
| None -> Format.printf "Please enter an integer!\n"
|
||||
| Some i -> input := Some i
|
||||
done;
|
||||
match !input with
|
||||
@ -208,15 +195,21 @@ let repl_interpreter (p: program) : unit =
|
||||
in
|
||||
let ctx = read_inputs_from_stdin func p.program_mult_factor in
|
||||
let ctx = interpret_function f func ctx in
|
||||
Printf.printf "Here are the functions outputs:\n";
|
||||
List.iter (fun var ->
|
||||
Printf.printf "%s : float = %f\n"
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
((Int64.to_float (Ast.IntVariableMap.find var ctx.int_values)) /.
|
||||
(float_of_int p.program_mult_factor))
|
||||
) (fst func.outputs);
|
||||
List.iter (fun var ->
|
||||
Printf.printf "%s : bool = %b\n"
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
(Ast.BoolVariableMap.find var ctx.bool_values)
|
||||
) (snd func.outputs)
|
||||
Format.printf "Here are the functions outputs:\n%a@\n%a@\n"
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
|
||||
(fun fmt var ->
|
||||
Format.fprintf fmt "%s : float = %f"
|
||||
(Pos.unmark var.Ast.IntVariable.name)
|
||||
((Int64.to_float (Ast.IntVariableMap.find var ctx.int_values)) /.
|
||||
(float_of_int p.program_mult_factor))
|
||||
))
|
||||
(fst func.outputs)
|
||||
(Format.pp_print_list
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
|
||||
(fun fmt var ->
|
||||
Format.fprintf fmt "%s : bool = %b\n"
|
||||
(Pos.unmark var.Ast.BoolVariable.name)
|
||||
(Ast.BoolVariableMap.find var ctx.bool_values)
|
||||
))
|
||||
(snd func.outputs)
|
||||
|
||||
@ -22,9 +22,9 @@ type position = {
|
||||
pos_loc: (Lexing.position * Lexing.position)
|
||||
}
|
||||
|
||||
let format_position (pos: position) : string =
|
||||
let format_position fmt (pos: position) =
|
||||
let (s, e) = pos.pos_loc in
|
||||
Printf.sprintf "in file %s, from %d:%d to %d:%d"
|
||||
Format.fprintf fmt "in file %s, from %d:%d to %d:%d"
|
||||
pos.pos_filename
|
||||
s.Lexing.pos_lnum (s.Lexing.pos_cnum - s.Lexing.pos_bol + 1)
|
||||
e.Lexing.pos_lnum (e.Lexing.pos_cnum - e.Lexing.pos_bol + 1)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user