Adding comments
This commit is contained in:
@ -9,30 +9,48 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
|||||||
match program with
|
match program with
|
||||||
Integer _ -> Ok IntegerType
|
Integer _ -> Ok IntegerType
|
||||||
| Boolean _ -> Ok BooleanType
|
| Boolean _ -> Ok BooleanType
|
||||||
| Variable x -> (
|
| Variable x -> ( (* check for the type in the context *)
|
||||||
match VariableMap.find_opt x context with
|
match VariableMap.find_opt x context with
|
||||||
None -> Error (`AbsentAssignment ("The variable " ^ x ^ " is not defined."))
|
None -> Error (`AbsentAssignment
|
||||||
|
("The variable " ^ x ^ " is not defined."))
|
||||||
| Some t -> Ok t
|
| Some t -> Ok t
|
||||||
)
|
)
|
||||||
| Function (xs, typef, fbody) -> (
|
| Function (xs, typef, fbody) -> (
|
||||||
|
(* first check that the function has the right specified type then check
|
||||||
|
that the number of inputs are the right number, finally eval the type
|
||||||
|
of the body using the bindings for the inputs *)
|
||||||
match typef with
|
match typef with
|
||||||
FunctionType (tin, tout) -> (
|
FunctionType (tin, tout) -> (
|
||||||
if List.length xs <> List.length tin then
|
if List.length xs <> List.length tin then
|
||||||
Error (`WrongTypeSpecification "Type specification for function has wrong arity.")
|
Error (`WrongTypeSpecification
|
||||||
|
("Type specification for function has wrong arity."))
|
||||||
else
|
else
|
||||||
let context1 = List.fold_left2 (fun acc x t -> VariableMap.add x t acc) context xs tin in
|
let context1 = List.fold_left2
|
||||||
|
(fun acc x t -> VariableMap.add x t acc)
|
||||||
|
context
|
||||||
|
xs
|
||||||
|
tin
|
||||||
|
in
|
||||||
let* typefbody = evaluate_type fbody context1 in
|
let* typefbody = evaluate_type fbody context1 in
|
||||||
match (typefbody = tout) with
|
if (typefbody = tout) then
|
||||||
(false) -> Error (`WrongTypeSpecification "Function does not return specified type.")
|
Ok typef
|
||||||
| (true) -> Ok typef
|
else
|
||||||
|
Error (`WrongTypeSpecification
|
||||||
|
("Function does not return specified type."))
|
||||||
)
|
)
|
||||||
| _ -> Error (`WrongTypeSpecification "Specification of function is not a function type.")
|
| _ -> Error (`WrongTypeSpecification
|
||||||
|
("Specification of function is not a function type."))
|
||||||
)
|
)
|
||||||
| Application (f, xs) -> (
|
| Application (f, xs) -> (
|
||||||
|
(* check that the type is actually a function, then checks that the
|
||||||
|
supplied inputs are of the right type, returns the return type if all
|
||||||
|
inputs are supplied, otherwise a function from the remaining inputs to
|
||||||
|
the output types *)
|
||||||
let* evalf = evaluate_type f context in
|
let* evalf = evaluate_type f context in
|
||||||
match evalf with
|
match evalf with
|
||||||
FunctionType (tin, tout) -> (
|
FunctionType (tin, tout) -> (
|
||||||
let rec helper params typeparams =
|
let rec helper (params: t_exp list) (typeparams: ftype list) =
|
||||||
|
(* consumes until params are exausted *)
|
||||||
match (params, typeparams) with
|
match (params, typeparams) with
|
||||||
([], _) -> Ok typeparams
|
([], _) -> Ok typeparams
|
||||||
| (_, []) -> Error (`WrongArity ("Function application has arity " ^
|
| (_, []) -> Error (`WrongArity ("Function application has arity " ^
|
||||||
@ -72,8 +90,10 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
|||||||
let* typez = evaluate_type z context in
|
let* typez = evaluate_type z context in
|
||||||
match typex, typey, typez with
|
match typex, typey, typez with
|
||||||
| (IntegerType, IntegerType, IntegerType) -> Ok IntegerType
|
| (IntegerType, IntegerType, IntegerType) -> Ok IntegerType
|
||||||
| (IntegerType, IntegerType, _) -> Error (`WrongType "Third term is not an integer.")
|
| (IntegerType, IntegerType, _) -> Error (`WrongType ("Third term is " ^
|
||||||
| (IntegerType, _, _) -> Error (`WrongType "Second term is not an integer.")
|
"not an integer."))
|
||||||
|
| (IntegerType, _, _) -> Error (`WrongType
|
||||||
|
("Second term is not an integer."))
|
||||||
| (_, _, _) -> Error (`WrongType "First term is not an integer.")
|
| (_, _, _) -> Error (`WrongType "First term is not an integer.")
|
||||||
)
|
)
|
||||||
| Rand (x) -> (
|
| Rand (x) -> (
|
||||||
@ -123,26 +143,37 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
|||||||
| (_, _, _) -> Error (`WrongType "If guard is not a boolean.")
|
| (_, _, _) -> Error (`WrongType "If guard is not a boolean.")
|
||||||
)
|
)
|
||||||
| LetIn (x, xval, rest) ->
|
| LetIn (x, xval, rest) ->
|
||||||
|
(* bind the type to the variable name in the context *)
|
||||||
let* typex = evaluate_type xval context in
|
let* typex = evaluate_type xval context in
|
||||||
evaluate_type rest (VariableMap.add x typex context)
|
evaluate_type rest (VariableMap.add x typex context)
|
||||||
| LetFun (f, xs, typef, fbody, rest) ->
|
| LetFun (f, xs, typef, fbody, rest) ->
|
||||||
|
(* like with the function type, but also add f itself to the bindings *)
|
||||||
match typef with
|
match typef with
|
||||||
FunctionType (tin, tout) -> (
|
FunctionType (tin, tout) -> (
|
||||||
if List.length xs <> List.length tin then
|
if List.length xs <> List.length tin then
|
||||||
Error (`WrongArity "Type specification for function has wrong arity.")
|
Error (`WrongArity "Type specification for function has wrong arity.")
|
||||||
else
|
else
|
||||||
let context1 = VariableMap.add f typef context in
|
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
|
let context2 = List.fold_left2
|
||||||
|
(fun acc x t -> VariableMap.add x t acc)
|
||||||
|
context1
|
||||||
|
xs
|
||||||
|
tin
|
||||||
|
in
|
||||||
let* typefbody = evaluate_type fbody context2 in
|
let* typefbody = evaluate_type fbody context2 in
|
||||||
let* typerest = evaluate_type rest context1 in
|
let* typerest = evaluate_type rest context1 in
|
||||||
match (typefbody = tout, typerest) with
|
match (typefbody = tout, typerest) with
|
||||||
(false, _) -> Error (`WrongTypeSpecification "Function does not return specified type.")
|
(false, _) -> Error (`WrongTypeSpecification
|
||||||
|
"Function does not return specified type.")
|
||||||
| (true, t) -> Ok t
|
| (true, t) -> Ok t
|
||||||
)
|
)
|
||||||
| _ -> Error (`WrongTypeSpecification "Specification of function is not a function type.")
|
| _ -> Error (`WrongTypeSpecification
|
||||||
|
"Specification of function is not a function type.")
|
||||||
|
|
||||||
let typecheck (program: t_exp) : (ftype, error) result =
|
let typecheck (program: t_exp) : (ftype, error) result =
|
||||||
let* typeprogram = evaluate_type program VariableMap.empty in
|
let* typeprogram = evaluate_type program VariableMap.empty in
|
||||||
match typeprogram with
|
match typeprogram with
|
||||||
FunctionType ([IntegerType], IntegerType) -> Ok (FunctionType ([IntegerType], IntegerType))
|
FunctionType ([IntegerType], IntegerType) -> (
|
||||||
|
Ok (FunctionType ([IntegerType], IntegerType))
|
||||||
|
)
|
||||||
| _ -> Error (`WrongType "Program is not a function from int to int.")
|
| _ -> Error (`WrongType "Program is not a function from int to int.")
|
||||||
|
|||||||
Reference in New Issue
Block a user