text:
module Core.Coverage

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import Data.List
import Data.Maybe
import Data.String

import Libraries.Data.NameMap
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Data.String.Extra

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

-- Return whether any of the name matches conflict
conflictMatch : {vars : _} -> List (Name, Term vars) -> Bool
conflictMatch [] = False
conflictMatch ((x, tm) :: ms) = conflictArgs x tm ms || conflictMatch ms
  where
    clash : Term vars -> Term vars -> Bool
    clash (Ref _ (DataCon t _) _) (Ref _ (DataCon t' _) _)
        = t /= t'
    clash (Ref _ (TyCon t _) _) (Ref _ (TyCon t' _) _)
        = t /= t'
    clash (PrimVal _ c) (PrimVal _ c')
      = c /= c'
    clash (Ref _ t _) (PrimVal _ _) = isJust (isCon t)
    clash (PrimVal _ _) (Ref _ t _) = isJust (isCon t)
    clash (Ref _ t _) (TType _) = isJust (isCon t)
    clash (TType _) (Ref _ t _) = isJust (isCon t)
    clash (TType _) (PrimVal _ _) = True
    clash (PrimVal _ _) (TType _) = True
    clash _ _ = False

    findN : Nat -> Term vars -> Bool
    findN i (Local _ _ i' _) = i == i'
    findN i tm
        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                   | _ => False in
              any (findN i) args

    -- Assuming in normal form. Look for: mismatched constructors, or
    -- a name appearing strong rigid in the other term
    conflictTm : Term vars -> Term vars -> Bool
    conflictTm (Local _ _ i _) tm
        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                   | _ => False in
              any (findN i) args
    conflictTm tm (Local _ _ i _)
        = let (Ref _ (DataCon _ _) _, args) = getFnArgs tm
                   | _ => False in
              any (findN i) args
    conflictTm tm tm'
        = let (f, args) = getFnArgs tm
              (f', args') = getFnArgs tm' in
          clash f f' || any (uncurry conflictTm) (zip args args')

    conflictArgs : Name -> Term vars -> List (Name, Term vars) -> Bool
    conflictArgs n tm [] = False
    conflictArgs n tm ((x, tm') :: ms)
        = (n == x && conflictTm tm tm') || conflictArgs n tm ms

-- Return whether any part of the type conflicts in such a way that they
-- can't possibly be equal (i.e. mismatched constructor)
conflict : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Defs -> Env Term vars -> NF vars -> Name -> Core Bool
conflict defs env nfty n
    = do Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure False
         case (definition gdef, type gdef) of
              (DCon t arity _, dty)
                  => do Nothing <- conflictNF 0 nfty !(nf defs [] dty)
                            | Just ms => pure $ conflictMatch ms
                        pure True
              _ => pure False
  where
    mutual
      conflictArgs : Int -> List (Closure vars) -> List (Closure []) ->
                     Core (Maybe (List (Name, Term vars)))
      conflictArgs _ [] [] = pure (Just [])
      conflictArgs i (c :: cs) (c' :: cs')
          = do cnf <- evalClosure defs c
               cnf' <- evalClosure defs c'
               Just ms <- conflictNF i cnf cnf'
                    | Nothing => pure Nothing
               Just ms' <- conflictArgs i cs cs'
                    | Nothing => pure Nothing
               pure (Just (ms ++ ms'))
      conflictArgs _ _ _ = pure (Just [])

      -- If the constructor type (the NF []) matches the variable type,
      -- then there may be a way to construct it, so return the matches in
      -- the indices.
      -- If any of those matches clash, the constructor is not valid
      -- e.g, Eq x x matches Eq Z (S Z), with x = Z and x = S Z
      -- conflictNF returns the list of matches, for checking
      conflictNF : Int -> NF vars -> NF [] ->
                   Core (Maybe (List (Name, Term vars)))
      conflictNF i t (NBind fc x b sc)
          -- invent a fresh name, in case a user has bound the same name
          -- twice somehow both references appear in the result  it's unlikely
          -- put posslbe
          = let x' = MN (show x) i in
                conflictNF (i + 1) t
                       !(sc defs (toClosure defaultOpts [] (Ref fc Bound x')))
      conflictNF i nf (NApp _ (NRef Bound n) [])
          = do empty <- clearDefs defs
               pure (Just [(n, !(quote empty env nf))])
      conflictNF i (NDCon _ n t a args) (NDCon _ n' t' a' args')
          = if t == t'
               then conflictArgs i (map snd args) (map snd args')
               else pure Nothing
      conflictNF i (NTCon _ n t a args) (NTCon _ n' t' a' args')
          = if n == n'
               then conflictArgs i (map snd args) (map snd args')
               else pure Nothing
      conflictNF i (NPrimVal _ c) (NPrimVal _ c')
          = if c == c'
               then pure (Just [])
               else pure Nothing
      conflictNF _ _ _ = pure (Just [])

-- Return whether the given type is definitely empty (due to there being
-- no constructors which can possibly match it.)
export
isEmpty : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          Defs -> Env Term vars -> NF vars -> Core Bool
isEmpty defs env (NTCon fc n t a args)
  = do Just nty <- lookupDefExact n (gamma defs)
         | _ => pure False
       case nty of
            TCon _ _ _ _ flags _ cons _
                 => if not (external flags)
                       then allM (conflict defs env (NTCon fc n t a args)) cons
                       else pure False
            _ => pure False
isEmpty defs env _ = pure False

-- Need this to get a NF from a Term; the names are free in any case
freeEnv : FC -> (vs : List Name) -> Env Term vs
freeEnv fc [] = []
freeEnv fc (n :: ns) = PVar fc top Explicit (Erased fc False) :: freeEnv fc ns

-- Given a normalised type, get all the possible constructors for that
-- type family, with their type, name, tag, and arity
getCons : {auto c : Ref Ctxt Defs} ->
          {vars : _} ->
          Defs -> NF vars -> Core (List (NF [], Name, Int, Nat))
getCons defs (NTCon _ tn _ _ _)
    = case !(lookupDefExact tn (gamma defs)) of
           Just (TCon _ _ _ _ _ _ cons _) =>
                do cs' <- traverse addTy cons
                   pure (mapMaybe id cs')
           _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
  where
    addTy : Name -> Core (Maybe (NF [], Name, Int, Nat))
    addTy cn
        = do Just gdef <- lookupCtxtExact cn (gamma defs)
                  | _ => pure Nothing
             case (definition gdef, type gdef) of
                  (DCon t arity _, ty) =>
                        pure (Just (!(nf defs [] ty), cn, t, arity))
                  _ => pure Nothing
getCons defs _ = pure []

emptyRHS : FC -> CaseTree vars -> CaseTree vars
emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts)
  where
    emptyRHSalt : CaseAlt vars -> CaseAlt vars
    emptyRHSalt (ConCase n t args sc) = ConCase n t args (emptyRHS fc sc)
    emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc)
    emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc)
    emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc)
emptyRHS fc (STerm i s) = STerm i (Erased fc False)
emptyRHS fc sc = sc

mkAlt : {vars : _} ->
        FC -> CaseTree vars -> (Name, Int, Nat) -> CaseAlt vars
mkAlt fc sc (cn, t, ar)
    = ConCase cn t (map (MN "m") (take ar [0..]))
              (weakenNs (map take) (emptyRHS fc sc))

altMatch : CaseAlt vars -> CaseAlt vars -> Bool
altMatch _ (DefaultCase _) = True
altMatch (DelayCase _ _ t) (DelayCase _ _ t') = True
altMatch (ConCase _ t _ _) (ConCase _ t' _ _) = t == t'
altMatch (ConstCase c _) (ConstCase c' _) = c == c'
altMatch _ _ = False

-- Given a type and a list of case alternatives, return the
-- well-typed alternatives which were *not* in the list
getMissingAlts : {auto c : Ref Ctxt Defs} ->
                 {vars : _} ->
                 FC -> Defs -> NF vars -> List (CaseAlt vars) ->
                 Core (List (CaseAlt vars))
-- If it's a primitive other than WorldVal, there's too many to reasonably
-- check, so require a catch all
getMissingAlts fc defs (NPrimVal _ WorldType) alts
    = if isNil alts
         then pure [DefaultCase (Unmatched "Coverage check")]
         else pure []
getMissingAlts fc defs (NPrimVal _ c) alts
  = do log "coverage.missing" 50 $ "Looking for missing alts at type " ++ show c
       if any isDefault alts
         then do log "coverage.missing" 20 "Found default"
                 pure []
         else pure [DefaultCase (Unmatched "Coverage check")]
-- Similarly for types
getMissingAlts fc defs (NType _) alts
    = do log "coverage.missing" 50 "Looking for missing alts at type Type"
         if any isDefault alts
           then do log "coverage.missing" 20 "Found default"
                   pure []
           else pure [DefaultCase (Unmatched "Coverage check")]
getMissingAlts fc defs nfty alts
    = do log "coverage.missing" 50 $ "Getting constructors for: " ++ show nfty
         logNF "coverage.missing" 20 "Getting constructors for" (mkEnv fc _) nfty
         allCons <- getCons defs nfty
         pure (filter (noneOf alts)
                 (map (mkAlt fc (Unmatched "Coverage check") . snd) allCons))
  where
    -- Return whether the alternative c matches none of the given cases in alts
    noneOf : List (CaseAlt vars) -> CaseAlt vars -> Bool
    noneOf alts c = not $ any (altMatch c) alts

-- Mapping of variable to constructor tag already matched for it
KnownVars : List Name -> Type -> Type
KnownVars vars a = List (Var vars, a)

getName : {idx : Nat} -> {vars : List Name} -> (0 p : IsVar n idx vars) -> Name
getName {vars = v :: _} First = v
getName (Later p) = getName p

showK : {ns : _} ->
        Show a => KnownVars ns a -> String
showK {a} xs = show (map aString xs)
  where
    aString : {vars : _} ->
              (Var vars, a) -> (Name, a)
    aString (MkVar v, t) = (getName v, t)

weakenNs : SizeOf args -> KnownVars vars a -> KnownVars (args ++ vars) a
weakenNs args [] = []
weakenNs args ((v, t) :: xs)
  = (weakenNs args v, t) :: weakenNs args xs

findTag : {idx, vars : _} ->
          (0 p : IsVar n idx vars) -> KnownVars vars a -> Maybe a
findTag v [] = Nothing
findTag v ((v', t) :: xs)
    = if sameVar (MkVar v) v'
         then Just t
         else findTag v xs

addNot : {idx, vars : _} ->
         (0 p : IsVar n idx vars) -> Int -> KnownVars vars (List Int) ->
         KnownVars vars (List Int)
addNot v t [] = [(MkVar v, [t])]
addNot v t ((v', ts) :: xs)
    = if sameVar (MkVar v) v'
         then ((v', t :: ts) :: xs)
         else ((v', ts) :: addNot v t xs)

tagIs : Int -> CaseAlt vars -> Bool
tagIs t (ConCase _ t' _ _) = t == t'
tagIs t (ConstCase _ _) = False
tagIs t (DelayCase _ _ _) = False
tagIs t (DefaultCase _) = True

tagIsNot : List Int -> CaseAlt vars -> Bool
tagIsNot ts (ConCase _ t' _ _) = not (t' `elem` ts)
tagIsNot ts (ConstCase _ _) = True
tagIsNot ts (DelayCase _ _ _) = True
tagIsNot ts (DefaultCase _) = False

-- Replace a default case with explicit branches for the constructors.
-- This is easier than checking whether a default is needed when traversing
-- the tree (just one constructor lookup up front).
replaceDefaults : {auto c : Ref Ctxt Defs} ->
                  {vars : _} ->
                  FC -> Defs -> NF vars -> List (CaseAlt vars) ->
                  Core (List (CaseAlt vars))
-- Leave it alone if it's a primitive type though, since we need the catch
-- all case there
replaceDefaults fc defs (NPrimVal _ _) cs = pure cs
replaceDefaults fc defs (NType _) cs = pure cs
replaceDefaults fc defs nfty cs
    = do cs' <- traverse rep cs
         pure (dropRep (concat cs'))
  where
    rep : CaseAlt vars -> Core (List (CaseAlt vars))
    rep (DefaultCase sc)
        = do allCons <- getCons defs nfty
             pure (map (mkAlt fc sc . snd) allCons)
    rep c = pure [c]

    dropRep : List (CaseAlt vars) -> List (CaseAlt vars)
    dropRep [] = []
    dropRep (c@(ConCase n t args sc) :: rest)
          -- assumption is that there's no defaultcase in 'rest' because
          -- we've just removed it
        = c :: dropRep (filter (not . tagIs t) rest)
    dropRep (c :: rest) = c :: dropRep rest

-- Traverse a case tree and refine the arguments while matching, so that
-- when we reach a leaf we know what patterns were used to get there,
-- and return those patterns.
-- The returned patterns are those arising from the *missing* cases
buildArgs : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            FC -> Defs ->
            KnownVars vars Int -> -- Things which have definitely match
            KnownVars vars (List Int) -> -- Things an argument *can't* be
                                    -- (because a previous case matches)
            List ClosedTerm -> -- ^ arguments, with explicit names
            CaseTree vars -> Core (List (List ClosedTerm))
buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
  -- If we've already matched on 'el' in this branch, restrict the alternatives
  -- to the tag we already know. Otherwise, add missing cases and filter out
  -- the ones it can't possibly be (the 'not') because a previous case
  -- has matched.
    = do let fenv = freeEnv fc _
         nfty <- nf defs fenv ty
         alts <- replaceDefaults fc defs nfty altsIn
         let alts' = alts ++ !(getMissingAlts fc defs nfty alts)
         let altsK = maybe alts' (\t => filter (tagIs t) alts')
                              (findTag el known)
         let altsN = maybe altsK (\ts => filter (tagIsNot ts) altsK)
                              (findTag el not)
         buildArgsAlt not altsN
  where
    buildArgAlt : KnownVars vars (List Int) ->
                  CaseAlt vars -> Core (List (List ClosedTerm))
    buildArgAlt not' (ConCase n t args sc)
        = do let l = mkSizeOf args
             let con = Ref fc (DataCon t (size l)) n
             let ps' = map (substName var
                             (apply fc
                                    con (map (Ref fc Bound) args))) ps
             buildArgs fc defs (weakenNs l ((MkVar el, t) :: known))
                               (weakenNs l not') ps' sc
    buildArgAlt not' (DelayCase t a sc)
        = let l = mkSizeOf [t, a] in
          let ps' = map (substName var (TDelay fc LUnknown
                                             (Ref fc Bound t)
                                             (Ref fc Bound a))) ps in
              buildArgs fc defs (weakenNs l known) (weakenNs l not')
                                ps' sc
    buildArgAlt not' (ConstCase c sc)
        = do let ps' = map (substName var (PrimVal fc c)) ps
             buildArgs fc defs known not' ps' sc
    buildArgAlt not' (DefaultCase sc)
        = buildArgs fc defs known not' ps sc

    buildArgsAlt : KnownVars vars (List Int) -> List (CaseAlt vars) ->
                   Core (List (List ClosedTerm))
    buildArgsAlt not' [] = pure []
    buildArgsAlt not' (c@(ConCase _ t _ _) :: cs)
        = pure $ !(buildArgAlt not' c) ++
                 !(buildArgsAlt (addNot el t not') cs)
    buildArgsAlt not' (c :: cs)
        = pure $ !(buildArgAlt not' c) ++ !(buildArgsAlt not' cs)

buildArgs fc defs known not ps (STerm _ vs)
    = pure [] -- matched, so return nothing
buildArgs fc defs known not ps (Unmatched msg)
    = pure [ps] -- unmatched, so return it
buildArgs fc defs known not ps Impossible
    = pure [] -- not a possible match, so return nothing

-- Traverse a case tree and return pattern clauses which are not
-- matched. These might still be invalid patterns, or patterns which are covered
-- elsewhere (turning up due to overlapping clauses) so the results should be
-- checked
export
getMissing : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             FC -> Name -> CaseTree vars ->
             Core (List ClosedTerm)
getMissing fc n ctree
   = do defs <- get Ctxt
        let psIn = map (Ref fc Bound) vars
        patss <- buildArgs fc defs [] [] psIn ctree
        let pats = concat patss
        unless (null pats) $
          logC "coverage.missing" 20 $ map unlines $
            flip traverse pats $ \ pat =>
              show <$> toFullNames pat
        pure (map (apply fc (Ref fc Func n)) patss)

-- For the given name, get the names it refers to which are not themselves
-- covering.
-- Also need to go recursively into case blocks, since we only calculate
-- references for them at the top level clause
export
getNonCoveringRefs : {auto c : Ref Ctxt Defs} ->
                     FC -> Name -> Core (List Name)
getNonCoveringRefs fc n
   = do defs <- get Ctxt
        Just d <- lookupCtxtExact n (gamma defs)
           | Nothing => undefinedName fc n
        let ds = mapMaybe noAssert (toList (refersTo d))
        let cases = filter isCase !(traverse toFullNames ds)

        -- Case blocks aren't recursive, so we're safe!
        cbad <- traverse (getNonCoveringRefs fc) cases
        topbad <- filterM (notCovering defs) ds
        pure (topbad ++ concat cbad)
  where
    isCase : Name -> Bool
    isCase (NS _ n) = isCase n
    isCase (CaseBlock _ _) = True
    isCase _ = False

    noAssert : (Name, Bool) -> Maybe Name
    noAssert (n, True) = Nothing
    noAssert (n, False) = Just n

    notCovering : Defs -> Name -> Core Bool
    notCovering defs n
        = case !(lookupCtxtExact n (gamma defs)) of
               Just def => case isCovering (totality def) of
                                IsCovering => pure False
                                _ => pure True
               _ => pure False

-- Does the second term match against the first?
-- 'Erased' matches against anything, we assume that's a Rig0 argument that
-- we don't care about
match : Term vs -> Term vs -> Bool
match (Local _ _ i _) _ = True
match (Ref _ Bound n) _ = True
match (Ref _ _ n) (Ref _ _ n') = n == n'
match (App _ f a) (App _ f' a') = match f f' && match a a'
match (As _ _ _ p) (As _ _ _ p') = match p p'
match (As _ _ _ p) p' = match p p'
match (TDelayed _ _ t) (TDelayed _ _ t') = match t t'
match (TDelay _ _ _ t) (TDelay _ _ _ t') = match t t'
match (TForce _ _ t) (TForce _ _ t') = match t t'
match (PrimVal _ c) (PrimVal _ c') = c == c'
match (Erased _ _) _ = True
match _ (Erased _ _) = True
match (TType _) (TType _) = True
match _ _ = False

-- Erase according to argument position
eraseApps : {auto c : Ref Ctxt Defs} ->
            Term vs -> Core (Term vs)
eraseApps {vs} tm
    = case getFnArgs tm of
           (Ref fc Bound n, args) =>
                do args' <- traverse eraseApps args
                   pure (apply fc (Ref fc Bound n) args')
           (Ref fc nt n, args) =>
                do defs <- get Ctxt
                   mgdef <- lookupCtxtExact n (gamma defs)
                   let eargs = maybe [] eraseArgs mgdef
                   args' <- traverse eraseApps (dropPos fc 0 eargs args)
                   pure (apply fc (Ref fc nt n) args')
           (tm, args) =>
                do args' <- traverse eraseApps args
                   pure (apply (getLoc tm) tm args')
  where
    dropPos : FC -> Nat -> List Nat -> List (Term vs) -> List (Term vs)
    dropPos fc i ns [] = []
    dropPos fc i ns (x :: xs)
        = if i `elem` ns
             then Erased fc False :: dropPos fc (S i) ns xs
             else x :: dropPos fc (S i) ns xs

-- if tm would be matched by trylhs, then it's not an impossible case
-- because we've already got it. Ignore anything in erased position.
clauseMatches : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                Env Term vars -> Term vars ->
                ClosedTerm -> Core Bool
clauseMatches env tm trylhs
    = let lhs = !(eraseApps (close (getLoc tm) env tm)) in
          pure $ match !(toResolvedNames lhs) !(toResolvedNames trylhs)
  where
    mkSubstEnv : {vars : _} ->
                 FC -> Int -> Env Term vars -> SubstEnv vars []
    mkSubstEnv fc i [] = Nil
    mkSubstEnv fc i (v :: vs)
       = Ref fc Bound (MN "cov" i) :: mkSubstEnv fc (i + 1) vs

    close : {vars : _} ->
            FC -> Env Term vars -> Term vars -> ClosedTerm
    close {vars} fc env tm
        = substs (mkSubstEnv fc 0 env)
              (rewrite appendNilRightNeutral vars in tm)

export
checkMatched : {auto c : Ref Ctxt Defs} ->
               List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
checkMatched cs ulhs
    = do logTerm "coverage" 5 "Checking coverage for" ulhs
         logC "coverage" 10 $ pure $ "(raw term: " ++ show !(toFullNames ulhs) ++ ")"
         ulhs <- eraseApps ulhs
         logTerm "coverage" 5 "Erased to" ulhs
         logC "coverage" 5 $ do
            cs <- traverse toFullNames cs
            pure $ "Against clauses:\n" ++
                   (show $ indent {ann = ()} 2 $ vcat $ map (pretty . show) cs)
         tryClauses cs ulhs
  where
    tryClauses : List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
    tryClauses [] ulhs
        = do logTermNF "coverage" 10 "Nothing matches" [] ulhs
             pure $ Just ulhs
    tryClauses (MkClause env lhs _ :: cs) ulhs
        = if !(clauseMatches env lhs ulhs)
             then do logTermNF "coverage" 10 "Yes" env lhs
                     pure Nothing -- something matches, discared it
             else do logTermNF "coverage" 10 "No match" env lhs
                     tryClauses cs ulhs


text:
module Example

import Text.PrettyPrint.Bernardy
import Data.Maybe

data SExp = SAtom String | SList (List SExp)

Pretty SExp where
    pretty (SAtom x) = fromString x
    pretty (SList xs) = hcat ["(", sep $ map pretty xs, ")"]

generateSExp : Nat -> SExp
generateSExp Z = SList [SAtom "a", SAtom "b", SAtom "c", SAtom "d", SAtom "e", SAtom "f"]
generateSExp (S k) =
    let sub = generateSExp k
     in SList [sub, sub, sub]

mySExp : SExp
mySExp = SList [SAtom "abcd", SAtom "efgh", SAtom "ijkl", SAtom "mnop"]

exp2 : SExp
exp2 = SList [mySExp, mySExp, mySExp]

opts : LayoutOpts
opts = Opts 60

main : IO ()
main = putStrLn $ fromMaybe "ERROR" $ Doc.render opts $ pretty $ generateSExp 7

ext: idr

max_stars_repo_name: Z-snails/prettier

max_issues_repo_name: Z-snails/prettier

max_forks_repo_name: Z-snails/prettier


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3
import Solver

-- ---------------------------------------------------------------------------
-- References

data IORef a = MkIORef (Array a)

newIORef : a -> IO (IORef a)
newIORef x = pure MkIORef <$> mkArray [x]

readIORef : IORef a -> IO a
readIORef (MkIORef arr) = getNth arr 0

writeIORef : IORef a -> a -> IO ()
writeIORef (MkIORef arr) x = setNth arr 0 x

modifyIORef : IORef a -> (a -> a) -> IO ()
modifyIORef r f = (pure f <$> readIORef r) >>= writeIORef r

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

strong : String -> String
strong s = "<strong>" ++ s ++ "</strong>"

litToHtml : Lit -> String
litToHtml (MkLit Pos lit) = lit
litToHtml (MkLit Neg lit) = "¬" ++ lit

clauseToHtml' : List Lit -> String
clauseToHtml' lits =
  case lits of
    [] => "□"
    ls => mconcat $ intersperse " ∨ " $ map litToHtml ls

clauseToHtml : Clause -> String
clauseToHtml (MkClause _ lits) = clauseToHtml' lits

litListToHtml : List Lit -> String
litListToHtml lits =
  "[" ++ (mconcat $ intersperse ", " $ map litToHtml lits) ++ "]"

-- ---------------------------------------------------------------------------
-- Message view

data MsgView = MkMsgView (Sel NoData NoData)

createMsgView : String -> Sel a b -> IO MsgView
createMsgView cssClass parent = do
  pure MkMsgView <$> (parent ??
    append "div" >=>
    forgetBoundData >=>
    classed cssClass True)

refreshMsgView : MsgView -> String -> IO ()
refreshMsgView (MkMsgView v) msg = do
  v ?? text msg
  return ()

refreshMsgViewHtml : MsgView -> String -> IO ()
refreshMsgViewHtml (MkMsgView v) msg = do
  v ?? html msg
  return ()

-- ---------------------------------------------------------------------------
-- Clause view

data ClauseView = MkClauseView (Sel NoData NoData)

createClauseView : String -> Sel a b -> IO ClauseView
createClauseView cssClass parent = do
  pure MkClauseView <$> (parent ??
    append "ul" >=>
    forgetBoundData >=>
    classed cssClass True >=>
    classed "clauseViewRoot" True)

refreshClauseView :
  ClauseView ->
  List Clause ->
  Trail ->
  List (CId, (Lit, Lit)) ->
  Operation ->
  IO ()
refreshClauseView (MkClauseView v) clauseList trail watched operation = do
    clauseArr <- mkArray clauseList

    let assig = trailToAssig trail

    clauses <- v ?? selectAll "ul.clauseViewRoot > li" >=>
               bind clauseArr
    clauses ?? exit >=> remove
    clauses ?? enter >=>
      append "li" >=>
      append "ul"
    clauses ??
      attr' "class" (const . pure . clauseClass)

    lits <- clauses ?? select "ul" >=>
              selectAll "li" >=>
              bind' (\d, i => mkArray $ map (\l => (getCId d, l)) $ getLits d)
    lits ?? exit >=> remove
    lits ?? enter >=>
      append "li" >=>
      append "span"

    lits ??
      attr' "class" (\cidLit, i => return $ litClass cidLit assig) >=>
      select "span" >=>
      html' (\cidLit, i => return $ litToHtml $ snd cidLit)

    return ()
  where
    getCId : Clause -> CId
    getCId (MkClause cid _) = cid
    clauseClass : Clause -> String
    clauseClass (MkClause cid _) =
      case operation of
        OPropagate before (cur :: after) =>
          if cid `clElem` before then
            "before"
          else if cid `clElem` [cur] then
            "cur"
          else if cid `clElem` after then
            "after"
          else
            ""
        -- All clauses are processed.
        OPropagate before [] =>
          if cid `clElem` before then
            "before"
          else
            ""
        _ => ""
      where
        clElem : CId -> List Clause -> Bool
        clElem cid' cs = isJust $ find ((== cid') . getCId) cs
    litClass : (CId, Lit) -> Assignment -> String
    litClass (cid, lit) assig =
      case assig lit of
        LTrue => "sat" ++ watchedCls
        LFalse => "unsat" ++ watchedCls
        LUndef => "unassigned" ++ watchedCls
      where
        watchedCls : String
        watchedCls = case find (\(cid', _) => cid' == cid) watched of
                       Nothing => ""
                       Just (_, (l, l')) =>
                         if lit == negLit l || lit == negLit l' then
                           " watched"
                         else
                           ""

-- ---------------------------------------------------------------------------
-- Assignment view

data AssigView = MkAssigView (Sel NoData NoData)

createAssigView : String -> Sel a b -> IO AssigView
createAssigView cssClass parent = do
  pure MkAssigView <$> (parent ??
    append "ul" >=>
    forgetBoundData >=>
    classed cssClass True >=>
    classed "assigViewRoot" True)

refreshAssigView : AssigView -> List Clause -> Trail -> IO ()
refreshAssigView (MkAssigView v) clauses trail = do
    trailArr <- emptyA ()
    mapM_ (mkArray >=> pushA trailArr) $ groupBy sameLevel $ reverse trail

    levels <- v ?? selectAll "ul.assigViewRoot > li" >=>
                bind trailArr
    levels ?? exit >=> remove
    levels ?? enter >=>
      append "li" >=>
      append "ul"

    lits <- levels ?? select "ul" >=>
              selectAll "li" >=>
              bind' (const . pure)
    lits ?? exit >=> remove
    lits ?? enter >=>
      append "li"

    lits ??
      html' (const . pure . litHtml) >=>
      attr' "title" (const . decodeEntities . litTitle) >=>
      attr' "class" (const . pure . litClass)

    return ()
  where
    sameLevel : (Lit, Maybe Ante, Level) -> (Lit, Maybe Ante, Level) -> Bool
    sameLevel (_, _, l) (_, _, l') = l == l'
    litTitle : (Lit, Maybe Ante, Level) -> String
    litTitle (_, Nothing, _) = ""
    litTitle (_, Just cid, _) = clauseToHtml $ findClause cid clauses
    litHtml : (Lit, Maybe Ante, Level) -> String
    litHtml (lit, _, _) = litToHtml lit
    litClass : (Lit, Maybe Ante, Level) -> String
    litClass (_, Nothing, _) = "decided"
    litClass (_, Just _, _) = "forced"

-- ---------------------------------------------------------------------------
-- Implication graph view

data Vertex
  = VLit Lit
  | VConfl

instance Eq Vertex where
  (VLit l) == (VLit l') = l == l'
  VConfl   == VConfl    = True
  _        == _         = False

instance Show Vertex where
  show (VLit l) = show l
  show VConfl = "?K"

Edge : Type
Edge = (Vertex, Vertex)

getVertex : Node Vertex -> IO Vertex
getVertex = getNData

getEdge : Link Vertex () -> IO Edge
getEdge = getSrcTgt >=> mapTupleM getVertex

data ImplGraphView
  = MkImplGraphView
      (ForceLayout Vertex ())
      (Sel NoData NoData) -- Link layer.
      (Sel NoData NoData) -- Node layer.
      (Sel NoData NoData) -- Text layer.

createImplGraphView : String -> Float -> Float -> Sel a b -> IO ImplGraphView
createImplGraphView cssClass width height parent = do

  svg <- parent ?? append "svg" >=>
           forgetBoundData >=>
           attr "width" (show width) >=>
           attr "height" (show height) >=>
           classed cssClass True

  let setupMarker =
    attr "viewBox" "0 -4 9 8" >=>
    attr "refX" "16" >=>
    attr "markerWidth" "9" >=>
    attr "markerHeight" "8" >=>
    attr "orient" "auto" >=>
    append "svg:path" >=>
    attr "d" "M0 -4 L9 0 L0 4"

  defs <- svg ?? append "svg:defs"
  defs ?? append "svg:marker" >=>
    attr "id" "arrow" >=>
    setupMarker
  defs ?? append "svg:marker" >=>
    attr "id" "arrowCut" >=>
    attr "fill" "#00f" >=>
    setupMarker
  defs ?? append "svg:marker" >=>
    attr "id" "arrowProc" >=>
    attr "fill" "#cc0000" >=>
    setupMarker
  defs ?? append "svg:marker" >=>
    attr "id" "arrowMinim" >=>
    attr "fill" "#cc0000" >=>
    setupMarker

  [| MkImplGraphView
       (mkForceLayout width height >>=
          linkDistanceL 100 >>=
          chargeL (-300))
       (svg ?? append "svg:g")
       (svg ?? append "svg:g")
       (svg ?? append "svg:g")
  |]

refreshImplGraphView :
  ImplGraphView ->
  List Clause ->
  Trail ->
  Operation ->
  IO ()
refreshImplGraphView
  (MkImplGraphView fl linkLayer nodeLayer textLayer)
  clauses
  trail
  operation = do

    stopL fl

    --
    -- Update arrays with nodes and links.
    --

    -- Remove old nodes and links.
    nodes <- getNodes fl >>= filterA (getVertex >=> pure . vertInModel)
    links <- getLinks fl >>=
               filterA (getEdge >=>
                        mapTupleM (vertInView nodes) >=>
                        pure . uncurry (&&))

    -- Add new nodes.
    newVertices <- filterM (vertInView nodes >=> pure . not)
                     $ map toVert trail
    mapM_ (mkNode >=> pushA nodes) newVertices
    addConfl nodes

    -- Add new links.
    newEdges <- filterM (edgeInView links >=> pure . not)
                  $ concatMap edgesLeadingToLit trail
    mapM_
      (mapTupleM (findNode nodes) >=>
         flip (uncurry mkLink) () >=>
         pushA links)
      newEdges
    addLinksToConfl nodes links

    putNodes fl nodes
    putLinks fl links

    --
    -- Bind arrays.
    --

    lines <- linkLayer ?? selectAll "line" >=>
               bindK links (const . linkKey)
    lines ?? exit >=> remove
    lines ?? enter >=> append "svg:line"
    lines ??
      attr' "class" (const . (getEdge >=> pure . edgeClass)) >=>
      attr' "marker-end" (const . (getEdge >=> pure . edgeMarkerEnd)) >=>
      attr' "stroke-dasharray" (const . (getEdge >=> pure . edgeDashArray))

    circles <- nodeLayer ?? selectAll "circle" >=>
                 bindK nodes (const . nodeKey)
    circles ?? exit >=> remove
    circles ?? enter >=>
      append "svg:circle" >=>
      makeDraggableL fl >=>
      attr "r" "7"
    circles ?? attr' "class" (const . (getVertex >=> pure . vertClass))

    textGroups <- textLayer ?? selectAll "g" >=>
                    bindK nodes (const . nodeKey)
    textGroups ?? exit >=> remove
    newTextGroups <- textGroups ?? enter >=> append "svg:g"

    -- Shadow.
    newTextGroups ?? append "svg:text" >=>
      attr "class" "shadow" >=>
      text' (const . (getVertex >=> vertLabel))

    -- Text.
    newTextGroups ?? append "svg:text" >=>
      text' (const . (getVertex >=> vertLabel))

    labels <- textGroups ?? selectAll "text" >=>
                forgetBoundData >=>
                castBoundData

    --
    -- Tick handler.
    --

    fl `onTickL` tickHandler lines circles labels

    startL fl
  where
    toVert : (Lit, Maybe Ante, Level) -> Vertex
    toVert (lit, _, _) = VLit lit
    vertInModel : Vertex -> Bool
    vertInModel v = case v of
                      VLit _ => isJust $ find ((== v) . toVert) trail
                      VConfl => case operation of
                                  OLearn _ _ _ => True
                                  _ => False
    vertInView : Array (Node Vertex) -> Vertex -> IO Bool
    vertInView ns v = anyA (getVertex >=> pure . (== v)) ns
    edgesLeadingToLit : (Lit, Maybe Ante, Level) -> List Edge
    edgesLeadingToLit (_, Nothing, _) = []
    edgesLeadingToLit (lit, Just cid, _) =
      -- Source literal is negated since it is assigned false.
      map (\l => (VLit $ negLit l, VLit lit))
        -- No edge from itself.
        $ filter (/= lit)
        $ getLits
        $ findClause cid clauses
    edgeInView : Array (Link Vertex ()) -> Edge -> IO Bool
    edgeInView ls e = anyA (getEdge >=> pure . (== e)) ls
    findNode : Array (Node Vertex) -> Vertex -> IO (Node Vertex)
    findNode ns v =
      fromJust `fmap` findA (getVertex >=> pure . (== v)) ns
    addConfl : Array (Node Vertex) -> IO ()
    addConfl ns = do
      inView <- vertInView ns VConfl
      if not inView && vertInModel VConfl then
        mkNode VConfl >>= pushA ns
      else
        return ()
    addLinksToConfl : Array (Node Vertex) -> Array (Link Vertex ()) -> IO ()
    addLinksToConfl ns ls =
      case operation of
        OLearn _ (MkClause _ lits) _ => do
          newEdges <- filterM (edgeInView ls >=> pure . not)
                        $ map (\l => (VLit $ negLit l, VConfl)) lits
          mapM_
            (mapTupleM (findNode ns) >=>
               flip (uncurry mkLink) () >=>
               pushA ls)
            newEdges
        _ => return ()

    linkKey : Link Vertex () -> IO String
    linkKey link = do
      (v, v') <- getEdge link
      return $ show v ++ "--->" ++ show v'
    nodeKey : Node Vertex -> IO String
    nodeKey = getVertex >=> pure . show
    isInConflClause : List Lit -> Vertex -> Bool
    isInConflClause _ VConfl = False
    isInConflClause conflCl (VLit (MkLit _ var)) =
      isJust $ find (\(MkLit _ v) => v == var) conflCl
    isProc : List Var -> Vertex -> Bool
    isProc _ VConfl = True
    isProc vars (VLit (MkLit _ var)) = isJust $ find (== var) vars
    edgeCase : String -> String -> String -> String -> Edge -> String
    edgeCase normal cut proc minim (src, tgt) =
      case operation of
        OLearn conflCl _ vars =>
          if isProc vars src then
            proc
          else if isInConflClause conflCl src && isProc vars tgt then
            cut
          else
            normal
        OMinimize lits =>
          case (src, tgt) of
            (VLit s, VLit t) =>
              if (s `elem` lits) && (t `elem` lits) then
                minim
              else
                normal
            _ => "error"
        _ => normal
    edgeCase _ _ _ _ (VConfl, _) = "error"
    edgeClass : Edge -> String
    edgeClass = edgeCase "" "cut" "proc" "minim"
    edgeMarkerEnd : Edge -> String
    edgeMarkerEnd = edgeCase
                      "url(#arrow)"
                      "url(#arrowCut)" "url(#arrowProc)"
                      "url(#arrowMinim)"
    edgeDashArray : Edge -> String
    edgeDashArray = edgeCase "" "" "4, 4" ""
    vertClass : Vertex -> String
    vertClass (VLit (MkLit s var)) = cls ++ opCls
      where
        v : Vertex
        v = VLit $ MkLit s var
        cls = case findInTrail var trail of
                Just (_, Nothing, _) => "decided"
                Just (_, Just _, _) => "forced"
                Nothing => "error"
        opCls = case operation of
                  OLearn conflCl _ vars =>
                    if isProc vars v then
                      " proc"
                    else if isInConflClause conflCl v then
                      " inConflClause"
                    else
                      ""
                  OMinimize lits =>
                    if (MkLit s var) `elem` lits then
                      " minim"
                    else
                      ""
                  _ => ""
    vertClass VConfl = "conflVertex"
    vertLabel : Vertex -> IO String
    vertLabel (VLit l) = decodeEntities $ litToHtml l
    vertLabel VConfl = return "K"

    tickHandler :
      Sel NoData (Link Vertex ()) ->
      Sel NoData (Node Vertex) ->
      Sel NoData (Node Vertex) ->
      () -> IO ()
    tickHandler lines circles labels () = do
      lines ??
        attr' "x1" (const . (getSource >=> getX >=> pure . show)) >=>
        attr' "y1" (const . (getSource >=> getY >=> pure . show)) >=>
        attr' "x2" (const . (getTarget >=> getX >=> pure . show)) >=>
        attr' "y2" (const . (getTarget >=> getY >=> pure . show))
      circles ??
        attr' "cx" (const . (getX >=> pure . show)) >=>
        attr' "cy" (const . (getY >=> pure . show))
      labels ??
        attr' "x" (const . (getX >=> pure . show . (+ 10))) >=>
        attr' "y" (const . (getY >=> pure . show . (+ 10)))
      return ()

-- ---------------------------------------------------------------------------
-- Check box

data CheckBox = MkCheckBox (Sel NoData NoData)

createCheckBox : String -> String -> Bool -> Sel a b -> IO CheckBox
createCheckBox cssClass label checked parent = do
  cb <- parent ?? append "span" >=>
          forgetBoundData >=>
          classed cssClass True >=>
          classed "checkBoxRoot" True
  cb ?? append "input" >=>
    attr "type" "checkbox" >=>
    boolProperty "checked" checked
  cb ?? append "span" >=>
    text label
  return $ MkCheckBox cb

isChecked : CheckBox -> IO Bool
isChecked (MkCheckBox cb) =
  cb ?? select "input" >=>
    getBoolProperty "checked"

setChecked : CheckBox -> Bool -> IO ()
setChecked (MkCheckBox cb) checked = do
  cb ?? select "input" >=>
    boolProperty "checked" checked
  return ()

removeCheckBox : CheckBox -> IO ()
removeCheckBox (MkCheckBox cb) = cb ?? remove

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

record State : Type where
  MkState :
    (stSol : Sol) ->
    (stSolHist : List Sol) ->
    (stAutoAssig : Bool) ->
    (stConflAnalVis : Bool) ->
    (stLastInterrupt : Maybe (Event, Sol -> AlgoResult Sol Event Result)) ->
    (stInterruptHist : List (Event, Sol -> AlgoResult Sol Event Result)) ->
    (stMsgView : MsgView) ->
    (stClauseView : ClauseView) ->
    (stAssigView : AssigView) ->
    (stImplGraphView : ImplGraphView) ->
    (stAddClauseBtn : Sel NoData NoData) ->
    (stStartVisBtn : Sel NoData NoData) ->
    (stPrevBtn : Sel NoData NoData) ->
    (stNextBtn : Sel NoData NoData) ->
    State

consMaybe : Maybe a -> List a -> List a
consMaybe Nothing xs = xs
consMaybe (Just x) xs = x :: xs

-- Updates the message and the information about the last interrupt.
procAlgoResult : AlgoResult Sol Event Result -> IORef State -> IO ()
procAlgoResult algoRes r = do
  s <- readIORef r
  let origSol = stSol s
  let origLastInterrupt = stLastInterrupt s
  let origSolHist = stSolHist s
  let origInterruptHist = stInterruptHist s
  let putMsg = refreshMsgViewHtml (stMsgView s)
  let funcs = ( strong . litToHtml
              , strong . clauseToHtml'
              , strong . clauseToHtml
              , strong . litListToHtml )
  let (lit2Html, clause2Html', clause2Html, litList2Html) = funcs
  let revertState = (record { stSol = origSol
                            , stSolHist = origSolHist
                            , stLastInterrupt = origLastInterrupt
                            , stInterruptHist = origInterruptHist })
  modifyIORef r (record { stSolHist = origSol :: origSolHist
                        , stInterruptHist = consMaybe
                                              origLastInterrupt
                                              origInterruptHist })
  case algoRes of
    Finish sol res => do
      (stNextBtn s) ?? style "display" "none" >=>
        (\x => return ()) -- Change result type to satisfy the compiler.
      modifyIORef r (record { stSol = sol, stLastInterrupt = Nothing })
      case res of
        Sat => putMsg "SAT"
        Unsat => putMsg "UNSAT - conflict clause on decision level 0"
    Interrupt sol e k => do
      modifyIORef r (record { stSol = sol, stLastInterrupt = Just (e, k) })
      case e of
        EChoose (v :: _) =>
          if stAutoAssig s then do
            -- Place automatically chosen literal into the solver.
            let sol2 = record { sChosen = Just $ MkLit Pos v } sol
            -- Don't save current sol and interrupt into history.
            modifyIORef r revertState
            procAlgoResult (resume sol2 k) r
          else
            putMsg $ "Choose unassigned literal to be satisfied"
        EDecide lit => putMsg $ "Decision: satisfy " ++ lit2Html lit
        EProp lit cl =>
          putMsg $ "Propagation: clause "
            ++ clause2Html cl
            ++ " forces "
            ++ lit2Html lit
        EConfl cl =>
          putMsg $ "Conflict clause "
            ++ clause2Html cl
            ++ " detected"
        EWShortClause l cl =>
          putMsg $ "Propagation: satisfy "
            ++ lit2Html l
        EWPropLitStart l =>
          putMsg $ "Propagation: process clauses where "
            ++ lit2Html l
            ++ " is watched"
        EWOtherLitTrue l l' cl =>
          putMsg $ "Propagation: skip clause "
            ++ clause2Html cl
            ++ " because other watched literal "
            ++ lit2Html l'
            ++ " is true"
        EWReplaceLit oldL newL cl =>
          putMsg $ "Propagation: replace watched literal "
            ++ lit2Html oldL
            ++ " by "
            ++ lit2Html newL
            ++ " in clause "
            ++ clause2Html cl
        EWConfl l l' cl =>
          putMsg $ "Propagation: literal "
            ++ lit2Html l
            ++ " watched in clause "
            ++ clause2Html cl
            ++ " cannot be replaced and other watched literal "
            ++ lit2Html l'
            ++ " is false"
        EWProp l l' cl =>
          putMsg $ "Propagation: literal "
            ++ lit2Html l
            ++ " watched in clause "
            ++ clause2Html cl
            ++ " cannot be replaced, so other watched literal "
            ++ lit2Html l'
            ++ " is forced"
        EAnalyzeStart cl =>
          if stConflAnalVis s then
            putMsg $ "Analysis: make asserting clause "
              ++ "from current conflict clause " ++ clause2Html cl
          else do
            -- Don't save current sol and interrupt into history.
            modifyIORef r revertState
            procAlgoResult (resume sol k) r
        EResolve v conflCl anteCl resolvent =>
          if stConflAnalVis s then
            putMsg $ "Analysis: resolve current conflict clause "
              ++ clause2Html' conflCl
              ++ " with " ++ clause2Html anteCl
              ++ " on variable " ++ strong v
              ++ " and form new conflict clause "
              ++ clause2Html' resolvent
          else do
            -- Don't save current sol and interrupt into history.
            modifyIORef r revertState
            procAlgoResult (resume sol k) r
        ESkip v conflCl anteCl =>
          if stConflAnalVis s then
            putMsg $ "Analysis: variable "
              ++ strong v ++ " is not present in current conflict clause "
              ++ clause2Html' conflCl
          else do
            -- Don't save current sol and interrupt into history.
            modifyIORef r revertState
            procAlgoResult (resume sol k) r
        EAnalyzeEnd cl =>
          if stConflAnalVis s then
            putMsg $ "Analysis: found asserting clause "
              ++ clause2Html' cl
          else do
            -- Don't save current sol and interrupt into history.
            modifyIORef r revertState
            procAlgoResult (resume sol k) r
        EMinStart candidates assertingCl =>
          putMsg $ "Minimization:"
            ++ " remove redundant literals from asserting clause "
            ++ clause2Html' assertingCl
            ++ "; candidates for removal are "
            ++ litList2Html candidates
        ETestRedundant l assertingCl =>
          putMsg $ "Minimization:"
            ++ " test whether literal "
            ++ lit2Html l
            ++ " is redundant in asserting clause "
            ++ clause2Html' assertingCl
        ERedundant l assertingCl =>
          putMsg $ "Minimization:"
            ++ " literal "
            ++ lit2Html l
            ++ " is redundant in asserting clause "
            ++ clause2Html' assertingCl
        ENotRedundant l assertingCl =>
          putMsg $ "Minimization:"
            ++ " literal "
            ++ lit2Html l
            ++ " isn't redundant in asserting clause "
            ++ clause2Html' assertingCl
        EMinEnd redundantLits assertingCl minAssertingCl =>
          putMsg $ "Minimization:"
            ++ " remove redundant literals "
            ++ litList2Html redundantLits
            ++ " from asserting clause "
            ++ clause2Html' assertingCl
            ++ " and form new asserting clause "
            ++ clause2Html' minAssertingCl
        ELearn cl =>
          putMsg $ "Learning: add asserting clause "
            ++ clause2Html cl
        EBacktrack lit _ => putMsg $ "Backtracking: undo " ++ lit2Html lit

refreshClauseAssigImplGraphViews : IORef State -> Sol -> IO ()
refreshClauseAssigImplGraphViews r sol = do
  s <- readIORef r
  refreshClauseView
    (stClauseView s)
    (sClauses sol)
    (sTrail sol)
    (sWatched sol)
    (sOp sol)
  refreshAssigView
    (stAssigView s)
    (sClauses sol)
    (sTrail sol)
  refreshImplGraphView
    (stImplGraphView s)
    (sClauses sol)
    (sTrail sol)
    (sOp sol)

-- Updates the visualization to correspond to the current state.
-- Runs the solver and updates the message with the description
-- of what the solver did.
next : IORef State -> IO ()
next r = do
  s <- readIORef r
  let sol = stSol s
  case stLastInterrupt s of
    Nothing => return ()
    Just (e, k) => do
      refreshClauseAssigImplGraphViews r sol
      case e of
        EChoose vars => do
          litStr <- prompt "Choose literal to be satisfied"
          case pure parseLit <$> litStr of
            Just (Right (MkLit sign v)) =>
              if v `elem` vars then do
                (stPrevBtn s) ?? style "display" "block" >=>
                  (\x => return ()) -- Change result type to satisfy the compiler.
                -- Place chosen literal into the solver.
                let sol2 = record { sChosen = Just $ MkLit sign v } sol
                procAlgoResult (resume sol2 k) r
              else
                return ()
            _ =>
              return ()
        _ => do
          (stPrevBtn s) ?? style "display" "block" >=>
            (\x => return ()) -- Change result type to satisfy the compiler.
          procAlgoResult (resume sol k) r

prev : IORef State -> IO ()
prev r = do
  s <- readIORef r
  case stInterruptHist s of
    [] => return ()
    (e, k) :: interruptHist => do
      -- Currently (hd $ stSolHist s) and (stLastInterrupt s) are visualized.
      let sol = hd $ tl $ stSolHist s
      refreshClauseAssigImplGraphViews r sol
      modifyIORef r (record { stSol = sol
                            , stSolHist = tl $ tl $ stSolHist s
                            , stLastInterrupt = head' interruptHist
                            , stInterruptHist = drop 1 interruptHist })
      (stNextBtn s) ?? style "display" "block" >=>
        (\x => return ()) -- Change result type to satisfy the compiler.
      if isNil interruptHist then
        (stPrevBtn s) ?? style "display" "none" >=>
          (\x => return ()) -- Change result type to satisfy the compiler.
      else
        return ()
      procAlgoResult (Interrupt (hd $ stSolHist s) e k) r
      return ()
    _ => return ()

initSolver : Sel NoData NoData -> (Bool, Bool, Bool, Bool) -> IO ()
initSolver parent (autoAssig, conflAnalVis, watchedLits, minClause) = do
  msgView <- parent ?? createMsgView "msgView"

  clauseView <- parent ?? createClauseView "clauseView"

  assigView <- parent ?? createAssigView "assigView"

  implGraphView <- parent ?? createImplGraphView "implGraphView" 600 468

  addClauseBtn <- parent ?? append "input" >=>
                    classed "addClauseBtn" True >=>
                    attr "type" "button" >=>
                    property "value" "Add clause"

  startVisBtn <- parent ?? append "input" >=>
                   classed "startVisBtn" True >=>
                   attr "type" "button" >=>
                   property "value" "Start visualization"

  r <- newIORef $ MkState
         (record { sEnableWatchedLits = watchedLits
                 , sEnableMinimization = minClause } emptySol)
         []
         autoAssig
         conflAnalVis
         Nothing -- Last interrupt.
         []
         msgView
         clauseView
         assigView
         implGraphView
         addClauseBtn
         startVisBtn
         d3 -- Dummy.
         d3 -- Dummy.

  addClauseBtn `onClick` \() => do
    litsStr <- prompt "Enter clause"
    s <- readIORef r
    case pure parseLits <$> litsStr of
      -- Prompt cancelled by user.
      Nothing => return ()
      -- Literals cannot be parsed.
      Just (Left err) =>
        refreshMsgView (stMsgView s) $ "Cannot parse literals: " ++ err
      -- Literals are ok.
      Just (Right lits) => do
        let lits' = nub lits
        let vars : List Var = map (\(MkLit _ v) => v) lits'
        if isNil lits' then
          refreshMsgView (stMsgView s) "Clause is ignored because it is empty"
        else if vars /= nub vars then
          refreshMsgViewHtml (stMsgView s) $ "Clause "
            ++ strong (clauseToHtml' lits')
            ++ " is ignored because it contains complementary literals"
        -- Add clause.
        else
          case run (stSol s) (addClause lits') of
            Interrupt _ _ _ =>
              putStrLn "Internal error: unexpected interrupt when adding clause"
            Finish sol _ => do
              modifyIORef r (record { stSol = sol })
              refreshClauseView
                (stClauseView s)
                (sClauses sol)
                (sTrail sol)
                (sWatched sol)
                (sOp sol)
              refreshMsgView (stMsgView s) ""

  startVisBtn `onClick` \() => do
    s <- readIORef r
    (stAddClauseBtn s) ?? remove
    (stStartVisBtn s) ?? remove

    prevBtn <- parent ?? append "input" >=>
                 classed "prevBtn" True >=>
                 attr "type" "button" >=>
                 property "value" "Prev" >=>
                 style "display" "none"
    prevBtn `onClick` \() => prev r

    nextBtn <- parent ?? append "input" >=>
                 classed "nextBtn" True >=>
                 attr "type" "button" >=>
                 property "value" "Next"
    nextBtn `onClick` \() => next r

    modifyIORef r (record { stPrevBtn = prevBtn
                          , stNextBtn = nextBtn })

    procAlgoResult (run (stSol s) solve) r

init : Sel NoData NoData -> IO ()
init parent = do
  cfg <- parent ?? append "div"

  autoAssigCB <- createCheckBox
                   "autoAssigCB"
                   "Automatic assignment"
                   True cfg

  conflAnalVisCB <- createCheckBox
                      "conflAnalVisCB"
                      "Conflict analysis visualization"
                      True cfg

  watchedLitsCB <- createCheckBox
                     "watchedLitsCB"
                     "Watched literals"
                     False cfg

  minClauseCB <- createCheckBox
                   "minClauseCB"
                   "Minimize asserting clause"
                   False cfg

  goOnBtn <- cfg ?? append "input" >=>
               classed "goOnBtn" True >=>
               attr "type" "button" >=>
               property "value" "Go on"

  goOnBtn `onClick` \() => do
    autoAssig <- isChecked autoAssigCB
    conflAnalVis <- isChecked conflAnalVisCB
    watchedLits <- isChecked watchedLitsCB
    minClause <- isChecked minClauseCB
    cfg ?? remove
    initSolver parent (autoAssig, conflAnalVis, watchedLits, minClause)

main : IO ()
main =
  d3 ?? select "body" >=> init

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Data.Compress.Huffman

import Data.Fin
import Data.Vect
import Data.List
import Data.List1
import Data.Bits
import Data.Stream
import Data.Compress.Utils.Misc
import Data.Compress.Utils.Parser

data Tree : Type -> Type where
  Node : Tree a -> Tree a -> Tree a
  Leaf : a -> Tree a

mk : List Bool -> a -> Tree (Maybe a)
mk [] k = Leaf (Just k)
mk (False :: dirs) k = Node (mk dirs k) (Leaf Nothing)
mk (True :: dirs) k = Node (Leaf Nothing) (mk dirs k)

insert : List Bool -> a -> Tree (Maybe a) -> Maybe (Tree (Maybe a))
insert [] k (Leaf Nothing) = pure $ Leaf (Just k)
insert [] k (Leaf (Just _)) = Nothing
insert [] k (Node _ _) = Nothing
insert (False :: xs) k (Node left right) = pure $ Node !(insert xs k left) right
insert (True :: xs) k (Node left right) = pure $ Node left !(insert xs k right)
insert (False :: xs) k (Leaf Nothing) = pure $ Node !(insert xs k (Leaf Nothing)) (Leaf Nothing)
insert (True :: xs) k (Leaf Nothing) = pure $ Node (Leaf Nothing) !(insert xs k (Leaf Nothing))
insert (_ :: _) k (Leaf (Just _)) = Nothing

lookup_count : Eq a => List (a, Nat) -> a -> Nat
lookup_count list key =
  case lookup key list of
    Just x => x
    Nothing => Z

max' : Ord a => List1 a -> a
max' (x ::: xs) = foldl max x xs

smallest_codes : (Bits32 -> Nat) -> (n : Nat) -> Vect (S n) Bits32
smallest_codes bl_count max_code_length =
  take (S max_code_length) $ map fst $ iterate go (0,0)
  where
    go : (Bits32, Bits32) -> (Bits32, Bits32)
    go (prev_code, prev_index) = (shiftL (prev_code + cast (bl_count prev_index)) 1, prev_index + 1)

make_tree_from_length : {n : Nat} -> List Bits32 -> Vect (S n) Bits32 -> List Bits32 -> Maybe (List Bits32)
make_tree_from_length acc next_code [] = Just $ reverse acc
make_tree_from_length acc next_code (x :: xs) = do
  x' <- natToFin (cast x) (S n)
  let v = index x' next_code
  make_tree_from_length (v :: acc) (updateAt x' (+1) next_code) xs

decompose_bits32 : Bits32 -> Fin 32 -> List Bool
decompose_bits32 i FZ = [ testBit i FZ ]
decompose_bits32 i (FS n) = testBit i (FS n) :: decompose_bits32 i (weaken n)

decompose_l_i : Bits32 -> Bits32 -> Maybe (List Bool)
decompose_l_i l i = decompose_bits32 i <$> natToFin (cast (l-1)) 32

public export
record HuffmanTree where
  constructor MkTree
  parse_literals : Parser Bitstream (SimpleError String) Bits32
  parse_distance : Parser Bitstream (SimpleError String) Bits32

export
default_tree : HuffmanTree
default_tree = MkTree first (get_huff 5) where
  first : Parser Bitstream (SimpleError String) Bits32
  first = do
    x <- get_huff 7
    if x < 24 then pure (x + 256) else do
      x <- map ((shiftL x 1) .|.) get_bit
      if x < 192 then pure (x - 48)
        else if x < 200 then pure (x + 88)
        else map (\y => ((shiftL x 1) .|. y) - 256) get_bit

tree_to_parser : Tree (Maybe a) -> Parser Bitstream (SimpleError String) a
tree_to_parser (Leaf Nothing) = fail $ msg "no value at leaf"
tree_to_parser (Leaf (Just v)) = pure v
tree_to_parser (Node false true) = do
  b <- token
  if b then tree_to_parser true else tree_to_parser false

export
make_tree : Ord a => List (a, Bits32) -> Nat -> Maybe (Parser Bitstream (SimpleError String) a)
make_tree elem_code_length max_n_code = do
  let elem_code_length = filter (\(a,b) => b > 0) $ sortBy (\a,b => compare (fst a) (fst b)) elem_code_length
  let code_length = map snd elem_code_length

  guard ((length code_length) <= max_n_code)
  let code_length_count = count code_length
  let bl_count = lookup_count code_length_count
  code_length_count1 <- fromList code_length_count

  let max_code_length = cast $ max' $ map fst code_length_count1
  let next_code = smallest_codes bl_count max_code_length

  tree <- make_tree_from_length [] next_code code_length
  elem_code <- traverse (\(i,(v,l)) => (,v) <$> decompose_l_i l i) $ zip tree elem_code_length
  (elem_code_head ::: elem_code_tail) <- fromList elem_code

  b_tree <- foldlM (\t,(p,v) => insert p v t) (uncurry mk elem_code_head) elem_code_tail

  pure $ tree_to_parser b_tree


text:
module Test.JSON

import JS
import JS.JSON
import Hedgehog
import Test.Object

import Generics.Derive

%language ElabReflection

%runElab derive "Test.Object.Address" [ToJSON1,FromJSON1]

roundTrip : Eq a => FromJSON a => ToJSON a => Show a => Gen a -> Property
roundTrip g = property $ do v <- forAll g
                            let enc = encode v
                            footnote enc
                            Right v === decode enc

--------------------------------------------------------------------------------
--          Fast Eq for Nat
--------------------------------------------------------------------------------

||| The default Eq for Nat runs in O(n), which leads to stack overflows
||| for large Nats
export
[FastNatEq] Eq Nat where
  (==) = (==) `on` natToInteger

||| The default Ord for Nat runs in O(n), which leads to stack overflows
||| for large Nats
export
[FastNatOrd] Ord Nat using FastNatEq where
  compare = compare `on` natToInteger

--------------------------------------------------------------------------------
--          Sum Type
--------------------------------------------------------------------------------

data Sum : (a : Type) -> Type where
  Con1 : (name : String) -> (age : Bits32) -> (female : Bool) -> Sum a
  Con2 : (treasure : List a) -> (weight : Bits64) -> Sum a
  Con3 : (foo : Maybe a) -> (bar : Either Bool a) -> Sum a

%runElab derive "Sum" [Generic,Meta,Show,Eq,ToJSON,FromJSON]

--------------------------------------------------------------------------------
--          Generators
--------------------------------------------------------------------------------

bits8All : Gen Bits8
bits8All = bits8 $ linear 0 255

bits16All : Gen Bits16
bits16All = bits16 $ exponential 0 65535

bits32All : Gen Bits32
bits32All = bits32 $ exponential 0 4294967295

bits64All : Gen Bits64
bits64All = bits64 $ exponential 0 18446744073709551615

unicode16 : Gen Char
unicode16 = charc '\0' '\65535'

doubleE100 : Gen Double
doubleE100 = double $ exponentialFrom 0 (-1.0e100) 1.0e100

intAll : Gen Int
intAll = int $ exponential (-9223372036854775808) 9223372036854775807

integer128 : Gen Integer
integer128 = integer $ exponentialFrom 0 (-0x100000000000000000000000000000000) 0x100000000000000000000000000000000

nat128 : Gen Nat
nat128 = nat $ exponential @{FastNatOrd} 0 0x100000000000000000000000000000000

list20 : Gen a -> Gen (List a)
list20 = list (linear 0 20)

list1_20 : Gen a -> Gen (List1 a)
list1_20 = list1 (linear 1 20)

optional : Gen a -> Gen (Optional a)
optional = map maybeToOptional . maybe

string20 : Gen Char -> Gen String
string20 = string $ linear 0 20

string20Ascii : Gen String
string20Ascii = string20 ascii

string20Unicode16 : Gen String
string20Unicode16 = string20 unicode16

array20 : Gen a -> Gen (IArray a)
array20 = map fromList . list20

vect13 : Gen a -> Gen (Vect 13 a)
vect13 = vect 13

sum : Gen (Sum Int)
sum = map to $ sop $ MkPOP [ [ string20 alphaNum, bits32All, bool ]
                           , [ list20 intAll, bits64All ]
                           , [ maybe intAll, either bool intAll ]
                           ]

--------------------------------------------------------------------------------
--          Properties
--------------------------------------------------------------------------------

prop_unit : Property
prop_unit = roundTrip $ pure ()

prop_array : Property
prop_array = roundTrip $ array20 bits8All

prop_bits8 : Property
prop_bits8 = roundTrip bits8All

prop_bits16 : Property
prop_bits16 = roundTrip bits16All

prop_bits32 : Property
prop_bits32 = roundTrip bits32All

prop_bits64 : Property
prop_bits64 = roundTrip bits64All

prop_bool : Property
prop_bool = roundTrip bool

prop_char : Property
prop_char = roundTrip unicode16

prop_double : Property
prop_double = roundTrip doubleE100

prop_either : Property
prop_either = roundTrip $ either bits8All ascii

prop_int : Property
prop_int = roundTrip intAll

prop_integer : Property
prop_integer = roundTrip integer128

prop_list : Property
prop_list = roundTrip $ list20 bits8All

prop_list1 : Property
prop_list1 = roundTrip $ list1_20 unicode16

prop_maybe : Property
prop_maybe = roundTrip $ maybe (either bool bits32All)

prop_nat : Property
prop_nat = roundTrip @{FastNatEq} nat128

prop_np : Property
prop_np = roundTrip $ np [ integer128, bool, unicode16, maybe string20Ascii ]

prop_ns : Property
prop_ns = roundTrip $ ns [ integer128, bool, unicode16, maybe string20Ascii ]

prop_optional : Property
prop_optional = roundTrip $ optional bits64All

prop_pair : Property
prop_pair = roundTrip [| (,) (list1_20 bool) (maybe ascii) |]

prop_string : Property
prop_string = roundTrip $ string20 unicode

prop_sum : Property
prop_sum = roundTrip sum

prop_vect : Property
prop_vect = roundTrip $ vect13 intAll

prop_address : Property
prop_address = roundTrip addresses

export
test : IO ()
test = ignore . checkGroup . withTests 1000 $ MkGroup "JSON" [
            ("prop_address", prop_address)
          , ("prop_array", prop_array)
          , ("prop_bits8", prop_bits8)
          , ("prop_bits16", prop_bits16)
          , ("prop_bits32", prop_bits32)
          , ("prop_bits64", prop_bits64)
          , ("prop_bool", prop_bool)
          , ("prop_char", prop_char)
          , ("prop_double", prop_double)
          , ("prop_either", prop_either)
          , ("prop_int", prop_int)
          , ("prop_integer", prop_integer)
          , ("prop_list", prop_list)
          , ("prop_list1", prop_list1)
          , ("prop_maybe", prop_maybe)
          , ("prop_nat", prop_nat)
          , ("prop_np", prop_np)
          , ("prop_ns", prop_ns)
          , ("prop_optional", prop_optional)
          , ("prop_pair", prop_pair)
          , ("prop_string", prop_string)
          , ("prop_sum", prop_sum)
          , ("prop_unit", prop_unit)
          , ("prop_vect", prop_vect)
          ]


text:
1 f : (1 _ : Nat) -> Nat
f x = S x -- + 1 -- !! Wow, `+` is not linear! I can't use it here!

g : Nat -> Nat
g x = f x

h : Nat -> Nat
h x = let fx = f x in ?foo -- fx is linear because the whole function is!

--- Passing the functions ---

-- Like `f` but without `1` quantity on the whole function.
f' : (1 _ : Nat) -> Nat
f' x = S x

fi : (1 f : (1 _ : Nat) -> Nat) -> Nat -> Nat
fi f x = let fx = f x in fx -- ?foo_fi -- fx is linear like above

fi_f : Nat -> Nat
fi_f = fi f

fi_f' : Nat -> Nat
fi_f' = fi f'

fj : (f : (1 _ : Nat) -> Nat) -> Nat -> Nat
fj f x = let fx = f x in ?foo_fj -- fx is NOT linear

fj_f' : Nat -> Nat
fj_f' = fj f'

useTwice : Nat -> Nat -> Nat
useTwice x y = let fx = f x
                   fy = f y
                   xx = f
               in ?foo_twice

fj_f : Nat -> Nat
fj_f = fj ?foo_f -- if we try `f` here, we get "trying to use f in non-linear context"

------

local : Nat -> Nat
local x = let 1 foj : (1 _ : Nat) -> Nat
              foj x = S x in
          let 1 foy : (1 _ : Nat) -> Nat
              foy = foj in
          --let 1 fox = foj in
          x
  where
    1 foo : (1 _ : Nat) -> Nat
    foo x = S x

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Language.LSP.Message.ServerCapabilities

import Data.SortedMap
import Language.JSON
import Language.LSP.Message.CallHierarchy
import Language.LSP.Message.Cancel
import Language.LSP.Message.CodeAction
import Language.LSP.Message.CodeLens
import Language.LSP.Message.Command
import Language.LSP.Message.Completion
import Language.LSP.Message.Declaration
import Language.LSP.Message.Definition
import Language.LSP.Message.Derive
import Language.LSP.Message.Diagnostics
import Language.LSP.Message.DocumentColor
import Language.LSP.Message.DocumentFormatting
import Language.LSP.Message.DocumentHighlight
import Language.LSP.Message.DocumentLink
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.FoldingRange
import Language.LSP.Message.Hover
import Language.LSP.Message.Implementation
import Language.LSP.Message.LinkedEditingRange
import Language.LSP.Message.Location
import Language.LSP.Message.Markup
import Language.LSP.Message.Method
import Language.LSP.Message.Moniker
import Language.LSP.Message.Progress
import Language.LSP.Message.References
import Language.LSP.Message.Registration
import Language.LSP.Message.RegularExpressions
import Language.LSP.Message.Rename
import Language.LSP.Message.SelectionRange
import Language.LSP.Message.SemanticTokens
import Language.LSP.Message.SignatureHelp
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Trace
import Language.LSP.Message.Utils
import Language.LSP.Message.Window
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record FileOperationsServerCapabilities where
  constructor MkFileOperationsServerCapabilities
  didCreate  : Maybe FileOperationRegistrationOptions
  willCreate : Maybe FileOperationRegistrationOptions
  didRename  : Maybe FileOperationRegistrationOptions
  willRename : Maybe FileOperationRegistrationOptions
  didDelete  : Maybe FileOperationRegistrationOptions
  willDelete : Maybe FileOperationRegistrationOptions
%runElab deriveJSON defaultOpts `{{FileOperationsServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record WorkspaceServerCapabilities where
  constructor MkWorkspaceServerCapabilities
  workspaceFolders : Maybe WorkspaceFoldersServerCapabilities
  fileOperations   : Maybe FileOperationsServerCapabilities
%runElab deriveJSON defaultOpts `{{WorkspaceServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record ServerCapabilities where
  constructor MkServerCapabilities
  textDocumentSync                 : Maybe (TextDocumentSyncOptions .+. TextDocumentSyncKind)
  completionProvider               : Maybe CompletionOptions
  hoverProvider                    : Maybe (Bool .+. HoverOptions)
  signatureHelpProvider            : Maybe SignatureHelpOptions
  declarationProvider              : Maybe (Bool .+. DefinitionOptions)
  typeDefinitionProvider           : Maybe (Bool .+. TypeDefinitionOptions .+. TypeDefinitionRegistrationOptions)
  implementationProvider           : Maybe (Bool .+. ImplementationOptions .+. ImplementationRegistrationOptions)
  referencesProvider               : Maybe (Bool .+. ReferenceOptions)
  documentHighlightProvider        : Maybe (Bool .+. DocumentHighlightOptions)
  documentSymbolProvider           : Maybe (Bool .+. DocumentSymbolOptions)
  codeActionProvider               : Maybe (Bool .+. CodeActionOptions)
  codeLensProvider                 : Maybe CodeLensOptions
  documentLinkProvider             : Maybe DocumentLinkOptions
  colorProvider                    : Maybe (Bool .+. DocumentColorOptions .+. DocumentColorRegistrationOptions)
  documentFormattingProvider       : Maybe (Bool .+. DocumentFormattingOptions)
  documentRangeFormattingProvider  : Maybe (Bool .+. DocumentRangeFormattingOptions)
  documentOnTypeFormattingProvider : Maybe DocumentOnTypeFormattingOptions
  renameProvider                   : Maybe (Bool .+. RenameOptions)
  foldingRangeProvider             : Maybe (Bool .+. FoldingRangeOptions .+. FoldingRangeRegistrationOptions)
  executeCommandProvider           : Maybe ExecuteCommandOptions
  selectionRangeProvider           : Maybe (Bool .+. SelectionRangeOptions .+. SelectionRangeRegistrationOptions)
  linkedEditingRangeProvider       : Maybe (Bool .+. LinkedEditingRangeOptions .+. LinkedEditingRangeRegistrationOptions)
  callHierarchyProvider            : Maybe (Bool .+. CallHierarchyOptions .+. CallHierarchyRegistrationOptions)
  semanticTokensProvider           : Maybe (SemanticTokensOptions .+. SemanticTokensRegistrationOptions)
  monikerProvider                  : Maybe (Bool .+. MonikerOptions .+. MonikerRegistrationOptions)
  workspaceSymbolProvider          : Maybe (Bool .+. WorkspaceSymbolOptions)
  workspace                        : Maybe WorkspaceServerCapabilities
  experimental                     : Maybe JSON
%runElab deriveJSON defaultOpts `{{ServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record ServerInfo where
  constructor MkServerInfo
  name    : String
  version : Maybe String
%runElab deriveJSON defaultOpts `{{ServerInfo}}


text:
module Dart.FFI.Enums

import Dart.Core

public export
interface IsEnum a where

namespace Enum
  %inline
  public export
  equals : IsEnum a => a -> a -> Bool
  equals x y = toBool (prim__dart_eq x y)

export
IsEnum a => Eq a where
  (==) = Enum.equals


text:
module Main

import lib.Library1
import lib.Library2

main : IO ()
main = putStrLn (salute1 ++ "\n" ++ salute2)


text:
module Crypto.Curve.XCurves

-- This doesn't implement the Point interface because I can't be bothered will implementing
-- point addition. This module is for DH strictly.

import Data.Bits
import Data.Bool.Xor
import Data.Vect
import Utils.Bytes
import Utils.Misc

data XCurvesParameter : (n : Nat) -> Type where
  XCParam : {n : Nat} ->
            (bits : Nat) ->
            (u : Integer) ->
            (a24 : Integer) ->
            (scalar_decoder : Vect n Bits8 -> Integer) ->
            (prime : Integer) ->
            XCurvesParameter n

cswap : Integer -> Integer -> Integer -> (Integer, Integer)
cswap swap x2 x3 =
  let dummy = (0 - swap) .&. (x2 `xor` x3)
  in (x2 `xor` dummy, x3 `xor` dummy)

mul_go : {n : Nat} -> XCurvesParameter n -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Integer -> Nat ->
         (Integer, Integer, Integer, Integer, Integer)
mul_go param@(XCParam _ _ a24 _ prime) x1 x2 z2 x3 z3 swap k t =
  let mul = (\a,b => mul_mod a b prime)
      pow = (\a,b => pow_mod a b prime)
      k_t = (shiftR k t) .&. 1
      swap' = xor swap k_t
      (x2, x3) = cswap swap' x2 x3
      (z2, z3) = cswap swap' z2 z3
      a = x2 + z2
      aa = a `mul` a
      b = x2 - z2
      bb = b `mul` b
      e = aa - bb
      c = x3 + z3
      d = x3 - z3
      da = d `mul` a
      cb = c `mul` b
      x3 = pow (da + cb) 2
      z3 = x1 `mul` (pow (da - cb) 2)
      x2 = aa `mul` bb
      z2 = e `mul` (aa + (a24 `mul` e))
  in case t of
       Z => (x2, x3, z2, z3, k_t)
       S t' => mul_go param x1 x2 z2 x3 z3 k_t k t'

public export
mul : {n : Nat} -> XCurvesParameter n -> Vect n Bits8 -> Vect n Bits8 -> Maybe (Vect n Bits8)
mul {n} param@(XCParam bits _ a24 decode prime) k u =
  let u' = le_to_integer u
      k' = decode k
      (x2, x3, z2, z3, swap) = mul_go param u' 1 0 u' 1 0 k' (minus bits 1)
      (x2', x3') = cswap swap x2 x3
      (z2', z3') = cswap swap z2 z3
      beta = pow_mod z2' (prime-2) prime
      secret = mul_mod x2' beta prime
  in guard (secret /= 0) *> (pure $ integer_to_le _ secret )

generator : {n : Nat} -> XCurvesParameter n -> Vect n Bits8
generator (XCParam _ u _ _ _) = integer_to_le _ u

public export
derive_public_key : {n : Nat} -> XCurvesParameter n -> Vect n Bits8 -> Maybe (Vect n Bits8)
derive_public_key param k = mul param k $ generator param

decode_scalar_25519 : Vect 32 Bits8 -> Integer
decode_scalar_25519 =
  le_to_integer
  . updateAt 0  (.&. 248)
  . updateAt 31 (.&. 127)
  . updateAt 31 (.|.  64)

decode_scalar_448 : Vect 56 Bits8 -> Integer
decode_scalar_448 =
  le_to_integer
  . updateAt 0  (.&. 252)
  . updateAt 55 (.|. 128)

public export
x25519 : XCurvesParameter 32
x25519 = XCParam 255 9 121665 decode_scalar_25519 $ (bit 255) - 19

public export
x448 : XCurvesParameter 56
x448 = XCParam 448 5 39081 decode_scalar_448 $ (bit 448) - (bit 224) - 1


text:
module Parser.Rule.Package

import public Parser.Lexer.Package

import Data.List
import Data.List1

import Core.Name.Namespace

%default total

public export
Rule : Type -> Type
Rule = Grammar () Token True

public export
EmptyRule : Type -> Type
EmptyRule = Grammar () Token False

export
equals : Rule ()
equals = terminal "Expected equals" $
                  \case
                    Equals => Just ()
                    _ => Nothing

export
lte : Rule ()
lte = terminal "Expected <=" $
               \case
                 LTE => Just ()
                 _ => Nothing

export
gte : Rule ()
gte = terminal "Expected >=" $
               \case
                 GTE => Just ()
                 _ => Nothing

export
lt : Rule ()
lt = terminal "Expected <=" $
              \case
                LT => Just ()
                _ => Nothing

export
gt : Rule ()
gt = terminal "Expected >=" $
              \case
                GT => Just ()
                _ => Nothing

export
eqop : Rule ()
eqop = terminal "Expected ==" $
                \case
                  EqOp => Just ()
                  _ => Nothing

export
andop : Rule ()
andop = terminal "Expected &&" $
                 \case
                   AndOp => Just ()
                   _ => Nothing

export
eoi : Rule ()
eoi = terminal "Expected end of input" $
               \case
                 EndOfInput => Just ()
                 _ => Nothing

export
exactProperty : String -> Rule String
exactProperty p = terminal ("Expected property " ++ p) $
                           \case
                             DotSepIdent Nothing p' =>
                               if p == p' then Just p else Nothing
                             _ => Nothing

export
stringLit : Rule String
stringLit = terminal "Expected string" $
                     \case
                       StringLit str => Just str
                       _ => Nothing

export
integerLit : Rule Integer
integerLit = terminal "Expected integer" $
                      \case
                        IntegerLit i => Just i
                        _ => Nothing

export
namespacedIdent : Rule (Maybe Namespace, String)
namespacedIdent = terminal "Expected namespaced identifier" $
                           \case
                             DotSepIdent ns n => Just (ns, n)
                             _ => Nothing

export
moduleIdent : Rule ModuleIdent
moduleIdent = terminal "Expected module identifier" $
                       \case
                         DotSepIdent ns m =>
                           Just $ nsAsModuleIdent $
                                  mkNestedNamespace ns m
                         _ => Nothing

export
packageName : Rule String
packageName = terminal "Expected package name" $
                       \case
                         DotSepIdent Nothing str =>
                           if isIdent AllowDashes str
                              then Just str
                              else Nothing
                         _ => Nothing

export
dot' : Rule ()
dot' = terminal "Expected dot" $
                \case
                  Dot => Just ()
                  _ => Nothing

sep' : Rule ()
sep' = terminal "Expected separator" $
                \case
                  Separator => Just ()
                  _ => Nothing

export
sep : Rule t -> Rule (List t)
sep rule = forget <$> sepBy1 sep' rule


text:
module Basics

trivial : Elab ()
trivial = do compute
             g <- snd <$> getGoal
             case g of
                  `((=):Type) => do fill `(Var (UN "Refl"))
                                    solve
                  `(():Type) => do fill `(():())
                                   solve
                  otherGoal  => fail [TermPart otherGoal,
                                      TextPart "is not trivial"
                                     ]

|||
||| Enumerated Types
|||

||| Days of the Week
|||
data Day : Type where
     Monday    : Day
     Tuesday   : Day
     Wednesday : Day
     Thursday  : Day
     Friday    : Day
     Saturday  : Day
     Sunday    : Day

next_weekday : (d : Day) -> Day
next_weekday d = case d of
             Monday    => Tuesday
             Tuesday   => Wednesday
             Wednesday => Thursday
             Thursday  => Friday
             Friday    => Monday
             Saturday  => Monday
             Sunday    => Monday

||| next_weekeday assertions
is_next_weekday1 : (d : Day) -> next_weekday Friday = Monday
is_next_weekday1 d = Refl

is_next_weekday2 : (d : Day) -> next_weekday (next_weekday Saturday) = Tuesday
is_next_weekday2 d = Refl

test_next_weekday : (next_weekday (next_weekday Saturday)) = Tuesday
test_next_weekday = Refl

||| Booleans
|||
data Boolean : Type where
     Top : Boolean
     Bot : Boolean

negb : (b : Boolean) -> Boolean
negb b = case b of
     Top => Bot
     Bot => Top

andb : (b1,b2 : Boolean) -> Boolean
andb b1 b2 = case b1 of
     Top => b2
     Bot => Bot

orb : (b1,b2 : Boolean) -> Boolean
orb b1 b2 = case b1 of
    Top => Top
    Bot => b2

||| orb assertions
test_orb1 : (orb Top Bot) = Top
test_orb1 = Refl

test_orb2 : (orb Bot Bot) = Bot
test_orb2 = Refl

test_orb3 : (orb Bot Top) = Top
test_orb3 = Refl

test_orb4 : (orb Top Top) = Top
test_orb4 = Refl

||| Exercise: 1 star (nandb)
||| Complete the definition of the following function, then make sure that the
|||   assertions below can each be verified by Idris.
|||
||| This function should return true if either or both of its inputs are false.
|||
nandb : (b1,b2 : Boolean) -> Boolean
nandb b1 b2 = (negb (andb b1 b2))

||| nandb assertions
test_nandb1 : (nandb Top Bot) = Top
test_nandb1 = Refl

test_nandb2 : (nandb Bot Bot) = Top
test_nandb2 = Refl

test_nandb3 : (nandb Bot Top) = Top
test_nandb3 = Refl

test_nandb4 : (nandb Top Top) = Bot
test_nandb4 = Refl

||| Exercise: 1 star (andb3)
||| Do the same for the andb3 function below. This function should return true
|||   when all of its inpouts are true, and false otherwise.
|||
andb3 : (b1,b2,b3 : Boolean) -> Boolean
andb3 b1 b2 b3 = (andb b1 (andb b2 b3))

||| andb3 assertions
test_andb31 : (andb3 Top Top Top) = Top
test_andb31 = Refl

test_andb32 : (andb3 Bot Top Top) = Bot
test_andb32 = Refl

test_andb33 : (andb3 Top Bot Top) = Bot
test_andb33 = Refl

test_andb34 : (andb3 Top Top Bot) = Bot
test_andb34 = Refl

|||
||| Function Types
|||

||| Numbers
|||

||| data Nats : Type where
|||      O : Nats
|||      S : Nats -> Nats
pred : (n : Nat) -> Nat
pred n = case n of
     Z   => Z
     S k => k

minusTwo : (n : Nat) -> Nat
minusTwo n = case n of
         Z       => Z
         S Z     => Z
         S (S k) => k

evenb : (n : Nat) -> Boolean
evenb n = case n of
      Z       => Top
      S Z     => Bot
      S (S k) => Top

oddb : (n : Nat) -> Boolean
oddb n = negb (evenb n)

||| oddb assertions
test_oddb1 : (oddb (S Z)) = Top
test_oddb1 = Refl

test_oddb2 : (oddb (S (S (S (S Z))))) = Bot
test_oddb2 = Refl

plus' : (n,m : Nat) -> Nat
plus' n m = case n of
      Z   => m
      S k => S (plus' k m)

mult' : (n,m : Nat) -> Nat
mult' n m = case n of
      Z   => Z
      S k => plus m (mult' k m)

minus' : (n,m : Nat) -> Nat
minus' n m = case (n,m) of
       (Z,   _  ) => Z
       (S _, Z  ) => n
       (S k, S j) => minus k j

exp : (base,power : Nat) -> Nat
exp base power = case power of
    Z   => S Z
    S p => mult' base (exp base p)

||| Exercise: 1 star (factorial)
||| Translate the standard factorial function into Idris.
|||
factorial : (n : Nat) -> Nat
factorial n = case n of
          Z   => S Z
          S Z => S Z
          S k => (mult' n (factorial k))

||| factorial assertions
test_factorial1 : (factorial 3) = 6
test_factorial1 = Refl

test_factorial2 : (factorial 5) = (mult' 10 12)
test_factorial2 = Refl

beq_nat : (n,m : Nat) -> Boolean
beq_nat n m = case n of
        Z => case m of
          Z   => Top
          S j => Bot
        S k => case m of
          Z   => Bot
          S j => beq_nat k j

ble_nat : (n,m : Nat) -> Boolean
ble_nat n m = case n of
        Z   => Top
        S k => case m of
            Z   => Bot
            S j => ble_nat k j

||| ble_nat assertions
test_ble_nat1 : (ble_nat 2 2) = Top
test_ble_nat1 = Refl

test_ble_nat2 : (ble_nat 2 4) = Top
test_ble_nat2 = Refl

test_ble_nat3 : (ble_nat 4 2) = Bot
test_ble_nat3 = Refl

||| Exercise: 2 stars (blt_nat)
||| The blt_nat function test natural numbers for less-than, yielding a boolean.
|||
blt_nat : (n,m : Nat) -> Boolean
blt_nat n m = case (beq_nat n m) of
        Top => Bot
        Bot => (ble_nat n m)

||| blt_nat assertions
test_blt_nat1 : (blt_nat 2 2) = Bot
test_blt_nat1 = Refl

test_blt_nat2 : (blt_nat 2 4) = Top
test_blt_nat2 = Refl

test_blt_nat3 : (blt_nat 4 2) = Bot
test_blt_nat3 = Refl

|||
||| Proof by Simplification
|||

plus_Z_n : {n : Nat} -> 0 + n = n
plus_Z_n = ?plus_Z_n

max_stars_repo_name: abbottk/idris-sf

max_issues_repo_name: abbottk/idris-sf

max_forks_repo_name: abbottk/idris-sf