text:
module TTImp.TTImp

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.Options
import Core.Options.Log
import Core.TT
import Core.TTC
import Core.Value

import Data.List
import Data.Maybe

%default covering

-- Information about names in nested blocks
public export
record NestedNames (vars : List Name) where
  constructor MkNested
  -- A map from names to the decorated version of the name, and the new name
  -- applied to its enclosing environment
  -- Takes the location and name type, because we don't know them until we
  -- elaborate the name at the point of use
  names : List (Name, (Maybe Name,  -- new name if there is one
                       List (Var vars), -- names used from the environment
                       FC -> NameType -> Term vars))

export
Weaken NestedNames where
  weaken (MkNested ns) = MkNested (map wknName ns)
    where
      wknName : (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars)) ->
                (Name, (Maybe Name, List (Var (n :: vars)), FC -> NameType -> Term (n :: vars)))
      wknName (n, (mn, vars, rep))
          = (n, (mn, map weaken vars, \fc, nt => weaken (rep fc nt)))

-- Unchecked terms, with implicit arguments
-- This is the raw, elaboratable form.
-- Higher level expressions (e.g. case, pattern matching let, where blocks,
-- do notation, etc, should elaborate via this, perhaps in some local
-- context).
public export
data BindMode = PI RigCount | PATTERN | NONE

