Removed multiple input functions, added tuples, fixed parser
This commit is contained in:
@ -15,59 +15,35 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
||||
("The variable " ^ x ^ " is not defined."))
|
||||
| Some t -> Ok t
|
||||
)
|
||||
| Function (xs, typef, fbody) -> (
|
||||
| Tuple (x, y) -> (
|
||||
let* xtype = evaluate_type x context in
|
||||
let* ytype = evaluate_type y context in
|
||||
Ok (TupleType (xtype, ytype))
|
||||
)
|
||||
| Function (x, 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 *)
|
||||
the type of the body using the bindings for the input *)
|
||||
match typef with
|
||||
FunctionType (tin, tout) -> (
|
||||
if List.length xs <> List.length tin then
|
||||
Error (`WrongTypeSpecification
|
||||
("Type specification for function has wrong arity."))
|
||||
let* typefbody = evaluate_type fbody (VariableMap.add x tin context) in
|
||||
if (typefbody = tout) then
|
||||
Ok typef
|
||||
else
|
||||
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
|
||||
if (typefbody = tout) then
|
||||
Ok typef
|
||||
else
|
||||
Error (`WrongTypeSpecification
|
||||
("Function does not return specified type."))
|
||||
Error (`WrongTypeSpecification
|
||||
("Function does not return specified type."))
|
||||
)
|
||||
| _ -> Error (`WrongTypeSpecification
|
||||
("Specification of function is not a function type."))
|
||||
)
|
||||
| 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 *)
|
||||
| Application (f, x) -> (
|
||||
let* evalf = evaluate_type f context in
|
||||
let* evalx = evaluate_type x context in
|
||||
match evalf with
|
||||
FunctionType (tin, tout) -> (
|
||||
let rec helper (params: t_exp list) (typeparams: ftype list) =
|
||||
(* consumes until params are exausted *)
|
||||
match (params, typeparams) with
|
||||
([], _) -> 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 = Ok v then
|
||||
helper tlparams tltypeparams
|
||||
else
|
||||
Error (`WrongType "Argument with wrong type.")
|
||||
in
|
||||
let* typesremaining = helper xs tin in
|
||||
match typesremaining with
|
||||
[] -> Ok tout
|
||||
| t -> Ok (FunctionType (t, tout))
|
||||
if tin = evalx then
|
||||
Ok tout
|
||||
else
|
||||
Error (`WrongType "Appling function with wrong input type to value")
|
||||
)
|
||||
| _ -> Error (`WrongType "Applying to a non function type")
|
||||
)
|
||||
@ -117,6 +93,18 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
||||
| (BooleanType) -> Ok BooleanType
|
||||
| (_) -> Error (`WrongType "Term is not a boolean.")
|
||||
)
|
||||
| First (x) -> (
|
||||
let* typex = evaluate_type x context in
|
||||
match typex with
|
||||
| (TupleType (x, _)) -> Ok x
|
||||
| (_) -> Error (`WrongType "Term is not a tuple.")
|
||||
)
|
||||
| Second (x) -> (
|
||||
let* typex = evaluate_type x context in
|
||||
match typex with
|
||||
| (TupleType (_, x)) -> Ok x
|
||||
| (_) -> Error (`WrongType "Term is not a tuple.")
|
||||
)
|
||||
| Cmp (x, y)
|
||||
| CmpLess (x, y)
|
||||
| CmpLessEq (x, y)
|
||||
@ -146,26 +134,18 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
||||
(* bind the type to the variable name in the context *)
|
||||
let* typex = evaluate_type xval context in
|
||||
evaluate_type rest (VariableMap.add x typex context)
|
||||
| LetFun (f, xs, typef, fbody, rest) ->
|
||||
(* like with the function type, but also add f itself to the bindings *)
|
||||
| LetFun (f, x, typef, fbody, rest) ->
|
||||
(* like with the function case, but also add f itself to the bindings *)
|
||||
match typef with
|
||||
FunctionType (tin, tout) -> (
|
||||
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
|
||||
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
|
||||
let newcontext = VariableMap.add f typef context in
|
||||
let newcontextwithx = VariableMap.add x tin newcontext in
|
||||
let* typefbody = evaluate_type fbody newcontextwithx in
|
||||
let* typerest = evaluate_type rest newcontext in
|
||||
match (typefbody = tout, typerest) with
|
||||
(false, _) -> Error (`WrongTypeSpecification
|
||||
"Function does not return specified type.")
|
||||
| (true, t) -> Ok t
|
||||
)
|
||||
| _ -> Error (`WrongTypeSpecification
|
||||
"Specification of function is not a function type.")
|
||||
@ -173,7 +153,7 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
|
||||
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))
|
||||
FunctionType (IntegerType, IntegerType) -> (
|
||||
Ok (typeprogram)
|
||||
)
|
||||
| _ -> Error (`WrongType "Program is not a function from int to int.")
|
||||
|
||||
Reference in New Issue
Block a user