module Unison.Var
  ( Var (..),
    Type (..),
    InferenceType (..),
    bakeId,
    blank,
    freshIn,
    inferAbility,
    inferInput,
    inferOther,
    inferOutput,
    inferPatternBindE,
    inferPatternBindV,
    inferPatternPureE,
    inferPatternPureV,
    inferTypeConstructor,
    inferTypeConstructorArg,
    isAction,
    missingResult,
    name,
    nameStr,
    named,
    nameds,
    rawName,
    reset,
    uncapitalize,
    universallyQuantifyIfFree,
    unnamedRef,
    unnamedTest,
  )
where

import Data.Char (isAlphaNum, isLower, toLower)
import Data.Text (pack)
import Data.Text qualified as Text
import Unison.ABT qualified as ABT
import Unison.Prelude
import Unison.Reference qualified as Reference
import Unison.WatchKind (WatchKind, pattern TestWatch)

-- | A class for variables. Variables may have auxiliary information which
-- may not form part of their identity according to `Eq` / `Ord`. Laws:
--
--   * `typeOf (typed n) == n`
--   * `typeOf (ABT.freshIn vs v) == typeOf v`:
--     `ABT.freshIn` does not alter the name
class (Show v, ABT.Var v) => Var v where
  typed :: Type -> v
  typeOf :: v -> Type
  freshId :: v -> Word64
  freshenId :: Word64 -> v -> v

freshIn :: (ABT.Var v) => Set v -> v -> v
freshIn :: forall v. Var v => Set v -> v -> v
freshIn = Set v -> v -> v
forall v. Var v => Set v -> v -> v
ABT.freshIn

named :: (Var v) => Text -> v
named :: forall v. Var v => Text -> v
named Text
n = Type -> v
forall v. Var v => Type -> v
typed (Text -> Type
User Text
n)

-- This bakes the fresh id into the name portion of the variable
-- and resets the id to 0.
bakeId :: (Var v) => v -> v
bakeId :: forall v. Var v => v -> v
bakeId v
v = Text -> v
forall v. Var v => Text -> v
named (v -> Text
forall v. Var v => v -> Text
name v
v)

rawName :: Type -> Text
rawName :: Type -> Text
rawName Type
typ = case Type
typ of
  User Text
n -> Text
n
  Inference InferenceType
Ability -> Text
"𝕖"
  Inference InferenceType
Input -> Text
"𝕒"
  Inference InferenceType
Output -> Text
"𝕣"
  Inference InferenceType
Other -> Text
"𝕩"
  Inference InferenceType
PatternPureE -> Text
"𝕞"
  Inference InferenceType
PatternPureV -> Text
"𝕧"
  Inference InferenceType
PatternBindE -> Text
"𝕞"
  Inference InferenceType
PatternBindV -> Text
"𝕧"
  Inference InferenceType
TypeConstructor -> Text
"𝕗"
  Inference InferenceType
TypeConstructorArg -> Text
"𝕦"
  Type
MissingResult -> Text
"_"
  Type
Blank -> Text
"_"
  Type
Eta -> Text
"_eta"
  Type
ANFBlank -> Text
"_anf"
  Type
Float -> Text
"_float"
  Type
Pattern -> Text
"_pattern"
  Type
Irrelevant -> Text
"_irrelevant"
  UnnamedReference Id
ref -> Id -> Text
Reference.idToText Id
ref
  UnnamedWatch WatchKind
k Text
guid -> WatchKind -> Text
forall a. IsString a => WatchKind -> a
fromString WatchKind
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
guid
  Type
Delay -> Text
"()"

name :: (Var v) => v -> Text
name :: forall v. Var v => v -> Text
name v
v = Type -> Text
rawName (v -> Type
forall v. Var v => v -> Type
typeOf v
v) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> v -> Text
forall v. Var v => v -> Text
showid v
v
  where
    showid :: v -> Text
showid (v -> Word64
forall v. Var v => v -> Word64
freshId -> Word64
0) = Text
""
    showid (v -> Word64
forall v. Var v => v -> Word64
freshId -> Word64
n) = WatchKind -> Text
pack (Word64 -> WatchKind
forall a. Show a => a -> WatchKind
show Word64
n)

-- | Currently, actions in blocks are encoded as bindings
-- with names of the form _123 (an underscore, followed by
-- 1 or more digits). This function returns `True` if the
-- input variable has this form.
--
-- Various places check for this (the pretty-printer, to
-- determine how to print the binding), and the typechecker
-- (to decide if it should ensure the binding has type `()`).
isAction :: (Var v) => v -> Bool
isAction :: forall v. Var v => v -> Bool
isAction v
v = case Text -> WatchKind
Text.unpack (v -> Text
forall v. Var v => v -> Text
name v
v) of
  (Char
'_' : WatchKind
rest) | Just Int
_ <- (WatchKind -> Maybe Int
forall a. Read a => WatchKind -> Maybe a
readMaybe WatchKind
rest :: Maybe Int) -> Bool
True
  WatchKind
