{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}

-- I generally try to avoid modules full of (only) types but these are here
-- so the can be shared in both Technique.Translate and Technique.Builtins.

-- |
-- Builing blocks for the translation stage of the compiler.
module Technique.Internal where

import Core.Text
import Data.DList
import Technique.Language
import Technique.Quantity

-- FIXME ??? upgrade to named IVar
newtype Promise = Promise Value

-- |
-- The resolved value of eiter a literal or function applicaiton, either as
-- that literal, the expression, or as the result of waiting on the variable
-- it was assigned to.
--
-- Need names? Science names newly discovered creatures in Latin. I don't
-- speak Latin, but neither does anyone else so we can just make words up.
-- Yeay! (The lengths some people will go to in order to avoid qualified
-- imports is really impressive, isn't it?)
data Value
  = Unitus
  | Literali Rope
  | Quanticle Quantity
  | Tabularum [(Rope, Value)]
  | Parametriq [Value]
  deriving (Value -> Value -> Bool
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq, Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)

-- |
-- The internal representation of a Procedure, with ambiguities resolved.
--
-- We landed on Subroutine as the name of translated user-defined Procedure.
--
-- Procedures which are actually fundamental [in the context of the domain
-- specific language] represented by builtin IO actions which we call
-- Primatives.
--
-- The first constructor, Unresolved, is for the first stage pass through the
-- translate phase when we are still accumulating definitions, thereby
-- allowing for the forward use of not-yet-defiend procedures that will be
-- encountered in the same scope.

-- Didn't want to call this "function" because that means something in
-- functional programming and in programming language theory and this isn't
-- it. Other alternatives considered include Instance (the original name,
-- but we've reserved that to be used when instantiating a procedure at
-- runtime), Representation, and Internal. Subroutine is ok.
data Function
  = Unresolved Identifier
  | Subroutine Procedure Step
  | Primitive Procedure (Step -> IO Value)

functionName :: Function -> Identifier
functionName :: Function -> Identifier
functionName Function
func = case Function
func of
  Unresolved Identifier
name -> Identifier
name
  Subroutine Procedure
proc Step
_ -> Procedure -> Identifier
procedureName Procedure
proc
  Primitive Procedure
prim Step -> IO Value
_ -> Procedure -> Identifier
procedureName Procedure
prim

instance Show Function where
  show :: Function -> String
show Function
func =
    let name :: String
name = Rope -> String
forall α. Textual α => Rope -> α
fromRope (Identifier -> Rope
unIdentifier (Function -> Identifier
functionName Function
func))
     in case Function
func of
          Unresolved Identifier
_ -> String
"Unresolved \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\""
          Subroutine Procedure
_ Step
step -> String
"Subroutine \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Step -> String
forall a. Show a => a -> String
show Step
step
          Primitive Procedure
_ Step -> IO Value
_ -> String
"Primitive \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\""

instance Eq Function where
  == :: Function -> Function -> Bool
(==) Function
f1 Function
f2 = case Function
f1 of
    Unresolved Identifier
i1 -> case Function
f2 of
      Unresolved Identifier
i2 -> Identifier
i1 Identifier -> Identifier -> Bool
forall a. Eq a => a -> a -> Bool
== Identifier
i2
      Function
_ -> Bool
False
    Subroutine Procedure
proc1 Step
step1 -> case Function
f2 of
      Subroutine Procedure
proc2 Step
step2 -> Procedure
proc1 Procedure -> Procedure -> Bool
forall a. Eq a => a -> a -> Bool
== Procedure
proc2 Bool -> Bool -> Bool
&& Step
step1 Step -> Step -> Bool
forall a. Eq a => a -> a -> Bool
== Step
step2
      Function
_ -> Bool
False
    -- this is weak, but we can't compare Haskell functions for equality so if
    -- the Procedures are the same then we assume the Primitives are.

    Primitive Procedure
proc1 Step -> IO Value
_ -> case Function
f2 of
      Primitive Procedure
proc2 Step -> IO Value
_ -> Procedure
proc1 Procedure -> Procedure -> Bool
forall a. Eq a => a -> a -> Bool
== Procedure
proc2
      Function
_ -> Bool
False

newtype Name = Name Rope -- ??? upgrade to named IVar := Promise ???
  deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq, Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show)

