-- | This module contains various utilities related to the implementation of record types.
module Unison.DataDeclaration.Records
  ( generateRecordAccessors,
  )
where

import Data.List.NonEmpty (pattern (:|))
import Data.List.NonEmpty qualified as List (NonEmpty)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Unison.ABT qualified as ABT
import Unison.ConstructorReference (GConstructorReference (..))
import Unison.Pattern qualified as Pattern
import Unison.Prelude
import Unison.Reference (TypeReference)
import Unison.Term (Term)
import Unison.Term qualified as Term
import Unison.Type (Type)
import Unison.Type qualified as Type
import Unison.Var (Var)
import Unison.Var qualified as Var

-- | Generate getter, setter, and modify functions for each field of
-- a record-style data declaration.
--
-- Each accessor body is wrapped with a 'Term.Ann' carrying its
-- declared type. The annotation is what lets the typechecker check
-- (rather than infer) the accessor against fields whose declared
-- type contains nested 'forall' quantifiers — pattern matching on
-- such a constructor argument produces instantiated existentials
-- that can't be re-generalized in a purely inferred result, but
-- check-direction handling skolemizes the inner foralls and
-- succeeds.
--
-- The setter and modifier are given their /fully general/ types: the
-- type variables that a field is the sole one to reference can change
-- when that field is updated, so they are freshened in the result
-- type. For example @type These a b = { here : a, there : b }@ yields
--
-- > These.here.set    : c -> These a b -> These c b
-- > These.here.modify : (a -> c) -> These a b -> These c b
--
-- since @here@ is the only field mentioning @a@. A variable shared by
-- more than one field (or referenced by no field) is left fixed, so
-- such records get the usual non-type-changing accessors.
generateRecordAccessors ::
  (Semigroup a, Var v) =>
  (List.NonEmpty v -> v) ->
  (a -> a) ->
  -- | Each field as @(name, annotation, declared type)@. The
  -- declared type is used to build the accessor's annotation.
  [(v, a, Type v a)] ->
  -- | Type-level parameters of the enclosing data declaration. These
  -- become the outermost 'forall' on each accessor's annotation so
  -- the body is polymorphic in them.
  [v] ->
  v ->
  TypeReference ->
  [(v, a, Term v a)]
generateRecordAccessors :: forall a v.
(Semigroup a, Var v) =>
(NonEmpty v -> v)
-> (a -> a)
-> [(v, a, Type v a)]
-> [v]
-> v
-> TypeReference
-> [(v, a, Term v a)]
generateRecordAccessors NonEmpty v -> v
namespaced a -> a
generatedAnn [(v, a, Type v a)]
fields [v]
tyvars v
typename TypeReference
typ =
  [[(v, a, Term v a)]] -> [(v, a, Term v a)]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join [(v, a, Type v a) -> Int -> [(v, a, Term v a)]
tm (v, a, Type v a)
t Int
i | ((v, a, Type v a)
t, Int
i) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [(Int
0 :: Int) ..]]
  where
    argname :: v
argname = v -> v
forall v. Var v => v -> v
Var.uncapitalize v
typename
    tyvarSet :: Set v
tyvarSet = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v]
tyvars
    -- The enclosing record's own type, applied to its parameters with
    -- the given type-variable renaming: e.g. @Point a b@ (or, under a
    -- @{a ↦ a1}@ renaming, @Point a1 b@) for @type Point a b = …@.
    selfTypeWith :: a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
renaming =
      (Type v a -> v -> Type v a) -> Type v a -> [v] -> Type v a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
        (\Type v a
acc v
tyv -> a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app a
ann Type v a
acc (a -> v -> Type v a
forall v a. Ord v => a -> v -> Type v a
Type.var a
ann (v -> v -> Map v v -> v
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault v
tyv v
tyv Map v v
renaming)))
        (a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
Type.ref a
ann TypeReference
typ)
        [v]
tyvars
    -- All variable names to steer clear of when minting fresh type
    -- variables for type-changing accessors.
    avoidVars :: Set v
avoidVars =
      [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Set v
tyvarSet Set v -> [Set v] -> [Set v]
forall a. a -> [a] -> [a]
: v -> Set v
forall a. a -> Set a
Set.singleton v
argname Set v -> [Set v] -> [Set v]
forall a. a -> [a] -> [a]
: [Type v a -> Set v
forall v a. Type v a -> Set v
Type.freeVars Type v a
ty | (v
_, a
_, Type v a
ty) <- [(v, a, Type v a)]
fields])
    arrow :: a -> Type v a -> Type v a -> Type v a
