text:
module Invincy.Printing
import Data.Vect
import Invincy.Core

%access public export

data Printer : (o, r : Type) -> Type where
  MkPrinter : (r -> o) -> Printer o r

runPrinter : Printer o r -> r -> o
runPrinter (MkPrinter f) = f

infixl 4 >$
interface Contravariant (f: Type -> Type) where
  contramap : (a -> b) -> f b -> f a
  (>$) : b -> f b -> f a
  (>$) = contramap . const

implementation Contravariant (Printer o) where
  contramap f (MkPrinter p) = MkPrinter $ p . f

interface Contravariant f => Divisible (f: Type -> Type) where
  divide : (a -> (b, c)) -> f b -> f c -> f a
  conquer : f a

implementation Monoid i => Divisible (Printer i) where
  divide p (MkPrinter f) (MkPrinter g) = MkPrinter $ \r => case p r of
    (fi, gi) => f fi <+> g gi
  conquer = MkPrinter $ const neutral

divided : Divisible f => f a -> f b -> f (a, b)
divided = divide id

(*>) : Divisible f => f () -> f a -> f a
(*>) = divide (MkPair ())

(<*) : Divisible f => f a -> f () -> f a
(<*) = divide (flip MkPair ())

interface Divisible f => Decidable (f: Type -> Type) where
  lose : (a -> Void) -> f a
  choose : (a -> Either b c) -> Lazy (f b) -> Lazy (f c) -> f a

implementation Monoid i => Decidable (Printer i) where
  lose _ = conquer
  choose e f g = MkPrinter $ \x => case e x of
    Left fi => runPrinter f fi
    Right gi => runPrinter g gi

chosen : Decidable f => Lazy (f b) -> Lazy (f c) -> f (Either b c)
chosen = choose id

-- could be used for the invertible sat, with no check
itemP : Stream t s => Printer s t
itemP = MkPrinter single

ignoreP : Monoid i => i -> Printer i ()
ignoreP = MkPrinter . const

valP : Stream t s => t -> Printer s ()
valP = ignoreP . single

optionP : Monoid i => a -> Printer i a -> Printer i (Maybe a)
optionP x = contramap (maybe x id)

-- same as manyTill, and perhaps will use for `some`
manyP : Monoid i => Printer i a -> Printer i (List a)
manyP x = MkPrinter $ \l => concatMap (runPrinter x) l

someP : Monoid i => Printer i a -> Printer i (x:List a ** NonEmpty x)
someP = contramap getWitness . manyP

manyTillP : Monoid i => Printer i a -> Printer i () -> Printer i (List a)
manyTillP p t = manyP p <* t

sepBy1P : Monoid i => Printer i a -> Printer i () -> Printer i (x:List a ** NonEmpty x)
sepBy1P p s = MkPrinter $ \(x::xs ** _) =>
  runPrinter p x <+> runPrinter (contramap List.toList (manyP (s *> p))) xs

sepByP : Monoid i => Printer i a -> Printer i () -> Printer i (List a)
sepByP {i} p s = MkPrinter sep
  where
    sep : List a -> i
    sep [] = neutral
    sep (x::xs) = runPrinter (sepBy1P p s) (x::xs ** IsNonEmpty)

integerP : Printer (List Char) Integer
integerP = MkPrinter $ unpack . cast

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
||| An expression language with mechanical proof of type-safety.
|||
||| `Variant` is an expression language supporting Let-bindings, and
||| type safe variants.  Standard constructions are used to
||| represent the language as an EDSL, together with proof of progress
||| taken from PLFA Part 2.
|||
||| This module compliments Section 4.3 of the Functional Pearl.
|||
||| Although the code appears to be total, there is a known issues
||| with Idris2 totality checker that causes it to slow down when
||| dealing with mutually defined terms.
|||
module Razor.Variant.Unique

import Razor.Common

%default covering

namespace Types

  public export
  data Level = TYPE | VALUE

  public export
  data Ty : Level -> Type where
    IntTyDesc : Ty TYPE
    IntTy     : Ty VALUE

    CharTyDesc : Ty TYPE
    CharTy     : Ty VALUE

    VariantTyDesc : (fields : Vect (S n) (Ty TYPE))  -> Ty TYPE
    VariantTy     : (fields : Vect (S n) (Ty VALUE)) -> Ty VALUE

  public export
  data TyCheckVariant : (prfTy : (desc : Ty TYPE) -> (type : Ty VALUE) -> Type)
                     -> (fieldsD : Vect (S n) (Ty TYPE))
                     -> (fieldsV : Vect (S n) (Ty VALUE))
                                -> Type
    where
      CheckOne  : (prf : check type value) -> TyCheckVariant check [type] [value]
      CheckRest : (one  : check type value)
               -> (rest : TyCheckVariant check        types          values)
                       -> TyCheckVariant check (type::types) (value::values)

  public export
  data TyCheck : (desc : Ty TYPE)
              -> (type : Ty VALUE)
                      -> Type
    where
      CheckInt  : TyCheck IntTyDesc  IntTy
      CheckChar : TyCheck CharTyDesc CharTy
      CheckVar  : (prf : TyCheckVariant TyCheck types values)
                      -> TyCheck (VariantTyDesc types) (VariantTy values)

namespace Context
  public export
  Context : List Level -> Type
  Context = DList Level Ty

  public export
  Elem : {level : Level}
      -> {levels : List Level}
      -> (ctxt : Context levels)
      -> (type : Ty level)
      -> Type
  Elem ctxt type = Elem Level Ty type ctxt

namespace Terms
  mutual

    namespace Patterns
      public export
      data Case : (ctxt  : Context levels)
               -> (type  : Ty VALUE)
               -> (body  : Ty level)
               -> Type
        where
          MkCase : {type : Ty VALUE}
                -> {body : Ty level}
                -> (branch : Variant (ctxt +=    type) body)
                          -> Case     ctxt       type  body

      public export
      data Cases : (ctxt  : Context levels)
                -> (types : Vect (S n) (Ty VALUE))
                -> (body  : Ty level)
                -> Type
        where
            Singleton : {type : Ty VALUE}
                     -> {body : Ty level}
                     -> (branch : Case  ctxt  type   body)
                               -> Cases ctxt [type] body

            Extend :  {type : Ty VALUE}
                   -> {body : Ty level}
                   -> (branch : Case  ctxt   type         body)
                   -> (rest   : Cases ctxt          kvs  body)
                             -> Cases ctxt (type :: kvs) body

    namespace Delcarations
      public export
      data Field : (ctxt  : Context levels)
                -> (type  : Ty TYPE)
                -> Type
        where
          MkField : {type : Ty TYPE}
                 -> (desc : Variant ctxt type)
                         -> Field   ctxt type

      public export
      data Fields : (ctxt : Context levels)
                 -> (kvs  : Vect (S n) (Ty TYPE))
                 -> Type
        where
          Singleton : (field : Field  ctxt  type)
                            -> Fields ctxt [type]

          Extend : (field : Field  ctxt            type)
                -> (rest  : Fields ctxt  fields)
                         -> Fields ctxt (fields += type)

    public export
    data Variant : forall lvls, lvl . Context lvls -> Ty lvl -> Type where
      -- Let-Bindings & Variables
      Var : Elem g ty -> Variant g ty

      Let : {expr : Ty levelE}
         -> {body : Ty levelB}
         -> (this     : Variant        g  expr)
         -> (beInThis : Variant (expr::g) body)
                     -> Variant        g  body

      -- Base Values
      I : Int  -> Variant g IntTy
      C : Char -> Variant g CharTy

      -- Type Constructors
      TyInt  : Variant g IntTyDesc
      TyChar : Variant g CharTyDesc

      TyVariant : {kvs : Vect (S n) (Ty TYPE)}
               -> (fields : Fields   g                kvs)
                         -> Variant  g (VariantTyDesc kvs)

      -- Variant Value Constructors
      Tag : {ty    : Ty VALUE}
         -> {types  : Vect (S n) (Ty TYPE)}
         -> {values : Vect (S n) (Ty VALUE)}
         -> (value : Variant g ty)
         -> (type  : Variant g (VariantTyDesc types))
         -> (chk   : TyCheck   (VariantTyDesc types) (VariantTy values))
         -> (prf   : Elem       ty         values)
                  -> Variant g (VariantTy  values)

      -- Variant Matching
      Match : {values : Vect (S n) (Ty VALUE)}
           -> (value : Variant g (VariantTy values))
           -> (cases : Cases   g            values   b)
                    -> Variant g                     b

