ProbTime external updates (#802)

* Update external interface for ProbTime

* Remove batched inference external

* Add rt library dependency

* Fix performance issue in toRope

* Fix reversed order of toRope

* Retry running GitHub actions

* Make it more convenient to add built-in types

* Remove unused but problematic dependency

* Improve matching in peval

* Add empty old empty environment alias to not break DSLs

---------

Co-authored-by: Oscar Eriksson <oerikss@kth.se>

src/main/accelerate.mc

@@ -79,7 +79,7 @@ lang MExprCudaCompile =
 end
 
 let keywordsSymEnv =
-  {symEnvEmpty with varEnv =
+  {symEnvDefault with varEnv =
     mapFromSeq
       cmpString
       (map (lam s. (s, nameSym s)) mexprExtendedKeywords)}

stdlib/c/compile.mc

@@ -1387,7 +1387,7 @@ use Test in
 let compile: CompileCOptions -> Expr -> CProg = lam opts. lam prog.
 
   -- Symbolize with empty environment
-  let prog = symbolizeExpr symEnvEmpty prog in
+  let prog = symbolizeExpr symEnvDefault prog in
 
   -- Type check and annotate
   let prog = typeCheck prog in

stdlib/ext/rtppl-ext.ext-ocaml.mc

@@ -3,7 +3,7 @@ include "ocaml/ast.mc"
 
 let tyts_ = tytuple_ [tyint_, tyunknown_]
 let impl = lam arg : {expr : String, ty : Type }.
-  [ { expr = arg.expr, ty = arg.ty, libraries = ["rtppl-support"], cLibraries = [] } ]
+  [ { expr = arg.expr, ty = arg.ty, libraries = ["rtppl-support"], cLibraries = ["rt"] } ]
 
 let timespec = otytuple_ [tyint_, tyint_]
 let readDistTy = lam ty. otyarray_ (otytuple_ [tyfloat_, ty])
@@ -39,12 +39,24 @@ let rtpplExtMap =
     ( "rtpplCloseFileDescriptor"
     , impl { expr = "Rtppl.close_file_descriptor"
            , ty = tyarrow_ tyint_ otyunit_ } ),
+    ( "rtpplReadInt"
+    , impl { expr = "Rtppl.read_int"
+           , ty = tyarrow_ tyint_ (otyarray_ (otytuple_ [timespec, tyint_])) } ),
+    ( "rtpplWriteInt"
+    , impl { expr = "Rtppl.write_int"
+           , ty = tyarrows_ [tyint_, otytuple_ [timespec, tyint_], otyunit_] } ),
     ( "rtpplReadFloat"
     , impl { expr = "Rtppl.read_float"
            , ty = tyarrow_ tyint_ (otyarray_ (otytuple_ [timespec, tyfloat_])) } ),
     ( "rtpplWriteFloat"
     , impl { expr = "Rtppl.write_float"
            , ty = tyarrows_ [tyint_, otytuple_ [timespec, tyfloat_], otyunit_] } ),
+    ( "rtpplReadIntRecord"
+    , impl { expr = "Rtppl.read_int_record"
+           , ty = tyarrows_ [tyint_, tyint_, otyarray_ (otytuple_ [timespec, tyunknown_])] } ),
+    ( "rtpplWriteIntRecord"
+    , impl { expr = "Rtppl.write_int_record"
+           , ty = tyarrows_ [tyint_, tyint_, otytuple_ [timespec, tyunknown_], otyunit_] } ),
     ( "rtpplReadDistFloat"
     , impl { expr = "Rtppl.read_dist_float"
            , ty = tyarrow_ tyint_ (otyarray_ (otytuple_ [timespec, readDistTy tyfloat_])) } ),
@@ -56,8 +68,5 @@ let rtpplExtMap =
            , ty = tyarrows_ [tyint_, tyint_, otyarray_ (otytuple_ [timespec, readDistTy tyunknown_])] } ),
     ( "rtpplWriteDistFloatRecord"
     , impl { expr = "Rtppl.write_dist_float_record"
-           , ty = tyarrows_ [tyint_, tyint_, otytuple_ [timespec, writeDistTy tyunknown_], otyunit_] } ),
-    ( "rtpplBatchedInference"
-    , impl { expr = "Rtppl.rtppl_batched_inference"
-           , ty = tyarrows_ [tyarrow_ otyunit_ tyunknown_, timespec, otylist_ tyunknown_] } )
+           , ty = tyarrows_ [tyint_, tyint_, otytuple_ [timespec, writeDistTy tyunknown_], otyunit_] } )
   ]

