text:
{-
  An embeded DSL for prolog-style logic programming, based on the
  pure-prolog parser and interpreter originally written in Haskell

  Original author: Ken Friis Larsen      <kflarsen@diku.dk>
  Translated into Idris by Nathan Bedell <nbedell@tulane.edu>
-}

module Interp

import Ast

%access public export

----------------------------------------------------------------------
-- Interpreter
----------------------------------------------------------------------

Unifier : Type
Unifier = List (Variable, Term)

-- A non-lazy version of maybe
maybe' : b -> (a -> b) -> Maybe a -> b
maybe' n j Nothing  = n
maybe' n j (Just x) = j x

subs : Unifier -> Term -> Term
subs u (Var x)   = maybe' (Var x) id (lookup x u)
subs u (Comp n ts) = Comp n (map (subs u) ts)

compose : Unifier -> Unifier -> Unifier
compose u1 u2 = (map (\(v, t) => (v, subs u2 t)) u1) ++ u2

occursIn : Variable -> Term -> Bool
occursIn v (Var x)     = v == x
occursIn v (Comp _ ms) = any (occursIn v) ms

mutual
  unify : Term -> Term -> Maybe Unifier
  unify (Var "_") t                         = pure []
  unify t (Var "_")                         = pure []
  unify (Var x) (Var y) with (x == y)
     unify (Var x) (Var y) | True           = pure []
  unify (Var x) t with (not (x `occursIn` t))
      unify (Var x) t   | True              = pure [(x, t)]
  unify t v@(Var _)                         = unify v t
  unify (Comp m ms) (Comp n ns) with (m == n)
     unify (Comp m ms) (Comp n ns) | True   = unifyList ms ns
  unify _ _ = Nothing

  unifyList : Terms -> Terms -> Maybe Unifier
  unifyList (t :: ts) (r :: rs) =
      do u1 <- unify t r
         u2 <- unifyList (map (subs u1) ts) (map (subs u1) rs)
  -- Note: I'm not sure if Idris supports backtick notation for operators
         pure $ u1 `compose` u2
  unifyList [] [] = Just []
  unifyList _ _   = Nothing

mutual
  vars : Term -> List Variable
  vars (Var "_") = []
  vars (Var x) = [x]
  vars (Comp _ ts) = varsList ts

  varsList : Terms -> List Variable
  varsList ts = [ v | t <- ts, v <- vars t]

variables : Terms -> List Variable
variables ts = nub $ varsList ts

freshen : List Variable -> (Term, Terms) -> (Term, Terms)
freshen bound (tc, tb) = (subs sub tc, map (subs sub) tb)
    where vars : List Variable
          vars = variables (tc :: tb)
          sub = [ (v, Var $ nextVar 0 v) | v <- vars, v `elem` bound]
	  nextVar : Int -> Variable -> Variable
          nextVar i v = let v' = "_" ++ show i ++ "_" ++ v in
                        if v' `elem` bound then nextVar (i+1) v
                        else v'

data Solution : Type where
    MkSolution : List (Variable, Term) -> Solution

implementation Eq Solution where
    (MkSolution x) == (MkSolution y) = assert_total $ x == y
    x == y = assert_total $ False

Show Solution where
  show (MkSolution [])            = "True"
  show (MkSolution xs ) = (concat $ intersperse "\n" $ map renderBindings xs)
    where renderBindings : (Variable, Term) -> String
          renderBindings (v, t) = v ++ " = " ++ show t

isPlain : List Char -> Bool
isPlain (c :: cs) = isLower c && all (\c => c == '_' || isAlphaNum c) cs
isPlain [] = False
isPlain _ = False

data SearchTree : Type where
  Sol : Solution -> SearchTree
  Node : Goal -> List SearchTree -> SearchTree

Eq SearchTree where
  (Sol x) == (Sol y) = assert_total $ x == y
  (Node x y) == (Node x' y') = assert_total $ (x == x') && (y == y')
  x == y = False

isReportGoal : Term -> Bool
isReportGoal (Comp "_report" _) = True
isReportGoal _                  = False

getSolution : Term -> Solution
getSolution (Comp "_report" args) = MkSolution sol
    where nontriv : (String, Term) -> Bool
          nontriv (x, (Var y)) with (x == y)
	      nontriv (x, (Var y)) | True = False
          nontriv _ = True
	  sol = filter nontriv $ map (\ (Comp "=" [Comp v [], t]) => (v, t)) args
getSolution _ = MkSolution [("ERROR", Var "_Error")]

-- Uses the List monad for backtracking
solve : Program -> Goal -> List SearchTree
solve prog [r] with (isReportGoal r)
    solve prog [r] | True  =  pure $ Sol $ getSolution r
    solve prog [r] | False = []
solve prog g@(t1 :: ts) = pure $ Node g trees
    where trees = do c <- prog
                     let (tc, tsc) = freshen (variables g) c
                     case unify tc t1 of
                       Just u => do
                         let g' = map (subs u) $ tsc ++ ts
                         solve prog g'
                       Nothing => []

makeReportGoal : Terms -> List Term
makeReportGoal goal = [Comp "_report" reportVars]
    where vars : List Variable
          vars = variables goal
	  reportVars : Terms
          reportVars = map (\ v => Comp "=" [Comp v [], Var v]) vars

-- Use the trick of inserting an extra reporting goal
makeReportTree : Program -> Goal -> SearchTree
makeReportTree prog goal = Node goal $ solve prog (goal ++ makeReportGoal goal)

----------------------------------------------------------------------
-- Traveral of Search Trees
----------------------------------------------------------------------

-- Depth first
dfs : SearchTree -> List Solution
dfs (Sol sols) = [sols]
dfs (Node _ st) = [ s | t <- st, s <- dfs t]

-- Breath first
bfs : SearchTree -> List Solution
bfs t = trav [t]
    where trav [] = []
          trav ((Sol x) :: q) = x :: trav q
          trav ((Node _ st)  :: q) = trav (q ++ st)

-- Limited depth first
limitedDfs : Int -> SearchTree -> List Solution
limitedDfs _ (Sol sols)  = [sols]
limitedDfs 0 _           = []
limitedDfs n (Node _ st) = [ s | t <- st, s <- limitedDfs (n-1) t]

-----------------------------------------------------------------------
--- Syntax for the DSL ---
-----------------------------------------------------------------------

-- Note: I might actually want to do something here like apply some
-- function to "h" and "b" here in order to supply some more syntatic
-- sugar.

syntax [h] ":-" [b] = (h, b)

empty : List Term
empty = []

syntax [p] "." = (p, empty)

syntax "?-" [q] = nub $ bfs $ makeReportTree program [q]

max_stars_repo_name: Sintrastes/idr-pure-prolog

max_issues_repo_name: Sintrastes/idr-pure-prolog

max_forks_repo_name: Sintrastes/idr-pure-prolog


text:
module BiNat.Properties.LT

import BiNat
import BiNat.Properties.Plus
import BiNat.Properties.Induction

%access public export
%default total

nIsNotLessThanItself : (n : BiNat) -> Not (LT n n)
nIsNotLessThanItself J         lt = uninhabited {t = LT J J} lt
nIsNotLessThanItself (ns -: n) (JLT ms m) impossible
nIsNotLessThanItself (ns -: n) (LTLeading _ _ _) impossible
nIsNotLessThanItself (ns -: n) (LTAppend ns ns lt n n) = nIsNotLessThanItself ns lt

lessThanImpliesNotEqual : (m, n : BiNat) -> LT m n -> Not (m = n)
lessThanImpliesNotEqual m n lt eq = nIsNotLessThanItself n $ replace {P = \z => LT z n} eq lt

greaterThanImpliesNotEqual : (m, n : BiNat) -> GT m n -> Not (m = n)
greaterThanImpliesNotEqual m n gt = (lessThanImpliesNotEqual n m gt) . sym

lessThanImpliesNotGreaterThan : (m, n : BiNat) -> LT m n -> Not (GT m n)
lessThanImpliesNotGreaterThan J         (ns -: n) (JLT ns n) lt = uninhabited lt
lessThanImpliesNotGreaterThan (ms -: O) (ns -: I) (LTLeading ms ns eq) (LTAppend ns ms lt I O) =
  nIsNotLessThanItself ns (replace eq lt)
lessThanImpliesNotGreaterThan (ms -: I) (ns -: O) (LTAppend ms ns lt I O) (LTLeading ns ms eq) =
  nIsNotLessThanItself ms (replace {P = \z => LT ms z} eq lt)
lessThanImpliesNotGreaterThan (ms -: m) (ns -: n) (LTAppend ms ns lt1 m n) (LTAppend ns ms lt2 n m) =
  lessThanImpliesNotGreaterThan ms ns lt1 lt2

lessThanTransitive : BiNat.LT l m -> LT m n -> LT l n
lessThanTransitive (JLT ms O)               (LTLeading ms ns eq)     = JLT ns I
lessThanTransitive (JLT ms m)               (LTAppend ms ns lt m n)  = JLT ns n
lessThanTransitive (LTLeading ls ms eq)     (LTAppend ms ns lt I n)  =
  LTAppend ls ns (replace {P = \z => BiNat.LT z ns} (sym eq) lt) O n
lessThanTransitive (LTAppend ls ms lt l O)  (LTLeading ms ns eq)     =
  LTAppend ls ns (replace {P = \z => BiNat.LT ls z} eq lt) l I
lessThanTransitive (LTAppend ls ms lt1 l m) (LTAppend ms ns lt2 m n) =
  LTAppend ls ns (lessThanTransitive lt1 lt2) l n

lessThanEqualTransitive : BiNat.LTE l m -> LTE m n -> LTE l n
lessThanEqualTransitive (LTEEqual l m eq1)    (LTEEqual m n eq2)    =
  LTEEqual l n (replace {P = \z => z = n} (sym eq1) eq2)
lessThanEqualTransitive (LTELessThan l m lt1) (LTEEqual m n eq2)    =
  LTELessThan l n (replace {P = \z => LT l z} eq2 lt1)
lessThanEqualTransitive (LTEEqual l m eq1)    (LTELessThan m n lt2) =
  LTELessThan l n (replace {P = \z => LT z n} (sym eq1) lt2)
lessThanEqualTransitive (LTELessThan l m lt1) (LTELessThan m n lt2) =
  LTELessThan l n (lessThanTransitive lt1 lt2)

lessThanEqualAntiSymmetric : (m, n : BiNat) -> LTE m n -> GTE m n -> m = n
lessThanEqualAntiSymmetric m n (LTEEqual m n eq1)    (LTEEqual n m eq2)    = eq1
lessThanEqualAntiSymmetric m n (LTEEqual m n eq1)    (LTELessThan n m lt2) =
  absurd $ nIsNotLessThanItself n (replace {P = \z => LT n z} eq1 lt2)
lessThanEqualAntiSymmetric m n (LTELessThan m n lt1) (LTEEqual n m eq2)    =
  absurd $ nIsNotLessThanItself m (replace {P = \z => LT m z} eq2 lt1)
lessThanEqualAntiSymmetric m n (LTELessThan m n lt1) (LTELessThan n m lt2) =
  absurd $ lessThanImpliesNotGreaterThan m n lt1 lt2

transLTandLTE : BiNat.LT l m -> LTE m n -> LT l n
transLTandLTE lt1 (LTEEqual m n eq)     = rewrite sym eq in lt1
transLTandLTE lt1 (LTELessThan m n lt2) = lessThanTransitive lt1 lt2

transLTEandLT : BiNat.LTE l m -> LT m n -> LT l n
transLTEandLT (LTEEqual l m eq)     lt2 = rewrite eq in lt2
transLTEandLT (LTELessThan l m lt1) lt2 = lessThanTransitive lt1 lt2

lessThanOrGTE : (m, n : BiNat) -> Either (LT m n) (GTE m n)
lessThanOrGTE J         J         = Right $ LTEEqual J J Refl
lessThanOrGTE J         (ns -: n) = Left $ JLT ns n
lessThanOrGTE (ms -: m) J         = Right $ LTELessThan J (ms -: m) (JLT ms m)
lessThanOrGTE (ms -: O) (ns -: O) =
  case lessThanOrGTE ms ns of
    Left lt                      => Left (LTAppend ms ns lt O O)
    Right (LTEEqual ns ms eq)    => Right $ rewrite sym eq in LTEEqual (ns -: O) (ns -: O) Refl
    Right (LTELessThan ns ms gt) => Right $ LTELessThan (ns -: O) (ms -: O) (LTAppend ns ms gt O O)
lessThanOrGTE (ms -: O) (ns -: I) =
  case lessThanOrGTE ms ns of
    Left lt                      => Left (LTAppend ms ns lt O I)
    Right (LTEEqual ns ms eq)    => Left $ rewrite eq in LTLeading ms ms Refl
    Right (LTELessThan ns ms gt) => Right $ LTELessThan (ns -: I) (ms -: O) (LTAppend ns ms gt I O)
lessThanOrGTE (ms -: I) (ns -: O) =
  case lessThanOrGTE ms ns of
    Left lt                      => Left (LTAppend ms ns lt I O)
    Right (LTEEqual ns ms eq)    => Right $ LTELessThan (ns -: O) (ms -: I) (rewrite sym eq in LTLeading ns ns Refl)
    Right (LTELessThan ns ms gt) => Right $ LTELessThan (ns -: O) (ms -: I) (LTAppend ns ms gt O I)
lessThanOrGTE (ms -: I) (ns -: I) =
  case lessThanOrGTE ms ns of
    Left lt                      => Left (LTAppend ms ns lt I I)
    Right (LTEEqual ns ms eq)    => Right $ rewrite sym eq in LTEEqual (ns -: I) (ns -: I) Refl
    Right (LTELessThan ns ms gt) => Right $ LTELessThan (ns -: I) (ms -: I) (LTAppend ns ms gt I I)

lessThanAppended : (n : BiNat) -> (b : Bit) -> LT n (n -: b)
lessThanAppended J         b = JLT J b
lessThanAppended (ns -: n) b = LTAppend ns (ns -: n) (lessThanAppended ns n) n b

succGreaterThanJ : (n : BiNat) -> GT (succ n) J
succGreaterThanJ J         = JLT J O
succGreaterThanJ (ns -: O) = JLT ns I
succGreaterThanJ (ns -: I) = rewrite succDashAppendsAcc ns [O] in JLT (succ ns) O

