better API + documentation

src/lib/frontend/translate.ml

@@ -561,7 +561,7 @@ and handle_ty_app ?(update = false) ty_c l =
       List.fold_left2 (
         fun acc tv ty ->
           match tv with
-          | Ty.Tvar tv -> Ty.Subst.bind tv ty acc
+          | Ty.Tvar tv -> Ty.Subst.update tv ty acc
           | _ -> assert false
       ) Ty.Subst.id args tyl
     in

src/lib/structures/ty.ml

@@ -273,12 +273,24 @@ module Subst = struct
     | ty -> ty
     | exception Not_found -> Tvar tv
 
-  let bind (tv : tvar) ty sbt =
+  let update tv ty sbt =
     match ty with
     | Tvar tv' when DE.Ty.Var.equal tv tv' -> sbt
     | _ -> TvMap.add tv ty sbt
 
-  let is_in_dom = TvMap.mem
+  let try_bind tv ty sbt =
+    match ty with
+    | Tvar tv' when DE.Ty.Var.equal tv tv' -> sbt
+    | _ ->
+      TvMap.update tv
+        (fun ty_opt ->
+           match ty_opt with
+           | None -> Some ty
+           | Some t when equal t ty -> Some t
+           | Some t -> raise (TypeClash (t, ty)))
+        sbt
+
+  let in_domain = TvMap.mem
 
   let restrict set sbt =
     TvMap.filter (fun tv _ -> TvSet.mem tv set) sbt
@@ -306,15 +318,7 @@ type subst = Subst.subst
 (*** matching with a substitution mechanism ***)
 let rec matching s pat t =
   match pat, t with
-  | Tvar tv, _ ->
-    begin
-      if Subst.is_in_dom tv s then
-        (if not @@ equal (Subst.eval s tv) t then
-           raise (TypeClash (pat, t));
-         s)
-      else
-        Subst.bind tv t s
-    end
+  | Tvar tv, _ -> Subst.try_bind tv t s
   | Text (l1,s1) , Text (l2,s2) when DE.Ty.Const.equal s1 s2 ->
     List.fold_left2 matching s l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
@@ -368,11 +372,11 @@ let apply_subst =
 let rec fresh ty subst =
   match ty with
   | Tvar tv ->
-    if Subst.is_in_dom tv subst then
+    if Subst.in_domain tv subst then
       Subst.eval subst tv, subst
     else
       let ntv = fresh_tvar () in
-      ntv, Subst.bind tv ntv subst
+      ntv, Subst.update tv ntv subst
   | Text (args, n) ->
     let args, subst = fresh_list args subst in
     Text (args, n), subst
@@ -466,7 +470,7 @@ module Decls = struct
             List.fold_left2
               (fun sbt vty ty ->
                  match vty with
-                 | Tvar tv -> Subst.bind tv ty sbt
+                 | Tvar tv -> Subst.update tv ty sbt
                  | _ ->
                    Printer.print_err "vty = %a and ty = %a"
                      print vty print ty;

src/lib/structures/ty.mli

@@ -182,21 +182,46 @@ val trecord :
 
 module Subst : sig
   type subst
+  (** Type of substitution from type variables to types.
+
+      A substitution is equal to the identity substitution but for a finite
+      number of type variables.
+
+      The domain of the substitution is the set of types variable that
+      are not sent on itself. *)
 
   val id : subst
   (** The identity substitution. *)
 
   val is_id : subst -> bool
+  (** Check if the substitution is the identify substitution. *)
 
   val eval : subst -> tvar -> t
+  (** [eval sbt tv] returns the value of the substitution for [tv]. *)
+
+  val update : tvar -> t -> subst -> subst
+  (** [update tv ty sbt] replaces the value of [sbt] for [tv] by [ty].
+
+      If the previous value of [tv] in [sbt] is equal to [ty] for [equal],
+      the returned substitution is physically equal to [sbt]. *)
+
+  val try_bind : tvar -> t -> subst -> subst
+  (** [try_bind tv ty sbt] tries to bind [tv] with [ty]. The function
+      succeeds if [tv] is not in the domain of [sbt] or the current
+      value of [tv] in [sbt] is equal to [ty].
+
+      If the current value of [tv] is not compatible with [ty], raises
+      the exception {!exception TypeClash}.
 
-  val bind : tvar -> t -> subst -> subst
+      If the previous value of [tv] in [sbt] is equal to [ty] for [equal],
+      the returned substitution is physically equal to [sbt]. *)
 
-  val is_in_dom : tvar -> subst -> bool
+  val in_domain : tvar -> subst -> bool
+  (** [in_domain tv sbt] checks if [tv] is in the domain of [sbt]. *)
 
   val restrict : TvSet.t -> subst -> subst
-  (** [restrict set sbt] restrict the domain of the substitution [sbt] to be a
-      subset of [set]. *)
+  (** [restrict set sbt] returns a substitution that is equal to [sbt] on
+      the set [set] and the identity otherwise. *)
 
   val compare : subst -> subst -> int
   (** Comparison of substitutions. *)
@@ -211,8 +236,6 @@ module Subst : sig
 end
 
 type subst = Subst.subst
-(** The type of substitution, i.e. maps
-    from type variables identifiers to types.*)
 
 val apply_subst : subst -> t -> t
 (** Substitution application. *)