stdlib/ext/rtppl-ext.mc

@@ -23,11 +23,13 @@ external rtpplCloseFileDescriptor : Int -> ()
 type Opaque
 
 -- Writing and reading RTPPL data types to and from a given file descriptor.
+external rtpplReadInt : Int -> [(Timespec, Int)]
+external rtpplWriteInt : Int -> (Timespec, Int) -> ()
 external rtpplReadFloat : Int -> [(Timespec, Float)]
 external rtpplWriteFloat : Int -> (Timespec, Float) -> ()
+external rtpplReadIntRecord : Int -> Int -> [(Timespec, Opaque)]
+external rtpplWriteIntRecord : Int -> Int -> (Timespec, Opaque) -> ()
 external rtpplReadDistFloat : Int -> [(Timespec, [(Float, Float)])]
 external rtpplWriteDistFloat : Int -> (Timespec, ([Float], [Float])) -> ()
 external rtpplReadDistFloatRecord : Int -> Int -> [(Timespec, [(Float, Opaque)])]
 external rtpplWriteDistFloatRecord : Int -> Int -> (Timespec, ([Opaque], [Float])) -> ()
-
-external rtpplBatchedInference : (() -> Opaque) -> Timespec -> [Opaque]

stdlib/mexpr/keyword-maker.mc

@@ -11,7 +11,6 @@
 include "ast.mc"
 include "info.mc"
 include "error.mc"
-include "mexpr.mc"
 include "ast-builder.mc"
 include "eq.mc"
 
@@ -163,7 +162,7 @@ end
 
 -- A test fragment that is used to test the approach. This
 -- fragment can be used as a template when using the keyword maker.
-lang _testKeywordMaker = KeywordMaker + MExpr + MExprEq
+lang _testKeywordMaker = KeywordMaker + MExprEq
 
   -- Example terms that will be used to represent the values of the
   -- the keyword expressions (the new language constructs). The term

stdlib/mexpr/symbolize.mc

@@ -31,19 +31,29 @@ type SymEnv = {
   ignoreExternals: Bool
 }
 
