elvis/lci
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Refactoring, errors are not thrown anymore

Browse Source
This commit is contained in:
elvis
2024-10-26 01:47:30 +02:00
parent 8427133fd7
commit 3e4e1615d2
11 changed files with 413 additions and 339 deletions
Download Patch File Download Diff File Expand all files Collapse all files

317
lib/miniFun/Semantics.ml
View File

@ -3,50 +3,52 @@ open Types;;
Random.self_init ()
let rec evaluate (mem: memory) (command: t_exp) =
let (let*) = Result.bind
let rec evaluate (mem: memory) (command: t_exp) : (permittedValues, error) result =
match command with
Integer n -> (IntegerPermitted n)
| Boolean b -> (BooleanPermitted b)
Integer n -> Ok (IntegerPermitted n)
| Boolean b -> Ok (BooleanPermitted b)
| Variable v -> (
match VariableMap.find_opt v mem.assignments with
None -> raise (AbsentAssignment ("The variable " ^
v ^
" is not defined."))
| Some a -> a
None -> Error (`AbsentAssignment ("The variable " ^ v ^ " is not defined."))
| Some a -> Ok a
)
| Function (xs, _, f) ->
(FunctionPermitted
Ok (FunctionPermitted
{inputList = xs;
body = f;
assignments = mem.assignments;
recursiveness = None}
)
| Application (f, xs) -> (
let funcClosure = (
match (evaluate mem f) with
FunctionPermitted ff -> ff
| IntegerPermitted _ -> raise (WrongType ("Function is not a function, "
let* evalf = evaluate mem f in
let* funcClosure = (
match evalf with
FunctionPermitted ff -> Ok ff
| IntegerPermitted _ -> Error (`WrongType ("Function is not a function,"
^ " it's an integer"))
| BooleanPermitted _ -> raise (WrongType ("Function is not a function, "
| BooleanPermitted _ -> Error (`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 =
match (params, values) with
(_, []) -> (m, params)
(_, []) -> Ok (m, params)
| ([], _) ->
raise (WrongArity ("Function application has arity " ^
Error (`WrongArity ("Function application has arity " ^
(List.length funcClosure.inputList
|> string_of_int) ^
", but was applied to " ^
(List.length xs |> string_of_int) ^
" parameters"))
| (p::tlparams, v::tlvalues) -> helper
| (p::tlparams, (Ok v)::tlvalues) -> helper
(VariableMap.add p v m)
tlparams
tlvalues
| (_, (Error e)::_) -> Error e
in
let (mem2assignments, params) = helper
let* (mem2assignments, params) = helper
funcClosure.assignments
funcClosure.inputList
parmList
@ -65,227 +67,266 @@ let rec evaluate (mem: memory) (command: t_exp) =
match params with
[] -> evaluate mem2 funcClosure.body
| _ -> (
FunctionPermitted {funcClosure with inputList = params;
assignments = mem2assignments})
Ok (FunctionPermitted {funcClosure with inputList = params;
assignments = mem2assignments}))
)
| Plus (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (aval + bval))
Ok (IntegerPermitted (aval + bval))
| Minus (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (aval - bval))
Ok (IntegerPermitted (aval - bval))
| Times (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (aval * bval))
Ok (IntegerPermitted (aval * bval))
| Division (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in (
try
(IntegerPermitted (aval / bval))
with Division_by_zero -> raise (DivisionByZero "Dividing by zero")
Ok (IntegerPermitted (aval / bval))
with Division_by_zero -> Error (`DivisionByZero "Dividing by zero")
)
| Modulo (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (aval mod bval))
Ok (IntegerPermitted (aval mod bval))
| Power (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (Utility.pow aval bval))
Ok (IntegerPermitted (Utility.pow aval bval))
| PowerMod (a, b, c) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
let cval = (
let* cval = (
match evaluate mem c with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
(IntegerPermitted (Utility.powmod aval bval cval))
Ok (IntegerPermitted (Utility.powmod aval bval cval))
| Rand (a) ->
let aval = (
let* aval = (
match evaluate mem a with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
)
in
IntegerPermitted (Random.int aval)
Ok (IntegerPermitted (Random.int aval))
| BAnd (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
BooleanPermitted x -> x
| _ -> raise (WrongType ("Value is not an boolean"))
Ok BooleanPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an boolean"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
BooleanPermitted x -> x
| _ -> raise (WrongType ("Value is not an boolean"))
Ok BooleanPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an boolean"))
)
in
(BooleanPermitted (aval && bval))
Ok (BooleanPermitted (aval && bval))
| BOr (a, b) ->
let aval = (
let* aval = (
match evaluate mem a with
BooleanPermitted x -> x
| _ -> raise (WrongType ("Value is not an boolean"))
Ok BooleanPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an boolean"))
)
in
let bval = (
let* bval = (
match evaluate mem b with
BooleanPermitted x -> x
| _ -> raise (WrongType ("Value is not an boolean"))
Ok BooleanPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an boolean"))
)
in
(BooleanPermitted (aval || bval))
Ok (BooleanPermitted (aval || bval))
| BNot a ->
let aval = (
let* aval = (
match evaluate mem a with
BooleanPermitted x -> x
| _ -> raise (WrongType ("Value is not an boolean"))
Ok BooleanPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an boolean"))
)
in
(BooleanPermitted (not aval))
| Cmp (exp_1, exp_2) -> (
let exp_1val = match evaluate mem exp_1 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
Ok (BooleanPermitted (not aval))
| Cmp (exp_1, exp_2) ->
let* exp_1val = match evaluate mem exp_1 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
let exp_2val = match evaluate mem exp_2 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_2val = match evaluate mem exp_2 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
BooleanPermitted (exp_1val = exp_2val)
)
Ok (BooleanPermitted (exp_1val = exp_2val))
| CmpLess (exp_1, exp_2) -> (
let exp_1val = match evaluate mem exp_1 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_1val = match evaluate mem exp_1 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
let exp_2val = match evaluate mem exp_2 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_2val = match evaluate mem exp_2 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
BooleanPermitted (exp_1val < exp_2val)
Ok (BooleanPermitted (exp_1val < exp_2val))
)
| CmpLessEq (exp_1, exp_2) -> (
let exp_1val = match evaluate mem exp_1 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_1val = match evaluate mem exp_1 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
let exp_2val = match evaluate mem exp_2 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_2val = match evaluate mem exp_2 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
BooleanPermitted (exp_1val <= exp_2val)
Ok (BooleanPermitted (exp_1val <= exp_2val))
)
| CmpGreater (exp_1, exp_2) -> (
let exp_1val = match evaluate mem exp_1 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_1val = match evaluate mem exp_1 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
let exp_2val = match evaluate mem exp_2 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_2val = match evaluate mem exp_2 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
BooleanPermitted (exp_1val > exp_2val)
Ok (BooleanPermitted (exp_1val > exp_2val))
)
| CmpGreaterEq (exp_1, exp_2) -> (
let exp_1val = match evaluate mem exp_1 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_1val = match evaluate mem exp_1 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
let exp_2val = match evaluate mem exp_2 with
IntegerPermitted x -> x
| _ -> raise (WrongType ("Value is not an integer"))
let* exp_2val = match evaluate mem exp_2 with
Ok IntegerPermitted x -> Ok x
| Error e -> Error e
| _ -> Error (`WrongType ("Value is not an integer"))
in
BooleanPermitted (exp_1val >= exp_2val)
Ok (BooleanPermitted (exp_1val >= exp_2val))
)
| IfThenElse (guard, if_exp, else_exp) ->
let bguard = (
let* bguard = (
match evaluate mem guard with
BooleanPermitted b -> b
| _ -> raise (WrongType ("Value in if guard is not a boolean"))
Ok BooleanPermitted b -> Ok b
| Error e -> Error e
| _ -> Error (`WrongType ("Value in if guard is not a boolean"))
) in
if bguard then
evaluate mem if_exp
else
evaluate mem else_exp
| LetIn (x, xval, rest) ->
let evalxval = evaluate mem xval in
let* evalxval = evaluate mem xval in
let mem2 = {assignments = VariableMap.add x evalxval mem.assignments} in
evaluate mem2 rest
| LetFun (f, xs, _, fbody, rest) ->
@ -303,9 +344,9 @@ let rec evaluate (mem: memory) (command: t_exp) =
evaluate mem2 rest
let reduce (program: t_exp) (iin : int) =
let reduce (program: t_exp) (iin : int) : (int, error) result =
let program' = (Application (program, [(Integer iin)])) in
let mem : memory = {assignments = VariableMap.empty} in
match (evaluate mem program') with
IntegerPermitted a -> a
| _ -> raise (WrongType ("Main function doesn't return an integer"))
Ok IntegerPermitted a -> Ok a
| _ -> Error (`WrongType ("Main function doesn't return an integer"))

2
lib/miniFun/Semantics.mli
View File

@ -1 +1 @@
val reduce : Types.t_exp -> int -> int
val reduce : Types.t_exp -> int -> (int, Types.error) result

143
lib/miniFun/TypeChecker.ml
View File

@ -3,48 +3,55 @@ open Types;;
Random.self_init ()
let rec evaluate_type (program: t_exp) context =
let (let*) = Result.bind
let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, error) result =
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)
Integer _ -> Ok IntegerType
| Boolean _ -> Ok BooleanType
| Variable x -> (
match VariableMap.find_opt x context with
None -> Error (`AbsentAssignment ("The variable " ^ x ^ " is not defined."))
| Some t -> Ok 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.")
if List.length xs <> List.length tin then
Error (`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
let* typefbody = evaluate_type fbody context1 in
match (typefbody = tout) with
(false) -> Error (`WrongTypeSpecification "Function does not return specified type.")
| (true) -> Ok typef
)
| _ -> raise (WrongTypeSpecification "Specification of function is not a function type.")
| _ -> Error (`WrongTypeSpecification "Specification of function is not a function type.")
)
| Application (f, xs) -> (
match evaluate_type f context with
let* evalf = evaluate_type f context in
match evalf with
FunctionType (tin, tout) -> (
let rec helper params typeparams =
match (params, typeparams) with
([], _) -> typeparams
| (_, []) -> raise (WrongArity ("Function application has arity " ^
([], _) -> Ok typeparams
| (_, []) -> Error (`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
if evaluate_type p context = Ok v then
helper tlparams tltypeparams
else
raise (WrongType "Argument with wrong type.")
Error (`WrongType "Argument with wrong type.")
in
match helper xs tin with
[] -> tout
| t -> FunctionType (t, tout)
let* typesremaining = helper xs tin in
match typesremaining with
[] -> Ok tout
| t -> Ok (FunctionType (t, tout))
)
| _ -> raise (WrongType "Applying to a non function type")
| _ -> Error (`WrongType "Applying to a non function type")
)
| Plus (x, y)
| Minus (x, y)
@ -52,74 +59,90 @@ let rec evaluate_type (program: t_exp) context =
| 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.")
let* typex = evaluate_type x context in
let* typey = evaluate_type y context in
match typex, typey with
| (IntegerType, IntegerType) -> Ok IntegerType
| (IntegerType, _) -> Error (`WrongType "Second term is not an integer.")
| (_, _) -> Error (`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.")
let* typex = evaluate_type x context in
let* typey = evaluate_type y context in
let* typez = evaluate_type z context in
match typex, typey, typez with
| (IntegerType, IntegerType, IntegerType) -> Ok IntegerType
| (IntegerType, IntegerType, _) -> Error (`WrongType "Third term is not an integer.")
| (IntegerType, _, _) -> Error (`WrongType "Second term is not an integer.")
| (_, _, _) -> Error (`WrongType "First term is not an integer.")
)
| Rand (x) -> (
match (evaluate_type x context) with
| (IntegerType) -> IntegerType
| (_) -> raise (WrongType "Term is not an integer.")
let* typex = evaluate_type x context in
match typex with
| (IntegerType) -> Ok IntegerType
| (_) -> Error (`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.")
let* typex = evaluate_type x context in
let* typey = evaluate_type y context in
match typex, typey with
| (BooleanType, BooleanType) -> Ok BooleanType
| (BooleanType, _) -> Error (`WrongType "Second term is not a boolean.")
| (_, _) -> Error (`WrongType "First term is not a boolean.")
)
| BNot (x) -> (
match (evaluate_type x context) with
| (BooleanType) -> BooleanType
| (_) -> raise (WrongType "Term is not a boolean.")
let* typex = evaluate_type x context in
match typex with
| (BooleanType) -> Ok BooleanType
| (_) -> Error (`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.")
let* typex = evaluate_type x context in
let* typey = evaluate_type y context in
match typex, typey with
| (IntegerType, IntegerType) -> Ok BooleanType
| (IntegerType, _) -> Error (`WrongType "Second term is not an integer.")
| (_, _) -> Error (`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
let* typeguard = evaluate_type guard context in
let* typeif_exp = evaluate_type if_exp context in
let* typeelse_exp = evaluate_type else_exp context in
match typeguard, typeif_exp, typeelse_exp with
(BooleanType, t1, t2) -> (
if t1 = t2 then
t1
Ok t1
else
raise (WrongType "If branches do not have the same type.")
Error (`WrongType "If branches do not have the same type.")
)
| (_, _, _) -> raise (WrongType "If guard is not a boolean.")
| (_, _, _) -> Error (`WrongType "If guard is not a boolean.")
)
| LetIn (x, xval, rest) ->
let typex = evaluate_type xval context in
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.")
if List.length xs <> List.length tin then
Error (`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."
let* typefbody = evaluate_type fbody context2 in
let* typerest = evaluate_type rest context1 in
match (typefbody = tout, typerest) with
(false, _) -> Error (`WrongTypeSpecification "Function does not return specified type.")
| (true, t) -> Ok t
)
| (true, t) -> t
)
| _ -> raise (WrongTypeSpecification "Specification of function is not a function type.")
| _ -> Error (`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.")
let typecheck (program: t_exp) : (ftype, error) result =
let* typeprogram = evaluate_type program VariableMap.empty in
match typeprogram with
FunctionType ([IntegerType], IntegerType) -> Ok (FunctionType ([IntegerType], IntegerType))
| _ -> Error (`WrongType "Program is not a function from int to int.")

2
lib/miniFun/TypeChecker.mli
View File

@ -1 +1 @@
val typecheck : Types.t_exp -> bool
val typecheck : Types.t_exp -> (Types.ftype, Types.error) result

12
lib/miniFun/Types.ml
View File

@ -48,8 +48,10 @@ 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
type error = [
`AbsentAssignment of string
| `WrongType of string
| `DivisionByZero of string
| `WrongArity of string
| `WrongTypeSpecification of string
]

60
lib/miniFun/Types.mli
View File

@ -8,30 +8,30 @@ type ftype =
| 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
Integer of int (* x := a *)
| Boolean of bool (* v *)
| Variable of variable (* x *)
| Function of variable list * ftype * t_exp (* lambda x: t. x *)
| Application of t_exp * t_exp list (* x x *)
| Plus of t_exp * t_exp (* x + x *)
| Minus of t_exp * t_exp (* x - x *)
| Times of t_exp * t_exp (* x * x *)
| Division of t_exp * t_exp (* x / x *)
| Modulo of t_exp * t_exp (* x % x *)
| Power of t_exp * t_exp (* x ^ x *)
| PowerMod of t_exp * t_exp * t_exp (* (x ^ x) % x *)
| Rand of t_exp (* rand(0, x) *)
| BAnd of t_exp * t_exp (* x and x *)
| BOr of t_exp * t_exp (* x or x *)
| BNot of t_exp (* not x *)
| Cmp of t_exp * t_exp (* x == x *)
| CmpLess of t_exp * t_exp (* x < x *)
| CmpLessEq of t_exp * t_exp (* x <= x *)
| CmpGreater of t_exp * t_exp (* x > x *)
| CmpGreaterEq of t_exp * t_exp (* x >= x *)
| IfThenElse of t_exp * t_exp * t_exp (* if b then c else c *)
| LetIn of variable * t_exp * t_exp (* let x = x in x *)
| LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x*)
type permittedValues =
IntegerPermitted of int
@ -48,8 +48,10 @@ 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
type error = [
`AbsentAssignment of string
| `WrongType of string
| `DivisionByZero of string
| `WrongArity of string
| `WrongTypeSpecification of string
]

1
lib/miniImp/Types.ml
View File

@ -32,7 +32,6 @@ and a_exp =
| Rand of a_exp (* rand(0, a) *)
module VariableMap = Map.Make(String)
type memory = {

1
lib/miniImp/Types.mli
View File

@ -32,7 +32,6 @@ and a_exp =
| Rand of a_exp (* rand(0, a) *)
module VariableMap : Map.S with type key = variable
type memory = {

26
test/testingFun.ml
View File

@ -11,7 +11,7 @@ let program =
)
;;
Printf.printf "Identity program: %d\n" (reduce program 1)
Printf.printf "Identity program: %d\n" (Result.get_ok (reduce program 1))
(* -------------------------------------------------------------------------- *)
(* Constant program *)
@ -23,7 +23,7 @@ let program =
)
;;
Printf.printf "Constant program: %d\n" (reduce program 10)
Printf.printf "Constant program: %d\n" (Result.get_ok (reduce program 10))
(* -------------------------------------------------------------------------- *)
(* Partial application of function program *)
@ -37,7 +37,7 @@ let program =
)
;;
Printf.printf "Partial application of function program: %d\n" (reduce program 2)
Printf.printf "Partial application of function program: %d\n" (Result.get_ok (reduce program 2))
(* -------------------------------------------------------------------------- *)
(* Partial application of function program *)
@ -53,7 +53,7 @@ let program =
)
;;
Printf.printf "Partial application of function program: %d\n" (reduce program 3)
Printf.printf "Partial application of function program: %d\n" (Result.get_ok (reduce program 3))
(* -------------------------------------------------------------------------- *)
(* Passing functions to functions program *)
@ -89,8 +89,8 @@ let program =
)
;;
Printf.printf "Passing functions to functions program 1: %d\n" (reduce program (3));
Printf.printf "Passing functions to functions program 2: %d\n" (reduce program (-3))
Printf.printf "Passing functions to functions program 1: %d\n" (Result.get_ok (reduce program (3)));
Printf.printf "Passing functions to functions program 2: %d\n" (Result.get_ok (reduce program (-3)))
(* -------------------------------------------------------------------------- *)
(* Recursive function program *)
@ -104,7 +104,7 @@ let program =
)
;;
Printf.printf "Recursive function program: %d\n" (reduce program 10)
Printf.printf "Recursive function program: %d\n" (Result.get_ok (reduce program 10))
(* -------------------------------------------------------------------------- *)
(* Scope program *)
@ -116,7 +116,7 @@ let program =
)
;;
Printf.printf "Scope program: %d\n" (reduce program 4)
Printf.printf "Scope program: %d\n" (Result.get_ok (reduce program 4))
(* -------------------------------------------------------------------------- *)
(* Factorial program *)
@ -130,7 +130,7 @@ let program =
)
;;
Printf.printf "Factorial program: %d\n" (reduce program 10)
Printf.printf "Factorial program: %d\n" (Result.get_ok (reduce program 10))
;;
(* -------------------------------------------------------------------------- *)
@ -154,7 +154,7 @@ let program =
)
;;
Printf.printf "Hailstone sequence's lenght program: %d\n" (reduce program 77031)
Printf.printf "Hailstone sequence's lenght program: %d\n" (Result.get_ok (reduce program 77031))
;;
(* -------------------------------------------------------------------------- *)
@ -176,7 +176,7 @@ let program =
)
;;
Printf.printf "Sum multiples of 3 and 5 program: %d\n" (reduce program 12345)
Printf.printf "Sum multiples of 3 and 5 program: %d\n" (Result.get_ok (reduce program 12345))
;;
(* -------------------------------------------------------------------------- *)
@ -190,7 +190,7 @@ let program =
;;
Printf.printf "Rand program: %b\n" ((reduce program 10) < 10)
Printf.printf "Rand program: %b\n" ((Result.get_ok (reduce program 10) < 10))
;;
(* -------------------------------------------------------------------------- *)
@ -213,5 +213,5 @@ let program =
;;
Printf.printf "Fibonacci program: %d\n" (reduce program 48)
Printf.printf "Fibonacci program: %d\n" (Result.get_ok (reduce program 48))
;;

