text:
module Yaffle.REPL

import Core.AutoSearch
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.FC
import Core.Metadata
import Core.Normalise
import Core.Termination
import Core.TT
import Core.Unify
import Core.Value

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Interactive.ExprSearch
import TTImp.Interactive.GenerateDef
import TTImp.Parser
import TTImp.ProcessDecls
import TTImp.TTImp
import TTImp.Unelab

import Parser.Source

%default covering

showInfo : (Name, Int, GlobalDef) -> Core ()
showInfo (n, _, d)
    = coreLift_ $ putStrLn (show n ++ " ==>\n" ++
                   "\t" ++ show (definition d) ++ "\n" ++
                   "\t" ++ show (sizeChange d) ++ "\n")

-- Returns 'True' if the REPL should continue
process : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          ImpREPL -> Core Bool
process (Eval ttimp)
    = do (tm, _) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
         defs <- get Ctxt
         tmnf <- normalise defs [] tm
         coreLift_ (printLn !(unelab [] tmnf))
         pure True
process (Check (IVar _ n))
    = do defs <- get Ctxt
         ns <- lookupTyName n (gamma defs)
         traverse_ printName ns
         pure True
  where
    printName : (Name, Int, ClosedTerm) -> Core ()
    printName (n, _, tyh)
        = do defs <- get Ctxt
             ty <- normaliseHoles defs [] tyh
             coreLift_ $ putStrLn $ show n ++ " : " ++
                                    show !(unelab [] ty)
process (Check ttimp)
    = do (tm, gty) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing
         defs <- get Ctxt
         tyh <- getTerm gty
         ty <- normaliseHoles defs [] tyh
         coreLift_ (printLn !(unelab [] ty))
         pure True
process (ProofSearch n_in)
    = do defs <- get Ctxt
         [(n, i, ty)] <- lookupTyName n_in (gamma defs)
              | [] => undefinedName (justFC defaultFC) n_in
              | ns => throw (AmbiguousName (justFC defaultFC) (map fst ns))
         def <- search (justFC defaultFC) top False 1000 n ty []
         defs <- get Ctxt
         defnf <- normaliseHoles defs [] def
         coreLift_ (printLn !(toFullNames defnf))
         pure True
process (ExprSearch n_in)
    = do defs <- get Ctxt
         [(n, i, ty)] <- lookupTyName n_in (gamma defs)
              | [] => undefinedName (justFC defaultFC) n_in
              | ns => throw (AmbiguousName (justFC defaultFC) (map fst ns))
         results <- exprSearchN (justFC defaultFC) 1 n []
         traverse_ (coreLift . printLn) results
         pure True
process (GenerateDef line name)
    = do defs <- get Ctxt
         Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p)
              | Nothing => do coreLift_ (putStrLn ("Can't find declaration for " ++ show name))
                              pure True
         case !(lookupDefExact n' (gamma defs)) of
              Just None =>
                  catch
                    (do ((fc, cs) :: _) <- logTime "Generation" $
                                makeDefN (\p, n => onLine line p) 1 n'
                           | _ => coreLift_ (putStrLn "Failed")
                        coreLift_ $ putStrLn (show cs))
                    (\err => coreLift_ $ putStrLn $ "Can't find a definition for " ++ show n')
              Just _ => coreLift_ $ putStrLn "Already defined"
              Nothing => coreLift_ $ putStrLn $ "Can't find declaration for " ++ show name
         pure True
process (Missing n_in)
    = do defs <- get Ctxt
         case !(lookupCtxtName n_in (gamma defs)) of
              [] => undefinedName emptyFC n_in
              ts => do traverse_ (\fn =>
                          do tot <- getTotality emptyFC fn
                             case isCovering tot of
                                  MissingCases cs =>
                                     coreLift_ (putStrLn (show fn ++ ":\n" ++
                                                 showSep "\n" (map show cs)))
                                  NonCoveringCall ns =>
                                     coreLift_ (putStrLn
                                         (show fn ++ ": Calls non covering function"
                                           ++ case ns of
                                                   [fn] => " " ++ show fn
                                                   _ => "s: " ++ showSep ", " (map show ns)))
                                  _ => coreLift_ $ putStrLn (show fn ++ ": All cases covered"))
                        (map fst ts)
                       pure True
process (CheckTotal n)
    = do defs <- get Ctxt
         case !(lookupCtxtName n (gamma defs)) of
              [] => undefinedName emptyFC n
              ts => do traverse_ (\fn =>
                          do ignore $ checkTotal emptyFC fn
                             tot <- getTotality emptyFC fn
                             coreLift_ (putStrLn (show fn ++ " is " ++ show tot)))
                               (map fst ts)
                       pure True
process (DebugInfo n)
    = do defs <- get Ctxt
         traverse_ showInfo !(lookupCtxtName n (gamma defs))
         pure True
process Quit
    = do coreLift_ $ putStrLn "Bye for now!"
         pure False

processCatch : {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               ImpREPL -> Core Bool
processCatch cmd
    = catch (process cmd)
            (\err => do coreLift_ (putStrLn (show err))
                        pure True)

export
repl : {auto c : Ref Ctxt Defs} ->
       {auto m : Ref MD Metadata} ->
       {auto u : Ref UST UState} ->
       Core ()
repl
    = do coreLift_ (putStr "Yaffle> ")
         inp <- coreLift getLine
         case runParser (Virtual Interactive) Nothing inp command of
              Left err => do coreLift_ (printLn err)
                             repl
              Right (_, _, cmd) => when !(processCatch cmd) repl


text:
module Sub07Apply108x27

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+9) --F[5,-2]->C[4,-4]--> 3(32x+7)
fc108x27To96x21 :
  (o:Nat) -> P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) 2
    -> P (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))) 2
fc108x27To96x21 o prf =
  let prf2 = lvDown (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) 2
                    prf in
    let prf3 = fc108x27To96x21' o prf2 in lvDown (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))) 3 prf3

export
apply108x27 : P (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                               (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))),
         P m 2))
apply108x27 {o} col = let col2 = fc108x27To96x21 o col in ((S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                            (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))) ** (lte108x27 o, col2)) where
  lte108x27 : (o:Nat) -> LTE (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                              (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                        (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                              (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))
          (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))
  lte108x27 Z = (lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x27 (S o) = let lemma = lte108x27 o in
    rewrite (sym (plusSuccRightSucc o o)) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (plus (plus o o) o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (plus (plus (plus o o) o) (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))) in

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

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (S (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) (plus o o))
                                                                                (plus (plus o o) (plus o o)))
                                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                    (plus (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o o)))
                                                                                (plus (plus (plus o o)
                                                                                (plus o o))
                                                                                (plus (plus o o)
                                                                                (plus o
                                                                                o)))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma

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

ext: idr


text:
module Test.API2

import Common

userAPI : API String (String, String, String)


text:
module Test

import API


text:
module Control.Monad.Freer

