From 6828a266b8ee64338e663a2018ceb13a3d8073a2 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Sat, 14 Feb 2026 11:35:20 +0100 Subject: [PATCH 1/3] fix optimiser --- src/Compiler/Lambda/OptLambda.sml | 23 +++++++++++++++++++++-- test/all.tst | 13 +++++++------ test/stringconcat.sml | 6 ++++++ test/stringconcat.sml.out.ok | 1 + 4 files changed, 35 insertions(+), 8 deletions(-) create mode 100644 test/stringconcat.sml create mode 100644 test/stringconcat.sml.out.ok diff --git a/src/Compiler/Lambda/OptLambda.sml b/src/Compiler/Lambda/OptLambda.sml index 3277dc6a..02b2d833 100644 --- a/src/Compiler/Lambda/OptLambda.sml +++ b/src/Compiler/Lambda/OptLambda.sml @@ -3535,6 +3535,14 @@ structure OptLambda : OPT_LAMBDA = declared_excons=declared_excons} ) end + | CHECK_REML{lvar,tyvars,Type,il,rep} => + (case Lvars.Map.lookup phi lvar of + NONE => die "flt.look.CHECK_REML" + | SOME NOFIXphi => e + | SOME (FIXphi(t,_,_)) => + let val Type = on_ty t Type + in CHECK_REML{lvar=lvar,tyvars=tyvars,Type=Type,il=il,rep=rep} + end) | _ => LambdaBasics.map_lamb (flt phi) e in (flt phi e, case !framephi of @@ -3543,6 +3551,10 @@ structure OptLambda : OPT_LAMBDA = ) end + (* noOpt is used when the optimiser is disabled *) + fun noOpt phi e = + flatten (fn {phi,function,mutrec} => (function,Id,fn x => x)) phi e + fun dropOpt (phi:phi) (e:LambdaExp) : LambdaExp * phi = let fun F {phi:phi,function={lvar,regvars,tyvars,Type,constrs,vtys,body},mutrec} = let val vs0 = if mutrec @@ -3740,6 +3752,12 @@ structure OptLambda : OPT_LAMBDA = in (e, phi_mod(phi_mod(phi1,phi2),phi3)) end + fun flattening_noopt phi e = + let val () = log "flattening - noopt\n" + val (e',phi') = noOpt phi e + in (e',phi') + end + (* Pickling *) val pu_t = let fun toInt t = @@ -4081,14 +4099,15 @@ structure OptLambda : OPT_LAMBDA = in (lamb, (inveta_env, let_env)) end - (* ----------------------------------------------------------------- * The Optimiser * ----------------------------------------------------------------- *) fun maybeoptimise cenv phi e = if optimise_p() then optimise cenv phi e - else (e, contract_env_dummy e, FixFlatten.dummy_phi e) + else let val (e',phi') = FixFlatten.flattening_noopt phi e + in (e', contract_env_dummy e', phi') + end fun optimise (env, PGM(DATBINDS db,lamb)) = let val (env1,env2,phi,cenv) = env diff --git a/test/all.tst b/test/all.tst index 29d8e182..4ab46f40 100644 --- a/test/all.tst +++ b/test/all.tst @@ -7,7 +7,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 @@ -67,10 +67,10 @@ elabDecBug.sml ccl ecte oh-no.sml ccl nobasislib oh-no2.sml ccl nobasislib real_match.sml nobasislib -gc0.sml nobasislib nooptimiser -gc01.sml nobasislib nooptimiser -exn.sml nobasislib nooptimiser -exn-alpha.sml nobasislib nooptimiser +gc0.sml nobasislib noopt +gc01.sml nobasislib noopt +exn.sml nobasislib noopt +exn-alpha.sml nobasislib noopt (* Tests of some benchmark programs *) @@ -182,4 +182,5 @@ auto2.sml (* ffi auto-conversion *) foldbug.sml seltuptup.sml poll.sml -enum-eq.sml \ No newline at end of file +enum-eq.sml +stringconcat.sml noopt (* check transformation of calls to argument-transformed functions *) \ No newline at end of file diff --git a/test/stringconcat.sml b/test/stringconcat.sml new file mode 100644 index 00000000..32a3791e --- /dev/null +++ b/test/stringconcat.sml @@ -0,0 +1,6 @@ +(* Check that even when the optimiser is disabled (-no_opt), calls to +argument-transformed functions are still transformed... *) + +val s = "Hello" ^ " world\n" + +val () = print s diff --git a/test/stringconcat.sml.out.ok b/test/stringconcat.sml.out.ok new file mode 100644 index 00000000..802992c4 --- /dev/null +++ b/test/stringconcat.sml.out.ok @@ -0,0 +1 @@ +Hello world From 05ff3bbb64b4641516606f8c7630ba180ae316b8 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Sat, 14 Feb 2026 17:36:06 +0100 Subject: [PATCH 2/3] cleanup --- test/parallelism/all.tst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/parallelism/all.tst b/test/parallelism/all.tst index b3a22031..a6cfaf63 100644 --- a/test/parallelism/all.tst +++ b/test/parallelism/all.tst @@ -7,7 +7,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 From ae4ef98d0a3610c35b4fe751e41433a74c58ab06 Mon Sep 17 00:00:00 2001 From: Martin Elsman Date: Mon, 16 Feb 2026 09:24:07 +0100 Subject: [PATCH 3/3] fixes --- src/Compiler/Regions/SpreadExpression.sml | 88 +++++++++++++---------- test/explicit_regions/all.tst | 18 +++-- test/explicit_regions/mod.sml | 4 +- test/explicit_regions/mod.sml.log.ok | 4 +- test/explicit_regions/mod2.sml | 4 +- test/explicit_regions/mod2.sml.log.ok | 10 +-- test/explicit_regions/mod3.sml | 4 +- test/explicit_regions/mod3.sml.log.ok | 4 +- test/explicit_regions/mod4.sml | 9 ++- test/explicit_regions/mod4.sml.log.ok | 8 +-- test/explicit_regions/mod6.sml | 14 ++++ test/explicit_regions/mod6.sml.log.ok | 22 ++++++ test/explicit_regions/mod7.sml | 15 ++++ test/explicit_regions/mod7.sml.log.ok | 22 ++++++ 14 files changed, 158 insertions(+), 68 deletions(-) create mode 100644 test/explicit_regions/mod6.sml create mode 100644 test/explicit_regions/mod6.sml.log.ok create mode 100644 test/explicit_regions/mod7.sml create mode 100644 test/explicit_regions/mod7.sml.log.ok diff --git a/src/Compiler/Regions/SpreadExpression.sml b/src/Compiler/Regions/SpreadExpression.sml index afec7e6c..4f720673 100644 --- a/src/Compiler/Regions/SpreadExpression.sml +++ b/src/Compiler/Regions/SpreadExpression.sml @@ -1581,29 +1581,7 @@ good *) in (B,sigma') end handle X => (print "SIGMA'\n"; raise X) - (* Two checks: - (1) unify (instance sigma, tauOf sigma') - (2) unify (instance sigma', tauOf sigma0) - *) - - fun check str s s' B = - let (* - val () = ( print ("IN " ^ str ^ "\ns=") - ; print_sigma s - ; 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 {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 - end (*handle X => (print (str ^ "\n"); raise X)*) + infix // fun r // r' = Report.// (r,r') fun rep_sigma s = let val r = !Flags.print_types @@ -1614,30 +1592,62 @@ good *) before Flags.print_types := r end - infix // fun r // r' = Report.// (r,r') - val B = check "CHECK1" sigma sigma' B - handle Report.DeepError rep0 => + (* + val () = ( print ("CHECK_REML\ns=") + ; print_sigma sigma + ; print "\ns'=" + ; print_sigma sigma' + ; print "\ns0=" + ; print_sigma sigma0 + ; print "\n" + ) + *) + + (* Two checks: + (1) unify (instance sigma, tauOf sigma'): + Implementation does not unify regions and effects that + are specified to be disjoint. + (2) sigma = unifySigma (fresh sigma, fresh sigma'): + Signature type should have no influence on the + implementation type. + *) + + fun check1 B = + let val (_,_,tvs',t') = R.un_scheme sigma' + val B = Eff.push B + val (t,B) = instFresh {preserve_explicit=false} (sigma,map R.mkTYVAR (map #1 tvs')) B + val B = R.unify_ty (t',t) B + val (_,B) = Eff.pop B + in B + end handle Report.DeepError rep0 => raise Report.DeepError ( rep - // Report.line "The implementation type " + // Report.line "The implementation type" // rep_sigma sigma - // Report.line "is not as general as the specified type" + // Report.line "is less general than the specified type" // rep_sigma sigma' // Report.line "Please modify either the implementation or the specification." // rep0 ) + fun check2 B = + let val s = R.alpha_rename (sigma,B) + val (_,_,_,t) = R.un_scheme s + val s' = R.alpha_rename (sigma',B) + val (_,_,_,t') = R.un_scheme s' + val B = R.unify_ty(t,t')B + in if R.alpha_equal (sigma,s) B then B + else raise Report.DeepError + ( rep + // Report.line "The specification type" + // rep_sigma sigma' + // Report.line "is less general than the implementation type" + // rep_sigma sigma + // Report.line "Please modify either the implementation or the specification." + ) + end - 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 - ) + val B = check1 B + val B = check2 B in (B, E'.TR(E'.UB_RECORD nil, E'.Mus nil, diff --git a/test/explicit_regions/all.tst b/test/explicit_regions/all.tst index b292d840..ce8776d5 100644 --- a/test/explicit_regions/all.tst +++ b/test/explicit_regions/all.tst @@ -86,8 +86,16 @@ 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 *) -mod4.sml ccl ecte -mod5.sml (* ok matching *) \ No newline at end of file +mod.sml ccl ecte (* Signature matching: It is an error if the implementation + type is less general than the specified type. *) +mod2.sml ccl ecte (* Signature matching: It is an error if the specified + type is less general than the implementation type. *) +mod3.sml ccl ecte (* Signature matching: It is an error if the implementation type + is less general than the specified type. *) +mod4.sml ccl ecte (* Signature matching: It is an error if the implementation type + is less general than the specified type (enrichment). *) +mod5.sml (* Signature matching: ok. *) +mod6.sml ccl ecte (* Signature matching: It is an error if the specification type + is less general than the implementation type. *) +mod7.sml ccl ecte (* Signature matching: It is an error if the specification type + is less general than the implementation type. *) \ No newline at end of file diff --git a/test/explicit_regions/mod.sml b/test/explicit_regions/mod.sml index 8e4fd51a..4f5407f1 100644 --- a/test/explicit_regions/mod.sml +++ b/test/explicit_regions/mod.sml @@ -1,5 +1,5 @@ -(* Transparent signature matching: It is checked that the type of an implementation - * is at least as general as the specified type. *) +(* Transparent signature matching: It is an error if the implementation + type is less general than the specified type. *) signature X = sig val f : string`r1 -> string`r2 diff --git a/test/explicit_regions/mod.sml.log.ok b/test/explicit_regions/mod.sml.log.ok index 4549e2b2..ad9d627d 100644 --- a/test/explicit_regions/mod.sml.log.ok +++ b/test/explicit_regions/mod.sml.log.ok @@ -14,9 +14,9 @@ mod.sml, line 12, column 15: structure K2 = K1 : X ^^^^^^ -The implementation type +The implementation type val f : all `r1.(string,`r1)->(string,`r1) -is not as general as the specified type +is less general than 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: diff --git a/test/explicit_regions/mod2.sml b/test/explicit_regions/mod2.sml index 39bf70c9..1180b557 100644 --- a/test/explicit_regions/mod2.sml +++ b/test/explicit_regions/mod2.sml @@ -1,5 +1,5 @@ -(* Transparent signature matching: It is checked that an explicitly specified - * type is at least as general as the implementation. *) +(* Transparent signature matching: It is an error if the specified + type is less general than the implementation type. *) signature X = sig val f : string`r1 -> string`r1 diff --git a/test/explicit_regions/mod2.sml.log.ok b/test/explicit_regions/mod2.sml.log.ok index bffe5926..dfcc57df 100644 --- a/test/explicit_regions/mod2.sml.log.ok +++ b/test/explicit_regions/mod2.sml.log.ok @@ -14,13 +14,9 @@ mod2.sml, line 12, column 15: structure K2 = K1 : X ^^^^^^ -The specified type +The specification type val f : all `r1.(string,`r1)->(string,`r1) -is not as general as the implementation type +is less general than 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 +Please modify either the implementation or the specification. Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/mod3.sml b/test/explicit_regions/mod3.sml index d722bb45..663465d9 100644 --- a/test/explicit_regions/mod3.sml +++ b/test/explicit_regions/mod3.sml @@ -1,5 +1,5 @@ -(* Transparent signature matching: It is checked that the type of an implementation - * is at least as general as the specified type. *) +(* Transparent signature matching: It is an error if the implementation type + is less general than the specified type. *) signature X = sig val f : string`r1 -> string`r2 diff --git a/test/explicit_regions/mod3.sml.log.ok b/test/explicit_regions/mod3.sml.log.ok index a0753b7b..34d589db 100644 --- a/test/explicit_regions/mod3.sml.log.ok +++ b/test/explicit_regions/mod3.sml.log.ok @@ -14,9 +14,9 @@ mod3.sml, line 12, column 15: structure K2 = K1 : X ^^^^^^ -The implementation type +The implementation type val f : all r19.(string,r19)->(string,r19) -is not as general as the specified type +is less general than 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: diff --git a/test/explicit_regions/mod4.sml b/test/explicit_regions/mod4.sml index bac54545..ed57c388 100644 --- a/test/explicit_regions/mod4.sml +++ b/test/explicit_regions/mod4.sml @@ -1,6 +1,9 @@ -(* 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. *) +(* Transparent signature matching: It is an error if the implementation type is + less general than the specified type. In this test, from an ML-type + perspective, the implementation is more general than the specification, but, + from a region-and-effect perspective, the instantiated implementation type + scheme (\/r.string`r -> string`r) is less general than the specified + type (\/r1,r2.string`r1 -> string`r2). *) signature X = sig val f : string`r1 -> string`r2 diff --git a/test/explicit_regions/mod4.sml.log.ok b/test/explicit_regions/mod4.sml.log.ok index 94689fb5..8af7744c 100644 --- a/test/explicit_regions/mod4.sml.log.ok +++ b/test/explicit_regions/mod4.sml.log.ok @@ -11,15 +11,15 @@ sig val f : string`r1 -> string`r2 end -mod4.sml, line 13, column 15: +mod4.sml, line 16, column 15: structure K2 = K1 : X ^^^^^^ -The implementation type +The implementation type val f : all `r1.(string,`r1)->(string,`r1) -is not as general as the specified type +is less general than 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: +mod4.sml, line 9, column 30: val f : string`r1 -> string`r2 ^^ Cannot unify the explicit region variables `r2 and `r1 diff --git a/test/explicit_regions/mod6.sml b/test/explicit_regions/mod6.sml new file mode 100644 index 00000000..9a111fb8 --- /dev/null +++ b/test/explicit_regions/mod6.sml @@ -0,0 +1,14 @@ +(* Transparent signature matching: It is an error if the specification type is less + * general than the implementation type. *) + +signature X = sig + val concat : string`r1 * string`r1 -> string`r1 +end + +structure K1 = struct + fun concat (s1,s2) = s1 ^ s2 +end + +structure K2 = K1 : X + +val () = print (K2.concat("Hello"," World\n")) diff --git a/test/explicit_regions/mod6.sml.log.ok b/test/explicit_regions/mod6.sml.log.ok new file mode 100644 index 00000000..6e5b4c61 --- /dev/null +++ b/test/explicit_regions/mod6.sml.log.ok @@ -0,0 +1,22 @@ +[reading source file: mod6.sml] +> signature X = + sig + val concat : string`r1 * string`r1 -> string`r1 + end + structure K1 : + sig + val concat : string * string -> string + end + structure K2 : + sig + val concat : string`r1 * string`r1 -> string`r1 + end +mod6.sml, line 12, column 15: + structure K2 = K1 : X + ^^^^^^ +The specification type + val concat : all `r1.<(string,`r1), (string,`r1)>->(string,`r1) +is less general than the implementation type + val concat : all r33,r31,r29.<(string,r29), (string,r31)>->(string,r33) +Please modify either the implementation or the specification. +Stopping compilation of MLB-file due to error (code 1). diff --git a/test/explicit_regions/mod7.sml b/test/explicit_regions/mod7.sml new file mode 100644 index 00000000..1d3d70d7 --- /dev/null +++ b/test/explicit_regions/mod7.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/mod7.sml.log.ok b/test/explicit_regions/mod7.sml.log.ok new file mode 100644 index 00000000..3dcd5599 --- /dev/null +++ b/test/explicit_regions/mod7.sml.log.ok @@ -0,0 +1,22 @@ +[reading source file: mod7.sml] +> signature X = + sig + val f : string`r1 -> string`r1 + end + structure K1 : + sig + val f : string -> string + end + structure K2 : + sig + val f : string`r1 -> string`r1 + end +mod7.sml, line 13, column 15: + structure K2 = K1 : X + ^^^^^^ +The specification type + val f : all `r1.(string,`r1)->(string,`r1) +is less general than the implementation type + val f : all r29,r27.(string,r27)->(string,r29) +Please modify either the implementation or the specification. +Stopping compilation of MLB-file due to error (code 1).