_ -> Bool
False

uncapitalize :: (Var v) => v -> v
uncapitalize :: forall v. Var v => v -> v
uncapitalize v
v = WatchKind -> v
forall v. Var v => WatchKind -> v
nameds (WatchKind -> v) -> WatchKind -> v
forall a b. (a -> b) -> a -> b
$ WatchKind -> WatchKind
go (v -> WatchKind
forall v. Var v => v -> WatchKind
nameStr v
v)
  where
    go :: WatchKind -> WatchKind
go (Char
c : WatchKind
rest) = Char -> Char
toLower Char
c Char -> WatchKind -> WatchKind
forall a. a -> [a] -> [a]
: WatchKind
rest
    go WatchKind
n = WatchKind
n

missingResult,
  blank,
  inferInput,
  inferOutput,
  inferAbility,
  inferPatternPureE,
  inferPatternPureV,
  inferPatternBindE,
  inferPatternBindV,
  inferTypeConstructor,
  inferTypeConstructorArg,
  inferOther ::
    (Var v) => v
missingResult :: forall v. Var v => v
missingResult = Type -> v
forall v. Var v => Type -> v
typed Type
MissingResult
blank :: forall v. Var v => v
blank = Type -> v
forall v. Var v => Type -> v
typed Type
Blank
inferInput :: forall v. Var v => v
inferInput = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
Input)
inferOutput :: forall v. Var v => v
inferOutput = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
Output)
inferAbility :: forall v. Var v => v
inferAbility = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
Ability)
inferPatternPureE :: forall v. Var v => v
inferPatternPureE = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
PatternPureE)
inferPatternPureV :: forall v. Var v => v
inferPatternPureV = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
PatternPureV)
inferPatternBindE :: forall v. Var v => v
inferPatternBindE = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
PatternBindE)
inferPatternBindV :: forall v. Var v => v
inferPatternBindV = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
PatternBindV)
inferTypeConstructor :: forall v. Var v => v
inferTypeConstructor = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
TypeConstructor)
inferTypeConstructorArg :: forall v. Var v => v
inferTypeConstructorArg = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
TypeConstructorArg)
inferOther :: forall v. Var v => v
inferOther = Type -> v
forall v. Var v => Type -> v
typed (InferenceType -> Type
Inference InferenceType
Other)

unnamedRef :: (Var v) => Reference.Id -> v
unnamedRef :: forall v. Var v => Id -> v
unnamedRef Id
ref = Type -> v
forall v. Var v => Type -> v
typed (Id -> Type
UnnamedReference Id
ref)

unnamedTest :: (Var v) => Text -> v
unnamedTest :: forall v. Var v => Text -> v
unnamedTest Text
guid = Type -> v
forall v. Var v => Type -> v
typed (WatchKind -> Text -> Type
UnnamedWatch WatchKind
forall a. (Eq a, IsString a) => a
TestWatch Text
guid)

data Type
  = -- User provided variables, these should generally be left alone
    User Text
  | -- Variables created during type inference
    Inference InferenceType
  | -- Variables created to finish a block that doesn't end with an expression
    MissingResult
  | -- Variables invented for placeholder values inserted by user or by TDNR
    Blank
  | -- | An unnamed reference, created during unhashing a term/decl component.
    UnnamedReference Reference.Id
  | -- An unnamed watch expression of the given kind, for instance:
    --
    --  test> Ok "oog"
    --    has kind "test"
    --  > 1 + 1
    --    has kind ""
    UnnamedWatch WatchKind Text -- guid
    -- An unnamed variable for constructor eta expansion
  | Eta
  | -- An unnamed variable introduced by ANF transformation
    ANFBlank
  | -- An unnamed variable for a floated lambda
    Float
  | -- An unnamed variable introduced from pattern compilation
    Pattern
  | -- A variable for situations where we need to make up one that
    -- definitely won't be used.
    Irrelevant
  | -- A variable used to represent the ignored argument to a thunk, as in '(1 + 1)
    Delay
  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
/= :: Type -> Type -> Bool
Eq, Eq Type
Eq Type =>
(Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Type -> Type -> Ordering
compare :: Type -> Type -> Ordering
$c< :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
>= :: Type -> Type -> Bool
$cmax :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
min :: Type -> Type -> Type
Ord, Int -> Type -> WatchKind -> WatchKind
[Type] -> WatchKind -> WatchKind
Type -> WatchKind
(Int -> Type -> WatchKind -> WatchKind)
-> (Type -> WatchKind)
-> ([Type] -> WatchKind -> WatchKind)
-> Show Type
forall a.
(Int -> a -> WatchKind -> WatchKind)
-> (a -> WatchKind) -> ([a] -> WatchKind -> WatchKind) -> Show a
$cshowsPrec :: Int -> Type -> WatchKind -> WatchKind
showsPrec :: Int -> Type -> WatchKind -> WatchKind
$cshow :: Type -> WatchKind
show :: Type -> WatchKind
$cshowList :: [Type] -> WatchKind -> WatchKind
showList :: [Type] -> WatchKind -> WatchKind
Show)