import Control.Monad.Free
import Control.Monad.Syntax
import Data.CoList

%default total
%access public export

-- ported from https://github.com/robrix/freer-cofreer

data Freer : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Freer f a
  Bind : f x -> (x -> Freer f a) -> Freer f a

Functor (Freer f) where
  map f (Pure result)     = Pure (f result)
  map f (Bind step yield) = Bind step (\x => map f $ yield x)

Applicative (Freer f) where
  pure = Pure

  (Pure f)            <*> param = map f param
  (Bind action yield) <*> param = Bind action (\x => (yield x) <*> param)

Monad (Freer f) where
  (Pure a)   >>= f = f a
  (Bind r f) >>= g = Bind r (f >=> g)

liftF : f a -> Freer f a
liftF action = action `Bind` Pure

hoistFreer : {f, g : Type -> Type} -> (fg : {a : Type} -> f a -> g a) -> Freer f b -> Freer g b
hoistFreer _  (Pure result)     = Pure result
hoistFreer fg (Bind step yield) = Bind (fg step) (\x => hoistFreer fg $ yield x)

||| Tear down a `Freer` `Monad` using iteration with an explicit continuation.
|||
||| This is analogous to `iter` with a continuation for the interior values, and
||| is therefore suitable for defining interpreters for GADTs/types lacking a
||| `Functor` instance.
iterFreer : (algebra : {x : Type} -> (x -> a) -> f x -> a) -> Freer f a -> a
iterFreer _       (Pure result)          = result
iterFreer algebra (Bind action continue) = algebra (\x => iterFreer algebra $ continue x) action

||| Tear down a `Freer` `Monad` using iteration.
|||
||| This is analogous to `cata` where the `Pure`ed values are placeholders for
||| the result of the computation.
iter : Functor f => (algebra : f a -> a) -> Freer f a -> a
iter algebra = iterFreer (\yield => algebra . map yield)

||| Tear down a `Freer` `Monad` using iteration with an explicit continuation in some `Applicative` context.
|||
||| This is analogous to `iterA` with a continuation for the interior values, and
||| is therefore suitable for defining interpreters for GADTs/types lacking a
||| `Functor` instance.
iterFreerA : Applicative m => (algebra : {x : Type} -> (x -> m a) -> f x -> m a) -> Freer f a -> m a
iterFreerA algebra r = iterFreer algebra (map pure r)

||| Tear down a `Freer` `Monad` using iteration in some `Applicative` context.
|||
||| This is analogous to `cata` where the `Pure` values are placeholders for
||| the result of the computation.
iterA : (Functor f, Applicative m) => (algebra : f (m a) -> m a) -> Freer f a -> m a
iterA algebra = iterFreerA (\yield => algebra . map yield)

||| Run a program to completion by repeated refinement, and return its result.
-- TODO can it be made total? use `Fuel`?
partial
runFreer : (refine : {x : Type} -> f x -> Freer f x) -> Freer f result -> result
runFreer refine = iterFreer (\xa, fx => xa $ runFreer refine $ refine fx)

||| Run a program to completion by repeated refinement in some `Monad`ic
||| context, and return its result.
-- TODO can it be made total? use `Fuel`?
partial
runFreerM : Monad m => (refine : {x : Type} -> f x -> Freer f (m x)) -> Freer f result -> m result
runFreerM {m} refine r = go (map pure r)
  where
  partial
  go : Freer f (m x) -> m x
  go = iterFreer ((. (go . refine)) . (=<<))

||| Run a single step of a program by refinement, returning `Either` its result
||| or the next step.
stepFreer : (refine : {x : Type} -> f x -> Freer f x) -> Freer f result -> Either result (Freer f result)
stepFreer _      (Pure a)          = Left a
stepFreer refine (Bind step yield) = Right (refine step >>= yield)

||| Run a program to completion by repeated refinement, returning the list of
||| steps up to and including the final result.
|||
||| The steps are unfolded lazily, making this total and suitable for stepwise
||| evaluation of nonterminating programs.
freerSteps : (refine : {x : Type} -> f x -> Freer f x) -> Freer f result -> CoList (Freer f result)
freerSteps refine r = case stepFreer refine r of
  Left  a    => [Pure a]
  Right step => step :: (freerSteps refine step)

retract : Monad m => Freer m a -> m a
retract = iterFreerA (=<<)

foldFreer : Monad m => ({x : Type} -> f x -> m x) -> Freer f a -> m a
foldFreer f = retract . hoistFreer f

cutoff : Nat -> Freer f a -> Freer f (Either (Freer f a) a)
cutoff  Z     r                = pure (Left r)
cutoff (S n) (Bind step yield) = Bind step (cutoff n . yield)
cutoff  _     r                = Right <$> r

MonadFree (Freer f) f where
  wrap action = action `Bind` id

Foldable f => Foldable (Freer f) where
  foldr ff c (Pure a)   = ff a c
  foldr ff c (Bind r t) = foldr (\x,c1 => foldr ff c1 (t x)) c r

Traversable f => Traversable (Freer f) where
  traverse f (Pure a)   = pure <$> f a
  traverse f (Bind r t) = wrap <$> traverse (\a => traverse f (t a)) r

max_stars_repo_name: clayrat/idris-free

max_issues_repo_name: clayrat/idris-free

max_forks_repo_name: clayrat/idris-free


text:
module Data.Double.FloatUtils.Chez

import Data.DPair
import Data.Fin
import Libraries.Utils.Scheme

%default total

rebool1 : (a -> Int) -> (a -> Bool)
rebool1 f = \x => (f x) == 1

rebool2 : (a -> a -> Int) -> (a -> a -> Bool)
rebool2 f = \x,y => (f x y) == 1

rebool3 : (a -> a -> a -> Int) -> (a -> a -> a -> Bool)
rebool3 f = \x,y,z => (f x y z) == 1

rebool4 : (a -> a -> a -> a -> Int) -> (a -> a -> a -> a -> Bool)
rebool4 f = \w,x,y,z => (f w x y z) == 1

namespace Vector
  data ForeignVector : Nat -> Type -> Type where
    [external]

  public export
  0 Vector : Nat -> Type -> Type
  Vector n ty = Ptr $ ForeignVector n ty

  %foreign "scheme,chez:idris-vector-ref"
  prim__vectorRef : Vector n ty -> Fin n -> ty

  export
  vectorRef : (i : Fin n) -> (v : Vector n ty) -> ty
  vectorRef i v = prim__vectorRef v i

