REML signature matching

.github/workflows/main.yml

@@ -44,12 +44,12 @@ jobs:
       - name: Install dependencies (linux)
         if: ${{ env.OS == 'linux' }}
         run: |
-          # sudo apt-get -qq update
+          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://bitbucket.org/ariya/phantomjs/downloads/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 ..
@@ -135,8 +135,8 @@ jobs:
         timeout-minutes: 240
         run: |
           gcc --version
-          make mlkit
-          make mlkit_basislibs
+          make mlkit VERBOSE=1
+          make mlkit_basislibs VERBOSE=1
 
       - name: Install MLKit
         run: |

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

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

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

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

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

src/Common/STATOBJECT.sml

@@ -300,4 +300,4 @@ signature STATOBJECT =
 	val tynamesRng              : realisation -> TyName.Set.Set
       end (*Realisation*)
 
-  end;
+  end

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

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 * Type list) list
 
     (* compileTypeScheme is used by constrain *)
     val set_compileTypeScheme : (TypeScheme -> tyvar list * Type) -> unit   (* MEGA HACK *)

src/Compiler/Lambda/CompileDec.sml

@@ -3543,8 +3543,23 @@ 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,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"
          | APPstrexp(i,funid,strexp) =>
@@ -3562,14 +3577,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

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',il')]
+                                     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

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

src/Compiler/Lambda/LAMBDA_EXP.sml

@@ -82,6 +82,10 @@ signature LAMBDA_EXP =
     val stringType      : Type
     val chararrayType   : Type
 
+    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. *)
       | Frame of {declared_lvars: {lvar : lvar, tyvars: tyvar list, Type: Type} list,
@@ -121,25 +125,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 +155,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, 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