From 9972db22ecd8c9b1dde8e908e889d8ca71c0d99f Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:16:17 +0100 Subject: [PATCH 01/18] progress --- src/Common/ELABDEC.sig | 4 +- src/Common/ELABTOPDEC.sml | 6 +- src/Common/ENVIRONMENTS.sml | 2 +- .../EfficientElab/MODULE_STATOBJECT.sml | 8 +- src/Common/EfficientElab/StatObject.sml | 4 +- src/Common/STATOBJECT.sml | 2 +- src/Compiler/Lambda/COMPILER_ENV.sml | 2 +- src/Compiler/Lambda/CompileDec.sml | 21 +++- src/Compiler/Lambda/CompilerEnv.sml | 71 ++++++----- src/Compiler/Lambda/EliminateEq.sml | 1 + src/Compiler/Lambda/LAMBDA_EXP.sml | 29 +++-- src/Compiler/Lambda/LambdaBasics.sml | 26 ++++- src/Compiler/Lambda/LambdaExp.sml | 73 +++++++++--- src/Compiler/Lambda/LambdaStatSem.sml | 25 +++- src/Compiler/Lambda/OptLambda.sml | 29 +++-- src/Compiler/Regions/RTYPE.sig | 2 +- src/Compiler/Regions/RType.sml | 3 +- src/Compiler/Regions/SpreadExpression.sml | 106 +++++++++++++++-- src/Manager/IntModules.sml | 4 +- src/Tools/Tester/Tester.sml | 1 + test/explicit_regions/Makefile | 4 +- test/explicit_regions/all.tst | 110 +++++++++--------- test/explicit_regions/mod.sml | 12 ++ test/explicit_regions/mod.sml.log.ok | 26 +++++ test/explicit_regions/mod2.sml | 12 ++ test/explicit_regions/mod2.sml.log.ok | 26 +++++ test/explicit_regions/mod3.sml | 12 ++ test/explicit_regions/mod3.sml.log.ok | 26 +++++ 28 files changed, 487 insertions(+), 160 deletions(-) create mode 100644 test/explicit_regions/mod.sml create mode 100644 test/explicit_regions/mod.sml.log.ok create mode 100644 test/explicit_regions/mod2.sml create mode 100644 test/explicit_regions/mod2.sml.log.ok create mode 100644 test/explicit_regions/mod3.sml create mode 100644 test/explicit_regions/mod3.sml.log.ok diff --git a/src/Common/ELABDEC.sig b/src/Common/ELABDEC.sig index 2b05fe3bd..7124162aa 100644 --- a/src/Common/ELABDEC.sig +++ b/src/Common/ELABDEC.sig @@ -8,11 +8,11 @@ sig type PreElabTy and PostElabTy val elab_dec : Context * PreElabDec -> TyName list * Env * PostElabDec - and elab_ty : Context * PreElabTy -> Type option * PostElabTy + val elab_ty : Context * PreElabTy -> Type option * PostElabTy (* elab_ty returns `NONE' if an error occurred when elborating the * type expression. The reason we do things this way is that * errors are dealt with in two different ways depending on the * construct the type expression is part of. *) -end; +end diff --git a/src/Common/ELABTOPDEC.sml b/src/Common/ELABTOPDEC.sml index cb25e2b55..81e445113 100644 --- a/src/Common/ELABTOPDEC.sml +++ b/src/Common/ELABTOPDEC.sml @@ -8,9 +8,9 @@ signature ELABTOPDEC = type absprjid (* absolute project identifier *) - val elab_topdec: absprjid * StaticBasis * PreElabTopdec - -> StaticBasis * PostElabTopdec + val elab_topdec : absprjid * StaticBasis * PreElabTopdec + -> StaticBasis * PostElabTopdec type StringTree val layoutStaticBasis: StaticBasis -> StringTree - end; + end diff --git a/src/Common/ENVIRONMENTS.sml b/src/Common/ENVIRONMENTS.sml index 58ec16c80..3740df708 100644 --- a/src/Common/ENVIRONMENTS.sml +++ b/src/Common/ENVIRONMENTS.sml @@ -339,4 +339,4 @@ signature ENVIRONMENTS = val create_restrictor : {longstrids: longstrid list, longtycons: longtycon list, longvids: longid list} -> restrictor - end; + end diff --git a/src/Common/EfficientElab/MODULE_STATOBJECT.sml b/src/Common/EfficientElab/MODULE_STATOBJECT.sml index 896b19478..e87673ed1 100644 --- a/src/Common/EfficientElab/MODULE_STATOBJECT.sml +++ b/src/Common/EfficientElab/MODULE_STATOBJECT.sml @@ -33,7 +33,7 @@ signature MODULE_STATOBJECT = | MISSINGEXC of strid list * id | S_RIGIDTYCLASH of longtycon | S_CONFLICTING_DOMCE of longtycon - | NOTYENRICHMENT of {qualid: strid list * id, + | NOTYENRICHMENT of {qualid: strid list * id, str_sigma : TypeScheme, str_vce: string, sig_sigma : TypeScheme, sig_vce: string} | EXCNOTEQUAL of strid list * id * (Type * Type) @@ -80,7 +80,7 @@ signature MODULE_STATOBJECT = (*functor signature*) - structure Phi : + structure Phi : sig val from_T_and_E_and_Sigma : TyName.Set.Set * Env * Sig -> FunSig val to_T_and_E_and_Sigma : FunSig -> TyName.Set.Set * Env * Sig @@ -90,7 +90,7 @@ signature MODULE_STATOBJECT = val layout : FunSig -> StringTree (*If Sigma'= match (Phi, E) succeeds, then E matches the - argument signature of the functor signature Phi and Sigma' is + argument signature of the functor signature Phi and Sigma' is the signature of the actual result of the functor application. match will raise No_match if there is no match:*) @@ -103,4 +103,4 @@ signature MODULE_STATOBJECT = val pu : FunSig Pickle.pu end - end; + end diff --git a/src/Common/EfficientElab/StatObject.sml b/src/Common/EfficientElab/StatObject.sml index 01b8f9930..d63d091e5 100644 --- a/src/Common/EfficientElab/StatObject.sml +++ b/src/Common/EfficientElab/StatObject.sml @@ -1368,7 +1368,7 @@ structure StatObject: STATOBJECT = | (rvopt,NONE) => rvopt | (SOME rv, SOME rv') => if RegVar.eq(#2 rv,#2 rv') then SOME rv - else raise Unify "diffent explicit region variables") (rvi,rvi') + else raise Unify "different explicit region variables") (rvi,rvi') else () fun unifyRegVars (rvis,rvis') = @@ -1378,7 +1378,7 @@ structure StatObject: STATOBJECT = | (SOME (i,rvs), SOME (_,rvs')) => if ListPair.allEq (fn (rv,rv') => RegVar.eq(#2 rv,#2 rv')) (rvs,rvs') then SOME (i,rvs) - else raise Unify "diffent lists of explicit region variables") + else raise Unify "different lists of explicit region variables") (rvis,rvis') else () diff --git a/src/Common/STATOBJECT.sml b/src/Common/STATOBJECT.sml index 84a38f084..ec599644b 100644 --- a/src/Common/STATOBJECT.sml +++ b/src/Common/STATOBJECT.sml @@ -300,4 +300,4 @@ signature STATOBJECT = val tynamesRng : realisation -> TyName.Set.Set end (*Realisation*) - end; + end diff --git a/src/Compiler/Lambda/COMPILER_ENV.sml b/src/Compiler/Lambda/COMPILER_ENV.sml index 0a7efd27f..6423c149c 100644 --- a/src/Compiler/Lambda/COMPILER_ENV.sml +++ b/src/Compiler/Lambda/COMPILER_ENV.sml @@ -95,7 +95,7 @@ signature COMPILER_ENV = * list contains the tynames of the * associated tystr. *) type ElabEnv and TypeScheme - val constrain : CEnv * ElabEnv -> CEnv + val constrain : CEnv * ElabEnv -> CEnv * (lvar * tyvar list * Type) list (* compileTypeScheme is used by constrain *) val set_compileTypeScheme : (TypeScheme -> tyvar list * Type) -> unit (* MEGA HACK *) diff --git a/src/Compiler/Lambda/CompileDec.sml b/src/Compiler/Lambda/CompileDec.sml index 34eaa2857..6b12eb708 100644 --- a/src/Compiler/Lambda/CompileDec.sml +++ b/src/Compiler/Lambda/CompileDec.sml @@ -3543,8 +3543,21 @@ the 12 lines above are very similar to the code below val E = case to_TypeInfo info of SOME (ElabInfo.TypeInfo.TRANS_CONSTRAINT_INFO E) => E | _ => die "comp_strexp.TRANSPARENT_CONSTRAINTstrexp.no env info" - val ce2 = CE.constrain(ce1,E) - in (ce2, f) + (* + val () = pr "** Transparent constraint; E =\n" + val () = pr_st(Environments.E.layout E) + *) + val (ce2,checks) = CE.constrain(ce1,E) + val rep = loc_report_of_ElabInfo info + fun g cs e = + case cs of + nil => e + | (lv,tvs,t)::cs => g cs (LET{pat=nil, + bind=CHECK_REML {lvar=lv, + tyvars=tvs, + Type=t,rep=rep}, + scope=e}) + in (ce2, f o (g checks)) end | OPAQUE_CONSTRAINTstrexp(info, strexp, _) => die "OPAQUE_CONSTRAINTstrexp.not impl" | APPstrexp(i,funid,strexp) => @@ -3562,14 +3575,14 @@ the 12 lines above are very similar to the code below val (strid,E,strexp0,ce0,ife0) = lookupInlineFunApp fe' funid handle X => (print "**looking up funid failed**\n"; raise X) val E' = Environments.Realisation.on_Env phi E - val ce2 = CE.constrain(ce1,E') + val (ce2,_) = CE.constrain(ce1,E') val strexp0' = TopdecGrammar.map_strexp_info (on_ElabInfo phi) strexp0 val (ce3, f2) = comp_strexp((ife0,lookupInlineFunApp), CE.plus(ce0, CE.declare_strid(strid,ce2,CE.emptyCEnv)), strexp0') - val ce4 = CE.constrain(ce3,Eres) + val (ce4,_) = CE.constrain(ce3,Eres) val _ = chat ("[compiling functor application end.]") in (ce4, f1 o f2) end diff --git a/src/Compiler/Lambda/CompilerEnv.sml b/src/Compiler/Lambda/CompilerEnv.sml index 718e3f26a..a8fcb9f4e 100644 --- a/src/Compiler/Lambda/CompilerEnv.sml +++ b/src/Compiler/Lambda/CompilerEnv.sml @@ -533,7 +533,14 @@ structure CompilerEnv: COMPILER_ENV = pr_st (layout_scheme(tvs',tau')); raise X) val il' = map (LambdaBasics.on_Type S) il - in LVAR(lv,tvs',tau',il') + (* + val () = print ("TypeScheme(" ^ Lvars.pr_lvar lv ^ "):\n") + val () = pr_st(layout_scheme(tvs',tau')) + *) + val checks = if LambdaExp.contains_regvars tau' + then [(lv,tvs',tau')] + else nil + in (LVAR(lv,tvs',tau',il'), checks) end | _ => die "constr_ran.LVAR.longvar expected") | CON(con,tvs,tau,il) => @@ -545,7 +552,7 @@ structure CompilerEnv: COMPILER_ENV = handle X => (print ("\nMatch failed for var matching con " ^ Con.pr_con con ^ "\n"); raise X) val il' = map (LambdaBasics.on_Type S) il - in CON(con,tvs',tau',il') + in (CON(con,tvs',tau',il'),nil) end | VE.LONGCON sigma => let val (tvs',tau') = compileTypeScheme sigma @@ -554,7 +561,7 @@ structure CompilerEnv: COMPILER_ENV = handle X => (print ("\nMatch failed for con matching con " ^ Con.pr_con con ^ "\n"); raise X) val il' = map (LambdaBasics.on_Type S) il - in if LambdaBasics.eq_sigma((tvs,tau),(tvs',tau')) then CON(con,tvs',tau',il') + in if LambdaBasics.eq_sigma((tvs,tau),(tvs',tau')) then (CON(con,tvs',tau',il'), nil) else (print "\nconstr_ran.CON.type schemes should be equal.\n"; print "Elaboration environment:\n\n"; pr_st (Environments.E.layout elabE); @@ -572,49 +579,55 @@ structure CompilerEnv: COMPILER_ENV = of VE.LONGVAR sigma => let val (tvs',tau') = compileTypeScheme sigma handle ? => (print ("constr_ran.EXCON: excon = " ^ Excon.pr_excon excon ^ "\n"); raise ?) - in if tvs' = [] andalso LambdaBasics.eq_Type(tau,tau') then EXCON(excon,tau) + in if tvs' = [] andalso LambdaBasics.eq_Type(tau,tau') then (EXCON(excon,tau),nil) else die "constr_ran.EXCON.LONGVAR" end - | VE.LONGEXCON _ => EXCON(excon,tau) (* we could check equality of types *) + | VE.LONGEXCON _ => (EXCON(excon,tau),nil) (* we could check equality of types *) | _ => die "constr_ran.EXCON.longvar or longexcon expected") | _ => die "constr_ran.expecting LVAR, CON or EXCON" - fun constr_ce(CENV{StrEnv, VarEnv, TyEnv, PathEnv}, elabE) = - let val (elabSE, elabTE, elabVE, elabR) = E.un elabE - in CENV{StrEnv=constr_se(StrEnv,elabSE), VarEnv=constr_ve(VarEnv,elabVE), - TyEnv=constr_te(TyEnv,elabTE), - PathEnv=emptyPathEnv} - end - - and constr_se(STRENV se, elabSE) = - STRENV(SE.Fold (fn (strid, elabE) => fn se' => - case StrId.Map.lookup se strid - of SOME ce => let val ce' = constr_ce(ce,elabE) - in StrId.Map.add(strid,ce',se') - end - | NONE => die "constr_se") StrId.Map.empty elabSE) - - and constr_ve(ve, elabVE) = - VE.Fold (fn (id, elabRan) => fn ve' => + fun constr_ce (CENV{StrEnv, VarEnv, TyEnv, PathEnv}, elabE) = + let val (elabSE, elabTE, elabVE, elabR) = E.un elabE + val (se,c1) = constr_se(StrEnv,elabSE) + val (ve,c2) = constr_ve(VarEnv,elabVE) + in (CENV{StrEnv=se, + VarEnv=ve, + TyEnv=constr_te(TyEnv,elabTE), + PathEnv=emptyPathEnv}, + c2@c1) + end + + and constr_se (STRENV se, elabSE) = + let val (se,c) = + SE.Fold (fn (strid, elabE) => fn (se',c0) => + case StrId.Map.lookup se strid of + SOME ce => let val (ce',c) = constr_ce(ce,elabE) + in (StrId.Map.add(strid,ce',se'), c@c0) + end + | NONE => die "constr_se") (StrId.Map.empty,nil) elabSE + in (STRENV se,c) + end + + and constr_ve (ve, elabVE) = + VE.Fold (fn (id, elabRan) => fn (ve',c0) => case Ident.Map.lookup ve id - of SOME transRan => let val transRan' = constr_ran(transRan, elabRan) - in Ident.Map.add(id,transRan', ve') + of SOME transRan => let val (transRan',c) = constr_ran(transRan, elabRan) + in (Ident.Map.add(id,transRan', ve'),c@c0) end - | NONE => die ("constr_ve: no " ^ Ident.pr_id id)) Ident.Map.empty elabVE + | NONE => die ("constr_ve: no " ^ Ident.pr_id id)) (Ident.Map.empty,nil) elabVE - and constr_te(TYENV te, elabTE) = + and constr_te (TYENV te, elabTE) = TYENV(TE.Fold(fn (tycon, _) => fn te' => case TyCon.Map.lookup te tycon of SOME tynames => TyCon.Map.add(tycon,tynames,te') | NONE => die "constr_te") TyCon.Map.empty elabTE) (* val _ = print "\n[Constraining ...\n" *) - val res = constr_ce(ce, elabE) + val (res,c) = constr_ce(ce, elabE) (* val _ = print " Done]\n" *) - in res + in (res,c) end - fun pp_tynames l = let fun pp [] = "" | pp [t] = TyName.pr_TyName t diff --git a/src/Compiler/Lambda/EliminateEq.sml b/src/Compiler/Lambda/EliminateEq.sml index 291b8aab3..a2dab9a5d 100644 --- a/src/Compiler/Lambda/EliminateEq.sml +++ b/src/Compiler/Lambda/EliminateEq.sml @@ -804,6 +804,7 @@ structure EliminateEq : ELIMINATE_EQ = in FRAME {declared_lvars = declared_lvars @ new_declared_lvars, declared_excons = declared_excons} end + | CHECK_REML _ => e end in f lexp diff --git a/src/Compiler/Lambda/LAMBDA_EXP.sml b/src/Compiler/Lambda/LAMBDA_EXP.sml index e99e65717..96311dc67 100644 --- a/src/Compiler/Lambda/LAMBDA_EXP.sml +++ b/src/Compiler/Lambda/LAMBDA_EXP.sml @@ -82,6 +82,9 @@ signature LAMBDA_EXP = val stringType : Type val chararrayType : Type + val contains_regvars : Type -> bool + val regvarsType : Type -> regvar list + datatype TypeList = (* To allow the result of a declaration *) Types of Type list (* to be a raised Bind exception. *) | Frame of {declared_lvars: {lvar : lvar, tyvars: tyvar list, Type: Type} list, @@ -121,25 +124,25 @@ signature LAMBDA_EXP = (* list of mutual recursive datatype declarations *) and LambdaExp = - VAR of {lvar: lvar, instances : Type list, regvars: regvar list} + VAR of {lvar: lvar, instances: Type list, regvars: regvar list} | INTEGER of IntInf.int * Type | WORD of IntInf.int * Type | STRING of string * regvar option | REAL of string * regvar option | F64 of string - | FN of {pat : (lvar * Type) list, body : LambdaExp} - | LET of {pat : (lvar * tyvar list * Type) list, - bind : LambdaExp, + | FN of {pat: (lvar * Type) list, body: LambdaExp} + | LET of {pat: (lvar * tyvar list * Type) list, + bind: LambdaExp, scope: LambdaExp} | LETREGION of {regvars: regvar list, scope: LambdaExp} - | FIX of {functions : {lvar : lvar, - regvars: regvar list, - tyvars : tyvar list, - Type : Type, - constrs: constr list, - bind : LambdaExp} list, - scope : LambdaExp} + | FIX of {functions: {lvar: lvar, + regvars: regvar list, + tyvars : tyvar list, + Type: Type, + constrs: constr list, + bind: LambdaExp} list, + scope: LambdaExp} | APP of LambdaExp * LambdaExp * bool option (* tail call? *) | EXCEPTION of excon * Type option * LambdaExp | RAISE of LambdaExp * TypeList @@ -151,11 +154,13 @@ signature LAMBDA_EXP = | SWITCH_E of (excon*lvar option) Switch | TYPED of LambdaExp * Type * constr list | PRIM of Type prim * LambdaExp list - | FRAME of {declared_lvars: {lvar : lvar, tyvars: tyvar list, Type: Type} list, + | FRAME of {declared_lvars: {lvar: lvar, tyvars: tyvar list, Type: Type} list, declared_excons: (excon * Type option) list} (* a frame is the result of a structure-level * declaration. *) + | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, rep: Report} + (* REML: Check that lvar has the type scheme specified... *) and 'a Switch = SWITCH of LambdaExp * ('a * LambdaExp) list * LambdaExp option diff --git a/src/Compiler/Lambda/LambdaBasics.sml b/src/Compiler/Lambda/LambdaBasics.sml index a1bfa192c..f4c16cbe1 100644 --- a/src/Compiler/Lambda/LambdaBasics.sml +++ b/src/Compiler/Lambda/LambdaBasics.sml @@ -64,6 +64,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(lamb,t,cs) => TYPED(passTD f lamb,t,cs) | PRIM(prim,lambs) => PRIM(prim,map (passTD f) lambs) | FRAME _ => lamb + | CHECK_REML _ => lamb end @@ -109,7 +110,8 @@ structure LambdaBasics: LAMBDA_BASICS = | SWITCH_E switch => SWITCH_E(passSwitch (passBU f) switch) | TYPED(lamb,t,cs) => TYPED(passBU f lamb,t,cs) | PRIM(prim,lambs) => PRIM(prim,map (passBU f) lambs) - | FRAME _ => lamb) + | FRAME _ => lamb + | CHECK_REML _ => lamb) end @@ -148,6 +150,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(lamb,t,_) => foldTD f new_acc lamb | PRIM(prim,lambs) => foldl' (foldTD f) new_acc lambs | FRAME _ => new_acc + | CHECK_REML _ => new_acc end @@ -195,6 +198,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,t,cs) => TYPED(f e,t,cs) | PRIM(prim, lambs) => PRIM(prim, map f lambs) | FRAME _ => lamb + | CHECK_REML _ => lamb (* ----------------------------------------------------------------- @@ -233,6 +237,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,t,_) => f e | PRIM(prim, lambs) => app f lambs | FRAME _ => () + | CHECK_REML _ => () (* ----------------------------------------------------------------- * app_lamb_tail f t lamb - apply f to sub-expressions and propagate @@ -272,6 +277,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,ty,_) => f t e | PRIM(prim, lambs) => app (f NOTAIL) lambs | FRAME _ => () + | CHECK_REML _ => () (* ----------------------------------------------------------------- @@ -313,6 +319,7 @@ structure LambdaBasics: LAMBDA_BASICS = fun fv e : unit = case e of VAR {lvar,...} => insert_lv lvar + | CHECK_REML {lvar,...} => insert_lv lvar | APP(VAR{lvar,...},PRIM(UB_RECORDprim, es),_) => (insert_lv lvar; appi (fn (i, VAR {lvar=y,...}) => insert_lv_call_arg lvar i y @@ -496,8 +503,8 @@ structure LambdaBasics: LAMBDA_BASICS = in CCALLprim {name=name, instances=map (on_tau ren) instances, tyvars=map (on_tv ren_local) tyvars, Type=on_tau ren_local Type} (*the type scheme (tyvars, Type) is for a special purpose in the - region infere nce and back end; it must not be changed; we must rename bound - tyvars, however. *) + region inference and back end; it must not be changed; we must rename bound + tyvars, however. *) end | RESET_REGIONSprim {instance} => RESET_REGIONSprim {instance=on_tau ren instance} | FORCE_RESET_REGIONSprim {instance} => FORCE_RESET_REGIONSprim {instance=on_tau ren instance} @@ -543,6 +550,14 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,t,cs) => TYPED(on_e ren e, on_tau ren t,cs) | PRIM(prim,es) => PRIM(on_prim ren prim, map (on_e ren) es) | FRAME _ => lamb + | CHECK_REML {lvar,tyvars,Type,rep} => + let val tvs_pairs = map (fn tv => (tv, new_tv tv)) tyvars + val ren_local = add_tvs tvs_pairs empty_ren + in CHECK_REML {lvar=on_lv ren lvar, + tyvars=map (on_tv ren_local) tyvars, + Type=on_tau ren_local Type, + rep=rep} + end (* MEMO: frames; hopefully, we will NOT rename expressions containing frames... *) in @@ -726,6 +741,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(lamb,t,cs) => TYPED(f S lamb,on_Type S t,cs) | PRIM (prim,lambs) => PRIM(on_prim S prim,map (f S) lambs) | FRAME _ => lamb (*MEMO*) + | CHECK_REML _ => lamb (* type scheme closed! *) end in f S lamb @@ -859,7 +875,7 @@ structure LambdaBasics: LAMBDA_BASICS = (fn NONE => PP.LEAF "none" | SOME bl => PP.LEAF (pp_bl bl)) val pu = let open Pickle - in Lvars.Map.pu Lvars.pu (optionGen(listGen(bool))) + in Lvars.Map.pu Lvars.pu (optionGen(listGen bool)) end fun t (nil,nil) = nil @@ -931,6 +947,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,t,cs) => TYPED(N E e, t,cs) | PRIM(p,es) => PRIM(p, map (N E) es) | FRAME fr => FRAME(Nf E fr) + | CHECK_REML _ => e end and Ntl E tl = @@ -1010,6 +1027,7 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,tau,cs) => TYPED(t false e, tau,cs) | PRIM(p,es) => PRIM(p, map (t false) es) | FRAME fr => e + | CHECK_REML _ => e end in t false e end diff --git a/src/Compiler/Lambda/LambdaExp.sml b/src/Compiler/Lambda/LambdaExp.sml index 173dcbabb..76f9e18e0 100644 --- a/src/Compiler/Lambda/LambdaExp.sml +++ b/src/Compiler/Lambda/LambdaExp.sml @@ -103,6 +103,36 @@ structure LambdaExp : LAMBDA_EXP = fun isCharType (CONStype(_,tn,_)) = TyName.eq (tn, TyName.tyName_CHAR) | isCharType _ = false + fun contains_regvars t = + case t of + TYVARtype _ => false + | ARROWtype(ts1,ro1,ts2,ro2) => Option.isSome ro1 orelse Option.isSome ro2 orelse + contains_regvarss ts1 orelse contains_regvarss ts2 + | CONStype(ts,_,rso) => Option.isSome rso orelse contains_regvarss ts + | RECORDtype (ts,ro) => Option.isSome ro orelse contains_regvarss ts + and contains_regvarss (t::ts) = + contains_regvars t orelse contains_regvarss ts + | contains_regvarss nil = false + + fun regvarsType (t:Type) : regvar list = + let fun ins r a = if List.exists (fn r' => RegVar.eq(r,r')) a then a + else r::a + fun add NONE a = a + | add (SOME r) a = ins r a + fun adds nil a = a + | adds (r::rs) a = adds rs (ins r a) + fun rvst t a = + case t of + TYVARtype _ => a + | ARROWtype(ts1,ro1,ts2,ro2) => add ro1 (add ro2 (rvsts ts1 (rvsts ts2 a))) + | CONStype(ts,_,NONE) => rvsts ts a + | CONStype(ts,_,SOME rs) => adds rs (rvsts ts a) + | RECORDtype (ts,ro) => add ro (rvsts ts a) + and rvsts nil a = a + | rvsts (t::ts) a = rvsts ts (rvst t a) + in rvst t nil + end + datatype TypeList = (* To allow the result of a declaration *) Types of Type list (* to be a raised Bind exception. *) | Frame of {declared_lvars: {lvar : lvar, tyvars: tyvar list, Type: Type} list, @@ -142,25 +172,25 @@ structure LambdaExp : LAMBDA_EXP = (* list of mutual recursive datatype declarations *) and LambdaExp = - VAR of {lvar: lvar, instances : Type list, regvars: regvar list} + VAR of {lvar: lvar, instances: Type list, regvars: regvar list} | INTEGER of IntInf.int * Type | WORD of IntInf.int * Type | STRING of string * regvar option | REAL of string * regvar option | F64 of string - | FN of {pat : (lvar * Type) list, body : LambdaExp} - | LET of {pat : (lvar * tyvar list * Type) list, - bind : LambdaExp, + | FN of {pat: (lvar * Type) list, body: LambdaExp} + | LET of {pat: (lvar * tyvar list * Type) list, + bind: LambdaExp, scope: LambdaExp} | LETREGION of {regvars: regvar list, scope: LambdaExp} - | FIX of {functions : {lvar : lvar, - regvars: regvar list, - tyvars : tyvar list, - Type : Type, - constrs: constr list, - bind : LambdaExp} list, - scope : LambdaExp} + | FIX of {functions: {lvar: lvar, + regvars: regvar list, + tyvars: tyvar list, + Type: Type, + constrs: constr list, + bind: LambdaExp} list, + scope: LambdaExp} | APP of LambdaExp * LambdaExp * bool option (* tail call? *) | EXCEPTION of excon * Type option * LambdaExp | RAISE of LambdaExp * TypeList @@ -172,11 +202,13 @@ structure LambdaExp : LAMBDA_EXP = | SWITCH_E of (excon*lvar option) Switch | TYPED of LambdaExp * Type * constr list | PRIM of Type prim * LambdaExp list - | FRAME of {declared_lvars: {lvar : lvar, tyvars: tyvar list, Type: Type} list, + | FRAME of {declared_lvars: {lvar: lvar, tyvars: tyvar list, Type: Type} list, declared_excons: (excon * Type option) list} (* a frame is the result of a structure-level * declaration. *) + | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, rep: Report} + (* REML: Check that lvar has the type scheme specified... *) and 'a Switch = SWITCH of LambdaExp * ('a * LambdaExp) list * LambdaExp option @@ -223,6 +255,7 @@ structure LambdaExp : LAMBDA_EXP = | TYPED (lamb,tau,_) => foldTD fcns new_acc lamb | PRIM(prim,lambs) => foldl' (foldTD fcns) new_acc lambs | FRAME _ => acc + | CHECK_REML _ => acc end and foldPrim (g: 'a -> Type -> 'a) (acc:'a) (prim:Type prim) : 'a = @@ -379,6 +412,7 @@ structure LambdaExp : LAMBDA_EXP = | TYPED (lamb,_,_) => safe raiseOk lamb | PRIM(prim,lambs) => (safe_prim prim; app (safe raiseOk) lambs) | FRAME _ => () + | CHECK_REML _ => raise NotSafe fun safeLambdaExps0 raiseOk lambs = (app (safe raiseOk) lambs; true) @@ -1296,6 +1330,9 @@ structure LambdaExp : LAMBDA_EXP = indent=0,children=lvs@exs} end else layoutFrame "FRAME" fr + | CHECK_REML {lvar, tyvars, Type, rep= _} => + PP.NODE{start="CHECK_REML(",finish=")", indent=11, + childsep=PP.NOSEP,children=[layVarSigma(lvar,tyvars,Type)]} and maybepar context t = parenthesise (context > 13) t @@ -1689,6 +1726,7 @@ structure LambdaExp : LAMBDA_EXP = | toInt (FRAME _) = 19 | toInt (LETREGION _) = 20 | toInt (F64 _) = 21 + | toInt (CHECK_REML _) = 22 fun fun_VAR pu_LambdaExp = Pickle.con1 VAR (fn VAR a => a | _ => die "pu_LambdaExp.VAR") @@ -1774,7 +1812,12 @@ structure LambdaExp : LAMBDA_EXP = (Pickle.pairGen0(Pickle.listGen RegVar.pu,pu_LambdaExp)) fun fun_F64 pu_LambdaExp = Pickle.con1 F64 (fn F64 a => a | _ => die "pu_LambdaExp.F64") - Pickle.string + Pickle.string + fun fun_CHECK_REML _ = + Pickle.con1 (fn (a,b,c,r) => CHECK_REML {lvar=a,tyvars=b,Type=c,rep=r}) + (fn CHECK_REML{lvar,tyvars,Type,rep} => (lvar,tyvars,Type,rep) + | _ => die "pu_LambdaExp.CHECK_REML") + (Pickle.tup4Gen0(Lvars.pu,pu_tyvars,pu_Type,Report.pu)) in Pickle.dataGen("LambdaExp.LambdaExp",toInt,[fun_VAR, fun_INTEGER, @@ -1797,7 +1840,8 @@ structure LambdaExp : LAMBDA_EXP = fun_PRIM, fun_FRAME, fun_LETREGION, - fun_F64]) + fun_F64, + fun_CHECK_REML]) end structure TyvarSet = NatSet @@ -1870,6 +1914,7 @@ structure LambdaExp : LAMBDA_EXP = | TYPED (e,tau,_) => tyvars_Type s tau (tyvars_Exp s e acc) | PRIM(p,es) => tyvars_Exps s es (tyvars_Prim s p acc) | FRAME fr => tyvars_Frame s fr acc + | CHECK_REML {lvar,tyvars,Type,rep= _} => tyvars_Scheme s (tyvars, Type) acc end and tyvars_Exps s nil acc = acc diff --git a/src/Compiler/Lambda/LambdaStatSem.sml b/src/Compiler/Lambda/LambdaStatSem.sml index 87cb45b45..166f2317b 100644 --- a/src/Compiler/Lambda/LambdaStatSem.sml +++ b/src/Compiler/Lambda/LambdaStatSem.sml @@ -451,6 +451,7 @@ structure LambdaStatSem: LAMBDA_STAT_SEM = val eq_Type = LambdaBasics.eq_Type val eq_Types = LambdaBasics.eq_Types + val eq_sigma = LambdaBasics.eq_sigma fun check_t_no_f64_but_top s t = if eq_Type(t, f64Type) then () @@ -500,6 +501,16 @@ structure LambdaStatSem: LAMBDA_STAT_SEM = | eqTypes s (ty1::tys1, ty2::tys2) = (eqType s (ty1,ty2); eqTypes s (tys1, tys2)) | eqTypes s _ = die "eqTypes" + fun eqSigma s (sigma,sigma') = if eq_sigma(sigma,sigma') then () + else (log "--------------------------------\n"; + log ("Error in lambda type checking (" ^ s ^ "):\n"); + log "The type scheme\n"; + log_st (layoutTypeScheme sigma); + log "is not compatible with type scheme\n"; + log_st (layoutTypeScheme sigma'); + log "--------------------------------\n"; + die ("eqSigma")) + val unit_Type = RECORDtype ([],NONE) @@ -983,10 +994,16 @@ structure LambdaStatSem: LAMBDA_STAT_SEM = Frame {declared_lvars = map on_lvar declared_lvars, declared_excons = map on_excon declared_excons} end - ) handle AbortExp => raise AbortExp - | ? => (log_st (layoutLambdaExp lexp) ; - log_st (layout_env env); - raise AbortExp) + | CHECK_REML {lvar,tyvars,Type,rep= _} => + let val sigma = lookup_lvar env lvar + in eqSigma "CHECK_REML" (sigma,(tyvars,Type)) + ; Types nil + end + + ) handle AbortExp => raise AbortExp + | ? => (log_st (layoutLambdaExp lexp) ; + log_st (layout_env env); + raise AbortExp) fun check_bindings (e:LambdaExp) : unit = let val bound_lvs = LB.foldTD (fn acc => fn e => diff --git a/src/Compiler/Lambda/OptLambda.sml b/src/Compiler/Lambda/OptLambda.sml index 43065f0f1..3277dc6a9 100644 --- a/src/Compiler/Lambda/OptLambda.sml +++ b/src/Compiler/Lambda/OptLambda.sml @@ -689,6 +689,7 @@ structure OptLambda : OPT_LAMBDA = | PRIM(CCALLprim{name="__real_to_f64",...},[VAR _]) => () | PRIM(_, es) => safeLooks es | FRAME {declared_lvars,...} => List.app (fn {lvar,...} => if Lvars.eq(lv,lvar) then raise Bad else ()) declared_lvars + | CHECK_REML {lvar,...} => if Lvars.eq(lv,lvar) then raise Bad else () and safeLooks es = List.app safeLook es in (safeLook lamb; true) handle Bad => false @@ -728,6 +729,7 @@ structure OptLambda : OPT_LAMBDA = | PRIM(p,es) => PRIM(p,map subst es) | FRAME _ => if lvar_in_lamb lv e then die "subst_real_lvar_f64_in_lamb: impossible" else e + | CHECK_REML {lvar,...} => if Lvars.eq(lvar,lv) then die "subst_real_lvar_f64_in_lamb.CHECK_REML" else e in subst lamb end @@ -1289,6 +1291,7 @@ structure OptLambda : OPT_LAMBDA = | STRING _ => NONE | FN _ => NONE | HANDLE _ => NONE + | CHECK_REML _ => NONE in exn e end @@ -1313,9 +1316,11 @@ structure OptLambda : OPT_LAMBDA = | zero_uses (lv::lvs) = Lvars.zero_use lv andalso zero_uses lvs fun incr_uses (VAR{lvar,...}) = incr_use lvar (* Increase uses in an expression. *) + | incr_uses (CHECK_REML{lvar,...}) = incr_use lvar | incr_uses lamb = app_lamb incr_uses lamb fun decr_uses (VAR{lvar,...}) = decr_use lvar (* Decrease uses in an expression. *) + | decr_uses (CHECK_REML {lvar,...}) = decr_use lvar | decr_uses lamb = app_lamb decr_uses lamb (* ----------------------------------------------------------------- @@ -1323,17 +1328,18 @@ structure OptLambda : OPT_LAMBDA = * ----------------------------------------------------------------- *) fun init e = - case e - of VAR{lvar,instances,regvars} => incr_use lvar - | LET{pat,bind,scope} => (app (Lvars.reset_use o #1) pat; init bind; init scope) - | FN{pat,body} => (app (Lvars.reset_use o #1) pat; init body) - | FIX{functions,scope} => (app (Lvars.reset_use o #lvar) functions; - app (mark_lvar o #lvar) functions; - app (init o #bind) functions; - app (unmark_lvar o # lvar) functions; - init scope) - | FRAME {declared_lvars,...} => app (fn {lvar,...} => (incr_use lvar; incr_use lvar)) declared_lvars - | _ => app_lamb init e + case e of + VAR{lvar,instances,regvars} => incr_use lvar + | CHECK_REML {lvar,...} => incr_use lvar + | LET{pat,bind,scope} => (app (Lvars.reset_use o #1) pat; init bind; init scope) + | FN{pat,body} => (app (Lvars.reset_use o #1) pat; init body) + | FIX{functions,scope} => (app (Lvars.reset_use o #lvar) functions; + app (mark_lvar o #lvar) functions; + app (init o #bind) functions; + app (unmark_lvar o # lvar) functions; + init scope) + | FRAME {declared_lvars,...} => app (fn {lvar,...} => (incr_use lvar; incr_use lvar)) declared_lvars + | _ => app_lamb init e fun is_inlinable_fn lvar lamb = case lamb of @@ -1976,6 +1982,7 @@ structure OptLambda : OPT_LAMBDA = in (lamb, on_cv S cv) end) | NONE => ((*output(!Flags.log, "none\n");*) (lamb, CVAR {exp=lamb}))) + | CHECK_REML _ => fail | VAR _ => fail (* explicit region parameters *) | INTEGER _ => (lamb, CCONST {exp=lamb}) | WORD _ => (lamb, CCONST {exp=lamb}) diff --git a/src/Compiler/Regions/RTYPE.sig b/src/Compiler/Regions/RTYPE.sig index 82ecf4901..d2862b113 100644 --- a/src/Compiler/Regions/RTYPE.sig +++ b/src/Compiler/Regions/RTYPE.sig @@ -132,7 +132,7 @@ sig val c_function_effects : sigma * mu -> (place * int option) list type StringTree - (* the boolean in the following functions should be true iff on want to + (* the boolean in the following functions should be true iff one wants to omit region information *) val mk_layout : bool -> (Type -> StringTree) * (mu -> StringTree) val mk_lay_sigma : bool -> sigma -> StringTree diff --git a/src/Compiler/Regions/RType.sml b/src/Compiler/Regions/RType.sml index c763b3efb..978815966 100644 --- a/src/Compiler/Regions/RType.sml +++ b/src/Compiler/Regions/RType.sml @@ -505,7 +505,8 @@ struct val effs2 = ann_ty ty2 [] in List.foldl u cone (ListPair.zipEq(effs1,effs2)) - handle X => let val (lay_ty,_) = mk_layout false; + handle (X as Report.DeepError _) => raise X + | X => let val (lay_ty,_) = mk_layout false; fun dump ty = PP.outputTree(fn s => TextIO.output(!Flags.log, s), lay_ty ty, !Flags.colwidth) in TextIO.output(!Flags.log, "ty1 = "); dump ty1; diff --git a/src/Compiler/Regions/SpreadExpression.sml b/src/Compiler/Regions/SpreadExpression.sml index 0528a9942..69e2da65e 100644 --- a/src/Compiler/Regions/SpreadExpression.sml +++ b/src/Compiler/Regions/SpreadExpression.sml @@ -93,22 +93,24 @@ struct fun logtree (t:PP.StringTree) = PP.outputTree(logsay, t, !Flags.colwidth) fun fst (a,b) = a + fun layout_sigma sigma = R.mk_lay_sigma false sigma + fun log_sigma (sigma1, lvar) = case R.bv sigma1 of (_, _, []) => (say ("***" ^ Lvars.pr_lvar lvar ^ " is:"); logsay (Lvars.pr_lvar lvar ^ " is:\n"); - logtree(R.mk_lay_sigma false sigma1); + logtree(layout_sigma sigma1); logsay "\n") | ([],_,alpha::alphas) => (say ("******" ^ Lvars.pr_lvar lvar ^ " is polymorphic with escaping regions"); logsay (Lvars.pr_lvar lvar ^ " is polymorphic with escaping regions:\n"); - logtree(R.mk_lay_sigma false sigma1); + logtree(layout_sigma sigma1); logsay "\n") | (_,_,alpha::alphas) => (say ("***" ^ Lvars.pr_lvar lvar ^ " is polymorphic"); logsay (Lvars.pr_lvar lvar ^ " is polymorphic:\n"); - logtree(R.mk_lay_sigma false sigma1); + logtree(layout_sigma sigma1); logsay "\n"); fun print_tree t = PP.outputTree(print, t, !Flags.colwidth) @@ -121,7 +123,7 @@ struct children=map Eff.layout_effect effects}) fun print_tau tau = print_tree (R.mk_lay_sigma' false ([],[],[],tau)) - fun print_sigma sigma = print_tree (R.mk_lay_sigma false sigma) + fun print_sigma sigma = print_tree (layout_sigma sigma) fun noSome x msg = case x of @@ -400,6 +402,12 @@ struct fun enforceConstraint rse = R.enforceConstraint (RSE.lookupRegVar rse) deepError + fun fresh_regvars_with_rhos (B,rvs) = + List.foldr (fn (rv,(acc,B)) => + let val (rho,B) = Eff.freshRhoEpsRegVar (B,rv) + in ((rv,rho)::acc,B) + end) (nil,B) rvs + fun mk_sigma_hats (B,retract_level) [] = (B,[]) | mk_sigma_hats (B,retract_level) ({lvar,regvars,tyvars,Type,constrs,bind}::rest) = let @@ -409,11 +417,7 @@ struct case Type of E.ARROWtype p => p | _ => die "mk_sigma_hats" - val (regvars_with_rhos,B) = - List.foldr (fn (rv,(acc,B)) => - let val (rho,B) = Eff.freshRhoEpsRegVar (B,rv) - in ((rv,rho)::acc,B) - end) (nil,B) regvars + val (regvars_with_rhos,B) = fresh_regvars_with_rhos (B,regvars) val (tau_0, B) = freshType' regvars_with_rhos (Type,B) val (B,sigma) = R.generalize_all(B,retract_level,map (fn tv => (tv,NONE)) tyvars,tau_0) val sigma_hat = R.drop_alphas sigma @@ -1520,6 +1524,90 @@ good *) NOTAIL, []) end + | E.CHECK_REML {lvar,tyvars,Type,rep} => + let val (compound,create_region_record,regvars,sigma,p,_,_) = + noSome (RSE.lookupLvar rse lvar) "declared lvar of CHECK_REML not in scope" + + val (B,sigma') = + let val level = Eff.level B + val B = Eff.push B + val (regvars_rhos,B) = fresh_regvars_with_rhos (B,E.regvarsType Type) + val (tau_0, B) = freshType' regvars_rhos (Type,B) + val (B,sigma') = R.generalize_all(B,level,map (fn tv => (tv,NONE)) tyvars,tau_0) + val (_,B) = Eff.pop B + in (B,sigma') + end handle X => (print "SIGMA'\n"; raise X) + + (* Two checks: + (1) unify (instance sigma, tauOf sigma') + (2) unify (tauOf sigma, instance sigma') + *) + fun instFresh (sigma,tvs) B = + let val tvs = map #1 tvs + val (rhos,epss,_,_) = R.un_scheme sigma + val (rhos',B) = Eff.freshRhosPreserveRT (rhos,B) + val (epss',B) = Eff.freshEpss (epss,B) + val il = R.mk_il (rhos',epss',map R.mkTYVAR tvs) + in R.inst (NONE,sigma,il) B + end (*handle X => (print "instFresh\n"; raise X)*) + + fun check str s s' B = + let (* + val () = ( print ("IN " ^ str ^ "\n") + ; print_sigma s + ; print "\n" + ; print_sigma s' + ; print "\n" + ) + *) + val (_,_,tvs',t') = R.un_scheme s' + val B = Eff.push B + val (t,B) = instFresh (s,tvs') B + val B = R.unify_ty (t',t) B + val (_,B) = Eff.pop B + in B + end (*handle X => (print (str ^ "\n"); raise X)*) + + fun rep_sigma s = + let val r = !Flags.print_types + in Flags.print_types := true + ; PP.reportStringTree (PP.NODE{start=" val " ^ Lvars.pr_lvar lvar ^ " : ", finish="", + indent=4,childsep=PP.NOSEP, + children=[layout_sigma s]}) + before Flags.print_types := r + end + + infix // fun r // r' = Report.// (r,r') + val B = check "CHECK1" sigma sigma' B + handle Report.DeepError rep0 => + raise Report.DeepError + ( rep + // Report.line "The implementation type " + // rep_sigma sigma + // Report.line "is not as general as the specified type" + // rep_sigma sigma' + // Report.line "Please modify either the implementation or the specification." + // rep0 + ) + + val B = check "CHECK2" sigma' sigma B + handle Report.DeepError rep0 => + raise Report.DeepError + ( rep + // Report.line "The specified type " + // rep_sigma sigma' + // Report.line "is not as general as the implementation type" + // rep_sigma sigma + // Report.line "Please modify either the specification or the implementation." + // rep0 + ) + + in (B, E'.TR(E'.UB_RECORD nil, + E'.Mus nil, + Eff.empty), + NOTAIL, + []) + end | _ => die "S: unknown expression" ) in diff --git a/src/Manager/IntModules.sml b/src/Manager/IntModules.sml index 98ad99658..5a4af1f7b 100644 --- a/src/Manager/IntModules.sml +++ b/src/Manager/IntModules.sml @@ -424,7 +424,7 @@ functor IntModules(structure ManagerObjects : MANAGER_OBJECTS0 val E = case to_TypeInfo i of SOME (ElabInfo.TypeInfo.TRANS_CONSTRAINT_INFO E) => E | _ => die "int_strexp.TRANSPARENT_CONSTRAINTstrexp.no env info" - val ce' = CE.constrain(ce,E) + val (ce',_) = CE.constrain(ce,E) in (ce', cb, mc) end | OPAQUE_CONSTRAINTstrexp(i, strexp, sigexp) => @@ -460,7 +460,7 @@ functor IntModules(structure ManagerObjects : MANAGER_OBJECTS0 val (absprjid,strid,E,BBC,intB0) = IntFunEnv.lookup ((#1 o IntBasis.un) intB) funid val E' = Environments.Realisation.on_Env phi E val _ = chat "[constraining argument begin...]" - val ce = CE.constrain(ce,E') + val (ce,_) = CE.constrain(ce,E') val _ = chat "[constraining argument end...]" val intB1 = IntBasis.mk(IntFunEnv.empty,IntSigEnv.empty,CE.declare_strid(strid,ce,CE.emptyCEnv), CompileBasis.plus(#4 (IntBasis.un intB), cb)) (* The argument may use things *) diff --git a/src/Tools/Tester/Tester.sml b/src/Tools/Tester/Tester.sml index b8ce59ccc..a4431fb49 100644 --- a/src/Tools/Tester/Tester.sml +++ b/src/Tools/Tester/Tester.sml @@ -81,6 +81,7 @@ structure Tester : TESTER = val compile_command_base = kitexe ^ (if !logdirect then " " else " --log_to_file ") ^ (if opt "nobasislib" then "-no_basislib " else "") ^ + (if opt "noopt" then "-no_opt " else "") ^ (if opt "tc" (*Time Compiler*) then "--timings " else "") ^ (if opt "ccl" (*Compare Compiler Logs*) then "--report_file_sig " else "") ^ concatWith " " flags diff --git a/test/explicit_regions/Makefile b/test/explicit_regions/Makefile index 430b8cd5a..3f23dc587 100644 --- a/test/explicit_regions/Makefile +++ b/test/explicit_regions/Makefile @@ -1,9 +1,9 @@ -FLAGS=-no_basislib --maximum_inline_size 0 -no_opt +FLAGS=--maximum_inline_size 0 REML=../../bin/reml $(FLAGS) SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expty1.sml err_expty2.sml \ err_expty3.sml err_patty1.sml err_funty1.sml err_funty2.sml err_funty3.sml expty1.sml expty2.sml \ - disputs.sml disputs2.sml server.sml + disputs.sml disputs2.sml server.sml mod.sml mod2.sml .PHONY: all all: diff --git a/test/explicit_regions/all.tst b/test/explicit_regions/all.tst index 670755334..d4da1130d 100644 --- a/test/explicit_regions/all.tst +++ b/test/explicit_regions/all.tst @@ -6,7 +6,7 @@ consists of a file name path (with extension sml, sig, or mlb) followed by a list of tokens. The following tokens are supported: nobasislib ; do not import basis library - nooptimiser ; disable lambda optimiser + noopt ; disable lambda optimiser ccl ; compare compiler logs tx ; time executable tc ; time compiler @@ -21,67 +21,71 @@ Test files may contain Standard ML like comments. (* Testing expression annotations *) (* ------------------------------ *) -er1.sml ccl ecte (* It is an error to declare a region with a name that is already in scope (region decs) *) -er2.sml ccl ecte (* It is an error to have duplicate region names in a region declaration *) -er3.sml ccl ecte (* A region cannot be used for values that belong to different region types *) -er4.sml ccl ecte (* It is an error to refer to a region that is not in scope *) -er5.sml ccl ecte (* It is an error to declare a region variable that is already in scope (function params) *) -er6.sml ccl ecte (* It is an error to unify a region parameter with a global region variable *) -er7.sml ccl ecte (* It is an error to unify a local region with a global region variable *) -er8.sml ccl ecte (* It is an error to unify a local region with a region parameter *) -er9.sml ccl ecte (* It is an error to unify two region parameters *) -er10.sml ccl ecte (* It is an error for a value in an explicit local region to escape *) -er11.sml ccl ecte (* It is an error for a value in an explicit local region to escape in a closure *) -er12.sml ccl ecte (* It is an error to refer to a region that is not in scope (function parameter) *) -er13.sml ccl ecte (* It is an error to call a function with a different non-zero number of region parameters than the function declares *) -er14.sml ccl ecte (* It is an error to give multiple explicit regions to ref *) -er15.sml ccl ecte (* It is an error to give multiple explicit regions to con0 *) -er16.sml ccl ecte (* It is an error to give multiple explicit regions to con1 *) -er17.sml ccl ecte (* It is an error to have constructors of different conditional branches to be allocated in different regions *) -er18.sml ccl ecte (* Empty record types cannot be annotated with explicit regions *) -er19.sml ccl ecte (* It is an error to use an effect variable for allocation *) -param.sml (* Functions can be declared to take region parameters *) -param1.sml (* Functions can be declared to take one region parameter *) -tup.sml (* Tuples can be allocated in explicit regions *) -tup2.sml (* Two tuples can be allocated in the same explicit region *) -rec.sml (* Records can be allocated in explicit regions *) -string.sml (* Strings can be allocated in explicit regions *) -ref.sml (* Ref constructor can be allocated in explicit regions *) -con0.sml (* Con0 constructor can be allocated in explicit regions *) -con1.sml (* Con1 constructor can be allocated in explicit regions *) -call.sml -call2.sml -ty1.sml (* Types can be annotated with explicit regions *) +er1.sml ccl ecte nobasislib noopt (* It is an error to declare a region with a name that is already in scope (region decs) *) +er2.sml ccl ecte nobasislib noopt (* It is an error to have duplicate region names in a region declaration *) +er3.sml ccl ecte nobasislib noopt (* A region cannot be used for values that belong to different region types *) +er4.sml ccl ecte nobasislib noopt (* It is an error to refer to a region that is not in scope *) +er5.sml ccl ecte nobasislib noopt (* It is an error to declare a region variable that is already in scope (function params) *) +er6.sml ccl ecte nobasislib noopt (* It is an error to unify a region parameter with a global region variable *) +er7.sml ccl ecte nobasislib noopt (* It is an error to unify a local region with a global region variable *) +er8.sml ccl ecte nobasislib noopt (* It is an error to unify a local region with a region parameter *) +er9.sml ccl ecte nobasislib noopt (* It is an error to unify two region parameters *) +er10.sml ccl ecte nobasislib noopt (* It is an error for a value in an explicit local region to escape *) +er11.sml ccl ecte nobasislib noopt (* It is an error for a value in an explicit local region to escape in a closure *) +er12.sml ccl ecte nobasislib noopt (* It is an error to refer to a region that is not in scope (function parameter) *) +er13.sml ccl ecte nobasislib noopt (* It is an error to call a function with a different non-zero number of region parameters than the function declares *) +er14.sml ccl ecte nobasislib noopt (* It is an error to give multiple explicit regions to ref *) +er15.sml ccl ecte nobasislib noopt (* It is an error to give multiple explicit regions to con0 *) +er16.sml ccl ecte nobasislib noopt (* It is an error to give multiple explicit regions to con1 *) +er17.sml ccl ecte nobasislib noopt (* It is an error to have constructors of different conditional branches to be allocated in different regions *) +er18.sml ccl ecte nobasislib noopt (* Empty record types cannot be annotated with explicit regions *) +er19.sml ccl ecte nobasislib noopt (* It is an error to use an effect variable for allocation *) +param.sml nobasislib noopt (* Functions can be declared to take region parameters *) +param1.sml nobasislib noopt (* Functions can be declared to take one region parameter *) +tup.sml nobasislib noopt (* Tuples can be allocated in explicit regions *) +tup2.sml nobasislib noopt (* Two tuples can be allocated in the same explicit region *) +rec.sml nobasislib noopt (* Records can be allocated in explicit regions *) +string.sml nobasislib noopt (* Strings can be allocated in explicit regions *) +ref.sml nobasislib noopt (* Ref constructor can be allocated in explicit regions *) +con0.sml nobasislib noopt (* Con0 constructor can be allocated in explicit regions *) +con1.sml nobasislib noopt (* Con1 constructor can be allocated in explicit regions *) +call.sml nobasislib noopt +call2.sml nobasislib noopt +ty1.sml nobasislib noopt (* Types can be annotated with explicit regions *) (* ----------------------------------- *) (* Testing the use of type annotations *) (* ----------------------------------- *) -err_expty1.sml ccl ecte (* The global region variable of type T cannot be associated with a pair type *) -err_expty2.sml ccl ecte (* The global region variable of type pair cannot be associated with a function type *) -err_expty3.sml ccl ecte (* Escaping functions cannot live in local regions *) -err_patty1.sml ccl ecte (* The global region variable of type T cannot be associated with a pair type (pattern) *) -err_funty1.sml ccl ecte (* The global region variable of type T cannot be associated with a pair type (function return type) *) -err_funty2.sml ccl ecte (* Inconsistent use of a parameter region. A region cannot hold both pairs and triples. *) -err_funty3.sml ccl ecte (* Inconsistent use of a parameter region. A region cannot hold both pairs and strings. *) +err_expty1.sml ccl ecte nobasislib noopt (* The global region variable of type T cannot be associated with a pair type *) +err_expty2.sml ccl ecte nobasislib noopt (* The global region variable of type pair cannot be associated with a function type *) +err_expty3.sml ccl ecte nobasislib noopt (* Escaping functions cannot live in local regions *) +err_patty1.sml ccl ecte nobasislib noopt (* The global region variable of type T cannot be associated with a pair type (pattern) *) +err_funty1.sml ccl ecte nobasislib noopt (* The global region variable of type T cannot be associated with a pair type (function return type) *) +err_funty2.sml ccl ecte nobasislib noopt (* Inconsistent use of a parameter region. A region cannot hold both pairs and triples. *) +err_funty3.sml ccl ecte nobasislib noopt (* Inconsistent use of a parameter region. A region cannot hold both pairs and strings. *) -expty1.sml (* A local function can be forced into a global region *) -expty2.sml (* A locally generated function that is returned can be stored in a passed region *) +expty1.sml nobasislib noopt (* A local function can be forced into a global region *) +expty2.sml nobasislib noopt (* A locally generated function that is returned can be stored in a passed region *) -err_ty1.sml ccl ecte (* An effect variable (beginning with 'e') cannot be used as a region variable *) -funty1.sml (* A local function can be forced to have toplevel effect *) -err_copylist.sml ccl ecte (* Exomorphisms by non-unifiable explicit region variables *) +err_ty1.sml ccl ecte nobasislib noopt (* An effect variable (beginning with 'e') cannot be used as a region variable *) +funty1.sml nobasislib noopt (* A local function can be forced to have toplevel effect *) +err_copylist.sml ccl ecte nobasislib noopt (* Exomorphisms by non-unifiable explicit region variables *) -effty1.sml ccl ecte (* A function with a local effect cannot escape *) +effty1.sml ccl ecte nobasislib noopt (* A function with a local effect cannot escape *) -nomut-err.sml ccl ecte (* Violation of nomut constraint on function *) -nomut-ok.sml (* Satisfiability of nomut constraint on function *) +nomut-err.sml ccl ecte nobasislib noopt (* Violation of nomut constraint on function *) +nomut-ok.sml nobasislib noopt (* Satisfiability of nomut constraint on function *) -nomut2-err.sml ccl ecte (* Violation of nomut constraint on function instantiation *) +nomut2-err.sml ccl ecte nobasislib noopt (* Violation of nomut constraint on function instantiation *) -disputs.sml ccl ecte (* Violation of disjoint put-effects (##) - let rec *) -disputs2.sml ccl ecte (* Violation of disjoint put-effects (##) - fun *) +disputs.sml ccl ecte nobasislib noopt (* Violation of disjoint put-effects (##) - let rec *) +disputs2.sml ccl ecte nobasislib noopt (* Violation of disjoint put-effects (##) - fun *) -par.sml (* A sound implementation of par with constraint *) -par-no.sml ccl ecte (* But it needs to be satisfied *) -par-no2.sml ccl ecte (* The trivial definition of par is not ok *) \ No newline at end of file +par.sml nobasislib noopt (* A sound implementation of par with constraint *) +par-no.sml ccl ecte nobasislib noopt (* But it needs to be satisfied *) +par-no2.sml ccl ecte nobasislib noopt (* The trivial definition of par is not ok *) + +mod.sml ccl ecte (* Transparent signature matching: spec type at least as general as impl type *) +mod2.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) +mod3.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) diff --git a/test/explicit_regions/mod.sml b/test/explicit_regions/mod.sml new file mode 100644 index 000000000..0d480c32b --- /dev/null +++ b/test/explicit_regions/mod.sml @@ -0,0 +1,12 @@ +(* Transparent signature matching: It is checked that the type of an implementation is + * is at least as general as the specified type. *) + +signature X = sig + val f : string`r1 -> string`r2 +end + +structure K1 = struct + fun f `[r1] (a:string`r1) : string`r1 = a ^ "" +end + +structure K2 = K1 : X diff --git a/test/explicit_regions/mod.sml.log.ok b/test/explicit_regions/mod.sml.log.ok new file mode 100644 index 000000000..4549e2b2b --- /dev/null +++ b/test/explicit_regions/mod.sml.log.ok @@ -0,0 +1,26 @@ +[reading source file: mod.sml] +> signature X = + sig + val f : string`r1 -> string`r2 + end + structure K1 : + sig + val f : string`r1 -> string`r1 + end + structure K2 : + sig + val f : string`r1 -> string`r2 + end +mod.sml, line 12, column 15: + structure K2 = K1 : X + ^^^^^^ +The implementation type + val f : all `r1.(string,`r1)->(string,`r1) +is not as general as the specified type + val f : all `r2,`r1.(string,`r1)->(string,`r2) +Please modify either the implementation or the specification. +mod.sml, line 5, column 30: + val f : string`r1 -> string`r2 + ^^ +Cannot unify the explicit region variables `r2 and `r1 +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/mod2.sml b/test/explicit_regions/mod2.sml new file mode 100644 index 000000000..39bf70c9c --- /dev/null +++ b/test/explicit_regions/mod2.sml @@ -0,0 +1,12 @@ +(* Transparent signature matching: It is checked that an explicitly specified + * type is at least as general as the implementation. *) + +signature X = sig + val f : string`r1 -> string`r1 +end + +structure K1 = struct + fun f `[r1 r2] (a:string`r1) : string`r2 = a ^ "" +end + +structure K2 = K1 : X diff --git a/test/explicit_regions/mod2.sml.log.ok b/test/explicit_regions/mod2.sml.log.ok new file mode 100644 index 000000000..bffe59269 --- /dev/null +++ b/test/explicit_regions/mod2.sml.log.ok @@ -0,0 +1,26 @@ +[reading source file: mod2.sml] +> signature X = + sig + val f : string`r1 -> string`r1 + end + structure K1 : + sig + val f : string`r1 -> string`r2 + end + structure K2 : + sig + val f : string`r1 -> string`r1 + end +mod2.sml, line 12, column 15: + structure K2 = K1 : X + ^^^^^^ +The specified type + val f : all `r1.(string,`r1)->(string,`r1) +is not as general as the implementation type + val f : all `r2,`r1.(string,`r1)->(string,`r2) +Please modify either the specification or the implementation. +mod2.sml, line 9, column 8: + fun f `[r1 r2] (a:string`r1) : string`r2 = a ^ "" + ^^^^^^^^ +Cannot unify the explicit region variables `r2 and `r1 +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/mod3.sml b/test/explicit_regions/mod3.sml new file mode 100644 index 000000000..1b3df6fa5 --- /dev/null +++ b/test/explicit_regions/mod3.sml @@ -0,0 +1,12 @@ +(* Transparent signature matching: It is checked that the type of an implementation is + * is at least as general as the specified type. *) + +signature X = sig + val f : string`r1 -> string`r2 +end + +structure K1 = struct + fun f (a:string) = a +end + +structure K2 = K1 : X diff --git a/test/explicit_regions/mod3.sml.log.ok b/test/explicit_regions/mod3.sml.log.ok new file mode 100644 index 000000000..705c777f5 --- /dev/null +++ b/test/explicit_regions/mod3.sml.log.ok @@ -0,0 +1,26 @@ +[reading source file: mod3.sml] +> signature X = + sig + val f : string`r1 -> string`r2 + end + structure K1 : + sig + val f : string -> string + end + structure K2 : + sig + val f : string`r1 -> string`r2 + end +mod3.sml, line 12, column 15: + structure K2 = K1 : X + ^^^^^^ +The implementation type + val f : all r15.(string,r15)->(string,r15) +is not as general as the specified type + val f : all `r2,`r1.(string,`r1)->(string,`r2) +Please modify either the implementation or the specification. +mod3.sml, line 5, column 30: + val f : string`r1 -> string`r2 + ^^ +Cannot unify the explicit region variables `r2 and `r1 +Stopping compilation of MLB-file due to error (code 1). From 668601705e2e32ee932179c40dae5a745136ca97 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:23:37 +0100 Subject: [PATCH 02/18] fix js backend --- src/Compiler/Backend/JS/ExpToJs2.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Compiler/Backend/JS/ExpToJs2.sml b/src/Compiler/Backend/JS/ExpToJs2.sml index a20307d5c..4516ccad9 100644 --- a/src/Compiler/Backend/JS/ExpToJs2.sml +++ b/src/Compiler/Backend/JS/ExpToJs2.sml @@ -1006,6 +1006,7 @@ fun toj C (P:{clos_p:bool}) (e:Exp) : ret = end | L.RAISE (e,_) => resolveS (toj1 C P e) (fn e' => fn k => J.Throw e') | L.TYPED (e,_,_) => toj C P e + | L.CHECK_REML _ => die "REML check not supported by JS backend" and toj_let C P (lvs, binds, scope) = let From 70188827af54c19e0f335c84cb18609dc5d3c5b7 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:27:42 +0100 Subject: [PATCH 03/18] fixes of typos in tests --- test/explicit_regions/Makefile | 2 +- test/explicit_regions/mod.sml | 2 +- test/explicit_regions/mod3.sml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/explicit_regions/Makefile b/test/explicit_regions/Makefile index 3f23dc587..7500fd0d5 100644 --- a/test/explicit_regions/Makefile +++ b/test/explicit_regions/Makefile @@ -3,7 +3,7 @@ REML=../../bin/reml $(FLAGS) SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expty1.sml err_expty2.sml \ err_expty3.sml err_patty1.sml err_funty1.sml err_funty2.sml err_funty3.sml expty1.sml expty2.sml \ - disputs.sml disputs2.sml server.sml mod.sml mod2.sml + disputs.sml disputs2.sml server.sml mod.sml mod2.sml mod3.sml .PHONY: all all: diff --git a/test/explicit_regions/mod.sml b/test/explicit_regions/mod.sml index 0d480c32b..8e4fd51a0 100644 --- a/test/explicit_regions/mod.sml +++ b/test/explicit_regions/mod.sml @@ -1,4 +1,4 @@ -(* Transparent signature matching: It is checked that the type of an implementation is +(* Transparent signature matching: It is checked that the type of an implementation * is at least as general as the specified type. *) signature X = sig diff --git a/test/explicit_regions/mod3.sml b/test/explicit_regions/mod3.sml index 1b3df6fa5..d722bb457 100644 --- a/test/explicit_regions/mod3.sml +++ b/test/explicit_regions/mod3.sml @@ -1,4 +1,4 @@ -(* Transparent signature matching: It is checked that the type of an implementation is +(* Transparent signature matching: It is checked that the type of an implementation * is at least as general as the specified type. *) signature X = sig From dc52953bf67366819bd68b120e9fe18c916849d2 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:31:14 +0100 Subject: [PATCH 04/18] fix action --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 9876f640d..5a17ade3c 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -44,8 +44,8 @@ jobs: - name: Install dependencies (linux) if: ${{ env.OS == 'linux' }} run: | - # sudo apt-get -qq update - sudo apt-get install -y gcc autoconf make + #sudo apt-get -qq update + #sudo apt-get install -y gcc autoconf make echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs From f21fc9f6f3a0250a3234462cbbc2a3bbf5f72a7b Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:35:12 +0100 Subject: [PATCH 05/18] fix action --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 5a17ade3c..ecdd76455 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -44,8 +44,8 @@ jobs: - name: Install dependencies (linux) if: ${{ env.OS == 'linux' }} run: | - #sudo apt-get -qq update - #sudo apt-get install -y gcc autoconf make + sudo apt-get -qq update + sudo apt-get install -y gcc autoconf make echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs From 8d56ac54927174dfaa51f51ffe5051e1ef4b9b68 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 12:50:15 +0100 Subject: [PATCH 06/18] fix action --- .github/workflows/main.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index ecdd76455..24cd3a76b 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -45,6 +45,7 @@ jobs: if: ${{ env.OS == 'linux' }} run: | sudo apt-get -qq update + sudo apt-get upgrade -y sudo apt-get install -y gcc autoconf make echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs From 55b89e66e067257347fe9e0753e47f5c64662925 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:00:17 +0100 Subject: [PATCH 07/18] fix action --- .github/workflows/main.yml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 24cd3a76b..b56bd653c 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -45,15 +45,25 @@ jobs: if: ${{ env.OS == 'linux' }} run: | sudo apt-get -qq update + echo $? sudo apt-get upgrade -y + echo $? sudo apt-get install -y gcc autoconf make + echo $? echo "THECC=gcc" >> $GITHUB_ENV + echo $? mkdir phantomjs + echo $? cd phantomjs + echo $? wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 + echo $? tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 + echo $? cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ + echo $? cd .. + echo $? - name: Install dependencies (linux, mlton) if: ${{ env.OS == 'linux' && matrix.mlcomp == 'mlton' }} From 163cd34cf736a75da6b1860461a77836edf8f971 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:00:47 +0100 Subject: [PATCH 08/18] fix action --- .github/workflows/main.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b56bd653c..a02d4c4f4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -46,8 +46,6 @@ jobs: run: | sudo apt-get -qq update echo $? - sudo apt-get upgrade -y - echo $? sudo apt-get install -y gcc autoconf make echo $? echo "THECC=gcc" >> $GITHUB_ENV From a7f0d48cd7213546661f4acfbbbdd16f0a3f5e7c Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:46:43 +0100 Subject: [PATCH 09/18] fix action --- .github/workflows/main.yml | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index a02d4c4f4..bc8bae156 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -44,6 +44,7 @@ jobs: - name: Install dependencies (linux) if: ${{ env.OS == 'linux' }} run: | + set -e sudo apt-get -qq update echo $? sudo apt-get install -y gcc autoconf make @@ -67,6 +68,7 @@ jobs: if: ${{ env.OS == 'linux' && matrix.mlcomp == 'mlton' }} working-directory: ${{ env.RUNHOME }} run: | + set -e echo "[OS: $OS, HOME: $RUNHOME, THECC: ${{env.THECC}}]" wget -q https://github.com/MLton/mlton/releases/download/on-20241230-release/mlton-20241230-1.amd64-linux.ubuntu-24.04_static.tgz tar xzf mlton-20241230-1.amd64-linux.ubuntu-24.04_static.tgz @@ -103,6 +105,7 @@ jobs: - name: Install MLKit and smlpkg working-directory: ${{ env.RUNHOME }} run: | + set -e echo "[OS: $OS, HOME: $RUNHOME, THECC: ${{env.THECC}}]" wget -q https://github.com/diku-dk/smlpkg/releases/download/v0.1.4/smlpkg-bin-dist-${{env.OS}}.tgz tar xzf smlpkg-bin-dist-${{env.OS}}.tgz @@ -116,6 +119,7 @@ jobs: - name: Check MLton if: ${{ matrix.mlcomp == 'mlton' }} run: | + set -e mlton echo 'github.event_name: ' ${{ github.event_name }} echo 'github.ref: ' ${{ github.ref }} @@ -123,6 +127,7 @@ jobs: - name: Check MLKit if: ${{ matrix.mlcomp == 'mlkit' }} run: | + set -e mlkit --version smlpkg --version echo 'github.event_name: ' ${{ github.event_name }} @@ -131,28 +136,33 @@ jobs: - name: Configure With MLton if: ${{ matrix.mlcomp == 'mlton' }} run: | + set -e ./autobuild CC=${{env.THECC}} ./configure --with-compiler='mlton @MLton ram-slop 0.7 -- -drop-pass deepFlatten -drop-pass refFlatten -verbose 2' - name: Configure With MLKit if: ${{ matrix.mlcomp == 'mlkit' }} run: | + set -e ./autobuild CC=${{env.THECC}} ./configure --with-compiler=mlkit - name: Build MLKit timeout-minutes: 240 run: | + set -e gcc --version - make mlkit - make mlkit_basislibs + make mlkit VERBOSE=1 + make mlkit_basislibs VERBOSE=1 - name: Install MLKit run: | + set -e sudo make install - name: Run MLKit tests run: | + set -e make -C test_dev test make -C test_dev test_prof make -C test test_mlkit @@ -164,15 +174,18 @@ jobs: - name: Configure SmlToJs if: ${{ matrix.mlcomp == 'mlton' }} run: | + set -e ./configure --with-compiler="SML_LIB=`pwd` `pwd`/bin/mlkit" - name: Build SmlToJs run: | + set -e make smltojs make smltojs_basislibs - name: Install SmlToJs run: | + set -e sudo make install_smltojs - name: Run SmlToJs tests (darwin) @@ -183,20 +196,24 @@ jobs: - name: Run SmlToJs tests (linux) if: ${{ env.OS == 'linux' }} run: | + set -e export OPENSSL_CONF=/dev/null make -C js/test test - name: Build and run Barry tests run: | + set -e make barry make -C test/barry all - name: Build binary distribution run: | + set -e make mlkit_bin_dist - name: Install binary distribution and test it run: | + set -e mkdir -p ${{ env.RUNHOME }}/tmp cp dist/mlkit-bin-dist-${{ env.OS }}.tgz ${{ env.RUNHOME }}/tmp/ cd ${{ env.RUNHOME }}/tmp/ @@ -211,6 +228,7 @@ jobs: - name: Test bootstrapping run: | + set -e make bootstrap - name: Upload release From 8494bea7657ebd993356cb0c9360ab9679f36d8d Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:50:11 +0100 Subject: [PATCH 10/18] fix action --- .github/workflows/main.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index bc8bae156..1837923b0 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -61,8 +61,7 @@ jobs: echo $? cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ echo $? - cd .. - echo $? + #cd .. - name: Install dependencies (linux, mlton) if: ${{ env.OS == 'linux' && matrix.mlcomp == 'mlton' }} From 23e7bf31de7c77765899ba26b600ed5c50a17a8e Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:53:43 +0100 Subject: [PATCH 11/18] fix action --- .github/workflows/main.yml | 18 +++++------------- 1 file changed, 5 insertions(+), 13 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 1837923b0..c2d0baf77 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -46,21 +46,13 @@ jobs: run: | set -e sudo apt-get -qq update - echo $? sudo apt-get install -y gcc autoconf make - echo $? echo "THECC=gcc" >> $GITHUB_ENV - echo $? - mkdir phantomjs - echo $? - cd phantomjs - echo $? - wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 - echo $? - tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 - echo $? - cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ - echo $? + #mkdir phantomjs + #cd phantomjs + #wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 + #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 + #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ #cd .. - name: Install dependencies (linux, mlton) From 1dcc9932788a244f29373569dbf7bdbab3783dde Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:56:03 +0100 Subject: [PATCH 12/18] fix action --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index c2d0baf77..63dc88a0a 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -48,8 +48,8 @@ jobs: sudo apt-get -qq update sudo apt-get install -y gcc autoconf make echo "THECC=gcc" >> $GITHUB_ENV - #mkdir phantomjs - #cd phantomjs + mkdir phantomjs + cd phantomjs #wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ From 42175d736e718a1923355da81e2b23779561c9d6 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:57:10 +0100 Subject: [PATCH 13/18] fix action --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 63dc88a0a..653f6280d 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -50,7 +50,7 @@ jobs: echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs - #wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 + wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ #cd .. From e1cfaf72e4f3710e9f3f698cc41f9b8c9727d8a0 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 13:59:00 +0100 Subject: [PATCH 14/18] fix action --- .github/workflows/main.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 653f6280d..cfbfcebd2 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -43,6 +43,7 @@ jobs: - name: Install dependencies (linux) if: ${{ env.OS == 'linux' }} + working-directory: ${{ env.RUNHOME }} run: | set -e sudo apt-get -qq update From faed872c323a4382edc688cd43464b8304796468 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 14:08:50 +0100 Subject: [PATCH 15/18] fix action --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index cfbfcebd2..edd6accbc 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -51,7 +51,7 @@ jobs: echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs - wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2 + wget -q https://github.com/melsman/phantomjs-bin/blob/main/phantomjs-2.1.1-linux-x86_64.tar.bz2 #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ #cd .. From 32e3a251c23641445d792a8ddf7a220a425205c8 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 14:13:23 +0100 Subject: [PATCH 16/18] fix action --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index edd6accbc..8c5e40c2e 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -51,7 +51,7 @@ jobs: echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs - wget -q https://github.com/melsman/phantomjs-bin/blob/main/phantomjs-2.1.1-linux-x86_64.tar.bz2 + wget -q https://github.com/melsman/phantomjs-bin/raw/refs/heads/main/phantomjs-2.1.1-linux-x86_64.tar.bz2 #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ #cd .. From 43c4178a7a5798d1e44025800f8fcab5552257b6 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Thu, 12 Feb 2026 14:16:36 +0100 Subject: [PATCH 17/18] fix action --- .github/workflows/main.yml | 25 +++---------------------- 1 file changed, 3 insertions(+), 22 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8c5e40c2e..23d0630b5 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -43,24 +43,21 @@ jobs: - name: Install dependencies (linux) if: ${{ env.OS == 'linux' }} - working-directory: ${{ env.RUNHOME }} run: | - set -e sudo apt-get -qq update sudo apt-get install -y gcc autoconf make echo "THECC=gcc" >> $GITHUB_ENV mkdir phantomjs cd phantomjs wget -q https://github.com/melsman/phantomjs-bin/raw/refs/heads/main/phantomjs-2.1.1-linux-x86_64.tar.bz2 - #tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 - #cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ - #cd .. + tar xjf phantomjs-2.1.1-linux-x86_64.tar.bz2 + cp -p phantomjs-2.1.1-linux-x86_64/bin/phantomjs /usr/local/bin/ + cd .. - name: Install dependencies (linux, mlton) if: ${{ env.OS == 'linux' && matrix.mlcomp == 'mlton' }} working-directory: ${{ env.RUNHOME }} run: | - set -e echo "[OS: $OS, HOME: $RUNHOME, THECC: ${{env.THECC}}]" wget -q https://github.com/MLton/mlton/releases/download/on-20241230-release/mlton-20241230-1.amd64-linux.ubuntu-24.04_static.tgz tar xzf mlton-20241230-1.amd64-linux.ubuntu-24.04_static.tgz @@ -97,7 +94,6 @@ jobs: - name: Install MLKit and smlpkg working-directory: ${{ env.RUNHOME }} run: | - set -e echo "[OS: $OS, HOME: $RUNHOME, THECC: ${{env.THECC}}]" wget -q https://github.com/diku-dk/smlpkg/releases/download/v0.1.4/smlpkg-bin-dist-${{env.OS}}.tgz tar xzf smlpkg-bin-dist-${{env.OS}}.tgz @@ -111,7 +107,6 @@ jobs: - name: Check MLton if: ${{ matrix.mlcomp == 'mlton' }} run: | - set -e mlton echo 'github.event_name: ' ${{ github.event_name }} echo 'github.ref: ' ${{ github.ref }} @@ -119,7 +114,6 @@ jobs: - name: Check MLKit if: ${{ matrix.mlcomp == 'mlkit' }} run: | - set -e mlkit --version smlpkg --version echo 'github.event_name: ' ${{ github.event_name }} @@ -128,33 +122,28 @@ jobs: - name: Configure With MLton if: ${{ matrix.mlcomp == 'mlton' }} run: | - set -e ./autobuild CC=${{env.THECC}} ./configure --with-compiler='mlton @MLton ram-slop 0.7 -- -drop-pass deepFlatten -drop-pass refFlatten -verbose 2' - name: Configure With MLKit if: ${{ matrix.mlcomp == 'mlkit' }} run: | - set -e ./autobuild CC=${{env.THECC}} ./configure --with-compiler=mlkit - name: Build MLKit timeout-minutes: 240 run: | - set -e gcc --version make mlkit VERBOSE=1 make mlkit_basislibs VERBOSE=1 - name: Install MLKit run: | - set -e sudo make install - name: Run MLKit tests run: | - set -e make -C test_dev test make -C test_dev test_prof make -C test test_mlkit @@ -166,18 +155,15 @@ jobs: - name: Configure SmlToJs if: ${{ matrix.mlcomp == 'mlton' }} run: | - set -e ./configure --with-compiler="SML_LIB=`pwd` `pwd`/bin/mlkit" - name: Build SmlToJs run: | - set -e make smltojs make smltojs_basislibs - name: Install SmlToJs run: | - set -e sudo make install_smltojs - name: Run SmlToJs tests (darwin) @@ -188,24 +174,20 @@ jobs: - name: Run SmlToJs tests (linux) if: ${{ env.OS == 'linux' }} run: | - set -e export OPENSSL_CONF=/dev/null make -C js/test test - name: Build and run Barry tests run: | - set -e make barry make -C test/barry all - name: Build binary distribution run: | - set -e make mlkit_bin_dist - name: Install binary distribution and test it run: | - set -e mkdir -p ${{ env.RUNHOME }}/tmp cp dist/mlkit-bin-dist-${{ env.OS }}.tgz ${{ env.RUNHOME }}/tmp/ cd ${{ env.RUNHOME }}/tmp/ @@ -220,7 +202,6 @@ jobs: - name: Test bootstrapping run: | - set -e make bootstrap - name: Upload release From 4d95a9207dee8c75a7313032c35675bcd1202a01 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Fri, 13 Feb 2026 14:55:02 +0100 Subject: [PATCH 18/18] fixes --- src/Compiler/Lambda/COMPILER_ENV.sml | 2 +- src/Compiler/Lambda/CompileDec.sml | 12 ++-- src/Compiler/Lambda/CompilerEnv.sml | 2 +- src/Compiler/Lambda/LAMBDA_EXP.sml | 3 +- src/Compiler/Lambda/LambdaBasics.sml | 3 +- src/Compiler/Lambda/LambdaExp.sml | 54 ++++++++------- src/Compiler/Lambda/LambdaStatSem.sml | 4 +- src/Compiler/Regions/EFFECT.sig | 4 +- src/Compiler/Regions/Effect.sml | 51 ++++++++------ src/Compiler/Regions/SpreadExpression.sml | 83 ++++++++++++++++------- test/explicit_regions/Makefile | 2 +- test/explicit_regions/all.tst | 8 ++- test/explicit_regions/mod3.sml.log.ok | 2 +- test/explicit_regions/mod4.sml | 13 ++++ test/explicit_regions/mod4.sml.log.ok | 26 +++++++ test/explicit_regions/mod5.sml | 15 ++++ test/explicit_regions/mod5.sml.out.ok | 1 + 17 files changed, 202 insertions(+), 83 deletions(-) create mode 100644 test/explicit_regions/mod4.sml create mode 100644 test/explicit_regions/mod4.sml.log.ok create mode 100644 test/explicit_regions/mod5.sml create mode 100644 test/explicit_regions/mod5.sml.out.ok diff --git a/src/Compiler/Lambda/COMPILER_ENV.sml b/src/Compiler/Lambda/COMPILER_ENV.sml index 6423c149c..50e5a57b5 100644 --- a/src/Compiler/Lambda/COMPILER_ENV.sml +++ b/src/Compiler/Lambda/COMPILER_ENV.sml @@ -95,7 +95,7 @@ signature COMPILER_ENV = * list contains the tynames of the * associated tystr. *) type ElabEnv and TypeScheme - val constrain : CEnv * ElabEnv -> CEnv * (lvar * tyvar list * Type) list + val constrain : CEnv * ElabEnv -> CEnv * (lvar * tyvar list * Type * Type list) list (* compileTypeScheme is used by constrain *) val set_compileTypeScheme : (TypeScheme -> tyvar list * Type) -> unit (* MEGA HACK *) diff --git a/src/Compiler/Lambda/CompileDec.sml b/src/Compiler/Lambda/CompileDec.sml index 6b12eb708..b60b99fa8 100644 --- a/src/Compiler/Lambda/CompileDec.sml +++ b/src/Compiler/Lambda/CompileDec.sml @@ -3552,11 +3552,13 @@ the 12 lines above are very similar to the code below fun g cs e = case cs of nil => e - | (lv,tvs,t)::cs => g cs (LET{pat=nil, - bind=CHECK_REML {lvar=lv, - tyvars=tvs, - Type=t,rep=rep}, - scope=e}) + | (lv,tvs,t,il)::cs => g cs (LET{pat=nil, + bind=CHECK_REML {lvar=lv, + tyvars=tvs, + Type=t, + il=il, + rep=rep}, + scope=e}) in (ce2, f o (g checks)) end | OPAQUE_CONSTRAINTstrexp(info, strexp, _) => die "OPAQUE_CONSTRAINTstrexp.not impl" diff --git a/src/Compiler/Lambda/CompilerEnv.sml b/src/Compiler/Lambda/CompilerEnv.sml index a8fcb9f4e..fc9be4d4f 100644 --- a/src/Compiler/Lambda/CompilerEnv.sml +++ b/src/Compiler/Lambda/CompilerEnv.sml @@ -538,7 +538,7 @@ structure CompilerEnv: COMPILER_ENV = val () = pr_st(layout_scheme(tvs',tau')) *) val checks = if LambdaExp.contains_regvars tau' - then [(lv,tvs',tau')] + then [(lv,tvs',tau',il')] else nil in (LVAR(lv,tvs',tau',il'), checks) end diff --git a/src/Compiler/Lambda/LAMBDA_EXP.sml b/src/Compiler/Lambda/LAMBDA_EXP.sml index 96311dc67..1f42d1d97 100644 --- a/src/Compiler/Lambda/LAMBDA_EXP.sml +++ b/src/Compiler/Lambda/LAMBDA_EXP.sml @@ -84,6 +84,7 @@ signature LAMBDA_EXP = val contains_regvars : Type -> bool val regvarsType : Type -> regvar list + val regvarsTypes : Type list -> regvar list datatype TypeList = (* To allow the result of a declaration *) Types of Type list (* to be a raised Bind exception. *) @@ -159,7 +160,7 @@ signature LAMBDA_EXP = (* a frame is the result of a structure-level * declaration. *) - | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, rep: Report} + | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, il: Type list, rep: Report} (* REML: Check that lvar has the type scheme specified... *) and 'a Switch = SWITCH of LambdaExp * ('a * LambdaExp) list * LambdaExp option diff --git a/src/Compiler/Lambda/LambdaBasics.sml b/src/Compiler/Lambda/LambdaBasics.sml index f4c16cbe1..5433f3695 100644 --- a/src/Compiler/Lambda/LambdaBasics.sml +++ b/src/Compiler/Lambda/LambdaBasics.sml @@ -550,12 +550,13 @@ structure LambdaBasics: LAMBDA_BASICS = | TYPED(e,t,cs) => TYPED(on_e ren e, on_tau ren t,cs) | PRIM(prim,es) => PRIM(on_prim ren prim, map (on_e ren) es) | FRAME _ => lamb - | CHECK_REML {lvar,tyvars,Type,rep} => + | CHECK_REML {lvar,tyvars,Type,il,rep} => let val tvs_pairs = map (fn tv => (tv, new_tv tv)) tyvars val ren_local = add_tvs tvs_pairs empty_ren in CHECK_REML {lvar=on_lv ren lvar, tyvars=map (on_tv ren_local) tyvars, Type=on_tau ren_local Type, + il=map (on_tau ren) il, rep=rep} end diff --git a/src/Compiler/Lambda/LambdaExp.sml b/src/Compiler/Lambda/LambdaExp.sml index 76f9e18e0..95df52c05 100644 --- a/src/Compiler/Lambda/LambdaExp.sml +++ b/src/Compiler/Lambda/LambdaExp.sml @@ -114,24 +114,27 @@ structure LambdaExp : LAMBDA_EXP = contains_regvars t orelse contains_regvarss ts | contains_regvarss nil = false - fun regvarsType (t:Type) : regvar list = - let fun ins r a = if List.exists (fn r' => RegVar.eq(r,r')) a then a - else r::a - fun add NONE a = a - | add (SOME r) a = ins r a - fun adds nil a = a - | adds (r::rs) a = adds rs (ins r a) - fun rvst t a = - case t of - TYVARtype _ => a - | ARROWtype(ts1,ro1,ts2,ro2) => add ro1 (add ro2 (rvsts ts1 (rvsts ts2 a))) - | CONStype(ts,_,NONE) => rvsts ts a - | CONStype(ts,_,SOME rs) => adds rs (rvsts ts a) - | RECORDtype (ts,ro) => add ro (rvsts ts a) - and rvsts nil a = a - | rvsts (t::ts) a = rvsts ts (rvst t a) - in rvst t nil - end + (* Find regvars in types *) + local + fun ins r a = if List.exists (fn r' => RegVar.eq(r,r')) a then a + else r::a + fun add NONE a = a + | add (SOME r) a = ins r a + fun adds nil a = a + | adds (r::rs) a = adds rs (ins r a) + fun rvst t a = + case t of + TYVARtype _ => a + | ARROWtype(ts1,ro1,ts2,ro2) => add ro1 (add ro2 (rvsts ts1 (rvsts ts2 a))) + | CONStype(ts,_,NONE) => rvsts ts a + | CONStype(ts,_,SOME rs) => adds rs (rvsts ts a) + | RECORDtype (ts,ro) => add ro (rvsts ts a) + and rvsts nil a = a + | rvsts (t::ts) a = rvsts ts (rvst t a) + in + fun regvarsType (t:Type) : regvar list = rvst t nil + fun regvarsTypes (ts:Type list) : regvar list = rvsts ts nil + end datatype TypeList = (* To allow the result of a declaration *) Types of Type list (* to be a raised Bind exception. *) @@ -207,7 +210,7 @@ structure LambdaExp : LAMBDA_EXP = (* a frame is the result of a structure-level * declaration. *) - | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, rep: Report} + | CHECK_REML of {lvar: lvar, tyvars: tyvar list, Type: Type, il: Type list, rep: Report} (* REML: Check that lvar has the type scheme specified... *) and 'a Switch = SWITCH of LambdaExp * ('a * LambdaExp) list * LambdaExp option @@ -1330,9 +1333,10 @@ structure LambdaExp : LAMBDA_EXP = indent=0,children=lvs@exs} end else layoutFrame "FRAME" fr - | CHECK_REML {lvar, tyvars, Type, rep= _} => + | CHECK_REML {lvar, tyvars, Type, rep= _, il} => PP.NODE{start="CHECK_REML(",finish=")", indent=11, - childsep=PP.NOSEP,children=[layVarSigma(lvar,tyvars,Type)]} + childsep=PP.RIGHT ",",children=[layVarSigma(lvar,tyvars,Type), + layoutTypes il]} and maybepar context t = parenthesise (context > 13) t @@ -1814,10 +1818,10 @@ structure LambdaExp : LAMBDA_EXP = Pickle.con1 F64 (fn F64 a => a | _ => die "pu_LambdaExp.F64") Pickle.string fun fun_CHECK_REML _ = - Pickle.con1 (fn (a,b,c,r) => CHECK_REML {lvar=a,tyvars=b,Type=c,rep=r}) - (fn CHECK_REML{lvar,tyvars,Type,rep} => (lvar,tyvars,Type,rep) + Pickle.con1 (fn ((a,b,c,il),r) => CHECK_REML {lvar=a,tyvars=b,Type=c,il=il,rep=r}) + (fn CHECK_REML{lvar,tyvars,Type,il,rep} => ((lvar,tyvars,Type,il),rep) | _ => die "pu_LambdaExp.CHECK_REML") - (Pickle.tup4Gen0(Lvars.pu,pu_tyvars,pu_Type,Report.pu)) + (Pickle.pairGen0(Pickle.tup4Gen0(Lvars.pu,pu_tyvars,pu_Type,Pickle.listGen pu_Type),Report.pu)) in Pickle.dataGen("LambdaExp.LambdaExp",toInt,[fun_VAR, fun_INTEGER, @@ -1914,7 +1918,7 @@ structure LambdaExp : LAMBDA_EXP = | TYPED (e,tau,_) => tyvars_Type s tau (tyvars_Exp s e acc) | PRIM(p,es) => tyvars_Exps s es (tyvars_Prim s p acc) | FRAME fr => tyvars_Frame s fr acc - | CHECK_REML {lvar,tyvars,Type,rep= _} => tyvars_Scheme s (tyvars, Type) acc + | CHECK_REML {lvar,tyvars,Type,il,rep= _} => tyvars_Types s il (tyvars_Scheme s (tyvars, Type) acc) end and tyvars_Exps s nil acc = acc diff --git a/src/Compiler/Lambda/LambdaStatSem.sml b/src/Compiler/Lambda/LambdaStatSem.sml index 166f2317b..42fba4c8d 100644 --- a/src/Compiler/Lambda/LambdaStatSem.sml +++ b/src/Compiler/Lambda/LambdaStatSem.sml @@ -994,8 +994,10 @@ structure LambdaStatSem: LAMBDA_STAT_SEM = Frame {declared_lvars = map on_lvar declared_lvars, declared_excons = map on_excon declared_excons} end - | CHECK_REML {lvar,tyvars,Type,rep= _} => + | CHECK_REML {lvar,tyvars,Type,il,rep= _} => let val sigma = lookup_lvar env lvar + val tau = mk_instance(sigma,il) + val sigma = (tyvars,tau) in eqSigma "CHECK_REML" (sigma,(tyvars,Type)) ; Types nil end diff --git a/src/Compiler/Regions/EFFECT.sig b/src/Compiler/Regions/EFFECT.sig index 04c8ebae8..3e399c78e 100644 --- a/src/Compiler/Regions/EFFECT.sig +++ b/src/Compiler/Regions/EFFECT.sig @@ -144,7 +144,9 @@ signature EFFECT = sig val freshRho : cone -> effect * cone val freshRhos : place list * cone -> place list * cone - val freshRhosPreserveRT: place list * cone -> place list * cone + val freshRhosPreserveRT : place list * cone -> place list * cone + val freshRhosPreserveRTandExplicit : place list * cone -> place list * cone + val renameRhos : place list * cone -> place list * cone (* fresh variables, preserve runtime types and pix *) val cloneRhos : place list * cone -> place list * cone (* fresh variables, diff --git a/src/Compiler/Regions/Effect.sml b/src/Compiler/Regions/Effect.sml index 5c250644a..cf720458b 100644 --- a/src/Compiler/Regions/Effect.sml +++ b/src/Compiler/Regions/Effect.sml @@ -876,6 +876,12 @@ struct fun freshRhoRegVar (B,rv) = freshRho0 (SOME rv) B end + fun getRegVar (place:place) : RegVar.regvar option = + case G.find_info place of + RHO{explicit,...} => explicit + | EPS{explicit,...} => explicit + | _ => die "getRegVar: node is not a region variable or an effect variable" + fun insertRho rho (cone as (n,c)) = add(rho,n, key_of_rho rho, cone) fun insertEps eps (cone as (n,c)) = add(eps,n, get_key_of_eps eps, cone) @@ -929,30 +935,43 @@ struct log_tree(layout_effect_deep eps); die "renameEpss: not an effect variable") ) ([],c) epss - fun renameEpss (epss, c: cone as (n,_)) : effect list * cone = - rename_epss_aux(epss,c,fn(ref int) => int, fn(ref int) => int) - fun cloneEpss (epss, c: cone as (n,_)) : effect list * cone = - rename_epss_aux(epss,c,fn(ref int) => ~1, fn _ => n) + fun renameEpss (epss, B:cone) : effect list * cone = + rename_epss_aux(epss,B,fn (ref i) => i, fn (ref i) => i) + + fun cloneEpss (epss, B:cone as (n,_)) : effect list * cone = + rename_epss_aux(epss,B,fn _ => ~1, fn _ => n) - fun freshRhoWithTy (rt: runType, cone:cone as (n, c)): effect * cone = + fun freshRhoExplicitWithTy (rt:runType, explicit:regvar option, B:cone as (n,_)): effect * cone = let val key = freshRhoInt() val node = G.mk_node(RHO{key = ref key, level = ref n, put = NONE, get = NONE, mut = NONE, instance = ref NONE, pix = ref ~1, ty = rt, - explicit=NONE,protected=ref 0,constraints=ref nil}) - in (node, add(node, n, key, cone)) + explicit=explicit,protected=ref 0,constraints=ref nil}) + in (node, add(node, n, key, B)) end - fun freshRhosPreserveRT (rhos,c: cone): effect list * cone = - foldr (fn (rho,(rhos',c)) => + fun freshRhoWithTy (rt:runType,B:cone) : effect * cone = + freshRhoExplicitWithTy (rt, NONE, B) + + fun freshRhosPreserveRT (rhos,B:cone) : effect list * cone = + foldr (fn (rho,(rhos',B)) => (case get_place_ty rho of NONE => die "freshRhosPreserveRT" | SOME rt => - let val (rho',c) = freshRhoWithTy(rt, c) - in (rho'::rhos',c) - end)) ([],c) rhos + let val (rho',B) = freshRhoWithTy(rt, B) + in (rho'::rhos',B) + end)) ([],B) rhos - fun setRunType (place:place) (rt: runType) : unit = + fun freshRhosPreserveRTandExplicit (rhos,B:cone) : effect list * cone = + foldr (fn (rho,(rhos',B)) => + (case get_place_ty rho of + NONE => die "freshRhosPreserveRT" + | SOME rt => + let val (rho',B) = freshRhoExplicitWithTy(rt, getRegVar rho, B) + in (rho'::rhos',B) + end)) ([],B) rhos + + fun setRunType (place:place) (rt:runType) : unit = case G.find_info place of RHO{put,get,mut,key,level,instance,pix,ty,explicit,protected,constraints} => G.set_info place (RHO{put=put,get=get,mut=mut,key=key,level=level,instance=instance, @@ -960,12 +979,6 @@ struct constraints=constraints}) | _ => die "setRunType: node is not a region variable" - fun getRegVar (place:place) : RegVar.regvar option = - case G.find_info place of - RHO{explicit,...} => explicit - | EPS{explicit,...} => explicit - | _ => die "getRegVar: node is not a region variable or an effect variable" - (* freshEps(cone): Generate a fresh effect variable at the topmost layer of cone and insert it in this topmost layer *) diff --git a/src/Compiler/Regions/SpreadExpression.sml b/src/Compiler/Regions/SpreadExpression.sml index 69e2da65e..afec7e6cb 100644 --- a/src/Compiler/Regions/SpreadExpression.sml +++ b/src/Compiler/Regions/SpreadExpression.sml @@ -385,20 +385,35 @@ struct val (freshType, freshMu) = R.freshType lookup_tn (RSE.lookupRegVar rse) deepError - fun freshType' regvars_with_rhos = + fun freshType' regvars_rhos = let val rse = List.foldl (fn ((rv,rho),rse) => RSE.declareRegVar(rv,rho,rse)) - rse regvars_with_rhos + rse regvars_rhos val (freshTy, _) = R.freshType lookup_tn (RSE.lookupRegVar rse) deepError in freshTy end - fun freshTypesWithPlaces (cone:cone, types: E.Type list) = + fun freshMu' regvars_rhos = + let val rse = List.foldl (fn ((rv,rho),rse) => RSE.declareRegVar(rv,rho,rse)) + rse regvars_rhos + val (_, freshMu) = R.freshType lookup_tn (RSE.lookupRegVar rse) deepError + in freshMu + end + + fun freshMus' regvars_rhos (B:cone,types:E.Type list) = + case types of + [] => ([],B) + | tau::rest => let val (mu, B) = freshMu' regvars_rhos (tau,B) + val (mus, B) = freshMus' regvars_rhos (B, rest) + in (mu::mus, B) + end + + fun freshTypesWithPlaces (B:cone, types: E.Type list) = case types of - [] => ([],cone) - | (tau_ml::rest) => let val (mu, cone) = freshMu(tau_ml,cone) - val (mus, cone) = freshTypesWithPlaces(cone, rest) - in (mu::mus, cone) - end + [] => ([],B) + | tau::rest => let val (mu, B) = freshMu(tau,B) + val (mus, B) = freshTypesWithPlaces(B, rest) + in (mu::mus, B) + end fun enforceConstraint rse = R.enforceConstraint (RSE.lookupRegVar rse) deepError @@ -1524,10 +1539,38 @@ good *) NOTAIL, []) end - | E.CHECK_REML {lvar,tyvars,Type,rep} => - let val (compound,create_region_record,regvars,sigma,p,_,_) = + | E.CHECK_REML {lvar,tyvars,Type,il,rep} => + let val (compound,create_region_record,regvars,sigma0,p,_,_) = noSome (RSE.lookupLvar rse lvar) "declared lvar of CHECK_REML not in scope" + fun instFresh {preserve_explicit:bool} (sigma,mus) B = + let val (rhos,epss,_,_) = R.un_scheme sigma + val (rhos',B) = + if preserve_explicit then Eff.freshRhosPreserveRTandExplicit (rhos,B) + else Eff.freshRhosPreserveRT (rhos,B) + val (epss',B) = Eff.freshEpss (epss,B) + val il = R.mk_il (rhos',epss',mus) + in R.inst (NONE,sigma,il) B + end (*handle X => (print "instFresh\n"; raise X)*) + + (* The sigma in the environment is the sigma for the declared variable + lvar. However, the view application code has on this lvar may have + been (partially) refined by enrichment (sigmature matching), which is + witnessed through the instantiation list il. Thus, to create the sigma + to check against, we first instantiate sigma with a freshly spreaded + version of il and then create the modified sigma by generalizing over + all free variables (type variables are taken from sigma')... *) + + val (B,sigma) = + let val level = Eff.level B + val B = Eff.push B + val (regvars_rhos,B) = fresh_regvars_with_rhos (B,E.regvarsTypes il) + val (mus,B) = freshMus' regvars_rhos (B,il) + val (t,B) = instFresh {preserve_explicit=true} (sigma0,mus) B + val (B,sigma) = R.generalize_all(B,level,map (fn tv => (tv,NONE)) tyvars,t) + in (#2(Eff.pop B),sigma) + end + val (B,sigma') = let val level = Eff.level B val B = Eff.push B @@ -1540,29 +1583,23 @@ good *) (* Two checks: (1) unify (instance sigma, tauOf sigma') - (2) unify (tauOf sigma, instance sigma') + (2) unify (instance sigma', tauOf sigma0) *) - fun instFresh (sigma,tvs) B = - let val tvs = map #1 tvs - val (rhos,epss,_,_) = R.un_scheme sigma - val (rhos',B) = Eff.freshRhosPreserveRT (rhos,B) - val (epss',B) = Eff.freshEpss (epss,B) - val il = R.mk_il (rhos',epss',map R.mkTYVAR tvs) - in R.inst (NONE,sigma,il) B - end (*handle X => (print "instFresh\n"; raise X)*) fun check str s s' B = let (* - val () = ( print ("IN " ^ str ^ "\n") + val () = ( print ("IN " ^ str ^ "\ns=") ; print_sigma s - ; print "\n" + ; print "\ns'=" ; print_sigma s' + ; print "\ns0=" + ; print_sigma sigma0 ; print "\n" ) - *) + *) val (_,_,tvs',t') = R.un_scheme s' val B = Eff.push B - val (t,B) = instFresh (s,tvs') B + val (t,B) = instFresh {preserve_explicit=false} (s,map R.mkTYVAR (map #1 tvs')) B val B = R.unify_ty (t',t) B val (_,B) = Eff.pop B in B diff --git a/test/explicit_regions/Makefile b/test/explicit_regions/Makefile index 7500fd0d5..e1eac3265 100644 --- a/test/explicit_regions/Makefile +++ b/test/explicit_regions/Makefile @@ -3,7 +3,7 @@ REML=../../bin/reml $(FLAGS) SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expty1.sml err_expty2.sml \ err_expty3.sml err_patty1.sml err_funty1.sml err_funty2.sml err_funty3.sml expty1.sml expty2.sml \ - disputs.sml disputs2.sml server.sml mod.sml mod2.sml mod3.sml + disputs.sml disputs2.sml server.sml mod.sml mod2.sml mod3.sml mod4.sml mod5.sml .PHONY: all all: diff --git a/test/explicit_regions/all.tst b/test/explicit_regions/all.tst index d4da1130d..b292d8400 100644 --- a/test/explicit_regions/all.tst +++ b/test/explicit_regions/all.tst @@ -86,6 +86,8 @@ par.sml nobasislib noopt (* A sound implementation of pa par-no.sml ccl ecte nobasislib noopt (* But it needs to be satisfied *) par-no2.sml ccl ecte nobasislib noopt (* The trivial definition of par is not ok *) -mod.sml ccl ecte (* Transparent signature matching: spec type at least as general as impl type *) -mod2.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) -mod3.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) +mod.sml ccl ecte (* Transparent signature matching: spec type at least as general as impl type *) +mod2.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) +mod3.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *) +mod4.sml ccl ecte +mod5.sml (* ok matching *) \ No newline at end of file diff --git a/test/explicit_regions/mod3.sml.log.ok b/test/explicit_regions/mod3.sml.log.ok index 705c777f5..a0753b7b7 100644 --- a/test/explicit_regions/mod3.sml.log.ok +++ b/test/explicit_regions/mod3.sml.log.ok @@ -15,7 +15,7 @@ mod3.sml, line 12, column 15: structure K2 = K1 : X ^^^^^^ The implementation type - val f : all r15.(string,r15)->(string,r15) + val f : all r19.(string,r19)->(string,r19) is not as general as the specified type val f : all `r2,`r1.(string,`r1)->(string,`r2) Please modify either the implementation or the specification. diff --git a/test/explicit_regions/mod4.sml b/test/explicit_regions/mod4.sml new file mode 100644 index 000000000..bac545450 --- /dev/null +++ b/test/explicit_regions/mod4.sml @@ -0,0 +1,13 @@ +(* Transparent signature matching: It is checked that the type of an implementation + * is at least as general as the specified type. In this test, the implementation + * is more general than the specification, also from an ML-type perspective. *) + +signature X = sig + val f : string`r1 -> string`r2 +end + +structure K1 = struct + fun f a = a +end + +structure K2 = K1 : X diff --git a/test/explicit_regions/mod4.sml.log.ok b/test/explicit_regions/mod4.sml.log.ok new file mode 100644 index 000000000..94689fb55 --- /dev/null +++ b/test/explicit_regions/mod4.sml.log.ok @@ -0,0 +1,26 @@ +[reading source file: mod4.sml] +> signature X = + sig + val f : string`r1 -> string`r2 + end + structure K1 : + sig + val f : 'a -> 'a + end + structure K2 : + sig + val f : string`r1 -> string`r2 + end +mod4.sml, line 13, column 15: + structure K2 = K1 : X + ^^^^^^ +The implementation type + val f : all `r1.(string,`r1)->(string,`r1) +is not as general as the specified type + val f : all `r2,`r1.(string,`r1)->(string,`r2) +Please modify either the implementation or the specification. +mod4.sml, line 6, column 30: + val f : string`r1 -> string`r2 + ^^ +Cannot unify the explicit region variables `r2 and `r1 +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/mod5.sml b/test/explicit_regions/mod5.sml new file mode 100644 index 000000000..545945ca3 --- /dev/null +++ b/test/explicit_regions/mod5.sml @@ -0,0 +1,15 @@ +(* Transparent signature matching: It is checked that the type of an implementation + * is at least as general as the specified type. In this test, the implementation + * satisfies the specification. *) + +signature X = sig + val f : string`r1 -> string`r1 +end + +structure K1 = struct + fun f (a:string) = a +end + +structure K2 = K1 : X + +val () = print (K2.f "Hello" ^ " World\n") diff --git a/test/explicit_regions/mod5.sml.out.ok b/test/explicit_regions/mod5.sml.out.ok new file mode 100644 index 000000000..557db03de --- /dev/null +++ b/test/explicit_regions/mod5.sml.out.ok @@ -0,0 +1 @@ +Hello World