Core S-Expression Syntax

The concrete syntax of Juvix once we Hit Core, namely the Named version (HR)

Generation

Term

Star

Haskell ADT

  = -- | (sort i) i th ordering of (closed) universe.
    Star Universe

ML Syntax

  -- Universe 0
  ×₀
  -- Universe 1
  ×₁
  -- Universe n
  ×ₙ

S-expression Syntax

  ;; universe 0
  (:star 0)
  ;; universe 1
  (:star 1)
  ;; universe n
  (:star n)

Prim type

Haskell ADT

  | -- | PrimTy primitive type
    PrimTy primTy

ML Syntax
```
  primTy Michelson.Int
```
S-expression Syntax
```
  (:prim-ty Michelson.add)
```

Prim

Haskell ADT

  | -- | primitive constant
    Prim primVal

ML Syntax
```
  prim Michelson.Add
```
S-expression Syntax
```
  (:prim Michelson.add)
```

Π / Pi

Haskell ADT

  | -- | formation rule of the dependent function type PI.
    -- the Usage(π) tracks how many times x is used.
    Pi Usage NameSymbol.T (Term primTy primVal) (Term primTy primVal)

ML Syntax

  (Π (0 | typ : ×₀) (Π (1 | _ : typ) typ))

S-expression Syntax

  (:pi (typ 0 (:star 0)) (:pi (_ 1 typ) typ))

Lam

Haskell ADT

  | -- | LAM Introduction rule of PI.
    -- The abstracted variables usage is tracked with the Usage(π).
    Lam NameSymbol.T (Term primTy primVal)

ML Syntax

  -- Note we don't have (λ x : unit -> x) : unit -> unit, as that requires
  -- the type to be given in the Haskell ADT, and is thus handled in Π
  λ x ⟶ ∅

S-expression Syntax
```
  (:named-lambda x :unit)
```

Sig

Haskell ADT

  | -- | Dependent pair (Σ) type, with each half having its own usage
    Sig Usage NameSymbol.T (Term primTy primVal) (Term primTy primVal)

ML Syntax

  Π (ω | x : A) ⟶
    Σ (ω | y : B) ⟶
     C x y

S-expression Syntax

  (:pi (x ω A)
     (:sigma (y ω b)
        (C x y)))

Pair

Haskell ADT

  | -- | Pair value
    Pair (Term primTy primVal) (Term primTy primVal)

ML Syntax
```
  ‹f x y, g x y›
```
S-expression Syntax
```
  (:pair (f x y) (g x y))
```

Let

Haskell ADT

  | -- | Let binder.
    -- the local definition is bound to de Bruijn index 0.
    Let Usage NameSymbol.T (Elim primTy primVal) (Term primTy primVal)

ML Syntax
```
  let 2 | a = f x y in
    <a,a>
```

S-expression Syntax

  (:named-let (a 2 (f x y))
    (:pair a a))

Unit type

Note
Should this be treated specially?
Haskell ADT
```
  | -- | Unit type.
    UnitTy
```
ML Syntax
```
  Unit
```
S-expression Syntax
```
  :unit-type
```

Unit

Note
Should this be treated specially?
Haskell ADT
```
  | -- | Unit Value
    Unit
```
ML Syntax
```
  ∅
```
S-expression Syntax
```
  :unit
```

Elim

Should we even have Elims with this strategy, we know by exclusion, an explicit tome for it seems needless? Depends how the code turns out.

Record

Haskell ADT

  | -- | Constructor for a record type.
    Record [(Symbol, Term primTy primVal)]

ML Syntax

  {name₁ = term₁, name₂ = term₂, …, nameₙ = termₙ}

S-expression Syntax

  (:record name₁ term₁ name₂ term₂ … nameₙ termₙ)

RecordTy

Haskell ADT

  | -- | Record type. (It's a list not a map because the dependency order
    -- needs to be preserved.)
    RecordTy [(Symbol, Usage, Term primTy primVal)]

ML Syntax

  {name₁ usage₁ : term₁, name₂ usage₂ : term₂, …, nameₙ usageₙ : termₙ}

S-expression Syntax

  (:record-ty
    (name₁ usage₁ term₁)
    (name₂ usage₂ term₂)
    ...
    (nameₙ usageₙ termₙ))

Elim

Var

Haskell ADT

  = -- | Named Variables
    Var NameSymbol.T

ML Syntax
```
  λ x ⟶ x
```
S-expression Syntax
```
  (:named-lambda x x)
```
- We treat vars as simple any atom in the list that isn't a special form.

App

Haskell ADT

  | -- | elimination rule of PI (APP).
    App (Elim primTy primVal) (Term primTy primVal)

