208 lines
8.2 KiB
OCaml
208 lines
8.2 KiB
OCaml
module Utility = Utility
|
|
open Types;;
|
|
|
|
Random.self_init ()
|
|
|
|
let (let*) = Result.bind
|
|
|
|
let evaluate_type_polimorphic (_program: t_exp) (_context: typingshape) : (typingshape, error) result =
|
|
failwith "Not implemented"
|
|
(* match program with *)
|
|
(* Integer _ -> Ok (VariableMap.empty, IntegerType) *)
|
|
(* | Boolean _ -> Ok (VariableMap.empty, BooleanType) *)
|
|
(* | Variable x -> ( *)
|
|
(* match (VariableMap.find_opt x (fst context)) with *)
|
|
(* (None) -> ( *)
|
|
(* let u = PolimorphicType (Utility.fromIntToString !globalIdentifier) in *)
|
|
(* globalIdentifier := !globalIdentifier + 1; *)
|
|
(* Ok (VariableMap.singleton x u, u) *)
|
|
(* ) *)
|
|
(* | (Some u) -> Ok (VariableMap.singleton x u, u) *)
|
|
(* ) *)
|
|
(* | Function (xs, typef, fbody) -> failwith "Not Implemented" *)
|
|
(* | Application (f, xs) -> failwith "Not Implemented" *)
|
|
(* | Plus (x, y) *)
|
|
(* | Minus (x, y) *)
|
|
(* | Times (x, y) *)
|
|
(* | Division (x, y) *)
|
|
(* | Modulo (x, y) *)
|
|
(* | Power (x, y) -> ( *)
|
|
(* let* partialResx = evaluate_type x context in *)
|
|
(* let* partialResy = evaluate_type y context in *)
|
|
(* match (partialResx, partialResy) with *)
|
|
(* ((conx, IntegerType), (cony, IntegerType)) -> *)
|
|
(* Ok (VariableMap.union (fun _ x _ -> Some x) conx cony, *)
|
|
(* FunctionType ([IntegerType; IntegerType], IntegerType)) *)
|
|
(* | ((conx, PolimorphicType xv), (cony, IntegerType)) -> *)
|
|
(* Ok (unify ) *)
|
|
(* | ((_conx, IntegerType), (_cony, PolimorphicType _yv)) *)
|
|
(* | ((_conx, PolimorphicType _xv), (_cony, PolimorphicType _yv)) -> failwith "ads" *)
|
|
(* | (_, _) -> Error (`WrongType "The arguments are of the wrong type") *)
|
|
(* ) *)
|
|
(* | PowerMod (x, y, z) -> failwith "Not Implemented" *)
|
|
(* | Rand (x) -> failwith "Not Implemented" *)
|
|
(* | BAnd (x, y) *)
|
|
(* | BOr (x, y) -> failwith "Not Implemented" *)
|
|
(* | BNot (x) -> failwith "Not Implemented" *)
|
|
(* | Cmp (x, y) *)
|
|
(* | CmpLess (x, y) *)
|
|
(* | CmpLessEq (x, y) *)
|
|
(* | CmpGreater (x, y) *)
|
|
(* | CmpGreaterEq (x, y) -> failwith "Not Implemented" *)
|
|
(* | IfThenElse (guard, if_exp, else_exp) -> failwith "Not Implemented" *)
|
|
(* | LetIn (x, xval, rest) -> failwith "Not Implemented" *)
|
|
(* | LetFun (f, xs, typef, fbody, rest) -> failwith "Not Implemented" *)
|
|
|
|
let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, [> typechecking_error]) result =
|
|
match program with
|
|
Integer _ -> Ok IntegerType
|
|
| Boolean _ -> Ok BooleanType
|
|
| Variable x -> ( (* check for the type in the context *)
|
|
match VariableMap.find_opt x context with
|
|
None -> Error (`AbsentAssignment
|
|
("The variable " ^ x ^ " is not defined."))
|
|
| Some t -> Ok t
|
|
)
|
|
| 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
|
|
the type of the body using the bindings for the input *)
|
|
match typef with
|
|
FunctionType (tin, tout) -> (
|
|
let* typefbody = evaluate_type fbody (VariableMap.add x tin context) in
|
|
if (typefbody = tout) then
|
|
Ok typef
|
|
else
|
|
Error (`WrongTypeSpecification
|
|
("Function does not return specified type."))
|
|
)
|
|
| _ -> Error (`WrongTypeSpecification
|
|
("Specification of function is not a function type."))
|
|
)
|
|
| Application (f, x) -> (
|
|
let* evalf = evaluate_type f context in
|
|
let* evalx = evaluate_type x context in
|
|
match evalf with
|
|
FunctionType (tin, 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")
|
|
)
|
|
| Plus (x, y)
|
|
| Minus (x, y)
|
|
| Times (x, y)
|
|
| Division (x, y)
|
|
| Modulo (x, y)
|
|
| Power (x, y) -> (
|
|
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) -> (
|
|
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) -> (
|
|
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) -> (
|
|
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) -> (
|
|
let* typex = evaluate_type x context in
|
|
match typex with
|
|
| (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)
|
|
| CmpGreater (x, y)
|
|
| CmpGreaterEq (x, y) -> (
|
|
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) -> (
|
|
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
|
|
Ok t1
|
|
else
|
|
Error (`WrongType "If branches do not have the same type.")
|
|
)
|
|
| (_, _, _) -> Error (`WrongType "If guard is not a boolean.")
|
|
)
|
|
| LetIn (x, xval, rest) ->
|
|
(* 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, x, typef, fbody, rest) ->
|
|
(* like with the function case, but also add f itself to the bindings *)
|
|
match typef with
|
|
FunctionType (tin, tout) -> (
|
|
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.")
|
|
|
|
let typecheck (program: t_exp) : (ftype, [> typechecking_error]) result =
|
|
let* typeprogram = evaluate_type program VariableMap.empty in
|
|
match typeprogram with
|
|
FunctionType (IntegerType, IntegerType) -> (
|
|
Ok (typeprogram)
|
|
)
|
|
| _ -> Error (`WrongType "Program is not a function from int to int.")
|