arrow a
ann Type v a
i Type v a
o = a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.arrow a
ann Type v a
i Type v a
o
    tm :: (v, a, Type v a) -> Int -> [(v, a, Term v a)]
tm (v
fname, a
fieldAnn, Type v a
fieldTy) Int
i =
      [ (NonEmpty v -> v
namespaced (v
typename v -> [v] -> NonEmpty v
forall a. a -> [a] -> NonEmpty a
:| [v
fname]), a
ann, a -> Term v a -> Type v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> Term2 vt at ap v a -> Type vt at -> Term2 vt at ap v a
Term.ann a
ann Term v a
get Type v a
getTy),
        (NonEmpty v -> v
namespaced (v
typename v -> [v] -> NonEmpty v
forall a. a -> [a] -> NonEmpty a
:| [v
fname, Text -> v
forall v. Var v => Text -> v
Var.named Text
"set"]), a
ann, a -> Term v a -> Type v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> Term2 vt at ap v a -> Type vt at -> Term2 vt at ap v a
Term.ann a
ann Term v a
set Type v a
setTy),
        (NonEmpty v -> v
namespaced (v
typename v -> [v] -> NonEmpty v
forall a. a -> [a] -> NonEmpty a
:| [v
fname, Text -> v
forall v. Var v => Text -> v
Var.named Text
"modify"]), a
ann, a -> Term v a -> Type v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> Term2 vt at ap v a -> Type vt at -> Term2 vt at ap v a
Term.ann a
ann Term v a
modify Type v a
modifyTy)
      ]
      where
        ann :: a
ann = a -> a
generatedAnn a
fieldAnn
        conref :: GConstructorReference TypeReference
conref = TypeReference
-> ConstructorId -> GConstructorReference TypeReference
forall r. r -> ConstructorId -> GConstructorReference r
ConstructorReference TypeReference
typ ConstructorId
0
        pat :: [Pattern a] -> Pattern a
pat = a
-> GConstructorReference TypeReference -> [Pattern a] -> Pattern a
forall loc.
loc
-> GConstructorReference TypeReference
-> [Pattern loc]
-> Pattern loc
Pattern.Constructor a
ann GConstructorReference TypeReference
conref

        -- The decl's type variables that this field is the /sole/ one
        -- to reference. Updating this field can change them without
        -- affecting any other field, so the setter and modifier
        -- freshen them in their result type.
        soleTyvars :: [v]
soleTyvars =
          [ v
v
          | v
v <- [v]
tyvars,
            v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v Set v
thisFieldVars,
            Bool -> Bool
not (v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v Set v
otherFieldVars)
          ]
          where
            thisFieldVars :: Set v
thisFieldVars = Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set v
tyvarSet (Type v a -> Set v
forall v a. Type v a -> Set v
Type.freeVars Type v a
fieldTy)
            otherFieldVars :: Set v
otherFieldVars =
              [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
                [ Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set v
tyvarSet (Type v a -> Set v
forall v a. Type v a -> Set v
Type.freeVars Type v a
ty)
                | ((v
_, a
_, Type v a
ty), Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [(Int
0 :: Int) ..],
                  Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i
                ]
        -- A fresh counterpart for each sole-referenced variable.
        renaming :: Map v v
renaming = (Set v, Map v v) -> Map v v
forall a b. (a, b) -> b
snd (((Set v, Map v v) -> v -> (Set v, Map v v))
-> (Set v, Map v v) -> [v] -> (Set v, Map v v)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Set v, Map v v) -> v -> (Set v, Map v v)
forall {a}. Var a => (Set a, Map a a) -> a -> (Set a, Map a a)
freshen (Set v
avoidVars, Map v v
forall k a. Map k a
Map.empty) [v]
soleTyvars)
          where
            freshen :: (Set a, Map a a) -> a -> (Set a, Map a a)
freshen (Set a
used, Map a a
m) a
v =
              let v' :: a
v' = Set a -> a -> a
forall v. Var v => Set v -> v -> v
Var.freshIn Set a
used a
v
               in (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
v' Set a
used, a -> a -> Map a a -> Map a a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
v a
v' Map a a
m)
        freshTyvars :: [v]
freshTyvars = Map v v -> [v]
forall k a. Map k a -> [a]
Map.elems Map v v
renaming
        -- @fieldTy@ with the sole-referenced variables freshened.
        fieldTy' :: Type v a
fieldTy' = Map v v -> Type v a -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
ABT.renames Map v v
renaming Type v a
fieldTy

        -- Accessor type annotations. Quantifying over the data decl's
        -- tyvars (plus the fresh ones for set/modify) wraps the outer
        -- 'forall'; the field's own 'forall's (if any) remain nested
        -- inside @fieldTy@.
        getTy :: Type v a
getTy = a -> [v] -> Type v a -> Type v a
forall v a. Ord v => a -> [v] -> Type v a -> Type v a
Type.foralls a
ann [v]
tyvars (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann (a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
forall a. Monoid a => a
mempty) Type v a
fieldTy)
        setTy :: Type v a
setTy =
          a -> [v] -> Type v a -> Type v a
forall v a. Ord v => a -> [v] -> Type v a -> Type v a
Type.foralls
            a
ann
            ([v]
tyvars [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> [v]
freshTyvars)
            (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann Type v a
fieldTy' (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann (a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
forall a. Monoid a => a
mempty) (a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
renaming)))
        modifyTy :: Type v a