lessThanSucc : (n : BiNat) -> LT n (succ n)
lessThanSucc J         = JLT J O
lessThanSucc (ns -: O) = LTLeading ns ns Refl
lessThanSucc (ns -: I) =
  replace {P = \z => LT (ns -: I) z} (sym $ succDashAppendsAcc ns [O]) $
  LTAppend ns (succ ns) (lessThanSucc ns) I O

predIsLessThan : (n : BiNat) -> LT J n -> LT (pred n) n
predIsLessThan J _ impossible
predIsLessThan (J -: O)       _ = JLT J O
predIsLessThan (ns -: O -: O) _ =
  replace {P = \z => LT z (ns -: O -: O)} (sym $ predDashAppendsAcc (ns -: O) [I]) $
  LTAppend (pred (ns -: O)) (ns -: O) (predIsLessThan (ns -: O) (JLT ns O)) I O
predIsLessThan (ns -: I -: O) _ = LTAppend (ns -: O) (ns -: I) (LTLeading ns ns Refl) I O
predIsLessThan (ns -: I)      _ = LTLeading ns ns Refl

predLessThanEqual : (n : BiNat) -> LTE (pred n) n
predLessThanEqual J              = LTEEqual J J Refl
predLessThanEqual (J -: O)       = LTELessThan J (J -: O) (JLT J O)
predLessThanEqual (ns -: n -: O) =
  rewrite predDashAppendsAcc (ns -: n) [I] in
  let lt = predIsLessThan (ns -: n) (JLT ns n) in
  LTELessThan (pred (ns -: n) -: I) (ns -: n -: O) (LTAppend (pred (ns -: n)) (ns -: n) lt I O)
predLessThanEqual (ns -: I)      = LTELessThan (ns -: O) (ns -: I) (LTLeading ns ns Refl)

lessThanImpliesLTEPred : (m, n : BiNat) -> LT m n -> LTE m (pred n)
lessThanImpliesLTEPred m J lt impossible
lessThanImpliesLTEPred J (J -: O)       _ = LTEEqual J J Refl
lessThanImpliesLTEPred J (ns -: O -: O) _ =
  replace {P = \z => LTE J z} (sym $ predDashAppendsAcc (ns -: O) [I]) $
  LTELessThan J (pred (ns -: O) -: I) (JLT (pred (ns -: O)) I)
lessThanImpliesLTEPred J (ns -: I -: O) _ = LTELessThan J (ns -: O -: I) (JLT (ns -: O) I)
lessThanImpliesLTEPred J (ns -: I)      _ = LTELessThan J (ns -: O) (JLT ns O)
lessThanImpliesLTEPred (ms -: O) (ns -: O) (LTAppend ms ns lt O O) =
  case ns of
    J          => absurd (uninhabited lt)
    (ns2 -: n) =>
      replace {P = \z => LTE (ms -: O) z} (sym $ predDashAppendsAcc (ns2 -: n) [I]) $
      case lessThanImpliesLTEPred ms (ns2 -: n) lt of
        LTEEqual _ _ eq =>
          replace {P = \z => LTE (ms -: O) (z -: I)} eq (LTELessThan (ms -: O) (ms -: I) (LTLeading ms ms Refl))
        LTELessThan _ _ lt2 =>
          LTELessThan (ms -: O) (pred (ns2 -: n) -: I) (LTAppend ms (pred (ns2 -: n)) lt2 O I)
lessThanImpliesLTEPred (ms -: O) (ns -: I) (LTLeading ms ns eq) =
  LTEEqual (ms -: O) (ns -: O) (rewrite eq in Refl)
lessThanImpliesLTEPred (ms -: O) (ns -: I) (LTAppend ms ns lt O I) =
  LTELessThan (ms -: O) (ns -: O) (LTAppend ms ns lt O O)
lessThanImpliesLTEPred (ms -: I) (J -: O) (LTAppend ms J lt I O) impossible
lessThanImpliesLTEPred (ms -: I) (ns -: n -: O) (LTAppend ms (ns -: n) lt I O) =
  replace {P = \z => LTE (ms -: I) z} (sym $ predDashAppendsAcc (ns -: n) [I]) $
  case lessThanImpliesLTEPred ms (ns -: n) lt of
    LTEEqual _ _ eq =>
      replace {P = \z => LTE (ms -: I) (z -: I)} eq (LTEEqual (ms -: I) (ms -: I) Refl)
    LTELessThan _ _ lt2 =>
      LTELessThan (ms -: I) (pred (ns -: n) -: I) (LTAppend ms (pred (ns -: n)) lt2 I I)
lessThanImpliesLTEPred (ms -: I) (ns -: I) (LTAppend ms ns lt I I) =
  LTELessThan (ms -: I) (ns -: O) (LTAppend ms ns lt I O)

lessThanImpliesSuccLTE : (m, n : BiNat) -> LT m n -> LTE (succ m) n
lessThanImpliesSuccLTE m         J lt impossible
lessThanImpliesSuccLTE J         (J -: O)       (JLT J O) = LTEEqual (J -: O) (J -: O) Refl
lessThanImpliesSuccLTE J         (J -: I)       (JLT J I) =
  LTELessThan (J -: O) (J -: I) (LTLeading J J Refl)
lessThanImpliesSuccLTE J         (ns -: n -: O) lt        =
  LTELessThan (J -: O) (ns -: n -: O) (LTAppend J (ns -: n) (JLT ns n) O O)
lessThanImpliesSuccLTE J         (ns -: n -: I) lt        =
  LTELessThan (J -: O) (ns -: n -: I) (LTAppend J (ns -: n) (JLT ns n) O I)
lessThanImpliesSuccLTE (ms -: O) (ns -: O)      (LTAppend ms ns lt O O) =
  LTELessThan (ms -: I) (ns -: O) (LTAppend ms ns lt I O)
lessThanImpliesSuccLTE (ms -: O) (ns -: I)      (LTLeading ms ns eq) =
  LTEEqual (ms -: I) (ns -: I) (rewrite eq in Refl)
lessThanImpliesSuccLTE (ms -: O) (ns -: I)      (LTAppend ms ns lt O I) =
  LTELessThan (ms -: I) (ns -: I) (LTAppend ms ns lt I I)
lessThanImpliesSuccLTE (ms -: I) (ns -: O)      (LTAppend ms ns lt I O) =
  rewrite succDashAppendsAcc ms [O] in
  case lessThanImpliesSuccLTE ms ns lt of
    LTEEqual _ _ eq =>
      rewrite eq in LTEEqual (ns -: O) (ns -: O) Refl
    LTELessThan _ _ lt2 =>
      LTELessThan (succ ms -: O) (ns -: O) (LTAppend (succ ms) ns lt2 O O)
lessThanImpliesSuccLTE (ms -: I) (ns -: I)      (LTAppend ms ns lt I I) =
  rewrite succDashAppendsAcc ms [O] in
  case lessThanImpliesSuccLTE ms ns lt of
    LTEEqual _ _ eq =>
      rewrite eq in LTELessThan (ns -: O) (ns -: I) (LTLeading ns ns Refl)
    LTELessThan _ _ lt2 =>
      LTELessThan (succ ms -: O) (ns -: I) (LTAppend (succ ms) ns lt2 O I)

succKeepsLessThan : (m, n : BiNat) -> LT m n -> LT (succ m) (succ n)
succKeepsLessThan m         J              lt impossible
succKeepsLessThan J         (J -: O)       lt = LTLeading J J Refl
succKeepsLessThan J         (ns -: n -: O) lt = LTAppend J (ns -: n) (JLT ns n) O I
succKeepsLessThan J         (J -: I)       lt = LTAppend J (J -: O) (JLT J O) O O
succKeepsLessThan J         (ns -: n -: I) lt =
  rewrite succDashAppendsAcc (ns -: n) [O] in
  LTAppend J (succ (ns -: n)) (lessThanTransitive (JLT ns n) (lessThanSucc (ns -: n))) O O
succKeepsLessThan (ms -: O) (ns -: O)      (LTAppend ms ns lt O O) = LTAppend ms ns lt I I
succKeepsLessThan (ms -: O) (ns -: I)      (LTLeading ms ns eq) =
  rewrite sym eq in
  rewrite succDashAppendsAcc ms [O] in
  LTAppend ms (succ ms) (lessThanSucc ms) I O
succKeepsLessThan (ms -: O) (ns -: I)      (LTAppend ms ns lt O I) =
  rewrite succDashAppendsAcc ns [O] in
  LTAppend ms (succ ns) (lessThanTransitive lt (lessThanSucc ns)) I O
succKeepsLessThan (ms -: I) (ns -: O)      (LTAppend ms ns lt I O) =
  rewrite succDashAppendsAcc ms [O] in
  case lessThanImpliesSuccLTE ms ns lt of
    LTEEqual _ _ eq     => rewrite eq in LTLeading ns ns Refl
    LTELessThan _ _ lt2 => LTAppend (succ ms) ns lt2 O I
succKeepsLessThan (ms -: I) (ns -: I)      (LTAppend ms ns lt I I) =
  rewrite succDashAppendsAcc ms [O] in
  rewrite succDashAppendsAcc ns [O] in
  LTAppend (succ ms) (succ ns) (succKeepsLessThan ms ns lt) O O

plusNKeepsLessThan : (l, m : BiNat) -> LT l m -> (n : BiNat) -> LT (plus l n) (plus m n)
plusNKeepsLessThan l m lt n =
  induction
    (\k => LT (plus l k) (plus m k))
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite plusAssociative l k J in
      rewrite plusAssociative m k J in
      rewrite plusJIsSucc (plus l k) in
      rewrite plusJIsSucc (plus m k) in
      succKeepsLessThan (plus l k) (plus m k) pk
    )
    (rewrite plusJIsSucc l in rewrite plusJIsSucc m in succKeepsLessThan l m lt)
    n

succsRecoversLessThan : (m, n : BiNat) -> LT (succ m) (succ n) -> LT m n
succsRecoversLessThan m n lt =
  case
    replace {P = \z => LTE (succ m) z} (predOfSucc n) $
    lessThanImpliesLTEPred (succ m) (succ n) lt
  of
    LTEEqual _ _ eq =>
      rewrite sym eq in lessThanSucc m
    LTELessThan _ _ lt2 =>
      lessThanTransitive (lessThanSucc m) lt2

lessThanImpliesLTEOfPreds : (m, n : BiNat) -> LT m n -> LTE (pred m) (pred n)
lessThanImpliesLTEOfPreds J         (J -: O)       lt = LTEEqual J J Refl
lessThanImpliesLTEOfPreds J         (ns -: n -: O) lt =
  rewrite predDashAppendsAcc (ns -: n) [I] in
  LTELessThan J (pred (ns -: n) -: I) (JLT (pred (ns -: n)) I)
lessThanImpliesLTEOfPreds J         (ns -: I)      lt = LTELessThan J (ns -: O) (JLT ns O)
lessThanImpliesLTEOfPreds (ms -: m) ns             lt =
  lessThanEqualTransitive
    (LTELessThan (pred (ms -: m)) (ms -: m) (predIsLessThan (ms -: m) (JLT ms m)))
    (lessThanImpliesLTEPred (ms -: m) ns lt)

predKeepsLessThan : (m, n : BiNat) -> LT J m -> LT m n -> LT (pred m) (pred n)
predKeepsLessThan m n jltm lt =
  case lessThanImpliesLTEOfPreds m n lt of
    LTEEqual (pred m) (pred n) eq =>
      let nIsNotJ = greaterThanImpliesNotEqual n J (lessThanTransitive jltm lt) in
      let mIsNotJ = greaterThanImpliesNotEqual m J jltm in
      let mEQn = replace {P = \z => m = z} (succOfPred n nIsNotJ) $
                 replace {P = \z => z = succ (pred n)} (succOfPred m mIsNotJ) $
                 replace {P = \z => succ (pred m) = succ z} eq Refl in
      absurd $ lessThanImpliesNotEqual m n lt mEQn
    LTELessThan (pred m) (pred n) lt =>
      lt

predRecoversLT : (m, n : BiNat) -> LT (pred m) (pred n) -> LT m n
predRecoversLT m         J         lt impossible
predRecoversLT J         (ns -: n) lt = JLT ns n
predRecoversLT (ms -: m) (ns -: n) lt =
  rewrite sym $ succOfPred (ms -: m) uninhabited in
  rewrite sym $ succOfPred (ns -: n) uninhabited in
  succKeepsLessThan (pred (ms -: m)) (pred (ns -: n)) lt

lessThanPlus : (m, n : BiNat) -> LT m (plus n m)
lessThanPlus m n =
  induction
    (\k => LT m (plus k m))
    (\k, pk =>
      replace {P = \z => LT m (plus z m)} (jPlusIsSucc k) $
      replace {P = \z => LT m z} (plusAssociative J k m) $
      replace {P = \z => LT m z} (sym $ jPlusIsSucc (plus k m)) $
      lessThanTransitive pk (lessThanSucc (plus k m))
    )
    (replace (sym $ jPlusIsSucc m) (lessThanSucc m))
    n

completeInduction :
  (P : BiNat -> Type) ->
  ((k : BiNat) -> ((m : BiNat) -> LT m k -> P m) -> P k) ->
  (n : BiNat) -> P n
completeInduction prop trans n =
  trans n $ induction
    (\k => (m : BiNat) -> LT m k -> prop m)
    (\k, pk, m, lt =>
      case lessThanImpliesLTEPred m (succ k) lt of
        LTEEqual _ _ eq =>
          rewrite eq in rewrite predOfSucc k in trans k pk
        LTELessThan _ _ lt2 =>
          pk m (replace (predOfSucc k) lt2)
    )
    (\m, lt => absurd (uninhabited lt))
    n

compareSelf : (m, n : BiNat) -> m = n -> (last : Ordering) -> compare' m n last = last
compareSelf m J         eq last = rewrite eq in Refl
compareSelf m (ns -: O) eq last = rewrite eq in compareSelf ns ns Refl last
compareSelf m (ns -: I) eq last = rewrite eq in compareSelf ns ns Refl last

