Type checking for miniFun, adding some tests

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.")

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

test/dune

@@ -5,3 +5,7 @@
 (test
  (name testingFun)
  (libraries lang))
+
+(test
+ (name testingTypeFun)
+ (libraries lang))

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])))
   )
 
 ;;

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

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)
+;;