-let symEnvEmpty = {
+let _symEnvEmpty = {
   varEnv = mapEmpty cmpString,
   conEnv = mapEmpty cmpString,
   tyVarEnv = mapEmpty cmpString,
-
-  -- Built-in type constructors
-  tyConEnv =
-  mapFromSeq cmpString (map (lam t. (t.0, nameNoSym t.0)) builtinTypes),
-
+  tyConEnv = mapEmpty cmpString,
   allowFree = false,
   ignoreExternals = false
 }
 
+let symEnvAddBuiltinTypes : all a. SymEnv -> [(String, a)] -> SymEnv
+  = lam env. lam tys. {
+    env with tyConEnv =
+      foldl (lam env. lam t. mapInsert t.0 (nameNoSym t.0) env) env.tyConEnv tys
+  }
+
+let symEnvDefault =
+  symEnvAddBuiltinTypes _symEnvEmpty builtinTypes
+
+-- TODO(oerikss, 2023-11-14): Change all DSLs that use this name for the
+-- symbolize environment to instead point to `symEnvDefault` and then
+-- remove this alias and rename `_symEnvEmpty` to `symEnvEmpty`.
+let symEnvEmpty = symEnvDefault
+
 lang SymLookup
   type LookupParams = {kind : String, info : [Info], allowFree : Bool}
 
@@ -125,13 +135,13 @@ lang Sym = Ast + SymLookup
   -- Symbolize with builtin environment
   sem symbolize =
   | expr ->
-    let env = symEnvEmpty in
+    let env = symEnvDefault in
     symbolizeExpr env expr
 
   -- Symbolize with builtin environment and ignore errors
   sem symbolizeAllowFree =
   | expr ->
-    let env = { symEnvEmpty with allowFree = true } in
+    let env = { symEnvDefault with allowFree = true } in
     symbolizeExpr env expr
 
   -- Add top-level identifiers (along the spine of the program) in `t`
@@ -509,7 +519,7 @@ utest isFullySymbolized (nulam_ x (nvar_ x)) with true in
 let testSymbolize = lam ast. lam testEqStr.
   let symbolizeCalls =
     [ symbolize
-    , symbolizeExpr {symEnvEmpty with allowFree = true}] in
+    , symbolizeExpr {symEnvDefault with allowFree = true}] in
   foldl
     (lam acc. lam symb.
       if acc then

stdlib/mexpr/type-check.mc

@@ -38,19 +38,33 @@ type TCEnv = {
   disableRecordPolymorphism: Bool
 }
 
-let _tcEnvEmpty = {
+let typcheckEnvEmpty = {
   varEnv = mapEmpty nameCmp,
   conEnv = mapEmpty nameCmp,
   tyVarEnv = mapEmpty nameCmp,
-  tyConEnv =
-  mapFromSeq nameCmp
-    (map (lam t: (String, [String]).
-      (nameNoSym t.0, (0, map nameSym t.1, tyvariant_ []))) builtinTypes),
-
+  tyConEnv = mapEmpty nameCmp,
   currentLvl = 0,
   disableRecordPolymorphism = true
 }
 
+let typecheckEnvAddBuiltinTypes : TCEnv -> [(String, [String])] -> TCEnv
+  = lam env. lam tys. {
+    env with
+    tyConEnv =
+      foldl
+        (lam env. lam t.
+          mapInsert (nameNoSym t.0) (0, map nameSym t.1, tyvariant_ []) env)
+        env.tyConEnv tys
+  }
+
+let typcheckEnvDefault =
+  typecheckEnvAddBuiltinTypes typcheckEnvEmpty builtinTypes
+
+-- TODO(oerikss, 2023-11-14): Change all DSLs that use this name for the
+-- type-check environment to instead point to `typcheckEnvDefault` and then
+-- remove this alias.
+let _tcEnvEmpty = typcheckEnvDefault
+
 let _insertVar = lam name. lam ty. lam env : TCEnv.
   {env with varEnv = mapInsert name ty env.varEnv}
 
@@ -444,7 +458,7 @@ lang TypeCheck = TCUnify + Generalize + RemoveMetaVar
   sem typeCheck : Expr -> Expr
   sem typeCheck =
   | tm ->
-    removeMetaVarExpr (typeCheckExpr _tcEnvEmpty tm)
+    removeMetaVarExpr (typeCheckExpr typcheckEnvDefault tm)
 
   -- Type check `expr' under the type environment `env'. The resulting
   -- type may contain unification variables and links.
@@ -994,8 +1008,8 @@ let typeOf = lam test : TypeTest.
   let tyEnv = mapFromSeq nameCmp bindings in
   unwrapTypes
     (tyTm
-       (typeCheckExpr {_tcEnvEmpty with varEnv = tyEnv}
-          (symbolizeExpr {symEnvEmpty with varEnv = symEnv} test.tm)))
+       (typeCheckExpr {typcheckEnvDefault with varEnv = tyEnv}
+          (symbolizeExpr {symEnvDefault with varEnv = symEnv} test.tm)))
 in
 
 let runTest =

stdlib/peval/ast.mc

@@ -5,6 +5,7 @@ include "mexpr/type-check.mc"
 include "mexpr/eval.mc"
 include "mexpr/info.mc"
 include "mexpr/eq.mc"
+include "mexpr/mexpr.mc"
 
 include "peval/peval.mc"
 include "error.mc"

stdlib/peval/peval.mc

@@ -434,7 +434,8 @@ lang ConstPEval = PEval + ConstEvalNoDefault
 end
 
 lang MatchPEval =
-  PEval + MatchEval + RecordAst + ConstAst + DataAst + SeqAst + NeverAst + VarAst
+  PEval + MatchEval + RecordAst + ConstAst + DataAst + SeqAst + NeverAst +
+  VarAst + NamedPat
 
   sem pevalBindThis =
   | TmMatch _ -> true
@@ -443,23 +444,36 @@ lang MatchPEval =
   | TmMatch r ->
     pevalBind ctx
       (lam target.
-        switch target
-        case t & TmNever _ then k t
-          -- TODO(oerikss, 2023-07-07): This check is not exhaustive, we must
-          -- probably redefine tryMatch and handle each particular pattern type.
-        case TmRecord _ | TmConst _ | TmConApp _ | TmSeq _ then
-          match tryMatch ctx.env target r.pat with Some env then
-            pevalBind { ctx with env = env } k r.thn
-          else pevalBind ctx k r.els
+        switch (target, tryMatch ctx.env target r.pat)
+        case (TmNever r, _) then TmNever r
+        case (_, Some env) then
+          pevalBind { ctx with env = env } k r.thn
+        case (!TmVar _, None _) then
+          pevalBind ctx k r.els
         case _ then
+          match freshPattern ctx.env r.pat with (env, pat) in
           let ctx = { ctx with recFlag = false } in
-          k (TmMatch {r with
-                      target = target,
-                      thn = pevalBind ctx (lam x. x) r.thn,
-                      els = pevalBind ctx (lam x. x) r.els
-          })
+          k (TmMatch { r with
+                       target = target,
+                       pat = pat,
+                       thn = pevalBind { ctx with env = env } (lam x. x) r.thn,
+                       els = pevalBind ctx (lam x. x) r.els })
         end)
       r.target
+
+  sem freshPattern : EvalEnv -> Pat -> (EvalEnv, Pat)
+  sem freshPattern env =
+  | PatNamed (r & {ident = PName name}) ->
+    let newname = nameSetNewSym name in
+    let newvar = TmVar {
+      ident = newname,
+      ty = r.ty,
+      info = r.info,
+      frozen = false
+    } in
+    (evalEnvInsert name newvar env,
+     PatNamed { r with ident = PName newname })
+  | p -> smapAccumL_Pat_Pat freshPattern env p
 end
 
 lang UtestPEval = PEval + UtestAst

stdlib/pmexpr/utils.mc

@@ -77,7 +77,7 @@ let typeCheckEnv = lam env : [(Name, Type)]. lam expr.
       (lam env. lam x : (Name, Type).
         match x with (id, ty) in
         _insertVar id ty env)
-      _tcEnvEmpty env in
+      typcheckEnvDefault env in
   removeMetaVarExpr (typeCheckExpr tcEnv expr)
 in
 

stdlib/seq.mc

@@ -36,7 +36,18 @@ utest eqSeq eqi [2] [1] with false
 
 -- Converting between List and Rope
 let toRope = lam seq.
-  createRope (length seq) (lam i. get seq i)
+  recursive let work = lam acc. lam seq.
+    match seq with [h] ++ t then
+      work (cons h acc) t
+    else
+      acc
+  in
+  if isRope seq then seq else
+  let s = work [] seq in
+  -- NOTE(larshum, 2023-10-24): The below line ensures the elements of the rope
+  -- are in the right order, and it also collapses the rope (to ensure
+  -- constant-time random access).
+  reverse s
 
 let toList = lam seq.
   createList (length seq) (lam i. get seq i)