42
test/testingTypeFun.expected
View File

@ -1,21 +1,21 @@
Error absent assignment program: error
Error wrong arity program 1: error
Error wrong arity program 2: error
Error wrong return type program: error
Error wrong specification program: error
Error wrong input type program: error
Error not a function program: error
Error if branches with different types program: error
Error if guard is not a boolean program: error
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
Error absent assignment program: error (success)
Error wrong arity program 1: error (success)
Error wrong arity program 2: error (success)
Error wrong return type program: error (success)
Error wrong specification program: error (success)
Error wrong input type program: error (success)
Error not a function program: error (success)
Error if branches with different types program: error (success)
Error if guard is not a boolean program: error (success)
Identity program: success
Constant program: success
Partial application of function program 1: success
Partial application of function program 2: success
Passing functions to functions program: success
Recursive function program: success
Scope program: success
Factorial program: success
Hailstone sequence's lenght program: success
Sum multiples of 3 and 5 program: success
Rand program: success
Fibonacci program: success

120
test/testingTypeFun.ml
View File

@ -8,14 +8,13 @@ let program =
Function
(["a"],
FunctionType ([IntegerType], IntegerType),
(Variable "x")
Plus (Variable "x", Integer 1)
)
;;
try
Printf.printf "Error absent assignment program: %b\n" (typecheck program)
with AbsentAssignment _ ->
Printf.printf "Error absent assignment program: error\n"
match typecheck program with
Error (`AbsentAssignment _) -> Printf.printf "Error absent assignment program: error (success)\n"
| _ -> Printf.printf "Error absent assignment program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error wrong arity program *)
@ -28,10 +27,9 @@ let program =
)
;;
try
Printf.printf "Error wrong arity program 1: %b\n" (typecheck program)
with WrongTypeSpecification _ ->
Printf.printf "Error wrong arity program 1: error\n"
match typecheck program with
Error (`WrongTypeSpecification _) -> Printf.printf "Error wrong arity program 1: error (success)\n"
| _ -> Printf.printf "Error wrong arity program 1: failed\n"
let program =
LetFun
@ -43,11 +41,9 @@ let program =
)
;;
try
Printf.printf "Error wrong arity program 2: %b\n" (typecheck program)
with WrongArity _ ->
Printf.printf "Error wrong arity program 2: error\n"
match typecheck program with
Error (`WrongArity _) -> Printf.printf "Error wrong arity program 2: error (success)\n"
| _ -> Printf.printf "Error wrong arity program 2: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error wrong return type program *)
@ -60,10 +56,9 @@ let program =
)
;;
try
Printf.printf "Error wrong return type program: %b\n" (typecheck program)
with WrongTypeSpecification _ ->
Printf.printf "Error wrong return type program: error\n"
match typecheck program with
Error (`WrongTypeSpecification _) -> Printf.printf "Error wrong return type program: error (success)\n"
| _ -> Printf.printf "Error wrong return type program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error wrong specification program *)
@ -76,10 +71,9 @@ let program =
)
;;
try
Printf.printf "Error wrong specification program: %b\n" (typecheck program)
with WrongTypeSpecification _ ->
Printf.printf "Error wrong specification program: error\n"
match typecheck program with
Error (`WrongTypeSpecification _) -> Printf.printf "Error wrong specification program: error (success)\n"
| _ -> Printf.printf "Error wrong specification program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error wrong input type program *)
@ -95,10 +89,9 @@ let program =
)
;;
try
Printf.printf "Error wrong input type program: %b\n" (typecheck program)
with WrongType _ ->
Printf.printf "Error wrong input type program: error\n"
match typecheck program with
Error (`WrongType _) -> Printf.printf "Error wrong input type program: error (success)\n"
| _ -> Printf.printf "Error wrong input type program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error not a function program *)
@ -110,10 +103,9 @@ let program =
)
;;
try
Printf.printf "Error not a function program: %b\n" (typecheck program)
with WrongType _ ->
Printf.printf "Error not a function program: error\n"
match typecheck program with
Error (`WrongType _) -> Printf.printf "Error not a function program: error (success)\n"
| _ -> Printf.printf "Error not a function program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error if branches with different types program *)
@ -126,10 +118,9 @@ let program =
)
;;
try
Printf.printf "Error if branches with different types program: %b\n" (typecheck program)
with WrongType _ ->
Printf.printf "Error if branches with different types program: error\n"
match typecheck program with
Error (`WrongType _) -> Printf.printf "Error if branches with different types program: error (success)\n"
| _ -> Printf.printf "Error if branches with different types program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Error if guard is not a boolean program *)
@ -142,11 +133,9 @@ let program =
)
;;
try
Printf.printf "Error if guard is not a boolean program: %b\n" (typecheck program)
with WrongType _ ->
Printf.printf "Error if guard is not a boolean program: error\n"
match typecheck program with
Error (`WrongType _) -> Printf.printf "Error if guard is not a boolean program: error (success)\n"
| _ -> Printf.printf "Error if guard is not a boolean program: failed\n"
(* -------------------------------------------------------------------------- *)
@ -159,7 +148,9 @@ let program =
)
;;
Printf.printf "Identity program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Identity program: success\n"
| _ -> Printf.printf "Identity program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Constant program *)
@ -171,7 +162,9 @@ let program =
)
;;
Printf.printf "Constant program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Constant program: success\n"
| _ -> Printf.printf "Constant program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Partial application of function program *)
@ -185,7 +178,9 @@ let program =
)
;;
Printf.printf "Partial application of function program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Partial application of function program 1: success\n"
| _ -> Printf.printf "Partial application of function program 1: failed\n"
(* -------------------------------------------------------------------------- *)
(* Partial application of function program *)
@ -201,7 +196,9 @@ let program =
)
;;
Printf.printf "Partial application of function program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Partial application of function program 2: success\n"
| _ -> Printf.printf "Partial application of function program 2: failed\n"
(* -------------------------------------------------------------------------- *)
(* Passing functions to functions program *)
@ -237,7 +234,9 @@ let program =
)
;;
Printf.printf "Passing functions to functions program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Passing functions to functions program: success\n"
| _ -> Printf.printf "Passing functions to functions program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Recursive function program *)
@ -251,7 +250,9 @@ let program =
)
;;
Printf.printf "Recursive function program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Recursive function program: success\n"
| _ -> Printf.printf "Recursive function program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Scope program *)
@ -263,7 +264,9 @@ let program =
)
;;
Printf.printf "Scope program: %b\n" (typecheck program)
match typecheck program with
Ok _ -> Printf.printf "Scope program: success\n"
| _ -> Printf.printf "Scope program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Factorial program *)
@ -277,8 +280,9 @@ let program =
)
;;
Printf.printf "Factorial program: %b\n" (typecheck program)
;;
match typecheck program with
Ok _ -> Printf.printf "Factorial program: success\n"
| _ -> Printf.printf "Factorial program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Hailstone sequence's lenght program *)
@ -301,8 +305,9 @@ let program =
)
;;
Printf.printf "Hailstone sequence's lenght program: %b\n" (typecheck program)
;;
match typecheck program with
Ok _ -> Printf.printf "Hailstone sequence's lenght program: success\n"
| _ -> Printf.printf "Hailstone sequence's lenght program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Sum multiples of 3 and 5 program *)
@ -323,8 +328,9 @@ let program =
)
;;
Printf.printf "Sum multiples of 3 and 5 program: %b\n" (typecheck program)
;;
match typecheck program with
Ok _ -> Printf.printf "Sum multiples of 3 and 5 program: success\n"
| _ -> Printf.printf "Sum multiples of 3 and 5 program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Rand program *)
@ -337,8 +343,9 @@ let program =
;;
Printf.printf "Rand program: %b\n" (typecheck program)
;;
match typecheck program with
Ok _ -> Printf.printf "Rand program: success\n"
| _ -> Printf.printf "Rand program: failed\n"
(* -------------------------------------------------------------------------- *)
(* Fibonacci program *)
@ -360,5 +367,6 @@ let program =
;;
Printf.printf "Fibonacci program: %b\n" (typecheck program)
;;
match typecheck program with
Ok _ -> Printf.printf "Fibonacci program: success\n"
| _ -> Printf.printf "Fibonacci program: failed\n"