compareLT : (m, n : BiNat) -> LT m n -> (last : Ordering) -> compare' m n last = LT
compareLT m         J         _                       _    impossible
compareLT J         (ns -: n) _                       _    = Refl
compareLT (ms -: O) (ns -: O) (LTAppend ms ns lt O O) last = compareLT ms ns lt last
compareLT (ms -: O) (ns -: I) (LTAppend ms ns lt O I) last = compareLT ms ns lt LT
compareLT (ms -: O) (ns -: I) (LTLeading ms ns eq)    last = rewrite eq in compareSelf ns ns Refl LT
compareLT (ms -: I) (ns -: O) (LTAppend ms ns lt I O) last = compareLT ms ns lt GT
compareLT (ms -: I) (ns -: I) (LTAppend ms ns lt I I) last = compareLT ms ns lt last

compareGT : (m, n : BiNat) -> GT m n -> (last : Ordering) -> compare' m n last = GT
compareGT J         n         _                       _    impossible
compareGT (ms -: m) J         _                       _    = Refl
compareGT (ms -: O) (ns -: O) (LTAppend ns ms gt O O) last = compareGT ms ns gt last
compareGT (ms -: O) (ns -: I) (LTAppend ns ms gt I O) last = compareGT ms ns gt LT
compareGT (ms -: I) (ns -: O) (LTAppend ns ms gt O I) last = compareGT ms ns gt GT
compareGT (ms -: I) (ns -: O) (LTLeading ns ms eq)    last = rewrite eq in compareSelf ms ms Refl GT
compareGT (ms -: I) (ns -: I) (LTAppend ns ms gt I I) last = compareGT ms ns gt last

-- These should be in Prelude.Interfaces
Uninhabited (EQ = LT) where
  uninhabited Refl impossible
Uninhabited (EQ = GT) where
  uninhabited Refl impossible
Uninhabited (LT = EQ) where
  uninhabited Refl impossible
Uninhabited (Prelude.Interfaces.LT = GT) where
  uninhabited Refl impossible
Uninhabited (GT = EQ) where
  uninhabited Refl impossible
Uninhabited (Prelude.Interfaces.GT = LT) where
  uninhabited Refl impossible

compareRecoversEQ : (m, n : BiNat) -> compare m n = EQ -> m = n
compareRecoversEQ m n eq =
  case lessThanOrGTE m n of
    Left lt                    => absurd $ uninhabited $ trans (sym eq) (compareLT m n lt EQ)
    Right (LTEEqual n m eq2)   => sym eq2
    Right (LTELessThan n m gt) => absurd $ uninhabited $ trans (sym eq) (compareGT m n gt EQ)

compareRecoversLT : (m, n : BiNat) -> compare m n = LT -> LT m n
compareRecoversLT m n eq =
  case lessThanOrGTE m n of
    Left lt                    => lt
    Right (LTEEqual n m eq2)   => absurd $ uninhabited $ trans (sym eq) (compareSelf m n (sym eq2) EQ)
    Right (LTELessThan n m gt) => absurd $ uninhabited $ trans (sym eq) (compareGT m n gt EQ)

compareRecoversGT : (m, n : BiNat) -> compare m n = GT -> GT m n
compareRecoversGT m n eq =
  case lessThanOrGTE n m of
    Left gt                    => gt
    Right (LTEEqual m n eq2)   => absurd $ uninhabited $ trans (sym eq) (compareSelf m n eq2 EQ)
    Right (LTELessThan m n lt) => absurd $ uninhabited $ trans (sym eq) (compareLT m n lt EQ)

ext: idr

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
> module NonNegDouble.Predicates

> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import Double.Predicates

> %default total
> %access public export
> %auto_implicits off

> ||| Proofs that `x` is less than or equal to `y`
> ||| @ x the smaller number
> ||| @ y the larger number
> LTE : (x, y : NonNegDouble) -> Type
> LTE x y = LTE (toDouble x) (toDouble y)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Solutions.Functions1

--------------------------------------------------------------------------------
--          Exercise 1
--------------------------------------------------------------------------------

square : Integer -> Integer
square n = n * n

testSquare : (Integer -> Bool) -> Integer -> Bool
testSquare fun = fun . square

twice : (Integer -> Integer) -> Integer -> Integer
twice f = f . f

--------------------------------------------------------------------------------
--          Exercise 2
--------------------------------------------------------------------------------

isEven : Integer -> Bool
isEven n = (n `mod` 2) == 0

isOdd : Integer -> Bool
isOdd = not . isEven

--------------------------------------------------------------------------------
--          Exercise 3
--------------------------------------------------------------------------------

isSquareOf : Integer -> Integer -> Bool
isSquareOf n x = n == x * x

--------------------------------------------------------------------------------
--          Exercise 4
--------------------------------------------------------------------------------

isSmall : Integer -> Bool
isSmall n = n <= 100

--------------------------------------------------------------------------------
--          Exercise 5
--------------------------------------------------------------------------------

absIsSmall : Integer -> Bool
absIsSmall = isSmall . abs

--------------------------------------------------------------------------------
--          Exercise 6
--------------------------------------------------------------------------------

and : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool
and f1 f2 n = f1 n && f2 n

or : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool
or f1 f2 n = f1 n || f2 n

negate : (Integer -> Bool) -> Integer -> Bool
negate f = not . f

--------------------------------------------------------------------------------
--          Exercise 7
--------------------------------------------------------------------------------

(&&) : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool
(&&) = and

(||) : (Integer -> Bool) -> (Integer -> Bool) -> Integer -> Bool
(||) = or

not : (Integer -> Bool) -> Integer -> Bool
not = negate


text:
module Idris.Doc.Annotations

import Core.Metadata
import Core.Name

import Idris.Pretty

%default total

public export
data IdrisDocAnn
  = Header
  | Deprecation
  | Declarations
  | Decl Name
  | DocStringBody
  | UserDocString
  | Syntax IdrisSyntax

export
-- TODO: how can we deal with bold & so on?
docToDecoration : IdrisDocAnn -> Maybe Decoration
docToDecoration (Syntax syn) = syntaxToDecoration syn
docToDecoration _ = Nothing

export
styleAnn : IdrisDocAnn -> AnsiStyle
styleAnn Header        = underline
styleAnn Deprecation   = bold
styleAnn Declarations  = []
styleAnn (Decl{})      = []
styleAnn DocStringBody = []
styleAnn UserDocString = []
styleAnn (Syntax syn)  = syntaxAnn syn

export
tCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
tCon n = annotate (Syntax $ TCon (Just n))

export
dCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
dCon n = annotate (Syntax $ DCon (Just n))

export
fun : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
fun n = annotate (Syntax $ Fun n)

export
header : Doc IdrisDocAnn -> Doc IdrisDocAnn
header d = annotate Header d <+> colon


text:
module Flutter.Widgets.Stateless

import Dart.FFI
import Flutter.FFI

%inline
public export
Stateless : Type
Stateless = Struct "_Stateless,
import 'package:flutter/material.dart' as material;

class _Stateless extends material.StatelessWidget {
  final material.Widget Function(material.BuildContext) onBuild;
  _Stateless({material.Key key, this.onBuild}) : super(key: key);
  @$.override
  material.Widget build(material.BuildContext context) {
    return onBuild(context);
  }
}
" []

public export
IsAssignableFrom Widget Stateless where

namespace Stateless

  namespace New

    public export
    data Tag : Type where

    %inline
    public export
    key : Parameter Tag
    key = mkParameter "key" Key

    %inline
    public export
    onBuild : Parameter Tag
    onBuild = mkParameter "onBuild" (BuildContext -> IO Widget)

    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [
      Stateless.New.key,
      Stateless.New.onBuild
    ]

  %inline
  public export
  new : Stateless.New.NamedParameters -> IO Stateless
  new ps = primIO (prim__dart_new Stateless [] ps)


text:
module CompoInt2Float

import Int2Str

-- This function is used to fill the hole that the registry is
-- supposed fill by returning the service and procedure implementing a
-- given type signature.
export
registry_hole_filler : a -> b

-- int2float is defined using the registry hole filler.  Basically
-- assuming (Registry.retrieve (String -> Double)) would return a
-- function with such type signature, then int2float can be
-- implemented as
--
-- (Registry.retrieve (String -> Double)) . int2str
export
int2float : Int -> Double
int2float = registry_hole_filler . Int2Str.int2str

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Control.Effect.Writer

import Control.EffectAlgebra

import Control.Monad.Writer

||| Writer effect.
public export
data WriterE : Type -> (Type -> Type) -> Type -> Type where
  Tell : w -> WriterE w m ()

export
Functor (\w => WriterE w m a) where
  map f (Tell x) = Tell (f x)

||| Write the value to the context within a monadic computation that supports it.
public export
tell : Inj (WriterE w) sig => Algebra sig m => w -> m ()
tell s = send (Tell s)

namespace Algebra
  ||| Successive writes overwrite the preceding state.
  public export
  [Overwrite] Algebra sig m => Algebra (WriterE s :+: sig) (WriterT s m) where
    alg ctx hdl (Inl (Tell s)) = MkWriterT $ \_ => pure (ctx, s)
    alg ctxx hdl (Inr x) = MkWriterT $ \r => do
     res <- alg
       {f = Functor.Compose @{(Functor.LeftPair, %search)}}
       (ctxx, r) h x
     pure res
     where
      h : Handler ((,s) . ctx) n m
      h =
         (~<~) {g = Functor.LeftPair}
          {ctx1 = (,s), ctx2 = ctx}
          {l = n}
          {m = WriterT s m} {n = m} (uncurry unWriterT) hdl

  ||| Newer writes are concatenated from the left, via the `Monoid` instance.
  public export
  [ConcatLeft] Monoid s => Algebra sig m => Algebra (WriterE s :+: sig) (WriterT s m) where
    alg ctxx hdl (Inl (Tell s)) = MkWriterT $ \s' => pure (ctxx, (s <+> s'))
    alg ctxx hdl (Inr x) = MkWriterT $ \r => do
     -- hdl : Hander ctx n (WriterT s m)
     -- h : Handler (,s) (WriterT s m) m
     -- h ~<~ hdl : Handler ((, s) . ctx) n m
     res <- alg
       {f = Functor.Compose @{(Functor.LeftPair, %search)}}
       (ctxx, r) h x
     pure res
     where
      h : Handler ((,s) . ctx) n m
      h =
         (~<~) {g = Functor.LeftPair}
          {ctx1 = (,s), ctx2 = ctx}
          {l = n}
          {m = WriterT s m} {n = m} (uncurry unWriterT) hdl


text:
module chap06_printf

-- intermediate type
data Format = Number Format     -- %d
            | Str Format        -- %s
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number f) = (i : Int) -> PrintfType f
PrintfType (Str f) = (str : String) -> PrintfType f
PrintfType (Lit s f) = PrintfType f
PrintfType End = String

-- helper function
printfFmt : (f : Format) -> (acc : String) -> PrintfType f
printfFmt (Number f) acc = \i => printfFmt f (acc ++ show i)
printfFmt (Str f) acc = \str => printfFmt f (acc ++ str)
printfFmt (Lit s f) acc = printfFmt f (acc ++ s)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars)        = Lit "%" (toFormat chars)
toFormat (c :: chars)          = case toFormat chars of
                                      Lit lit chars' => Lit (strCons c lit) chars'
                                      fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

-- *chap06_printf> :t printf
-- printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
-- *chap06_printf> printf "hey, %s"
-- \str => prim__concat "hey, " str : String -> String
-- *chap06_printf> printf "hey, %s" "you"
-- "hey, you" : String


text:
module Test.Data.CatList

import Test.Assert
import Data.CatQueue
import Data.CatList

%access public export

-------------------------------------------------------------------------------

foo : CatList Nat
foo =
  CatCons 1
    (MkCatQueue
      [(CatCons 2
          (MkCatQueue
            [(CatCons 3 (MkCatQueue [] []))]
            [])
      )]
      [])

showFoo : IO ()
showFoo =
  assertEq
    (show foo)
    "CatCons 1 MkCatQueue [CatCons 2 MkCatQueue [CatCons 3 MkCatQueue [] []] []] []"

max_stars_repo_name: Risto-Stevcev/idris-catenatable-lists

max_issues_repo_name: Risto-Stevcev/idris-catenable-lists

max_forks_repo_name: Risto-Stevcev/idris-catenatable-lists


text:
-- -------------------------------------------------------------- [ Common.idr ]
-- Module    : Common.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Writer.Common

import Effects
import Effect.Exception
import Effect.File
import Effect.StdIO

import Text.Markup.Edda.Model

%access export
-- -------------------------------------------------------------------- [ Body ]

strFromMaybe : (a -> String) -> Maybe a -> String
strFromMaybe f Nothing  = "EMPTY"
strFromMaybe f (Just x) = f x

writeEddaFileE : (Edda DOC -> String)
              -> String
              -> Edda DOC
              -> Eff (FileOpSuccess) [FILE ()]
writeEddaFileE write fname doc = writeFile fname (write doc)

writeEddaFile : (Edda DOC -> String)
             -> String
             -> Edda DOC
             -> IO (Either FileError ())
writeEddaFile write fname doc = writeFile fname (write doc)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
> module Nat.LTProperties

> import Nat.BasicProperties
> import Nat.LTEProperties

> %default total
> %auto_implicits on
> %access export
> -- %access public export

|LT| is unique:

> ||| LT is unique
> uniqueLT : (p1 : LT m n) -> (p2 : LT m n) -> p1 = p2
> uniqueLT {m} {n} = uniqueLTE {m = S m} {n = n}
> %freeze uniqueLT

> |||
> uniqueLT' : m1 = m2 -> n1 = n2 -> (p1 : LT m1 n1) -> (p2 : LT m2 n2) -> p1 = p2
> uniqueLT' Refl Refl p1 p2 = uniqueLT p1 p2
> %freeze uniqueLT'

|LT| is decidable:

> ||| LT is decidable
> decLT : (m : Nat) -> (n : Nat) -> Dec (LT m n)
> decLT m n = decLTE (S m) n
> %freeze decLT

Properties of |LT| and successor:

> |||
> ltLemma1 : (m : Nat) -> (n : Nat) -> LT (S m) n -> LT m n
> ltLemma1 m n prf = lteLemma1 (S m) n prf
> %freeze ltLemma1

> ||| LT is contained in LTE
> ltInLTE : (m : Nat) -> (n : Nat) -> LT m n -> LTE m n
> ltInLTE = lteLemma1
> %freeze ltInLTE

