optimiser: transform calls to imported functions also when optimisation is disabled

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

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,

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
+enum-eq.sml
+stringconcat.sml               noopt         (* check transformation of calls to argument-transformed functions *)

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 *)
+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. *)

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

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:

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

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).

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

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:

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

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

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"))

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).

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")

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).