modifyTy =
          a -> [v] -> Type v a -> Type v a
forall v a. Ord v => a -> [v] -> Type v a -> Type v a
Type.foralls
            a
ann
            ([v]
tyvars [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> [v]
freshTyvars)
            (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann Type v a
fieldTy Type v a
fieldTy') (a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann (a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
forall a. Monoid a => a
mempty) (a -> Map v v -> Type v a
selfTypeWith a
ann Map v v
renaming)))

        -- point -> case point of Point _ y _ -> y
        get :: Term v a
get =
          a -> (a, v) -> Term v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> (a, v) -> Term2 vt at ap v a -> Term2 vt at ap v a
Term.lam a
ann (a
ann, v
argname) (Term v a -> Term v a) -> Term v a -> Term v a
forall a b. (a -> b) -> a -> b
$
            a -> Term v a -> [MatchCase a (Term v a)] -> Term v a
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
Term.match
              a
ann
              (a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
argname)
              [Pattern a -> Maybe (Term v a) -> Term v a -> MatchCase a (Term v a)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
Term.MatchCase ([Pattern a] -> Pattern a
pat [Pattern a]
cargs) Maybe (Term v a)
forall a. Maybe a
Nothing Term v a
rhs]
          where
            -- [_, y, _]
            cargs :: [Pattern a]
cargs =
              [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then a -> Pattern a
forall loc. loc -> Pattern loc
Pattern.Var a
ann else a -> Pattern a
forall loc. loc -> Pattern loc
Pattern.Unbound a
ann
              | ((v, a, Type v a)
_, Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..]
              ]
            -- y -> y
            rhs :: Term v a
rhs = a -> v -> Term v a -> Term v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs' a
ann v
fname (a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
fname)

        -- y' point -> case point of Point x _ z -> Point x y' z
        set :: Term v a
set =
          a -> [(a, v)] -> Term v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> [(a, v)] -> Term2 vt at ap v a -> Term2 vt at ap v a
Term.lam' a
ann [(a
ann, v
fname'), (a
ann, v
argname)] (Term v a -> Term v a) -> Term v a -> Term v a
forall a b. (a -> b) -> a -> b
$
            a -> Term v a -> [MatchCase a (Term v a)] -> Term v a
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
Term.match
              a
ann
              (a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
argname)
              [Pattern a -> Maybe (Term v a) -> Term v a -> MatchCase a (Term v a)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
Term.MatchCase ([Pattern a] -> Pattern a
pat [Pattern a]
cargs) Maybe (Term v a)
forall a. Maybe a
Nothing Term v a
rhs]
          where
            -- y'
            fname' :: v
fname' =
              Text -> v
forall v. Var v => Text -> v
Var.named (Text -> v) -> (v -> Text) -> v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Text
forall v. Var v => v -> Text
Var.name (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$
                Set v -> v -> v
forall v. Var v => Set v -> v -> v
Var.freshIn ([v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> Set v) -> [v] -> Set v
forall a b. (a -> b) -> a -> b
$ [v
argname] [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> ((v, a, Type v a) -> v
forall {a} {b} {c}. (a, b, c) -> a
fst3 ((v, a, Type v a) -> v) -> [(v, a, Type v a)] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, a, Type v a)]
fields)) v
fname
            -- [x, _, z]
            cargs :: [Pattern a]
cargs =
              [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then a -> Pattern a
forall loc. loc -> Pattern loc
Pattern.Unbound a
ann else a -> Pattern a
forall loc. loc -> Pattern loc
Pattern.Var a
ann
              | ((v, a, Type v a)
_, Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..]
              ]
            -- x z -> Point x y' z
            rhs :: Term v a