data InferenceType
  = Ability
  | Input
  | Output
  | PatternPureE
  | PatternPureV
  | PatternBindE
  | PatternBindV
  | TypeConstructor
  | TypeConstructorArg
  | Other
  deriving (InferenceType -> InferenceType -> Bool
(InferenceType -> InferenceType -> Bool)
-> (InferenceType -> InferenceType -> Bool) -> Eq InferenceType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InferenceType -> InferenceType -> Bool
== :: InferenceType -> InferenceType -> Bool
$c/= :: InferenceType -> InferenceType -> Bool
/= :: InferenceType -> InferenceType -> Bool
Eq, Eq InferenceType
Eq InferenceType =>
(InferenceType -> InferenceType -> Ordering)
-> (InferenceType -> InferenceType -> Bool)
-> (InferenceType -> InferenceType -> Bool)
-> (InferenceType -> InferenceType -> Bool)
-> (InferenceType -> InferenceType -> Bool)
-> (InferenceType -> InferenceType -> InferenceType)
-> (InferenceType -> InferenceType -> InferenceType)
-> Ord InferenceType
InferenceType -> InferenceType -> Bool
InferenceType -> InferenceType -> Ordering
InferenceType -> InferenceType -> InferenceType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InferenceType -> InferenceType -> Ordering
compare :: InferenceType -> InferenceType -> Ordering
$c< :: InferenceType -> InferenceType -> Bool
< :: InferenceType -> InferenceType -> Bool
$c<= :: InferenceType -> InferenceType -> Bool
<= :: InferenceType -> InferenceType -> Bool
$c> :: InferenceType -> InferenceType -> Bool
> :: InferenceType -> InferenceType -> Bool
$c>= :: InferenceType -> InferenceType -> Bool
>= :: InferenceType -> InferenceType -> Bool
$cmax :: InferenceType -> InferenceType -> InferenceType
max :: InferenceType -> InferenceType -> InferenceType
$cmin :: InferenceType -> InferenceType -> InferenceType
min :: InferenceType -> InferenceType -> InferenceType
Ord, Int -> InferenceType -> WatchKind -> WatchKind
[InferenceType] -> WatchKind -> WatchKind
InferenceType -> WatchKind
(Int -> InferenceType -> WatchKind -> WatchKind)
-> (InferenceType -> WatchKind)
-> ([InferenceType] -> WatchKind -> WatchKind)
-> Show InferenceType
forall a.
(Int -> a -> WatchKind -> WatchKind)
-> (a -> WatchKind) -> ([a] -> WatchKind -> WatchKind) -> Show a
$cshowsPrec :: Int -> InferenceType -> WatchKind -> WatchKind
showsPrec :: Int -> InferenceType -> WatchKind -> WatchKind
$cshow :: InferenceType -> WatchKind
show :: InferenceType -> WatchKind
$cshowList :: [InferenceType] -> WatchKind -> WatchKind
showList :: [InferenceType] -> WatchKind -> WatchKind
Show)

reset :: (Var v) => v -> v
reset :: forall v. Var v => v -> v
reset v
v = Type -> v
forall v. Var v => Type -> v
typed (v -> Type
forall v. Var v => v -> Type
typeOf v
v)

nameStr :: (Var v) => v -> String
nameStr :: forall v. Var v => v -> WatchKind
nameStr = Text -> WatchKind
Text.unpack (Text -> WatchKind) -> (v -> Text) -> v -> WatchKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Text
forall v. Var v => v -> Text
name

nameds :: (Var v) => String -> v
nameds :: forall v. Var v => WatchKind -> v
nameds WatchKind
s = Text -> v
forall v. Var v => Text -> v
named (WatchKind -> Text
Text.pack WatchKind
s)

universallyQuantifyIfFree :: forall v. (Var v) => v -> Bool
universallyQuantifyIfFree :: forall v. Var v => v -> Bool
universallyQuantifyIfFree v
v =
  (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isLower (Int -> Text -> Text
Text.take Int
1 Text
n) Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
Text.all Char -> Bool
isAlphaNum Text
n
  where
    n :: Text
n = v -> Text
forall v. Var v => v -> Text
name (v -> Text) -> v -> Text
forall a b. (a -> b) -> a -> b
$ v -> v
forall v. Var v => v -> v
reset v
v