-- |
-- Names. Always needing names. These ones are from original work when we
-- envisioned technique as a shallow embedding of a domain specific
-- language implemented in Haskell. Comments describing constructors are
-- taken from a suggestion by Oleg Kiselyov on page 23 of his course "Typed
-- Tagless Final Interpreters" that the constructors of a simply typed
-- lambda calculus in this style could be considered a "minimal
-- intuitionistic logic" which is absolutely fabulous.

-- While it probably would work to put an Asynchronous into a Tuple list,
-- it's not valid from the point of view of the surface language syntax.
data Step
  = Known Offset Value -- literals ("axioms")
  | Bench Offset [(Label, Step)]
  | Depends Offset Name -- block waiting on a value ("reference to a hypothesis denoted by a variable")
  | NoOp
  | Tuple Offset [Step]
  | Asynchronous Offset [Name] Step -- assignment (ie lambda, "implication introduction"
  | Invocation Offset Attribute Function Step -- function application ("implication elimination") on a [sub] Procedure
  | Nested Offset (DList Step)
  -- assumption axiom?
  -- weakening?
  deriving (Step -> Step -> Bool
(Step -> Step -> Bool) -> (Step -> Step -> Bool) -> Eq Step
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Step -> Step -> Bool
$c/= :: Step -> Step -> Bool
== :: Step -> Step -> Bool
$c== :: Step -> Step -> Bool
Eq, Int -> Step -> ShowS
[Step] -> ShowS
Step -> String
(Int -> Step -> ShowS)
-> (Step -> String) -> ([Step] -> ShowS) -> Show Step
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Step] -> ShowS
$cshowList :: [Step] -> ShowS
show :: Step -> String
$cshow :: Step -> String
showsPrec :: Int -> Step -> ShowS
$cshowsPrec :: Int -> Step -> ShowS
Show)

instance Located Step where
  locationOf :: Step -> Int
locationOf Step
step = case Step
step of
    Known Int
o Value
_ -> Int
o
    Bench Int
o [(Label, Step)]
_ -> Int
o
    Depends Int
o Name
_ -> Int
o
    Step
NoOp -> -Int
2
    Tuple Int
o [Step]
_ -> Int
o
    Asynchronous Int
o [Name]
_ Step
_ -> Int
o
    Invocation Int
o Attribute
_ Function
_ Step
_ -> Int
o
    Nested Int
o DList Step
_ -> Int
o

instance Semigroup Step where
  <> :: Step -> Step -> Step
(<>) = Step -> Step -> Step
forall a. Monoid a => a -> a -> a
mappend

instance Monoid Step where
  mempty :: Step
mempty = Step
NoOp
  mappend :: Step -> Step -> Step
mappend Step
NoOp Step
s2 = Step
s2
  mappend Step
s1 Step
NoOp = Step
s1
  mappend (Nested Int
o1 DList Step
list1) (Nested Int
_ DList Step
list2) = Int -> DList Step -> Step
Nested Int
o1 (DList Step -> DList Step -> DList Step
forall a. DList a -> DList a -> DList a
append DList Step
list1 DList Step
list2)
  mappend (Nested Int
o1 DList Step
list1) Step
s2 = Int -> DList Step -> Step
Nested Int
o1 (DList Step -> Step -> DList Step
forall a. DList a -> a -> DList a
snoc DList Step
list1 Step
s2)
  mappend Step
s1 (Nested Int
_ DList Step
list2) = Int -> DList Step -> Step
Nested (Step -> Int
forall a. Located a => a -> Int
locationOf Step
s1) (Step -> DList Step -> DList Step
forall a. a -> DList a -> DList a
cons Step
s1 DList Step
list2)
  mappend Step
s1 Step
s2 = Int -> DList Step -> Step
Nested (Step -> Int
forall a. Located a => a -> Int
locationOf Step
s1) (DList Step -> Step -> DList Step
forall a. DList a -> a -> DList a
snoc (Step -> DList Step
forall a. a -> DList a
singleton Step
s1) Step
s2)