🧩 [add-unused]: Eq and Ord instances for terms.

src/Eval.purs

@@ -24,11 +24,11 @@ import Lattice ((∧), erase, top)
 import Pretty (prettyP)
 import Primitive (intPair, string)
 import Trace (AppTrace(..), Trace(..), VarDef(..)) as T
-import Trace (AppTrace, ForeignTrace, ForeignTrace'(..), Match(..), Trace)
+import Trace (AppTrace, ForeignTrace(..), ForeignTrace'(..), Match(..), Trace)
 import Util (type (×), absurd, both, check, error, orElse, successful, throw, with, (×))
 import Util.Pair (unzip) as P
 import Val (Fun(..), Val(..)) as V
-import Val (class Ann, DictRep(..), Env, ForeignOp'(..), MatrixRep(..), (<+>), Val, for, lookup', restrict)
+import Val (class Ann, DictRep(..), Env, ForeignOp(..), ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>))
 
 patternMismatch :: String -> String -> String
 patternMismatch s s' = "Pattern mismatch: found " <> s <> ", expected " <> s'
@@ -77,7 +77,7 @@ apply (V.Fun β (V.Closure γ1 ρ σ) × v) = do
    γ3 × e'' × β' × w <- match v σ
    t'' × v'' <- eval (γ1 <+> γ2 <+> γ3) (asExpr e'') (β ∧ β')
    pure $ T.AppClosure (S.fromFoldable (keys ρ)) w t'' × v''
-apply (V.Fun α (V.Foreign φ vs) × v) = do
+apply (V.Fun α (V.Foreign (ForeignOp (id × φ)) vs) × v) = do
    t × v'' <- runExists apply' φ
    pure $ T.AppForeign (length vs + 1) t × v''
    where
@@ -86,9 +86,9 @@ apply (V.Fun α (V.Foreign φ vs) × v) = do
    apply' :: forall t. ForeignOp' t -> m (ForeignTrace × Val _)
    apply' (ForeignOp' φ') = do
       t × v'' <- do
-         if φ'.arity > length vs' then pure $ Nothing × V.Fun α (V.Foreign φ vs')
+         if φ'.arity > length vs' then pure $ Nothing × V.Fun α (V.Foreign (ForeignOp (id × φ)) vs')
          else first Just <$> φ'.op vs'
-      pure $ mkExists (ForeignTrace' (ForeignOp' φ') t) × v''
+      pure $ ForeignTrace (id × mkExists (ForeignTrace' (ForeignOp' φ') t)) × v''
 apply (V.Fun α (V.PartialConstr c vs) × v) = do
    check (length vs < n) ("Too many arguments to " <> showCtr c)
    pure $ T.AppConstr c × v'

src/EvalBwd.purs

@@ -25,11 +25,11 @@ import GaloisConnection (GaloisConnection(..))
 import Lattice (Raw, bot, botOf, expand, (∨))
 import Partial.Unsafe (unsafePartial)
 import Trace (AppTrace(..), Trace(..), VarDef(..)) as T
-import Trace (AppTrace, ForeignTrace'(..), Match(..), Trace)
+import Trace (AppTrace, ForeignTrace(..), ForeignTrace'(..), Match(..), Trace)
 import Util (type (×), Endo, absurd, definitely', error, nonEmpty, successful, (!), (×))
 import Util.Pair (zip) as P
 import Val (Fun(..), Val(..)) as V
-import Val (class Ann, DictRep(..), Env, ForeignOp, ForeignOp'(..), MatrixRep(..), Val, append_inv, (<+>))
+import Val (class Ann, DictRep(..), Env, ForeignOp(..), ForeignOp'(..), MatrixRep(..), Val, append_inv, (<+>))
 
 closeDefsBwd :: forall a. Ann a => Env a -> Env a × RecDefs a × a
 closeDefsBwd γ =
@@ -79,14 +79,14 @@ applyBwd (T.AppClosure xs w t3 × v) =
    γ1 × γ2 = append_inv xs γ1γ2
    γ1' × δ' × β' = closeDefsBwd γ2
    v' × σ = matchBwd γ3 (ContExpr e) β w
-applyBwd (T.AppForeign n t × v) =
+applyBwd (T.AppForeign n (ForeignTrace (id × t)) × v) =
    V.Fun α (V.Foreign φ vs'') × v2'
    where
    φ × α × { init: vs'', last: v2' } = second (second (definitely' <<< unsnoc)) $ runExists applyBwd' t
       where
       applyBwd' :: forall t. ForeignTrace' t -> ForeignOp × a × List (Val _)
       applyBwd' (ForeignTrace' (ForeignOp' φ) t') =
-         mkExists (ForeignOp' φ) ×
+         ForeignOp (id × mkExists (ForeignOp' φ)) ×
             if φ.arity > n then unsafePartial $ let V.Fun α (V.Foreign _ vs'') = v in α × vs''
             else bot × φ.op_bwd (definitely' t' × v)
 applyBwd (T.AppConstr c × v) =

src/EvalGraph.purs

@@ -34,7 +34,7 @@ import Pretty (prettyP)
 import Primitive (string, intPair)
 import Util (type (×), check, concatM, error, orElse, successful, throw, with, (×))
 import Util.Pair (unzip) as P
-import Val (DictRep(..), Env, ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>))
+import Val (DictRep(..), Env, ForeignOp(..), ForeignOp'(..), MatrixRep(..), Val, for, lookup', restrict, (<+>))
 import Val (Fun(..), Val(..)) as V
 
 type GraphConfig g =
@@ -92,15 +92,15 @@ apply (V.Fun α (V.Closure γ1 ρ σ)) v = do
    γ2 <- closeDefs γ1 ρ (singleton α)
    γ3 × κ × αs <- match v σ
    eval (γ1 <+> γ2 <+> γ3) (asExpr κ) (insert α αs)
-apply (V.Fun α (V.Foreign φ vs)) v =
+apply (V.Fun α (V.Foreign (ForeignOp (id × φ)) vs)) v =
    runExists apply' φ
    where
    vs' = snoc vs v
 
    apply' :: forall t. ForeignOp' t -> m (Val Vertex)
    apply' (ForeignOp' φ') =
       if φ'.arity > length vs' then
-         V.Fun <$> new (singleton α) <@> V.Foreign φ vs'
+         V.Fun <$> new (singleton α) <@> V.Foreign (ForeignOp (id × φ)) vs'
       else φ'.op' vs'
 apply (V.Fun α (V.PartialConstr c vs)) v = do
    check (length vs < n) ("Too many arguments to " <> showCtr c)

src/Expr.purs

@@ -121,6 +121,80 @@ instance BV (Cont a) where
    bv (ContElim σ) = bv σ
    bv (ContExpr _) = empty
 
+instance JoinSemilattice a => JoinSemilattice (Elim a) where
+   maybeJoin (ElimVar x κ) (ElimVar x' κ') = ElimVar <$> (x ≞ x') <*> maybeJoin κ κ'
+   maybeJoin (ElimConstr cκs) (ElimConstr cκs') =
+      ElimConstr <$> ((keys cκs `consistentWith` keys cκs') *> maybeJoin cκs cκs')
+   maybeJoin (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord <$> (xs ≞ ys) <*> maybeJoin κ κ'
+   maybeJoin _ _ = throw "Incompatible eliminators"
+
+   join σ = definedJoin σ
+
+instance BoundedJoinSemilattice a => Expandable (Elim a) (Raw Elim) where
+   expand (ElimVar x κ) (ElimVar x' κ') = ElimVar (x ≜ x') (expand κ κ')
+   expand (ElimConstr cκs) (ElimConstr cκs') = ElimConstr (expand cκs cκs')
+   expand (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord (xs ≜ ys) (expand κ κ')
+   expand _ _ = error "Incompatible eliminators"
+
+instance JoinSemilattice a => JoinSemilattice (Cont a) where
+   maybeJoin ContNone ContNone = pure ContNone
+   maybeJoin (ContExpr e) (ContExpr e') = ContExpr <$> maybeJoin e e'
+   maybeJoin (ContElim σ) (ContElim σ') = ContElim <$> maybeJoin σ σ'
+   maybeJoin _ _ = throw "Incompatible continuations"
+
+   join κ = definedJoin κ
+
+instance BoundedJoinSemilattice a => Expandable (Cont a) (Raw Cont) where
+   expand ContNone ContNone = ContNone
+   expand (ContExpr e) (ContExpr e') = ContExpr (expand e e')
+   expand (ContElim σ) (ContElim σ') = ContElim (expand σ σ')
+   expand _ _ = error "Incompatible continuations"
+
+instance JoinSemilattice a => JoinSemilattice (VarDef a) where
+   join def = definedJoin def
+   maybeJoin (VarDef σ e) (VarDef σ' e') = VarDef <$> maybeJoin σ σ' <*> maybeJoin e e'
+
+instance BoundedJoinSemilattice a => Expandable (VarDef a) (Raw VarDef) where
+   expand (VarDef σ e) (VarDef σ' e') = VarDef (expand σ σ') (expand e e')
+
+instance JoinSemilattice a => JoinSemilattice (Expr a) where
+   maybeJoin (Var x) (Var x') = Var <$> (x ≞ x')
+   maybeJoin (Op op) (Op op') = Op <$> (op ≞ op')
+   maybeJoin (Int α n) (Int α' n') = Int (α ∨ α') <$> (n ≞ n')
+   maybeJoin (Str α str) (Str α' str') = Str (α ∨ α') <$> (str ≞ str')
+   maybeJoin (Float α n) (Float α' n') = Float (α ∨ α') <$> (n ≞ n')
+   maybeJoin (Record α xes) (Record α' xes') = Record (α ∨ α') <$> maybeJoin xes xes'
+   maybeJoin (Dictionary α ees) (Dictionary α' ees') = Dictionary (α ∨ α') <$> maybeJoin ees ees'
+   maybeJoin (Constr α c es) (Constr α' c' es') = Constr (α ∨ α') <$> (c ≞ c') <*> maybeJoin es es'
+   maybeJoin (Matrix α e1 (x × y) e2) (Matrix α' e1' (x' × y') e2') =
+      Matrix (α ∨ α') <$> maybeJoin e1 e1' <*> ((x ≞ x') `lift2 (×)` (y ≞ y')) <*> maybeJoin e2 e2'
+   maybeJoin (Lambda α σ) (Lambda α' σ') = Lambda (α ∨ α') <$> maybeJoin σ σ'
+   maybeJoin (Project e x) (Project e' x') = Project <$> maybeJoin e e' <*> (x ≞ x')
+   maybeJoin (App e1 e2) (App e1' e2') = App <$> maybeJoin e1 e1' <*> maybeJoin e2 e2'
+   maybeJoin (Let def e) (Let def' e') = Let <$> maybeJoin def def' <*> maybeJoin e e'
+   maybeJoin (LetRec α ρ e) (LetRec α' ρ' e') = LetRec (α ∨ α') <$> maybeJoin ρ ρ' <*> maybeJoin e e'
+   maybeJoin _ _ = throw "Incompatible expressions"
+
+   join e = definedJoin e
+
+instance BoundedJoinSemilattice a => Expandable (Expr a) (Raw Expr) where
+   expand (Var x) (Var x') = Var (x ≜ x')
+   expand (Op op) (Op op') = Op (op ≜ op')
+   expand (Int α n) (Int _ n') = Int α (n ≜ n')
+   expand (Str α str) (Str _ str') = Str α (str ≜ str')
+   expand (Float α n) (Float _ n') = Float α (n ≜ n')
+   expand (Record α xes) (Record _ xes') = Record α (expand xes xes')
+   expand (Dictionary α ees) (Dictionary _ ees') = Dictionary α (expand ees ees')
+   expand (Constr α c es) (Constr _ c' es') = Constr α (c ≜ c') (expand es es')
+   expand (Matrix α e1 (x × y) e2) (Matrix _ e1' (x' × y') e2') =
+      Matrix α (expand e1 e1') ((x ≜ x') × (y ≜ y')) (expand e2 e2')
+   expand (Lambda α σ) (Lambda _ σ') = Lambda α (expand σ σ')
+   expand (Project e x) (Project e' x') = Project (expand e e') (x ≜ x')
+   expand (App e1 e2) (App e1' e2') = App (expand e1 e1') (expand e2 e2')
+   expand (Let def e) (Let def' e') = Let (expand def def') (expand e e')
+   expand (LetRec α ρ e) (LetRec _ ρ' e') = LetRec α (expand ρ ρ') (expand e e')
+   expand _ _ = error "Incompatible expressions"
+
 -- ======================
 -- boilerplate
 -- ======================
@@ -221,76 +295,7 @@ instance Foldable ProgCxt where
    foldr f = foldrDefault f
    foldMap f = foldMapDefaultL f
 
-instance JoinSemilattice a => JoinSemilattice (Elim a) where
-   maybeJoin (ElimVar x κ) (ElimVar x' κ') = ElimVar <$> (x ≞ x') <*> maybeJoin κ κ'
-   maybeJoin (ElimConstr cκs) (ElimConstr cκs') =
-      ElimConstr <$> ((keys cκs `consistentWith` keys cκs') *> maybeJoin cκs cκs')
-   maybeJoin (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord <$> (xs ≞ ys) <*> maybeJoin κ κ'
-   maybeJoin _ _ = throw "Incompatible eliminators"
-
-   join σ = definedJoin σ
-
-instance BoundedJoinSemilattice a => Expandable (Elim a) (Raw Elim) where
-   expand (ElimVar x κ) (ElimVar x' κ') = ElimVar (x ≜ x') (expand κ κ')
-   expand (ElimConstr cκs) (ElimConstr cκs') = ElimConstr (expand cκs cκs')
-   expand (ElimRecord xs κ) (ElimRecord ys κ') = ElimRecord (xs ≜ ys) (expand κ κ')
-   expand _ _ = error "Incompatible eliminators"
-
-instance JoinSemilattice a => JoinSemilattice (Cont a) where
-   maybeJoin ContNone ContNone = pure ContNone
-   maybeJoin (ContExpr e) (ContExpr e') = ContExpr <$> maybeJoin e e'
-   maybeJoin (ContElim σ) (ContElim σ') = ContElim <$> maybeJoin σ σ'
-   maybeJoin _ _ = throw "Incompatible continuations"
-
-   join κ = definedJoin κ
-
-instance BoundedJoinSemilattice a => Expandable (Cont a) (Raw Cont) where
-   expand ContNone ContNone = ContNone
-   expand (ContExpr e) (ContExpr e') = ContExpr (expand e e')
-   expand (ContElim σ) (ContElim σ') = ContElim (expand σ σ')
-   expand _ _ = error "Incompatible continuations"
-
-instance JoinSemilattice a => JoinSemilattice (VarDef a) where
-   join def = definedJoin def
-   maybeJoin (VarDef σ e) (VarDef σ' e') = VarDef <$> maybeJoin σ σ' <*> maybeJoin e e'
-
-instance BoundedJoinSemilattice a => Expandable (VarDef a) (Raw VarDef) where
-   expand (VarDef σ e) (VarDef σ' e') = VarDef (expand σ σ') (expand e e')
-
-instance JoinSemilattice a => JoinSemilattice (Expr a) where
-   maybeJoin (Var x) (Var x') = Var <$> (x ≞ x')
-   maybeJoin (Op op) (Op op') = Op <$> (op ≞ op')
-   maybeJoin (Int α n) (Int α' n') = Int (α ∨ α') <$> (n ≞ n')
-   maybeJoin (Str α str) (Str α' str') = Str (α ∨ α') <$> (str ≞ str')
-   maybeJoin (Float α n) (Float α' n') = Float (α ∨ α') <$> (n ≞ n')
-   maybeJoin (Record α xes) (Record α' xes') = Record (α ∨ α') <$> maybeJoin xes xes'
-   maybeJoin (Dictionary α ees) (Dictionary α' ees') = Dictionary (α ∨ α') <$> maybeJoin ees ees'
-   maybeJoin (Constr α c es) (Constr α' c' es') = Constr (α ∨ α') <$> (c ≞ c') <*> maybeJoin es es'
-   maybeJoin (Matrix α e1 (x × y) e2) (Matrix α' e1' (x' × y') e2') =
-      Matrix (α ∨ α') <$> maybeJoin e1 e1' <*> ((x ≞ x') `lift2 (×)` (y ≞ y')) <*> maybeJoin e2 e2'
-   maybeJoin (Lambda α σ) (Lambda α' σ') = Lambda (α ∨ α') <$> maybeJoin σ σ'
-   maybeJoin (Project e x) (Project e' x') = Project <$> maybeJoin e e' <*> (x ≞ x')
-   maybeJoin (App e1 e2) (App e1' e2') = App <$> maybeJoin e1 e1' <*> maybeJoin e2 e2'
-   maybeJoin (Let def e) (Let def' e') = Let <$> maybeJoin def def' <*> maybeJoin e e'
-   maybeJoin (LetRec α ρ e) (LetRec α' ρ' e') = LetRec (α ∨ α') <$> maybeJoin ρ ρ' <*> maybeJoin e e'
-   maybeJoin _ _ = throw "Incompatible expressions"
-
-   join e = definedJoin e
-
-instance BoundedJoinSemilattice a => Expandable (Expr a) (Raw Expr) where
-   expand (Var x) (Var x') = Var (x ≜ x')
-   expand (Op op) (Op op') = Op (op ≜ op')
-   expand (Int α n) (Int _ n') = Int α (n ≜ n')
-   expand (Str α str) (Str _ str') = Str α (str ≜ str')
-   expand (Float α n) (Float _ n') = Float α (n ≜ n')
-   expand (Record α xes) (Record _ xes') = Record α (expand xes xes')
-   expand (Dictionary α ees) (Dictionary _ ees') = Dictionary α (expand ees ees')
-   expand (Constr α c es) (Constr _ c' es') = Constr α (c ≜ c') (expand es es')
-   expand (Matrix α e1 (x × y) e2) (Matrix _ e1' (x' × y') e2') =
-      Matrix α (expand e1 e1') ((x ≜ x') × (y ≜ y')) (expand e2 e2')
-   expand (Lambda α σ) (Lambda _ σ') = Lambda α (expand σ σ')
-   expand (Project e x) (Project e' x') = Project (expand e e') (x ≜ x')
-   expand (App e1 e2) (App e1' e2') = App (expand e1 e1') (expand e2 e2')
-   expand (Let def e) (Let def' e') = Let (expand def def') (expand e e')
-   expand (LetRec α ρ e) (LetRec _ ρ' e') = LetRec α (expand ρ ρ') (expand e e')
-   expand _ _ = error "Incompatible expressions"
+derive instance Ord a => Ord (Expr a)
+derive instance Ord a => Ord (Elim a)
+derive instance Ord a => Ord (Cont a)
+derive instance Ord a => Ord (VarDef a)

src/Pretty.purs

@@ -4,7 +4,6 @@ import Prelude hiding (absurd, between)
 
 import Bindings (Bind, key, val, Var, (↦))
 import Data.Array (foldl)
-import Data.Exists (runExists)
 import Data.Foldable (class Foldable)
 import Data.List (List(..), fromFoldable, null, uncons, (:))
 import Data.List.NonEmpty (NonEmptyList, groupBy, singleton, toList)
@@ -29,7 +28,7 @@ import Util (type (+), type (×), Endo, absurd, assert, error, intersperse, (×)
 import Util.Pair (Pair(..), toTuple)
 import Util.Pretty (Doc(..), atop, beside, empty, hcat, render, text)
 import Val (Fun(..), Val(..)) as V
-import Val (class Ann, class Highlightable, DictRep(..), ForeignOp', Fun, MatrixRep(..), Val, highlightIf)
+import Val (class Ann, class Highlightable, DictRep(..), ForeignOp(..), Fun, MatrixRep(..), Val, highlightIf)
 
 class Pretty p where
    pretty :: p -> Doc
@@ -434,11 +433,11 @@ instance Highlightable a => Pretty (Val a) where
 
 instance Highlightable a => Pretty (a × Fun a) where
    pretty (α × V.Closure _ _ _) = (highlightIf α $ text "<closure>")
-   pretty (_ × V.Foreign φ _) = runExists pretty φ
+   pretty (_ × V.Foreign φ _) = pretty φ
    pretty (α × V.PartialConstr c vs) = prettyConstr α c vs
 
-instance Pretty (ForeignOp' t) where
-   pretty _ = text "<extern op>" -- TODO
+instance Pretty ForeignOp where
+   pretty (ForeignOp (s × _)) = text s
 
 instance (Pretty a, Pretty b) => Pretty (a + b) where
    pretty = pretty ||| pretty