ReML type bindings

src/Common/DEC_GRAMMAR.sml

@@ -74,7 +74,7 @@ sig
   and FClause = FCLAUSE of info * atpat list * ty option * exp * FClause option
 
   and typbind =
-        TYPBIND of info * tyvar list * tycon * ty * typbind option
+        TYPBIND of info * tyvar list * (info * regvar list) * tycon * ty * typbind option
 
   and datbind =
         DATBIND of info * tyvar list * tycon * conbind * datbind option
@@ -107,7 +107,7 @@ sig
   and ty =
         TYVARty of info * tyvar |
         RECORDty of info * tyrow option * (info*regvar) option |
-        CONty of info * ty list * longtycon |
+        CONty of info * ty list * (info*regvar) list * longtycon |
         FNty of info * ty * (info*regvar) option * ty |
         PARty of info * ty * (info*(info*regvar)list) option |
         WITHty of info * ty * constraint                               (* ReML *)
@@ -175,7 +175,9 @@ sig
 
 
   val getExplicitTyVarsTy      : ty -> tyvar list
-  and getExplicitTyVarsConbind : conbind -> tyvar list
+  val getExplicitTyVarsConbind : conbind -> tyvar list
+
+  val getRegVarsTy             : ty -> regvar list                        (* ReML *)
 
   (*expansive harmless_con exp = true iff exp is expansive.
    harmless_con longid = true iff longid is an excon or a con different

src/Common/DecGrammar.sml

@@ -83,7 +83,7 @@ struct
   and FClause = FCLAUSE of info * atpat list * ty option * exp * FClause option
 
   and typbind =
-        TYPBIND of info * tyvar list * tycon * ty * typbind option
+        TYPBIND of info * tyvar list * (info * regvar list) * tycon * ty * typbind option
 
   and datbind =
         DATBIND of info * tyvar list * tycon * conbind * datbind option
@@ -116,7 +116,7 @@ struct
   and ty =
         TYVARty of info * tyvar |
         RECORDty of info * tyrow option * (info*regvar) option |
-        CONty of info * ty list * longtycon |
+        CONty of info * ty list * (info*regvar) list * longtycon |
         FNty of info * ty * (info*regvar) option * ty |
         PARty of info * ty * (info*(info*regvar)list) option |
         WITHty of info * ty * constraint
@@ -251,7 +251,7 @@ struct
         | PUTateff x => #1 x
         | GETateff x => #1 x
 
-  fun get_info_typbind (TYPBIND (info, tyvars, tycon, ty, typbind_opt)) = info
+  fun get_info_typbind (TYPBIND (info, tyvars, regvars, tycon, ty, typbind_opt)) = info
 
   fun get_info_tyrow (TYROW (info, lab, ty, tyrow_opt)) = info
 
@@ -362,8 +362,8 @@ struct
       | RECvalbind(i, valbind) =>
           RECvalbind(f i, map_valbind_info f valbind)
 
-    and map_typbind_info f (TYPBIND(i,tyvars,tycon,ty,typbind_opt)): typbind =
-      TYPBIND(f i,tyvars,tycon,map_ty_info f ty,
+    and map_typbind_info f (TYPBIND(i,tyvars,(ir,regvars),tycon,ty,typbind_opt)): typbind =
+      TYPBIND(f i,tyvars,(f ir,regvars),tycon,map_ty_info f ty,
               do_opt typbind_opt (map_typbind_info f))
 
     and map_datbind_info f (DATBIND(i,tyvars,tycon,conbind,datbind_opt)): datbind =
@@ -418,7 +418,7 @@ struct
       case ty of
         TYVARty(i,tyvar) => TYVARty(f i, tyvar)
       | RECORDty(i,tyrow_opt,opt) => RECORDty(f i, do_opt tyrow_opt (map_tyrow_info f),Option.map (fn (i,rv) => (f i,rv)) opt)
-      | CONty(i,tys,longtycon) => CONty(f i, map (map_ty_info f) tys,longtycon)
+      | CONty(i,tys,regvars,longtycon) => CONty(f i, map (map_ty_info f) tys, map (fn (i,r) => (f i,r)) regvars, longtycon)
       | FNty(i,ty,opt,ty') => FNty(f i, map_ty_info f ty, Option.map (fn (i,rv) => (f i,rv)) opt, map_ty_info f ty')
       | PARty(i,ty,opt) => PARty(f i, map_ty_info f ty, Option.map (fn (i,rvis) => (f i,List.map (fn (i,rv) => (f i,rv)) rvis)) opt)
       | WITHty (i,t,c) => WITHty (f i, map_ty_info f t, map_constraint_info f c)
@@ -487,7 +487,7 @@ struct
         TYVARty(_, tv) => tv::res
       | RECORDty(_, NONE, _) => res
       | RECORDty(_, SOME tyrow, _) => fTyrow tyrow res
-      | CONty(_, tys, _) => foldl (fn (ty,res) => fTy ty res) res tys
+      | CONty(_, tys, _, _) => foldl (fn (ty,res) => fTy ty res) res tys
       | FNty(_, ty1, _, ty2) => fTy ty1 (fTy ty2 res)
       | PARty(_, ty, _) => fTy ty res
       | WITHty(_, ty, _) => fTy ty res
@@ -505,12 +505,53 @@ struct
           NONE => res'
         | SOME conbind => fConbind conbind res'
       end
-
   in
-    fun getExplicitTyVarsTy ty =  fTy ty []
+    fun getExplicitTyVarsTy ty = fTy ty []
     fun getExplicitTyVarsConbind ty = fConbind ty []
   end
 
+  local
+    fun ins r xs = if List.exists (fn x => RegVar.eq(x,r)) xs then xs
+                   else r::xs
+    fun inss nil xs = xs
+      | inss (r::rs) xs = ins r (inss rs xs)
+    fun fInfoRegVar x acc =
+        case x of
+            NONE => acc
+          | SOME (_,r) => ins r acc
+    fun fTy ty acc =
+      case ty of
+        TYVARty _ => acc
+      | RECORDty(_, NONE, iro) => fInfoRegVar iro acc
+      | RECORDty(_, SOME tyrow, iro) => fTyrow tyrow (fInfoRegVar iro acc)
+      | CONty(_, tys, irs, _) => foldl (fn (ty,acc) => fTy ty acc) (inss (map #2 irs) acc) tys
+      | FNty(_, ty1, iro, ty2) => fTy ty1 (fInfoRegVar iro (fTy ty2 acc))
+      | PARty(_, ty, NONE) => fTy ty acc
+      | PARty(_, ty, SOME (_,irs)) => fTy ty (inss (map #2 irs) acc)
+      | WITHty(_, ty, c) => fTy ty (fConstraint c acc)
+    and fConstraint c acc =
+        case c of
+            DISJOINTconstraint (_,e1,e2,_) => fEff e1 (fEff e2 acc)
+          | INCLconstraint (_,(_,r),e) => fEff e (ins r acc)
+          | PROPconstraint (_,_,e) => fEff e acc
+    and fEff e acc =
+        case e of
+            SETeff (_, aes) => fAtEffs aes acc
+          | VAReff (_,r) => ins r acc
+    and fAtEffs nil acc = acc
+      | fAtEffs (ae::aes) acc =
+        case ae of
+            VARateff (_,r) => ins r (fAtEffs aes acc)
+          | PUTateff (_,(_,r)) => ins r (fAtEffs aes acc)
+          | GETateff (_,(_,r)) => ins r (fAtEffs aes acc)
+    and fTyrow (TYROW(_, _, ty, tyrowopt)) acc =
+        case tyrowopt of
+            NONE => fTy ty acc
+          | SOME tyrow => fTyrow tyrow (fTy ty acc)
+  in
+    fun getRegVarsTy ty = fTy ty []
+  end
+
   (* finding the string name of a topmost value identifier in a pattern, if any exists: *)
 
   fun find_topmost_id_in_pat (ATPATpat(_, atpat)): string option = find_topmost_id_in_atpat atpat
@@ -850,22 +891,36 @@ struct
                               }
                       )
 
+    and layoutRegvarseq regvars =
+      case regvars
+        of nil => NONE
+         | [rv] => SOME(LEAF("`" ^ RegVar.pr rv))
+         | rvs => SOME(NODE{start="`[", finish="]", indent=1,
+                            children=map (LEAF o RegVar.pr) rvs,
+                            childsep=RIGHT " "
+                           }
+                      )
+
     and layoutTypbind typbind : StringTree =
       let
-        fun treesOfTypbind(TYPBIND(_, tyvars, tycon, ty, typbind_opt))
-          : StringTree list =
+        fun treesOfTypbind (TYPBIND(_, tyvars, (_,regvars), tycon, ty, typbind_opt))
+            : StringTree list =
           let
             val tyvars_opt = layoutTyvarseq tyvars
+            val regvars_opt = layoutRegvarseq regvars
             val tyconT = LEAF(TyCon.pr_TyCon tycon)
-            val eqT = LEAF " = "
+            val eqT = LEAF "="
             val tyT = layoutTy ty
 
             val this =
               NODE{start="", finish="", indent=0,
                       children=(case tyvars_opt of SOME x => [x]
                                                  | NONE => nil
-                               ) @  [tyconT, eqT, tyT],
-                      childsep=NOSEP
+                               ) @
+                               (case regvars_opt of SOME x => [x]
+                                                  | NONE => nil
+                               ) @ [tyconT, eqT, tyT],
+                      childsep=RIGHT " "
                      }
           in
             this :: (case typbind_opt
@@ -1128,23 +1183,28 @@ struct
                  | NONE => LEAF "{}" (* "unit" ? *)
            end
 
-         | CONty(_, tys, longtycon) =>
+         | CONty(_, tys, regvars, longtycon) =>
              let
-               fun idTail t =
-                 NODE{start="", finish=" " ^ TyCon.pr_LongTyCon longtycon,
-                         indent=0, children=[t], childsep=NOSEP
-                         }
-             in
-               case tys
-                 of nil => LEAF(TyCon.pr_LongTyCon longtycon)
-
-                  | [ty] => idTail(layoutTy ty)
-
-                  | tys => idTail(NODE{start="(", finish=")", indent=1,
-                                          children=map layoutTy tys,
-                                          childsep=RIGHT ", "
-                                         }
-                                 )
+               fun idTail ts =
+                   NODE{start="", finish=" " ^ TyCon.pr_LongTyCon longtycon,
+                        indent=0, children=ts, childsep=RIGHT " "
+                       }
+               fun layRegvars () = NODE{start="`[", finish="]", indent=2,
+                                        children=map (fn (_,r) => LEAF(RegVar.pr r)) regvars,
+                                        childsep=RIGHT " "}
+               fun layTys () = NODE{start="(", finish=")", indent=1,
+                                    children=map layoutTy tys,
+                                    childsep=RIGHT ", "}
+             in case tys of
+                    nil => (case regvars of
+                                nil => LEAF(TyCon.pr_LongTyCon longtycon)
+                              | _ => idTail [layRegvars()])
+                  | [ty] => (case regvars of
+                                 nil => idTail [layoutTy ty]
+                               | _ => idTail [layoutTy ty, layRegvars()])
+                  | tys => (case regvars of
+                                nil => idTail [layTys()]
+                              | _ => idTail [layTys(), layRegvars()])
              end
 
          | FNty(_, ty1, opt, ty2) =>

src/Common/ERROR_INFO.sml

@@ -1,6 +1,6 @@
 
 signature ERROR_INFO =         (* ErrorInfo is part of the ElabInfo.  See ELAB_INFO for an
-				* overview of the different kinds of info.*)
+                                * overview of the different kinds of info.*)
   sig
     type TyName
     type TyVar
@@ -19,19 +19,19 @@ signature ERROR_INFO =         (* ErrorInfo is part of the ElabInfo.  See ELAB_I
     type regvar
 
     datatype RepeatedId = ID_RID of id      (* Repeated identifier, syntax *)
-			| LAB_RID of lab    (* errors *)
-			| TYCON_RID of tycon
-			| EXCON_RID of id
-			| CON_RID of id
-			| TYVAR_RID of TyVar
-			| STRID_RID of strid
-			| SIGID_RID of sigid
-			| FUNID_RID of funid
+                        | LAB_RID of lab    (* errors *)
+                        | TYCON_RID of tycon
+                        | EXCON_RID of id
+                        | CON_RID of id
+                        | TYVAR_RID of TyVar
+                        | STRID_RID of strid
+                        | SIGID_RID of sigid
+                        | FUNID_RID of funid
                         | REGVAR_RID of regvar
 
     datatype ErrorInfo =
      (* Core errors: *)
-	UNIFICATION of Type * Type
+        UNIFICATION of Type * Type
       | UNIFICATION_TEXT of string * Type * string * Type
       | UNIFICATION_RANK of Type * Type * TyVar * TyName
       | LOOKUP_LONGID of longid
@@ -84,10 +84,14 @@ signature ERROR_INFO =         (* ErrorInfo is part of the ElabInfo.  See ELAB_I
       | REGVARS_SCOPED_TWICE of regvar list
       | REGVAR_TY_UNBOXED
       | REGVAR_TY_ANNOTATE of string
+      | REGVARS_NOT_IN_REGVARSEQ of regvar list
+      | REGVARS_INVALID_ORDER of regvar list
+      | REGVARS_WRONG_ARITY_R of {expected: int, actual: int}
+      | REGVARS_WRONG_ARITY_E of {expected: int, actual: int}
 
     type Report
     val report : ErrorInfo -> Report
 
     structure ErrorCode : ERROR_CODE      (* Support for error testing and handling. *)
       sharing type ErrorCode.ErrorInfo = ErrorInfo
-  end;
+  end

src/Common/EfficientElab/ElabTopdec.sml

@@ -582,7 +582,7 @@ structure ElabTopdec: ELABTOPDEC  =
                                 else if TyName.arity t <> List.length alphas then
                                   fail (ErrorInfo.WHERE_TYPE_ARITY (alphas, (longtycon, t)), out_ty)
                                 else
-                                  let val theta' = TypeFcn.from_TyVars_and_Type (alphas, tau)
+                                  let val theta' = TypeFcn.from_TyVars_and_Type (alphas, nil, tau)    (* MEMO ReML *)
                                       val phi = Realisation.singleton (t, theta')
                                       val phi_E = Realisation.on_Env phi E
                                   in
@@ -907,7 +907,7 @@ structure ElabTopdec: ELABTOPDEC  =
              val tyvars = map TyVar.from_ExplicitTyVar explicittyvars
              val tyvars_repeated = repeaters (op =) explicittyvars
              val arity = List.length explicittyvars
-             val t = TyName.freshTyName {tycon=tycon, arity=arity, equality=equality}
+             val t = TyName.freshTyName {tycon=tycon, arity=arity, arity_reml=(0,0), equality=equality}  (* ReML MEMO *)
              val theta = TypeFcn.from_TyName t
              val tystr = TyStr.from_theta_and_VE (theta, VE.empty)
              val (error, ids) = add_ids_tycon(ids,tycon)

src/Common/EfficientElab/Environments.sml

@@ -92,7 +92,7 @@ structure Environments: ENVIRONMENTS =
             EqSet.empty
         | RECORDty(_, SOME tyrow, _) =>
             ExplicitTyVarsTyRow tyrow
-        | CONty(_, tylist, _) =>
+        | CONty(_, tylist, _, _) =>
             foldl (uncurry EqSet.union) EqSet.empty (map ExplicitTyVarsTy tylist)
         | FNty(_,ty1,_,ty2) =>
             EqSet.union (ExplicitTyVarsTy ty1)
@@ -199,7 +199,7 @@ structure Environments: ENVIRONMENTS =
           [tyvar]
         | unguarded_ty(DecGrammar.RECORDty(_,tyrow_opt,_)) =
           unguarded_opt unguarded_tyrow tyrow_opt
-        | unguarded_ty(DecGrammar.CONty(_,ty_list,_)) =
+        | unguarded_ty(DecGrammar.CONty(_,ty_list,_,_)) =
           foldl (fn (ty, tyvarset) => unguarded_ty ty ++ tyvarset)
           [] ty_list
         | unguarded_ty(DecGrammar.FNty(_,ty1,_,ty2)) =
@@ -755,14 +755,16 @@ structure Environments: ENVIRONMENTS =
                  (tyname, TypeFcn.from_TyName
                            (TyName.freshTyName
                              {tycon = TyName.tycon tyname,
-                              arity = TyName.arity tyname, equality = true})))
+                              arity = TyName.arity tyname,
+                              arity_reml = TyName.arity_reml tyname,
+                              equality = true})))
       in
         fun equality_maximising_realisation (TE : TyEnv) : realisation =
               generate (iterate (tynames_of_nonequality_datatypes TE) TE)
       end (*local*)
 
       fun init' explicittyvars tycon =
-        let val tyname = TyName.freshTyName {tycon=tycon, arity=List.length explicittyvars, equality=false}
+        let val tyname = TyName.freshTyName {tycon=tycon, arity=List.length explicittyvars, arity_reml=(0,0), equality=false}
             val TE = singleton (tycon, TyStr.from_theta_and_VE (TypeFcn.from_TyName tyname, VE.empty))
         in (tyname, TE)
         end
@@ -1271,7 +1273,7 @@ structure Environments: ENVIRONMENTS =
                                   mk_tystr (TyName.tyName_REF, VE.close refVE_to_TE))
 
         local   (* initial TE for unit *)
-          val theta_unit = TypeFcn.from_TyVars_and_Type ([], Type.Unit)
+          val theta_unit = TypeFcn.from_TyVars_and_Type ([], nil, Type.Unit)
           val VE_unit = VE.empty
         in
           val TE_unit = TE.singleton (TyCon.tycon_UNIT,
@@ -1679,6 +1681,7 @@ structure Environments: ENVIRONMENTS =
         let val tyname = noSome (TypeFcn.to_TyName theta) "modifyTyStr"
             val tyname_abs = TyName.freshTyName {tycon=TyName.tycon tyname,
                                                  arity=TyName.arity tyname,
+                                                 arity_reml=TyName.arity_reml tyname,
                                                  equality=false}
             val phi = singleton(tyname_abs, TypeFcn.from_TyName tyname)
             val phi_inv = singleton(tyname, TypeFcn.from_TyName tyname_abs)