namespace Misc
  export
  %foreign "scheme,chez:fllp"
  fllp : Double -> Int

  %foreign "scheme,chez:idris-+nan.0"
  prim__positiveNaN : Double

  %foreign "scheme,chez:idris-+inf.0"
  prim__positiveInf : Double

  %foreign "scheme,chez:idris--inf.0"
  prim__negativeInf : Double

  %foreign "scheme,chez:idris-isnan"
  prim__isNan : Double -> Int

  %foreign "scheme,chez:idris-notnan"
  prim__notNan : Double -> Int

  export
  nan : Double
  nan = prim__positiveNaN

  export
  isNan : Double -> Bool
  isNan = rebool1 prim__isNan

  export
  notNan : Double -> Bool
  notNan = rebool1 prim__notNan

  export
  0 invertIsNan : forall x. not (isNan x) = True -> notNan x = True
  invertIsNan = believe_me

  export
  0 invertNotNan : forall x. not (notNan x) = True -> isNan x = True
  invertNotNan = believe_me

  export
  inf : Double
  inf = prim__positiveInf

  -- Kind of redundant, because we have Neg Double, so we can write `- inf`
  export
  negInf : Double
  negInf = prim__negativeInf

  %foreign "scheme,chez:idris-flnonpositive"
  prim__isNonPositive : Double -> Int

  export
  isNonPositive : Double -> Bool
  isNonPositive = rebool1 prim__isNonPositive

  %foreign "scheme,chez:idris-flnonnegative"
  prim__isNonNegative : Double -> Int

  export
  isNonNegative : Double -> Bool
  isNonNegative = rebool1 prim__isNonNegative

  public export
  record DoubleInfo where
    constructor MkDoubleInfo
    mantissa : Int
    exponent : Int
    sign : Int

  %foreign "scheme,chez:decode-float"
  prim__decodeDouble : Double -> Vector 3 Int

  decodeDouble : (x : Double) -> DoubleInfo
  decodeDouble x =
    let result = prim__decodeDouble x in
      MkDoubleInfo
        (vectorRef 0 result)
        (vectorRef 1 result)
        (vectorRef 2 result)

namespace Comparison
  %foreign "scheme,chez:idris-compare"
  prim__compare : Double -> Double -> Int

  %foreign "scheme,chez:idris-fl=-2"
  prim__doubleEq2 : Double -> Double -> Int
  %foreign "scheme,chez:idris-fl=-3"
  prim__doubleEq3 : Double -> Double -> Double -> Int
  %foreign "scheme,chez:idris-fl=-4"
  prim__doubleEq4 : Double -> Double -> Double -> Double -> Int

  export
  doubleEq2 : Double -> Double -> Bool
  doubleEq2 = rebool2 prim__doubleEq2
  export
  doubleEq3 : Double -> Double -> Double -> Bool
  doubleEq3 = rebool3 prim__doubleEq3
  export
  doubleEq4 : Double -> Double -> Double -> Double -> Bool
  doubleEq4 = rebool4 prim__doubleEq4

  %foreign "scheme,chez:idris-fl>-2"
  prim__doubleGt2 : Double -> Double -> Int
  %foreign "scheme,chez:idris-fl>-3"
  prim__doubleGt3 : Double -> Double -> Double -> Int
  %foreign "scheme,chez:idris-fl>-4"
  prim__doubleGt4 : Double -> Double -> Double -> Double -> Int

  export
  doubleGt2 : Double -> Double -> Bool
  doubleGt2 = rebool2 prim__doubleGt2
  export
  doubleGt3 : Double -> Double -> Double -> Bool
  doubleGt3 = rebool3 prim__doubleGt3
  export
  doubleGt4 : Double -> Double -> Double -> Double -> Bool
  doubleGt4 = rebool4 prim__doubleGt4

  %foreign "scheme,chez:idris-fl>=-2"
  prim__doubleGte2 : Double -> Double -> Int
  %foreign "scheme,chez:idris-fl>=-3"
  prim__doubleGte3 : Double -> Double -> Double -> Int
  %foreign "scheme,chez:idris-fl>=-4"
  prim__doubleGte4 : Double -> Double -> Double -> Double -> Int

  export
  doubleGte2 : Double -> Double -> Bool
  doubleGte2 = rebool2 prim__doubleGte2
  export
  doubleGte3 : Double -> Double -> Double -> Bool
  doubleGte3 = rebool3 prim__doubleGte3
  export
  doubleGte4 : Double -> Double -> Double -> Double -> Bool
  doubleGte4 = rebool4 prim__doubleGte4

  %foreign "scheme,chez:idris-fl<-2"
  prim__doubleLt2 : Double -> Double -> Int
  %foreign "scheme,chez:idris-fl<-3"
  prim__doubleLt3 : Double -> Double -> Double -> Int
  %foreign "scheme,chez:idris-fl<-4"
  prim__doubleLt4 : Double -> Double -> Double -> Double -> Int

  export
  doubleLt2 : Double -> Double -> Bool
  doubleLt2 = rebool2 prim__doubleLt2
  export
  doubleLt3 : Double -> Double -> Double -> Bool
  doubleLt3 = rebool3 prim__doubleLt3
  export
  doubleLt4 : Double -> Double -> Double -> Double -> Bool
  doubleLt4 = rebool4 prim__doubleLt4

  %foreign "scheme,chez:idris-fl<=-2"
  prim__doubleLte2 : Double -> Double -> Int
  %foreign "scheme,chez:idris-fl<=-3"
  prim__doubleLte3 : Double -> Double -> Double -> Int
  %foreign "scheme,chez:idris-fl<=-4"
  prim__doubleLte4 : Double -> Double -> Double -> Double -> Int

  export
  doubleLte2 : Double -> Double -> Bool
  doubleLte2 = rebool2 prim__doubleLte2
  export
  doubleLte3 : Double -> Double -> Double -> Bool
  doubleLte3 = rebool3 prim__doubleLte3
  export
  doubleLte4 : Double -> Double -> Double -> Double -> Bool
  doubleLte4 = rebool4 prim__doubleLte4

  export
  %foreign "scheme,chez:max"
  doubleMax2 : Double -> Double -> Double
  export
  %foreign "scheme,chez:max"
  doubleMax3 : Double -> Double -> Double -> Double
  export
  %foreign "scheme,chez:max"
  doubleMax4 : Double -> Double -> Double -> Double -> Double

  export
  %foreign "scheme,chez:min"
  doubleMin2 : Double -> Double -> Double
  export
  %foreign "scheme,chez:min"
  doubleMin3 : Double -> Double -> Double -> Double
  export
  %foreign "scheme,chez:min"
  doubleMin4 : Double -> Double -> Double -> Double -> Double

  public export
  implementation [chezFloat] Ord Double where
    compare x y =
      if x < y
      then LT
      else
        if x > y
        then GT
        else EQ
    (<) = doubleLt2
    (>) = doubleGt2
    (<=) = doubleLte2
    (>=) = doubleGte2
    max = doubleMax2
    min = doubleMin2

  namespace NanSafe
    0 DoubleNotNan : Type
    DoubleNotNan = Subset Double (\x => notNan x = True)

    -- implementation Functor DoubleNotNan where
    --   map f (Element x px) = ?help

    unwrap : DoubleNotNan -> Double
    unwrap (Element x _) = x

    wrap1 : (Double -> a) -> (DoubleNotNan -> a)
    wrap1 f = \ (Element x _) => f x

    wrap2 : (Double -> Double -> a) -> (DoubleNotNan -> DoubleNotNan -> a)
    wrap2 f = \ (Element x _), (Element y _) => f x y

    export
    doubleCompareSafe : DoubleNotNan -> DoubleNotNan -> Ordering
    doubleCompareSafe (Element x _) (Element y _) =
      assert_total $ case prim__compare x y of
        1 => GT
        -1 => LT
        0 => EQ

    export
    doubleLt2Safe : DoubleNotNan -> DoubleNotNan -> Bool
    doubleLt2Safe = wrap2 doubleLt2

    export
    doubleGt2Safe : DoubleNotNan -> DoubleNotNan -> Bool
    doubleGt2Safe = wrap2 doubleGt2

    export
    doubleLte2Safe : DoubleNotNan -> DoubleNotNan -> Bool
    doubleLte2Safe = wrap2 doubleLte2

    export
    doubleGte2Safe : DoubleNotNan -> DoubleNotNan -> Bool
    doubleGte2Safe = wrap2 doubleGte2

    export
    doubleMax2Safe : DoubleNotNan -> DoubleNotNan -> DoubleNotNan
    doubleMax2Safe = believe_me $ wrap2 doubleMax2

    export
    doubleMin2Safe : DoubleNotNan -> DoubleNotNan -> DoubleNotNan
    doubleMin2Safe = believe_me $ wrap2 doubleMin2

    public export
    implementation [chezFloatNanSafe] Ord DoubleNotNan where
      compare = doubleCompareSafe
      (<) = wrap2 doubleLt2
      (>) = wrap2 doubleGt2
      (<=) = wrap2 doubleLte2
      (>=) = wrap2 doubleGte2
      max = believe_me $ wrap2 doubleMax2
      min = believe_me $ wrap2 doubleMin2

  namespace List
    %foreign "scheme,chez:idris-fl=-apply"
    prim__doubleEq : List Double -> Int
    %foreign "scheme,chez:idris-fl>-apply"
    prim__doubleGt : List Double -> Int
    %foreign "scheme,chez:idris-fl>=-apply"
    prim__doubleGte : List Double -> Int
    %foreign "scheme,chez:idris-fl<-apply"
    prim__doubleLt : List Double -> Int
    %foreign "scheme,chez:idris-fl<=-apply"
    prim__doubleLte : List Double -> Int

    export
    doubleEq : List Double -> Bool
    doubleEq xs = (prim__doubleEq xs) == 1
    export
    doubleGt : List Double -> Bool
    doubleGt xs = (prim__doubleGt xs) == 1
    export
    doubleGte : List Double -> Bool
    doubleGte xs = (prim__doubleGte xs) == 1
    export
    doubleLt : List Double -> Bool
    doubleLt xs = (prim__doubleLt xs) == 1
    export
    doubleLte : List Double -> Bool
    doubleLte xs = (prim__doubleLte xs) == 1

    export
    %foreign "scheme,chez:idris-max-apply"
    doubleMax : List Double -> Double
    export
    %foreign "scheme,chez:idris-min-apply"
    doubleMin : List Double -> Double

