Paris7/unification-pfa
Archived
1
0
Fork 0
Code Issues Activity

small fixes

Browse source
This commit is contained in:
Mylloon 2024-04-11 11:18:14 +02:00
parent 03e0e0244d
commit 8e11322256
Signed by: Anri
GPG key ID: A82D63DFF8D1317F
3 changed files with 17 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
lib/typeSubstitution.ml
View file

@ -12,11 +12,12 @@ let singleton id ty = IdentifierMap.singleton id ty
(** Apply substitution to a type *) (** Apply substitution to a type *)
let rec apply subst = function let rec apply subst = function
| Type.Int -> Type.Int
| Type.Var id as t -> | Type.Var id as t ->
(* Look for a substitution in the map *)
(match IdentifierMap.find_opt id subst with (match IdentifierMap.find_opt id subst with
| Some ty' -> apply subst ty' | Some ty' -> apply subst ty'
| None -> t) | None -> t)
| Type.Int -> Type.Int
| Type.Product (ty1, ty2) -> Type.Product (apply subst ty1, apply subst ty2) | Type.Product (ty1, ty2) -> Type.Product (apply subst ty1, apply subst ty2)
| Type.Arrow (ty1, ty2) -> Type.Arrow (apply subst ty1, apply subst ty2) | Type.Arrow (ty1, ty2) -> Type.Arrow (apply subst ty1, apply subst ty2)
;; ;;
@ -27,10 +28,10 @@ let compose s2 s1 =
(fun _ ty1 ty2 -> (fun _ ty1 ty2 ->
match ty1, ty2 with match ty1, ty2 with
(* If we have 2, we pick one of them *) (* If we have 2, we pick one of them *)
| Some ty1, Some _ -> Some (apply s2 ty1) | Some ty1', Some _ -> Some (apply s2 ty1')
(* If we have 1, we pick the one we have *) (* If we have 1, we pick the one we have *)
| Some ty1, None -> Some (apply s2 ty1) | Some ty1', None -> Some (apply s2 ty1')
| None, Some ty2 -> Some (apply s2 ty2) | None, Some ty2' -> Some (apply s2 ty2')
(* If we have 0, we return nothing *) (* If we have 0, we return nothing *)
| None, None -> None) | None, None -> None)
s1 s1

2
lib/typeSubstitution.mli
View file

@ -5,4 +5,4 @@ val apply : t -> Type.t -> Type.t
(* compose s2 s1 : first s1, then s2 *) (* compose s2 s1 : first s1, then s2 *)
val compose : t -> t -> t val compose : t -> t -> t
val empty : t val empty : t
val singleton : Identifier.t -> Type.t -> Type.t Map.Make(Identifier).t val singleton : Identifier.t -> Type.t -> t

19
lib/unification.ml
View file

@ -1,16 +1,19 @@
(** Unify 2 types and, if exists, returns the substitution *) (** Unify 2 types and, if exists, returns the substitution *)
let rec unify ty1 ty2 = let rec unify ty1 ty2 =
match ty1, ty2 with match ty1, ty2 with
| Type.Product (p1_ty1, p1_ty2), Type.Product (p2_ty1, p2_ty2) (* Same types *)
| Type.Arrow (p1_ty1, p1_ty2), Type.Arrow (p2_ty1, p2_ty2) -> | Type.Int, Type.Int -> Some TypeSubstitution.empty
(match unify p1_ty1 p2_ty1 with | Type.Var id1, Type.Var id2 when id1 = id2 -> Some TypeSubstitution.empty
(* Different types *)
| Type.Var id, ty | ty, Type.Var id -> Some (TypeSubstitution.singleton id ty)
| Type.Product (l1, r1), Type.Product (l2, r2) | Type.Arrow (l1, r1), Type.Arrow (l2, r2)
->
(match unify l1 l2 with
| Some s1 -> | Some s1 ->
(match (* Apply the substitution *)
unify (TypeSubstitution.apply s1 p1_ty2) (TypeSubstitution.apply s1 p2_ty2) (match unify (TypeSubstitution.apply s1 r1) (TypeSubstitution.apply s1 r2) with
with
| Some s2 -> Some (TypeSubstitution.compose s2 s1) | Some s2 -> Some (TypeSubstitution.compose s2 s1)
| None -> None) | None -> None)
| None -> None) | None -> None)
| ty1, ty2 when ty1 = ty2 -> Some TypeSubstitution.empty | _, _ -> None
| _ -> None
;; ;;