Started work for type inference
This commit is contained in:
elvis
@ -5,175 +5,56 @@ Random.self_init ()
|
|||||||
|
|
||||||
let (let*) = Result.bind
|
let (let*) = Result.bind
|
||||||
|
|
||||||
let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, 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
|
|
||||||
)
|
|
||||||
| 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
|
|
||||||
FunctionType (tin, tout) -> (
|
|
||||||
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
|
|
||||||
let* typefbody = evaluate_type fbody context1 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, 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
|
|
||||||
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))
|
|
||||||
)
|
|
||||||
| _ -> 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.")
|
|
||||||
)
|
|
||||||
| 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, xs, typef, fbody, rest) ->
|
|
||||||
(* like with the function type, 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
|
|
||||||
)
|
|
||||||
| _ -> Error (`WrongTypeSpecification
|
|
||||||
"Specification of function is not a function type.")
|
|
||||||
|
|
||||||
let typecheck (program: t_exp) : (ftype, error) result =
|
let rec principalTypings (D: ) (e: t_exp) : () result
|
||||||
let* typeprogram = evaluate_type program VariableMap.empty in
|
|
||||||
match typeprogram with
|
let evaluate_type (_program: t_exp) (_context: typingshape) : (typingshape, error) result =
|
||||||
FunctionType ([IntegerType], IntegerType) -> (
|
failwith "asd"
|
||||||
Ok (FunctionType ([IntegerType], IntegerType))
|
(* match program with *)
|
||||||
)
|
(* Integer _ -> Ok (VariableMap.empty, IntegerType) *)
|
||||||
| _ -> Error (`WrongType "Program is not a function from int to int.")
|
(* | 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 typecheck (_program: t_exp) : (ftype, error) result =
|
||||||
|
failwith "Not Implemented"
|
||||||
|
|||||||
@ -1,12 +1,21 @@
|
|||||||
type variable = string
|
type variable = string
|
||||||
|
|
||||||
|
let globalIdentifier = ref 1
|
||||||
|
|
||||||
module VariableMap = Map.Make(String)
|
module VariableMap = Map.Make(String)
|
||||||
module VariableSet = Set.Make(String)
|
module VariableSet = Set.Make(String)
|
||||||
|
|
||||||
type ftype =
|
type ftype =
|
||||||
IntegerType
|
IntegerType
|
||||||
| BooleanType
|
| BooleanType
|
||||||
|
| PolimorphicType of string
|
||||||
| FunctionType of ftype list * ftype
|
| FunctionType of ftype list * ftype
|
||||||
|
type fsubstitution = (* goes from polimorphic types to types *)
|
||||||
|
ftype VariableMap.t
|
||||||
|
type fenvironment = (* goes from variables to types *)
|
||||||
|
ftype VariableMap.t
|
||||||
|
type typingshape = (* tuple of a simple type environment and a simple type *)
|
||||||
|
fenvironment * ftype
|
||||||
|
|
||||||
type t_exp =
|
type t_exp =
|
||||||
Integer of int (* x := a *)
|
Integer of int (* x := a *)
|
||||||
@ -32,7 +41,7 @@ type t_exp =
|
|||||||
| CmpGreaterEq 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 *)
|
| 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 *)
|
| 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*)
|
| LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x *)
|
||||||
|
|
||||||
type permittedValues =
|
type permittedValues =
|
||||||
IntegerPermitted of int
|
IntegerPermitted of int
|
||||||
|
|||||||
@ -1,12 +1,47 @@
|
|||||||
type variable = string
|
type variable = string
|
||||||
|
|
||||||
|
val globalIdentifier : int ref
|
||||||
|
|
||||||
module VariableMap : Map.S with type key = variable
|
module VariableMap : Map.S with type key = variable
|
||||||
module VariableSet : Set.S with type elt = string
|
module VariableSet : Set.S with type elt = string
|
||||||
|
|
||||||
type ftype =
|
type ftype =
|
||||||
IntegerType
|
IntegerType
|
||||||
| BooleanType
|
| BooleanType
|
||||||
|
| PolimorphicType of variable
|
||||||
| FunctionType of ftype list * ftype
|
| FunctionType of ftype list * ftype
|
||||||
|
type fsubstitution = (* goes from polimorphic types to types *)
|
||||||
|
ftype VariableMap.t
|
||||||
|
type fenvironment = (* goes from variables to types *)
|
||||||
|
ftype VariableMap.t
|
||||||
|
type typingshape = (* tuple of a simple type environment and a simple type *)
|
||||||
|
fenvironment * ftype
|
||||||
|
|
||||||
|
type intermediaryType =
|
||||||
|
IInteger
|
||||||
|
| IBoolean
|
||||||
|
| IVariable of variable
|
||||||
|
| IFunction of variable list * ftype list * intermediaryType
|
||||||
|
| IApplication of intermediaryType * intermediaryType list
|
||||||
|
| IPlus of intermediaryType * intermediaryType
|
||||||
|
| IMinus of intermediaryType * intermediaryType
|
||||||
|
| ITimes of intermediaryType * intermediaryType
|
||||||
|
| IDivision of intermediaryType * intermediaryType
|
||||||
|
| IModulo of intermediaryType * intermediaryType
|
||||||
|
| IPower of intermediaryType * intermediaryType
|
||||||
|
| IPowerMod of intermediaryType * intermediaryType * intermediaryType
|
||||||
|
| IRand of intermediaryType
|
||||||
|
| IBAnd of intermediaryType * intermediaryType
|
||||||
|
| IBOr of intermediaryType * intermediaryType
|
||||||
|
| IBNot of intermediaryType
|
||||||
|
| ICmp of intermediaryType * intermediaryType
|
||||||
|
| ICmpLess of intermediaryType * intermediaryType
|
||||||
|
| ICmpLessEq of intermediaryType * intermediaryType
|
||||||
|
| ICmpGreater of intermediaryType * intermediaryType
|
||||||
|
| ICmpGreaterEq of intermediaryType * intermediaryType
|
||||||
|
| IIfThenElse of intermediaryType * intermediaryType * intermediaryType
|
||||||
|
| ILetIn of variable * ftype * intermediaryType * intermediaryType
|
||||||
|
| ILetFun of variable * ftype * variable list * ftype list * intermediaryType * intermediaryType
|
||||||
|
|
||||||
type t_exp =
|
type t_exp =
|
||||||
Integer of int (* x := a *)
|
Integer of int (* x := a *)
|
||||||
@ -32,7 +67,7 @@ type t_exp =
|
|||||||
| CmpGreaterEq 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 *)
|
| 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 *)
|
| 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*)
|
| LetFun of variable * variable list * ftype * t_exp * t_exp (* let rec x: t. x in x *)
|
||||||
|
|
||||||
type permittedValues =
|
type permittedValues =
|
||||||
IntegerPermitted of int
|
IntegerPermitted of int
|
||||||
|
|||||||
@ -11,3 +11,15 @@ let rec powmod a d = function
|
|||||||
| n ->
|
| n ->
|
||||||
let b = (powmod a d (n / 2)) mod d in
|
let b = (powmod a d (n / 2)) mod d in
|
||||||
(((b * b) mod d) * (if n mod 2 = 0 then 1 else a)) mod d
|
(((b * b) mod d) * (if n mod 2 = 0 then 1 else a)) mod d
|
||||||
|
|
||||||
|
|
||||||
|
let alphabet = "abcdefghijklmnopqrstuvwxyz"
|
||||||
|
let base = 26
|
||||||
|
|
||||||
|
let rec fromIntToString (x: int) : string =
|
||||||
|
if x < 0 then
|
||||||
|
""
|
||||||
|
else if x < base then
|
||||||
|
String.get alphabet x |> String.make 1
|
||||||
|
else
|
||||||
|
(fromIntToString (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1)
|
||||||
|
|||||||
@ -1,3 +1,5 @@
|
|||||||
val pow : int -> int -> int
|
val pow : int -> int -> int
|
||||||
|
|
||||||
val powmod : int -> int -> int -> int
|
val powmod : int -> int -> int -> int
|
||||||
|
|
||||||
|
val fromIntToString : int -> string
|
||||||
|
|||||||
Reference in New Issue
Block a user