implementation Show Ordering where
  show LT = "LT"
  show EQ = "EQ"
  show GT = "GT"

implementation Interpolation Int where
  interpolate = show

implementation Interpolation Ordering where
  interpolate = show

-- %foreign "scheme:idris-bad"
-- bad : () -> Nat

test : IO ()
test = do
  -- printLn $ bad ()
  printLn $ isNonNegative 3.6
  printLn $ doubleEq [1.5, 1.5]
  printLn $ doubleMax [1.5, 1.5, 2.5]
  printLn $ 1.5 == 1.5
  let out = decodeDouble 4.5
  printLn "m=\{out.mantissa} e=\{out.exponent} s\{out.sign}"


text:
-- ----------------------------------------------------------------- [ Eff.idr ]
-- Module      : XML.Reader.Eff
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module XML.Serialise.Eff

import Lightyear
import Lightyear.Strings
import Lightyear.StringFile

import Effects
import Effect.File
import Effect.Exception

import XML.DOM
import XML.Parser
import XML.Serialise

%access private

export
readXMLDoc : String
           -> Eff (Either XMLError (Document DOCUMENT))
                  [FILE ()]
readXMLDoc f = parseFile CannotReadFile FileParseError parseXMLDoc f

export
readXMLSnippet : String
              -> Eff (Either XMLError (Document ELEMENT))
                     [FILE ()]
readXMLSnippet f = parseFile CannotReadFile FileParseError parseXMLSnippet f

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
import NewEden.Natural
import Prelude

-- we can also formally prove things about abstract numbers (even large ones)
-- compare it with the standard Nat in the following:

x : Natural p
x = 1487129834719898712935812394810

x' : Nat
x' = 1487129834719898712935812394810

y : Natural p
y = 1234

y' : Nat
y' = 1234

z : Natural p
z = x * y

z' : Nat
z' = x' * y'

-- now let's prove that z is actually x * y...

prf : NewEden.Natural.(*) x y = z
prf = Refl

-- Aaand uncomment these lines if you want the compiler to explode!
-- It can't prove the following because the hacks to replace Nat
-- with efficient stuff aren't available at compile time.
-- But this is no problem for Natural p, since Natural p expresses
-- numbers in terms of a logarithmic number of axiomatic expessions!

-- prf' : (*) x' y' = z'
-- prf' = Refl

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module PositiveBug

data MyEmptyList : Type
data EmptyListLTE : Nat -> MyEmptyList -> Type

-- mutual
data MyEmptyList : Type where
    MyNil : MyEmptyList

data EmptyListLTE : Nat -> MyEmptyList -> Type where
    NilLTE : (x : Nat) -> EmptyListLTE x MyNil


text:
module PnP

-- Progress and Preservation

import Step
import Subst
import SubstLemmas
import Term
import Typing

%default total
%access export

------------------
-- Begin: PROGRESS

-- Progress: a closed, well-typed term is either a value
--           or it can take a step in the reduction relation.

progress : (e : Term) ->
           Typing [] e t ->
           Either (Value e) (e' : Term ** (Step e e'))
