fallbacks1.agda

{-
Modeled the following Haskell code in Agda
Confirmed that the Agda Termination Checker fails on it
https://github.com/khibino/dnsext/blob/95ae07de77174e8a6ea80f075412549222c9a900/dnsext-iterative/DNS/Iterative/Query/ResolveJust.hs#L550-L583
 -}

open import Agda.Builtin.Unit using (⊤; tt)
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.List using (List; []; _∷_)

--------------------------------------------------------------------
-- pseudo impementations

Unit : Set
Unit = ⊤

infix 10 _,_

record _,_ (a : Set) (b : Set) : Set where
  constructor _:,_
  field
    fst : a
    snd : b

data Either (e : Set) (a : Set) : Set where
  Left  : e → Either e a
  Right : a → Either e a

either : {e a b : Set} → (e → b) → (a → b) → Either e a → b
either left right (Left  e) = left  e
either left right (Right a) = right a

record NonEmpty (a : Set) : Set where
  constructor _:|_
  field
    nhead : a
    ntail : List a

NEtoList : {a : Set} → NonEmpty a → List a
NEtoList (x :| xs) = x ∷ xs

String : Set
String = List Char

Int : Set
Int = Unit

IP : Set
IP = Unit

DNSMessage : Set
DNSMessage = Unit

DNSError : Set
DNSError = Unit

ServerFailure : DNSError
ServerFailure = tt

RCODE : Set
RCODE = Unit

RR : Set
RR = Unit

Delegation : Set
Delegation = Unit

Domain : Set
Domain = Unit

Address : Set
Address = Unit

[_] : Set → Set
[_] = List

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

fmap : {m : Set → Set} {a b : Set} → (a → b) → m a → m b
fmap = {!!}

bind : {m : Set → Set} {a b : Set} → m a → (a → m b) → m b
bind = {!!}

then : {m : Set → Set} {a b : Set} →  m a → m b → m b
then {m} {a} {b} x y =  x >>= λ _a → y
  where
    _>>=_ = bind {m} {a} {b}

pureM : {m : Set → Set} {a : Set} → a → m a
pureM = {!!}

list : {a b : Set} → b → (a → [ a ] → b) → [ a ] → b
list nil cons  []       = nil
list nil cons (x ∷ xs)  = cons x xs

catchQuery2 : {m : Set → Set} {a e : Set} → m a → (e → m a) → m a
catchQuery2 = {!!}

throwDnsError : {m : Set → Set} {a : Set} → DNSError → m a
throwDnsError = {!!}

randomizedPermN : {m : Set → Set} {a : Set} → NonEmpty a → m (NonEmpty a)
randomizedPermN = {!!}

fillCachedDelegation : {m : Set → Set} → Delegation → m Delegation
fillCachedDelegation = {!!}

resolveNS : {m : Set → Set} → Domain → Bool → Int → Domain → m (Either (RCODE , String) (NonEmpty (IP , RR)))
resolveNS = {!!}

eh : {m : Set → Set} {x : Set} → String → m x
eh s = {!!}

fh : {m : Set → Set} {y : Set} → [ (String , [ Address ]) ] → m y
fh = {!!}

ah : {m : Set → Set} {z : Set} → [ Address ] → m z
ah = {!!}

disableV6NS : Bool
disableV6NS = {!!}

dc : Int
dc = {!!}

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

zone : Domain
zone = {!!}

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

catches : ∀ {m : Set → Set} {a : Set} {e : Set} → m a → [ m a ] → m a
catches {m} {a} {e} x  []       = x
catches {m} {a} {e} x (y ∷ ys)  = x <catchQuery> λ ex → catches {m} {a} {e} y ys
  where
    _<catchQuery>_ = catchQuery2 {m} {a} {e}

resolveNS' : {m : Set → Set} {a : Set} → Domain → Delegation → (Delegation → m a) → (Delegation → NonEmpty IP → m a) → m a
resolveNS' {m} {a} ns d emp ne =
        ((Right <$> (resolveNS {m} zone disableV6NS dc ns)) <catchQuery> λ ex → pure (Left ex))  >>= λ e  →
        fillCachedDelegation {m} d                                                                 >>= λ d' →
        either left (either rleft rright) e d'
  where
    RNS : Set
    RNS = Either (RCODE , String) (NonEmpty (IP , RR))
    infixl 40 _<$>_
    infixl 10 _>>=_ _>>_  -- _>>=₁_
    infixr 10 _=<<_
    _<$>_ = fmap {m} {RNS} {Either DNSError RNS}
    _<catchQuery>_ = catchQuery2 {m} {Either DNSError RNS}
    pure = pureM {m}
    _>>=_ = bind {m}
    -- _>>=₁_ = bind {m}
    _>>_ = then {m}
    _=<<_ : {p q : Set} → (p → m q) → m p → m q
    _=<<_ q p = bind {m} p q

    eh' = eh {m} {Unit}
    --
    left : DNSError → Delegation → m a
    left e d' = eh' ( [] {- show e ++ " for resolving " ++ show ns -}) >> emp d'
    rleft : (RCODE , String) → Delegation → m a
    rleft ( _rc :, ei ) d' = eh' ei >> emp d'
    rright : NonEmpty (IP , RR) → Delegation → m a
    rright axs d' = ne d' =<< randomizedPermN {m} {!!}

Result : Set
Result = (DNSMessage , Delegation)

fallbacks
  :  {m : Set → Set}
  → ([ (String , [ Address ]) ] → [ (String , [ Address ]) ])
  → Delegation
  → (String ,
      (    Delegation
       → (Delegation → m Result)
       → (Delegation → NonEmpty IP → m Result)
       → m Result)
     )
  → [
     (String ,
      (    Delegation
       → (Delegation → m Result)
       → (Delegation → NonEmpty IP → m Result)
       → m Result)
     )
     ]
  → m Result
fallbacks {m} aa d (tag :, runAxs) runsAxs =
    runAxs d emp ne
    -- runAxs d {!!} ne
    -- runAxs d emp {!!}
  where
    infixl 10 _>>_
    _>>_ = then {m} {Unit}
    _<catchQuery>_ = catchQuery2 {m} {Result} {DNSError}
    eh' = eh {m} {Unit}

    emp : Delegation → m Result
    emp d' = list (fh {m} (aa []) >> throwDnsError {m} ServerFailure) (fallbacks {m} (λ xs → aa ((tag :, []) ∷ xs)) d') runsAxs

    ne : Delegation → NonEmpty Address → m Result
    ne d' paxs = list step (λ g gs → step <catchQuery> λ e → hlog e >> fallbacks {m} (λ xs → (tag :, paxs') ∷ xs) d' g gs) runsAxs
      where
        step : m Result
        step = {!!}
        paxs' = NEtoList paxs
        hlog : DNSError → m Unit
        hlog e = eh' ([] {- unwords $ show e : "for" : map show paxs' -})