diff --git a/lib/miniFun.ml b/lib/miniFun.ml index 35d2b98..4cc388a 100644 --- a/lib/miniFun.ml +++ b/lib/miniFun.ml @@ -2,11 +2,16 @@ type variable = string module VariableMap = Map.Make(String) +type ftype = + IntegerType + | BooleanType + | FunctionType of ftype list * ftype + type t_exp = Integer of int | Boolean of bool | Variable of variable - | Function of variable list * t_exp + | Function of variable list * ftype * t_exp | Application of t_exp * t_exp list | Plus of t_exp * t_exp | Minus of t_exp * t_exp @@ -26,7 +31,7 @@ type t_exp = | CmpGreaterEq of t_exp * t_exp | IfThenElse of t_exp * t_exp * t_exp | LetIn of variable * t_exp * t_exp - | LetFun of variable * variable list * t_exp * t_exp + | LetFun of variable * variable list * ftype * t_exp * t_exp type permittedValues = IntegerPermitted of int @@ -47,6 +52,7 @@ exception AbsentAssignment of string exception WrongType of string exception DivisionByZero of string exception WrongAriety of string +exception WrongTypeSpecification of string module Utility = Utility;; @@ -63,7 +69,7 @@ let rec evaluate (mem: memory) (command: t_exp) = " is not defined.")) | Some a -> a ) - | Function (xs, f) -> + | Function (xs, _, f) -> (FunctionPermitted {inputList = xs; body = f; @@ -335,7 +341,7 @@ let rec evaluate (mem: memory) (command: t_exp) = let evalxval = evaluate mem xval in let mem2 = {assignments = VariableMap.add x evalxval mem.assignments} in evaluate mem2 rest - | LetFun (f, xs, fbody, rest) -> + | LetFun (f, xs, _, fbody, rest) -> let mem2 = { assignments = VariableMap.add @@ -356,3 +362,127 @@ let reduce (program: t_exp) (iin : int) = match (evaluate mem program') with IntegerPermitted a -> a | _ -> raise (WrongType ("Main function doesn't return an integer")) + + + + +let rec evaluate_type (program: t_exp) context = + match program with + Integer _ -> IntegerType + | Boolean _ -> BooleanType + | Variable x -> (match VariableMap.find_opt x context with + None -> raise (AbsentAssignment ("The variable " ^ x ^ " is not defined.")) + | Some t -> t) + | Function (xs, typef, fbody) -> ( + match typef with + FunctionType (tin, tout) -> ( + if List.length xs != List.length tin then + raise (WrongTypeSpecification "Type specification for function has wrong ariety.") + else + let context1 = List.fold_left2 (fun acc x t -> VariableMap.add x t acc) context xs tin in + match (evaluate_type fbody context1 = tout) with + (false) -> raise (WrongTypeSpecification "Function does not return specified type.") + | (true) -> typef + ) + | _ -> raise (WrongTypeSpecification "Specification of function is not a function type.") + ) + | Application (f, xs) -> ( + match evaluate_type f context with + FunctionType (tin, tout) -> ( + let rec helper params typeparams = + match (params, typeparams) with + ([], _) -> typeparams + | (_, []) -> raise (WrongAriety ("Function application has arity " ^ + (List.length tin |> string_of_int) ^ + ", but was applied to " ^ + (List.length xs |> string_of_int) ^ + " parameters")) + | (p::tlparams, v::tltypeparams) -> + if evaluate_type p context = v then + helper tlparams tltypeparams + else + raise (WrongType "Argument with wrong type.") + in + match helper xs tin with + [] -> tout + | t -> FunctionType (t, tout) + ) + | _ -> raise (WrongType "Applying to a non function type") + ) + | Plus (x, y) + | Minus (x, y) + | Times (x, y) + | Division (x, y) + | Modulo (x, y) + | Power (x, y) -> ( + match (evaluate_type x context, evaluate_type y context) with + | (IntegerType, IntegerType) -> IntegerType + | (IntegerType, _) -> raise (WrongType "Second term is not an integer.") + | (_, _) -> raise (WrongType "First term is not an integer.") + ) + | PowerMod (x, y, z) -> ( + match (evaluate_type x context, evaluate_type y context, evaluate_type z context) with + | (IntegerType, IntegerType, IntegerType) -> IntegerType + | (IntegerType, IntegerType, _) -> raise (WrongType "Third term is not an integer.") + | (IntegerType, _, _) -> raise (WrongType "Second term is not an integer.") + | (_, _, _) -> raise (WrongType "First term is not an integer.") + ) + | Rand (x) -> ( + match (evaluate_type x context) with + | (IntegerType) -> IntegerType + | (_) -> raise (WrongType "Term is not an integer.") + ) + | BAnd (x, y) + | BOr (x, y) -> ( + match (evaluate_type x context, evaluate_type y context) with + | (BooleanType, BooleanType) -> BooleanType + | (BooleanType, _) -> raise (WrongType "Second term is not a boolean.") + | (_, _) -> raise (WrongType "First term is not a boolean.") + ) + | BNot (x) -> ( + match (evaluate_type x context) with + | (BooleanType) -> BooleanType + | (_) -> raise (WrongType "Term is not a boolean.") + ) + | Cmp (x, y) + | CmpLess (x, y) + | CmpLessEq (x, y) + | CmpGreater (x, y) + | CmpGreaterEq (x, y) -> ( + match (evaluate_type x context, evaluate_type y context) with + | (IntegerType, IntegerType) -> BooleanType + | (IntegerType, _) -> raise (WrongType "Second term is not an integer.") + | (_, _) -> raise (WrongType "First term is not an integer.") + ) + | IfThenElse (guard, if_exp, else_exp) -> ( + match (evaluate_type guard context, evaluate_type if_exp context, evaluate_type else_exp context) with + (BooleanType, t1, t2) -> ( + if t1 = t2 then + t1 + else + raise (WrongType "If branches do not have the same type.") + ) + | (_, _, _) -> raise (WrongType "If guard is not a boolean.") + ) + | LetIn (x, xval, rest) -> + let typex = evaluate_type xval context in + evaluate_type rest (VariableMap.add x typex context) + | LetFun (f, xs, typef, fbody, rest) -> + match typef with + FunctionType (tin, tout) -> ( + if List.length xs != List.length tin then + raise (WrongAriety "Type specification for function has wrong ariety.") + else + let context1 = VariableMap.add f typef context in + let context2 = List.fold_left2 (fun acc x t -> VariableMap.add x t acc) context1 xs tin in + match (evaluate_type fbody context2 = tout, evaluate_type rest context1) with + (false, _) -> raise (WrongTypeSpecification "Function does not return specified type." + ) + | (true, t) -> t + ) + | _ -> raise (WrongTypeSpecification "Specification of function is not a function type.") + +let typecheck (program: t_exp) = + match evaluate_type program VariableMap.empty with + FunctionType ([IntegerType], IntegerType) -> true + | _ -> raise (WrongType "Program is not a function from int to int.") diff --git a/lib/miniFun.mli b/lib/miniFun.mli index 9960f52..eb0fbc5 100644 --- a/lib/miniFun.mli +++ b/lib/miniFun.mli @@ -1,12 +1,16 @@ type variable = string module VariableMap : Map.S with type key = variable +type ftype = + IntegerType + | BooleanType + | FunctionType of ftype list * ftype type t_exp = Integer of int | Boolean of bool | Variable of variable - | Function of variable list * t_exp + | Function of variable list * ftype * t_exp | Application of t_exp * t_exp list | Plus of t_exp * t_exp | Minus of t_exp * t_exp @@ -26,7 +30,7 @@ type t_exp = | CmpGreaterEq of t_exp * t_exp | IfThenElse of t_exp * t_exp * t_exp | LetIn of variable * t_exp * t_exp - | LetFun of variable * variable list * t_exp * t_exp + | LetFun of variable * variable list * ftype * t_exp * t_exp type permittedValues = IntegerPermitted of int @@ -47,5 +51,8 @@ exception AbsentAssignment of string exception WrongType of string exception DivisionByZero of string exception WrongAriety of string +exception WrongTypeSpecification of string val reduce : t_exp -> int -> int + +val typecheck : t_exp -> bool diff --git a/test/dune b/test/dune index 8d5c71b..6fa18f7 100644 --- a/test/dune +++ b/test/dune @@ -4,4 +4,8 @@ (test (name testingFun) + (libraries lang)) + +(test + (name testingTypeFun) (libraries lang)) \ No newline at end of file diff --git a/test/testingFun.ml b/test/testingFun.ml index 3de15e6..aba4820 100644 --- a/test/testingFun.ml +++ b/test/testingFun.ml @@ -5,6 +5,7 @@ open Lang.MiniFun let program = Function (["a"], + FunctionType ([IntegerType], IntegerType), (Variable "a") ) ;; @@ -16,6 +17,7 @@ Printf.printf "Identity program: %d\n" (reduce program 1) let program = Function (["a"], + FunctionType ([IntegerType], IntegerType), (Integer 1) ) ;; @@ -27,7 +29,9 @@ Printf.printf "Constant program: %d\n" (reduce program 10) let program = LetIn ("f", - (Function (["x"; "y"], Plus (Variable "x", Variable "y"))), + (Function (["x"; "y"], + FunctionType ([IntegerType; IntegerType], IntegerType), + Plus (Variable "x", Variable "y"))), (Application (Variable "f", [Integer 3])) ) ;; @@ -40,7 +44,10 @@ let program = LetFun ("f", ["x"], - (Function (["y"], Plus (Variable "x", Variable "y"))), + FunctionType ([IntegerType], IntegerType), + (Function (["y"], + FunctionType ([IntegerType], IntegerType), + Plus (Variable "x", Variable "y"))), (Application (Variable "f", [Integer 3])) ) ;; @@ -54,10 +61,13 @@ let program = ("f", (Function ( ["z"], + FunctionType ([FunctionType ([IntegerType], IntegerType)], IntegerType), (Function ( ["y"], + FunctionType ([FunctionType ([IntegerType], IntegerType)], IntegerType), Function ( ["x"], + FunctionType ([IntegerType], IntegerType), (IfThenElse ( CmpLess (Variable "x", Integer 0), (Application (Variable "y", [Variable "x"])), @@ -69,10 +79,10 @@ let program = ( (Application (Variable "f", - [Function (["x"], Plus (Variable "x", Integer 1))] + [Function (["x"], FunctionType ([IntegerType], IntegerType), Plus (Variable "x", Integer 1))] ) ), - [Function (["x"], Minus (Variable "x", Integer 1))] + [Function (["x"], FunctionType ([IntegerType], IntegerType), Minus (Variable "x", Integer 1))] ) ) ) @@ -87,6 +97,7 @@ let program = LetFun ("f", ["x"], + FunctionType ([IntegerType], IntegerType), (IfThenElse (CmpLess (Variable "x", Integer 2),Integer 1, Plus (Variable "x", Application (Variable "f", [Minus (Variable "x", Integer 1)])))), (Variable "f") ) @@ -99,7 +110,7 @@ Printf.printf "Recursive function program: %d\n" (reduce program 10) let program = LetIn ("f", - (LetIn ("a", Integer 1, (Function (["y"], Plus (Variable "y", Variable "a"))))), + (LetIn ("a", Integer 1, (Function (["y"], FunctionType ([IntegerType], IntegerType), Plus (Variable "y", Variable "a"))))), (LetIn ("a", Integer 2, Variable "f")) ) ;; @@ -112,6 +123,7 @@ let program = LetFun ( "f", ["x"], + FunctionType ([IntegerType], IntegerType), (IfThenElse (CmpLessEq (Variable "x", Integer 0), Integer 1, Times (Variable "x", Application (Variable "f", [Minus (Variable "x", Integer 1)])))), (Variable "f") ) @@ -127,6 +139,7 @@ let program = LetFun ( "collatz", ["n"; "count"], + FunctionType ([IntegerType; IntegerType], IntegerType), ( IfThenElse (BNot (Cmp (Variable "n", Integer 1)), (IfThenElse (Cmp (Modulo (Variable "n", Integer 2), Integer 0), @@ -134,7 +147,9 @@ let program = Application (Variable "collatz", [(Plus (Integer 1, Times (Integer 3, Variable "n"))); Plus (Integer 1, Variable "count")]))), (Variable "count")) ), - (Function (["x"], Application (Variable "collatz", [Variable "x"; Integer 1]))) + (Function (["x"], + FunctionType ([IntegerType], IntegerType), + Application (Variable "collatz", [Variable "x"; Integer 1]))) ) ;; @@ -148,6 +163,7 @@ let program = LetFun ( "sum", ["n"], + FunctionType ([IntegerType], IntegerType), (IfThenElse ((BOr (Cmp (Modulo (Variable "n", Integer 3), Integer 0), Cmp (Modulo (Variable "n", Integer 5), Integer 0))), Plus (Variable "n", Application (Variable "sum", [Minus (Variable "n", Integer 1)])), (IfThenElse ((CmpLessEq (Variable "n", Integer 1)), @@ -167,6 +183,7 @@ Printf.printf "Sum multiples of 3 and 5 program: %d\n" (reduce program 12345) let program = Function ( ["x"], + FunctionType ([IntegerType], IntegerType), Rand (Variable "x") ) @@ -181,13 +198,16 @@ let program = LetFun ( "fib", ["i"; "a"; "b"], + FunctionType ([IntegerType; IntegerType; IntegerType], IntegerType), (IfThenElse (Cmp (Variable "i", Integer 0), Variable "a", Application (Variable "fib", [Minus (Variable "i", Integer 1); Variable "b"; Plus (Variable "a", Variable "b")]) )), - Function (["x"], (Application (Variable "fib", [Variable "x"; Integer 0; Integer 1]))) + Function (["x"], + FunctionType ([IntegerType], IntegerType), + (Application (Variable "fib", [Variable "x"; Integer 0; Integer 1]))) ) ;; diff --git a/test/testingTypeFun.expected b/test/testingTypeFun.expected new file mode 100644 index 0000000..4dcb90d --- /dev/null +++ b/test/testingTypeFun.expected @@ -0,0 +1,12 @@ +Identity program: true +Constant program: true +Partial application of function program: true +Partial application of function program: true +Passing functions to functions program: true +Recursive function program: true +Scope program: true +Factorial program: true +Hailstone sequence's lenght program: true +Sum multiples of 3 and 5 program: true +Rand program: true +Fibonacci program: true diff --git a/test/testingTypeFun.ml b/test/testingTypeFun.ml new file mode 100644 index 0000000..c15c426 --- /dev/null +++ b/test/testingTypeFun.ml @@ -0,0 +1,215 @@ +open Lang.MiniFun + +(* -------------------------------------------------------------------------- *) +(* Identity program *) +let program = + Function + (["a"], + FunctionType ([IntegerType], IntegerType), + (Variable "a") + ) +;; + +Printf.printf "Identity program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Constant program *) +let program = + Function + (["a"], + FunctionType ([IntegerType], IntegerType), + (Integer 1) + ) +;; + +Printf.printf "Constant program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Partial application of function program *) +let program = + LetIn + ("f", + (Function (["x"; "y"], + FunctionType ([IntegerType; IntegerType], IntegerType), + Plus (Variable "x", Variable "y"))), + (Application (Variable "f", [Integer 3])) + ) +;; + +Printf.printf "Partial application of function program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Partial application of function program *) +let program = + LetFun + ("f", + ["x"], + FunctionType ([IntegerType], FunctionType ([IntegerType], IntegerType)), + (Function (["y"], + FunctionType ([IntegerType], IntegerType), + Plus (Variable "x", Variable "y"))), + (Application (Variable "f", [Integer 3])) + ) +;; + +Printf.printf "Partial application of function program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Passing functions to functions program *) +let program = + LetIn + ("f", + (Function ( + ["z"], + FunctionType ([FunctionType ([IntegerType], IntegerType)], FunctionType ([FunctionType ([IntegerType], IntegerType)], FunctionType ([IntegerType], IntegerType))), + (Function ( + ["y"], + FunctionType ([FunctionType ([IntegerType], IntegerType)], FunctionType ([IntegerType], IntegerType)), + Function ( + ["x"], + FunctionType ([IntegerType], IntegerType), + (IfThenElse ( + CmpLess (Variable "x", Integer 0), + (Application (Variable "y", [Variable "x"])), + (Application (Variable "z", [Variable "x"])) + ))) + )) + )), + (Application + ( + (Application + (Variable "f", + [Function (["x"], FunctionType ([IntegerType], IntegerType), Plus (Variable "x", Integer 1))] + ) + ), + [Function (["x"], FunctionType ([IntegerType], IntegerType), Minus (Variable "x", Integer 1))] + ) + ) + ) +;; + +Printf.printf "Passing functions to functions program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Recursive function program *) +let program = + LetFun + ("f", + ["x"], + FunctionType ([IntegerType], IntegerType), + (IfThenElse (CmpLess (Variable "x", Integer 2),Integer 1, Plus (Variable "x", Application (Variable "f", [Minus (Variable "x", Integer 1)])))), + (Variable "f") + ) +;; + +Printf.printf "Recursive function program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Scope program *) +let program = + LetIn + ("f", + (LetIn ("a", Integer 1, (Function (["y"], FunctionType ([IntegerType], IntegerType), Plus (Variable "y", Variable "a"))))), + (LetIn ("a", Integer 2, Variable "f")) + ) +;; + +Printf.printf "Scope program: %b\n" (typecheck program) + +(* -------------------------------------------------------------------------- *) +(* Factorial program *) +let program = + LetFun ( + "f", + ["x"], + FunctionType ([IntegerType], IntegerType), + (IfThenElse (CmpLessEq (Variable "x", Integer 0), Integer 1, Times (Variable "x", Application (Variable "f", [Minus (Variable "x", Integer 1)])))), + (Variable "f") + ) +;; + +Printf.printf "Factorial program: %b\n" (typecheck program) +;; + +(* -------------------------------------------------------------------------- *) +(* Hailstone sequence's lenght program *) + +let program = + LetFun ( + "collatz", + ["n"; "count"], + FunctionType ([IntegerType; IntegerType], IntegerType), + ( + IfThenElse (BNot (Cmp (Variable "n", Integer 1)), + (IfThenElse (Cmp (Modulo (Variable "n", Integer 2), Integer 0), + Application (Variable "collatz", [Division (Variable "n", Integer 2); Plus (Integer 1, Variable "count")]), + Application (Variable "collatz", [(Plus (Integer 1, Times (Integer 3, Variable "n"))); Plus (Integer 1, Variable "count")]))), + (Variable "count")) + ), + (Function (["x"], + FunctionType ([IntegerType], IntegerType), + Application (Variable "collatz", [Variable "x"; Integer 1]))) + ) +;; + +Printf.printf "Hailstone sequence's lenght program: %b\n" (typecheck program) +;; + +(* -------------------------------------------------------------------------- *) +(* Sum multiples of 3 and 5 program *) + +let program = + LetFun ( + "sum", + ["n"], + FunctionType ([IntegerType], IntegerType), + (IfThenElse ((BOr (Cmp (Modulo (Variable "n", Integer 3), Integer 0), Cmp (Modulo (Variable "n", Integer 5), Integer 0))), + Plus (Variable "n", Application (Variable "sum", [Minus (Variable "n", Integer 1)])), + (IfThenElse ((CmpLessEq (Variable "n", Integer 1)), + (Integer 0), + (Application (Variable "sum", [Minus (Variable "n", Integer 1)]))) + )) + ), + (Variable "sum") + ) +;; + +Printf.printf "Sum multiples of 3 and 5 program: %b\n" (typecheck program) +;; + +(* -------------------------------------------------------------------------- *) +(* Rand program *) +let program = + Function ( + ["x"], + FunctionType ([IntegerType], IntegerType), + Rand (Variable "x") + ) + +;; + +Printf.printf "Rand program: %b\n" (typecheck program) +;; + +(* -------------------------------------------------------------------------- *) +(* Fibonacci program *) +let program = + LetFun ( + "fib", + ["i"; "a"; "b"], + FunctionType ([IntegerType; IntegerType; IntegerType], IntegerType), + (IfThenElse (Cmp (Variable "i", Integer 0), + Variable "a", + Application (Variable "fib", [Minus (Variable "i", Integer 1); + Variable "b"; + Plus (Variable "a", Variable "b")]) + )), + Function (["x"], + FunctionType ([IntegerType], IntegerType), + (Application (Variable "fib", [Variable "x"; Integer 0; Integer 1]))) + ) + +;; + +Printf.printf "Fibonacci program: %b\n" (typecheck program) +;;