ML Syntax
```
  f a b
```
S-expression Syntax
```
  (f a b)
```
- We simply represent application as the car of the list if it's not a special form

Ann

Haskell ADT

  | -- | Annotation with usage.
    Ann Usage (Term primTy primVal) (Term primTy primVal) Universe

ML Syntax
```
  (ω | f x y : C x y : * 0)
```

S-expression Syntax

  (: (f x y) (:usage ω :universe 0)
     (C x y))

  ;; Should we adopt it without names?
  (: (f x y) (ω 0)
     (C x y))

Here we have a choice, I′m not sure which one I prefer, the first is more explicit, but may be a bit too verbose

Lookup

Haskell ADT

  | -- | Project an element from a record type.
    Lookup (Elim primTy primVal) Symbol

ML Syntax
```
  name.elim
```
S-expression Syntax
```
  (:lookup elim name)
```

Value

Instead of giving each variant a section, we will instead note that Values relate to Terms, except instead of an Elim they have a Neutral.

Thus, it's an extension of Term.

Neutral

Neutral is the same as Value, except we remove annotations from the possibilities

Pattern

Constructor

Haskell ADT

  = PCon GlobalName [Pattern primTy primVal]

ML Syntax
```
  (Cons a as)
```

S-expression Syntax

  ;; No other form has an unattended name with arguments, so this is
  ;; safe
  (Cons a as)

Pair

Haskell ADT

  | PPair (Pattern primTy primVal) (Pattern primTy primVal)

ML Syntax

  -- We have syntax for multi pairs
  ‹x, y, z›
  -- This is just an alias for
  ‹x, ‹y, z››

S-expression Syntax

  (:pair x y z)
  ;; This is just an alias for
  (:pair x (:pair y z))

Unit

Note
Should this be treated specially?
Haskell ADT
```
  | PUnit
```
ML Syntax
```
  ∅
```
S-expression Syntax
```
  :unit
```

Var

Haskell ADT
```
  | PVar PatternVar
```
ML Syntax
```
  (Constructor a b c)

  a

  z
```
S-expression Syntax
```
  (Constructor a b c)

  a

  z
```

Dot

Haskell ADT

  -- Deduction by the unifier, that the term should already be
  -- known
  | PDot (Term primTy primVal)

ML Syntax

  -- Taken From
  -- data Double (n : ℕ) : ℕ → Set where
  --   double : Double n (n + n)

  -- foo : ∀ m n → Double m n → {!!}
  -- foo m .(m + m) double = {!!}

  .(m + m)

S-expression Syntax
```
  (:dot (+ m m))
```

Primitive

Haskell ADT
```
  | PPrim primVal
```
ML Syntax
```
  (Prim +)
```
S-expression Syntax
```
  (:prim +)
```

Raw Globals

This is the target that the context type should hold. However we have to note a few facts about how things are stored.
We don't really have ML syntax counterparts for these, so instead we will give the raw structure as the syntax.

FunClause

In this the full type has many overlapping elements, thus we should just steal the RawFunClause field

Haskell ADT

  data RawFunction' ext primTy primVal = RawFunction
    { rawFunName :: GlobalName,
      rawFunUsage :: GlobalUsage,
      rawFunType :: Term' ext primTy primVal,
      -- The value we want
      rawFunClauses :: NonEmpty (RawFunClause' ext primTy primVal)
    }
    deriving (Generic)

  -- The Type that we will emulate
  data RawFunClause' ext primTy primVal = RawFunClause
    { rawClauseTel :: RawTelescope ext primTy primVal,
      rawClausePats :: [Pattern' ext primTy primVal], --TODO [SplitPattern]
      rawClauseBody :: Term' ext primTy primVal,
      rawClauseCatchall :: Bool
    }
    deriving (Generic)

Haskell Context ADT

  data Def term ty = D
      -- This mimics rawFunUsage
    { defUsage :: Maybe Usage.T,
      -- This mimics rawFunType
      defMTy :: Maybe ty,
      -- This field will mimic rawFunClause'
      defTerm :: term,
      defPrecedence :: Precedence
    }
    deriving (Show, Read, Generic, Eq, Data)

Raw Fun Clause Example

  RawFunClause
    { rawClauseTel = []
    , rawClausePats =
        [ PVar "x" ]
    , rawClauseBody = Elim'
                      ( Var "x" )
    , rawClauseCatchall = False } :| []

Currently I can't get a better example sadly.

S-expression Syntax

  (:raw-fun-clause () (x)
    x
    :false)

Last modified August 16, 2021 : Fix minor typo in the IR form (476109e)