This commit is contained in:
elvis
2024-10-25 21:29:49 +02:00
parent ec966ba67f
commit ccbba90ead
14 changed files with 251 additions and 236 deletions

View File

@ -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

View File

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

View File

@ -0,0 +1 @@
val reduce : Types.t_exp -> int -> int

125
lib/miniFun/TypeChecker.ml Normal file
View File

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

View File

@ -0,0 +1 @@
val typecheck : Types.t_exp -> bool

55
lib/miniFun/Types.ml Normal file
View File

@ -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

View File

@ -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

View File

@ -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;;

View File

@ -0,0 +1,3 @@
open Types
val reduce : p_exp -> int -> int

43
lib/miniImp/Types.ml Normal file
View File

@ -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

View File

@ -40,5 +40,4 @@ type memory = {
}
exception AbsentAssignment of string
val reduce : p_exp -> int -> int
exception DivisionByZero of string