--
progress (TVar Z)     (TyVar Refl) impossible
progress (TVar (S _)) (TyVar Refl) impossible
--
progress (TAbs e) (TyAbs s ty) = Left VAbs
--
progress (TApp e1 e2) (TyApp ty1 ty2) =
  case progress e1 ty1 of
    (Left v1) => case canonicalFun _ ty1 v1 of
                      (e1 ** Refl) => case progress e2 ty2 of
                                           (Left v2) => let st' = StBeta v2
                                                        in Right (_ ** st')
                                           (Right (_ ** st2)) => let st' = StApp2 v1 st2
                                                                 in Right (_ ** st')
    (Right (_ ** st1)) => let st' = StApp1 st1
                          in Right (_ ** st')
--
progress (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) =
  case progress e1 ty1 of
    (Left v1) => case canonicalNat _ ty1 v1 of
                      (Left Refl) => let st' = StRecZero
                                     in Right (_ ** st')
                      (Right (e' ** (v', Refl))) => let st' = StRecSucc v1
                                                    in Right (_ ** st')
    (Right (_ ** st1)) => let st' = StRec st1
                          in Right (_ ** st')
--
progress TZero TyZero = Left VZero
--
progress (TSucc e) (TySucc ty) =
  case progress e ty of
       (Left v) => Left $ VSucc v
       (Right (_ ** st)) => let st' = StSucc st
                            in Right (_ ** st')
--
progress (TPred e) (TyPred ty) =
  case progress e ty of
    (Left v) => case canonicalNat _ ty v of
                     (Left Refl) => let st' = StPredZero
                                    in Right (TZero ** st')
                     (Right (_ ** (v', Refl))) => let st' = StPredSucc v'
                                                  in Right (_ ** st')
    (Right (_ ** st)) => let st' = StPred st
                         in Right (_ ** st')
--
progress (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) =
  case progress e1 ty1 of
    (Left v1) => case canonicalNat _ ty1 v1 of
                      (Left Refl) => Right (_ ** StIfzZero)
                      (Right (_ ** (v1', Refl))) => Right (_ ** StIfzSucc v1')
    (Right (_ ** st)) => let st' = StIfz st
                         in Right (_ ** st')

-- End: PROGRESS
----------------

-------------------------------------------------
-- Begin: WELL-TYPED IRREDUCIBLE TERMS ARE VALUES

irreducibleValue : (e : Term) ->
                   Typing [] e t ->
                   ((e' : Term) -> Step e e' -> Void) ->
                   Value e
irreducibleValue e ty nostep =
  case progress e ty of
       (Left v) => v
       (Right (_ ** st)) => absurd $ nostep _ st

-- End: WELL-TYPED IRREDUCIBLE TERMS ARE VALUES
-----------------------------------------------

----------------------
-- Begin: PRESERVATION

-- Preservation: after reducing a term of type 't' by one
--               step, the resulting term is again of type 't'.

preservation : (e : Term) ->
               Typing ctx e t ->
               Step e e' ->
               Typing ctx e' t
--
preservation (TVar i) (TyVar prf) st impossible
--
preservation (TAbs e) (TyAbs s ty) st impossible
--
preservation (TApp e1 e2) (TyApp ty1 ty2) (StApp1 st1) =
  let ty1' = preservation e1 ty1 st1
  in TyApp ty1' ty2
preservation (TApp e1 e2) (TyApp ty1 ty2) (StApp2 v1 st2) =
  let ty2' = preservation e2 ty2 st2
  in TyApp ty1 ty2'
preservation (TApp (TAbs e) e2) (TyApp ty1 ty2) (StBeta v2) =
  case ty1 of
       (TyAbs s ty1') => substPreservesTy {ctx1=[]} e ty1' e2 ty2
--
preservation (TRec e1 e2 e3) (TyRec ty1 ty2 ty3) (StRec st1) =
  let ty1' = preservation e1 ty1 st1
  in TyRec ty1' ty2 ty3
preservation (TRec TZero e2 e3) (TyRec ty1 ty2 ty3) StRecZero = ty2
preservation (TRec (TSucc n) e2 e3) (TyRec ty1 ty2 ty3) (StRecSucc v) =
  case ty1 of
       (TySucc tyn) => let tyrn = TyRec tyn ty2 ty3
                           tya  = TyApp ty3 tyn
                       in TyApp tya tyrn
--
preservation TZero TyZero st impossible
--
preservation (TSucc e) (TySucc ty) (StSucc st) =
  let ty' = preservation e ty st
  in TySucc ty'
--
preservation (TPred e) (TyPred ty) (StPred st) =
  let ty' = preservation e ty st
  in TyPred ty'
preservation (TPred TZero) (TyPred ty) StPredZero = TyZero
preservation (TPred (TSucc e')) (TyPred ty) (StPredSucc v') =
  case ty of
       (TySucc ty') => ty'
--
preservation (TIfz e1 e2 e3) (TyIfz ty1 ty2 ty3) (StIfz st1) =
  let ty1' = preservation e1 ty1 st1
  in TyIfz ty1' ty2 ty3
preservation (TIfz TZero e2 e3) (TyIfz ty1 ty2 ty3) StIfzZero = ty2
preservation (TIfz (TSucc n) e2 e3) (TyIfz ty1 ty2 ty3) (StIfzSucc v) = ty3

transPreservation : (e : Term) ->
                    Typing ctx e t ->
                    TransStep e e' ->
                    Typing ctx e' t
transPreservation e ty (TStRefl e)       = ty
transPreservation e ty (TStTrans st tst) =
  let ty' = preservation e ty st
  in transPreservation _ ty' tst

-- End: PRESERVATION
--------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Control.Monad.Ref

import public Control.Monad.Identity
import public Control.Monad.Trans
import public Data.IORef
import public Experiment.UniverseRecord

%default total
%access public export

%hide Language.Reflection.Ref
%hide Language.Reflection.Universe

-- Interface -------------------------------------------------------------------

interface Monad m => MonadRef (u : Universe) (l : Ty u -> Type) (m : Type -> Type) | m where
  ref    : (typeOf u a) -> m (l a)
  deref  : l a -> m (typeOf u a)
  assign : l a -> (typeOf u a) -> m ()

infix 4 :=
(:=) : MonadRef u l m => l a -> (typeOf u a) -> m ()
(:=) = assign

-- Instances -------------------------------------------------------------------

-- MonadRef u IORef IO where
--   ref    = newIORef
--   deref  = readIORef
--   assign = writeIORef

-- Helpers ---------------------------------------------------------------------

modify : MonadRef u l m => l a -> (typeOf u a -> typeOf u a) -> m ()
modify l f = do
  x <- deref l
  l := f x

{- Tests -----------------------------------------------------------------------

test0 : IO Int
test0 = do
  r <- newIORef 5
  writeIORef r 10
  x <- readIORef r
  pure x

test : MonadRef IORef IO => IO Int
test = do
  r <- ref (the Int 5)
  r := (the Int 10)
  x <- deref r
  pure x

-------------------------------------------------------------------------------}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
%default total

zeroImpossible : (k : Nat) -> k === Z -> Void
zeroImpossible (S k) eq impossible


text:
data Natural = Zero | S Natural

eval : Natural -> Int
eval Zero = 0
eval (S n) = succ (eval n)

fromInt : Int -> Natural
fromInt n = case n <= 0 of
  True      => Zero
  otherwise => S (fromInt (pred n))


text:
> module Real.Properties

> import Real.Postulates

> %default total
> %access public export

* Implementations:

> ||| Real is an implementation of Num
> implementation [NumReal] Num Real where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

> using implementation NumReal
>   ||| Real is an implementation of Neg
>   implementation [NegReal] Neg Real where
>     negate x = zero `minus` x
>     (-) = minus

> using implementation NumReal
>   ||| Real is an implementation of Fractional
>   implementation [FractionalReal] Fractional Real where
>     (/) = div

> using implementation NegReal
>   |||
>   minusLemma : {x : Real} -> x - x = 0

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import ListLast

describe_help : (Show a) => (input : List a) -> (form : ListLast input) -> String
describe_help [] Empty = "Empty"
describe_help (xs ++ [x]) (NonEmpty xs x)
  = "Non-empty, initial portion = " ++ show xs

describe_list_end : Show a => List a -> String
describe_list_end xs = describe_help xs (listLast xs)

describe_list_end' : Show a => List a -> String
describe_list_end' xs with (listLast xs)
  describe_list_end' [] | Empty = "Empty"
  describe_list_end' (xs' ++ [x]) | (NonEmpty xs' x)
    = "Non-empty, initial portion = " ++ show xs'

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
everyOther : Stream a -> Stream a
everyOther (val1 :: val2 :: xs) = val2 :: everyOther xs

squareRootApprox : (number : Double) -> (approx : Double) -> Stream Double
squareRootApprox number approx =
    let next = (approx + (number / approx)) / 2 in
        next :: squareRootApprox number next

squareRootBound : (max : Nat) -> (number : Double) -> (bound : Double)->
    (approxs : Stream Double) -> Double
squareRootBound Z number bound (value :: xs) = value
squareRootBound (S k) number bound (value :: xs) =
    if value * value - number < bound
        then value
        else squareRootBound k number bound xs

squareRoot : (num : Double) -> Double
squareRoot num = squareRootBound 100 num 0.00000000001 (squareRootApprox num num)


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3

main : IO ()
main = do

  firstItem <- d3 ?? selectAll "ul" >=>
                 select "li"

  firstItem ??
    style "color" "red" >=>
    style "font-style" "italic"

  return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Search.Negation

import Data.List.Quantifiers
import Data.Nat

%default total

||| It is much easier to look for positive evidence than it is to look
||| for negative evidence. So instead of looking for `Not q`, we may
||| want to look for `p` instead
public export
interface Negates p q | q where
  toNegation : p -> Not q

public export
({0 x : a} -> Negates (p x) (q x)) => Negates (All p xs) (Any q xs) where
  toNegation all = allNegAny (mapProperty toNegation all)

public export
({0 x : a} -> Negates (p x) (q x)) => Negates (Any p xs) (All q xs) where
  toNegation any = anyNegAll (mapProperty toNegation any)

public export
Negates (m `LT` n) (m `GTE` n) where
  toNegation = LTImpliesNotGTE

public export
Negates (m `LTE` n) (m `GT` n) where
  toNegation = LTEImpliesNotGT


text:
module Extra.Debug

export
log : Show a => String -> a -> a
log msg x =
	let
		_ = unsafePerformIO (putStrLn $ msg ++ ": " ++ show x)
	in
		x

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module VerifiedInvertible

%default total
%hide Prelude.Algebra.(<*>)
%hide Prelude.Applicative.(<|>)

-- http://www.informatik.uni-marburg.de/~rendel/unparse/

-- core definitions

data T = tt

data PartIso : Type -> Type -> Type where
  MkPartIso : (to : a -> Maybe b) ->
              (from : b -> Maybe a) ->
              (toFrom : (y : b) -> maybe T (\x => x = y) (from y >>= to)) ->
              (fromTo : (x : a) -> maybe T (\y => y = x) (to x >>= from)) ->
              PartIso a b

class PartIsoFunctor (f : Type -> Type -> Type) where
  (<$>) : PartIso a b -> (f a c -> f b c)

class PFunctor (f : Type -> Type -> Type) where
  (<*>) : f a c -> Lazy (f b c) -> f (a, b) c

class PAlternative (f : Type -> Type -> Type) where
  (<|>) : f a c -> Lazy (f a c) -> f a c
  empty : f a c

class (PartIsoFunctor d, PFunctor d, PAlternative d) => Syntax (d : Type -> Type -> Type) c where
  pure : Eq a => a -> d a c
  item : d c c

-- helper functions

ipc_inverse : PartIso a b -> PartIso b a
ipc_inverse (MkPartIso f g tf ft) = MkPartIso g f ft tf

ipc_apply : PartIso a b -> a -> Maybe b
ipc_apply (MkPartIso f g ft ft) = f

ipc_unapply : PartIso a b -> b -> Maybe a
ipc_unapply = ipc_apply . ipc_inverse

-- Inspect and other stuff

data Inspect : a -> Type where
  wi : {A : Type} -> (x : A) -> (y : A) -> (eq: x = y) -> Inspect x

inspect : {A : Type} -> (x : A) -> Inspect x
inspect x = wi x _ refl

match : {A : Type} -> {x : A} -> (y : A) -> {eq : x = y} -> Inspect x
match y {eq} = wi _ y eq

maybe_assoc : (x : Maybe a) -> (f : a -> Maybe b) -> (g : b -> Maybe c) -> (x >>= (\y => f y >>= g)) = (x >>= f >>= g)
maybe_assoc Nothing f g = refl
maybe_assoc (Just x) f g = refl

maybe_unbind : (f : a -> Maybe b) -> (g : b -> Maybe c) -> (x : a) -> {y : b} ->
  (f x = Just y) -> g y = Just x >>= f >>= g
maybe_unbind f g x eq = rewrite eq in refl

-- Algebra

infixr 1 >=>
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x => f x >>= g

pId : PartIso a a
pId = MkPartIso (\x => Just x) (\x => Just x) (\x => refl) (\x => refl)

(.) : PartIso b c -> PartIso a b -> PartIso a c
(MkPartIso gTo gFrom gTF gFT) . (MkPartIso fTo fFrom fTF fFT) =
  MkPartIso
    (ipc_apply (MkPartIso fTo fFrom fTF fFT) >=> ipc_apply (MkPartIso gTo gFrom gTF gFT))
    (ipc_unapply (MkPartIso gTo gFrom gTF gFT) >=> ipc_unapply (MkPartIso fTo fFrom fTF fFT))
    tf ft
  where
    -- these two are identical, would be nice to generalize
    tf y with (inspect $ gFrom y)
      | match Nothing {eq=eq} = rewrite eq in tt
      | match (Just tfy) {eq=eq} = rewrite eq in
        rewrite (maybe_assoc ((Just tfy) >>= fFrom) fTo gTo) in
          case (inspect $ fFrom tfy >>= fTo) of
            match Nothing {eq=eq2} => rewrite eq2 in tt
            match (Just tfy') {eq=eq2} => rewrite eq2 in
              rewrite (replace eq2 {P=(\y => maybe T (\x => x = tfy) y)} (fTF tfy)) in
                rewrite (maybe_unbind gFrom gTo y eq) in (gTF y)
    ft y with (inspect $ fTo y)
      | match Nothing {eq=eq} = rewrite eq in tt
      | match (Just gty) {eq=eq} = rewrite eq in
        rewrite (maybe_assoc ((Just gty) >>= gTo) gFrom fFrom) in
          case (inspect $ gTo gty >>= gFrom) of
            match Nothing {eq=eq2} => rewrite eq2 in tt
            match (Just gty') {eq=eq2} => rewrite eq2 in
              rewrite (replace eq2 {P=(\y => maybe T (\x => x = gty) y)} (gFT gty)) in
                rewrite (maybe_unbind fTo fFrom y eq) in (fFT y)

-- pTup : PartIso a b -> PartIso c d -> PartIso (a, c) (b, d)
-- pTup i j = MkPartIso f g where
--   f (a, b) = case (ipc_apply i a) of
--     Nothing => Nothing
--     Just x => case (ipc_apply j b) of
--       Nothing => Nothing
--       Just y => Just (x, y)
--   g (c, d) = case (ipc_unapply i c) of
--     Nothing => Nothing
--     Just x => case (ipc_unapply j d) of
--       Nothing => Nothing
--       Just y => Just (x, y)

-- associate : PartIso (a, (b, c)) ((a, b), c)
-- associate = MkPartIso f g where
--   f (a, (b, c)) = Just ((a, b), c)
--   g ((a, b), c) = Just (a, (b, c))

commute : PartIso (a, b) (b, a)
commute = MkPartIso f f (\(a,b) => refl) (\(a,b) => refl) where
  f : (c, d) -> Maybe (d, c)
  f (a, b) = Just (b, a)

unit : {a : Type} -> PartIso a (a, ())
unit = MkPartIso f g tf ft where
  f : {a : Type} -> a -> Maybe (a, ())
  f a = Just (a, ())
  g : {a : Type} -> (a, ()) -> Maybe a
  g (a, ()) = Just a
  tf (a, ()) = refl
  ft a = refl

-- *>, <*

infixl 3 *>
(*>) : Syntax d c => d () c -> d a c -> d a c
p *> q = ipc_inverse unit . commute <$> p <*> q

infixl 3 <*
(<*) : Syntax d c => d a c -> d () c -> d a c
p <* q = ipc_inverse unit <$> p <*> q

-- this function can't be verified: there's no isomorphism when we are
-- ignoring input; neither can it be changed, because it's quite
-- important to be able to ignore input
ignore : a -> PartIso a ()
ignore x = MkPartIso f g tf ft where
  f : a -> Maybe ()
  f y = Just ()
  g : () -> Maybe a
  g () = Just x
  tf () = refl
  ft y = believe_me (x = y)

-- Parser

data Parser a c = MkParser (List c -> Maybe (a, List c))

parse : Parser a c -> List c -> Maybe a
parse (MkParser p) s = p s >>= pure . fst

instance PartIsoFunctor Parser where
  iso <$> (MkParser p) = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      y <- ipc_apply iso x
      return (y, rest)

instance PFunctor Parser where
  (MkParser p) <*> mkpq = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      case mkpq of
        (MkParser q) => do
          (y, ret) <- q rest
          return ((x, y), ret)

instance PAlternative Parser where
  (MkParser p) <|> mkpq = MkParser pf
  where
    pf l = case p l of
      Just x => Just x
      Nothing => case mkpq of
        (MkParser q) => q l
  empty = MkParser (\s => Nothing)

instance Syntax Parser c where
  pure x = MkParser (\s => Just (x, s))
  item = MkParser f
  where
    f [] = Nothing
    f (x :: xs) = Just (x, xs)

-- Printer

data Printer a c = MkPrinter (a -> Maybe (List c))

compose : Printer a c -> a -> Maybe (List c)
compose (MkPrinter p) x = p x

instance PartIsoFunctor Printer where
  iso <$> (MkPrinter p) = MkPrinter (\b => ipc_unapply iso b >>= p)

instance PFunctor Printer where
  (MkPrinter p) <*> mkpq = MkPrinter pf
  where
    pf (x, y) = do
      x' <- p x
      case mkpq of
        (MkPrinter q) => do
          y' <- q y
          return (x' ++ y')

instance PAlternative Printer where
  (MkPrinter p) <|> mkpq = MkPrinter $ \s =>
    case (p s) of
      Nothing => case mkpq of
        (MkPrinter q) => q s
      x => x
  empty = MkPrinter (\s => Nothing)

instance Syntax Printer γ where
  pure x = MkPrinter (\y =>
    if x == y
    then Just []
    else Nothing)
  item = MkPrinter (\t => Just [t])

-- Basic parsers/composers

sat : Syntax d a => (a -> Bool) -> d a a
sat {a} p = (MkPartIso check check verify verify) <$> item
  where
    check : a -> Maybe a
    check x = if p x then Just x else Nothing
    verify y with (inspect $ p y)
      | match False {eq=eq} = rewrite eq in tt
      | match True {eq=eq} = rewrite eq in
        rewrite eq in refl

val : (Syntax d a, Eq a) => a -> d a a
val x = sat (== x)

-- -- rep

-- nilv : PartIso () (Vect 0 a)
-- nilv = MkPartIso (const . Just $ Vect.Nil {a=a})
--                  (\xs => case xs of
--                    [] => Just ()
--                    _ => Nothing)

-- consv : PartIso (a, Vect n a) (Vect (S n) a)
-- consv = MkPartIso c1 c2
--   where c1 (x, xs) = Just (x :: xs)
--         c2 (x :: xs) = Just (x, xs)

-- rep : Syntax d c => (n : Nat) -> d a c -> d (Vect n a) c
-- rep Z p = nilv <$> pure ()
-- rep (S k) p = consv <$> p <*> rep k p

-- -- many

-- nil : PartIso () (List a)
-- nil = MkPartIso c1 c2
--   where
--     c1 () = Just []
--     c2 [] = Just ()
--     c2 (x :: xs) = Nothing

-- cons : PartIso (a, List a) (List a)
-- cons = MkPartIso c1 c2
--   where
--     c1 (x, l) = Just $ x :: l
--     c2 [] = Nothing
--     c2 (x :: xs) = Just (x, xs)

-- partial many : Syntax d c => d a c -> d (List a) c
-- many p = (cons <$> (p <*> (many p)))
--      <|> (nil <$> pure ())

-- -- Various types

-- -- List Bool <-> Nat, with size and endianness

-- data Endianness = BE | LE

-- order : Endianness -> Vect n Bool -> Vect n Bool
-- order BE = reverse
-- order LE = id

-- natToBits : Nat -> Endianness -> (k : Nat) -> Vect k Bool
-- natToBits n e v = order e $ natToBits' n v
--   where natToBits' : Nat -> (k : Nat) -> Vect k Bool
--         natToBits' n Z = []
--         natToBits' Z bits = replicate bits False
--         natToBits' n (S bits) = (mod n 2 /= Z) :: natToBits' (div n 2) bits

-- bitsToNat : Vect n Bool -> Endianness -> Nat
-- bitsToNat v e = bitsToNat' (order e v)
--   where bitsToNat' : Vect k Bool -> Nat
--         bitsToNat' [] = Z
--         bitsToNat' (v :: l) = (if v then 1 else 0) + 2 * bitsToNat' l

-- nat : Syntax d Bool => Endianness -> Nat -> d Nat Bool
-- nat endianness size = MkPartIso pf cf <$> rep size item
--   where
--     pf l = Just $ bitsToNat l endianness
--     cf x = Just $ natToBits x endianness size

-- testing

test : Syntax d Nat => d (Nat, Nat) Nat
test = (val 1) <*> item
   <|> (val 2) <*> (val 3)

-- test2 : Syntax d Bool => d (Nat, Bool) Bool
-- test2 = (nat BE 4) <*> (val True)
--     <|> (nat BE 2) <*> (val False)

-- partial test3 : Syntax d Bool => d (Bool, List Nat) Bool
-- test3 = (val True) <*> ((ignore False <$> item) *> (many $ nat BE 4))
--     <|> (val False) <*> ((ignore True <$> item) *> (many $ nat LE 3))

-- -- compose test3 (False, [1,2,3])
-- -- parse test3 [False, True, False, False, False, True, False, True, True, False]

-- -- foldl

-- partial driver : (a -> Maybe a) -> (a -> a)
-- driver step state = case step state of
--   Just state' => driver step state'
--   Nothing => state

-- partial iterate : PartIso a a -> PartIso a a
-- iterate step = MkPartIso f g where
--   f = Just . driver (ipc_apply step)
--   g = Just . driver (ipc_unapply step)

-- step : PartIso (a, b) a -> PartIso (a, List b) (a, List b)
-- step i = (pTup i pId) . associate . (pTup pId (ipc_inverse cons))

-- partial foldl : PartIso (a, b) a -> PartIso (a, List b) a
-- foldl i = ipc_inverse unit . (pTup pId (ipc_inverse nil)) . iterate (step i)

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
-- Conway's Game Of Life in Idris
module Conway.Conway

import Data.Vect

-- | An individual Cell can either be alive or dead
public export
data CellState = Alive | Dead

public export
data Conway : Nat -> Nat -> Type where
   MkConway : (Vect m (Vect n CellState)) -> Conway m n

-- | Neighbours of a given cell, typically has 8 neighbours
--   (we'll count the missing neighbours from edges as dead)
data Neighbours : Nat -> Type where
   MkNeighbours : CellState -> (Vect n CellState) -> Neighbours n

-- | Count number of alive neighbours, guaranteed to be <= total
--   number of neighbours
numAlive : Neighbours n -> Fin (n + 1)
numAlive {n} nbs = case natToFin (numAlive' nbs) (n + 1) of
                  Just f => f
  where
    -- | Count number of alive neighbours
    numAlive' : Neighbours n -> Nat
    numAlive' (MkNeighbours _ v) = foldl accFn 0 v
      where accFn : Nat -> CellState -> Nat
            accFn cnt Alive = (cnt + 1)
            accFn cnt Dead =  (cnt + 0)

-- | Count the number of dead neighbours, guaranteed to be <= total
--   number of given neighbours
numDead : Neighbours n -> Fin (n + 1)
numDead {n} nbs = case natToFin (numDead' nbs) (n + 1) of
                  Just f => f
  where
    -- | Count number of dead neighbours
    numDead' : Neighbours n -> Nat
    numDead' (MkNeighbours _ v) = foldl accFn 0 v
      where accFn : Nat -> CellState -> Nat
            accFn cnt Alive = (cnt + 0)
            accFn cnt Dead =  (cnt + 1)

-- | Work out the new state of a cell given its neighbours
newCellState : Neighbours n -> CellState
newCellState (MkNeighbours cs v) with (cs, finToInteger $ numAlive $ MkNeighbours cs v)
  |  (Alive, 2) = Alive -- Stays alive
  |  (_, 3) = Alive -- Comes to life or stays alive
  |  (_, _) = Dead -- < 2 dies or stays dead and > 3 dies or stays dead

-- | Generate Neighbours for a given point in the board
getNeighbours : Conway m n -> Fin m -> Fin n -> Neighbours 8
getNeighbours (MkConway v) y x =
  (MkNeighbours cs [l, topL, top, topR, r, botR, bot, botL])

  where
        -- Check if Cell at given position is Dead Or Alive
        -- If out of bounds the Cell is considered Dead
        getDoA : Conway a b -> Integer -> Integer -> CellState
        getDoA {a} {b} (MkConway v) y x  =
          case getCell of
            Just c => c
            Nothing => Dead

           where getCell : Maybe CellState
                 getCell = do
                    row <- integerToFin y a
                    col <- integerToFin x b
                    return $ index col (index row v)

        ix : Integer
        ix = finToInteger x
        iy : Integer
        iy = finToInteger y

        cs = index x (index y v)

        l    = getDoA (MkConway v)  iy      (ix - 1)
        topL = getDoA (MkConway v) (iy - 1) (ix - 1)
        top  = getDoA (MkConway v) (iy - 1)  ix
        topR = getDoA (MkConway v) (iy - 1) (ix + 1)
        r    = getDoA (MkConway v)  iy      (ix + 1)
        botR = getDoA (MkConway v) (iy + 1) (ix + 1)
        bot  = getDoA (MkConway v) (iy + 1)  ix
        botL = getDoA (MkConway v) (iy + 1) (ix - 1)

-- | Generates a List of values 0 to N - 1
--   Guarantees that returned Vector has N values
sequence : (n : Nat) -> Vect n Nat
sequence n = reverse $ sequence' n
  where sequence' : (m : Nat) -> Vect m Nat
        sequence' Z = Nil
        sequence' (S n) = n::(sequence' n)

-- | Generates a Vector of values 0 to N - 1
--   Guarantees that returned Vector has N values
--   and every values is < N
export
sequenceFin : (n : Nat) -> Vect n (Fin n)
sequenceFin n = map n2f (sequence n)
  where n2f : Nat -> Fin n
        n2f m = case natToFin m n of
                  Just f => f

-- | Get the next state from the current state
export
iterateGame : Conway m n -> Conway m n
iterateGame {m} {n} (MkConway v) =  MkConway (map iterateRow (sequenceFin m))
  where iterateRow : Fin m -> Vect n CellState
        iterateRow y = map iteratePos (sequenceFin n)
        where iteratePos : Fin n -> CellState
              iteratePos x = newCellState (getNeighbours (MkConway v) y x)

max_stars_repo_name: RossMeikleham/Idris-Conway

max_issues_repo_name: RossMeikleham/Idris-Conway

max_forks_repo_name: RossMeikleham/Idris-Conway