1
0
Fork 0
This repository has been archived on 2024-05-03. You can view files and clone it, but cannot push or open issues or pull requests.
unification-pfa/lib/inference.ml

56 lines
2.2 KiB
OCaml
Raw Normal View History

(** Infer the type of a given term and, if exists, returns the type of the term *)
2024-04-13 15:51:57 +02:00
let typeof t =
let rec infer env = function
| Term.Var id ->
( (match TypeSubstitution.find id env with
| Some ty -> Some ty
| None -> Some (Type.Var id))
, env )
| Term.IntConst _ -> Some Type.Int, env
| Term.Binop (t1, _, t2) ->
(* Both operands must have type Int *)
(match infer env t1, infer env t2 with
| (Some ty1, _), (Some ty2, _) ->
(match Unification.unify ty1 Type.Int, Unification.unify ty2 Type.Int with
| Some env1, Some env2 -> Some Type.Int, TypeSubstitution.compose env1 env2
| _ -> None, env)
| _, _ -> None, env)
| Term.Pair (t1, t2) ->
(match infer env t1, infer env t2 with
| (Some ty1, _), (Some ty2, _) -> Some (Type.Product (ty1, ty2)), env
| _, _ -> None, env)
| Term.Proj (proj, t) ->
(* Check if the term is a pair *)
(match infer env t with
| Some (Type.Product (ty1, ty2)), _ ->
(match proj with
| Term.First -> Some ty1, env
| Term.Second -> Some ty2, env)
| _ -> None, env)
| Term.Fun (id, body) ->
(match infer env body with
| Some ty_body, env' ->
(match infer env' (Term.Var id) with
| Some ty, _ -> Some (Type.Arrow (ty, ty_body)), env'
| None, _ -> Some (Type.Arrow (Type.Var id, ty_body)), env')
| _ -> None, env)
| Term.App (t1, t2) ->
2024-04-14 03:49:59 +02:00
(* Infer the type of t1 and t2 *)
2024-04-13 15:51:57 +02:00
(match infer env t1, infer env t2 with
| (Some (Type.Arrow (ty_param, ty_fn)), _), (Some ty_args, _) ->
2024-04-14 03:49:59 +02:00
(* Check if the argument type matches the parameter type *)
2024-04-13 15:51:57 +02:00
(match Unification.unify ty_param ty_args with
| Some _ -> Some ty_fn, env
| None -> None, env)
2024-04-14 03:49:59 +02:00
| (Some _ (* (Type.Var _ as ty1) *), _), _ ->
(* On this case we may have a function represented as the variable *)
(* let ty2 = Type.Arrow (ty1, ty1) in
(match Unification.unify ty1 ty2 with
| Some env' -> Some ty2, env'
| _ -> None, env) *)
None, env
| _ -> None, env)
2024-04-13 15:51:57 +02:00
in
fst (infer TypeSubstitution.empty t)
;;