> ||| Zero is smaller than any successor
> ltZS : (m : Nat) -> LT Z (S m)
> ltZS  Z    = LTESucc LTEZero
> ltZS (S m) = idSuccPreservesLTE (S Z) (S m) (ltZS m)
> %freeze ltZS

> ||| Zero is smaller than any successor
> ltZS' : {n : Nat} -> LT Z (S n)
> ltZS' {n = Z}   = LTESucc LTEZero
> ltZS' {n = S m} = idSuccPreservesLTE (S Z) (S m) ltZS'
> %freeze ltZS'

> ||| Any number is smaller than its successor
> ltIdS : (m : Nat) -> LT m (S m)
> ltIdS  Z    = LTESucc LTEZero
> ltIdS (S m) = LTESucc (ltIdS m)
> %freeze ltIdS

> ||| Any number which is not zero is greater than zero
> notZisgtZ : {n : Nat} -> Not (n = Z) -> LT Z n
> notZisgtZ {n = Z}   contra = void (contra Refl)
> notZisgtZ {n = S m} _      = ltZS m
> %freeze notZisgtZ

> ||| Any number which is greater than zero is not zero
> gtZisnotZ : {n : Nat} -> LT Z n -> Not (n = Z)
> gtZisnotZ {n = Z}   p = absurd p
> gtZisnotZ {n = S m} p = SIsNotZ
> %freeze gtZisnotZ

> ||| No number is less than zero
> notLTzero : {n : Nat} -> Not (LT n Z)
> notLTzero = succNotLTEzero
> %freeze notLTzero

> |||
> strengthenLT : (m : Nat) -> (n : Nat) -> LT m (S n) -> Not (m = n) -> LT m n
> strengthenLT  Z       n  _       zNEQn   = notZisgtZ (zNEQn . sym)
> strengthenLT (S m)  Z    smLTsz  _       = void (notLTzero (fromLteSucc smLTsz))
> strengthenLT (S m) (S n) smLTssn smNEQsn = LTESucc mLTn where
>   mLTsn : LT m (S n)
>   mLTsn = fromLteSucc smLTssn
>   mNEQn : Not (m = n)
>   mNEQn = predInjective m n smNEQsn
>   mLTn : LT m n
>   mLTn = strengthenLT m n mLTsn mNEQn
> %freeze strengthenLT

> {-

> ---}


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 11, section 3, part 1

import Data.Primitives.Views
import System

-- check that all functions are total
%default total

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                (seed' `shiftR` 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound num with (divides num 12)
      bound ((12 * div) + rem) | (DivBy prf) = rem + 1

data LazyFuel = LDry | LMore (Lazy LazyFuel)

partial
forever : LazyFuel
forever = LMore forever

data RunIO : Type -> Type where
  Quit : a -> RunIO a
  Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b

(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b
(>>=) = Do

run : LazyFuel -> RunIO a -> IO (Maybe a)
run _ (Quit value) = pure $ Just value
run LDry (Do act gen) = pure Nothing
run (LMore fuel) (Do act gen) = do res <- act
                                   run fuel $ gen res

greet : RunIO ()
greet = do putStr "Enter your name: "
           name <- getLine
           if name == ""
             then do putStrLn "Bye bye!"
                     Quit ()
             else do putStrLn $ "Hello " ++ name
                     greet

partial
main : IO ()
main = do run forever greet
          pure ()

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
||| Interface implementations for lazy values.
||| This module should be imported when automatically
||| deriving interface implementations of data types
||| containing `Lazy` fields.
module Data.Lazy

%default total

public export
Eq a => Eq (Lazy a) where
  x == y = x == y

public export
Ord a => Ord (Lazy a) where
  compare x y = compare x y

public export
Semigroup a => Semigroup (Lazy a) where
  x <+> y = x <+> y

public export
Monoid a => Monoid (Lazy a) where
  neutral = neutral

public export
Show a => Show (Lazy a) where
  showPrec p a = showPrec p a

public export
Num a => Num (Lazy a) where
  a + b = a + b
  a * b = a * b
  fromInteger n = fromInteger n

public export
Neg a => Neg (Lazy a) where
  negate a = negate a
  a - b = a - b

public export
Abs a => Abs (Lazy a) where
  abs a = abs a

public export
Fractional a => Fractional (Lazy a) where
  a / b = a / b
  recip a = recip a

public export
Integral a => Integral (Lazy a) where
  a `mod` b = a `mod` b
  a `div` b = a `div` b


text:
module Compiler.Erlang.Codegen.NamedCExpToErlExpr

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.Erlang.Name
import public Compiler.Erlang.IR.ErlExpr
import Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport

import Core.Context
import Core.Name
import Core.TT

import Data.List
import Data.NameMap
import Data.Stream
import Data.Vect

%default total

-- CONSTANTS

genConstant : Constant -> IdrisConstant
genConstant (I x) = IInt x
genConstant (BI x) = IInteger x
genConstant (B8 x) = IB8 x
genConstant (B16 x) = IB16 x
genConstant (B32 x) = IB32 x
genConstant (B64 x) = IB64 x
genConstant (Str x) = IString x
genConstant (Ch x) = IChar x
genConstant (Db x) = IDouble x
genConstant WorldVal = IWorldVal
genConstant IntType = IIntType
genConstant IntegerType = IIntegerType
genConstant Bits8Type = IBits8Type
genConstant Bits16Type = IBits16Type
genConstant Bits32Type = IBits32Type
genConstant Bits64Type = IBits64Type
genConstant StringType = IStringType
genConstant CharType = ICharType
genConstant DoubleType = IDoubleType
genConstant WorldType = IWorldType

-- OPERATORS

genOp : {auto lv : Ref LV LocalVars} -> Line -> PrimFn arity -> Vect arity ErlExpr -> Core ErlExpr
genOp l (Add IntType) [x, y] = pure $ genIntAdd l 63 x y
genOp l (Sub IntType) [x, y] = pure $ genIntSub l 63 x y
genOp l (Mul IntType) [x, y] = pure $ genIntMult l 63 x y
genOp l (Div IntType) [x, y] = pure $ genIntDiv l 63 x y
genOp l (Add Bits8Type) [x, y] = pure $ genIntAdd l 8 x y
genOp l (Sub Bits8Type) [x, y] = pure $ genIntSub l 8 x y
genOp l (Mul Bits8Type) [x, y] = pure $ genIntMult l 8 x y
genOp l (Div Bits8Type) [x, y] = pure $ genIntDiv l 8 x y
genOp l (Add Bits16Type) [x, y] = pure $ genIntAdd l 16 x y
genOp l (Sub Bits16Type) [x, y] = pure $ genIntSub l 16 x y
genOp l (Mul Bits16Type) [x, y] = pure $ genIntMult l 16 x y
genOp l (Div Bits16Type) [x, y] = pure $ genIntDiv l 16 x y
genOp l (Add Bits32Type) [x, y] = pure $ genIntAdd l 32 x y
genOp l (Sub Bits32Type) [x, y] = pure $ genIntSub l 32 x y
genOp l (Mul Bits32Type) [x, y] = pure $ genIntMult l 32 x y
genOp l (Div Bits32Type) [x, y] = pure $ genIntDiv l 32 x y
genOp l (Add Bits64Type) [x, y] = pure $ genIntAdd l 64 x y
genOp l (Sub Bits64Type) [x, y] = pure $ genIntSub l 64 x y
genOp l (Mul Bits64Type) [x, y] = pure $ genIntMult l 64 x y
genOp l (Div Bits64Type) [x, y] = pure $ genIntDiv l 64 x y
genOp l (Add ty) [x, y] = pure $ EOp l "+" x y
genOp l (Sub ty) [x, y] = pure $ EOp l "-" x y
genOp l (Mul ty) [x, y] = pure $ EOp l "*" x y
genOp l (Div IntegerType) [x, y] = pure $ EOp l "div" x y -- NOTE: Is allowed to be partial
genOp l (Div ty) [x, y] = pure $ EOp l "/" x y -- NOTE: Is allowed to be partial
genOp l (Mod ty) [x, y] = pure $ EOp l "rem" x y -- NOTE: Is allowed to be partial
genOp l (Neg ty) [x] = pure $ genFunCall l "erlang" "-" [x]
genOp l (ShiftL IntType) [x, y] = pure $ genIntShiftL l 63 x y
genOp l (ShiftL Bits8Type) [x, y] = pure $ genIntShiftL l 8 x y
genOp l (ShiftL Bits16Type) [x, y] = pure $ genIntShiftL l 16 x y
genOp l (ShiftL Bits32Type) [x, y] = pure $ genIntShiftL l 32 x y
genOp l (ShiftL Bits64Type) [x, y] = pure $ genIntShiftL l 64 x y
genOp l (ShiftL ty) [x, y] = pure $ EOp l "bsl" x y
genOp l (ShiftR ty) [x, y] = pure $ EOp l "bsr" x y
genOp l (BAnd ty) [x, y] = pure $ EOp l "band" x y
genOp l (BOr ty) [x, y] = pure $ EOp l "bor" x y
genOp l (BXOr ty) [x, y] = pure $ EOp l "bxor" x y
genOp l (LT StringType) [x, y] = pure $ genUnicodeStringLT l x y
genOp l (LTE StringType) [x, y] = pure $ genUnicodeStringLTE l x y
genOp l (EQ StringType) [x, y] = pure $ genUnicodeStringEQ l x y
genOp l (GTE StringType) [x, y] = pure $ genUnicodeStringGTE l x y
genOp l (GT StringType) [x, y] = pure $ genUnicodeStringGT l x y
genOp l (LT ty) [x, y] = pure $ genBoolToInt l (EOp l "<" x y)
genOp l (LTE ty) [x, y] = pure $ genBoolToInt l (EOp l "=<" x y)
genOp l (EQ ty) [x, y] = pure $ genBoolToInt l (EOp l "=:=" x y)
genOp l (GTE ty) [x, y] = pure $ genBoolToInt l (EOp l ">=" x y)
genOp l (GT ty) [x, y] = pure $ genBoolToInt l (EOp l ">" x y)
genOp l StrLength [str] = pure $ genUnicodeStringLength l str
genOp l StrHead [str] = pure $ genUnicodeStringHead l str
genOp l StrTail [str] = genUnicodeStringTail l str
genOp l StrIndex [str, index] = pure $ genUnicodeStringIndex l str index
genOp l StrCons [char, str] = pure $ genUnicodeStringCons l char str
genOp l StrAppend [str1, str2] = pure $ genUnicodeStringAppend l str1 str2
genOp l StrReverse [str] = pure $ genUnicodeStringReverse l str
genOp l StrSubstr [start, len, str] = pure $ genUnicodeStringSubstr l start len str

-- `e` is Euler's number, which approximates to: 2.718281828459045
genOp l DoubleExp [x] = pure $ genFunCall l "math" "pow" [EFloat l 2.718281828459045, x] -- Base is `e`
genOp l DoubleLog [x] = pure $ genFunCall l "math" "log" [x] -- Base is `e`
genOp l DoubleSin [x] = pure $ genFunCall l "math" "sin" [x]
genOp l DoubleCos [x] = pure $ genFunCall l "math" "cos" [x]
genOp l DoubleTan [x] = pure $ genFunCall l "math" "tan" [x]
genOp l DoubleASin [x] = pure $ genFunCall l "math" "asin" [x]
genOp l DoubleACos [x] = pure $ genFunCall l "math" "acos" [x]
genOp l DoubleATan [x] = pure $ genFunCall l "math" "atan" [x]
genOp l DoubleSqrt [x] = pure $ genFunCall l "math" "sqrt" [x]
genOp l DoubleFloor [x] = pure $ genFunCall l "erlang" "floor" [x]
genOp l DoubleCeiling [x] = pure $ genFunCall l "erlang" "ceil" [x]

genOp l (Cast IntegerType IntType) [x] = pure $ genIntegerToInt l x
genOp l (Cast IntegerType DoubleType) [x] = pure $ genIntegerToDouble l x
genOp l (Cast IntegerType StringType) [x] = pure $ genIntegerToString l x
genOp l (Cast IntegerType Bits8Type) [x] = pure $ genIntegerToBits l 8 x
genOp l (Cast IntegerType Bits16Type) [x] = pure $ genIntegerToBits l 16 x
genOp l (Cast IntegerType Bits32Type) [x] = pure $ genIntegerToBits l 32 x
genOp l (Cast IntegerType Bits64Type) [x] = pure $ genIntegerToBits l 64 x

genOp l (Cast IntType IntegerType) [x] = pure $ genIntToInteger l x
genOp l (Cast IntType DoubleType) [x] = pure $ genIntToDouble l x
genOp l (Cast IntType CharType) [x] = pure $ genIntToChar l x
genOp l (Cast IntType StringType) [x] = pure $ genIntToString l x

genOp l (Cast DoubleType IntegerType) [x] = pure $ genDoubleToInteger l x
genOp l (Cast DoubleType IntType) [x] = pure $ genDoubleToInt l x
genOp l (Cast DoubleType StringType) [x] = pure $ genDoubleToString l x

genOp l (Cast CharType IntegerType) [x] = pure $ genCharToInteger l x
genOp l (Cast CharType IntType) [x] = pure $ genCharToInt l x
genOp l (Cast CharType StringType) [x] = pure $ genCharToString l x

genOp l (Cast StringType IntegerType) [x] = genStringToInteger l x
genOp l (Cast StringType IntType) [x] = genStringToInt l x
genOp l (Cast StringType DoubleType) [x] = genStringToDouble l x

genOp l (Cast Bits8Type IntType) [x] = pure $ x
genOp l (Cast Bits8Type IntegerType) [x] = pure $ x
genOp l (Cast Bits8Type StringType) [x] = pure $ genIntegerToString l x

genOp l (Cast Bits16Type IntType) [x] = pure $ x
genOp l (Cast Bits16Type IntegerType) [x] = pure $ x
genOp l (Cast Bits16Type StringType) [x] = pure $ genIntegerToString l x

genOp l (Cast Bits32Type IntType) [x] = pure $ x
genOp l (Cast Bits32Type IntegerType) [x] = pure $ x
genOp l (Cast Bits32Type StringType) [x] = pure $ genIntegerToString l x

-- Bits64Type->IntType is omitted because Int may not be big enough to store a 64-bit unsigned integer
genOp l (Cast Bits64Type IntegerType) [x] = pure $ x
genOp l (Cast Bits64Type StringType) [x] = pure $ genIntegerToString l x

genOp l (Cast from to) [x] = pure $ genThrow l ("Invalid cast " ++ show from ++ "->" ++ show to)

genOp l BelieveMe [_, _, x] = pure $ x
genOp l Crash [_, msg] = do
  let crashMsg = EBinaryConcat l (EBinary l "Crash: ") msg
  pure $ genFunCall l "erlang" "throw" [crashMsg]

-- DATA CONSTRUCTORS

genCon : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genCon namespaceInfo l name args = do
  let (NS ns (UN un)) = name
    | _ => pure $ ECon l (constructorName name) args
  case (unsafeUnfoldNamespace ns, un, args) of
    -- List
    (["Types", "Prelude"], "Nil", []) =>
      pure $ ENil l
    (["Types", "Prelude"], "::", [x, xs]) =>
      pure $ ECons l x xs
    -- ErlAtom
    (["Types", "Erlang"], "MkAtom", [x]) =>
      pure $ genUnsafeStringToAtom l x
    -- ErlCharlist
    (["Types", "Erlang"], "MkCharlist", [x]) =>
      pure $ genFunCall l "unicode" "characters_to_list" [x]
    -- ErlNil
    (["MaybeImproperList", "Types", "Erlang"], "Nil", []) =>
      pure $ ENil l
    -- ErlCons
    (["MaybeImproperList", "Types", "Erlang"], "::", [x, y]) =>
      pure $ ECons l x y
    -- ErlList
    (["ProperList", "Types", "Erlang"], "Nil", []) =>
      pure $ ENil l
    (["ProperList", "Types", "Erlang"], "::", [x, xs]) =>
      pure $ ECons l x xs
    -- ErlTuple/A
    (["Types", "Erlang"], "MkTuple0", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple1", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple2", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple3", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple4", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple5", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple6", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple7", args) => pure $ ETuple l args
    (["Types", "Erlang"], "MkTuple8", args) => pure $ ETuple l args
    -- ErlFun/A
    (["Types", "Erlang"], "MkFun0", [fun]) => genUncurry l 0 id fun
    (["Types", "Erlang"], "MkFun1", [fun]) => genUncurry l 1 id fun
    (["Types", "Erlang"], "MkFun2", [fun]) => genUncurry l 2 id fun
    (["Types", "Erlang"], "MkFun3", [fun]) => genUncurry l 3 id fun
    (["Types", "Erlang"], "MkFun4", [fun]) => genUncurry l 4 id fun
    (["Types", "Erlang"], "MkFun5", [fun]) => genUncurry l 5 id fun
    (["Types", "Erlang"], "MkFun6", [fun]) => genUncurry l 6 id fun
    (["Types", "Erlang"], "MkFun7", [fun]) => genUncurry l 7 id fun
    (["Types", "Erlang"], "MkFun8", [fun]) => genUncurry l 8 id fun
    -- ErlIOFun/A
    (["Types", "Erlang"], "MkIOFun0", [fun]) => genUncurry l 0 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun1", [fun]) => genUncurry l 1 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun2", [fun]) => genUncurry l 2 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun3", [fun]) => genUncurry l 3 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun4", [fun]) => genUncurry l 4 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun5", [fun]) => genUncurry l 5 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun6", [fun]) => genUncurry l 6 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun7", [fun]) => genUncurry l 7 (genUnsafePerformIO namespaceInfo l) fun
    (["Types", "Erlang"], "MkIOFun8", [fun]) => genUncurry l 8 (genUnsafePerformIO namespaceInfo l) fun
    -- Default
    _ =>
      pure $ ECon l (constructorName name) args