namespace Renaming

  public export
  weaken : (f : Context.Elem old type
             -> Context.Elem new type)
        -> (Context.Elem (old += type') type
         -> Context.Elem (new += type') type)
  weaken func Here = Here
  weaken func (There rest) = There (func rest)

  mutual
    namespace Case

      public export
      rename : forall levelsO, levelsN
             . {old : Context levelsO}
            -> {new : Context levelsN}
            -> (forall level . {type : Ty level}
                            -> Context.Elem old type
                            -> Context.Elem new type)

            -> ({type : Ty VALUE} ->
                {body : Ty level} -> Case old type body
                                  -> Case new type body)
      rename f (MkCase branch)
        = MkCase (rename (weaken f) branch)

    namespace Cases
      public export
      rename : forall levelsO, levelsN
             . {old : Context levelsO}
            -> {new : Context levelsN}
            -> (f : forall level
                  . {type : Ty level}
                          -> Context.Elem old type
                          -> Context.Elem new type)

            -> (forall types . Cases old types type
                            -> Cases new types type)

      rename f (Singleton branch)
        = Singleton (Case.rename f branch)
      rename f (Extend branch rest)
        = Extend (Case.rename f branch) (rename f rest)

    namespace Fields
      public export
      rename : forall levelsO, levelsN
             . {old : Context levelsO}
            -> {new : Context levelsN}
            -> (f : forall level . {type : Ty level}
                                 -> Context.Elem old type
                                 -> Context.Elem new type)
            -> (forall types . Fields old types
                            -> Fields new types)

      rename f (Singleton (MkField first))
        = Singleton (MkField (rename f first))

      rename f (Extend (MkField next) rest)
        = Extend (MkField (rename f next)) (rename f rest)

    public export
    rename : forall levelsO, levelsN
           . {old : Context levelsO}
          -> {new : Context levelsN}
          -> (f : forall level . {type : Ty level}
                              -> Elem old type
                              -> Elem new type)
          -> (forall level . {type : Ty level}
                           -> Variant old type
                           -> Variant new type)
    -- Let Binding & Variables
    rename f (Var x) = Var (f x)
    rename f (Let this beInThis)
      = Let (rename f this) (rename (weaken f) beInThis)

    -- Base Values
    rename f (I x) = I x
    rename f (C x) = C x

    -- Type Constructors
    rename f (TyInt)  = TyInt
    rename f (TyChar) = TyChar
    rename f (TyVariant fields) = TyVariant (rename f fields)

    -- Variant Value Constructors
    rename f (Tag value type chk prf)
      = Tag (rename f value) (rename f type) chk prf

    -- Variant Matching
    rename f (Match value cases)
      = Match (rename f value) (rename f cases)

namespace Substitution

  public export
  weakens : forall levelsO, levelsN
          . {old   : Context levelsO}
         -> {new   : Context levelsN}
         -> {type  : Ty level}
         -> {type' : Ty level'}
         -> (f     : Elem    old type
                  -> Variant new type)
                  -> (Elem   (old += type') type
                  -> Variant (new += type') type)
  weakens func Here        = Var Here
  weakens func (There rest) = rename There (func rest)

  namespace General
    mutual
      namespace Fields
        public export
        subst : forall levelsO, levelsN
              . {old : Context levelsO}
             -> {new : Context levelsN}
             -> (f : forall level
                    . {type : Ty level}
                    -> Elem    old type
                    -> Variant new type)

             -> (forall types . Fields old types
                             -> Fields new types)

        subst f (Singleton (MkField desc))
          = Singleton (MkField (subst f desc))

        subst f (Extend (MkField desc) rest)
          = Extend (MkField (subst f desc)) (subst f rest)

      namespace Case
        public export
        subst : forall levelsO, levelsN
              . {old : Context levelsO}
             -> {new : Context levelsN}
             -> (f : forall level
                   . {type : Ty level}
                   -> Elem    old type
                   -> Variant new type)
             -> ({type : Ty VALUE} ->
                 {body : Ty level} -> Case old type body
                                   -> Case new type body)
        subst f (MkCase branch)
          = MkCase (subst (weakens f) branch)

      namespace Cases
        public export
        subst : forall levelsO, levelsN
              . {old : Context levelsO}
             -> {new : Context levelsN}
             -> (f : forall level
                   . {type : Ty level}
                   -> Elem    old type
                   -> Variant new type)
             -> (forall types . Cases old types type
                             -> Cases new types type)
        subst f (Singleton branch) =
          Singleton (Case.subst f branch)
        subst f (Extend branch rest)
          = Extend (Case.subst f branch) (subst f rest)

      public export
      subst : forall levelsO, levelsN
            . {old : Context levelsO}
           -> {new : Context levelsN}
           -> (f : forall level
                 . {type : Ty level}
                 -> Elem    old type
                 -> Variant new type)
           -> (forall level . {type : Ty level}
                            -> Variant old type
                            -> Variant new type)
      -- Let-Binding & Variables
      subst f (Var x) = f x
      subst f (Let this beInThis)
        = Let (subst f this)
              (subst (weakens f) beInThis)

      -- Base Values
      subst f (I x) = I x
      subst f (C x) = C x

      -- Type Constructors
      subst f TyInt  = TyInt
      subst f TyChar = TyChar

      subst f (TyVariant fields)
        = TyVariant (subst f fields)

      -- Variant Value Constructors
      subst f (Tag value type chk prf)
        = Tag (subst f value) (subst f type) chk prf

      -- Variant Matching
      subst f (Match value cases)
        = Match (subst f value) (subst f cases)

  namespace Single
    public export
    apply : forall levelA, levelB
          . {typeA  : Ty levelA}
         -> {typeB  : Ty levelB}
         -> (this   : Variant  ctxt           typeB)
         -> (idx    : Elem    (ctxt += typeB) typeA)
                   -> Variant  ctxt           typeA
    apply this Here         = this
    apply this (There rest) = Var rest

    public export
    subst : forall levelA, levelB
         .  {typeA  : Ty levelA}
         -> {typeB  : Ty levelB}
         -> {ctxt   : Context lvls}
         -> (this   : Variant  ctxt           typeB)
         -> (inThis : Variant (ctxt += typeB) typeA)
                   -> Variant  ctxt           typeA
    subst this inThis = General.subst (Single.apply this) inThis

namespace Values
  mutual
    namespace Field
      public export
      data Value : (field : Field g type) -> Type where
          MkField : (prf : Value field)
                        -> Value (MkField field)

    namespace Fields
      public export
      data Value : (fields : Fields g types) -> Type where
          Singleton : {field : Field g type}
                   -> (prf   : Value field)
                            -> Value (Singleton field)

          Extend : {field  : Field  g type}
                -> {fields : Fields g kvs}
                -> (prf    : Field.Value field)
                -> (rest   : Fields.Value fields)
                          -> Value (Extend field fields)
    public export
    data Value : Variant ctxt type -> Type where
      -- Base Values
      I : Value (I i)
      C : Value (C c)

      -- Type Constructors
      TyInt     : Value TyInt
      TyChar    : Value TyChar

      TyVariant : Value fields
               -> Value (TyVariant fields)

      -- Variant Value Constructors
      Tag : {types  : Vect (S n) (Ty TYPE)}
         -> {type   : Variant g (VariantTyDesc types)}

         -> {values : Vect (S n) (Ty VALUE)}

         -> {chk    : TyCheck (VariantTyDesc types) (VariantTy values)}

         -> {value  : Variant g value_type}

         -> {idx    : Elem value_type values}

         -> (prfT   : Value type)
         -> (prfV   : Value value)

                   -> Value (Tag value type chk idx)

namespace Reduction

  namespace Cases
    public export
    data Redux : (value  : Variant g type)
              -> (cases  : Cases g types body)
              -> (idx    : Elem type types)
              -> (result : Variant g body)
              -> Type
      where
        ReduceSingleton : {value : Variant g type}
                       -> {branch : Variant (type::g) type'}
                       -> Value value
                       -> Redux value
                                (Singleton (MkCase branch))
                                Here
                                (subst value branch)
        ReduceExtend : {value : Variant g type}
                    -> {rest : Cases g types body}
                    -> Value value
                    -> Redux value
                             (Extend (MkCase branch) rest)
                             Here
                             (subst value branch)

        SkipThis : Redux value rest later result
                -> Redux value
                         (Extend branch rest)
                         (There later)
                         result

  mutual
    namespace Field
      public export
      data Redux : (this, that : Field ctxt type) -> Type where
          SimplifyField :{this, that : Variant g type}
                       -> (prf : Redux this that)
                       -> Redux (MkField this) (MkField that)

    namespace Fields
      public export
      data Redux : (this, that : Fields g types) -> Type where
          SimplifySingleton : {this, that : Field g type}
                           -> (prf : Redux this that)
                                  -> Redux (Singleton this) (Singleton that)

          SimplifyExtendValue : {this, that : Field  g type}
                             -> {rest       : Fields g types}
                             -> (prf        : Redux this that)
                                           -> Redux (Extend this rest)
                                                    (Extend that rest)

          SimplifyExtendRest : {this, that : Fields ctxt types}
                            -> {field      : Field ctxt type}
                            -> (value      : Field.Value field)
                            -> (rest       : Redux this that)
                                          -> Redux (Extend field this)
                                                   (Extend field that)

    public export
    data Redux : (this, that : Variant ctxt type) -> Type where
      -- Let Bindings
      SimplifyLetValue : {this, that : Variant  ctxt typeV}
                      -> {body       : Variant (ctxt += typeV) typeB}
                      -> (redux      : Redux this that)
                                    -> Redux (Let this body)
                                             (Let that body)

      ReduceLetBody : {value : Variant ctxt typeV}
                   -> {body  : Variant (ctxt += typeV) typeB}
                   -> (prfV  : Value value)
                            -> Redux (Let value body)
                                    (subst value body)

      -- Variant Type Constructors
      SimplifyTyVariant : Redux this that
                       -> Redux (TyVariant this)
                                (TyVariant that)

      -- Variant Value Constructors
      SimplifyTagType : {this, that : Variant ctxt (VariantTyDesc kvs)}
                     -> {value      : Variant ctxt type}
                     -> (redux      : Redux this that)
                                   -> Redux (Tag value this chk idx)
                                            (Tag value that chk idx)

      SimplifyTagValue : {type       : Variant ctxt (VariantTyDesc types)}
                      -> (prfT       : Value type)
                      -> {this, that : Variant ctxt type'}
                      -> (redux      : Redux this that)
                                    -> Redux (Tag this type chk idx)
                                             (Tag that type chk idx)

      -- Variant Matching
      SimplifyMatchCase : {cases : Cases ctxt kvs type}
                       -> (redux : Redux this that)
                                -> Redux (Match this cases) (Match that cases)

      ReduceCases : {value : Variant g type_value}
                 -> {type  : Variant g (VariantTyDesc types)}

                 -> {this  : Cases g kvs body}
                 -> {that  : Variant g body}

                 -> (prfV  : Value value)
                 -> (prfT  : Value type)
                 -> (redux : Redux value this idx that)
                          -> Redux (Match (Tag value type chk idx) this)
                                   that

namespace Progress

  public export
  data Progress : (term : Variant Nil type)
               -> Type
    where
      Done : {term  : Variant Nil type}
          -> (value : Value term)
                   -> Progress term
      Step : {this, that : Variant Nil type}
          -> (step       : Redux this that)
                        -> Progress this

  namespace Field
    public export
    data Progress : (field : Field Nil type) -> Type where
      Done : (value : Value field) -> Progress field

      Step : {this, that : Field Nil type}
          -> (step       : Redux this that)
                        -> Progress this

  namespace Fields
    public export
    data Progress : (fields : Fields Nil types) -> Type where
      Done :  (value : Value fields) -> Progress fields

      Step : {this,that : Fields Nil types}
          -> (step      : Redux this that)
                       -> Progress this

  namespace Cases
    public export
    data Progress : (value : Variant Nil type)
                 -> (idx   : Elem type kvs)
                 -> (term  : Cases Nil kvs body)
                 -> Type
      where
        Step : {value : Variant Nil type'}
            -> {idx   : Elem type' kvs}
            -> {cases : Cases Nil kvs type}
            -> {that  : Variant Nil type}
            -> (step  : Redux value cases idx that)
                     -> Progress value idx cases

  -- The body is defined later on.
  public export
  progress : (term : Variant Nil type) -> Progress term

  mutual
    namespace Field
      public export
      progress : (field : Field Nil type) -> Progress field
      progress (MkField desc) with (Progress.progress desc)
        progress (MkField desc) | (Done value) = Done (MkField value)
        progress (MkField desc) | (Step step) = Step (SimplifyField step)

    namespace Fields
      public export
      progress : (fields : Fields Nil types) -> Progress fields
      progress (Singleton field) with (Field.progress field)
        progress (Singleton field) | (Done value) = Done (Singleton value)
        progress (Singleton field) | (Step step)  = Step (SimplifySingleton step)

      progress (Extend field rest) with (Field.progress field)
        progress (Extend field rest) | (Done value) with (Fields.progress rest)
          progress (Extend field rest) | (Done value) | (Done values)
            = Done (Extend value values)
          progress (Extend field rest) | (Done value) | (Step step)
            = Step (SimplifyExtendRest value step)
        progress (Extend field rest) | (Step step)
         = Step (SimplifyExtendValue step)

    namespace Cases
      public export
      progress : {value' : Variant Nil type}
              -> (idx   : Elem type kvs)
              -> (value : Value value')
              -> (term  : Cases Nil kvs body)
              -> Progress value' idx term
      progress Here value (Singleton (MkCase branch))
        = Step (ReduceSingleton value)

      progress Here value (Extend (MkCase branch) rest)
        = Step (ReduceExtend value)

      progress (There later) value (Extend branch rest) with (progress later value rest)
        progress (There later) value (Extend branch rest) | (Step step)
          = Step (SkipThis step)

    -- Body of progress from above.

    -- Let-Binding & Variables
    progress (Var _) impossible

    progress (Let this beInThis) with (progress this)
      progress (Let this beInThis) | (Done value) = Step (ReduceLetBody value)
      progress (Let this beInThis) | (Step step) = Step (SimplifyLetValue step)

    -- Base Value
    progress (I x) = Done I
    progress (C x) = Done C

    -- Variant Constructors
    progress TyInt  = Done TyInt
    progress TyChar = Done TyChar

    progress (TyVariant fields) with (Fields.progress fields)
      progress (TyVariant fields) | (Done value) = Done (TyVariant value)
      progress (TyVariant fields) | (Step step) = Step (SimplifyTyVariant step)

    -- Variant Value Constructors
    progress (Tag field type chk prf) with (progress type)
      progress (Tag field type chk prf) | (Done valueT) with (progress field)
        progress (Tag field type chk prf) | (Done valueT) | (Done valueF)
          = Done (Tag valueT valueF)
        progress (Tag field type chk prf) | (Done valueT) | (Step stepF)
          = Step (SimplifyTagValue valueT stepF)
      progress (Tag field type chk prf) | (Step step)
        = Step (SimplifyTagType step)

    -- Variant Matching
    progress (Match field cases) with (progress field)
      progress (Match (Tag label value t idx) cases) | (Done (Tag prfT prfV)) with (Cases.progress idx prfV cases)
        progress (Match (Tag label value t idx) cases) | (Done (Tag prfT prfV)) | (Step step)
          = Step (ReduceCases prfV prfT step)

      progress (Match field cases) | (Step step) = Step (SimplifyMatchCase step)

namespace Evaluation

  public export
  data Reduces : (this : Variant ctxt type)
              -> (that : Variant ctxt type)
              -> Type
    where
      Refl  : {this : Variant ctxt type}
                   -> Reduces this this

      Trans : {this, that, end : Variant ctxt type}
                              -> Redux this that
                              -> Reduces that end
                              -> Reduces this end

  public export
  data Finished : (term : Variant ctxt type)
                       -> Type
    where
      Normalised : {term : Variant ctxt type}
                        -> Value term
                        -> Finished term
      OOF : Finished term

  public export
  data Evaluate : (term : Variant Nil type) -> Type where
    RunEval : {this, that : Variant Nil type}
           -> (steps      : Inf (Reduces this that))
           -> (result     : Finished that)
                         -> Evaluate this

  public export
  data Fuel = Empty | More (Lazy Fuel)

  public export
  covering
  forever : Fuel
  forever = More forever

  public export
  compute : (fuel : Fuel)
         -> (term : Variant Nil type)
                 -> Evaluate term
  compute Empty term = RunEval Refl OOF
  compute (More fuel) term with (progress term)
    compute (More fuel) term | (Done value) = RunEval Refl (Normalised value)
    compute (More fuel) term | (Step step {that}) with (compute fuel that)
      compute (More fuel) term | (Step step {that}) | (RunEval steps result)
        = RunEval (Trans step steps) result

public export
covering
run : (this : Variant Nil type)
           -> Maybe (Subset (Variant Nil type) (Reduces this))
run this with (compute forever this)
  run this | (RunEval steps (Normalised {term} x))
    = Just (Element term steps)
  run this | (RunEval steps OOF) = Nothing

namespace Example
  public export
  iciTy : Variant Nil (VariantTyDesc [IntTyDesc, CharTyDesc])
  iciTy = TyVariant (Extend (MkField TyInt)
                            (Singleton (MkField TyChar)))

  public export
  ici : Variant Nil (VariantTy [IntTy, CharTy])
  ici = Tag (I 1) iciTy (CheckVar (CheckRest CheckInt (CheckOne CheckChar))) Here

  public export
  icc : Variant Nil (VariantTy [IntTy, CharTy])
  icc = Let iciTy (Tag (C 'c') (Var Here) (CheckVar (CheckRest CheckInt (CheckOne CheckChar))) (There Here))

  public export
  iciM : Variant Nil IntTy
  iciM = Match ici (Extend            (MkCase (Var Here))
                           (Singleton (MkCase (I 2))))

  public export
  iccM : Variant Nil IntTy
  iccM = Match icc (Extend            (MkCase (Var Here))
                           (Singleton (MkCase (I 2))))

ext: idr

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/values.html#integers
module WebAssembly.Structure.Values.Integers

-- Definition

-- This module only provides a rough over-approximation of WebAssembly's integer-data-types
-- Unsigned and uninterpreted integers are modelled by Idris' (unbounded) natural numbers
-- Signed integers are modelles by Idris' (unbounded) integers

||| Unsigned Integer 32 Bit
public export
U32 : Type
U32 = Nat

||| Signed Interer 32 Bit
public export
S32 : Type
S32 = Integer

||| Uninterpreted Integer 32 Bit
public export
I32 : Type
I32 = Nat

||| Unsigned Integer 32 Bit
public export
U64 : Type
U64 = Nat

||| Signed Interer 32 Bit
public export
S64 : Type
S64 = Integer

||| Uninterpreted Integer 32 Bit
public export
I64 : Type
I64 = Nat

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
import Data.Vect

readVect : IO (len ** Vect len String)
readVect = do x <- getLine
              if (x == "")
                    then pure (_ ** [])
                    else do (_ ** xs) <- readVect
                            pure (_ ** x :: xs)

zipInputs : IO ()
zipInputs = do putStrLn "Enter first vector (blank line to end):"
               (len1 ** vec1) <- readVect
               putStrLn "Enter second vector (blank line to end):"
               (len2 ** vec2) <-readVect
               (case exactLength len1 vec2 of
                     Nothing => putStrLn "Vectors are of different lengths"
                     (Just vec2') => printLn (zip vec1 vec2'))


text:
module BankersDeque

import Deque

%default total
%access private

export
data BankersDeque a = BD Int (List a) Int (List a)

c : Int
c = 3

check : Int -> List a -> Int -> List a -> BankersDeque a
check lenf f lenr r =
  if lenf > c * lenr + 1 then
     let i = assert_total $ (lenf + lenr) `div` 2
         j = lenf + lenr - i
         f' = take (toNat i) f
         r' = r ++ reverse (drop (toNat i) f)
     in BD i f' j r'
  else if lenr > c * lenf + 1 then
    let j = assert_total $ (lenf + lenr) `div` 2
        i = lenf + lenr - j
        r' = take (toNat j) r
        f' = f ++ reverse (drop (toNat j) r)
    in BD i f' j r'
  else BD lenf f lenr r

export
Deque BankersDeque where
  empty = BD 0 [] 0 []
  isEmpty (BD lenf f lenr r) = lenf + lenr == 0

  cons x (BD lenf f lenr r) = check (lenf + 1) (x :: f) lenr r

  head (BD lenf []        lenr [x]) = x -- Missing in Haskell original
  head (BD lenf []        lenr r)   = idris_crash "empty deque"
  head (BD lenf (x :: f') lenr r)   = x

  tail (BD lenf []        lenr [x]) = empty -- Missing in Haskell original
  tail (BD lenf []        lenr r)   = idris_crash "empty deque"
  tail (BD lenf (x :: f') lenr r)   = check (lenf - 1) f' lenr r

  snoc (BD lenf f lenr r) x = check lenf f (lenr + 1) (x :: r)

  last (BD lenf [x] lenr [])        = x -- Missing in Haskell original
  last (BD lenf f   lenr [])        = idris_crash "empty deque"
  last (BD lenf f   lenr (x :: r')) = x

  init (BD lenf [x] lenr [])        = empty -- Missing in Haskell original
  init (BD lenf f   lenr [])        = idris_crash "empty deque"
  init (BD lenf f   lenr (x :: r')) = check lenf f (lenr - 1) r'


text:
module Sub04LTE216t153

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(36t+25)+3 --AE[6,-2,-4]--> 6(4t+1)+3
export
lte216t153 : (m : Nat) -> LTE (S (S ((m+m)+(m+m))))
  (S (((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m))))))))
lte216t153 Z     = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc) LTEZero
lte216t153 (S m) =
  let lemma = lte216t153 m in

  rewrite (sym (plusSuccRightSucc m m)) in

  rewrite (sym (plusSuccRightSucc (plus m m) (S (plus m m)))) in
  rewrite (sym (plusSuccRightSucc (plus m m)    (plus m m))) in

  rewrite (sym (plusSuccRightSucc (plus m m) m)) in

  rewrite (sym (plusSuccRightSucc (plus (plus m m) m) (S (S (S (plus (plus m m) m)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus m m) m)    (S (S (plus (plus m m) m))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus m m) m)       (S (plus (plus m m) m)))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                        (S (S (S (S (S (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                           (S (S (S (S (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                              (S (S (S (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                                 (S (S (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                                    (S (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                                       (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                        (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                           (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                              (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                 (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                       (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                          (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                             (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                                (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                                   (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                                      (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus m m) m) (S (plus (plus m m) m)))
                    (S (S (S (plus (plus (plus m m) m) (S (plus (plus m m) m)))))))
                                                         (S (S (S (plus (plus (plus (plus m m) m)
                                                                (S (plus (plus m m) m)))
                                                          (S (S (S (plus (plus (plus m m) m)
                                                                         (S (plus (plus m m)
                                                          m)))))))))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                   (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                   (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                      (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                         (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                            (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                               (S (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                                  (S (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                                     (S (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                                        (S (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                                           (S (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus m m) m)
                                                      (S (plus (plus m m) m)))
                                                (S (S (S (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))))))
                                          (S (S (S (plus (plus (plus (plus m m) m)
                                                               (S (plus (plus m m) m)))
                                                         (S (S (S (plus (plus (plus m m) m)
                                                                        (S (plus (plus m m) m)))))))))))
                                              (S (S (S (plus (plus (plus (plus m m) m)
                                                                     (S (plus (plus m m) m)))
                                                    (S (S (S (plus (plus (plus m m) m)
                                                          (S (plus (plus m m)
                              m)))))))))))) in

    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
-- ---------------------------------------------------------------- [ Tree.idr ]
-- Module    : Tree.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A Dependently Typed Implementation of an AVL Tree optimised for
||| Dictionaries.
|||
||| This code is dervied from an original design by David
||| Christiansen.
|||
||| *Note* When using this Data Structure, the design is such that the
||| tree does not factor in unbalanced trees and so removal of items
||| is not permited.
module Data.AVL

%default total
%access export

namespace Core
  -- ------------------------------------------------------------- [ Definitions ]
  data Balance : Nat -> Nat -> Type where
    LHeavy   : Balance (S n) n
    RHeavy   : Balance n     (S n)
    Balanced : Balance n     n

  %name Balance b, bal

  ||| Indirection ensures that it reduces to at least S n' without
  ||| needing to case split on balance.
  |||
  ||| Should make proofs easier.
  height : Balance n m -> Nat
  height b = S (height' b)
    where
      height' : Balance n m -> Nat
      height' (LHeavy {n}) = S n
      height' (RHeavy {n}) = S n
      height' {n} (Balanced {n}) = n

  ||| The core tree key-value data structure used to represent an AVL
  ||| Tree.
  |||
  ||| This structure doesn't encode the invariants of the tree and is
  ||| *simply* a container. This structure ideally shouldn't be exposed
  ||| to the user at all. This structure should be used to build other
  ||| data structures.  See the modules alongside this for appropriate
  ||| interfaces for using the tree.
  |||
  ||| @keyTy The type associated with the key.
  ||| @valTy The type associated with the value.
  public export
  data Tree : (keyTy : Type)
           -> (valTy : Type)
           -> Type
    where
      ||| An empty Tree node.
      Empty : Tree k v

      ||| A Key Value node in the Tree.
      |||
      ||| @key   The key.
      ||| @val   The value associated with the key.
      ||| @left  The left child of the Node
      ||| @right THe right child of the Node.
      Node : (key   : k)
          -> (val   : v)
          -> (left  : Tree k v)
          -> (right : Tree k v)
          -> Tree k v

  %name Tree t, tree

  ||| Encoding of the AVL tree height invariants.
  |||
  ||| @height The height of a Tree.
  ||| @tree   The tree whose height we are capturing.
  public export
  data AVLInvariant : (height : Nat)
                   -> (tree   : Tree k v)
                   -> Type
    where
      ||| A tree of height zero.
      AVLEmpty : AVLInvariant 0 Empty
      ||| A Balanced tree.
      |||
      ||| @left  The invariant of the left child.
      ||| @right The invariant of the right child.
      ||| @b     The encoding of the nodes' balance.
      AVLNode : (left  : AVLInvariant n l)
             -> (right :  AVLInvariant m r)
             -> (b : Balance n m)
             -> AVLInvariant (height b) (Node k v l r)

  %name AVLInvariant inv

||| An AVL Tree.
|||
||| Modelled using subset to separate the invariants from the tree
||| implementation itself.
|||
||| @height  The height of the Tree.
||| @keyTy   The type associated with the keys.
||| @valueTy The type associated with the values.
public export
AVLTree : (height  : Nat)
       -> (keyTy   : Type)
       -> (valueTy : Type)
       -> Type
AVLTree n k v = Subset (Tree k v) (AVLInvariant n)

namespace Modification

 -- --------------------------------------------------------------- [ Rotations ]
  private
  data InsertRes : Nat -> (k : Type) -> Type -> Type where
    Same : AVLTree n k v     -> InsertRes n k v
    Grew : AVLTree (S n) k v -> InsertRes n k v

  %name InsertRes res, r

  ||| Process the result of an insertion of a new Key-Value pair into
  ||| the Tree, returning the new tree and proof of the new tree's
  ||| height.
  |||
  ||| `InsertRes` is obtained from the result of running `Tree.insert`.
  private
  runInsertRes : InsertRes n k v -> (n : Nat ** AVLTree n k v)
  runInsertRes (Same t) = (_ ** t)
  runInsertRes (Grew t) = (_ ** t)

  ||| Perform a Left roation.
  private
  rotLeft : k
         -> v
         -> AVLTree n k v
         -> AVLTree (S (S n)) k v
         -> InsertRes (S (S n)) k v
  -- Impossible because Empty has depth 0 and we know the depth is at least 2 from the type
  rotLeft key val l (Element Empty AVLEmpty) impossible

  rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr Balanced)) =
      Grew $ Element (Node key' val' (Node key val l rl) rr)
                          (AVLNode (AVLNode invl invrl RHeavy) invrr LHeavy)

  rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr LHeavy) invrr LHeavy)) =
      Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr)) -- Needs Checking
                     (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr RHeavy) Balanced)

  rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr RHeavy) invrr LHeavy)) =
      Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr))
                     (AVLNode (AVLNode invl invrll LHeavy) (AVLNode invrlr invrr Balanced) Balanced)

  rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr Balanced) invrr LHeavy)) =
      Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr))
                     (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr Balanced) Balanced) -- Needs Checking

  rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr RHeavy)) =
      Same $ Element (Node key' val' (Node key val l rl) rr)
                     (AVLNode (AVLNode invl invrl Balanced) invrr Balanced)

  ||| Perform a Right rotation.
  private
  rotRight : k
          -> v
          -> AVLTree (S (S n)) k v
          -> AVLTree n k v
          -> InsertRes (S (S n)) k v
  rotRight key val (Element Empty AVLEmpty) r impossible

  rotRight key'' val'' (Element (Node key val ll (Node key' val' lrl lrr))
               (AVLNode invll (AVLNode invlrl invlrr RHeavy) RHeavy)) (Element r invr) =
    Same $ Element (Node key' val' (Node key val ll lrl) (Node key'' val'' lrr r))
                   (AVLNode (AVLNode invll invlrl LHeavy) (AVLNode invlrr invr Balanced) Balanced)

  rotRight key'' val'' (Element (Node key val ll (Node key' val' lrl lrr))
               (AVLNode invll (AVLNode invlrl invlrr LHeavy) RHeavy)) (Element r invr) =
    Same $ Element (Node key' val' (Node key val ll lrl) (Node key'' val'' lrr r))
                   (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr RHeavy) Balanced)

  rotRight key val (Element (Node key' val' ll lr) (AVLNode invll invlr Balanced)) (Element r invr) =
    Grew $ Element (Node key' val' ll (Node key val lr r))
                   (AVLNode invll (AVLNode invlr invr LHeavy) RHeavy)

  rotRight key val (Element (Node key' val' ll lr) (AVLNode invll invlr LHeavy)) (Element r invr) =
    Same $ Element (Node key' val' ll (Node key val lr r))
                   (AVLNode invll (AVLNode invlr invr Balanced) Balanced)

  rotRight key val (Element (Node key' val' ll (Node key'' val'' lrl lrr))
               (AVLNode invll (AVLNode invlrl invlrr Balanced) RHeavy)) (Element r invr) =
    Same $ Element (Node key'' val'' (Node key' val' ll lrl) (Node key val lrr r))
                   (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr Balanced) Balanced)

-- --------------------------------------------------------------- [ Insertion ]

  ||| Perform an insertion into the tree returning the new tree wrapped
  ||| in a description describing the height change.
  private
  doInsert : (Ord k) => k
                     -> v
                     -> AVLTree n k v
                     -> InsertRes n k v
  doInsert newKey newVal (Element Empty AVLEmpty) = Grew (Element (Node newKey newVal Empty Empty)
                                                                (AVLNode AVLEmpty AVLEmpty Balanced))
  doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) with (compare newKey key)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | EQ = Same (Element (Node newKey newVal l r) (AVLNode invl invr b))

    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | LT with (assert_total $ doInsert newKey newVal (Element l invl))
      -- Totality checker not clever enough to see that this is smaller
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b))        | LT | (Same (Element l' invl'))
                                                                                = Same $ Element (Node key val l' r) (AVLNode invl' invr b)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr LHeavy))   | LT | (Grew (Element l' invl'))
                                                                                = rotRight key val (Element l' invl') (Element r invr)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr Balanced)) | LT | (Grew (Element l' invl'))
                                                                                = Grew $ Element (Node key val l' r) (AVLNode invl' invr LHeavy)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr RHeavy))   | LT | (Grew (Element l' invl'))
                                                                                = Same $ Element (Node key val l' r) (AVLNode invl' invr Balanced)

    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | GT with (assert_total $ doInsert newKey newVal (Element r invr))
    -- Totality checker not clever enough to see that this is smaller
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b))        | GT | (Same (Element r' invr'))
                                                                                = Same $ Element (Node key val l r') (AVLNode invl invr' b)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr LHeavy))   | GT | (Grew (Element r' invr'))
                                                                                = Same $ Element (Node key val l r') (AVLNode invl invr' Balanced)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr Balanced)) | GT | (Grew (Element r' invr'))
                                                                                = Grew $ Element (Node key val l r') (AVLNode invl invr' RHeavy)
      doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr RHeavy))   | GT | (Grew (Element r' invr'))
                                                                                = rotLeft key val (Element l invl) (Element r' invr')

-- --------------------------------------- [ Public API for working with Trees ]
namespace API

  ||| Insert a key value pair into the tree, returning a the new tree
  ||| and possibly its new height.
  insert : Ord k => k -> v -> AVLTree n k v -> (n : Nat ** AVLTree n k v)
  insert k v t = runInsertRes (doInsert k v t)

  ||| Find a value in the tree.
  lookup : (Ord k) => k -> AVLTree h k v -> Maybe v
  lookup key (Element t _) = lookup' key t
    where
      lookup' : (Ord k) => k -> Tree k v -> Maybe v
      lookup' key Empty = Nothing
      lookup' key (Node key' value' l r) with (compare key key')
        lookup' key (Node key' value' l r) | LT = lookup' key l
        lookup' key (Node key' value' l r) | EQ = Just value'
        lookup' key (Node key' value' l r) | GT = lookup' key r

  ||| Update an element in the tree.
  update : (Ord k) => k
                   -> (v -> v)
                   -> AVLTree h k v
                   -> AVLTree h k v
  update key f t@(Element Empty inv) = t
  update key f (Element (Node key' value' l r) inv) with (compare key key')
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | LT with (assert_total $ update key f (Element l invl)) -- Totality checker again
        update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | LT | (Element l' invl')
                                                             = Element (Node key' value' l' r) (AVLNode invl' invr b)
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | EQ
                                                             = Element (Node key' (f value') l r) (AVLNode invl invr b)
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | GT with (assert_total $ update key f (Element r invr))
        update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | GT | (Element r' invr')
                                                             = Element (Node key' value' l r') (AVLNode invl invr' b)

  ||| Perform a right fold over the tree.
  foldr : (step : k -> v -> p -> p)
       -> (init : p)
       -> AVLTree n k v
       -> p
  foldr step init (Element t _) = foldr' step init t
    where
      foldr' : (k -> v -> p -> p) -> p -> Tree k v -> p
      foldr' step' init' Empty = init'
      foldr' step' init' (Node key val l r) = foldr' step' (step' key val (foldr' step' init' r)) l

  ||| Construct a AVL Tree from an association list.
  fromList : (Ord k) => List (k, v)
                     -> (n : Nat ** AVLTree n k v)
  fromList [] = (0 ** Element Empty AVLEmpty)
  fromList ((k, v) :: xs) with (doInsert k v (snd (fromList xs)))
    fromList ((k, v) :: xs) | (Same x) = (_ ** x)
    fromList ((k, v) :: xs) | (Grew x) = (_ ** x)

  ||| Flatten the tree to an association list.
  toList : AVLTree n k v -> List (k, v)
  toList = foldr (\k,v,xs => (k, v) :: xs) []

  ||| Is the tree empty?
  isEmpty : AVLTree h k v -> Bool
  isEmpty (Element t _) = isEmpty' t
    where
      isEmpty' : Tree k v -> Bool
      isEmpty' Empty          = True
      isEmpty' (Node _ _ _ _) = False

  ||| Calculate the size of the tree.
  size : AVLTree h k v -> Nat
  size = foldr (\_,_=> S) 0

  ||| Return a list of keys in the tree.
  keys : AVLTree h k v -> List k
  keys = map fst . toList

  ||| Return a list of the values in the key.
  values : AVLTree h k v -> List v
  values = map snd . toList

  ||| Check if the provided check holds for all elements in the tree.
  all : (pred : k -> v -> Bool) ->  AVLTree h k v -> Bool
  all pred = foldr (\k,v,pred' => pred' && pred k v) True

  ||| Check if the provided check holds for at least one element in the tree.
  any : (pred : k -> v -> Bool) ->  AVLTree h k v -> Bool
  any pred = foldr (\k,v,pred' => pred' || pred k v) False

  ||| Does the given key exist in the tree?
  hasKey : (o : Ord k) => k -> AVLTree h k v -> Bool
  hasKey key = any (\key',value' => key == key')

  ||| Does the given value exist in the tree?
  hasValue : (Eq v) => v -> AVLTree h k v -> Bool
  hasValue value = any (\key',value' => value == value')

  ||| Find the first key that satisfies the provided predicate.
  findKey : (pred : v -> Bool) -> AVLTree h k v -> Maybe k
  findKey pred = foldr (\k,v,p => if pred v then Just k else p) Nothing

  ||| Find the key that is associated with provided value.
  findKeyOf : (Eq v) => v -> AVLTree h k v -> Maybe k
  findKeyOf value = findKey (== value)

-- --------------------------------------------------------- [ Implementations ]

private
eqTree : (Eq k, Eq v) => Tree k v -> Tree k v -> Bool
eqTree Empty              Empty              = True
eqTree (Node xk xv xl xr) (Node yk yv yl yr) =
      xk == yk  &&
      xv == yv  &&
      eqTree xl yl &&
      eqTree xr yr
eqTree _ _                                   = False

namespace Implementation

  (Eq k, Eq v) => Eq (Tree k v) where
    (==) = eqTree

  (Eq k, Eq v) => Eq (AVLTree h k v) where
    (==) (Element t _) (Element t' _) = t == t'

  (Show k, Show v) => Show (Tree k v) where
    show Empty          = ""
    show (Node k v l r) = unwords
        [
          "{"
        , show l
        , "(", show k, ":", show v, "),"
        , show r
        , "}"
        ]

  (Show k, Show v) => Show (AVLTree h k v) where
    show (Element t _) = show t

-- --------------------------------------------------------------------- [ Key ]

namespace Core
  namespace Quantifiers
    namespace OnKeys
      public export
      data AllKeys : (predicate : typeKey -> Type)
                  -> (tree      : Tree typeKey typeValue)
                  -> Type
        where
          Leaf : AllKeys p Empty
          Node : (prf : p key)
              -> (leftBranch  : AllKeys p left)
              -> (rightBranch : AllKeys p right)
              -> AllKeys p (Node key _ left right)

    namespace OnValues
      data AllValues : (predicate : typeValue -> Type)
                    -> (tree      : Tree typeKey typeValue)
                    -> Type
        where
          Leaf : AllValues p Empty
          Node : (prf : p value)
              -> (leftBranch  : AllValues p left)
              -> (rightBranch : AllValues p right)
              -> AllValues p (Node _ value left right)

    namespace OnKVPairs
       data AllKVPairs : (predicate : typeKey -> typeValue -> Type)
                      -> (tree      : Tree typeKey typeValue)
                      -> Type
        where
          Leaf : AllKVPairs p Empty
          Node : (prf : p key value)
              -> (leftBranch  : AllKVPairs p left)
              -> (rightBranch : AllKVPairs p right)
              -> AllKVPairs p (Node key value left right)

  namespace Predicate
    namespace OnValues
      public export
      data IsValueIn : (value : typeValue)
                    -> (tree  : Tree typeKey typeValue)
                    -> Type
        where
          Here    : IsValueIn value (Node _ value _ _)
          InRight : (later : IsValueIn value r) -> IsValueIn value (Node _ _ _ r)
          InLeft  : (later : IsValueIn value l) -> IsValueIn value (Node _ _ l _)

      emptyTreeHasNoValue : IsValueIn value Empty -> Void
      emptyTreeHasNoValue Here impossible
      emptyTreeHasNoValue (InRight _) impossible
      emptyTreeHasNoValue (InLeft _) impossible

      Uninhabited (IsValueIn value Empty) where
        uninhabited Here impossible
        uninhabited (InRight _) impossible
        uninhabited (InLeft _) impossible

      ||| A decision procedure for Value
      valueNotFound : (notHere : (value = val) -> Void)
                   -> (isNotLeft : IsValueIn value left -> Void)
                   -> (isNotRight : IsValueIn value right -> Void)
                   -> IsValueIn value (Node key val left right)
                   -> Void
      valueNotFound notHere isNotLeft isNotRight Here = notHere Refl
      valueNotFound notHere isNotLeft isNotRight (InRight later) = isNotRight later
      valueNotFound notHere isNotLeft isNotRight (InLeft later) = isNotLeft later

      isValue : DecEq typeValue
             => (value : typeValue)
             -> (tree : Tree typeKey typeValue)
             -> Dec (IsValueIn value tree)
      isValue value Empty = No emptyTreeHasNoValue
      isValue value (Node key val left right) with (decEq value val)
        isValue val (Node key val left right) | (Yes Refl) = Yes Here
        isValue value (Node key val left right) | (No notHere) with (isValue value left)
          isValue value (Node key val left right) | (No notHere) | (Yes prf) = Yes (InLeft prf)
          isValue value (Node key val left right) | (No notHere) | (No isNotLeft) with (isValue value right)
            isValue value (Node key val left right) | (No notHere) | (No isNotLeft) | (Yes prf) = Yes (InRight prf)
            isValue value (Node key val left right) | (No notHere) | (No isNotLeft) | (No isNotRight) = No (valueNotFound notHere isNotLeft isNotRight)

    namespace OnKeys
      ||| A proof that some key is found in a Tree
      public export
      data IsKeyIn : k -> Tree k v -> Type where
        Here : IsKeyIn key (Node key _ _ _)
        InRight : (later : IsKeyIn key r) -> IsKeyIn key (Node _ not_key _ r)
        InLeft : (later : IsKeyIn key l) -> IsKeyIn key (Node _ not_key l _)

      ||| An empty tree has no key
      emptyTreeHasNoKey : {key : k} -> IsKeyIn key Empty -> Void
      emptyTreeHasNoKey Here impossible
      emptyTreeHasNoKey (InRight _) impossible
      emptyTreeHasNoKey (InLeft _) impossible

      Uninhabited (IsKeyIn key Empty) where
        uninhabited = emptyTreeHasNoKey

      ||| An item that is not in the root, not in the left child and not in the
      ||| right child is not in the Tree at all
      noKeyFound : {key : k}
                -> {val : v}
                -> {key' : k}
                -> {l : Tree k v}
                -> {r : Tree k v}
                -> Not (key = key')
                -> Not (IsKeyIn key l)
                -> Not (IsKeyIn key r)
                -> Not (IsKeyIn key (Node key' val l r))
      noKeyFound notHere notInLeft notInRight Here = notHere Refl
      noKeyFound notHere notInLeft notInRight (InLeft later) = notInLeft later
      noKeyFound notHere notInLeft notInRight (InRight later) = notInRight later

      ||| A decision procedure for Key
      isKey : DecEq k
           => (key : k)
           -> (tree : Tree k v)
           -> Dec (IsKeyIn key tree)
      isKey key Empty = No emptyTreeHasNoKey
      isKey key (Node key' _ l r) with (decEq key key')
        isKey key (Node key  _ l r) | (Yes Refl) = Yes Here
        isKey key (Node key' _ l r) | (No notHere) with (isKey key l)
          isKey key (Node key' _ l r) | (No notHere) | (Yes inLeft) = Yes (InLeft inLeft)
          isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) with (isKey key r)
            isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) | (Yes inRight) = Yes (InRight inRight)
            isKey key (Node key' _ l r) | (No notHere) | (No notInLeft) | (No notInRight) = No (noKeyFound notHere notInLeft notInRight)

public export
data HasKey : (key : typeKey)
           -> (tree : AVLTree h typeKey typeValue)
           -> Type
  where
    IsKey : (prf : IsKeyIn key (Subset.getWitness avl))
         -> HasKey key avl

keyNotInAVlTree : (contra : IsKeyIn key tree -> Void)
               -> HasKey key (Element tree prf)
               -> Void
keyNotInAVlTree contra (IsKey x) = contra x

isKey : DecEq typeKey
     => (key : typeKey)
     -> (tree : AVLTree h typeKey typeValue)
     -> Dec (HasKey key tree)
isKey key (Element tree prf) with (isKey key tree)
  isKey key (Element tree prf) | (Yes x) = Yes (IsKey x)
  isKey key (Element tree prf) | (No contra) = No (keyNotInAVlTree contra)

public export
data HasValue : (value : typeValue)
             -> (tree : AVLTree h typeKey typeValue)
             -> Type
  where
    IsValue : (prf : IsValueIn value (Subset.getWitness avl))
           -> HasValue value avl

valueNotInAVLTree : (contra : IsValueIn value tree -> Void)
                 -> HasValue value (Element tree prf)
                 -> Void
valueNotInAVLTree contra (IsValue prf) = contra prf

isValue : DecEq typeValue
       => (value : typeValue)
       -> (tree : AVLTree h typeKey typeValue)
       -> Dec (HasValue value tree)
isValue value (Element tree prf) with (isValue value tree)
  isValue value (Element tree prf) | (Yes x) = Yes (IsValue x)
  isValue value (Element tree prf) | (No contra) = No (valueNotInAVLTree contra)

-- Quantifiers
public export
data AllKeys : (predicate : typeKey -> Type)
            -> (tree : AVLTree h typeKey typeValue)
            -> Type
  where
    AllKeysSatisfyPredicate : (prf : OnKeys.AllKeys p (Subset.getWitness avl))
                           -> AllKeys p avl

public export
data AllValues : (predicate : typeValue -> Type)
              -> (tree : AVLTree h typeKey typeValue)
              -> Type
  where
    AllValuesSatisfyPredicate : (prf : OnValues.AllValues p (Subset.getWitness avl))
                             -> AllValues p avl

public export
data AllKVPairs : (predicate : typeKey -> typeValue -> Type)
               -> (tree : AVLTree k typeKey typeValue)
               -> Type
  where
    AllKVPairsSatisfyPredicate : (prf : OnKVPairs.AllKVPairs p (Subset.getWitness avl))
                              -> AllKVPairs p avl
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: elba/idris-containers

max_issues_repo_name: elba/idris-containers

max_forks_repo_name: elba/idris-containers


text:
module Utils.IPAddr

import Data.String.Parser
import Data.Vect
import Data.Fin
import Data.String.Extra
import Data.String
import Utils.Num
import Utils.Misc
import Data.List
import Data.List1
import Data.Bits
import Utils.Bytes

public export
record IPv4Addr where
  constructor MkIPv4Addr
  body : Vect 4 Bits8

public export
Show IPv4Addr where
  show x = join "." $ map show x.body

public export
Eq IPv4Addr where
  x == y = x.body == y.body

public export
record IPv6Addr where
  constructor MkIPv6Addr
  body : Vect 16 Bits8

bits16_show : Bits16 -> String
bits16_show x = (show_hex (cast $ shiftR x 8)) <+> (show_hex $ cast x)

to_hextets : IPv6Addr -> Vect 8 Bits16
to_hextets addr = map from_be $ group 8 2 addr.body

public export
Show IPv6Addr where
  show x = assert_total $ join ":" $ map bits16_show (to_hextets x)

public export
Eq IPv6Addr where
  x == y = x.body == y.body

read_decimal_byte : Monad m => ParseT m Bits8
read_decimal_byte = do
  n <- natural
  if n < 256
    then pure $ cast n
    else fail "number out of bound"

parse_ipv4' : Monad m => ParseT m IPv4Addr
parse_ipv4' = do
  a <- read_decimal_byte
  _ <- char '.'
  b <- read_decimal_byte
  _ <- char '.'
  c <- read_decimal_byte
  _ <- char '.'
  d <- read_decimal_byte
  pure $ MkIPv4Addr [a, b, c, d]

export
parse_ipv4 : String -> Either String IPv4Addr
parse_ipv4 = map fst . parse parse_ipv4'

data IPv6R : Type -> Type where
  One : a -> IPv6R a
  Two : a -> a -> IPv6R a

splitDoubleColon : String -> Either String (IPv6R String)
splitDoubleColon str = do
  let (a ::: [b]) = split ((':', ':') ==) (f $ unpack str)
  | (a ::: []) => pure (One str)
  | _ => Left "too many double colons"
  pure $ Two (pack $ map fst a) (pack $ map snd b)
  where
    f : List Char -> List (Char, Char)
    f [] = []
    f (x :: xs) = zip (x :: xs) xs

parse_ipv6_to_octets : String -> Either String (IPv6R (List Bits16))
parse_ipv6_to_octets string = do
  Two a b <- splitDoubleColon string
  | One a => One <$> to a
  a <- to a
  b <- to b
  pure $ Two a b
  where
    go : String -> Either String Bits16
    go x = do
      let Just hex = stringToNat' 16 x
      | Nothing => Left $ "invalid hextet: " <+> x
      if hex < 65536
        then Right $ cast hex
        else Left "number out of bound"
    to : String -> Either String (List Bits16)
    to "" = Right []
    to x = traverse go $ toList $ split (':' ==) x

parse_ipv6_expand_columns : IPv6R (List Bits16) -> Either String (Vect 8 Bits16)
parse_ipv6_expand_columns (One a) = maybe_to_either (exactLength _ $ fromList a) "invalid length"
parse_ipv6_expand_columns (Two a b) = do
  let plen = minus 8 (length a + length b)
  let apb = a <+> replicate plen 0 <+> b
  maybe_to_either (exactLength _ $ fromList apb) "invalid length"

export
parse_ipv6 : String -> Either String IPv6Addr
parse_ipv6 x = do
  y <- (parse_ipv6_to_octets x >>= parse_ipv6_expand_columns)
  pure $ MkIPv6Addr $ concat $ map (to_be {n=2}) y


text:
import Adder
import DataStore
import DataStoreHoles
import Maybe
import Printf
import TypeFuns
import TypeSynonyms


text:
import Erlang

%default partial

foo : Maybe a -> a
foo (Just x) = x

data Vect : ? -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

lookup : Fin n -> Vect n a -> a
lookup FZ (x :: xs) = x
lookup (FS k) (x :: xs) = lookup k xs

lookup' : Fin n -> Vect n a -> a
lookup' (FS k) (x :: xs) = lookup' k xs

lookup'' : Fin n -> Vect n a -> a
lookup'' n xs = lookup' n xs

ex1 : IO ()
ex1 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  let x = foo Nothing
  printLn (the Int x)

ex2 : IO ()
ex2 = printLn $ lookup (FS FZ) [1,2,3,4]

ex3 : IO ()
ex3 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  printLn $ lookup' (FS FZ) [1,2,3,4]

ex4 : IO ()
ex4 = do
  putStr "" -- TODO: Workaround to avoid pruning this function
  printLn $ lookup'' (FS FZ) [1,2,3,4]

try : IO () -> IO ()
try action = do
  Right _ <- erlTryCatch action
    | Left (MkTuple3 _ msg _) => putStrLn (erlUnsafeCast String msg)
  pure ()

main : IO ()
main = do
  try ex1
  try ex2
  try ex3
  try ex4