59 lines
1.6 KiB
OCaml
59 lines
1.6 KiB
OCaml
(** Map of an id to a type *)
|
|
module IdentifierMap = Map.Make (Identifier)
|
|
|
|
(** Map type *)
|
|
type t = Type.t IdentifierMap.t
|
|
|
|
(* Empty substitution *)
|
|
let empty = IdentifierMap.empty
|
|
|
|
(** Create a substitution with one element *)
|
|
let singleton id ty = IdentifierMap.singleton id ty
|
|
|
|
(** Apply substitution to a type *)
|
|
let rec apply subst = function
|
|
| Type.Int -> Type.Int
|
|
| Type.Var id as t ->
|
|
(* Look for a substitution in the map *)
|
|
(match IdentifierMap.find_opt id subst with
|
|
| Some ty' -> apply subst ty'
|
|
| None -> t)
|
|
| Type.Product (ty1, ty2) -> Type.Product (apply subst ty1, apply subst ty2)
|
|
| Type.Arrow (ty1, ty2) -> Type.Arrow (apply subst ty1, apply subst ty2)
|
|
;;
|
|
|
|
(** Compose two substitutions, last with priority *)
|
|
let compose s2 s1 =
|
|
let merger =
|
|
IdentifierMap.merge
|
|
(* ID type_s1 type_s2 *)
|
|
(fun _ ty1 ty2 ->
|
|
match ty1, ty2 with
|
|
(* Give priority to s1 *)
|
|
| Some ty1', Some _ -> Some ty1'
|
|
(* Use of the substitution we already have *)
|
|
| Some ty1', None -> Some ty1'
|
|
| None, Some ty2' -> Some ty2'
|
|
(* Variable untyped *)
|
|
| None, None -> None)
|
|
s1
|
|
s2
|
|
in
|
|
merger
|
|
;;
|
|
|
|
let to_string map =
|
|
let rec ty_str = function
|
|
| Type.Var s -> "Var('" ^ s ^ "')"
|
|
| Type.Int -> "Int"
|
|
| Type.Product (a, b) -> "Product(" ^ ty_str a ^ ", " ^ ty_str b ^ ")"
|
|
| Type.Arrow (a, b) -> "Arrow(" ^ ty_str a ^ ", " ^ ty_str b ^ ")"
|
|
in
|
|
"{"
|
|
^ (IdentifierMap.bindings map
|
|
|> List.map (fun (id, ty) -> Printf.sprintf "'%s' typed as %s" id (ty_str ty))
|
|
|> String.concat "\n")
|
|
^ "}"
|
|
;;
|
|
|
|
let find = IdentifierMap.find_opt
|