-- DATA DECONSTRUCTORS

argsToErlMatchers : (args : List LocalVar) -> List (LocalVar, ErlMatcher)
argsToErlMatchers xs = map (\arg => (arg, MAny)) xs

readConAltFun : {auto lv : Ref LV LocalVars} -> Line -> (arity : Nat) -> (funVar : LocalVar) -> ErlExpr -> (transform : ErlExpr -> ErlExpr) -> Core ErlMatcher
readConAltFun l arity funVar body transform = do
  tempVar <- newLocalVar
  let curriedFunMatcher = MTransform MAny tempVar !(genCurry l arity transform (ELocal l tempVar))
  pure $ MTransform curriedFunMatcher funVar body

readConAlt : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> (args : List LocalVar) -> ErlExpr -> Core ErlMatcher
readConAlt namespaceInfo l name args body = do
  let NS ns (UN un) = name
    | _ => pure $ MTaggedTuple (constructorName name) (argsToErlMatchers args) body
  case (unsafeUnfoldNamespace ns, un, args) of
    -- List
    (["Types", "Prelude"], "Nil", []) =>
      pure $ MConst MNil body
    (["Types", "Prelude"], "::", [xVar, xsVar]) =>
      pure $ MCons MAny MAny xVar xsVar body
    -- ErlAtom
    (["Types", "Erlang"], "MkAtom", [xVar]) => do
      tempVar <- newLocalVar
      let convertAtomMatcher = MTransform MAny tempVar (genAtomToString l (ELocal l tempVar))
      pure $ MTransform convertAtomMatcher xVar body
    -- ErlCharlist
    (["Types", "Erlang"], "MkCharlist", [xVar]) => do
      tempVar <- newLocalVar
      let convertCharlistMatcher = MTransform MAny tempVar (genFunCall l "unicode" "characters_to_binary" [ELocal l tempVar])
      pure $ MTransform convertCharlistMatcher xVar body
    -- ErlNil
    (["MaybeImproperList", "Types", "Erlang"], "Nil", []) =>
      pure $ MConst MNil body
    -- ErlCons
    (["MaybeImproperList", "Types", "Erlang"], "::", [xVar, yVar]) =>
      pure $ MCons MAny MAny xVar yVar body
    -- ErlList
    (["ProperList", "Types", "Erlang"], "Nil", []) =>
      pure $ MConst MNil body
    (["ProperList", "Types", "Erlang"], "::", [xVar, xsVar]) =>
      pure $ MCons MAny MAny xVar xsVar body
    -- ErlTuple/A
    (["Types", "Erlang"], "MkTuple0", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple1", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple2", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple3", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple4", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple5", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple6", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple7", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    (["Types", "Erlang"], "MkTuple8", args) =>
      pure $ MTuple (argsToErlMatchers args) body
    -- ErlFun/A
    (["Types", "Erlang"], "MkFun0", [funVar]) =>
      readConAltFun l 0 funVar body id
    (["Types", "Erlang"], "MkFun1", [funVar]) =>
      readConAltFun l 1 funVar body id
    (["Types", "Erlang"], "MkFun2", [funVar]) =>
      readConAltFun l 2 funVar body id
    (["Types", "Erlang"], "MkFun3", [funVar]) =>
      readConAltFun l 3 funVar body id
    (["Types", "Erlang"], "MkFun4", [funVar]) =>
      readConAltFun l 4 funVar body id
    (["Types", "Erlang"], "MkFun5", [funVar]) =>
      readConAltFun l 5 funVar body id
    (["Types", "Erlang"], "MkFun6", [funVar]) =>
      readConAltFun l 6 funVar body id
    (["Types", "Erlang"], "MkFun7", [funVar]) =>
      readConAltFun l 7 funVar body id
    (["Types", "Erlang"], "MkFun8", [funVar]) =>
      readConAltFun l 8 funVar body id
    -- ErlIOFun/A
    (["Types", "Erlang"], "MkIOFun0", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 0 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun1", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 1 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun2", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 2 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun3", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 3 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun4", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 4 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun5", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 5 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun6", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 6 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun7", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 7 funVar body (genMkIO l worldVal)
    (["Types", "Erlang"], "MkIOFun8", [funVar]) => do
      worldVal <- newLocalVar
      readConAltFun l 8 funVar body (genMkIO l worldVal)
    -- Default
    _ =>
      pure $ MTaggedTuple (constructorName name) (argsToErlMatchers args) body

-- EXTERNAL PRIMITIVES

genDecode : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> ErlMatcher -> Core ErlExpr
genDecode l term matcher = do
  tempVar <- newLocalVar
  pure $ EMatcherCase l
    term
    [ MTransform matcher tempVar (genJust l (ELocal l tempVar))
    ]
    (genNothing l)

genDecodeTuple : {auto lv : Ref LV LocalVars} -> Line -> ErlExpr -> (arity : Nat) -> Core ErlExpr
genDecodeTuple l term arity = do
  args <- newLocalVars arity
  genDecode l term $ MTuple (argsToErlMatchers args) (ETuple l (map (ELocal l) args))

genExtPrim : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genExtPrim namespaceInfo l (NS _ (UN "void")) [_, _] =
  pure $ genThrow l "Error: Executed 'void'"
genExtPrim namespaceInfo l (NS _ (UN "prim__os")) [] =
  genOsType l
genExtPrim namespaceInfo l (NS _ (UN "prim__codegen")) [] =
  pure $ EBinary l "erlang"
genExtPrim namespaceInfo l (NS _ (UN "prim__erlUnsafeCall")) [_, ret, modName, fnName, args] = do
  pure $ genFunCall l "erlang" "apply" [genUnsafeStringToAtom l modName, genUnsafeStringToAtom l fnName, args]
genExtPrim namespaceInfo l (NS _ (UN "prim__erlTryCatch")) [_, action, world] = do
  okVar <- newLocalVar
  errorVar <- newLocalVar
  let actionExpr = genUnsafePerformIO namespaceInfo l action
  let body = ETryCatch l actionExpr okVar (genRight l (ELocal l okVar)) errorVar (genLeft l (ELocal l errorVar))
  pure $ genMkIORes l body
genExtPrim namespaceInfo l (NS _ (UN "prim__erlReceive")) [timeout, world] = do
  tempVar <- newLocalVar
  let receive = EReceive l [MTransform MAny tempVar (genJust l (ELocal l tempVar))] timeout (genNothing l)
  pure $ genMkIORes l receive
genExtPrim namespaceInfo l (NS _ (UN "prim__erlModule")) [] =
  pure $ EAtom l (currentModuleName namespaceInfo)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlMatchExact")) [x, y] =
  pure $ genBoolToInt l (EOp l "=:=" x y)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeCodepoint")) [term] =
  genDecode l term MCodepoint
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeInteger")) [term] =
   genDecode l term MInteger
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeDouble")) [term] =
  genDecode l term MFloat
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeAtom")) [term] =
  genDecode l term MAtom
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeBinary")) [term] =
  genDecode l term MBinary
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodePid")) [term] =
  genDecode l term MPid
genExtPrim namespaceInfo l (NS _ (UN "prim__erldecodeReference")) [term] =
  genDecode l term MRef
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodePort")) [term] =
  genDecode l term MPort
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeAnyMap")) [term] =
  genDecode l term MMap
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeAnyList")) [term] =
  genDecode l term MAnyList
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeNil")) [term] =
  genDecode l term MNil
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeCons")) [term] = do
  hdVar <- newLocalVar
  tlVar <- newLocalVar
  genDecode l term $ MCons MAny MAny hdVar tlVar (ECons l (ELocal l hdVar) (ELocal l tlVar))
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple0")) [term] =
  genDecodeTuple l term 0
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple1")) [term] =
  genDecodeTuple l term 1
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple2")) [term] =
  genDecodeTuple l term 2
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple3")) [term] =
  genDecodeTuple l term 3
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple4")) [term] =
  genDecodeTuple l term 4
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple5")) [term] =
  genDecodeTuple l term 5
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple6")) [term] =
  genDecodeTuple l term 6
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple7")) [term] =
  genDecodeTuple l term 7
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeTuple8")) [term] =
  genDecodeTuple l term 8
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun0")) [term] =
  genDecode l term (MFun 0)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun1")) [_, term] =
  genDecode l term (MFun 1)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun2")) [_, _, term] =
  genDecode l term (MFun 2)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun3")) [_, _, _, term] =
  genDecode l term (MFun 3)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun4")) [_, _, _, _, term] =
  genDecode l term (MFun 4)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun5")) [_, _, _, _, _, term] =
  genDecode l term (MFun 5)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun6")) [_, _, _, _, _, _, term] =
  genDecode l term (MFun 6)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun7")) [_, _, _, _, _, _, _, term] =
  genDecode l term (MFun 7)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlDecodeFun8")) [_, _, _, _, _, _, _, _, term] =
  genDecode l term (MFun 8)
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferNew")) [size] =
  pure $ EBufferNew l size
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferResize")) [bin, newSize] =
  pure $ EBufferResize l bin newSize
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferFlatten")) [bin, maxbytes] =
  pure $ EBufferFlatten l bin maxbytes
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetByte")) [bin, loc, value] =
  pure $ EBufferSetBits8 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetByte")) [bin, loc] =
  pure $ EBufferGetBits8 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetBits8")) [bin, loc, value] =
  pure $ EBufferSetBits8 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetBits8")) [bin, loc] =
  pure $ EBufferGetBits8 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetBits16")) [bin, loc, value] =
  pure $ EBufferSetBits16 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetBits16")) [bin, loc] =
  pure $ EBufferGetBits16 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetBits32")) [bin, loc, value] =
  pure $ EBufferSetBits32 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetBits32")) [bin, loc] =
  pure $ EBufferGetBits32 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetBits64")) [bin, loc, value] =
  pure $ EBufferSetBits64 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetBits64")) [bin, loc] =
  pure $ EBufferGetBits64 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetInt32")) [bin, loc, value] =
  pure $ EBufferSetInt32 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetInt32")) [bin, loc] =
  pure $ EBufferGetInt32 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetInt64")) [bin, loc, value] =
  pure $ EBufferSetInt64 l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetInt64")) [bin, loc] =
  pure $ EBufferGetInt64 l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetDouble")) [bin, loc, value] =
  pure $ EBufferSetDouble l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetDouble")) [bin, loc] =
  pure $ EBufferGetDouble l bin loc
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferSetString")) [bin, loc, value] =
  pure $ EBufferSetString l bin loc value
genExtPrim namespaceInfo l (NS _ (UN "prim__erlBufferGetString")) [bin, loc, len] =
  pure $ EBufferGetString l bin loc len
-- genExtPrim namespaceInfo l name args =
--   throw (InternalError ("Badly formed external primitive " ++ show name))
genExtPrim namespaceInfo l name args =
  pure $ genThrow l ("Error: Badly formed external primitive " ++ show name) -- TODO: Should fail at compile-time instead

-- %FOREIGN PRIMITIVES

genForeign : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> Line -> Name -> List ErlExpr -> Core ErlExpr
genForeign namespaceInfo l (NS _ (UN "prim__putStr")) [arg, world] = do
  let putStrCall = genUnicodePutStr l arg
  let retVal = genMkIORes l (genMkUnit l)
  pure $ ESequence l [putStrCall, retVal]
genForeign namespaceInfo l (NS _ (UN "prim__getStr")) [world] = do
  let getStrCall = genUnicodeGetStr l (ECharlist l "")
  pure $ genMkIORes l getStrCall
genForeign namespaceInfo l (NS _ (UN "fastPack")) [xs] = do
  pure $ genFunCall l "unicode" "characters_to_binary" [xs]
genForeign namespaceInfo l (NS _ (UN "fastConcat")) [xs] = do
  pure $ genFunCall l "unicode" "characters_to_binary" [xs] -- TODO: Can this be improved?
-- genForeign namespaceInfo l name args =
--   throw (InternalError ("Unsupported %foreign primitive " ++ show name))
genForeign namespaceInfo l name args =
  pure $ genThrow l ("Error: Unsupported %foreign primitive " ++ show name) -- TODO: Should fail at compile-time instead

-- CODE GENERATION

mutual
  export
  genNmExp : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> NameMap LocalVar -> NamedCExp -> Core ErlExpr
  genNmExp namespaceInfo vs (NmLocal fc name) = do
    let l = genFC fc
    let Just var = lookup name vs
      | Nothing => throw (InternalError ("Missing variable name: " ++ show name))
    pure $ ELocal l var
  genNmExp namespaceInfo vs (NmRef fc name) = do
    let l = genFC fc
    pure $ genRef namespaceInfo l name
  genNmExp namespaceInfo vs (NmLam fc x body) = do
    let l = genFC fc
    (vs', vars) <- addLocalVars [x] vs
    body' <- genNmExp namespaceInfo vs' body
    pure $ ELam l vars body'
  genNmExp namespaceInfo vs (NmLet fc x val body) = do
    let l = genFC fc
    val' <- genNmExp namespaceInfo vs val
    (vs', xVar) <- addLocalVar x vs
    body' <- genNmExp namespaceInfo vs' body
    pure $ ELet l xVar val' body'
  genNmExp namespaceInfo vs (NmApp fc x args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    pure $ EApp l !(genNmExp namespaceInfo vs x) args'
  genNmExp namespaceInfo vs (NmCon fc name tag args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    genCon namespaceInfo l name args'
  genNmExp namespaceInfo vs (NmOp fc op args) = do
    let l = genFC fc
    args' <- assert_total $ traverseVect namespaceInfo vs args
    genOp l op args'
  genNmExp namespaceInfo vs (NmExtPrim fc name args) = do
    let l = genFC fc
    args' <- assert_total $ traverse (genNmExp namespaceInfo vs) args
    genExtPrim namespaceInfo l name args'
  genNmExp namespaceInfo vs (NmForce fc t) = do
    let l = genFC fc
    pure $ EApp l !(genNmExp namespaceInfo vs t) []
  genNmExp namespaceInfo vs (NmDelay fc t) = do
    let l = genFC fc
    pure $ ELam l [] !(genNmExp namespaceInfo vs t)
  genNmExp namespaceInfo vs (NmConCase fc sc alts def) = do
    let l = genFC fc
    sc' <- genNmExp namespaceInfo vs sc
    alts' <- assert_total $ traverse (genConAlt namespaceInfo vs l) alts
    def' <- case def of
          Just defExpr => genNmExp namespaceInfo vs defExpr
          Nothing => pure $ genThrow l "Error: Unreachable branch"
    pure $ EMatcherCase l sc' alts' def'
  genNmExp namespaceInfo vs (NmConstCase fc sc alts def) = do
    let l = genFC fc
    sc' <- genNmExp namespaceInfo vs sc
    alts' <- assert_total $ traverse (genConstAlt namespaceInfo vs) alts
    def' <- case def of
          Just defExpr => genNmExp namespaceInfo vs defExpr
          Nothing => pure $ genThrow l "Error: Unreachable branch"
    pure $ EConstCase l sc' alts' def'
  genNmExp namespaceInfo vs (NmPrimVal fc c) = do
    let l = genFC fc
    pure $ EIdrisConstant l (genConstant c)
  genNmExp namespaceInfo vs (NmErased fc) = do
    let l = genFC fc
    pure $ genErased l
  genNmExp namespaceInfo vs (NmCrash fc msg) = do
    let l = genFC fc
    pure $ genThrow l msg

  traverseVect : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> NameMap LocalVar -> Vect n NamedCExp -> Core (Vect n ErlExpr)
  traverseVect namespaceInfo vs [] = pure []
  traverseVect namespaceInfo vs (arg :: args) = pure $ !(genNmExp namespaceInfo vs arg) :: !(traverseVect namespaceInfo vs args)

  genConAlt : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> NameMap LocalVar -> Line -> NamedConAlt -> Core ErlMatcher
  genConAlt namespaceInfo vs l (MkNConAlt name tag args body) = do
    (vs', vars) <- addLocalVars args vs
    readConAlt namespaceInfo l name vars !(genNmExp namespaceInfo vs' body)

  genConstAlt : {auto lv : Ref LV LocalVars} -> NamespaceInfo -> NameMap LocalVar -> NamedConstAlt -> Core ErlConstAlt
  genConstAlt namespaceInfo vs (MkNConstAlt constant body) =
    pure $ MkConstAlt (genConstant constant) !(genNmExp namespaceInfo vs body)

-- DEFINITIIONS

export
genDef : NamespaceInfo -> Line -> Name -> NamedDef -> Core (Maybe ErlFunDecl)
genDef namespaceInfo l name (MkNmFun args body) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  (vs, vars) <- addLocalVars args empty
  let funDecl = MkFunDecl l Public fnName vars !(genNmExp namespaceInfo vs body)
  pure $ Just funDecl
genDef namespaceInfo l name (MkNmCon tag arity nt) =
  pure Nothing
genDef namespaceInfo l name (MkNmForeign cs args ret) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  vars <- newLocalVars (length args)
  let funDecl = MkFunDecl l Public fnName vars !(genForeign namespaceInfo l name (map (ELocal l) vars))
  pure $ Just funDecl
genDef namespaceInfo l name (MkNmError body) = do
  lv <- newRef LV (initLocalVars "V")
  let (modName, fnName) = moduleNameFunctionName namespaceInfo name
  let funDecl = MkFunDecl l Private fnName [] !(genNmExp namespaceInfo empty body)
  pure $ Just funDecl

-- EXPORTS

data InternalArity = Value | Arity Nat

internalArity : NamedCExp -> InternalArity
internalArity (NmCon fc (NS ns (UN un)) _ _) =
  if ns == erlangTypesNS
    then case un of
      "ETFun" => Arity 1
      "ETErlFun0" => Arity 0
      "ETErlFun1" => Arity 1
      "ETErlFun2" => Arity 2
      "ETErlFun3" => Arity 3
      "ETErlFun4" => Arity 4
      "ETErlFun5" => Arity 5
      "ETErlFun6" => Arity 6
      "ETErlFun7" => Arity 7
      "ETErlFun8" => Arity 8
      "ETErlIOFun0" => Arity 0
      "ETErlIOFun1" => Arity 1
      "ETErlIOFun2" => Arity 2
      "ETErlIOFun3" => Arity 3
      "ETErlIOFun4" => Arity 4
      "ETErlIOFun5" => Arity 5
      "ETErlIOFun6" => Arity 6
      "ETErlIOFun7" => Arity 7
      "ETErlIOFun8" => Arity 8
      _ => Value
    else Value
internalArity _ = Value

externalArity : InternalArity -> Nat
externalArity Value = 0
externalArity (Arity arity) = arity

-- TODO: Do not require name of exported function to be a static string?
export
readExports : NamespaceInfo -> Line -> NamedCExp -> Core (List ErlFunDecl)
readExports namespaceInfo l tm = do
  case tm of
    NmCon fc (NS ns (UN "Fun")) tag [exprTy, NmPrimVal _ (Str fnName), expr] => do
      let True = ns == erlangIONS
        | False => throw (InternalError ("Invalid export: " ++ show tm))
      lv <- newRef LV (initLocalVars "V")
      body <- genNmExp namespaceInfo empty expr -- NOTE: Vars are not relevant to `body`
      let intArity = internalArity exprTy
      let extArity = externalArity intArity
      vars <- newLocalVars extArity
      let invokedBody =
          case intArity of
            Value => body
            Arity arity => EApp l body (genArgsToLocals l vars)
      let funDecl = MkFunDecl l Public fnName vars invokedBody
      pure $ [funDecl]
    NmCon fc (NS ns (UN "Combine")) tag [exports1, exports2] => do
      let True = ns == erlangIONS
        | False => throw (InternalError ("Invalid export: " ++ show tm))
      pure $ !(readExports namespaceInfo l exports1) ++ !(readExports namespaceInfo l exports2)
    _ =>
      throw (InternalError ("Invalid export: " ++ show tm))


text:
module Control.Effect.Fail

import Control.EffectAlgebra
import Control.Monad.Maybe
import Control.Monad.Either

public export
data FailE : Type -> (Type -> Type) -> (Type -> Type) where
  Fail : e -> FailE e m a

export
Functor (\e => FailE e m a) where
  map f (Fail x) = Fail (f x)

||| Fail a computation.
public export
fail : Inj (FailE e) sig => Algebra sig m => e -> m a
fail x = send (Fail x)

public export
fromEither : Inj (FailE e) sig => Algebra sig m => Either e b -> m b
fromEither (Left err) = fail err
fromEither (Right x) = pure x

||| Given a transformation between two failure types `e'` and `e`,
||| run an effectful computation `act` in the context
||| with the transformed failure.
export
glueFail : {0 m : Type -> Type}
        -> {0 e : Type}
        -> (fail : Inj (FailE e) sig)
        => (e' -> e)
        -> ((err : Inj (FailE e') sig) => m a)
        -> m a
glueFail morph act = act @{f}
 where
  f : Inj (FailE e') sig
  f = MkInj $ \case Fail x => inj (Fail (morph x))

namespace Algebra
  public export
  [Maybe] Algebra sig m => Algebra (FailE e :+: sig) (MaybeT m) where
    alg ctx hdl (Inl (Fail x)) = nothing
    alg ctxx hdl (Inr other) =
      let fused = (~<~) {ctx2 = ctx} {m = MaybeT m} f hdl in
      MkMaybeT (alg {f = Functor.Compose} {ctx = Maybe . ctx} (Just ctxx) fused other)
     where
      f : forall a. Maybe (MaybeT m a) -> m (Maybe a)
      f Nothing = pure Nothing
      f (Just x) = runMaybeT x

  public export
  [Either] Algebra sig m => Algebra (FailE e :+: sig) (EitherT e m) where
    alg ctx hdl (Inl (Fail x)) = left x
    alg ctxx hdl (Inr other) =
      let fused = (~<~) {ctx2 = ctx} {m = EitherT e m} f hdl in
      MkEitherT (alg {f = Functor.Compose} {ctx = Either e . ctx} (Right ctxx) fused other)
     where
      f : forall a. Either e (EitherT e m a) -> m (Either e a)
      f (Left x) = pure (Left x)
      f (Right x) = runEitherT x


text:
module Main

import System.Concurrency

main : IO ()
main = do
    sema <- makeSemaphore 0
    semaphorePost sema
    semaphorePost sema
    putStrLn "Hello"
    semaphoreWait sema
    semaphoreWait sema
    putStrLn "Goodbye"


text:
import Data.Fin
import Data.Vect

tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS

toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n =   Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))

record Iso a b where
  constructor MkIso
  to : a -> b
  from : b -> a
  toFrom : (y : b) -> to (from y) = y
  fromTo : (x : a) -> from (to x) = x

interface Finite t where
  card : Nat
  iso  : Iso t (Fin card)

  -- default methods

  foo : Vect card t
  foo = toVect (from iso)


text:
module Erlang.Process

import ErlPrelude

-- ProcRef l is a process that wants messages of type l.
data ProcRef : Type -> Type where
  MkProcRef : Ptr -> ProcRef l

-- Process l is a process that receives messages of type l.
data Process : (l:Type) -> Type -> Type where
  MkProc : (EIO a) -> Process l a

lift : EIO a -> Process l a
lift = MkProc

run : Process l a -> EIO a
run (MkProc p) = p

implementation Functor (Process l) where
 map f (MkProc p) = MkProc (map f p)

implementation Applicative (Process l) where
 pure a = MkProc (pure a)
 (MkProc f) <*> (MkProc a) = MkProc (f <*> a)

implementation Monad (Process l) where
  (MkProc a) >>= p = MkProc (a >>= (\as => case p as of (MkProc b) => b))

self : Process l (ProcRef l)
self = do pid <- lift $ self'
          pure $ MkProcRef pid
  where self' : EIO Ptr
        self' = foreign FFI_Erl "self" (EIO Ptr)

spawn : Process l () -> Process l' (ProcRef l)
spawn (MkProc p) = do p <- lift $ fork p
                      pure $ MkProcRef p

receive_from : ProcRef l' -> Process l l
receive_from (MkProcRef p) = do (MkERaw rec) <- lift $ receive_from' p
                                pure rec
  where receive_from' : Ptr -> EIO (ErlRaw l)
        receive_from' = foreign FFI_Erl "idris_erlang_conc:receive_from" (Ptr -> EIO (ErlRaw l))

receive_with_from : Process l (Ptr,l)
receive_with_from = do msg <- lift $ receive_with_from'
                       p   <- lift $ receive_get_from msg
                       (MkERaw rec) <- lift $ receive_get_rec msg
                       pure (p,rec)
  where receive_with_from' : EIO Ptr
        receive_with_from' = foreign FFI_Erl "idris_erlang_conc:receive_any" (EIO Ptr)
        receive_get_from : Ptr -> EIO Ptr
        receive_get_from = foreign FFI_Erl "idris_erlang_conc:receive_any_from" (Ptr -> EIO Ptr)
        receive_get_rec : Ptr -> EIO (ErlRaw l)
        receive_get_rec = foreign FFI_Erl "idris_erlang_conc:receive_any_msg" (Ptr -> EIO (ErlRaw l))

receive : Process l l
receive = do (_, msg) <- receive_with_from
             pure msg

send : ProcRef l' -> l' -> Process l ()
send (MkProcRef pid) msg = do lift $ send' pid (MkERaw msg)
                              pure ()
  where
    send' : Ptr -> ErlRaw l' -> EIO ()
    send' = foreign FFI_Erl "idris_erlang_conc:send" (Ptr -> (ErlRaw l') -> EIO ())

max_stars_repo_name: lenary/idris-erlang

max_issues_repo_name: yurrriq/idris-erlang

max_forks_repo_name: yurrriq/idris-erlang


text:
module Halfer
import Service
import System
import Numeric

%default total

-- Helpful type alias for even integers
public export
EvenNumber : Type
EvenNumber = (n : WFInt ** Parity n 2)

||| Return a Just EvenNumber if the number is even, or Nothing otherwise.
public export
maybeEven : Integer -> Maybe EvenNumber

||| Round a number down to the nearest even number
public export
forceEven : Integer -> EvenNumber

-- maybeEven a with (mod a 2) proof p
--   maybeEven a | 0 = Just ((cast a) ** ModIsZero p)
--   maybeEven a | _ = Nothing

-- Run external service
public export
runHalfer : EvenNumber -> IO Integer
runHalfer = do ?run

public export
halferContract : (a : EvenNumber) -> Contract (runHalfer a) Integer
halferContract a = MkContract (runHalfer a)

public export
halferService : EvenNumber -> Service Integer
halferService a = Promise (halferContract a)


text:
module Data.Matrix.RowEchelon

import Control.Algebra
import Classes.Verified
import Control.Algebra.VectorSpace -- definition of module

import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.ZZVerified

import Data.Matrix.ZZModuleSpan
import Data.Matrix.LinearCombinations

import Data.Fin.FinOrdering
import Data.Fin.Structural

-- For style. ((Reader r a) equivalent to (r -> a))
import Control.Monad.Identity
import Control.Monad.Reader

import Control.Isomorphism

%default total

{-
Table of contents:
* ZZ proofs
* Vect/Matrix proofs
* The leading nonzero of a vector
* DANRZ property
* Corollary bispannability property
* Row echelon properties
-}

{-
ZZ proofs
-}

zzZOrOrPosNeg : (z : ZZ) -> Either (z=Pos 0) $ Either (k : _ ** z = Pos (S k)) $ (k : _ ** z = NegS k)
zzZOrOrPosNeg (Pos Z) = Left Refl
zzZOrOrPosNeg (Pos (S k)) = Right (Left (k ** Refl))
zzZOrOrPosNeg (NegS k) = Right (Right (k ** Refl))

{-
Vect/Matrix proofs
-}

indicesConstColChariz : indices i FZ (map (r::) xs) = r
indicesConstColChariz {i} {r}
	= trans (sym $ indexMapChariz {f=index FZ})
	$ trans (cong {f=index i} $ leadingElemExtensionFirstColReplicate r)
	indexReplicateChariz

indicesConstColChariz2 : indices i (FS j) (map (r::) xs) = indices i j xs
indicesConstColChariz2 {i} {j}
	= trans (sym $ indexMapChariz {f=index (FS j)})
	$ trans (cong {f=index i} leadingElemExtensionColFSId)
	$ indexMapChariz {f=index j}

{-
The leading nonzero of a vector

* (leadingNonzeroNum) Its computation
* (leadingNonzeroProp) The leading nonzero property of a (Maybe (Fin n)) for a vector --
	if Nothing, the vector is 0
	if Just k, k is the leading nonzero of the vector
* (leadingNonzeroProof) Proof the computation gives the leading nonzero (has the leading nonzero prop)
-}

leadingNonzeroNum : (v : Vect n ZZ) -> Maybe (Fin n)
leadingNonzeroNum [] = Nothing
leadingNonzeroNum {n= S predn} (Pos Z::xs) = map FS $ leadingNonzeroNum xs
leadingNonzeroNum {n= S predn} (k::xs) = Just FZ

leadingNonzeroProp : (v : Vect n ZZ) -> Maybe (Fin n) -> Type
leadingNonzeroProp {n} v mnel =
	Either
		(mnel = Nothing, v = neutral)
		( nel : Fin n **
			(mnel = Just nel
			, {i : Fin n}
				-> finToNat i `LTRel` finToNat nel
				-> index i v = Pos Z
			, Not (index nel v = Pos Z) )
		)

leadingNonzeroProof_lemmaNeutToNothing : leadingNonzeroNum Algebra.neutral = Nothing
leadingNonzeroProof_lemmaNeutToNothing = ?leadingNonzeroProof_lemmaNeutToNothing'

leadingNonzeroProof_lemmaNeutToNothing' = proof
	intro n
	induction n
	exact Refl
	intro predn
	exact cong {f=map FS}

leadingNonzeroProof : {v : Vect n ZZ} -> leadingNonzeroProp v (leadingNonzeroNum v)
leadingNonzeroProof {v=[]} = Left (Refl, Refl)
leadingNonzeroProof {n=S predn} {v=Pos Z::rs} with (leadingNonzeroProof {v=rs})
	| Left (_, pr) = rewrite pr
		in Left (cong {f=map FS} leadingNonzeroProof_lemmaNeutToNothing, Refl)
	| Right (nel ** (isJ, l_fn, r_pr))
		= Right (FS nel ** (cong {f=map FS} isJ, l_fn', r_pr))
		where
			l_fn' : {ii : Fin (S predn)}
				-> finToNat ii `LTRel` finToNat (FS nel)
				-> index ii (Pos Z::rs) = Pos Z
			l_fn' {ii=FZ} _ = Refl
			l_fn' {ii=FS j} precondit = l_fn $ fromLteSucc precondit
leadingNonzeroProof {n=S predn} {v=Pos (S k)::rs}
	= Right ( FZ **
		(Refl, void . succNotLTEzero, flip (replace {P=distinguish_Z_SZ}) ()) )
		where
			distinguish_Z_SZ : ZZ -> Type
			distinguish_Z_SZ (Pos Z) = Void
			distinguish_Z_SZ z = ()
leadingNonzeroProof {n=S predn} {v=NegS k::rs}
	= Right ( FZ **
		(Refl, void . succNotLTEzero, flip (replace {P=distinguish_Z_SZ}) ()) )
		where
			distinguish_Z_SZ : ZZ -> Type
			distinguish_Z_SZ (Pos Z) = Void
			distinguish_Z_SZ z = ()

{-
lemma1 : leadingNonzeroNum rs = Nothing -> leadingNonzeroNum (Pos Z :: rs) = Nothing
lemma1 = ?lemma1'

lemma1_mat : leadingNonzeroNum (index nel xs) = Nothing
	-> leadingNonzeroNum (index (FS nel) $ map ((Pos Z)::) xs) = Nothing

lemma2 : leadingNonzeroNum rs = Nothing -> rs = Algebra.neutral
lemma2 = ?lemma2'

lemma3 : leadingNonzeroNum rs = Just mel
	-> leadingNonzeroNum (Pos Z :: rs) = Just (FS mel)

lemma3_mat : leadingNonzeroNum (index nel xs) = Just mel
	-> leadingNonzeroNum (index (FS nel) $ map ((Pos Z)::) xs) = Just (FS mel)
-}

||| (x::xs) leads with a nonzero for x not 0
leadingNonzeroIsFZIfNonzero :
	Not (index FZ x = Pos Z)
	-> leadingNonzeroNum x = Just FZ
leadingNonzeroIsFZIfNonzero {x=x::xs} nonz with ( runIso eitherBotRight $ map nonz $ mirror $ zzZOrOrPosNeg x )
	| Left (k ** prposS) = rewrite prposS in Refl
	| Right (k ** prnegS) = rewrite prnegS in Refl

{-
DANRZ property:
That every entry (<= horiz, > vert) below and not to the right of this one is 0.
-}

downAndNotRightOfEntryImpliesZ : (xs : Matrix n m ZZ) -> (row : Fin n) -> (col : Fin m) -> Type
downAndNotRightOfEntryImpliesZ xs nel mel {n} {m} = (i : Fin n) -> (j : Fin m) -> (finToNat nel `LTRel` finToNat i) -> (finToNat j `LTERel` finToNat mel) -> indices i j xs = Pos Z
{-
Equivalent properties:
1) map (take mel) (drop nel xs) = neutral
2) (nel `LT` i) -> (j `LTE` mel) -> indices i j xs = Pos Z
	# In pseudocode, because we decided not to use direct LT and LTE of Fins.

---

We cannot write

> downAndNotRightOfEntryImpliesZ : (xs : Matrix n m ZZ) -> (row : Fin n) -> (col : Fin m) -> Type
> downAndNotRightOfEntryImpliesZ xs nel mel {n} {m} = {i : Fin n} -> {j : Fin m} -> (finToNat nel `LTRel` finToNat i) -> (finToNat j `LTERel` finToNat mel) -> indices i j xs = Pos Z

because the error described in ImplicitArgsError applied to (i) and (j) in ({i : Fin n} -> {j : Fin m} -> ...).
-}

weakenDownAndNotRight :
	downAndNotRightOfEntryImpliesZ mat (FS prednel) mel
	-> ((j : _)
		-> LTERel (finToNat j) (finToNat mel)
		-> indices (FS prednel) j mat = Pos Z)
	-> downAndNotRightOfEntryImpliesZ mat (weaken prednel) mel
weakenDownAndNotRight {prednel} {mat} danrz newzfn i j iDown jNotRight
	= either
		(\b => danrz i j b jNotRight)
		(\pr => trans (cong {f=\e => indices e j mat} pr) $ newzfn j jNotRight)
	$ partitionNatWknLT prednel i iDown

||| A special case of (weakenDownAndNotRight).
weakenDownAndNotRightFZ :
	downAndNotRightOfEntryImpliesZ mat (FS prednel) FZ
	-> indices (FS prednel) FZ mat = Pos Z
	-> downAndNotRightOfEntryImpliesZ mat (weaken prednel) FZ
weakenDownAndNotRightFZ {prednel} {mat} danrz newz i FZ iDown fzNotRight
	= either
		(\b => danrz i FZ b fzNotRight)
		(\pr => trans (cong {f=\e => indices e FZ mat} pr) newz)
	$ partitionNatWknLT prednel i iDown
weakenDownAndNotRightFZ _ _ _ (FS prel) _ fzNotRight
	= void . succNotLTEzero . lteRelToLTE $ fzNotRight

total
afterUpdateAtCurStillDownAndNotRight :
	(downAndNotRightOfEntryImpliesZ mat (FS prednel) mel)
	-> (downAndNotRightOfEntryImpliesZ (updateAt (FS prednel) f mat) (FS prednel) mel)
afterUpdateAtCurStillDownAndNotRight {prednel=FZ} {mat=x::y::xs} {mel} danrz FZ j iDown jNotRight = void $ succNotLTEzero $ iDown
afterUpdateAtCurStillDownAndNotRight {prednel=FZ} {mat=x::y::xs} {mel} danrz (FS FZ) j iDown jNotRight = void $ succNotLTEzero $ fromLteSucc iDown
afterUpdateAtCurStillDownAndNotRight {prednel=FZ} {mat=x::y::xs} {mel} danrz (FS $ FS i) j iDown jNotRight = danrz (FS $ FS i) j iDown jNotRight
afterUpdateAtCurStillDownAndNotRight {prednel=FS predednel} {mat=x::xs} {f} danrz FZ j iDown jNotRight = danrz FZ j iDown jNotRight
afterUpdateAtCurStillDownAndNotRight {prednel=FS predednel} {mat=x::xs} {mel} {f} danrz (FS i) j iDown jNotRight = afterUpdateAtCurStillDownAndNotRight {prednel=predednel} {mat=xs} {mel=mel} {f=f} (\i_xs => \j_xs => \iDown_xs => \jNotRight_xs => danrz (FS i_xs) j_xs (LTESucc iDown_xs) jNotRight_xs) i j (fromLteSucc iDown) jNotRight

{-
Subsection proving (danrzLeadingZeroAlt)
-}

{-
Proved by noting
	getCol FZ xs = map (index FZ) xs
and
	\j => danrz j FZ ?lt ?lte :
		(j : Fin _) -> index FZ $ index j xs = Pos 0
becomes by (trans (indexMapChariz {f=index FZ})) a
	(j : Fin _) -> index j $ map (index FZ) xs = Pos 0.

So that it suffices to prove
	((i : Fin _) -> index i xs = index i ys)
	-> xs = ys.
-}
danrzTailHasLeadingZeros :
	downAndNotRightOfEntryImpliesZ (x::xs) FZ FZ
	-> getCol FZ xs = Algebra.neutral
danrzTailHasLeadingZeros danrz = vecIndexwiseEq
	(\j => trans (indexMapChariz {f=index FZ})
		$ trans (danrz (FS j) FZ (zLtSuccIsTrue $ finToNat j) $ Right Refl)
	$ sym $ indexNeutralIsNeutral1D j)

-- Corrollary : decEq w/ eitherBotRight lets you extract rowEchelon proofs.
-- In particular,
||| x|xs
||| 0|_
||| 0|_
||| ...
||| has 0th-col 0 or its 0th row leads with a nonzero
danrzLeadingZeroAlt :
	downAndNotRightOfEntryImpliesZ (x::xs) FZ FZ
	-> Either
		(getCol FZ (x::xs) = Algebra.neutral)
		(leadingNonzeroNum x = Just FZ)
danrzLeadingZeroAlt {x} {xs} danrz with ( decEq (index FZ x) $ Pos Z )
	| Yes preq = Left (vecHeadtailsEq preq $ danrzTailHasLeadingZeros danrz)
	| No prneq = Right $ leadingNonzeroIsFZIfNonzero prneq

danrzLastcolImpliesAllcol : {mat : Matrix (S _) (S mu) ZZ}
	-> downAndNotRightOfEntryImpliesZ mat FZ (last {n=mu})
	-> downAndNotRightOfEntryImpliesZ mat FZ mel
danrzLastcolImpliesAllcol danrzlast i j ltrel _ = danrzlast i j ltrel $ ltenatLastIsTrue2 j

danrzLastcolImpliesTailNeutral : {xs : Matrix n (S mu) ZZ}
	-> downAndNotRightOfEntryImpliesZ (x::xs) FZ (last {n=mu})
	-> xs=Algebra.neutral
danrzLastcolImpliesTailNeutral {x} {xs} {n} {mu} danrz
	= uniformValImpliesReplicate (replicate (S mu) $ Pos 0) xs
	$ \na => uniformValImpliesReplicate (Pos 0) (index na xs) (fn na)
	where
		fn : (prednel : Fin n) -> (j : Fin (S mu)) -> indices prednel j xs = Pos 0
		fn prednel j = danrz (FS prednel) j
			(zLtSuccIsTrue $ finToNat prednel)
			(ltenatLastIsTrue2 j)

{-
Corollary bispannability property
-}

bispansNulltailcolExtension : downAndNotRightOfEntryImpliesZ (x::xs) FZ FZ
	-> ys `bispanslz` map Vect.tail xs
	-> map ((Pos Z)::) ys `bispanslz` xs
bispansNulltailcolExtension = bispansNullcolExtension . danrzTailHasLeadingZeros

{-
Row echelon properties

Definitions
* (echPreTy) The per-row component of (rowEchelonPre)
* (rowEchelonPre) The row echelon property in terms of (leadingNonzeroNum) & its correctness
* (echTy) The per-row component of (rowEchelon)
* (rowEchelon) The row echelon property -- (rowEchelonPre) but with numbers having the leading nonzero property (leadingNonzeroProp) -- inferable about (leadingNonzeroNum) using (leadingNonzeroProof), hence inferable from a given (rowEchelonPre) proof.

Theorems
* rowEchelonPreZeroHeight
* rowEchelonPreExtension
	Inducing gaussian elimination verification from the lesser height & width cases,
	done when first column is nonzero.
* echelonPreNullcolExtension
	Inducing gaussian elimination from the lesser width cases,
	done when first column is zero.
* echelonPreFromDanrzLast
	For verifying gaussian elimination in the width = 1 case
* toEchTy
* toRowEchelon
-}

echPreTy : (xs : Matrix n m ZZ) -> (nel : Fin n) -> Type
echPreTy {n} {m} xs nel =
	Either
		((nelow : Fin n) -> (ltpr : finToNat nel `LTERel` finToNat nelow)
			-> index nelow xs = Algebra.neutral)
		(mel : Fin m ** (leadingNonzeroNum $ index nel xs = Just mel
			, downAndNotRightOfEntryImpliesZ xs nel mel))

{-
Lemma about left case of (echPreTy):

Everything zero below or at a row of xs
=>
for all (x::xs)
for mel = last
downAndNotRightOfEntryImpliesZ xs nel mel

See also (echelonFromDanrzLast),
the converse (danrzLastcolImpliesTailNeutral) of this from (ZZGaussianElimination)
-}

rowEchelonPre : (xs : Matrix n m ZZ) -> Type
rowEchelonPre {n} {m} xs = (narg : Fin n) -> echPreTy xs narg

||| For best results, prove in terms of `echPreTy` using `toEchTy`
echTy : (xs : Matrix n m ZZ) -> (nel : Fin n) -> Type
echTy {n} {m} xs nel =
	Either
		((nelow : Fin n) -> (ltpr : finToNat nel `LTERel` finToNat nelow)
			-> index nelow xs = Algebra.neutral)
		(mel : Fin m ** (leadingNonzeroProp (index nel xs) (Just mel)
			, downAndNotRightOfEntryImpliesZ xs nel mel))

||| For best results, prove in terms of `rowEchelonPre` using `toRowEchelon`
rowEchelon : (xs : Matrix n m ZZ) -> Type
rowEchelon {n} {m} xs = (narg : Fin n) -> echTy xs narg

rowEchelonPreZeroHeight : rowEchelonPre []
rowEchelonPreZeroHeight = \narg => FinZElim narg

rowEchelonPreZeroWidth : rowEchelonPre $ replicate n []
rowEchelonPreZeroWidth = \narg => Left $ \_ => \_ => indexReplicateChariz

rowEchelonPreExtension :
	{x : Vect (S predm) ZZ}
	-> {xs : Matrix n predm ZZ}
	-> leadingNonzeroNum x = Just FZ
	-> rowEchelonPre xs
	-> rowEchelonPre $ x :: map ((Pos 0)::) xs
rowEchelonPreExtension {n} {predm} {x} {xs} lnz ech FZ =
	Right (FZ ** (lnz, danrzFn))
	where
		danrzFn : (i : Fin (S n))
			-> (j : Fin (S predm))
			-> LTE 1 (finToNat i)
			-> Either (LTE (S (finToNat j)) 0) (finToNat j = 0)
			-> indices i j $ x :: map ((Pos 0)::) xs = Pos 0
		danrzFn FZ _ lteOZ _ = void $ succNotLTEzero lteOZ
		{- column 0 and row > 0 to x::(0-col|xs) is index 0 to a 0::(xs!i) is 0 -}
		danrzFn (FS k) j _ orJZ
			= rewrite
			either (void . succNotLTEzero) (finToNatInjective j FZ) orJZ
			in indicesConstColChariz
rowEchelonPreExtension {n} {predm} {x} {xs} lnz ech (FS narg) with ( ech narg )
	{-
	Left case
	---

	Outline:

	indices i j xs = Pos Z <=> index j $ index i xs = Pos Z

	index nelow xs = replicate predm (Pos 0)
	<=> forall j, index j $ index nelow xs = Pos Z

	Consider:

	lteSuccRight :: LTE (S m) n -> LTE (S m) (S n)

	Consider this context:

	intros
	exact Left _
	intro snelow
	intro ltReSnelow

	But instead we do:

	exact Left _
	intro snelow
	either snelow is FZ or snellow is FS k.
	If snelow is FZ, we need to show (index FZ $ x::_ = 0 === x = 0),
		so we must show snelow can't be FZ
		which follows from (ltReSnelow) being an either of two
		characterizations of (finToNat snelow) as a successor.
	If snelow is (FS predsnelow), we need to show
		(index predsnelow xs = 0),
	which follows from (neutfn predsnelow)
	given a weakening of the LTE
	-}
	| Left neutfn = Left zFn
		where
			zFn : (snelow : Fin (S n))
				-> Either
					((S $ finToNat narg) `LTRel` (finToNat snelow))
					(S $ finToNat narg = finToNat snelow)
				-> index snelow $ x :: map ((Pos 0)::) xs
					= Algebra.neutral
			zFn FZ ltReSnelow = void
				$ either succNotLTEzero SIsNotZ ltReSnelow
			zFn (FS predsnelow) ltReSnelow = trans indexMapChariz
				$ cong $ neutfn predsnelow
				$ either
					(Left . fromLteSucc)
					(Right . succInjective
						(finToNat narg)
						(finToNat predsnelow))
					ltReSnelow
	{-
	Right case
	---

	* lnzJMelEq -> lnzJMelEq' :
		If (leadingNonzeroNum xs!narg = Just mel),
		so will the extension (x::(0-col|xs)) have (Just (FS mel)) at (FS narg)
	* See (danrzFn) comments
	-}
	| Right (mel ** (lnzJMelEq, danrzNelMel))
		= Right (FS mel **
				(trans (cong {f=leadingNonzeroNum} indexMapChariz)
					$ cong {f=map FS} lnzJMelEq
				, danrzFn))
		where
			{-
			When i and j a successor, apply danrzNelMel.
			When i a successor and j = 0, const (const Refl).
			When i = 0, the LTE is absurd.
			-}
			danrzFn : (i : Fin (S n))
				-> (j : Fin (S predm))
				-> (S $ finToNat narg) `LTRel` (finToNat i)
				-> Either ((finToNat j) `LTRel` (S $ finToNat mel))
					(finToNat j = S $ finToNat mel)
				-> indices i j $ x :: map ((Pos 0)::) xs = Pos 0
			danrzFn FZ _ ltNI _ = void $ succNotLTEzero ltNI
			danrzFn (FS i') FZ ltNI ltJSM = indicesConstColChariz
			danrzFn (FS i') (FS j') ltNI ltJSM
				= trans indicesConstColChariz2
					$ danrzNelMel i' j' ltNI' ltJSM'
				where
					ltNI' = fromLteSucc ltNI
					ltJSM' = either
						(Left . fromLteSucc)
						(Right . succInjective
							(finToNat j')
							(finToNat mel))
						ltJSM

echelonPreNullcolExtension :
	{xs : Matrix n predm ZZ}
	-> rowEchelonPre xs
	-> rowEchelonPre $ map ((Pos 0)::) xs
echelonPreNullcolExtension {n} {predm} {xs} ech narg with ( ech narg )
	| Left neutfn = Left $ \nelow => \ltpr =>
		trans indexMapChariz
		$ cong {f=((Pos 0)::)} $ neutfn nelow ltpr
	| Right (mel ** (lnzJMelEq, danrzNelMel))
		= Right (FS mel **
			(trans (cong {f=leadingNonzeroNum} indexMapChariz)
			$ cong {f=map FS} lnzJMelEq
			, danrzFn))
		where
			{-
			When j = 0, const (const Refl)
			When j a successor, apply (danrzNelMel).
			-}
			danrzFn : (i : Fin n)
				-> (j : Fin (S predm))
				-> finToNat narg `LTRel` finToNat i
				-> finToNat j `LTERel` (S $ finToNat mel)
				-> indices i j $ map ((Pos 0)::) xs = Pos 0
			danrzFn i FZ _ _ = indicesConstColChariz
			danrzFn i (FS j') ltNI ltJSM = trans indicesConstColChariz2
				$ danrzNelMel i j' ltNI
				$ either
					(Left . fromLteSucc)
					(Right . succInjective
						(finToNat j')
						(finToNat mel))
					ltJSM

echelonPreFromDanrzLast :
	{mat : Matrix (S n) (S mu) ZZ}
	-> downAndNotRightOfEntryImpliesZ mat FZ (last {n=mu})
	-> rowEchelonPre mat
echelonPreFromDanrzLast {mat=x::xs} {n} {mu} danrz FZ with (leadingNonzeroProof {v=x})
	| Left nothPrAndZeroPr = Left echelonPreFromDanrzLast_Nothing
	where
		echelonPreFromDanrzLast_Nothing :
			(nelow : Fin (S n))
			-> (ltepr : Either (0 `LT` finToNat nelow) (0 = finToNat nelow))
			-> index nelow (x::xs) = Algebra.neutral
		echelonPreFromDanrzLast_Nothing nelow (Left ltpr)
			= trans
				(cong {f=\ts => Vect.index nelow (x::ts)}
				$ danrzLastcolImpliesTailNeutral {x=x} {xs=xs} danrz)
			$ trans (cong {f=(\i => Vect.index i (x::Algebra.neutral))}
				$ getProof $ gtnatFZImpliesIsFinSucc nelow ltpr)
			$ indexNeutralIsNeutral2D _
		echelonPreFromDanrzLast_Nothing nelow (Right eqpr)
			= rewrite sym $ finToNatInjective FZ nelow eqpr
			in snd nothPrAndZeroPr
	| Right (mel ** melpr)
		= Right $ (mel ** (fst melpr, danrzLastcolImpliesAllcol {mel=mel} danrz))
echelonPreFromDanrzLast {mat=x::xs} danrz (FS k) with (leadingNonzeroProof {v=index k xs})
	| Left nothPrAndZeroPr = Left echelonPreFromDanrzLast_Nothing2
	where
		echelonPreFromDanrzLast_Nothing2 :
			(nelow : Fin (S _))
			-> (ltepr : Either
				(finToNat (FS k) `LT` finToNat nelow)
				(finToNat (FS k) = finToNat nelow))
			-> index nelow (x::xs) = Algebra.neutral
		echelonPreFromDanrzLast_Nothing2 nelow (Left ltpr)
			= trans
				(cong {f=\ts => Vect.index nelow (x::ts)}
				$ danrzLastcolImpliesTailNeutral {x=x} {xs=xs} danrz)
			$ trans (cong {f=(\i => Vect.index i (x::Algebra.neutral))}
				$ getProof $ gtnatFZImpliesIsFinSucc nelow
				$ natGtAnyImpliesGtZ
					(S $ finToNat k) (finToNat nelow) ltpr)
			$ indexNeutralIsNeutral2D _
		echelonPreFromDanrzLast_Nothing2 nelow (Right eqpr)
			= rewrite sym $ finToNatInjective (FS k) nelow eqpr
			in snd nothPrAndZeroPr
	| Right (mel ** melpr) = void $ (snd $ snd melpr)
		$ flip trans (indexNeutralIsNeutral1D mel)
		$ cong {f=index mel}
		$ trans (cong {f=index k}
			$ danrzLastcolImpliesTailNeutral {x=x} {xs=xs} danrz)
		$ indexNeutralIsNeutral2D k

toEchTy : echPreTy xs nel -> echTy xs nel
toEchTy ech = map prrw ech
	where
		prrw (mel ** (pr, danrz))
			= (mel ** (rewrite sym pr in leadingNonzeroProof, danrz))

toRowEchelon : rowEchelonPre xs -> rowEchelon xs
toRowEchelon echxs = \narg => toEchTy (echxs narg)


text:
module Main

import Dart.Core
import Dart.FFI
import Dart.FFI.Elab

%inline
Foreign : Type
Foreign = Struct """
Foreign,

class Foreign {
  final Function() callback;
  Foreign({this.callback});
  Foreign.of(this.callback);
  void report() {
    $.print(callback == null ? 'callback is null' : 'callback is not null');
    callback?.call();
  }
}
""" []

%language ElabReflection

%runElab importDart [
  package "" [
    partial' $ class' "Foreign" [
      new "" [
        "callback" :? "IO" :<> "()"
      ],
      new "of" [
        "callback" :: "IO" :<> "()"
      ],
      io "void" "report" []
    ]
  ]
]

main : IO ()
main = do
  f <- Foreign.new [callback @= unsafeNull]
  f @. report

  f <- Foreign.new [callback @= putStrLn "foo"]
  f @. report

  f <- Foreign.of unsafeNull
  f @. report

  f <- Foreign.of (putStrLn "bar")
  f @. report