From ccbba90ead3628111a9df0719eb75cf12f4cbe3e Mon Sep 17 00:00:00 2001 From: elvis Date: Fri, 25 Oct 2024 21:29:49 +0200 Subject: [PATCH] Refactor --- lib/lang.ml | 12 +- lib/{miniFun.ml => miniFun/Semantics.ml} | 189 +---------------------- lib/miniFun/Semantics.mli | 1 + lib/miniFun/TypeChecker.ml | 125 +++++++++++++++ lib/miniFun/TypeChecker.mli | 1 + lib/miniFun/Types.ml | 55 +++++++ lib/{miniFun.mli => miniFun/Types.mli} | 5 +- lib/{miniImp.ml => miniImp/Semantics.ml} | 45 +----- lib/miniImp/Semantics.mli | 3 + lib/miniImp/Types.ml | 43 ++++++ lib/{miniImp.mli => miniImp/Types.mli} | 3 +- test/testingFun.ml | 1 + test/testingImp.ml | 1 + test/testingTypeFun.ml | 3 +- 14 files changed, 251 insertions(+), 236 deletions(-) rename lib/{miniFun.ml => miniFun/Semantics.ml} (58%) create mode 100644 lib/miniFun/Semantics.mli create mode 100644 lib/miniFun/TypeChecker.ml create mode 100644 lib/miniFun/TypeChecker.mli create mode 100644 lib/miniFun/Types.ml rename lib/{miniFun.mli => miniFun/Types.mli} (95%) rename lib/{miniImp.ml => miniImp/Semantics.ml} (72%) create mode 100644 lib/miniImp/Semantics.mli create mode 100644 lib/miniImp/Types.ml rename lib/{miniImp.mli => miniImp/Types.mli} (97%) diff --git a/lib/lang.ml b/lib/lang.ml index 9cb35a7..3ddfe33 100644 --- a/lib/lang.ml +++ b/lib/lang.ml @@ -1,5 +1,13 @@ module Exercises = Exercises -module MiniImp = MiniImp +(* -------------------------------- MINI IMP -------------------------------- *) +module MiniImpTypes = MiniImp.Types -module MiniFun = MiniFun +module MiniImp = MiniImp.Semantics + +(* -------------------------------- MINI FUN -------------------------------- *) +module MiniFunTypes = MiniFun.Types + +module MiniTyFun = MiniFun.TypeChecker + +module MiniFun = MiniFun.Semantics diff --git a/lib/miniFun.ml b/lib/miniFun/Semantics.ml similarity index 58% rename from lib/miniFun.ml rename to lib/miniFun/Semantics.ml index fbdc1f5..7451ed3 100644 --- a/lib/miniFun.ml +++ b/lib/miniFun/Semantics.ml @@ -1,60 +1,5 @@ -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 * ftype * t_exp - | Application of t_exp * t_exp list - | Plus of t_exp * t_exp - | Minus of t_exp * t_exp - | Times of t_exp * t_exp - | Division of t_exp * t_exp - | Modulo of t_exp * t_exp - | Power of t_exp * t_exp - | PowerMod of t_exp * t_exp * t_exp - | Rand of t_exp - | BAnd of t_exp * t_exp - | BOr of t_exp * t_exp - | BNot of t_exp - | Cmp of t_exp * t_exp - | CmpLess of t_exp * t_exp - | CmpLessEq of t_exp * t_exp - | CmpGreater of t_exp * 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 * ftype * t_exp * t_exp - -type permittedValues = - IntegerPermitted of int - | BooleanPermitted of bool - | FunctionPermitted of closure -and closure = { - inputList: variable list; - body: t_exp; - assignments: permittedValues VariableMap.t; - recursiveness: variable option -} - -type memory = { - assignments: permittedValues VariableMap.t -} - -exception AbsentAssignment of string -exception WrongType of string -exception DivisionByZero of string -exception WrongArity of string -exception WrongTypeSpecification of string - -module Utility = Utility;; +module Utility = Utility +open Types;; Random.self_init () @@ -80,8 +25,10 @@ let rec evaluate (mem: memory) (command: t_exp) = let funcClosure = ( match (evaluate mem f) with FunctionPermitted ff -> ff - | IntegerPermitted _ -> raise (WrongType ("Function is not a function, it's an integer")) - | BooleanPermitted _ -> raise (WrongType ("Function is not a function, it's a boolean")) + | IntegerPermitted _ -> raise (WrongType ("Function is not a function, " + ^ "it's an integer")) + | BooleanPermitted _ -> raise (WrongType ("Function is not a function, " + ^ "it's a boolean")) ) in let parmList = List.map (fun k -> evaluate mem k) xs in let rec helper m params values = @@ -362,127 +309,3 @@ 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 arity.") - 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 (WrongArity ("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 (WrongArity "Type specification for function has wrong arity.") - 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/Semantics.mli b/lib/miniFun/Semantics.mli new file mode 100644 index 0000000..0ad9651 --- /dev/null +++ b/lib/miniFun/Semantics.mli @@ -0,0 +1 @@ +val reduce : Types.t_exp -> int -> int diff --git a/lib/miniFun/TypeChecker.ml b/lib/miniFun/TypeChecker.ml new file mode 100644 index 0000000..7befe0f --- /dev/null +++ b/lib/miniFun/TypeChecker.ml @@ -0,0 +1,125 @@ +module Utility = Utility +open Types;; + +Random.self_init () + +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 arity.") + 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 (WrongArity ("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 (WrongArity "Type specification for function has wrong arity.") + 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/TypeChecker.mli b/lib/miniFun/TypeChecker.mli new file mode 100644 index 0000000..c0440e6 --- /dev/null +++ b/lib/miniFun/TypeChecker.mli @@ -0,0 +1 @@ +val typecheck : Types.t_exp -> bool diff --git a/lib/miniFun/Types.ml b/lib/miniFun/Types.ml new file mode 100644 index 0000000..87887bd --- /dev/null +++ b/lib/miniFun/Types.ml @@ -0,0 +1,55 @@ +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 * ftype * t_exp + | Application of t_exp * t_exp list + | Plus of t_exp * t_exp + | Minus of t_exp * t_exp + | Times of t_exp * t_exp + | Division of t_exp * t_exp + | Modulo of t_exp * t_exp + | Power of t_exp * t_exp + | PowerMod of t_exp * t_exp * t_exp + | Rand of t_exp + | BAnd of t_exp * t_exp + | BOr of t_exp * t_exp + | BNot of t_exp + | Cmp of t_exp * t_exp + | CmpLess of t_exp * t_exp + | CmpLessEq of t_exp * t_exp + | CmpGreater of t_exp * 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 * ftype * t_exp * t_exp + +type permittedValues = + IntegerPermitted of int + | BooleanPermitted of bool + | FunctionPermitted of closure +and closure = { + inputList: variable list; + body: t_exp; + assignments: permittedValues VariableMap.t; + recursiveness: variable option +} + +type memory = { + assignments: permittedValues VariableMap.t +} + +exception AbsentAssignment of string +exception WrongType of string +exception DivisionByZero of string +exception WrongArity of string +exception WrongTypeSpecification of string diff --git a/lib/miniFun.mli b/lib/miniFun/Types.mli similarity index 95% rename from lib/miniFun.mli rename to lib/miniFun/Types.mli index 3ffc761..1c256ec 100644 --- a/lib/miniFun.mli +++ b/lib/miniFun/Types.mli @@ -1,6 +1,7 @@ type variable = string module VariableMap : Map.S with type key = variable + type ftype = IntegerType | BooleanType @@ -52,7 +53,3 @@ exception WrongType of string exception DivisionByZero of string exception WrongArity of string exception WrongTypeSpecification of string - -val reduce : t_exp -> int -> int - -val typecheck : t_exp -> bool diff --git a/lib/miniImp.ml b/lib/miniImp/Semantics.ml similarity index 72% rename from lib/miniImp.ml rename to lib/miniImp/Semantics.ml index 961c1ae..1505899 100644 --- a/lib/miniImp.ml +++ b/lib/miniImp/Semantics.ml @@ -1,47 +1,4 @@ -type variable = string - -type p_exp = - Main of variable * variable * c_exp (* def main with input x output y as c *) -and c_exp = - Skip - | Assignment of variable * a_exp (* x := a *) - | Sequence of c_exp * c_exp (* c; c *) - | If of b_exp * c_exp * c_exp (* if b then c else c *) - | While of b_exp * c_exp (* while b do c *) - | For of c_exp * b_exp * c_exp * c_exp (* for c; b; c do c *) -and b_exp = - Boolean of bool (* v *) - | BAnd of b_exp * b_exp (* b and b *) - | BOr of b_exp * b_exp (* b or b *) - | BNot of b_exp (* not b *) - | BCmp of a_exp * a_exp (* a = a *) - | BCmpLess of a_exp * a_exp (* a < a *) - | BCmpLessEq of a_exp * a_exp (* a <= a *) - | BCmpGreater of a_exp * a_exp (* a > a *) - | BCmpGreaterEq of a_exp * a_exp (* a >= a *) -and a_exp = - Variable of variable (* x *) - | Integer of int (* n *) - | Plus of a_exp * a_exp (* a + a *) - | Minus of a_exp * a_exp (* a - a *) - | Times of a_exp * a_exp (* a * a *) - | Division of a_exp * a_exp (* a / a *) - | Modulo of a_exp * a_exp (* a % a *) - | Power of a_exp * a_exp (* a ^ a *) - | PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *) - | Rand of a_exp (* rand(0, a) *) - - - -module VariableMap = Map.Make(String) - -type memory = { - assignments: int VariableMap.t -} - - -exception AbsentAssignment of string -exception DivisionByZero of string +open Types module Utility = Utility;; diff --git a/lib/miniImp/Semantics.mli b/lib/miniImp/Semantics.mli new file mode 100644 index 0000000..ac04fd0 --- /dev/null +++ b/lib/miniImp/Semantics.mli @@ -0,0 +1,3 @@ +open Types + +val reduce : p_exp -> int -> int diff --git a/lib/miniImp/Types.ml b/lib/miniImp/Types.ml new file mode 100644 index 0000000..d39143d --- /dev/null +++ b/lib/miniImp/Types.ml @@ -0,0 +1,43 @@ +type variable = string + +type p_exp = + Main of variable * variable * c_exp (* def main with input x output y as c *) +and c_exp = + Skip + | Assignment of variable * a_exp (* x := a *) + | Sequence of c_exp * c_exp (* c; c *) + | If of b_exp * c_exp * c_exp (* if b then c else c *) + | While of b_exp * c_exp (* while b do c *) + | For of c_exp * b_exp * c_exp * c_exp (* for c; b; c do c *) +and b_exp = + Boolean of bool (* v *) + | BAnd of b_exp * b_exp (* b and b *) + | BOr of b_exp * b_exp (* b or b *) + | BNot of b_exp (* not b *) + | BCmp of a_exp * a_exp (* a = a *) + | BCmpLess of a_exp * a_exp (* a < a *) + | BCmpLessEq of a_exp * a_exp (* a <= a *) + | BCmpGreater of a_exp * a_exp (* a > a *) + | BCmpGreaterEq of a_exp * a_exp (* a >= a *) +and a_exp = + Variable of variable (* x *) + | Integer of int (* n *) + | Plus of a_exp * a_exp (* a + a *) + | Minus of a_exp * a_exp (* a - a *) + | Times of a_exp * a_exp (* a * a *) + | Division of a_exp * a_exp (* a / a *) + | Modulo of a_exp * a_exp (* a % a *) + | Power of a_exp * a_exp (* a ^ a *) + | PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *) + | Rand of a_exp (* rand(0, a) *) + + + +module VariableMap = Map.Make(String) + +type memory = { + assignments: int VariableMap.t +} + +exception AbsentAssignment of string +exception DivisionByZero of string diff --git a/lib/miniImp.mli b/lib/miniImp/Types.mli similarity index 97% rename from lib/miniImp.mli rename to lib/miniImp/Types.mli index cf1e73a..acb906f 100644 --- a/lib/miniImp.mli +++ b/lib/miniImp/Types.mli @@ -40,5 +40,4 @@ type memory = { } exception AbsentAssignment of string - -val reduce : p_exp -> int -> int +exception DivisionByZero of string diff --git a/test/testingFun.ml b/test/testingFun.ml index aba4820..daa7cc8 100644 --- a/test/testingFun.ml +++ b/test/testingFun.ml @@ -1,4 +1,5 @@ open Lang.MiniFun +open Lang.MiniFunTypes (* -------------------------------------------------------------------------- *) (* Identity program *) diff --git a/test/testingImp.ml b/test/testingImp.ml index b2d0d84..9bfa08b 100644 --- a/test/testingImp.ml +++ b/test/testingImp.ml @@ -1,4 +1,5 @@ open Lang.MiniImp +open Lang.MiniImpTypes (* -------------------------------------------------------------------------- *) (* Identity program *) diff --git a/test/testingTypeFun.ml b/test/testingTypeFun.ml index f7da472..103a723 100644 --- a/test/testingTypeFun.ml +++ b/test/testingTypeFun.ml @@ -1,4 +1,5 @@ -open Lang.MiniFun +open Lang.MiniTyFun +open Lang.MiniFunTypes (* -------------------------------------------------------------------------- *) (* Error absent assignment program *)