rhs =
              (v -> Term v a -> Term v a) -> Term v a -> [v] -> Term v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                (a -> v -> Term v a -> Term v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs' a
ann)
                (a -> GConstructorReference TypeReference -> Term v a
forall v a vt at ap.
Ord v =>
a -> GConstructorReference TypeReference -> Term2 vt at ap v a
Term.constructor a
ann GConstructorReference TypeReference
conref Term v a -> [Term v a] -> Term v a
forall v a vt at ap.
(Ord v, Semigroup a) =>
Term2 vt at ap v a -> [Term2 vt at ap v a] -> Term2 vt at ap v a
`Term.apps'` [Term v a]
vargs)
                [v
v | ((v
v, a
_, Type v a
_), Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..], Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i]
            -- [x, y', z]
            vargs :: [Term v a]
vargs =
              [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i then a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
fname' else a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
v
              | ((v
v, a
_, Type v a
_), Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..]
              ]

        -- example: `f point -> case point of Point x y z -> Point x (f y) z`
        modify :: Term v a
modify =
          a -> [(a, v)] -> Term v a -> Term v a
forall v a vt at ap.
Ord v =>
a -> [(a, v)] -> Term2 vt at ap v a -> Term2 vt at ap v a
Term.lam' a
ann [(a
ann, v
fname'), (a
ann, v
argname)] (Term v a -> Term v a) -> Term v a -> Term v a
forall a b. (a -> b) -> a -> b
$
            a -> Term v a -> [MatchCase a (Term v a)] -> Term v a
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
Term.match
              a
ann
              (a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
argname)
              [Pattern a -> Maybe (Term v a) -> Term v a -> MatchCase a (Term v a)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
Term.MatchCase ([Pattern a] -> Pattern a
pat [Pattern a]
cargs) Maybe (Term v a)
forall a. Maybe a
Nothing Term v a
rhs]
          where
            fname' :: v
fname' =
              Text -> v
forall v. Var v => Text -> v
Var.named (Text -> v) -> (v -> Text) -> v -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Text
forall v. Var v => v -> Text
Var.name (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$
                Set v -> v -> v
forall v. Var v => Set v -> v -> v
Var.freshIn
                  ([v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> Set v) -> [v] -> Set v
forall a b. (a -> b) -> a -> b
$ [v
argname] [v] -> [v] -> [v]
forall a. Semigroup a => a -> a -> a
<> ((v, a, Type v a) -> v
forall {a} {b} {c}. (a, b, c) -> a
fst3 ((v, a, Type v a) -> v) -> [(v, a, Type v a)] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, a, Type v a)]
fields))
                  (Text -> v
forall v. Var v => Text -> v
Var.named Text
"f")
            cargs :: [Pattern a]
cargs = [a -> Pattern a
forall loc. loc -> Pattern loc
Pattern.Var a
ann | (v, a, Type v a)
_ <- [(v, a, Type v a)]
fields]
            rhs :: Term v a
rhs =
              (v -> Term v a -> Term v a) -> Term v a -> [v] -> Term v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
                (a -> v -> Term v a -> Term v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs' a
ann)
                (a -> GConstructorReference TypeReference -> Term v a
forall v a vt at ap.
Ord v =>
a -> GConstructorReference TypeReference -> Term2 vt at ap v a
Term.constructor a
ann GConstructorReference TypeReference
conref Term v a -> [Term v a] -> Term v a
forall v a vt at ap.
(Ord v, Semigroup a) =>
Term2 vt at ap v a -> [Term2 vt at ap v a] -> Term2 vt at ap v a
`Term.apps'` [Term v a]
vargs)
                ((v, a, Type v a) -> v
forall {a} {b} {c}. (a, b, c) -> a
fst3 ((v, a, Type v a) -> v) -> [(v, a, Type v a)] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, a, Type v a)]
fields)
            vargs :: [Term v a]
vargs =
              [ if Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i
                  then Term v a -> [Term v a] -> Term v a
forall v a vt at ap.
(Ord v, Semigroup a) =>
Term2 vt at ap v a -> [Term2 vt at ap v a] -> Term2 vt at ap v a
Term.apps' (a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
fname') [a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
v]
                  else a -> v -> Term v a
forall a v vt at ap. a -> v -> Term2 vt at ap v a
Term.var a
ann v
v
              | ((v
v, a
_, Type v a
_), Int
j) <- [(v, a, Type v a)]
fields [(v, a, Type v a)] -> [Int] -> [((v, a, Type v a), Int)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Int
0 ..]
              ]

    fst3 :: (a, b, c) -> a
fst3 (a
x, b
_, c
_) = a
x