mutual

  public export
  RawImp : Type
  RawImp = RawImp' Name

  public export
  IRawImp : Type
  IRawImp = RawImp' KindedName

  public export
  data RawImp' : Type -> Type where
       IVar : FC -> nm -> RawImp' nm
       IPi : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name ->
             (argTy : RawImp' nm) -> (retTy : RawImp' nm) -> RawImp' nm
       ILam : FC -> RigCount -> PiInfo (RawImp' nm) -> Maybe Name ->
              (argTy : RawImp' nm) -> (lamTy : RawImp' nm) -> RawImp' nm
       ILet : FC -> (lhsFC : FC) -> RigCount -> Name ->
              (nTy : RawImp' nm) -> (nVal : RawImp' nm) ->
              (scope : RawImp' nm) -> RawImp' nm
       ICase : FC -> RawImp' nm -> (ty : RawImp' nm) ->
               List (ImpClause' nm) -> RawImp' nm
       ILocal : FC -> List (ImpDecl' nm) -> RawImp' nm -> RawImp' nm
       -- Local definitions made elsewhere, but that we're pushing
       -- into a case branch as nested names.
       -- An appearance of 'uname' maps to an application of
       -- 'internalName' to 'args'.
       ICaseLocal : FC -> (uname : Name) ->
                    (internalName : Name) ->
                    (args : List Name) -> RawImp' nm -> RawImp' nm

       IUpdate : FC -> List (IFieldUpdate' nm) -> RawImp' nm -> RawImp' nm

       IApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
       IAutoApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
       INamedApp : FC -> RawImp' nm -> Name -> RawImp' nm -> RawImp' nm
       IWithApp : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm

       ISearch : FC -> (depth : Nat) -> RawImp' nm
       IAlternative : FC -> AltType' nm -> List (RawImp' nm) -> RawImp' nm
       IRewrite : FC -> RawImp' nm -> RawImp' nm -> RawImp' nm
       ICoerced : FC -> RawImp' nm -> RawImp' nm

       -- Any implicit bindings in the scope should be bound here, using
       -- the given binder
       IBindHere : FC -> BindMode -> RawImp' nm -> RawImp' nm
       -- A name which should be implicitly bound
       IBindVar : FC -> String -> RawImp' nm
       -- An 'as' pattern, valid on the LHS of a clause only
       IAs : FC -> (nameFC : FC) -> UseSide -> Name -> RawImp' nm -> RawImp' nm
       -- A 'dot' pattern, i.e. one which must also have the given value
       -- by unification
       IMustUnify : FC -> DotReason -> RawImp' nm -> RawImp' nm

       -- Laziness annotations
       IDelayed : FC -> LazyReason -> RawImp' nm -> RawImp' nm -- the type
       IDelay : FC -> RawImp' nm -> RawImp' nm -- delay constructor
       IForce : FC -> RawImp' nm -> RawImp' nm

       -- Quasiquoting
       IQuote : FC -> RawImp' nm -> RawImp' nm
       IQuoteName : FC -> Name -> RawImp' nm
       IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm
       IUnquote : FC -> RawImp' nm -> RawImp' nm
       IRunElab : FC -> RawImp' nm -> RawImp' nm

       IPrimVal : FC -> (c : Constant) -> RawImp' nm
       IType : FC -> RawImp' nm
       IHole : FC -> String -> RawImp' nm

       IUnifyLog : FC -> LogLevel -> RawImp' nm -> RawImp' nm
       -- An implicit value, solved by unification, but which will also be
       -- bound (either as a pattern variable or a type variable) if unsolved
       -- at the end of elaborator
       Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp' nm

       -- with-disambiguation
       IWithUnambigNames : FC -> List Name -> RawImp' nm -> RawImp' nm

  public export
  IFieldUpdate : Type
  IFieldUpdate = IFieldUpdate' Name

  public export
  data IFieldUpdate' : Type -> Type where
       ISetField : (path : List String) -> RawImp' nm -> IFieldUpdate' nm
       ISetFieldApp : (path : List String) -> RawImp' nm -> IFieldUpdate' nm

  public export
  AltType : Type
  AltType = AltType' Name

  public export
  data AltType' : Type -> Type where
       FirstSuccess : AltType' nm
       Unique : AltType' nm
       UniqueDefault : RawImp' nm -> AltType' nm

  export
    Show nm => Show (RawImp' nm) where
      show (IVar fc n) = show n
      show (IPi fc c p n arg ret)
         = "(%pi " ++ show c ++ " " ++ show p ++ " " ++
           showPrec App n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
      show (ILam fc c p n arg sc)
         = "(%lam " ++ show c ++ " " ++ show p ++ " " ++
           showPrec App n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
      show (ILet fc lhsFC c n ty val sc)
         = "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
           " " ++ show val ++ " " ++ show sc ++ ")"
      show (ICase _ scr scrty alts)
         = "(%case (" ++ show scr ++ " : " ++ show scrty ++ ") " ++ show alts ++ ")"
      show (ILocal _ def scope)
         = "(%local (" ++ show def ++ ") " ++ show scope ++ ")"
      show (ICaseLocal _ uname iname args sc)
         = "(%caselocal (" ++ show uname ++ " " ++ show iname
               ++ " " ++ show args ++ ") " ++ show sc ++ ")"
      show (IUpdate _ flds rec)
         = "(%record " ++ showSep ", " (map show flds) ++ " " ++ show rec ++ ")"
      show (IApp fc f a)
         = "(" ++ show f ++ " " ++ show a ++ ")"
      show (INamedApp fc f n a)
         = "(" ++ show f ++ " [" ++ show n ++ " = " ++ show a ++ "])"
      show (IAutoApp fc f a)
         = "(" ++ show f ++ " [" ++ show a ++ "])"
      show (IWithApp fc f a)
         = "(" ++ show f ++ " | " ++ show a ++ ")"
      show (ISearch fc d)
         = "%search"
      show (IAlternative fc ty alts)
         = "(|" ++ showSep "," (map show alts) ++ "|)"
      show (IRewrite _ rule tm)
         = "(%rewrite (" ++ show rule ++ ") (" ++ show tm ++ "))"
      show (ICoerced _ tm) = "(%coerced " ++ show tm ++ ")"

      show (IBindHere fc b sc)
         = "(%bindhere " ++ show sc ++ ")"
      show (IBindVar fc n) = "$" ++ n
      show (IAs fc _ _ n tm) = show n ++ "@(" ++ show tm ++ ")"
      show (IMustUnify fc r tm) = ".(" ++ show tm ++ ")"
      show (IDelayed fc r tm) = "(%delayed " ++ show tm ++ ")"
      show (IDelay fc tm) = "(%delay " ++ show tm ++ ")"
      show (IForce fc tm) = "(%force " ++ show tm ++ ")"
      show (IQuote fc tm) = "(%quote " ++ show tm ++ ")"
      show (IQuoteName fc tm) = "(%quotename " ++ show tm ++ ")"
      show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
      show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
      show (IRunElab fc tm) = "(%runelab " ++ show tm ++ ")"
      show (IPrimVal fc c) = show c
      show (IHole _ x) = "?" ++ x
      show (IUnifyLog _ lvl x) = "(%logging " ++ show lvl ++ " " ++ show x ++ ")"
      show (IType fc) = "%type"
      show (Implicit fc True) = "_"
      show (Implicit fc False) = "?"
      show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")"

  export
  Show nm => Show (IFieldUpdate' nm) where
    show (ISetField p val) = showSep "->" p ++ " = " ++ show val
    show (ISetFieldApp p val) = showSep "->" p ++ " $= " ++ show val

  public export
  FnOpt : Type
  FnOpt = FnOpt' Name

  public export
  data FnOpt' : Type -> Type where
       Inline : FnOpt' nm
       TCInline : FnOpt' nm
       -- Flag means the hint is a direct hint, not a function which might
       -- find the result (e.g. chasing parent interface dictionaries)
       Hint : Bool -> FnOpt' nm
       -- Flag means to use as a default if all else fails
       GlobalHint : Bool -> FnOpt' nm
       ExternFn : FnOpt' nm
       -- Defined externally, list calling conventions
       ForeignFn : List (RawImp' nm) -> FnOpt' nm
       -- assume safe to cancel arguments in unification
       Invertible : FnOpt' nm
       Totality : TotalReq -> FnOpt' nm
       Macro : FnOpt' nm
       SpecArgs : List Name -> FnOpt' nm

  public export
  isTotalityReq : FnOpt' nm -> Bool
  isTotalityReq (Totality _) = True
  isTotalityReq _ = False

  export
  Show nm => Show (FnOpt' nm) where
    show Inline = "%inline"
    show TCInline = "%tcinline"
    show (Hint t) = "%hint " ++ show t
    show (GlobalHint t) = "%globalhint " ++ show t
    show ExternFn = "%extern"
    show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs)
    show Invertible = "%invertible"
    show (Totality Total) = "total"
    show (Totality CoveringOnly) = "covering"
    show (Totality PartialOK) = "partial"
    show Macro = "%macro"
    show (SpecArgs ns) = "%spec " ++ showSep " " (map show ns)

  export
  Eq FnOpt where
    Inline == Inline = True
    TCInline == TCInline = True
    (Hint x) == (Hint y) = x == y
    (GlobalHint x) == (GlobalHint y) = x == y
    ExternFn == ExternFn = True
    (ForeignFn xs) == (ForeignFn ys) = True -- xs == ys
    Invertible == Invertible = True
    (Totality tot_lhs) == (Totality tot_rhs) = tot_lhs == tot_rhs
    Macro == Macro = True
    (SpecArgs ns) == (SpecArgs ns') = ns == ns'
    _ == _ = False

  public export
  ImpTy : Type
  ImpTy = ImpTy' Name

  public export
  data ImpTy' : Type -> Type where
       MkImpTy : FC -> (nameFC : FC) -> (n : Name) -> (ty : RawImp' nm) -> ImpTy' nm

  export
  Show nm => Show (ImpTy' nm) where
    show (MkImpTy fc _ n ty) = "(%claim " ++ show n ++ " " ++ show ty ++ ")"

  public export
  data DataOpt : Type where
       SearchBy : List Name -> DataOpt -- determining arguments
       NoHints : DataOpt -- Don't generate search hints for constructors
       UniqueSearch : DataOpt -- auto implicit search must check result is unique
       External : DataOpt -- implemented externally
       NoNewtype : DataOpt -- don't apply newtype optimisation

  export
  Eq DataOpt where
    (==) (SearchBy xs) (SearchBy ys) = xs == ys
    (==) NoHints NoHints = True
    (==) UniqueSearch UniqueSearch = True
    (==) External External = True
    (==) NoNewtype NoNewtype = True
    (==) _ _ = False

  public export
  ImpData : Type
  ImpData = ImpData' Name

  public export
  data ImpData' : Type -> Type where
       MkImpData : FC -> (n : Name) -> (tycon : RawImp' nm) ->
                   (opts : List DataOpt) ->
                   (datacons : List (ImpTy' nm)) -> ImpData' nm
       MkImpLater : FC -> (n : Name) -> (tycon : RawImp' nm) -> ImpData' nm

  export
  Show nm => Show (ImpData' nm) where
    show (MkImpData fc n tycon _ cons)
        = "(%data " ++ show n ++ " " ++ show tycon ++ " " ++
           show cons ++ ")"
    show (MkImpLater fc n tycon)
        = "(%datadecl " ++ show n ++ " " ++ show tycon ++ ")"

  public export
  IField : Type
  IField = IField' Name

  public export
  data IField' : Type -> Type where
       MkIField : FC -> RigCount -> PiInfo (RawImp' nm) -> Name -> RawImp' nm ->
                  IField' nm

  -- TODO: turn into a proper datatype
  public export
  ImpParameter' : Type -> Type
  ImpParameter' nm = (Name, RigCount, PiInfo (RawImp' nm), RawImp' nm)

  public export
  ImpRecord : Type
  ImpRecord = ImpRecord' Name

  public export
  data ImpRecord' : Type -> Type where
       MkImpRecord : FC -> (n : Name) ->
                     (params : List (ImpParameter' nm)) ->
                     (conName : Name) ->
                     (fields : List (IField' nm)) ->
                     ImpRecord' nm

  export
  Show nm => Show (IField' nm) where
    show (MkIField _ c Explicit n ty) = show n ++ " : " ++ show ty
    show (MkIField _ c _ n ty) = "{" ++ show n ++ " : " ++ show ty ++ "}"

  export
  Show nm => Show (ImpRecord' nm) where
    show (MkImpRecord _ n params con fields)
        = "record " ++ show n ++ " " ++ show params ++
          " " ++ show con ++ "\n\t" ++
          showSep "\n\t" (map show fields) ++ "\n"

  public export
  data WithFlag
         = Syntactic -- abstract syntactically, rather than by value

  export
  Eq WithFlag where
      Syntactic == Syntactic = True

  public export
  ImpClause : Type
  ImpClause = ImpClause' Name

  public export
  IImpClause : Type
  IImpClause = ImpClause' KindedName

  public export
  data ImpClause' : Type -> Type where
       PatClause : FC -> (lhs : RawImp' nm) -> (rhs : RawImp' nm) -> ImpClause' nm
       WithClause : FC -> (lhs : RawImp' nm) ->
                    (wval : RawImp' nm) -> (prf : Maybe Name) ->
                    (flags : List WithFlag) ->
                    List (ImpClause' nm) -> ImpClause' nm
       ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm

  export
  Show nm => Show (ImpClause' nm) where
    show (PatClause fc lhs rhs)
       = show lhs ++ " = " ++ show rhs
    show (WithClause fc lhs wval prf flags block)
       = show lhs
       ++ " with " ++ show wval
       ++ maybe "" (\ nm => " proof " ++ show nm) prf
       ++ "\n\t" ++ show block
    show (ImpossibleClause fc lhs)
       = show lhs ++ " impossible"

  public export
  ImpDecl : Type
  ImpDecl = ImpDecl' Name

  public export
  data ImpDecl' : Type -> Type where
       IClaim : FC -> RigCount -> Visibility -> List (FnOpt' nm) ->
                ImpTy' nm -> ImpDecl' nm
       IData : FC -> Visibility -> ImpData' nm -> ImpDecl' nm
       IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm
       IParameters : FC ->
                     List (ImpParameter' nm) ->
                     List (ImpDecl' nm) -> ImpDecl' nm
       IRecord : FC ->
                 Maybe String -> -- nested namespace
                 Visibility -> ImpRecord' nm -> ImpDecl' nm
       INamespace : FC -> Namespace -> List (ImpDecl' nm) -> ImpDecl' nm
       ITransform : FC -> Name -> RawImp' nm -> RawImp' nm -> ImpDecl' nm
       IRunElabDecl : FC -> RawImp' nm -> ImpDecl' nm
       IPragma : List Name -> -- pragmas might define names that wouldn't
                       -- otherwise be spotted in 'definedInBlock' so they
                       -- can be flagged here.
                 ({vars : _} ->
                  NestedNames vars -> Env Term vars -> Core ()) ->
                 ImpDecl' nm
       ILog : Maybe (List String, Nat) -> ImpDecl' nm
       IBuiltin : FC -> BuiltinType -> Name -> ImpDecl' nm

  export
  Show nm => Show (ImpDecl' nm) where
    show (IClaim _ c _ opts ty) = show opts ++ " " ++ show c ++ " " ++ show ty
    show (IData _ _ d) = show d
    show (IDef _ n cs) = "(%def " ++ show n ++ " " ++ show cs ++ ")"
    show (IParameters _ ps ds)
        = "parameters " ++ show ps ++ "\n\t" ++
          showSep "\n\t" (assert_total $ map show ds)
    show (IRecord _ _ _ d) = show d
    show (INamespace _ ns decls)
        = "namespace " ++ show ns ++
          showSep "\n" (assert_total $ map show decls)
    show (ITransform _ n lhs rhs)
        = "%transform " ++ show n ++ " " ++ show lhs ++ " ==> " ++ show rhs
    show (IRunElabDecl _ tm)
        = "%runElab " ++ show tm
    show (IPragma _ _) = "[externally defined pragma]"
    show (ILog Nothing) = "%logging off"
    show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
      [] => show lvl
      _  => concat (intersperse "." topic) ++ " " ++ show lvl
    show (IBuiltin _ type name) = "%builtin " ++ show type ++ " " ++ show name

export
isIPrimVal : RawImp' nm -> Maybe Constant
isIPrimVal (IPrimVal _ c) = Just c
isIPrimVal _ = Nothing

-- REPL commands for TTImp interaction
public export
data ImpREPL : Type where
     Eval : RawImp -> ImpREPL
     Check : RawImp -> ImpREPL
     ProofSearch : Name -> ImpREPL
     ExprSearch : Name -> ImpREPL
     GenerateDef : Int -> Name -> ImpREPL
     Missing : Name -> ImpREPL
     CheckTotal : Name -> ImpREPL
     DebugInfo : Name -> ImpREPL
     Quit : ImpREPL

export
mapAltType : (RawImp' nm -> RawImp' nm) -> AltType' nm -> AltType' nm
mapAltType f (UniqueDefault x) = UniqueDefault (f x)
mapAltType _ u = u

export
lhsInCurrentNS : {auto c : Ref Ctxt Defs} ->
                 NestedNames vars -> RawImp -> Core RawImp
lhsInCurrentNS nest (IApp loc f a)
    = do f' <- lhsInCurrentNS nest f
         pure (IApp loc f' a)
lhsInCurrentNS nest (IAutoApp loc f a)
    = do f' <- lhsInCurrentNS nest f
         pure (IAutoApp loc f' a)
lhsInCurrentNS nest (INamedApp loc f n a)
    = do f' <- lhsInCurrentNS nest f
         pure (INamedApp loc f' n a)
lhsInCurrentNS nest (IWithApp loc f a)
    = do f' <- lhsInCurrentNS nest f
         pure (IWithApp loc f' a)
lhsInCurrentNS nest tm@(IVar loc (NS _ _)) = pure tm -- leave explicit NS alone
lhsInCurrentNS nest (IVar loc n)
    = case lookup n (names nest) of
           Nothing =>
              do n' <- inCurrentNS n
                 pure (IVar loc n')
           -- If it's one of the names in the current nested block, we'll
           -- be rewriting it during elaboration to be in the scope of the
           -- parent name.
           Just _ => pure (IVar loc n)
lhsInCurrentNS nest tm = pure tm

export
findIBinds : RawImp' nm -> List String
findIBinds (IPi fc rig p mn aty retty)
    = findIBinds aty ++ findIBinds retty
findIBinds (ILam fc rig p n aty sc)
    = findIBinds aty ++ findIBinds sc
findIBinds (IApp fc fn av)
    = findIBinds fn ++ findIBinds av
findIBinds (IAutoApp fc fn av)
    = findIBinds fn ++ findIBinds av
findIBinds (INamedApp _ fn _ av)
    = findIBinds fn ++ findIBinds av
findIBinds (IWithApp fc fn av)
    = findIBinds fn ++ findIBinds av
findIBinds (IAs fc _ _ (UN (Basic n)) pat)
    = n :: findIBinds pat
findIBinds (IAs fc _ _ n pat)
    = findIBinds pat
findIBinds (IMustUnify fc r pat)
    = findIBinds pat
findIBinds (IAlternative fc u alts)
    = concatMap findIBinds alts
findIBinds (IDelayed fc _ ty) = findIBinds ty
findIBinds (IDelay fc tm) = findIBinds tm
findIBinds (IForce fc tm) = findIBinds tm
findIBinds (IQuote fc tm) = findIBinds tm
findIBinds (IUnquote fc tm) = findIBinds tm
findIBinds (IRunElab fc tm) = findIBinds tm
findIBinds (IBindHere _ _ tm) = findIBinds tm
findIBinds (IBindVar _ n) = [n]
-- We've skipped lambda, case, let and local - rather than guess where the
-- name should be bound, leave it to the programmer
findIBinds tm = []

export
findImplicits : RawImp' nm -> List String
findImplicits (IPi fc rig p (Just (UN (Basic mn))) aty retty)
    = mn :: findImplicits aty ++ findImplicits retty
findImplicits (IPi fc rig p mn aty retty)
    = findImplicits aty ++ findImplicits retty
findImplicits (ILam fc rig p n aty sc)
    = findImplicits aty ++ findImplicits sc
findImplicits (IApp fc fn av)
    = findImplicits fn ++ findImplicits av
findImplicits (IAutoApp _ fn av)
    = findImplicits fn ++ findImplicits av
findImplicits (INamedApp _ fn _ av)
    = findImplicits fn ++ findImplicits av
findImplicits (IWithApp fc fn av)
    = findImplicits fn ++ findImplicits av
findImplicits (IAs fc _ _ n pat)
    = findImplicits pat
findImplicits (IMustUnify fc r pat)
    = findImplicits pat
findImplicits (IAlternative fc u alts)
    = concatMap findImplicits alts
findImplicits (IDelayed fc _ ty) = findImplicits ty
findImplicits (IDelay fc tm) = findImplicits tm
findImplicits (IForce fc tm) = findImplicits tm
findImplicits (IQuote fc tm) = findImplicits tm
findImplicits (IUnquote fc tm) = findImplicits tm
findImplicits (IRunElab fc tm) = findImplicits tm
findImplicits (IBindVar _ n) = [n]
findImplicits tm = []

-- Update the lhs of a clause so that any implicits named in the type are
-- bound as @-patterns (unless they're already explicitly bound or appear as
-- IBindVar anywhere else in the pattern) so that they will be available on the
-- rhs
export
implicitsAs : {auto c : Ref Ctxt Defs} ->
              Int -> Defs ->
              (vars : List Name) ->
              RawImp -> Core RawImp
implicitsAs n defs ns tm
  = do let implicits = findIBinds tm
       log "declare.def.lhs.implicits" 30 $ "Found implicits: " ++ show implicits
       setAs (map Just (ns ++ map (UN . Basic) implicits)) [] tm
  where
    -- Takes the function application expression which is the lhs of a clause
    -- and decomposes it into the underlying function symbol and the variables
    -- bound by appearing as arguments, and then passes this onto `findImps`.
    -- More precisely, implicit and explicit arguments are recorded separately,
    -- into `is` and `es` respectively.
    setAs : List (Maybe Name) -> List (Maybe Name) -> RawImp -> Core RawImp
    setAs is es (IApp loc f a)
        = do f' <- setAs is (Nothing :: es) f
             pure $ IApp loc f' a
    setAs is es (IAutoApp loc f a)
        = do f' <- setAs (Nothing :: is) es f
             pure $ IAutoApp loc f' a
    setAs is es (INamedApp loc f n a)
        = do f' <- setAs (Just n :: is) (Just n :: es) f
             pure $ INamedApp loc f' n a
    setAs is es (IWithApp loc f a)
        = do f' <- setAs is es f
             pure $ IWithApp loc f' a
    setAs is es (IVar loc nm)
        -- #834 Use the (already) resolved name rather than the local one
        = case !(lookupTyExact (Resolved n) (gamma defs)) of
            Nothing =>
               do log "declare.def.lhs.implicits" 30 $
                    "Could not find variable " ++ show n
                  pure $ IVar loc nm
            Just ty =>
               do ty' <- nf defs [] ty
                  implicits <- findImps is es ns ty'
                  log "declare.def.lhs.implicits" 30 $
                    "\n  In the type of " ++ show n ++ ": " ++ show ty ++
                    "\n  Using locals: " ++ show ns ++
                    "\n  Found implicits: " ++ show implicits
                  pure $ impAs (virtualiseFC loc) implicits (IVar loc nm)
      where
        -- If there's an @{c} in the list of given implicits, that's the next
        -- autoimplicit, so don't rewrite the LHS and update the list of given
        -- implicits
        updateNs : Name -> List (Maybe Name) -> Maybe (List (Maybe Name))
        updateNs n (Nothing :: ns) = Just ns
        updateNs n (x :: ns)
            = if Just n == x
                 then Just ns -- found it
                 else do ns' <- updateNs n ns
                         pure (x :: ns')
        updateNs n [] = Nothing

        -- Finds the missing implicits which should be added to the lhs of the
        -- original pattern clause.
        --
        -- The first argument, `ns`, specifies which implicit variables alredy
        -- appear in the lhs, and therefore need not be added.
        -- The second argument, `es`, specifies which *explicit* variables appear
        -- in the lhs: this is used to determine when to stop searching for further
        -- implicits to add.
        findImps : List (Maybe Name) -> List (Maybe Name) ->
                   List Name -> NF [] ->
                   Core (List (Name, PiInfo RawImp))
        -- #834 When we are in a local definition, we have an explicit telescope
        -- corresponding to the variables bound in the parent function.
        -- So we first peel off all of the explicit quantifiers corresponding
        -- to these variables.
        findImps ns es (_ :: locals) (NBind fc x (Pi _ _ Explicit _) sc)
          = do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
               findImps ns es locals body
               -- ^ TODO? check that name of the pi matches name of local?
        -- don't add implicits coming after explicits that aren't given
        findImps ns es [] (NBind fc x (Pi _ _ Explicit _) sc)
            = do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
                 case es of
                   -- Explicits were skipped, therefore all explicits are given anyway
                   Just (UN Underscore) :: _ => findImps ns es [] body
                   -- Explicits weren't skipped, so we need to check
                   _ => case updateNs x es of
                          Nothing => pure [] -- explicit wasn't given
                          Just es' => findImps ns es' [] body
        -- if the implicit was given, skip it
        findImps ns es [] (NBind fc x (Pi _ _ AutoImplicit _) sc)
            = do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
                 case updateNs x ns of
                   Nothing => -- didn't find explicit call
                      pure $ (x, AutoImplicit) :: !(findImps ns es [] body)
                   Just ns' => findImps ns' es [] body
        findImps ns es [] (NBind fc x (Pi _ _ p _) sc)
            = do body <- sc defs (toClosure defaultOpts [] (Erased fc False))
                 if Just x `elem` ns
                   then findImps ns es [] body
                   else pure $ (x, forgetDef p) :: !(findImps ns es [] body)
        findImps _ _ locals _
          = do log "declare.def.lhs.implicits" 50 $
                  "Giving up with the following locals left: " ++ show locals
               pure []

        impAs : FC -> List (Name, PiInfo RawImp) -> RawImp -> RawImp
        impAs loc' [] tm = tm
        impAs loc' ((nm@(UN (Basic n)), AutoImplicit) :: ns) tm
            = impAs loc' ns $
                 INamedApp loc' tm nm (IBindVar loc' n)

        impAs loc' ((n, Implicit) :: ns) tm
            = impAs loc' ns $
                 INamedApp loc' tm n
                     (IAs loc' EmptyFC UseLeft n (Implicit loc' True))

        impAs loc' ((n, DefImplicit t) :: ns) tm
            = impAs loc' ns $
                 INamedApp loc' tm n
                     (IAs loc' EmptyFC UseLeft n (Implicit loc' True))

        impAs loc' (_ :: ns) tm = impAs loc' ns tm
    setAs is es tm = pure tm

export
definedInBlock : Namespace -> -- namespace to resolve names
                 List ImpDecl -> List Name
definedInBlock ns decls =
    concatMap (defName ns) decls
  where
    getName : ImpTy -> Name
    getName (MkImpTy _ _ n _) = n

    getFieldName : IField -> Name
    getFieldName (MkIField _ _ _ n _) = n

    expandNS : Namespace -> Name -> Name
    expandNS ns n
       = if ns == emptyNS then n else case n of
           UN _ => NS ns n
           MN _ _ => NS ns n
           DN _ _ => NS ns n
           _ => n

    defName : Namespace -> ImpDecl -> List Name
    defName ns (IClaim _ _ _ _ ty) = [expandNS ns (getName ty)]
    defName ns (IData _ _ (MkImpData _ n _ _ cons))
        = expandNS ns n :: map (expandNS ns) (map getName cons)
    defName ns (IData _ _ (MkImpLater _ n _)) = [expandNS ns n]
    defName ns (IParameters _ _ pds) = concatMap (defName ns) pds
    defName ns (INamespace _ n nds) = concatMap (defName (ns <.> n)) nds
    defName ns (IRecord _ fldns _ (MkImpRecord _ n _ con flds))
        = expandNS ns con :: all
      where
        fldns' : Namespace
        fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns

        toRF : Name -> Name
        toRF (UN (Basic n)) = UN (Field n)
        toRF n = n

        fnsUN : List Name
        fnsUN = map getFieldName flds

        fnsRF : List Name
        fnsRF = map toRF fnsUN

        -- Depending on %prefix_record_projections,
        -- the record may or may not produce prefix projections (fnsUN).
        --
        -- However, since definedInBlock is pure, we can't check that flag
        -- (and it would also be wrong if %prefix_record_projections appears
        -- inside the parameter block)
        -- so let's just declare all of them and some may go unused.
        all : List Name
        all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)

    defName ns (IPragma pns _) = map (expandNS ns) pns
    defName _ _ = []

export
getFC : RawImp' nm -> FC
getFC (IVar x _) = x
getFC (IPi x _ _ _ _ _) = x
getFC (ILam x _ _ _ _ _) = x
getFC (ILet x _ _ _ _ _ _) = x
getFC (ICase x _ _ _) = x
getFC (ILocal x _ _) = x
getFC (ICaseLocal x _ _ _ _) = x
getFC (IUpdate x _ _) = x
getFC (IApp x _ _) = x
getFC (INamedApp x _ _ _) = x
getFC (IAutoApp x _ _) = x
getFC (IWithApp x _ _) = x
getFC (ISearch x _) = x
getFC (IAlternative x _ _) = x
getFC (IRewrite x _ _) = x
getFC (ICoerced x _) = x
getFC (IPrimVal x _) = x
getFC (IHole x _) = x
getFC (IUnifyLog x _ _) = x
getFC (IType x) = x
getFC (IBindVar x _) = x
getFC (IBindHere x _ _) = x
getFC (IMustUnify x _ _) = x
getFC (IDelayed x _ _) = x
getFC (IDelay x _) = x
getFC (IForce x _) = x
getFC (IQuote x _) = x
getFC (IQuoteName x _) = x
getFC (IQuoteDecl x _) = x
getFC (IUnquote x _) = x
getFC (IRunElab x _) = x
getFC (IAs x _ _ _ _) = x
getFC (Implicit x _) = x
getFC (IWithUnambigNames x _ _) = x

namespace ImpDecl

  public export
  getFC : ImpDecl' nm -> FC
  getFC (IClaim fc _ _ _ _) = fc
  getFC (IData fc _ _) = fc
  getFC (IDef fc _ _) = fc
  getFC (IParameters fc _ _) = fc
  getFC (IRecord fc _ _ _ ) = fc
  getFC (INamespace fc _ _) = fc
  getFC (ITransform fc _ _ _) = fc
  getFC (IRunElabDecl fc _) = fc
  getFC (IPragma _ _) = EmptyFC
  getFC (ILog _) = EmptyFC
  getFC (IBuiltin fc _ _) = fc

export
apply : RawImp' nm -> List (RawImp' nm) -> RawImp' nm
apply f [] = f
apply f (x :: xs) =
  let fFC = getFC f in
  apply (IApp (fromMaybe fFC (mergeFC fFC (getFC x))) f x) xs

export
gapply : RawImp' nm -> List (Maybe Name, RawImp' nm) -> RawImp' nm
gapply f [] = f
gapply f (x :: xs) = gapply (uncurry (app f) x) xs where

  app : RawImp' nm -> Maybe Name -> RawImp' nm -> RawImp' nm
  app f Nothing x =  IApp (getFC f) f x
  app f (Just nm) x = INamedApp (getFC f) f nm x

export
getFn : RawImp' nm -> RawImp' nm
getFn (IApp _ f _) = getFn f
getFn (IWithApp _ f _) = getFn f
getFn (INamedApp _ f _ _) = getFn f
getFn (IAutoApp _ f _) = getFn f
getFn (IAs _ _ _ _ f) = getFn f
getFn (IMustUnify _ _ f) = getFn f
getFn f = f

-- Everything below is TTC instances

export
TTC BuiltinType where
    toBuf b BuiltinNatural = tag 0
    toBuf b NaturalToInteger = tag 1
    toBuf b IntegerToNatural = tag 2
    fromBuf b = case !getTag of
        0 => pure BuiltinNatural
        1 => pure NaturalToInteger
        2 => pure IntegerToNatural
        _ => corrupt "BuiltinType"

mutual
  export
  TTC RawImp where
    toBuf b (IVar fc n) = do tag 0; toBuf b fc; toBuf b n
    toBuf b (IPi fc r p n argTy retTy)
        = do tag 1; toBuf b fc; toBuf b r; toBuf b p; toBuf b n
             toBuf b argTy; toBuf b retTy
    toBuf b (ILam fc r p n argTy scope)
        = do tag 2; toBuf b fc; toBuf b r; toBuf b p; toBuf b n;
             toBuf b argTy; toBuf b scope
    toBuf b (ILet fc lhsFC r n nTy nVal scope)
        = do tag 3; toBuf b fc; toBuf b lhsFC; toBuf b r; toBuf b n;
             toBuf b nTy; toBuf b nVal; toBuf b scope
    toBuf b (ICase fc y ty xs)
        = do tag 4; toBuf b fc; toBuf b y; toBuf b ty; toBuf b xs
    toBuf b (ILocal fc xs sc)
        = do tag 5; toBuf b fc; toBuf b xs; toBuf b sc
    toBuf b (ICaseLocal fc _ _ _ sc)
        = toBuf b sc
    toBuf b (IUpdate fc fs rec)
        = do tag 6; toBuf b fc; toBuf b fs; toBuf b rec
    toBuf b (IApp fc fn arg)
        = do tag 7; toBuf b fc; toBuf b fn; toBuf b arg
    toBuf b (INamedApp fc fn y arg)
        = do tag 8; toBuf b fc; toBuf b fn; toBuf b y; toBuf b arg
    toBuf b (IWithApp fc fn arg)
        = do tag 9; toBuf b fc; toBuf b fn; toBuf b arg
    toBuf b (ISearch fc depth)
        = do tag 10; toBuf b fc; toBuf b depth
    toBuf b (IAlternative fc y xs)
        = do tag 11; toBuf b fc; toBuf b y; toBuf b xs
    toBuf b (IRewrite fc x y)
        = do tag 12; toBuf b fc; toBuf b x; toBuf b y
    toBuf b (ICoerced fc y)
        = do tag 13; toBuf b fc; toBuf b y

    toBuf b (IBindHere fc m y)
        = do tag 14; toBuf b fc; toBuf b m; toBuf b y
    toBuf b (IBindVar fc y)
        = do tag 15; toBuf b fc; toBuf b y
    toBuf b (IAs fc nameFC s y pattern)
        = do tag 16; toBuf b fc; toBuf b nameFC; toBuf b s; toBuf b y;
             toBuf b pattern
    toBuf b (IMustUnify fc r pattern)
        -- No need to record 'r', it's for type errors only
        = do tag 17; toBuf b fc; toBuf b pattern

    toBuf b (IDelayed fc r y)
        = do tag 18; toBuf b fc; toBuf b r; toBuf b y
    toBuf b (IDelay fc t)
        = do tag 19; toBuf b fc; toBuf b t
    toBuf b (IForce fc t)
        = do tag 20; toBuf b fc; toBuf b t

    toBuf b (IQuote fc t)
        = do tag 21; toBuf b fc; toBuf b t
    toBuf b (IQuoteName fc t)
        = do tag 22; toBuf b fc; toBuf b t
    toBuf b (IQuoteDecl fc t)
        = do tag 23; toBuf b fc; toBuf b t
    toBuf b (IUnquote fc t)
        = do tag 24; toBuf b fc; toBuf b t
    toBuf b (IRunElab fc t)
        = do tag 25; toBuf b fc; toBuf b t

    toBuf b (IPrimVal fc y)
        = do tag 26; toBuf b fc; toBuf b y
    toBuf b (IType fc)
        = do tag 27; toBuf b fc
    toBuf b (IHole fc y)
        = do tag 28; toBuf b fc; toBuf b y
    toBuf b (IUnifyLog fc lvl x) = toBuf b x

    toBuf b (Implicit fc i)
        = do tag 29; toBuf b fc; toBuf b i
    toBuf b (IWithUnambigNames fc ns rhs)
        = do tag 30; toBuf b ns; toBuf b rhs
    toBuf b (IAutoApp fc fn arg)
        = do tag 31; toBuf b fc; toBuf b fn; toBuf b arg

    fromBuf b
        = case !getTag of
               0 => do fc <- fromBuf b; n <- fromBuf b;
                       pure (IVar fc n)
               1 => do fc <- fromBuf b;
                       r <- fromBuf b; p <- fromBuf b;
                       n <- fromBuf b
                       argTy <- fromBuf b; retTy <- fromBuf b
                       pure (IPi fc r p n argTy retTy)
               2 => do fc <- fromBuf b;
                       r <- fromBuf b; p <- fromBuf b; n <- fromBuf b
                       argTy <- fromBuf b; scope <- fromBuf b
                       pure (ILam fc r p n argTy scope)
               3 => do fc <- fromBuf b;
                       lhsFC <- fromBuf b;
                       r <- fromBuf b; n <- fromBuf b
                       nTy <- fromBuf b; nVal <- fromBuf b
                       scope <- fromBuf b
                       pure (ILet fc lhsFC r n nTy nVal scope)
               4 => do fc <- fromBuf b; y <- fromBuf b;
                       ty <- fromBuf b; xs <- fromBuf b
                       pure (ICase fc y ty xs)
               5 => do fc <- fromBuf b;
                       xs <- fromBuf b; sc <- fromBuf b
                       pure (ILocal fc xs sc)
               6 => do fc <- fromBuf b; fs <- fromBuf b
                       rec <- fromBuf b
                       pure (IUpdate fc fs rec)
               7 => do fc <- fromBuf b; fn <- fromBuf b
                       arg <- fromBuf b
                       pure (IApp fc fn arg)
               8 => do fc <- fromBuf b; fn <- fromBuf b
                       y <- fromBuf b; arg <- fromBuf b
                       pure (INamedApp fc fn y arg)
               9 => do fc <- fromBuf b; fn <- fromBuf b
                       arg <- fromBuf b
                       pure (IWithApp fc fn arg)
               10 => do fc <- fromBuf b; depth <- fromBuf b
                        pure (ISearch fc depth)
               11 => do fc <- fromBuf b; y <- fromBuf b
                        xs <- fromBuf b
                        pure (IAlternative fc y xs)
               12 => do fc <- fromBuf b; x <- fromBuf b; y <- fromBuf b
                        pure (IRewrite fc x y)
               13 => do fc <- fromBuf b; y <- fromBuf b
                        pure (ICoerced fc y)
               14 => do fc <- fromBuf b; m <- fromBuf b; y <- fromBuf b
                        pure (IBindHere fc m y)
               15 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IBindVar fc y)
               16 => do fc <- fromBuf b; nameFC <- fromBuf b
                        side <- fromBuf b;
                        y <- fromBuf b; pattern <- fromBuf b
                        pure (IAs fc nameFC side y pattern)
               17 => do fc <- fromBuf b
                        pattern <- fromBuf b
                        pure (IMustUnify fc UnknownDot pattern)

               18 => do fc <- fromBuf b; r <- fromBuf b
                        y <- fromBuf b
                        pure (IDelayed fc r y)
               19 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IDelay fc y)
               20 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IForce fc y)

               21 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IQuote fc y)
               22 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IQuoteName fc y)
               23 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IQuoteDecl fc y)
               24 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IUnquote fc y)
               25 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IRunElab fc y)

               26 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IPrimVal fc y)
               27 => do fc <- fromBuf b
                        pure (IType fc)
               28 => do fc <- fromBuf b; y <- fromBuf b
                        pure (IHole fc y)
               29 => do fc <- fromBuf b
                        i <- fromBuf b
                        pure (Implicit fc i)
               30 => do fc <- fromBuf b
                        ns <- fromBuf b
                        rhs <- fromBuf b
                        pure (IWithUnambigNames fc ns rhs)
               31 => do fc <- fromBuf b; fn <- fromBuf b
                        arg <- fromBuf b
                        pure (IAutoApp fc fn arg)
               _ => corrupt "RawImp"

  export
  TTC IFieldUpdate where
    toBuf b (ISetField p val)
        = do tag 0; toBuf b p; toBuf b val
    toBuf b (ISetFieldApp p val)
        = do tag 1; toBuf b p; toBuf b val

    fromBuf b
        = case !getTag of
               0 => do p <- fromBuf b; val <- fromBuf b
                       pure (ISetField p val)
               1 => do p <- fromBuf b; val <- fromBuf b
                       pure (ISetFieldApp p val)
               _ => corrupt "IFieldUpdate"

  export
  TTC BindMode where
    toBuf b (PI r) = do tag 0; toBuf b r
    toBuf b PATTERN = tag 1
    toBuf b NONE = tag 2

    fromBuf b
        = case !getTag of
               0 => do x <- fromBuf b
                       pure (PI x)
               1 => pure PATTERN
               2 => pure NONE
               _ => corrupt "BindMode"

  export
  TTC AltType where
    toBuf b FirstSuccess = tag 0
    toBuf b Unique = tag 1
    toBuf b (UniqueDefault x) = do tag 2; toBuf b x

    fromBuf b
        = case !getTag of
               0 => pure FirstSuccess
               1 => pure Unique
               2 => do x <- fromBuf b
                       pure (UniqueDefault x)
               _ => corrupt "AltType"

  export
  TTC ImpTy where
    toBuf b (MkImpTy fc nameFC n ty)
        = do toBuf b fc; toBuf b nameFC; toBuf b n; toBuf b ty
    fromBuf b
        = do fc <- fromBuf b; nameFC <- fromBuf b; n <- fromBuf b; ty <- fromBuf b
             pure (MkImpTy fc nameFC n ty)

  export
  TTC ImpClause where
    toBuf b (PatClause fc lhs rhs)
        = do tag 0; toBuf b fc; toBuf b lhs; toBuf b rhs
    toBuf b (ImpossibleClause fc lhs)
        = do tag 1; toBuf b fc; toBuf b lhs
    toBuf b (WithClause fc lhs wval prf flags cs)
        = do tag 2
             toBuf b fc
             toBuf b lhs
             toBuf b wval
             toBuf b prf
             toBuf b cs

    fromBuf b
        = case !getTag of
               0 => do fc <- fromBuf b; lhs <- fromBuf b;
                       rhs <- fromBuf b
                       pure (PatClause fc lhs rhs)
               1 => do fc <- fromBuf b; lhs <- fromBuf b;
                       pure (ImpossibleClause fc lhs)
               2 => do fc <- fromBuf b; lhs <- fromBuf b;
                       wval <- fromBuf b; prf <- fromBuf b;
                       cs <- fromBuf b
                       pure (WithClause fc lhs wval prf [] cs)
               _ => corrupt "ImpClause"

  export
  TTC DataOpt where
    toBuf b (SearchBy ns)
        = do tag 0; toBuf b ns
    toBuf b NoHints = tag 1
    toBuf b UniqueSearch = tag 2
    toBuf b External = tag 3
    toBuf b NoNewtype = tag 4

    fromBuf b
        = case !getTag of
               0 => do ns <- fromBuf b
                       pure (SearchBy ns)
               1 => pure NoHints
               2 => pure UniqueSearch
               3 => pure External
               4 => pure NoNewtype
               _ => corrupt "DataOpt"

  export
  TTC ImpData where
    toBuf b (MkImpData fc n tycon opts cons)
        = do tag 0; toBuf b fc; toBuf b n; toBuf b tycon; toBuf b opts
             toBuf b cons
    toBuf b (MkImpLater fc n tycon)
        = do tag 1; toBuf b fc; toBuf b n; toBuf b tycon

    fromBuf b
        = case !getTag of
               0 => do fc <- fromBuf b; n <- fromBuf b;
                       tycon <- fromBuf b; opts <- fromBuf b
                       cons <- fromBuf b
                       pure (MkImpData fc n tycon opts cons)
               1 => do fc <- fromBuf b; n <- fromBuf b;
                       tycon <- fromBuf b
                       pure (MkImpLater fc n tycon)
               _ => corrupt "ImpData"

  export
  TTC IField where
    toBuf b (MkIField fc c p n ty)
        = do toBuf b fc; toBuf b c; toBuf b p; toBuf b n; toBuf b ty

    fromBuf b
        = do fc <- fromBuf b; c <- fromBuf b; p <- fromBuf b
             n <- fromBuf b; ty <- fromBuf b
             pure (MkIField fc c p n ty)

  export
  TTC ImpRecord where
    toBuf b (MkImpRecord fc n ps con fs)
        = do toBuf b fc; toBuf b n; toBuf b ps; toBuf b con; toBuf b fs

    fromBuf b
        = do fc <- fromBuf b; n <- fromBuf b; ps <- fromBuf b
             con <- fromBuf b; fs <- fromBuf b
             pure (MkImpRecord fc n ps con fs)

  export
  TTC FnOpt where
    toBuf b Inline = tag 0
    toBuf b TCInline = tag 11
    toBuf b (Hint t) = do tag 1; toBuf b t
    toBuf b (GlobalHint t) = do tag 2; toBuf b t
    toBuf b ExternFn = tag 3
    toBuf b (ForeignFn cs) = do tag 4; toBuf b cs
    toBuf b Invertible = tag 5
    toBuf b (Totality Total) = tag 6
    toBuf b (Totality CoveringOnly) = tag 7
    toBuf b (Totality PartialOK) = tag 8
    toBuf b Macro = tag 9
    toBuf b (SpecArgs ns) = do tag 10; toBuf b ns

    fromBuf b
        = case !getTag of
               0 => pure Inline
               1 => do t <- fromBuf b; pure (Hint t)
               2 => do t <- fromBuf b; pure (GlobalHint t)
               3 => pure ExternFn
               4 => do cs <- fromBuf b; pure (ForeignFn cs)
               5 => pure Invertible
               6 => pure (Totality Total)
               7 => pure (Totality CoveringOnly)
               8 => pure (Totality PartialOK)
               9 => pure Macro
               10 => do ns <- fromBuf b; pure (SpecArgs ns)
               11 => pure TCInline
               _ => corrupt "FnOpt"

  export
  TTC ImpDecl where
    toBuf b (IClaim fc c vis xs d)
        = do tag 0; toBuf b fc; toBuf b c; toBuf b vis; toBuf b xs; toBuf b d
    toBuf b (IData fc vis d)
        = do tag 1; toBuf b fc; toBuf b vis; toBuf b d
    toBuf b (IDef fc n xs)
        = do tag 2; toBuf b fc; toBuf b n; toBuf b xs
    toBuf b (IParameters fc vis d)
        = do tag 3; toBuf b fc; toBuf b vis; toBuf b d
    toBuf b (IRecord fc ns vis r)
        = do tag 4; toBuf b fc; toBuf b ns; toBuf b vis; toBuf b r
    toBuf b (INamespace fc xs ds)
        = do tag 5; toBuf b fc; toBuf b xs; toBuf b ds
    toBuf b (ITransform fc n lhs rhs)
        = do tag 6; toBuf b fc; toBuf b n; toBuf b lhs; toBuf b rhs
    toBuf b (IRunElabDecl fc tm)
        = do tag 7; toBuf b fc; toBuf b tm
    toBuf b (IPragma _ f) = throw (InternalError "Can't write Pragma")
    toBuf b (ILog n)
        = do tag 8; toBuf b n
    toBuf b (IBuiltin fc type name)
        = do tag 9; toBuf b fc; toBuf b type; toBuf b name

    fromBuf b
        = case !getTag of
               0 => do fc <- fromBuf b; c <- fromBuf b
                       vis <- fromBuf b;
                       xs <- fromBuf b; d <- fromBuf b
                       pure (IClaim fc c vis xs d)
               1 => do fc <- fromBuf b; vis <- fromBuf b
                       d <- fromBuf b
                       pure (IData fc vis d)
               2 => do fc <- fromBuf b; n <- fromBuf b
                       xs <- fromBuf b
                       pure (IDef fc n xs)
               3 => do fc <- fromBuf b; vis <- fromBuf b
                       d <- fromBuf b
                       pure (IParameters fc vis d)
               4 => do fc <- fromBuf b; ns <- fromBuf b;
                       vis <- fromBuf b; r <- fromBuf b
                       pure (IRecord fc ns vis r)
               5 => do fc <- fromBuf b; xs <- fromBuf b
                       ds <- fromBuf b
                       pure (INamespace fc xs ds)
               6 => do fc <- fromBuf b; n <- fromBuf b
                       lhs <- fromBuf b; rhs <- fromBuf b
                       pure (ITransform fc n lhs rhs)
               7 => do fc <- fromBuf b; tm <- fromBuf b
                       pure (IRunElabDecl fc tm)
               8 => do n <- fromBuf b
                       pure (ILog n)
               9 => do fc <- fromBuf b
                       type <- fromBuf b
                       name <- fromBuf b
                       pure (IBuiltin fc type name)
               _ => corrupt "ImpDecl"

-- Log message with a RawImp
export
logRaw : {auto c : Ref Ctxt Defs} ->
         (s : String) ->
         {auto 0 _ : KnownTopic s} ->
         Nat -> Lazy String -> RawImp -> Core ()
logRaw str n msg tm
    = when !(logging str n) $
        do logString str n (msg ++ ": " ++ show tm)


text:
module rathivrunda.Odds

import Evens

import Intro

data IsOdd : Nat -> Type where
  OneOdd : IsOdd (S Z)
  SSOdd : (k: Nat)-> (IsOdd k) -> (IsOdd (S (S k)))

threeOdd : IsOdd 3
threeOdd = SSOdd (S Z) OneOdd

twoNotOdd: IsOdd 2 -> Void
twoNotOdd (SSOdd Z OneOdd) impossible
twoNotOdd (SSOdd Z (SSOdd _ _)) impossible

twoEven : IsEven 2
twoEven = SSEven 0 ZEven

SOddEven : (n: Nat) -> (IsOdd n) -> (IsEven (S n))
--SOddEven (S Z) (OneOdd) = twoEven
--SOddEven (S (S k)) (SSOdd k x) = SSEven (S k) (SOddEven k x)
SOddEven (S Z) OneOdd = SSEven 0 ZEven
SOddEven (S (S k)) (SSOdd k x) = SSEven (S k) (SOddEven k x)

SEvenOdd : (n: Nat) -> (IsEven n) -> (IsOdd (S n))
SEvenOdd Z(ZEven) =  (OneOdd)
SEvenOdd (S (S k)) (SSEven k x) = SSOdd (S k) (SEvenOdd k x)

nOddOrEven : (n: Nat) -> Either (IsEven n) (IsOdd n)
nOddOrEven Z = Left ZEven
nOddOrEven (S k) = case (nOddOrEven k) of
                       (Left l) => Right (SEvenOdd k l)
                       (Right r) => Left (SOddEven k r)

nNotBothOddEven : (n: Nat) -> (IsEven n) -> (IsOdd n) -> Void
nNotBothOddEven Z ZEven OneOdd impossible
nNotBothOddEven Z ZEven (SSOdd _ _) impossible
nNotBothOddEven (S (S k)) (SSEven k x) (SSOdd k y) = nNotBothOddEven k x y

SumEven : (n : Nat) -> (IsOdd n) -> (m :  Nat) -> (IsOdd m) -> (IsEven (add m n))
SumEven (S Z) OneOdd (S Z) OneOdd = twoEven
SumEven (S Z) OneOdd (S (S k)) (SSOdd k x) = SSEven (S k) (SOddEven k x)
SumEven (S (S k)) (SSOdd k x) m y = SSEven (add k m) SumEven k m

xyz : (f : Nat -> Nat) -> (n : Nat) -> (m : Nat) -> n = m -> f n = f m
xyz f m m (Refl {x = m}) = Refl {x = f m}

OddSdoubleEven : (n: Nat) -> IsOdd n -> (k: Nat ** S (double k) = n)
OddSdoubleEven (S Z) OneOdd = (Z ** Refl {x = 1})
OddSdoubleEven (S (S k)) (SSOdd k x) = step where
  step = case (OddSdoubleEven k x) of
            (m ** pf) => ((S m) ** xyz (\l => S (S l)) (S (double m)) k pf)

ext: idr


text:
module Printf

data Format = Number Format
            | Str Format
            | Lit Char Format  -- do we really need String literals?
            | Chr Format       -- from exercise 2
            | Dbl Format
            | End

total PrintfType : Format -> Type
PrintfType (Number fmt) = Int -> PrintfType fmt  -- NOTE: it would be nice if
                                                 -- we could specify
                                                 -- Num a => a -> PrintfType fmt
PrintfType (Str fmt) = String -> PrintfType fmt
PrintfType (Lit lit fmt) = PrintfType fmt
PrintfType End = String  -- teeechnically it should be IO ().
                         -- sprintf would have type ... -> String
PrintfType (Chr fmt) = Char -> PrintfType fmt
PrintfType (Dbl fmt) = Double -> PrintfType fmt

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ cast lit)
printfFmt End acc = acc
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ cast c)
printfFmt (Dbl fmt) acc = \d => printfFmt fmt (acc ++ show d)

toFormat : List Char -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: cs) = Number (toFormat cs)
toFormat ('%' :: 's' :: cs) = Str (toFormat cs)
toFormat ('%' :: 'c' :: cs) = Chr (toFormat cs)
toFormat ('%' :: 'f' :: cs) = Dbl (toFormat cs)
toFormat (c :: cs) = Lit c (toFormat cs)  -- sorry, I'm lazy

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

printfExample : String
printfExample = printf "%d %d      %%%%%%s" 10 2 "foo"

-- NOTEs:
-- Using Lit Char instead of Lit String made things easier when building
-- literals.  I'm curious about the efficiency though...

-- There's still a bit of dependency between format (PrintfType) and
-- toFormat.  For example there is no guarantee that toFormat
-- will produce a case for all possible Formats.
-- I wonder if there are languages where we can specify that a function
-- must be surjective.

-- Let's go back to Chapter6.idr

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module DatatypeGeneric

data Data : Type where
  Unit : Data
  Zero : Data
  Param : Data
  Rec : Data
  Sum : Data -> Data -> Data
  Prod : Data -> Data -> Data

interp : Data -> Type -> Type -> Type
interp Unit param rec = ()
interp Zero param rec = Void
interp Param param rec = param
interp Rec param rec = rec
interp (Sum x y) param rec = Either (interp x param rec) (interp y param rec)
interp (Prod x y) param rec = (interp x param rec, interp y param rec)

data Mu : (dataF : Data) -> (a : Type) -> Type where
  In : interp dataF a (Mu dataF a) -> Mu dataF a

bimap : (dataF : Data) -> (f : a -> b) -> (g : c -> d) -> interp dataF a c -> interp dataF b d
bimap Unit f g () = ()
bimap Param f g a = f a
bimap Rec f g c = g c
bimap (Sum x y) f g (Left l) = Left (bimap x f g l)
bimap (Sum x y) f g (Right r) = Right (bimap y f g r)
bimap (Prod x y) f g (a, b) = (bimap x f g a, bimap y f g b)

interface Representable (f : Type -> Type) where
  rep : Data
  fromRep : Mu rep a -> f a
  toRep : f a -> Mu rep a

Representable List where
  rep = Sum Unit (Prod Param Rec)

  fromRep (In (Left ())) = []
  fromRep (In (Right (a, b))) = a :: fromRep b

  toRep [] = In (Left ())
  toRep (x :: xs) = In (Right (x, toRep xs))

gmap : {dataF : Data} -> (a -> b) -> Mu dataF a -> Mu dataF b
gmap {dataF = dataF} f (In x) = In $ bimap dataF f (gmap f) x

gcata : {dataF : Data} -> (interp dataF a c -> c) -> Mu dataF a -> c
gcata {dataF = dataF} f (In x) = f $ bimap dataF id (gcata f) x

map' : Representable f => (a -> b) -> f a -> f b
map' f fa = fromRep $ gmap f (toRep fa)

test : List Int
test = map' (\x => x + 1) [1..10]

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Data.Sexp

import Data.List
import Data.String

%default total

public export
data Sexp : Type where
  SAtom : String -> Sexp
  SList : List Sexp -> Sexp

public export
interface ToSexp a where
  toSexp : a -> Sexp

public export
interface FromSexp a where
  fromSexp : Sexp -> Either String a

safeChar : Char -> Bool
safeChar c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_' || c == '-'

isSafe : String -> Bool
isSafe "" = False
isSafe s = let l = prim__strLength s in
               if l > 20 then False else
               go s l 0 where
                 go : String -> Int -> Int -> Bool
                 go s l i = if i >= l then True
                                      else safeChar (assert_total $ strIndex s i) && (assert_total $ go s l (i+1))

escapeChar : Char -> List Char
escapeChar '\n' = ['\\', 'n']
escapeChar '\t' = ['\\', 't']
escapeChar c = ('\\'::'{'::(unpack $ cast $ cast {to=Int} c)) ++ ['}']

safeCharInQuotes : Char -> Bool
safeCharInQuotes c = (c >= ' ' && c <= '~') && (c /= '\\') && (c /= '"')

safeShow : String -> String
safeShow s = fastPack ('"' :: reverse ('"' :: safeShow' (unpack s) []))
  where
    safeShow' : List Char -> List Char -> List Char
    safeShow' [] acc = acc
    safeShow' (c::rest) acc =
      if safeCharInQuotes c
         then safeShow' rest (c::acc)
         else safeShow' rest (reverseOnto acc (escapeChar c))

showSep : String -> List String -> String
showSep sep xs = showSepGo True xs "" where
  showSepGo : Bool -> List String -> String -> String
  showSepGo first [] acc = acc
  showSepGo first (x::xs) acc = if first then showSepGo False xs (acc ++ x)
                                         else showSepGo False xs (acc ++ " " ++ x)

export
Show Sexp where
  show (SAtom s) = if isSafe s then s else (safeShow s)
  show (SList xs) = "(" ++ (showSep " " (assert_total $ map show xs)) ++ ")"

export
unAtom : (errmsg : String) -> Sexp -> Either String String
unAtom _ (SAtom s) = Right s
unAtom m v = Left $ "expected an atom as " ++ m ++ ", got: " ++ show v

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Test

import Data.Vect
import System.File
import System
import Data.Buffer
import Data.String

test1 : Nat -> List String -> Vect n Int -> String
test1 1 (x :: xs) (y :: ys) = show 1 ++ show x ++ show xs ++ show y ++ show ys
test1 0 [] [x] = "m1 " ++ show x
test1 2 (x :: xs) (y :: []) = "m2 " ++ show x ++ show xs ++ show y
test1 (S k) d t = "m3 " ++ let x = test1 k (show k :: d) t in x
test1 k d t = "m4 " ++ show k ++ show d ++ show t

data MyDat = A1 | A2 | A3 | A4 | A5 | A6 | A7 | A8

Show MyDat where
   show A1 = "A1"
   show A2 = "A2"
   show A3 = "A3"
   show A4 = "A4"
   show A5 = "A5"
   show A6 = "A6"
   show A7 = "A7"
   show A8 = "A8"

ansiColorStr : String -> Vect 3 Int -> String
ansiColorStr str [r, g, b] = "\x1b[38;2;" ++ show r ++ ";" ++ show g ++ ";" ++ show b ++  "m" ++ str ++ "\x1b[0m"

namespace Either
   public export
   ignoreErr : (Show a) => IO (Either a b) -> IO b
   ignoreErr io =
      do
         (Right ok) <- io
            | Left err =>
                        do
                           putStrLn $ show err
                           exitFailure
         pure ok

namespace Maybe
   public export
   ignoreErr : IO (Maybe a) -> IO a
   ignoreErr io =
      do
         (Just ok) <- io
            | Nothing =>
                        do
                           putStrLn "Got nothing"
                           exitFailure
         pure ok

main : IO ()
main = do
   let aα = the Nat 5
   putStrLn $ show aα
   putStrLn $ test1 1 ["a", "b"] [2, 3, 4, 5]
   putStrLn $ test1 0 [] [6]
   putStrLn $ test1 2 ["c", "d", "e"] [1]
   putStrLn $ test1 3 ["p", "t"] [0]
   putStrLn $ test1 4 ["a"] [0, 1, 2, 3]
   putChar 'c'
   putChar 'b'
   putChar '\n'
   putStrLn $ show A1
   putStrLn $ show A8
   putStrLn $ show A6
   f <- ignoreErr $ openFile "data4.txt" Read
   putStrLn $ show !(fGetLine f)
   putStrLn $ show !(fEOF f)
   ignore $ fPutStrLn stdout "\x1b[38;2;255;100;0mThis is error\x1b[0m"
   ignore $ closeFile f
   ignore $ writeFile "data.txt" $ ansiColorStr "red\n" [255, 0, 0]
     ++ ansiColorStr "green\n" [0, 255, 0]
     ++ ansiColorStr "blue" [0, 0, 255]
   putStrLn $ show (the Int 257)
   putStrLn $ show !(ignoreErr $ readFile "data.txt")
   buf <- ignoreErr $ createBufferFromFile "data.txt"
   size <- rawSize buf
   putStrLn $ "buf size " ++ show size
   putStrLn $ "buf contents:\n" ++ !(getString buf 0 size)
   let i64s = 8
   ibuf <- ignoreErr $ newBuffer (i64s * 10)
   putStrLn $ "init size" ++ show !(rawSize ibuf)
   let list = [0..9]
   traverse_ (\i => do setInt ibuf (i64s * i) i;putStrLn $ "next size" ++ show !(rawSize ibuf)) list
   --setInt31 ibuf 114 (-991133)
   setInt ibuf 114 (-567)
   setDouble ibuf 122 (-241.123456789)
   setString ibuf 80 "hi there !"
   setString ibuf 90 "русский язык"
   dat2 <- ignoreErr $ openFile "data2.txt" WriteTruncate
   ignore $ writeBufferData dat2 ibuf 0 !(rawSize ibuf)
   putStrLn $ show $ !(getInt ibuf 0 )
   putStrLn $ show $ !(getInt ibuf 8 )
   putStrLn $ show $ !(getInt ibuf (8 * 9) )
   ignore $ closeFile dat2
   ibuf <- ignoreErr $ createBufferFromFile "data2.txt"
   putStrLn $ show $ !(getInt ibuf 0 )
   putStrLn $ show $ !(getInt ibuf 8 )
   putStrLn $ show $ !(getInt ibuf (8 * 9) )
   putStrLn $ show !(rawSize ibuf)
   putStrLn !(getString ibuf 80 10)
   putStrLn !(getString ibuf 90 24)
   putStrLn $ show !(getInt ibuf 114)
   putStrLn $ show !(getDouble ibuf 122)


text:
module Main

main : IO ()
main = do
  putStrLn $ "请输入第一个数字"
  x <- getLine
  putStrLn $ "请输入第二个数字"
  y <- getLine
  let z = cast x  + cast y

  putStrLn $ "两个数字之和为: " ++ (show z)


text:
module nattools

%default total

||| Make an isomorphism (of types) Nat to Nat<n + Nat >= n.

||| The natural numbers
--data Nat = Z  | S k

|||----------------------------------------------------------------------------
||| Nat < n.

||| Type of evidence for m < n.
||| Exists k:Nat where m+k+1=n.
data LTProof :  (m:Nat) -> (n:Nat) -> Type where
  MkLTProof : (m:Nat) -> (n:Nat) -> (k:Nat) -> plus m (S k) = n -> LTProof m n

|||-----------------------------------------------------------------------------
||| Nat >= n

||| Type of evidence for  m >= n.
||| Exists k where m = n + k.
data AtLeast : (m:Nat) -> (n:Nat) -> Type where
  MkAtLeast : (m:Nat) -> (n:Nat) -> (k:Nat) -> m = n+k -> AtLeast m n

|||-----------------------------------------------------------------------------
||| Nat -> Nat<n + Nat >= n

||| Type of evidence for  n < m xor m >= n
data SplitNatProof : (n:Nat) -> Type where
  Below : (n:Nat) -> (m:Nat) -> LTProof m n -> SplitNatProof n
  Above : (n:Nat) -> (m:Nat) -> AtLeast m n -> SplitNatProof n

||| have m+(S k)=n  and need (S m)+(S k)=S n
||| Cong {S} e : S ( m + (S k)) = S n  but need to rewrite, LHS.
||| Note, cong will implicitly find the S to apply to both sides by types it
||| has to match.
|||
||| by Plus associative we have (S m) + (S k)= S( m+ (S k))
||| we also have S(m+(S k))=S n
||| By transitivity we get (S m) + (S k) = S n
monotoneBelow : (m : Nat) -> (k : Nat) -> (e : plus m (S k) = n) -> plus (S m) (S k) = S n
monotoneBelow m k e = trans (plusAssociative 1 m (S k)) (cong e)

monotoneAbove : (n : Nat) -> (k : Nat) -> (e : m = (n + k)) -> S m = ((S n) + k)
monotoneAbove n k e = trans (cong e) Refl

monotoneSplit : SplitNatProof n -> SplitNatProof (S n)
monotoneSplit (Below n m (MkLTProof m n k e))  = Below (S n) (S m) (MkLTProof (S m) (S n) k (monotoneBelow m k e))
monotoneSplit (Above n m (MkAtLeast m n k e))  = Above (S n) (S m) (MkAtLeast (S m) (S n) k (monotoneAbove n k e))

||| Split Lemma: For every m:Nat every n:Nat, m < n or m >= n, exclussively
natsSplit : (n:Nat) -> (m:Nat) -> SplitNatProof n
natsSplit Z m = Above 0 m (MkAtLeast m 0 m Refl)
natsSplit (S k) Z = Below (S k) Z (MkLTProof 0  (S k) k Refl)
natsSplit (S k) (S j) = let x = natsSplit k j in (monotoneSplit x)

|||-----------------------------------------------------------------------------
||| Now the isomorphisms, what actually do things.

split : (n:Nat) -> Nat -> DPair Nat (\k=>SplitNatProof n)
split n m = (m**(natsSplit n m))

join : (n:Nat) -> DPair Nat (\k=>SplitNatProof k) -> Nat
join n (m**e) = m

--------------------------------------------------------------------------------
--- TODO: prove these are isomorphisms
--- I.e. join n split n m = m and split n join n x = x

max_stars_repo_name: algeboy/FormalAlgebra

max_issues_repo_name: algeboy/FormalAlgebra

max_forks_repo_name: algeboy/FormalAlgebra


text:
module Main

import Data.Vect

%default total

data Ty = TyBool | TyInt | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyBool = Bool
interpTy TyInt = Integer
interpTy (TyFun a b) = interpTy a -> interpTy b

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
  Stop : HasType FZ (t :: ctx) t
  Pop : HasType k ctx t -> HasType (FS k) (u :: ctx) t

data Expr : Vect n Ty -> Ty -> Type where
  Var : HasType i ctx t -> Expr ctx t
  Val : (x : Integer) -> Expr ctx TyInt
  Lam : Expr (a :: ctx) t -> Expr ctx (TyFun a t)
  App : Expr ctx (TyFun a t) -> Expr ctx a -> Expr ctx t
  Op : (interpTy a -> interpTy b -> interpTy c) -> Expr ctx a -> Expr ctx b -> Expr ctx c
  If : Expr ctx TyBool -> Lazy (Expr ctx a) -> Lazy (Expr ctx a) -> Expr ctx a

data Env : Vect n Ty -> Type where
  Nil : Env Nil
  (::) : interpTy a -> Env ctx -> Env (a :: ctx)

lookup : HasType i ctx t -> Env ctx -> interpTy t
lookup Stop (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

interp : Env ctx -> Expr ctx t -> interpTy t
interp env (Var i) = lookup i env
interp env (Val n) = n
interp env (Lam sc) = \x => interp (x :: env) sc
interp env (App f s) = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e) = if interp env x then interp env t
                                        else interp env e

add : Expr ctx (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

partial
fac : Expr ctx (TyFun TyInt TyInt)
fac = Lam (If (Op (==) (Var Stop) (Val 0))
              (Val 1)
              (Op (*) (App fac (Op (-) (Var Stop) (Val 1)))
                      (Var Stop)))

partial
main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          printLn (interp [] fac (cast x))

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Idris.IDEMode.Holes

import Core.Env
import Core.Context.Log

import Idris.Resugar
import Idris.Syntax
import Idris.Pretty

import Idris.IDEMode.Commands

import Libraries.Data.String.Extra as L
import Libraries.Utils.Term

%default covering

public export
record HolePremise where
  constructor MkHolePremise
  name         : Name
  type         : IPTerm
  multiplicity : RigCount
  isImplicit   : Bool

public export
record HoleData where
  constructor MkHoleData
  name : Name
  type : IPTerm
  context : List HolePremise

||| If input is a hole, return number of locals in scope at binding
||| point
export
isHole : GlobalDef -> Maybe Nat
isHole def
    = case definition def of
           Hole locs _ => Just locs
           PMDef pi _ _ _ _ =>
                 case holeInfo pi of
                      NotHole => Nothing
                      SolvedHole n => Just n
           None => Just 0
           _ => Nothing

-- Bring these back into REPL.idr
showName : Name -> Bool
showName (UN Underscore) = False
showName (MN _ _) = False
showName _ = True

impBracket : Bool -> String -> String
impBracket False str = str
impBracket True str = "{" ++ str ++ "}"

prettyImpBracket : Bool -> Doc ann -> Doc ann
prettyImpBracket False = id
prettyImpBracket True = braces

tidy : Name -> String
tidy (MN n _) = n
tidy n = show n

prettyName : Name -> Doc ann
prettyName (MN n _) = pretty n
prettyName n = pretty n

export
extractHoleData : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
          Core HoleData
extractHoleData defs env fn (S args) (Bind fc x (Let _ c val ty) sc)
  = extractHoleData defs env fn args (subst val sc)
extractHoleData defs env fn (S args) (Bind fc x b sc)
  = do rest <- extractHoleData defs (b :: env) fn args sc
       let True = showName x
         | False => do log "idemode.hole" 10 $ "Not showing name: " ++ show x
                       pure rest
       log "idemode.hole" 10 $ "Showing name: " ++ show x
       ity <- resugar env !(normalise defs env (binderType b))
       let premise = MkHolePremise x ity (multiplicity b) (isImplicit b)
       pure $ record { context $= (premise ::)  } rest
extractHoleData defs env fn args ty
  = do nty <- normalise defs env ty
       ity <- resugar env nty
       log "idemode.hole" 20 $
          "Return type: " ++ show !(toFullNames ty)
          ++ "\n  Evaluated to: " ++ show !(toFullNames nty)
          ++ "\n  Resugared to: " ++ show ity
       pure $ MkHoleData fn ity []

export
holeData : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           Defs -> Env Term vars -> Name -> Nat -> Term vars ->
           Core HoleData

holeData gam env fn args ty
  = do hdata <- extractHoleData gam env fn args ty
       pp <- getPPrint
       pure $ if showImplicits pp
              then hdata
              else record { context $= dropShadows } hdata
  where
    dropShadows : List HolePremise -> List HolePremise
    dropShadows [] = []
    dropShadows (premise :: rest)
        = if premise.name `elem` map name rest
             then            dropShadows rest
             else premise :: dropShadows rest

export
showHole : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          Defs -> Env Term vars -> Name -> Nat -> Term vars ->
          Core String
showHole defs env fn args ty
    = do hdata <- holeData defs env fn args ty
         case hdata.context of
           [] => pure $ show (hdata.name) ++ " : " ++ show hdata.type
           _  => pure $ concat
              (map (\premise => " " ++ showCount premise.multiplicity ++ " "
                             ++ (impBracket premise.isImplicit $
                                 tidy premise.name ++ " : " ++ (show premise.type) ++ "\n" )
                   ) hdata.context)
              ++ "-------------------------------------\n"
              ++ nameRoot (hdata.name) ++ " : " ++ show hdata.type

export
prettyRigHole : RigCount -> Doc ann
prettyRigHole = elimSemi (pretty '0' <+> space)
                         (pretty '1' <+> space)
                         (const $ space <+> space)

export
prettyHole : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             Defs -> Env Term vars -> Name -> Nat -> Term vars ->
             Core (Doc IdrisSyntax)
prettyHole defs env fn args ty
  = do hdata <- holeData defs env fn args ty
       case hdata.context of
            [] => pure $ pretty hdata.name <++> colon <++> prettyTerm hdata.type
            _  => pure $ (indent 1 $ vsep $
                            map (\premise => prettyRigHole premise.multiplicity
                                    <+> prettyImpBracket premise.isImplicit (prettyName premise.name <++> colon <++> prettyTerm premise.type))
                                    hdata.context) <+> hardline
                    <+> (pretty $ L.replicate 30 '-') <+> hardline
                    <+> pretty (nameRoot $ hdata.name) <++> colon <++> prettyTerm hdata.type

sexpPremise : HolePremise -> SExp
sexpPremise premise =
  SExpList [StringAtom $ " " ++ showCount premise.multiplicity ++ " "
                       ++ (impBracket premise.isImplicit $
                           tidy premise.name)
           ,StringAtom $ show premise.type
           ,SExpList [] -- TODO: metadata
           ]

export
sexpHole : HoleData -> SExp
sexpHole hole = SExpList
  [ StringAtom (show  hole.name)
  , SExpList $ map sexpPremise hole.context  -- Premises
  , SExpList [ StringAtom $ show hole.type   -- Conclusion
             , SExpList[]]    -- TODO: Highlighting information
  ]


text:
module Circuits.Idealised.Types

import Decidable.Equality

import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Renaming

import public Circuits.Common

%default total

public export
data GateKind = AND  | IOR  | XOR
              | ANDN | IORN | XORN | JOIN

public export
data Direction = INPUT | OUTPUT

Uninhabited (INPUT = OUTPUT) where
  uninhabited Refl impossible

DecEq Direction where
  decEq INPUT INPUT   = Yes Refl
  decEq INPUT OUTPUT  = No absurd
  decEq OUTPUT INPUT  = No (negEqSym absurd)
  decEq OUTPUT OUTPUT = Yes Refl

public export
data PortHasProperties : Direction -> DType -> (Direction, DType) -> Type
  where
    PortHas : PortHasProperties flow type (flow,type)

public export
data Ty : Type where
  TyUnit : Ty
  TyPort : (Direction, DType) -> Ty

  TyGate : Ty

Uninhabited (TyUnit = (TyPort x)) where
  uninhabited Refl impossible

Uninhabited (TyUnit = TyGate) where
  uninhabited Refl impossible

Uninhabited (TyPort x = TyGate) where
  uninhabited Refl impossible

export
DecEq Ty where
  decEq TyUnit TyUnit = Yes Refl
  decEq TyUnit (TyPort x) = No absurd
  decEq TyUnit TyGate = No absurd

  decEq (TyPort x) TyUnit = No (negEqSym absurd)
  decEq (TyPort x) (TyPort y) with (decEq x y)
    decEq (TyPort x) (TyPort x) | (Yes Refl)
      = Yes Refl
    decEq (TyPort x) (TyPort y) | (No contra)
      = No (\Refl => contra Refl)
  decEq (TyPort x) TyGate = No (absurd)

  decEq TyGate TyUnit = No (negEqSym absurd)
  decEq TyGate (TyPort x) = No (negEqSym absurd)
  decEq TyGate TyGate = Yes Refl

public export
data Used : (Ty, Usage) -> Type where
  IsUsed : Used (type, USED)

export
Uninhabited (Used (type,FREE)) where
  uninhabited IsUsed impossible

export
used : (p : (Ty,Usage)) -> Dec (Used p)
used (ty,USED) = Yes IsUsed
used (ty,FREE) = No absurd

public export
data Use : (old : List (Ty, Usage))
        -> (prf : IsVar old (type,FREE))
        -> (new : List (Ty, Usage))
        -> Type
  where
    H : Use ((type,FREE) :: rest)
            (V Z Here)
            ((type,USED) :: rest)

    T : Use old (V n later) new
     -> Use ((type',usage')::old)
            (V (S n) (There later))
            ((type',usage')::new)

Uninhabited (IsVar Nil type) where
  uninhabited (V _ Here) impossible
  uninhabited (V _ (There later)) impossible

Uninhabited (AtIndex type Nil pos) where
  uninhabited Here impossible
  uninhabited (There later) impossible

export
use : {ctxt : List (Ty, Usage)}
   -> (prf  : IsVar ctxt (type, FREE))
           -> (DPair (List (Ty, Usage))
                     (Use ctxt prf))
use {ctxt = Nil} (V _ Here) impossible
use {ctxt = ((type, FREE) :: xs)} (V 0 Here)
  = MkDPair ((type, USED) :: xs) H

use {ctxt = (y :: rest)} (V (S idx) (There later)) with (use (V idx later))
  use {ctxt = ((t,u) :: rest)} (V (S idx) (There later)) | (MkDPair fst snd)
    = MkDPair ((t,u) :: fst) (T snd)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
hours : List Nat
hours = [1..12]

nats : Stream Nat
nats = [0,1..]


text:
module IdrisWeb.CGI.Cgi

-- CGI Module, making use of the Effects DSL.
-- large amount of credit goes to the author of Network.Cgi.
-- SimonJF

import Effects
import IdrisWeb.CGI.CgiTypes
import IdrisWeb.CGI.CgiUtils
import SimpleParser
import Decidable.Equality
import IdrisWeb.DB.SQLite.SQLiteNew
import IdrisWeb.Session.Session
import Debug.Trace
%access public -- for now
-- %default total

-- Syntax macro, so that users don't have to bother with dependent pairs, etc.
syntax "handler args=" [args] ", effects=" [effs] ", fn=" [fn] ", name=" [name] = ((args, effs) ** (fn, name))

-- Bit of a hack for now, until I can get it so that the user doesn't
-- have to type this
initCGIState : (InitialisedCGI TaskRunning)
initCGIState = ICgi (CGIInf [] [] [] "" "" "" Z)

showFormVal : (fty : FormTy) -> interpFormTy fty -> String
showFormVal FormString s = s
showFormVal FormInt i = show i
showFormVal FormBool b = show b
showFormVal FormFloat f = show f
-- FIXME: extra comma...
showFormVal (FormList t) vs = "[" ++ (foldr (\v, str => (showFormVal t v) ++ "," ++ str) "" vs) ++ "]"
--  where showListElem : (fty' : FormTy) -> interpFormTy fty' -> String
  --      showListElem ft v =

serialiseSubmit : String ->
                  List FormTy ->
                  List WebEffect ->
                  String
serialiseSubmit name tys effs = "<input type=\"hidden\" name=\"handler\" value=\"" ++ name ++ "." ++
                                     serialised_tys ++ "." ++ serialised_effs ++ ".\"></input>" ++
                                    "<input type=\"submit\"></input></form>"
  where serialised_tys = foldr (\ty, str => str ++ (show ty) ++ "-") "" tys
        serialised_effs = foldr (\eff, str => str ++ (show eff) ++ "-") "" (reverse effs)

val_opts : (fty : FormTy) -> (Vect n (interpFormTy fty)) -> Vect n String -> String
val_opts fty [] [] = ""
val_opts fty (val :: vals) (name :: names) = "<option value=\"" ++ (showFormVal fty val) ++ "\">"
                                             ++ name ++ "</option>\n" ++ (val_opts fty vals names)
-- = foldr (\val, b => ("<option value=\"" ++ (showFormVal val) ++ "\">" ++ )

makeSelectBox : String -> (fty : FormTy) -> (Vect n (interpFormTy fty)) -> (Vect n String) -> String
makeSelectBox name fty vals val_names = select ++ (val_opts fty vals val_names) ++ "</select>
"
  where select = "<select name=\"" ++ name ++ "\">\n"

-- TODO: The Int thing is pretty hacky, fix
makeRadioGroup : String -> (fty : FormTy) -> (Vect n (interpFormTy fty)) -> (Vect n String) -> Int -> String
makeRadioGroup _ _ [] [] _ = ""
makeRadioGroup name fty (val :: vals) (val_name :: val_names) k =  "<input type=\"radio\" name=\"" ++
                                                                   name ++
                                                                   "\" value=\"" ++
                                                                   (showFormVal fty val) ++
                                                                   (if k == 0 then "\" checked>" else "\">") ++
                                                                   val_name ++ "
" ++
                                                                   makeRadioGroup name fty vals val_names (k - 1)

makeCheckBoxes : String -> (fty : FormTy) -> (Vect n (interpFormTy fty)) -> (Vect n String) -> (Vect n Bool) -> String
makeCheckBoxes _ _ [] [] _ = ""
makeCheckBoxes name fty (val :: vals) (val_name :: val_names) (is_checked :: checklist) =
                                                                   "<input type=\"checkbox\" name=\"" ++
                                                                   name ++
                                                                   "\" value=\"" ++
                                                                   (showFormVal fty val) ++
                                                                   (if is_checked then "\" checked>" else "\">") ++
                                                                   val_name ++ "
" ++
                                                                   makeCheckBoxes name fty vals val_names checklist

getDefValStr : (fty : FormTy) -> Maybe (interpFormTy fty) -> String
getDefValStr ty (Just val) = "value=\"" ++ (showFormVal ty val) ++ "\" "
getDefValStr ty Nothing = ""

instance Handler Form m where
-- Submit
  handle (FR len tys effs ser_str) (Submit fn name) k =
    k (FR Z [] [] ser_str) (ser_str ++ "
	" ++ (serialiseSubmit name tys effs) ++ "

")
-- Text box
  handle (FR len tys effs ser_str) (AddTextBox label fty def_val) k =
    k (FR (S len) (fty :: tys)
      effs (ser_str ++ "
" ++ label ++ "	<input name=\"inp" ++ (show len) ++ "\" " ++ (getDefValStr fty def_val) ++ "\"></input>
\n")) ()
-- Hidden field
  handle (FR len tys effs ser_str) (AddHidden fty val) k =
    k (FR (S len) (fty :: tys)
      effs (ser_str ++ "<input type=\"hidden\" name=\"inp" ++ (show len) ++ "\" value=\"" ++ (showFormVal fty val) ++ "\"></input>
\n")) ()
-- Dropdown selection box
  handle (FR len tys effs ser_str) (AddSelectionBox label fty opts names) k =
    k (FR (S len) (fty :: tys)
      effs (ser_str ++ "
" ++ label ++ "	" ++ (makeSelectBox ("inp" ++ (show len)) fty opts names) ++ "
\n")) ()
-- Radio button group
  handle (FR len tys effs ser_str) (AddRadioGroup label fty opts names default) k =
    k (FR (S len) (fty :: tys)
      effs (ser_str ++ "
" ++ label ++ "	" ++ (makeRadioGroup ("inp" ++ (show len)) fty opts names default) ++ "
\n" )) ()
-- Check boxes
  handle (FR len tys effs ser_str) (AddCheckBoxes label fty opts names checked) k =
    k (FR (S len) ((FormList fty) :: tys) effs
      (ser_str ++ "
" ++ label ++ "	" ++ (makeCheckBoxes ("inp" ++ (show len)) fty opts names checked) ++ "
\n" )) ()
    -- <input type="text" name="inpx" value="val">
-- Set effects
  handle (FR len tys _ ser_str) (UseEffects effs) k =
     k (FR len tys effs ser_str) ()

{- Form handling stuff -}
-- Gets the serialised value as the given type, if it's possible
--total
%assert_total
parseSerialisedValue : (ty : FormTy) -> String -> Maybe (interpFormTy ty)
parseSerialisedValue FormString val = Just val
parseSerialisedValue FormInt val = case parse int val of
                                        Left err => Nothing
                                        Right (i, _) => Just i
parseSerialisedValue FormBool val = case parse bool val of
                                         Left err => Nothing
                                         Right (b, _) => Just b
-- FIXME: Placeholder for now, todo: improve parser
parseSerialisedValue FormFloat val = Just 0.0
parseSerialisedValue (FormList x) val = Nothing -- My head's aching, recursion unsupported now!

getAs : (ty : FormTy) -> Int -> List (String, String) -> Maybe (interpFormTy ty)
getAs (FormList ty) n args = do let vals = filter (\(argname, _) => argname == ("inp" ++ (show n))) args
                                Just $ catMaybes $ map (\(_, x) => parseSerialisedValue ty x) vals
getAs ty n args = do val <- lookup ("inp" ++ (show n)) args
                     parseSerialisedValue ty val

-- Disregards args
public
mkFinalHandlerType : MkHandlerFnTy -> Type
mkFinalHandlerType (_, effs) = FormHandler (interpWebEffects effs)

getWebEnv' : (effs : List WebEffect) -> (InitialisedCGI TaskRunning) -> Effects.Env IO (interpWebEffects effs)
-- Def later

evalFn : (mkHTy : MkHandlerFnTy) ->
         (counter : Int) -> -- TODO: ftys would be far better as a Vect over some finite set indexed over n
         (args : List (String, String)) ->
         (fn : mkHandlerFn mkHTy) ->
         (InitialisedCGI TaskRunning) ->
         (mkFinalHandlerType mkHTy, PopFn)
evalFn (Prelude.List.Nil, effs) counter args fn cgi = (fn,
         (PF effs (interpWebEffects effs) (getWebEnv' effs cgi) fn))-- ?mv -- Just (fn, )
evalFn ((fty :: ftys), effs) counter args fn cgi =
  let arg = getAs fty counter args in
    evalFn (ftys, effs) (counter + 1) args (fn arg) cgi

{- Parser functions to grab arguments from a form -}
strFty : List (String, FormTy)
strFty = [("str", FormString), ("int", FormInt), ("bool", FormBool), ("float", FormFloat)]

strEff : List (String, WebEffect)
strEff = [("cgi", CgiEffect), ("sqlite", SqliteEffect), ("session", SessionEffect)]

arg : Parser FormTy
arg = do a_str <- strToken
         char '-'
         case lookup a_str strFty of
              Just fty => pure fty
              Nothing  => failure $ "Attempted to deserialise nonexistent function type " ++ a_str

ty_list : Parser FormTy
ty_list = nested_list <|> arg
 where nested_list : Parser FormTy
       nested_list = do string "list_"
                        xs <- ty_list
                        pure (FormList xs)

{-
ty_list : Parser FormTy
ty_list = do string "list_"
             a <- arg
             pure (FormList a)
-}

webEff : Parser WebEffect
webEff = do e_str <- strToken
            char '-'
            case lookup e_str strEff of
                 Just w_eff => pure w_eff
                 Nothing => failure $ "Attempted to deserialise nonexistent web effect " ++ e_str

parseFormFn' : Parser (String, MkHandlerFnTy)
parseFormFn' = do name <- strToken
                  char '.'
                  args <- many (arg <|> ty_list)
                  char '.' -- List delimiter
                  effs <- many webEff
                  pure (name, (args, effs))

-- The hidden field "handler" will be of the form:
-- <handler name>:type1;type2...typen;:<effects, eventually>
parseFormFn : String -> Maybe (String, MkHandlerFnTy)
parseFormFn str = case parse parseFormFn' str of
                       Left err => Nothing
                       Right ((name, parsed_fn), _) => Just (name, parsed_fn)

checkFunctions : (reg_fn_ty : MkHandlerFnTy) ->
                 (frm_fn_ty : MkHandlerFnTy) ->
                 mkHandlerFn reg_fn_ty ->
                 Maybe (mkHandlerFn frm_fn_ty)
checkFunctions reg_ty frm_ty reg_fn with (decEq reg_ty frm_ty)
  checkFunctions frm_ty frm_ty reg_fn | Yes refl = Just reg_fn
  checkFunctions reg_ty frm_ty reg_fn | No _ = Nothing

lookupHandler : String -> HandlerList -> Maybe HandlerFn
lookupHandler _ [] = Nothing
lookupHandler name ((ft ** (fn, fn_name))::fns) = if name == fn_name then (Just (ft ** (fn, fn_name)))
                                                              else lookupHandler name fns

-- Takes in a list of form POST / GET vars, a list of available handlers, and returns the appropriate handler
getHandler : List (String, String) ->
             (handler_name : String) ->
             (handler_ty : MkHandlerFnTy) ->
             HandlerList ->
             (InitialisedCGI TaskRunning) ->
             Maybe (mkFinalHandlerType handler_ty, PopFn)
getHandler vars handler_name handler_type handlers cgi = do
                              (ft ** (fn, fn_name)) <- lookupHandler handler_name handlers
                              rh_fn' <- checkFunctions ft handler_type fn
                              --let f_rh = (RH handler_type rh_fn')
                              --let (tys, effs) = handler_type
                              Just $ evalFn handler_type 0 vars rh_fn' cgi

inspectFinalEnv : (effs : List EFFECT) -> Env IO effs -> (InitialisedCGI TaskRunning) -> (InitialisedCGI TaskRunning)
inspectFinalEnv _ [] def = def
inspectFinalEnv ((CGI (InitialisedCGI TaskRunning)) :: effs) ((ICgi st) :: vals) def = (ICgi st)
inspectFinalEnv (_ :: effs) (_ :: vals) def = inspectFinalEnv effs vals def

--Eff IO
addOutput : String -> CGIInfo -> CGIInfo
-- TODO: GetEnv on the CGI
executeHandler : List (String, String) ->
                 HandlerList ->
                 (InitialisedCGI TaskRunning) ->
                 IO (InitialisedCGI TaskRunning, Bool)
executeHandler vars handlers cgi = case (lookup "handler" vars) >>= parseFormFn of
                                      Just (name, frm_ty) => case getHandler vars name frm_ty handlers cgi of
                                        Just (fn, (PF effs conc_effs env fn')) => do (env', res) <- runEnv env fn'
                                                                                let cgi' = inspectFinalEnv conc_effs env' cgi
                                                                                pure (cgi', True)
                                        Nothing => do let (ICgi st) = cgi
                                                      let cgi' = (addOutput "Found handler field; could not execute" st)
                                                      pure ((ICgi cgi'), False)
                                      Nothing => do let (ICgi st) = cgi
                                                    let cgi' = (addOutput "Could not find handler in vars / could not parse" st)
                                                    pure ((ICgi cgi'), False)

-- TODO: Action, also ideally we should have encoding/decoding instead of using text/plain
mkForm : Nat -> UserForm -> SerialisedForm
mkForm num frm = runPure [FR Z [] [] ("
<form name=\"" ++ (show num) ++
                         "\" action=\"\" method=\"post\">\n")] frm

-- In handle, then match on (ICGI s) to get access to state
-- State mutation functions, allowing for addition of headers / output
addHeaders : String -> CGIInfo -> CGIInfo
addHeaders str st = record { Headers = Headers st ++ str ++ "\r\n" } st

--addOutput : String -> CGIInfo -> CGIInfo
addOutput str st = record { Output = Output st ++ str } st

incrementFormCount : CGIInfo -> CGIInfo
incrementFormCount st = record { FormNumber = FormNumber st + 1} st
-- To create a CGI Program in Network.Cgi, one imports Network.Cgi,
-- and then creates a function CGIInfo -> IO (a, CGIInfo)) which is passed
-- into MkCGI.

-- This produces a complete CGI program, which can then be executed with
-- the required arguments.

-- For the implementation of CGI in the effects language, we'll want users
-- to be able to specify some function to be run inside the CGI effect.

-- This will take the form Eff IO [CGI] a, or more simply
-- CGIEff a.

-- Several CGI functions will also require access to the state, and some will require
-- access to the environment variables.

abstract
runAction : Env IO (CGI (InitialisedCGI TaskRunning) :: effs) -> CGIProg effs a -> Eff m [CGI (InitialisedCGI TaskRunning)] a
runAction init_env act = (RunAction init_env act)

getInfo : Eff m [CGI (InitialisedCGI TaskRunning)] CGIInfo
getInfo = GetInfo

abstract
getGETVars : Eff m [CGI (InitialisedCGI TaskRunning)] Vars
getGETVars = GETVars

abstract
getPOSTVars : Eff m [CGI (InitialisedCGI TaskRunning)] Vars
getPOSTVars = POSTVars

abstract
getCookieVars : Eff m [CGI (InitialisedCGI TaskRunning)] Vars
getCookieVars = CookieVars

abstract
queryGetVar : String -> Eff m [CGI (InitialisedCGI TaskRunning)] (Maybe String)
queryGetVar query = (QueryGetVar query)

abstract
queryCookieVar : String -> Eff m [CGI (InitialisedCGI TaskRunning)] (Maybe String)
queryCookieVar query = (QueryCookieVar query)

abstract
queryPostVar : String -> Eff m [CGI (InitialisedCGI TaskRunning)] (Maybe String)
queryPostVar query = (QueryPostVar query)

getOutput : Eff m [CGI (InitialisedCGI TaskRunning)] String
getOutput = GetOutput

getHeaders : Eff m [CGI (InitialisedCGI TaskRunning)] String
getHeaders = GetHeaders

abstract
flushHeaders : Eff m [CGI (InitialisedCGI TaskRunning)] ()
flushHeaders = FlushHeaders

abstract
flush : Eff m [CGI (InitialisedCGI TaskRunning)] ()
flush = Flush

initialise : EffM m [CGI ()] [CGI (InitialisedCGI Initialised)] ()
initialise = Init

startTask : EffM m [CGI (InitialisedCGI Initialised)] [CGI (InitialisedCGI TaskRunning)] ()
startTask = StartRun

finishTask : EffM m [CGI (InitialisedCGI TaskRunning)] [CGI (InitialisedCGI TaskCompleted)] ()
finishTask = FinishRun

writeHeaders : EffM m [CGI (InitialisedCGI TaskCompleted)] [CGI (InitialisedCGI HeadersWritten)] ()
writeHeaders = WriteHeaders

writeContent : EffM m [CGI (InitialisedCGI HeadersWritten)] [CGI (InitialisedCGI ContentWritten)] ()
writeContent = WriteContent

abstract
setCookie : String -> String -> Eff m [CGI (InitialisedCGI TaskRunning)] ()
setCookie name val = (SetCookie name val)

public
output : String -> Eff m [CGI (InitialisedCGI TaskRunning)] ()
output s = (OutputData s)

abstract
addForm : UserForm -> Eff m [CGI (InitialisedCGI TaskRunning)] ()
addForm form = (AddForm form)

abstract
handleForm : HandlerList -> Eff m [CGI (InitialisedCGI TaskRunning)] Bool
handleForm handlers = (HandleForm handlers)

-- Handler for CGI in the IO context
instance Handler Cgi IO where
  --handle (ICgi st) GetInfo k = k (ICgi st) (CgiInfo st)

  handle (ICgi st) GETVars k = k (ICgi st) (GET st)

  handle (ICgi st) POSTVars k = k (ICgi st) (POST st)

  handle (ICgi st) CookieVars k = k (ICgi st) (Cookies st)

  handle (ICgi st) (QueryGetVar q) k = k (ICgi st) (lookup q (GET st))

  handle (ICgi st) (QueryPostVar q) k = k (ICgi st) (lookup q (POST st))

  handle (ICgi st) (QueryCookieVar q) k = k (ICgi st) (lookup q (Cookies st))

  handle (ICgi st) GetOutput k = k (ICgi st) (Output st)

  handle (ICgi st) GetHeaders k = k (ICgi st) (Headers st)

  -- Should this also clear them from the state? It doesn't in the Network.Cgi imp
  -- but seems logical
  handle (ICgi st) FlushHeaders k = do putStrLn (Headers st)
                                       k (ICgi st) ()

  -- These two are purely to transition states, so we don't need to do anything
  handle (ICgi st) StartRun k = k (ICgi st) ()
  handle (ICgi st) FinishRun k = k (ICgi st) ()

  -- Handle writing out headers and content
  handle (ICgi st) WriteHeaders k = do putStr (Headers st)
                                       putStr "\r\n"
                                       k (ICgi st) ()

  -- Handle writing out headers and content
  handle (ICgi st) WriteContent  k = do --putStrLn ("OC: " ++ s)
                                         putStrLn (Output st)
                                         k (ICgi st) ()

  handle (ICgi st) Flush k = do putStrLn (Output st)
                                k (ICgi st) ()

  -- Get the variables from the environment
  handle () Init k = do
    query   <- safeGetEnvVar "QUERY_STRING"
    cookie  <- safeGetEnvVar "HTTP_COOKIE"
    agent   <- safeGetEnvVar "HTTP_USER_AGENT"
    content <- getContent
    let get_vars  = getVars ['&',';'] query
    let post_vars = getVars ['&'] content -- TODO: plain/text encoding
    let cookies   = getVars [';'] cookie

    let cgi_info = (CGIInf get_vars post_vars cookies agent
                    "Content-type: text/html\n" "" Z)
    k (ICgi cgi_info) ()

  handle (ICgi st) (OutputData s) k  = do let new_cgi_info = addOutput s st
                                          k (ICgi new_cgi_info) ()

-- TODO: don't hardcode date :P #lazyintern
  handle (ICgi st) (SetCookie name val) k = do let set_cookie_header = ("Set-Cookie: " ++
                                                name ++ "=" ++ val ++
                                                "; Expires=Thu, 26 Jun 2014 10:00:00 GMT")
                                               let new_info = addHeaders set_cookie_header st
                                               k (ICgi new_info) ()

  handle (ICgi st) (RunAction ((ICgi _) :: env) act) k = do (((ICgi st') :: env'), result) <- runEnv ((ICgi st) :: env) act
                                                            k (ICgi st') result

  handle (ICgi st) (AddForm form) k = k (ICgi $ incrementFormCount $ addOutput (mkForm (FormNumber st) form) st) ()

  -- TODO: allow GET vars
  handle (ICgi st) (HandleForm handlers) k = do let post_vars = POST st
                                                (cgi', res) <- executeHandler post_vars handlers (ICgi st)
                                                k cgi' res

-- Internal mechanism to run the user-specified action
private
runCGI' : Env IO ((CGI (InitialisedCGI TaskRunning)) :: effs) ->
          CGIProg effs a ->
          EffM IO [CGI ()] [CGI (InitialisedCGI ContentWritten)] a
runCGI' init_effs action = do initialise
                              -- Transition to TaskRunning
                              startTask
                              -- Perform the user-defined action and collect the result
                              res <- runAction init_effs action
                              -- Transition to TaskComplete
                              finishTask
                              -- Write out the headers
                              writeHeaders
                              -- Write out the content
                              writeContent
                              -- Finally, return the result
                              pure res

public
runCGI : Env IO ((CGI (InitialisedCGI TaskRunning)) :: effs) -> CGIProg effs a -> IO a
runCGI init_env act = do result <- run [()] (runCGI' init_env act)
                         pure result

getWebEnv' [] _ = []
getWebEnv' (CgiEffect :: xs) cgi = (cgi) :: getWebEnv' xs cgi
getWebEnv' (SqliteEffect :: xs) cgi = (()) :: getWebEnv' xs cgi
getWebEnv' (SessionEffect :: xs) cgi = (InvalidSession) :: getWebEnv' xs cgi

isHandlerSet : Eff IO [CGI (InitialisedCGI TaskRunning)] Bool
isHandlerSet = queryPostVar "handler" >>= (Effects.pure . isJust)

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Inigo.Async.Util

public export
toObject : String
toObject = "let toObject=((list)=>Object.fromEntries([...Array(list.h).keys()].map((i)=>{let x=list['a'+(i+1)];return [x.a1,x.a2]})));"

public export
toArray : String -> String
toArray str = "(function(){let toArray=(x)=>{if(x.h === 0){return []}else{return [x.a1].concat(toArray(x.a2))}};return " ++ str ++ "})()"

public export
promisifyPrim_ : String -> String
promisifyPrim_ str =
  "(...args)=>{let [w,err,ok,...fargs]=args.reverse();return (" ++ str ++ ")(...fargs.reverse()).then((x)=>ok(x)(w),(e)=>err(e)(w))}"

public export
promisifyPrim: String -> String
promisifyPrim str =
  "node:lambda:" ++ (promisifyPrim_ str)

public export
promisifyResolve: String -> String -> String
promisifyResolve res str =
  "node:lambda:" ++ promisifyPrim_ ( "(...inner)=>{(" ++ str ++ ")(...inner);return Promise.resolve(" ++ res ++ ");}" )

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
{-
<
=
>
6
2
8
-}

instance Show Ordering where
  show LT = "<"
  show GT = ">"
  show EQ = "="

test : Ord a => a -> a -> IO ()
test x y = printLn $ compare x y

l : List (Int, Int)
l = [(33, 42), (42, 42), (42, 33)]

main : IO ()
main = do
  traverse_ (uncurry test) l
  traverse_ (\op => printLn $ 4 `op` 2) [(+), (-), (*)]

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Data.LazyList

public export
data LazyList : Type -> Type where
  Nil : LazyList a
  (::) : a -> Lazy (LazyList a) -> LazyList a

data NonEmpty : LazyList a -> Type where
  IsNonEmpty : NonEmpty (_ :: _)

export
Functor LazyList where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

export
Show a => Show (LazyList a) where
  show [] = "[]"
  show (x :: xs) = show x ++ " :: " ++ show xs

public export
Semigroup (LazyList a) where
  [] <+> ys = ys
  (x :: xs) <+> ys = x :: (xs <+> ys)

public export
Monoid (LazyList a) where
  neutral = []

export
total
head : LazyList a -> Maybe a
head [] = Nothing
head (x :: _) = Just x

export
total
head' : (l : LazyList a) -> NonEmpty l => a
head' (x :: _) = x

export
partial
head'' : LazyList a -> a
head'' [] = idris_crash "head: LazyList was empty"
head'' (x :: _) = x

export
total
tail : LazyList a -> Maybe (LazyList a)
tail [] = Nothing
tail (_ :: xs) = Just xs

export
total
tail' : (l : LazyList a) -> NonEmpty l => LazyList a
tail' (_ :: xs) = xs

export
partial
tail'' : LazyList a -> LazyList a
tail'' [] = idris_crash "tail: LazyList was empty"
tail'' (_ :: xs) = xs

export
implementation  Foldable LazyList where
  foldr f z [] = z
  foldr f z (x :: xs) = f x (foldr f z xs)

export
||| Foldable's methods are strict due to needing (a -> b -> b). `map` and the
||| like can stay lazy probably because they have a constructors guarding their
||| recursion. We don't have that here and must instead be explicitly lazy in
||| our combining function.
foldr' : (a -> Lazy b -> Lazy b) -> b -> LazyList a -> b
foldr' f z [] = z
foldr' f z (x :: xs) = f x (Delay (foldr' f z xs))

export
toList : LazyList a -> List a
toList = foldr' (\x,xs => x :: force xs) []

export -- Not lazy
fromList : List a -> LazyList a
fromList = foldr (\x,xs => x :: xs) []

-- It's weird but the S Z case is necessary otherwise a list like
-- take 2 [1,2,idris_crash "foo"] will crash. I don't know why that should be,
-- given that xs is Lazy.
export
take : Nat -> LazyList a -> LazyList a
take Z _  = []
take _ [] = []
take (S Z) (x :: _) = x :: []
take (S k) (x :: xs) = x :: take k xs

export
take' : Nat -> Stream a -> LazyList a
take' Z (x :: xs) = []
take' (S k) (x :: xs) = x :: take' k xs

repeat : a -> LazyList a
repeat x = x :: repeat x

takeUntil : (a -> Bool) -> Stream a -> LazyList a
takeUntil f (x :: xs) = if f x then [x] else x :: takeUntil f xs

takeBefore : (a -> Bool) -> Stream a -> LazyList a
takeBefore f (x :: xs) = if f x then [] else x :: takeBefore f xs

export -- [2..7] = [2,3,4,5,6,7]
rangeFromTo : (Range a, Ord a) => a -> a -> LazyList a
rangeFromTo x y = if y > x then takeUntil (>= y) (rangeFrom x)
                           else []

export
||| yanked from Prelude.Types
unpack : String -> LazyList Char
unpack str = unpack' (prim__cast_IntegerInt (natToInteger (length str)) - 1) str []
  where
    unpack' : Int -> String -> LazyList Char -> LazyList Char
    unpack' pos str acc
        = if pos < 0
             then acc
             else assert_total $ unpack' (pos - 1) str (assert_total (prim__strIndex str pos)::acc)

export
zipWith : (a -> b -> c) -> LazyList a -> LazyList b -> LazyList c
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
zipWith _ _ _ = []

export
%inline
zip : LazyList a -> LazyList b -> LazyList (a,b)
zip = zipWith MkPair