text:
||| Combat logic for _Bautzen1945_
||| Section 8
module Bautzen.Game.Combat

import Bautzen.Combats
import Bautzen.GameUnit
import Bautzen.Game.Command
import Bautzen.Game.Core
import Bautzen.Odds
import Bautzen.Pos
import Bautzen.Terrain

import Data.List.Extra
import Prelude.Either

import Data.Nat
import Data.Nat.DivMod
import Data.List as L
import Data.Vect as V

-- section 8.1
-- Those are generalities about the combat that cannot be implemented alone

-- section 8.2

||| Start resolving an attack from given list of `attackers` to given list of `defenders`.
|||
||| This computes the base factors for the combat, without taking into account the support
||| provided by HQs, Artillery, etc. nor the change to odds coming from terrain...
||| * see section 8.2, alinea 3
|||
||| @attackers the group of units attacking
||| @defenders the group of defending units
attack : (attackers : List GameUnit) -> (defenders : List GameUnit) -> RawOdds
attack attackers defenders = MkRawOdds atk def
  where
    atk : Nat
    atk = sum $ map attackCapacity attackers

    def : Nat
    def = sum $ map defenseCapacity defenders

||| Update some `odds` with all relevant support factors.
|||
||| * see section 8.2, alinea 3
||| * see section 9.2
|||
||| @attackSupport list of units supporting the attack
||| @defenseSupport list of units supporting the defense
||| @baseOdds the base odds without support
support : (attackSupport : List GameUnit) -> (defenseSupport : List GameUnit) -> (baseOdds : RawOdds) -> RawOdds
support attackSupport defenseSupport baseOdds@(MkRawOdds atk def) = baseOdds <+> MkRawOdds atkSupport defSupport
  where
    atkSupport : Nat
    atkSupport = min atk $ sum (map supportCapacity attackSupport)

    defSupport : Nat
    defSupport = min def $ sum (map supportCapacity defenseSupport)

||| Given some odds and the result of 6-sided dice, provide combat outcome in the form of
||| a pair of numbers representing step loss for each side.
|||
||| * section 8.2, alinea 6
|||
||| @odds the final odds of the combat
||| @modifiedDiceRoll the result of the dice, with modifiers applied
resolve : (odds : Odds) -> (modifiedDiceRoll : Fin 8) -> Losses
resolve odds dice = dice `index` (toFin odds `index` CombatTable)

findUnit : String -> { positions : List (GameUnit, Pos) } -> Maybe (GameUnit, Pos)
findUnit n {positions} = find' (\ (u, p) => fullName u == n) positions

findUnits : List String -> (positions : List (GameUnit, Pos)) -> Either GameError (List (GameUnit, Pos))
findUnits names positions =
  case partitionEithers units of
       ([], us) => Right us
       (errs, _) => Left $ NoSuchUnits errs
  where
    units : List (Either String (GameUnit, Pos))
    units = map (\ n => case findUnit n {positions} of
                             Nothing => Left n
                             Just up => Right up) names

sameSide : Side -> (GameUnit, Pos) -> Bool
sameSide curSide (u, _) = side (nation u) == curSide

validateAttackers : (side : Side) -> (units : List (GameUnit, Pos)) -> (gameMap : Map)
                  -> (attackers : List (GameUnit, Pos)) -> (target : Pos)
                  -> Either GameError (List (GameUnit, Pos))
validateAttackers curSide units gameMap attackers target =
  if not (all (sameSide curSide) attackers)
  then Left (NotYourTurn curSide)
  else Right attackers

adjacentTo : Pos -> (GameUnit, Pos) -> Bool
adjacentTo target (_, p) = distance p target /= 1

checkAttackersAreAdjacentToTarget : (attackers : List (GameUnit, Pos)) -> (target : Pos)
                                  -> Either GameError (List (GameUnit, Pos))
checkAttackersAreAdjacentToTarget attackers target =
  case filter (adjacentTo target) attackers of
    [] => Right attackers
    errs => Left (NotAdjacentTo (map fst errs) target)

samePosition : Pos -> (GameUnit, Pos) -> Bool
samePosition target (_, p) = p == target

validateDefenders : (side : Side) -> (positions : List (GameUnit, Pos)) -> (gameMap : Map)
                  -> (target : Pos)
                  -> Either GameError (List (GameUnit, Pos))
validateDefenders attackerSide positions gameMap target =
  case filter (samePosition target) positions of
    [] => Left $ NothingToAttack target
    defenders => if any (sameSide attackerSide) defenders
                 then Left $ AttackingOwnUnits (map fst defenders) target
                 else Right defenders

||| Start a combat with given units attacking given hex.
export
attackWith : (side : Side) -> (units : List (GameUnit, Pos)) -> (gameMap : Map)
           -> (unitNames : List String) -> (target : Pos)
           -> Either GameError Event
attackWith side units gameMap unitNames target = do
  attackUnits <- findUnits unitNames units
  attackers <- validateAttackers side units gameMap attackUnits target
  -- section 8.1
  attackers' <- checkAttackersAreAdjacentToTarget attackers target
  defenders <- validateDefenders side units gameMap target
  pure $ CombatEngaged attackers defenders target

-- TODO units cannot be part of an attack twice

-- Support

checkSupportingUnits : (units : List (GameUnit, Pos))
                     -> Either GameError (List (GameUnit, Pos))
checkSupportingUnits units =
  let notSupporting = filter (not . isSupportingUnit . fst) units
  in case notSupporting of
       [] => Right units
       ns => Left $ NotSupportingUnits (map fst ns)

supportInRangeOf : (base : List (GameUnit, Pos)) -> (supporter: (GameUnit, Pos)) -> Bool
supportInRangeOf base (unit, pos) =
  let maxDistance = supportDistance unit
  in any (\ (u, p) => distance p pos <= maxDistance) base

checkSupportInRange : (base : List (GameUnit, Pos)) -> (supporters : List (GameUnit, Pos)) -> Either GameError (List (GameUnit, Pos))
checkSupportInRange base supporters =
  case filter (not . supportInRangeOf base) supporters of
    [] => Right supporters
    xs => Left $ NotInSupportRange (map fst xs)

hasNoHQ : List (GameUnit, Pos) -> (GameUnit, Pos) -> Bool
hasNoHQ base (u, _) = not (any (isHQFor u) $ map fst base)

checkChainOfCommand : (base : List (GameUnit, Pos)) -> (supporters : List (GameUnit, Pos)) -> Either GameError (List (GameUnit, Pos))
checkChainOfCommand base supporters =
  case filter (hasNoHQ base) hqs of
    [] => Right supporters
    xs => Left $ NotInChainOfCommand (map fst xs)
  where
    hqs : List (GameUnit, Pos)
    hqs = filter (isHQ . fst) supporters

validateSupport :  (supported : EngagedUnits)
                -> (supporters : List (GameUnit, Pos))
                -> Either GameError (List (GameUnit, Pos))
validateSupport (MkEngagedUnits base _ _) supporters =
  checkSupportingUnits supporters >>=
  checkSupportInRange base >>=
  checkChainOfCommand base

validateSupportUnits : (currentSide : Side) -> (supportedSide : Side)
                     -> (state : CombatState)
                     -> (units : List (GameUnit, Pos))
                     -> Either GameError (List (GameUnit, Pos))
validateSupportUnits currentSide supportedSide (MkCombatState _ atk def _) units =
  if (currentSide == supportedSide)
  then validateSupport atk units
  else validateSupport def units

||| Add support units to an _engaged_ combat.
|||
||| If successful, this will add some units to
|||
||| @currentSide the side whose turn it is to play, e.g the attacker's side
||| @supportSide the side which is expected to provide support
||| @units the positions and state of units on the map
||| @gameMap the map
||| @unitNames names of units providing support
||| @state overall state of the combat
export
supportWith : (currentSide : Side) -> (supportSide : Side)
           -> (units : List (GameUnit, Pos)) -> (gameMap : Map)
           -> (unitNames : List String)
           -> (state : CombatState)
           -> Either GameError Event
supportWith currentSide supportSide units gameMap unitNames state = do
  supportUnits <- findUnits unitNames units >>= validateSupportUnits currentSide supportSide state
  pure $ TacticalSupportProvided supportSide supportUnits

-- section 7.2
isSupportIn : Pos -> (GameUnit, Pos) -> Bool
isSupportIn hex (u, p) = p == hex &&  unitType u == SupplyColumn

findSupportColumn : (supportSide : Side) -> (hex : Pos) -> (units : List (GameUnit, Pos)) -> Either GameError (GameUnit, Pos)
findSupportColumn supportSide hex units =
  case find' (isSupportIn hex) units of
    Nothing => Left (NoSupplyColumnThere hex)
    Just sc => Right sc

--- section 7.2.1

neighboursUnits : Pos -> (GameUnit, Pos) -> Bool
neighboursUnits hex (u, p) = p == hex || (hex  `elem` neighbours p)

checkSCNeighboursEngagedUnits :
  List (GameUnit, Pos) -> (GameUnit, Pos) -> Either GameError (GameUnit, Pos)
checkSCNeighboursEngagedUnits base sc@(unit, hex) =
  if any (neighboursUnits hex) base
  then Right sc
  else Left (NotInSupportRange [unit] )

--- section 7.2.2

checkSomeUnitsAreInCommand :
  List (GameUnit, Pos) -> List (GameUnit, Pos) -> (GameUnit, Pos) -> Either GameError (GameUnit, Pos)
checkSomeUnitsAreInCommand base units sc =
  if any (underCommand units) (map Builtin.fst base)
  then Right sc
  else Left (NotInChainOfCommand [fst sc])

validateSC : EngagedUnits -> List (GameUnit, Pos) -> (GameUnit, Pos) -> Either GameError (GameUnit, Pos)
validateSC (MkEngagedUnits base _ _) units sc =
  checkSCNeighboursEngagedUnits base sc >>=
  checkSomeUnitsAreInCommand base units

validateSupportFromSC : (currentSide : Side) -> (supportSide : Side)
                      -> (state : CombatState)
                      -> (units : List (GameUnit, Pos))
                      -> (unit : (GameUnit, Pos))
                      -> Either GameError (GameUnit, Pos)
validateSupportFromSC currentSide supportSide (MkCombatState _ atk def _) units unit =
  if currentSide == supportSide
  then validateSC atk units unit
  else validateSC def units unit

||| Use a `SupplyColumn` type of unit as "Strategic" support fort the combat
|||
||| @currentSide the side whose turn it is to play, e.g the attacker's side
||| @supportSide the side which is expected to provide support
||| @units the positions and state of units on the map
||| @gameMap the map
||| @scLocation location of the supply column
||| @state overall state of the combat
useSupplyColumn : (currentSide : Side) -> (supportSide : Side)
           -> (units : List (GameUnit, Pos)) -> (gameMap : Map)
           -> (scLocation : Pos)
           -> (state : CombatState)
           -> Either GameError Event
useSupplyColumn currentSide supportSide units gameMap scLocation state = do
  unit <- findSupportColumn supportSide scLocation units >>= validateSupportFromSC currentSide supportSide state units
  pure $ SupplyColumnUsed supportSide scLocation

export
resolveCombat :
  (currentSide  : Side) -> (combat : CombatState)
  -> Either GameError Event
resolveCombat currentSide state@(MkCombatState combatHex (MkEngagedUnits atk tac strat) (MkEngagedUnits def tac' strat') losses) =
  let baseOdds = Combat.attack (map fst atk) (map fst def)
      supOdds = Combat.support (map fst tac) (map fst tac') baseOdds
      unmodOdds = odds supOdds
      shiftedOdds = (unmodOdds >>> strat) <<<  strat'
  in Right (CombatResolved state (resolve shiftedOdds 3)) -- need to handle dice rolling => store seed in game state

doLoseStep : (side : Side) -> (units : EngagedUnits) -> (losses : Nat) -> (unitName : String) -> Either GameError (GameUnit, Nat)
doLoseStep side (MkEngagedUnits base _ _) Z unitName = Left $ NoStepsToLose side
doLoseStep side (MkEngagedUnits base _ _) (S k) unitName = do
  case findUnit unitName {positions=base} of
    Nothing => Left $ NoSuchUnits [ unitName ]
    Just (u,p) => Right (u, k)

export
loseStep : (currentSide : Side) -> (lossSide : Side) -> (combat : CombatState)
         -> (unitName : String)
         -> Either GameError Event
loseStep _ side (MkCombatState _ _ _ Nothing) _ = Left $ NotYourTurn side -- TODO should never happen, error is a placeholder
loseStep currentSide lossSide (MkCombatState _ atk def (Just (al /> dl))) unitName =
  if currentSide == lossSide
  then do
    (u, k) <- doLoseStep lossSide atk al unitName
    pure $ StepLost lossSide u (k /> dl)
  else do
    (u, k) <- doLoseStep lossSide def dl unitName
    pure $ StepLost lossSide u (al /> k)

namespace CombatTest

  positions : List (GameUnit, Pos)
  positions = [ (GameUnit.p13_5dp, Hex 5 4)
              , (GameUnit.g21_20pz, Hex 4 4)
              , (GameUnit.g59_20pz, Hex 3 4)
              ]

  basic_odds_are_Sum_of_attack_over_sum_of_defense : attack [ GameUnit.g21_20pz ] [ Bautzen.GameUnit.p13_5dp ] = (MkRawOdds 6 4)
  basic_odds_are_Sum_of_attack_over_sum_of_defense = Refl

  adds_support_Factors_to_raw_odds : support [ GameUnit.p6l ] [ GameUnit.g20pz ] (MkRawOdds 6 7) =  (MkRawOdds 10 13)
  adds_support_Factors_to_raw_odds = Refl

  support_factors_can_excede_to_raw_odds : support [ GameUnit.p6l ] [ GameUnit.g20pz ] (MkRawOdds 6 4) =  (MkRawOdds 10 8)
  support_factors_can_excede_to_raw_odds = Refl

  fail_attack_if_names_do_not_exist : attackWith Axis CombatTest.positions TestMap [ "21/20Pz", "foo" ] (Hex 5 4) = Left (NoSuchUnits [ "foo" ])
  fail_attack_if_names_do_not_exist = Refl

  fail_attack_if_attacking_with_wrong_side : attackWith Axis CombatTest.positions TestMap [ "13/5DP" ] (Hex 5 4) = Left (NotYourTurn Axis)
  fail_attack_if_attacking_with_wrong_side = Refl

  -- fail_attack_if_not_adjacent_to_target_hex : attackWith Axis CombatTest.positions TestMap [ "59/20Pz", "21/20Pz" ] (Hex 5 4) = Left (NotAdjacentTo [ GameUnit.g59_20pz ] (Hex 5 4))
  -- fail_attack_if_not_adjacent_to_target_hex = Refl

  -- fail_attack_if_attacked_hex_is_empty : attackWith Axis CombatTest.positions TestMap [ "21/20Pz" ] (Hex 4 5) = Left (NothingToAttack (Hex 4 5))
  -- fail_attack_if_attacked_hex_is_empty = Refl

  -- fail_attack_if_attacked_units_Are_of_same_side_than_attacker : attackWith Axis CombatTest.positions TestMap [ "21/20Pz" ] (Hex 3 4) = Left (AttackingOwnUnits [ GameUnit.g59_20pz ] (Hex 3 4))
  -- fail_attack_if_attacked_units_Are_of_same_side_than_attacker = Refl

  combatState : CombatState
  combatState = MkCombatState (Hex 5 4)
                (MkEngagedUnits [ (GameUnit.g21_20pz, Hex 4 4) ] [] 0)
                (MkEngagedUnits [ (GameUnit.p13_5dp, Hex 5 4) ] [] 0)
                Nothing

  fail_support_if_unit_not_HQ_or_arty :
    supportWith Axis Axis CombatTest.positions TestMap [ "59/20Pz" ] CombatTest.combatState = Left (NotSupportingUnits [ GameUnit.g59_20pz ])
  fail_support_if_unit_not_HQ_or_arty = Refl

  -- fail_support_if_attacker_hq_not_in_support_range :
  --   supportWith Axis Axis ((GameUnit.g20pz, Hex 1 1) :: CombatTest.positions) TestMap [ "HQ/20Pz" ] CombatTest.combatState = Left (NotInSupportRange [ GameUnit.g20pz ])
  -- fail_support_if_attacker_hq_not_in_support_range = Refl

  -- fail_support_if_hq_cannot_command_unit :
  --   supportWith Axis Axis ((GameUnit.gBrgPzG, Hex 3 3) :: CombatTest.positions) TestMap [ "HQ/BrgPzG" ] CombatTest.combatState = Left (NotInChainOfCommand [ GameUnit.gBrgPzG ])
  -- fail_support_if_hq_cannot_command_unit = Refl

  -- can_support_with_arty_given_its_in_range :
  --   supportWith Axis Axis ((GameUnit.g777Arty, Hex 1 1) :: CombatTest.positions) TestMap [ "777" ] CombatTest.combatState = Right (TacticalSupportProvided Axis [ (GameUnit.g777Arty, Hex 1 1) ])
  -- can_support_with_arty_given_its_in_range = Refl

  fail_to_use_supply_column_if_no_sc_at_location :
    useSupplyColumn Axis Axis ((GameUnit.gSupplyColumn, Hex 5 3) :: CombatTest.positions) TestMap (Hex 5 4) CombatTest.combatState = Left (NoSupplyColumnThere (Hex 5 4))
  fail_to_use_supply_column_if_no_sc_at_location = Refl

  -- fail_to_use_supply_column_if_sc_not_neighbour_to_support_hex :
  --   useSupplyColumn Axis Axis ((GameUnit.gSupplyColumn, Hex 5 2) :: CombatTest.positions) TestMap (Hex 5 2) CombatTest.combatState = Left (NotInSupportRange [GameUnit.gSupplyColumn])
  -- fail_to_use_supply_column_if_sc_not_neighbour_to_support_hex = Refl

  -- fail_to_use_supply_column_if_units_are_not_commanded :
  --     useSupplyColumn Axis Axis ((GameUnit.gSupplyColumn, Hex 5 3) :: CombatTest.positions) TestMap (Hex 5 3) CombatTest.combatState = Left (NotInChainOfCommand [GameUnit.gSupplyColumn])
  -- fail_to_use_supply_column_if_units_are_not_commanded = Refl

  -- use_supply_column_returns_supply_column_used_event :
  --     useSupplyColumn Axis Axis ((GameUnit.g20pz, Hex 2 2) :: (GameUnit.gSupplyColumn, Hex 4 3) :: CombatTest.positions) TestMap (Hex 4 3) CombatTest.combatState = Right (SupplyColumnUsed Axis (Hex 4 3))
  -- use_supply_column_returns_supply_column_used_event = Refl

  lossState : CombatState
  lossState = record { losses = Just (1 /> 0) } CombatTest.combatState

  fail_to_lose_step_if_unit_is_not_engaged :
    loseStep Axis Axis CombatTest.lossState "foo" = Left (NoSuchUnits ["foo"])
  fail_to_lose_step_if_unit_is_not_engaged = Refl

  fail_to_lose_step_if_no_steps_to_lose :
    loseStep Axis Allies CombatTest.lossState "13/5DP" = Left (NoStepsToLose Allies)
  fail_to_lose_step_if_no_steps_to_lose = Refl

  lose_steps_returns_step_loss_event :
    loseStep Axis Axis CombatTest.lossState "21/20Pz" = Right (StepLost Axis GameUnit.g21_20pz (0 /> 0))
  lose_steps_returns_step_loss_event = Refl


text:
module Compiler.ES.Codegen

import Compiler.Common
import Core.CompileExpr
import Core.Context
import Core.Directory
import Core.Options
import Data.List1
import Data.String
import Compiler.ES.Ast
import Compiler.ES.Doc
import Compiler.ES.ToAst
import Compiler.ES.TailRec
import Compiler.ES.State
import Libraries.Data.SortedMap
import Libraries.Utils.Hex
import Libraries.Data.String.Extra

import Data.Vect

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

-- Split at the given character and remove it.
breakDrop1 : Char -> String -> (String, String)
breakDrop1 c = mapSnd (drop 1) . break (== c)

-- Display a quoted list of strings.
stringList : List String -> String
stringList = fastConcat . intersperse "," . map show

--------------------------------------------------------------------------------
--          JS Strings
--------------------------------------------------------------------------------

-- Convert an Idris2 string to a Javascript String
-- by escaping most non-alphanumeric characters.
jsString : String -> String
jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'"
  where
    okchar : Char -> String
    okchar c = if (c >= ' ') && (c /= '\\')
                  && (c /= '"') && (c /= '\'') && (c <= '~')
                  then cast c
                  else case c of
                            '\0' => "\\0"
                            '\'' => "\\'"
                            '"' => "\\\""
                            '\r' => "\\r"
                            '\n' => "\\n"
                            other => "\\u{" ++ asHex (cast {to=Int} c) ++ "}"

||| Alias for Text . jsString
jsStringDoc : String -> Doc
jsStringDoc = Text . jsString

-- A name from the preamble (file `support.js`).
-- the given string is just prefixed with an underscore.
esName : String -> String
esName x = "_" ++ x

-- convert a string to a Javascript identifier
-- by escaping non-alphanumeric characters (except underscores).
jsIdent : String -> String
jsIdent s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar '_' = "_"
    okchar c = if isAlphaNum c
                  then cast c
                  else "x" ++ the (String) (asHex (cast {to=Int} c))

keywordSafe : String -> String
keywordSafe "var"    = "var$"
keywordSafe "switch" = "switch$"
keywordSafe "return" = "return$"
keywordSafe "const"  = "const$"
keywordSafe "function" = "function$"
keywordSafe s = s

--------------------------------------------------------------------------------
--          JS Name
--------------------------------------------------------------------------------

jsUserName : UserName -> String
jsUserName (Basic n) = keywordSafe $ jsIdent n
jsUserName (Field n) = "rf__" ++ jsIdent n
jsUserName Underscore = keywordSafe $ jsIdent "_"

jsName : Name -> String
jsName (NS ns n) = jsIdent (showNSWithSep "_" ns) ++ "_" ++ jsName n
jsName (UN n) = jsUserName n
jsName (MN n i) = jsIdent n ++ "_" ++ show i
jsName (PV n d) = "pat__" ++ jsName n
jsName (DN _ n) = jsName n
jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
jsName (Resolved i) = "fn__" ++ show i

jsNameDoc : Name -> Doc
jsNameDoc = Text . jsName

mainExpr : Name
mainExpr = MN "__mainExpression" 0

--------------------------------------------------------------------------------
--          Pretty Printing
--------------------------------------------------------------------------------

var : Var -> Doc
var (VName x) = jsNameDoc x
var (VLoc x)  = Text $ "$" ++ asHex x
var (VRef x)  = Text $ "$R" ++ asHex x

minimal : Minimal -> Doc
minimal (MVar v)          = var v
minimal (MProjection n v) = minimal v <+> ".a" <+> shown n

tag2es : Either Int Name -> Doc
tag2es (Left x)  = shown x
tag2es (Right x) = jsStringDoc $ show x

constant : Doc -> Doc -> Doc
constant n d = "const" <++> n <+> softEq <+> d <+> ";"

applyList : (lparen : Doc) -> (rparen : Doc) -> (sep : Doc) -> List Doc -> Doc
applyList l r sep ds = l <+> (concat $ intersperse sep ds) <+> r

conTags : List Doc -> List Doc
conTags as = zipWith (\i,a => hcat ["a",shown i,softColon,a]) [1..length as] as

applyObj : (args : List Doc) -> Doc
applyObj = applyList "{" "}" softComma

-- fully applied constructors are converted to JS objects with fields
-- labeled `a1`, `a2`, and so on for the given list of arguments.
-- a header field (label: `h`) is added holding either the index of
-- the data constructor used or a string representing the type constructor
-- in question.
--
-- Exceptions based on the given `ConInfo`:
-- `NIL` and `NOTHING`-like data constructors are represented as `{h: 0}`,
-- while `CONS`, `JUST`, and `RECORD` come without the header field.
applyCon : ConInfo -> (tag : Either Int Name) -> (args : List Doc) -> Doc
applyCon NIL     _ [] = "{h" <+> softColon <+> "0}"
applyCon NOTHING _ [] = "{h" <+> softColon <+> "0}"
applyCon CONS    _ as = applyObj (conTags as)
applyCon JUST    _ as = applyObj (conTags as)
applyCon RECORD  _ as = applyObj (conTags as)
applyCon _       t as = applyObj (("h" <+> softColon <+> tag2es t)::conTags as)

-- applys the given list of arguments to the given function.
app : (fun : Doc) -> (args : List Doc) -> Doc
app fun args = fun <+> applyList "(" ")" softComma args

-- invoke a function whose name is given as a `String` instead
-- of a `Doc`.
callFun : String -> List Doc -> Doc
callFun = app . Text

-- like `callFun` but with just a single argument
callFun1 : String -> Doc -> Doc
callFun1 fun = callFun fun . pure

-- throws an error in JS land with the given error message.
jsCrashExp : (msg : Doc) -> Doc
jsCrashExp = callFun1 (esName "crashExp")

-- creates a toplevel function definition of the form
-- ```javascript
--  function name(args) {
--    body
--  }
function : (name : Doc) -> (args : List Doc) -> (body : Doc) -> Doc
function n args body =
  "function" <++> app n args <+> SoftSpace <+> block body

--------------------------------------------------------------------------------
--          Primitives
--------------------------------------------------------------------------------

toBigInt : Doc -> Doc
toBigInt = callFun1 "BigInt"

fromBigInt : Doc -> Doc
fromBigInt = callFun1 "Number"

-- we need to use `BigInt` in JS if an integral type's
-- bit size is greater than 32.
useBigInt' : Int -> Bool
useBigInt' = (> 32)

-- same as `useBigInt'` but based on `IntKind`
useBigInt : IntKind -> Bool
useBigInt (Signed $ P x)     = useBigInt' x
useBigInt (Signed Unlimited) = True
useBigInt (Unsigned x)       = useBigInt' x

-- call _bigIntOfString from the preamble, which
-- converts a string to a `BigInt`
jsBigIntOfString : Doc -> Doc
jsBigIntOfString = callFun1 (esName "bigIntOfString")

-- call _parseFloat from the preamble, which
-- converts a string to a `Number`
jsNumberOfString : Doc -> Doc
jsNumberOfString = callFun1 (esName "numberOfString")

-- convert an string to an integral type based
-- on its `IntKind`.
jsIntOfString : IntKind -> Doc -> Doc
jsIntOfString k =
  if useBigInt k
     then jsBigIntOfString
     else callFun1 (esName "intOfString")

-- introduce a binary infix operation
binOp : (symbol : String) -> (lhs : Doc) -> (rhs : Doc) -> Doc
binOp sym lhs rhs = hcat ["(", lhs, Text sym, rhs, ")"]

-- converts a `Number` to an integer
-- based on the given precision (`IntKind`).
toInt : IntKind -> Doc -> Doc
toInt k = if useBigInt k then toBigInt else id

-- converts an integer to a `Number`
-- based on the given precision (`IntKind`).
fromInt : IntKind -> Doc -> Doc
fromInt k = if useBigInt k then fromBigInt else id

-- converts a character (in JS, a string of length 1)
-- to an integer.
jsIntOfChar : IntKind -> Doc -> Doc
jsIntOfChar k s = toInt k $ s <+> ".codePointAt(0)"

-- converts a floating point number to an integer.
jsIntOfDouble : IntKind -> Doc -> Doc
jsIntOfDouble k = toInt k . callFun1 "Math.trunc"

jsAnyToString : Doc -> Doc
jsAnyToString s = "(''+" <+> s <+> ")"

-- converts an integer (`Number` or `BigInt`) to a character
-- by calling `_truncToChar` from the preamble.
jsCharOfInt : IntKind -> Doc -> Doc
jsCharOfInt k = callFun1 (esName "truncToChar") . fromInt k

-- Invokes a function from the preamble to check if an bounded
-- signed integer is within bounds, and - if that's not the case -
-- truncate it accordingly.
-- `isBigInt` reflects whether `int` is a `BigInt` or a `Number`.
--
-- Note: We can't determine `isBigInt` from the given number of bits, since
-- when casting from BigInt (for instance, a `Bits64`) to Number
-- we need to truncate the BigInt
-- first, otherwise we might lose precision.
truncateSigned : (isBigInt : Bool) -> (bits : Int) -> (int : Doc) -> Doc
truncateSigned isBigInt bits =
   let add = if isBigInt then "BigInt" else "Int"
    in callFun1 (esName "trunc" ++ add ++ show bits)

-- like `truncateSigned` but for unsigned integers
truncateUnsigned : (isBigInt : Bool) -> (bits : Int) -> (int : Doc) -> Doc
truncateUnsigned isBigInt bits =
   let add = if isBigInt then "BigInt" else "Int"
    in callFun1 (esName "truncU" ++ add ++ show bits)

-- invokes an arithmetic operation for a bounded integral value.
-- this is used to implement `boundedIntOp` and `boundedUIntOp`
-- where the suffix is set to "s" or "u", respectively.
boundedOp :  (suffix : String)
          -> (bits : Int)
          -> (op : String)
          -> (lhs : Doc)
          -> (rhs : Doc)
          -> Doc
boundedOp s bits o x y = callFun (fastConcat ["_", o, show bits, s]) [x,y]

-- alias for `boundedOp "s"`
boundedIntOp : Int -> String -> Doc -> Doc -> Doc
boundedIntOp = boundedOp "s"

-- alias for `boundedOp "u"`
boundedUIntOp : Int -> String -> Doc -> Doc -> Doc
boundedUIntOp = boundedOp "u"

-- generates code for a boolean binop, like `>=`.
boolOp : (op : String) -> (lhs : Doc) -> (rhs : Doc) -> Doc
boolOp o lhs rhs = "(" <+> binOp o lhs rhs <+> "?1:0)"

-- convert an Idris constant to its JS representation
jsConstant : Constant -> String
jsConstant (I i)    = show i
jsConstant (I8 i)   = show i
jsConstant (I16 i)  = show i
jsConstant (I32 i)  = show i
jsConstant (I64 i)  = show i ++ "n"
jsConstant (BI i)   = show i ++ "n"
jsConstant (Str s)  = jsString s
jsConstant (Ch c)   = jsString $ singleton c
jsConstant (Db f)   = show f
jsConstant WorldVal = esName "idrisworld"
jsConstant (B8 i)   = show i
jsConstant (B16 i)  = show i
jsConstant (B32 i)  = show i
jsConstant (B64 i)  = show i ++ "n"
jsConstant IntType = "#t"
jsConstant Int8Type = "#t"
jsConstant Int16Type = "#t"
jsConstant Int32Type = "#t"
jsConstant Int64Type = "#t"
jsConstant IntegerType = "#t"
jsConstant Bits8Type = "#t"
jsConstant Bits16Type = "#t"
jsConstant Bits32Type = "#t"
jsConstant Bits64Type = "#t"
jsConstant StringType = "#t"
jsConstant CharType = "#t"
jsConstant DoubleType = "#t"
jsConstant WorldType = "#t"

-- Creates the definition of a binary arithmetic operation.
-- Rounding / truncation behavior is determined from the
-- `IntKind`.
arithOp :  Maybe IntKind
        -> (sym : String) -- operator symbol (in case we can use the symbolic version)
        -> (op  : String)  -- operation name (for operations on bounded integrals)
        -> (lhs : Doc)
        -> (rhs : Doc)
        -> Doc
arithOp (Just $ Signed $ P n) _   op = boundedIntOp n op
arithOp (Just $ Unsigned n)   _   op = boundedUIntOp n op
arithOp _                     sym _  = binOp sym

-- use 32bit signed integer for `Int`.
jsIntKind : Constant -> Maybe IntKind
jsIntKind IntType = Just . Signed   $ P 32
jsIntKind x       = intKind x

-- implementation of all kinds of cast from and / or to integral
-- values.
castInt : Constant -> Constant -> Doc -> Core Doc
castInt from to x =
  case ((from, jsIntKind from), (to, jsIntKind to)) of
    ((CharType,_),  (_,Just k)) => truncInt (useBigInt k) k $ jsIntOfChar k x
    ((StringType,_),(_,Just k)) => truncInt (useBigInt k) k (jsIntOfString k x)
    ((DoubleType,_),(_,Just k)) => truncInt (useBigInt k) k $ jsIntOfDouble k x
    ((_,Just k),(CharType,_))   => pure $ jsCharOfInt k x
    ((_,Just k),(StringType,_)) => pure $ jsAnyToString x
    ((_,Just k),(DoubleType,_)) => pure $ fromInt k x
    ((_,Just k1),(_,Just k2))   => intImpl k1 k2
    _ => errorConcat $ ["invalid cast: + ",show from," + ' -> ' + ",show to]
  where
    truncInt : (isBigInt : Bool) -> IntKind -> Doc -> Core Doc
    truncInt b (Signed Unlimited) = pure
    truncInt b (Signed $ P n)     = pure . truncateSigned b n
    truncInt b (Unsigned n)       = pure . truncateUnsigned b n

    shrink : IntKind -> IntKind -> Doc -> Doc
    shrink k1 k2 = case (useBigInt k1, useBigInt k2) of
                        (True, False) => fromBigInt
                        _             => id

    expand : IntKind -> IntKind -> Doc -> Doc
    expand k1 k2 = case (useBigInt k1, useBigInt k2) of
                        (False,True) => toBigInt
                        _            => id

    -- when going from BigInt to Number, we must make
    -- sure to first truncate the BigInt, otherwise we
    -- might get rounding issues
    intImpl : IntKind -> IntKind -> Core Doc
    intImpl k1 k2 =
      let expanded = expand k1 k2 x
          shrunk   = shrink k1 k2 <$> truncInt (useBigInt k1) k2 x
       in case (k1,k2) of
            (_, Signed Unlimited)    => pure $ expanded
            (Signed m, Signed n)     =>
              if n >= m then pure expanded else shrunk

            (Signed _, Unsigned n)   =>
              case (useBigInt k1, useBigInt k2) of
                   (False,True)  => truncInt True k2 (toBigInt x)
                   _             => shrunk

            (Unsigned m, Unsigned n) =>
              if n >= m then pure expanded else shrunk

            -- Only if the precision of the target is greater
            -- than the one of the source, there is no need to cast.
            (Unsigned m, Signed n)   =>
              if n > P m then pure expanded else shrunk

-- implementations of primitive functions.
jsOp : {0 arity : Nat} ->
       PrimFn arity -> Vect arity Doc -> Core Doc
jsOp (Add ty) [x, y] = pure $ arithOp (jsIntKind ty) "+" "add" x y
jsOp (Sub ty) [x, y] = pure $ arithOp (jsIntKind ty) "-" "sub" x y
jsOp (Mul ty) [x, y] = pure $ arithOp (jsIntKind ty) "*" "mul" x y
jsOp (Div ty) [x, y] = pure $ arithOp (jsIntKind ty) "/" "div" x y
jsOp (Mod ty) [x, y] = pure $ binOp "%" x y
jsOp (Neg ty) [x] = pure $ "(-(" <+> x <+> "))"
jsOp (ShiftL Int32Type) [x, y] = pure $ binOp "<<" x y
jsOp (ShiftL IntType) [x, y] = pure $ binOp "<<" x y
jsOp (ShiftL ty) [x, y] = pure $ arithOp (jsIntKind ty) "<<" "shl" x y
jsOp (ShiftR Int32Type) [x, y] = pure $ binOp ">>" x y
jsOp (ShiftR IntType) [x, y] = pure $ binOp ">>" x y
jsOp (ShiftR ty) [x, y] = pure $ arithOp (jsIntKind ty) ">>" "shr" x y
jsOp (BAnd Bits32Type) [x, y] = pure $ boundedUIntOp 32 "and" x y
jsOp (BOr Bits32Type) [x, y]  = pure $ boundedUIntOp 32 "or" x y
jsOp (BXOr Bits32Type) [x, y] = pure $ boundedUIntOp 32 "xor" x y
jsOp (BAnd ty) [x, y] = pure $ binOp "&" x y
jsOp (BOr ty) [x, y] = pure $ binOp "|" x y
jsOp (BXOr ty) [x, y] = pure $ binOp "^" x y
jsOp (LT ty) [x, y] = pure $ boolOp "<" x y
jsOp (LTE ty) [x, y] = pure $ boolOp "<=" x y
jsOp (EQ ty) [x, y] = pure $ boolOp "===" x y
jsOp (GTE ty) [x, y] = pure $ boolOp ">=" x y
jsOp (GT ty) [x, y] = pure $ boolOp ">" x y
jsOp StrLength [x] = pure $ x <+> ".length"
jsOp StrHead [x] = pure $ "(" <+> x <+> ".charAt(0))"
jsOp StrTail [x] = pure $ "(" <+> x <+> ".slice(1))"
jsOp StrIndex [x, y] = pure $ "(" <+> x <+> ".charAt(" <+> y <+> "))"
jsOp StrCons [x, y] = pure $ binOp "+" x y
jsOp StrAppend [x, y] = pure $ binOp "+" x y
jsOp StrReverse [x] = pure $ callFun1 (esName "strReverse") x
jsOp StrSubstr [offset, len, str] =
  pure $ callFun (esName "substr") [offset,len,str]
jsOp DoubleExp [x]     = pure $ callFun1 "Math.exp" x
jsOp DoubleLog [x]     = pure $ callFun1 "Math.log" x
jsOp DoublePow [x, y]  = pure $ callFun "Math.pow" [x, y]
jsOp DoubleSin [x]     = pure $ callFun1 "Math.sin" x
jsOp DoubleCos [x]     = pure $ callFun1 "Math.cos" x
jsOp DoubleTan [x]     = pure $ callFun1 "Math.tan" x
jsOp DoubleASin [x]    = pure $ callFun1 "Math.asin" x
jsOp DoubleACos [x]    = pure $ callFun1 "Math.acos" x
jsOp DoubleATan [x]    = pure $ callFun1 "Math.atan" x
jsOp DoubleSqrt [x]    = pure $ callFun1 "Math.sqrt" x
jsOp DoubleFloor [x]   = pure $ callFun1 "Math.floor" x
jsOp DoubleCeiling [x] = pure $ callFun1 "Math.ceil" x

jsOp (Cast StringType DoubleType) [x] = pure $ jsNumberOfString x
jsOp (Cast ty StringType) [x] = pure $ jsAnyToString x
jsOp (Cast ty ty2) [x]        = castInt ty ty2 x
jsOp BelieveMe [_,_,x] = pure x
jsOp (Crash) [_, msg] = pure $ jsCrashExp msg

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

-- from an FFI declaration, reads the backend to use.
-- Example: `readCCPart "node:lambda: x => x"` yields
-- `("node","lambda: x => x")`.
readCCPart : String -> (String, String)
readCCPart = breakDrop1 ':'

-- search a an FFI implementation for one of the supported
-- backends.
searchForeign : List String -> List String -> Either (List String) String
searchForeign knownBackends decls =
  let pairs = map readCCPart decls
      backends = Left $ map fst pairs
   in maybe backends (Right. snd) $ find ((`elem` knownBackends) . fst) pairs

-- given a function name and FFI implementation string,
-- generate a toplevel function definition.
makeForeign :  {auto d : Ref Ctxt Defs}
            -> {auto c : Ref ESs ESSt}
            -> (name : Name)
            -> (ffDecl : String)
            -> Core Doc
makeForeign n x = do
  nd <- var <$> getOrRegisterRef n
  let (ty, def) = readCCPart x
  case ty of
    "lambda" => pure . constant nd . paren $ Text def
    "support" => do
      let (name, lib) = breakDrop1 ',' def
      lib_code <- readDataFile ("js/" ++ lib ++ ".js")
      addToPreamble lib lib_code
      pure . constant nd . Text $ lib ++ "_" ++ name
    "stringIterator" =>
      case def of
        "new"      => pure $ constant nd "__prim_stringIteratorNew"
        "next"     => pure $ constant nd "__prim_stringIteratorNext"
        "toString" => pure $ constant nd "__prim_stringIteratorToString"
        _ => errorConcat
               [ "Invalid string iterator function: ", def, ". "
               , "Supported functions are: "
               , stringList ["new","next","toString"], "."
               ]

    _ => errorConcat
           [ "Invalid foreign type : ", ty, ". "
           , "Supported types are: "
           , stringList ["lambda", "support", "stringIterator"]
           ]

-- given a function name and list of FFI declarations, tries
-- to extract a declaration for one of the supported backends.
foreignDecl :  {auto d : Ref Ctxt Defs}
            -> {auto c : Ref ESs ESSt}
            -> Name
            -> List String
            -> Core Doc
foreignDecl n ccs = do
  tys <- ccTypes <$> get ESs
  case searchForeign tys ccs of
    Right x        => makeForeign n x
    Left  backends =>
      errorConcat
        [ "No supported backend found in the definition of ", show n, ". "
        , "Supported backends: ", stringList tys, ". "
        , "Backends in definition: ", stringList backends, "."
        ]

-- implementations for external primitive functions.
jsPrim : {auto c : Ref ESs ESSt} -> Name -> List Doc -> Core Doc
jsPrim nm docs = case (dropAllNS nm, docs) of
  (UN (Basic "prim__newIORef"), [_,v,_]) => pure $ hcat ["({value:", v, "})"]
  (UN (Basic "prim__readIORef"), [_,r,_]) => pure $ hcat ["(", r, ".value)"]
  (UN (Basic "prim__writeIORef"), [_,r,v,_]) => pure $ hcat ["(", r, ".value=", v, ")"]
  (UN (Basic "prim__newArray"), [_,s,v,_]) => pure $ hcat ["(Array(", s, ").fill(", v, "))"]
  (UN (Basic "prim__arrayGet"), [_,x,p,_]) => pure $ hcat ["(", x, "[", p, "])"]
  (UN (Basic "prim__arraySet"), [_,x,p,v,_]) => pure $ hcat ["(", x, "[", p, "]=", v, ")"]
  (UN (Basic "void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
  (UN (Basic "prim__void"), [_, _]) => pure . jsCrashExp $ jsStringDoc "Error: Executed 'void'"
  (UN (Basic "prim__codegen"), []) => do
    (cg :: _) <- ccTypes <$> get ESs
        | _ => pure "\"javascript\""
    pure . Text $ jsString cg

-- fix #1839: Only support `prim__os` in Node backend but not in browsers
  (UN (Basic "prim__os"), []) => do
    tys <- ccTypes <$> get ESs
    case searchForeign tys ["node"] of
      Right _ => do
        addToPreamble "prim__os" $
          "const _sysos = ((o => o === 'linux'?'unix':o==='win32'?'windows':o)" ++
          "(require('os').platform()));"
        pure $ Text $ esName "sysos"
      Left  _ =>
        throw $ InternalError $ "prim not implemented: prim__os"

  _ => throw $ InternalError $ "prim not implemented: " ++ show nm

--------------------------------------------------------------------------------
--          Codegen
--------------------------------------------------------------------------------

-- checks, whether we accept the given `Exp` as a function argument, or
-- whether it needs to be lifted to the surrounding scope and assigned
-- to a new variable.
isArg : CGMode -> Exp -> Bool
isArg Pretty (ELam _ $ Block _ _)           = False
isArg Pretty (ELam _ $ ConSwitch _ _ _ _)   = False
isArg Pretty (ELam _ $ ConstSwitch _ _ _ _) = False
isArg Pretty (ELam _ $ Error _)             = False
isArg _      _                              = True

-- like `isArg` but for function expressions, which we are about
-- to apply
isFun : Exp -> Bool
isFun (ELam _ _) = False
isFun _          = True

-- creates a JS switch statment from the given scrutinee and
-- case blocks (the first entry in a pair is the value belonging
-- to a `case` statement, the second is the body
--
-- Example: switch "foo.a1" [("0","return 2;")] (Just "return 0;")
-- generates the following code:
-- ```javascript
--   switch(foo.a1) {
--     case 0: return 2;
--     default: return 0;
--   }
-- ```
switch :  (scrutinee : Doc)
       -> (alts : List (Doc,Doc))
       -> (def : Maybe Doc)
       -> Doc
switch sc alts def =
  let stmt    = "switch" <+> paren sc <+> SoftSpace
      defcase = concatMap (pure . anyCase "default") def
   in stmt <+> block (vcat $ map alt alts ++ defcase)

  where anyCase : Doc -> Doc -> Doc
        anyCase s d =
          let b = if isMultiline d then block d else d
           in s <+> softColon <+> b

        alt : (Doc,Doc) -> Doc
        alt (e,d) = anyCase ("case" <++> e) d

-- creates an argument list for a (possibly multi-argument)
-- anonymous function. An empty argument list is treated
-- as a delayed computation (prefixed by `() =>`).
lambdaArgs : List Var -> Doc
lambdaArgs [] = "()" <+> lambdaArrow
lambdaArgs xs = hcat $ (<+> lambdaArrow) . var <$> xs

insertBreak : (r : Effect) -> (Doc, Doc) -> (Doc, Doc)
insertBreak Returns x = x
insertBreak (ErrorWithout _) (pat, exp) = (pat, vcat [exp, "break;"])

mutual
  -- converts an `Exp` to JS code
  exp : {auto c : Ref ESs ESSt} -> Exp -> Core Doc
  exp (EMinimal x) = pure $ minimal x
  exp (ELam xs (Return $ y@(ECon _ _ _))) =
     map (\e => lambdaArgs xs <+> paren e) (exp y)
  exp (ELam xs (Return $ y)) = (lambdaArgs xs <+> ) <$> exp y
  exp (ELam xs y) = (lambdaArgs xs <+>) . block <$> stmt y
  exp (EApp x xs) = do
    o    <- exp x
    args <- traverse exp xs
    pure $ app o args

  exp (ECon tag ci xs) = applyCon ci tag <$> traverse exp xs

  exp (EOp x xs) = traverseVect exp xs >>= jsOp x
  exp (EExtPrim x xs) = traverse exp xs >>= jsPrim x
  exp (EPrimVal x) = pure . Text $ jsConstant x
  exp EErased = pure "undefined"

  -- converts a `Stmt e` to JS code.
  stmt : {e : _} -> {auto c : Ref ESs ESSt} -> Stmt e -> Core Doc
  stmt (Return y) = (\e => "return" <++> e <+> ";") <$> exp y
  stmt (Const v x) = constant (var v) <$> exp x
  stmt (Declare v s) =
    (\d => vcat ["let" <++> var v <+> ";",d]) <$> stmt s
  stmt (Assign v x) =
    (\d => hcat [var v,softEq,d,";"]) <$> exp x

  stmt (ConSwitch r sc alts def) = do
    as <- traverse (map (insertBreak r) . alt) alts
    d  <- traverseOpt stmt def
    pure $  switch (minimal sc <+> ".h") as d
    where
        alt : {r : _} -> EConAlt r -> Core (Doc,Doc)
        alt (MkEConAlt _ RECORD b)  = ("undefined",) <$> stmt b
        alt (MkEConAlt _ NIL b)     = ("0",) <$> stmt b
        alt (MkEConAlt _ CONS b)    = ("undefined",) <$> stmt b
        alt (MkEConAlt _ NOTHING b) = ("0",) <$> stmt b
        alt (MkEConAlt _ JUST b)    = ("undefined",) <$> stmt b
        alt (MkEConAlt t _ b)       = (tag2es t,) <$> stmt b

  stmt (ConstSwitch r sc alts def) = do
    as <- traverse (map (insertBreak r) . alt) alts
    d  <- traverseOpt stmt def
    ex <- exp sc
    pure $ switch ex as d
    where
        alt : EConstAlt r -> Core (Doc,Doc)
        alt (MkEConstAlt c b) = do
            d <- stmt b
            pure (Text $ jsConstant c, d)

  stmt (Error x)   = pure $ jsCrashExp (jsStringDoc x) <+> ";"
  stmt (Block ss s) = do
    docs <- traverse stmt $ forget ss
    doc  <- stmt s
    pure $ vcat (docs ++ [doc])

-- pretty print a piece of code based on the given
-- codegen mode.
printDoc : CGMode -> Doc -> String
printDoc Pretty y = pretty (y <+> LineBreak)
printDoc Compact y = compact y
printDoc Minimal y = compact y

-- generate code for the given toplevel function.
def : {auto c : Ref ESs ESSt} -> Function -> Core String
def (MkFunction n as body) = do
  reset
  ref  <- getOrRegisterRef n
  args <- traverse registerLocal as
  mde  <- mode <$> get ESs
  b    <- stmt Returns body >>= stmt
  case args of
    -- zero argument toplevel functions are converted to
    -- lazily evaluated constants.
    [] => pure $ printDoc mde $
      constant (var ref) (
        "__lazy(" <+> function neutral [] b <+> ")"
      )
    _  => pure $ printDoc mde $ function (var ref) (map var args) b

-- generate code for the given foreign function definition
foreign :  {auto c : Ref ESs ESSt}
        -> {auto d : Ref Ctxt Defs}
        -> (Name,FC,NamedDef)
        -> Core (List String)
foreign (n, _, MkNmForeign path _ _) = pure . pretty <$> foreignDecl n path
foreign _                            = pure []

-- name of the toplevel tail call loop from the
-- preamble.
tailRec : Name
tailRec = UN $ Basic "__tailRec"

||| Compiles the given `ClosedTerm` for the list of supported
||| backends to JS code.
export
compileToES : Ref Ctxt Defs -> (cg : CG) -> ClosedTerm -> List String -> Core String
compileToES c cg tm ccTypes = do
  cdata      <- getCompileData False Cases tm

  -- read a derive the codegen mode to use from
  -- user defined directives for the
  directives <- getDirectives cg
  let mode = if "minimal" `elem` directives then Minimal
             else if "compact" `elem` directives then Compact
             else Pretty

  -- initialize the state used in the code generator
  s <- newRef ESs $ init mode (isArg mode) isFun ccTypes

  -- register the toplevel `__tailRec` function to make sure
  -- it is not mangled in `Minimal` mode
  addRef tailRec (VName tailRec)

  -- the list of all toplevel definitions (including the main
  -- function)
  let allDefs =  (mainExpr, EmptyFC, MkNmFun [] $ forget cdata.mainExpr)
              :: cdata.namedDefs

      -- tail-call optimized set of toplevel functions
      defs    = TailRec.functions tailRec allDefs

  -- pretty printed toplevel function definitions
  defDecls <- traverse def defs

  -- pretty printed toplevel FFI definitions
  foreigns <- concat <$> traverse foreign allDefs

  -- lookup the (possibly mangled) name of the main function
  mainName <- compact . var <$> getOrRegisterRef mainExpr

  -- main function and list of all declarations
  let main =  "try{"
           ++ mainName
           ++ "()}catch(e){if(e instanceof IdrisError){console.log('ERROR: ' + e.message)}else{throw e} }"

      allDecls = fastUnlines $ foreigns ++ defDecls

  st <- get ESs

  -- main preamble containing primops implementations
  static_preamble <- readDataFile ("js/support.js")

  -- complete preamble, including content from additional
  -- support files (if any)
  let pre = showSep "\n" $ static_preamble :: (values $ preamble st)

  pure $ fastUnlines [pre,allDecls,main]

ext: idr


text:
module Basen

import Data.Fin

--Defines a data type Base that behaves like a list
data Base: (n: Nat) -> Type where
  Ones: (n: Nat) -> (Fin n) -> Base n
  Next: (n: Nat) -> (Fin n) -> (Base n) -> (Base n)

--Auxiliary function that reverses a Base (S n) onto anpther given Base (S n)
Revonto: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
Revonto n accum (Ones (S n) x) = Next (S n) x accum
Revonto n accum (Next (S n) x y) = Revonto n (Next (S n) x accum) y

--Reverses a Base (S n)
Rev: (n: Nat) -> (Base (S n)) -> (Base (S n))
Rev n (Ones (S n) x) = Ones (S n) x
Rev n (Next (S n) x y) = Revonto n (Ones (S n) x) y

concat: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
concat n (Ones (S n) x) y = Next (S n) x y
concat n (Next (S n) x z) y = Next (S n) x (concat n z y)

--Fin to Nat
tonatFin: (n: Nat) -> Fin(n) -> Nat
tonatFin (S k) FZ = Z
tonatFin (S k) (FS x) = S (tonatFin k x)

--List Fin to Nat
tonat: (n: Nat) -> Base (S n) -> Nat
tonat n (Ones (S n) FZ) = Z
tonat Z (Ones (S Z) (FS x)) impossible
tonat (S k) (Ones (S (S k)) (FS x)) = S(tonat k (Ones (S k) x))
tonat n (Next (S n) x y) = (tonat n (Ones (S n) x)) + (tonat n y)

--Euclid's div
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl a Z = (0, a)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

--Nat to Fin (modular values)
tofinNat: (a: Nat) -> (n: Nat) -> Fin n
tofinNat Z (S j) = FZ
tofinNat (S k) (S j) = case lte (S k) (S j) of
                True => FS (tofinNat k j)
                False =>  (tofinNat (snd(Eucl (S k) (S j))) (S j))

strp: (Base (S n)) -> (Base (S n))
strp (Ones (S n) x) = (Ones (S n) x)
strp (Next (S n) x y) = case x of
                  FZ => strp(y)
                  FS z => Next (S n) x y

-- Nat to List Fin n (base n representation)
tofin: Nat -> (n: Nat) -> Base (S n)
tofin Z n = Ones (S n) FZ
tofin (S k) n = strp(concat n (tofin q n) (Ones (S n) rem)) where
                    rem: Fin (S n)
                    rem = tofinNat (snd(Eucl (S k) (S n))) (S n)
                    q: Nat
                    q = fst(Eucl (S k) (S n))

--embedding Fin n in Fin S n vertically
embn: (n: Nat) -> Fin n -> Fin (S n)
embn (S k) FZ = FZ
embn (S k) (FS x) = FS (embn k x)

--Generates n in (Fin (S n))
Genn: (n: Nat) -> (Fin (S n))
Genn Z = FZ
Genn (S k) = FS (Genn k)

--Checks if a given element of Fin (S n) is in fact n
Isn: (n: Nat) -> (p: Fin (S n)) -> Bool
Isn Z x = True
Isn (S k) FZ = False
Isn (S k) (FS x) = Isn k x

--Proves that the definitional equality for Isn holds
IsnisIsn: (n: Nat) -> (p: Fin (S n)) -> (Isn (S n) (FS p)) = (Isn n p)
IsnisIsn n p = Refl

--Proves that if a given (FS x) is not n in (Fin (S n)), then x is not n-1 in (Fin n)
IsNotnPf:  (n: Nat) -> (p: Fin (S n)) ->  ((Isn (S n) (FS p)) = False) -> ((Isn n p) = False)
IsNotnPf Z _ Refl impossible
IsNotnPf (S k) FZ prf = Refl
IsNotnPf (S k) (FS x) prf = trans (sym (IsnisIsn (S k) (FS x))) prf

--Gives a back embedding whenever the value is not Genn
Predec: (n: Nat) -> (p: Fin (S n)) -> ((Isn n p) = False) -> (Fin n)
Predec Z _ Refl impossible
Predec (S k) FZ Refl = FZ
Predec (S k) (FS x) prf = FS (Predec k x (IsNotnPf (S k) (FS x) prf))

--Decidable type for Isn
DecIsn: (n: Nat) -> (p: (Fin (S n))) -> Either (Isn n p = True) (Isn n p = False)
DecIsn Z p = Left Refl
DecIsn (S k) FZ = Right Refl
DecIsn (S k) (FS x) = case (DecIsn k x) of
                        Left l => Left (trans (IsnisIsn k x) l)
                        Right r => Right (trans (IsnisIsn k x) r)

--adding two Fin n's
addfin: (n: Nat) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
addfin Z x y = (FZ,  FZ)
addfin (S k) FZ y = (FZ, y)
addfin (S k) (FS x) y = let
                    a = Genn (S k)
                    b = the (Fin (S (S k))) FZ
                    c = the (Fin (S k)) FZ
                    w = fst(addfin (S k) (embn (S k) x) y)
                    z = snd(addfin (S k) (embn (S k) x) y)
                    in
                    case (DecIsn (S k) z) of
                             Left l => (FS c, b)
                             Right r => (w, FS(Predec (S k) z r))

--adding two reversed lists as specified
addfinl: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
addfinl n (Ones (S n) x) (Ones (S n) y) = case (addfin n x y) of
                              (FZ, a) => Ones (S n) a
                              (FS c, a) => Next (S n) a (Ones (S n) (FS c))
addfinl n (Ones (S n) x) (Next (S n) y z) = Next (S n) (snd (addfin n x y)) (addfinl n (Ones (S n) (fst (addfin n x y))) z)
addfinl n (Next (S n) x z) (Ones (S n) y) = Next (S n) (snd (addfin n x y)) (addfinl n (Ones (S n) (fst (addfin n x y))) z)
addfinl n (Next (S n) x z) (Next (S n) y w) = Next (S n) (snd (addfin n x y)) (addfinl n (Ones (S n) (fst (addfin n x y))) (addfinl n z w))

--adding two lists
addfinlist: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
addfinlist n xs ys = (Rev n (addfinl n (Rev n xs) (Rev n ys)))

--multiply two reversed lists in Fin S n
mulfinl: (n: Nat) -> Base (S n) -> Base (S n) -> Base (S n)
mulfinl n (Ones (S n) FZ) y = Ones (S n) FZ
mulfinl n (Ones (S n) (FS x)) y = addfinl n y (mulfinl n (Ones (S n) (embn n x)) y)
mulfinl n (Next (S n) FZ z) y = Next (S n) FZ (mulfinl n z y)
mulfinl n (Next (S n) (FS x) z) y = addfinl n y (mulfinl n (Next (S n) (embn n x) z) y)

--multiply two lists
mulfinList: (n: Nat) -> (Base (S n)) -> (Base (S n)) -> (Base (S n))
mulfinList n xs ys = Rev n (mulfinl n (Rev n xs) (Rev n ys))

--Custom "functions are functors" function
ap: (x: Type) -> (y: Type) -> (f: x->y) -> (n = m) -> (f n = f m)
ap x y f Refl = Refl


text:
not : (arg1 : Bool) -> (arg2 : Bool)
not = ?a


text:
module AOC.Main

import AOC.Day
import AOC.Solution
import AOC.Solution.IO

import Data.List

main : IO ()
main = do
  sequence_ $ intersperse (putStrLn "") $ map printSolutionDP $ days


text:
namespace Foo
  export
  data A = B | C

namespace Bar
  export
  data A = D | E


text:
module Network.Curl.Prim.Easy

-------------------------------------------------
-- Easy
-------------------------------------------------
-- curl_easy_cleanup
-- curl_easy_duphandle
-- curl_easy_escape
-- curl_easy_getinfo
-- curl_easy_init
-- curl_easy_option_by_id
-- curl_easy_option_by_name
-- curl_easy_option_next
-- curl_easy_pause
-- curl_easy_perform
-- curl_easy_recv
-- curl_easy_reset
-- curl_easy_send
-- curl_easy_setopt
-- curl_easy_strerror
-- curl_easy_unescape
-- curl_easy_upkeep
-------------------------------------------------

import Data.Buffer

-- import Network.Curl.Prim.Mem
import Network.Curl.Prim.Other

import Network.Curl.Types
-- import Network.Curl.Types.CurlEOption as EO
-- import Derive.Enum

import Derive.Prim
%language ElabReflection

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

-- curl_easy_duphandle
%runElab makeHasIO "curl_easy_duphandle" Export
          `[ %foreign "C:curl_easy_duphandle,libcurl,curl/curl.h"
             export
             prim_curl_easy_duphandle : Ptr HandlePtr -> PrimIO (Ptr HandlePtr) ] --`

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

%foreign "C:curl_easy_init,libcurl,curl/curl.h"
prim_curl_easy_init : PrimIO (Ptr HandlePtr)

export
curl_easy_init : HasIO io => io (Maybe (CurlHandle Easy))
curl_easy_init = do r <- primIO prim_curl_easy_init
                    pure $ if believe_me r == 0 then Nothing
                                                else Just (MkH r)

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

%foreign "C:curl_easy_cleanup,libcurl,curl/curl.h"
prim_curl_easy_cleanup : Ptr HandlePtr -> PrimIO ()

export
curl_easy_cleanup : HasIO io => CurlHandle Easy -> io ()
curl_easy_cleanup (MkH h) = primIO $ prim_curl_easy_cleanup h

-- It's just a lookup, expect this to work unless curl itself is broken
%foreign "C:curl_easy_strerror,libcurl,curl/curl.h"
curl_easy_strerror : (curlcode : Int) -> String

export
curlEasyStrError : CurlECode -> String
curlEasyStrError c = curl_easy_strerror (toCode c)

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

%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt_long : Ptr HandlePtr -> Int -> Int -> PrimIO Int

%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt_objptr : Ptr HandlePtr -> Int -> AnyPtr -> PrimIO Int

%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt_off_t : Ptr HandlePtr -> Int -> Bits64 -> PrimIO Int

%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt_blob : Ptr HandlePtr -> Int -> Buffer -> PrimIO Int

%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt_string : Ptr HandlePtr -> Int -> String -> PrimIO Int

-- This is to fill the role of
{-
%foreign "C:curl_easy_setopt,libcurl,curl/curl.h"
prim_curl_easy_setopt : Ptr HandlePtr -> Int -> any -> PrimIO CurlECode
-}
-- We can't pass 'any' or an arbitrary Type to a foreign function, but we can
-- generate that function at the type we need.
%macro
eSetOptPrim : {opty : _} -> (opt : CurlEOption opty)
           -> Elab (Ptr HandlePtr -> Int -> paramType opt -> PrimIO Int)
eSetOptPrim opt = do
  let name = UN $ "setOptPrim_" ++ show opt
  z <- quote (paramType opt)
  str <- quote "C:curl_easy_setopt,libcurl,curl/curl.h"
  let ty = MkTy EmptyFC EmptyFC name `(Ptr HandlePtr -> Int -> ~z -> PrimIO Int)
  let claim = IClaim EmptyFC MW Private
                [ForeignFn [str]] ty
  declare [claim] -- generate prim
  check (IVar EmptyFC name) -- insert prim's name

||| It's kind of unfortunate we need to case all of these `opt` when the code
||| used on them is exactly the same and while it could be done with elaboration
||| it's not really worth the work. Users shouldn't actually be exposed to this
||| definition to be scared away by it anyway.
export
curl_easy_setopt : HasIO io => CurlHandle Easy -> {ty : _}
                -> (opt : CurlEOption ty) -> paramType opt -> io CurlECode
curl_easy_setopt (MkH h) opt@CURLOPT_WRITEFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_READFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_PROGRESSFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_HEADERFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_DEBUGFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_SSL_CTX_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_IOCTLFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CONV_FROM_NETWORK_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CONV_TO_NETWORK_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CONV_FROM_UTF8_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_SOCKOPTFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_OPENSOCKETFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_SEEKFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_SSH_KEYFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_INTERLEAVEFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CHUNK_BGN_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CHUNK_END_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_FNMATCH_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_CLOSESOCKETFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_XFERINFOFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_RESOLVER_START_FUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt (MkH h) opt@CURLOPT_TRAILERFUNCTION v = do
      let prim = eSetOptPrim opt
      pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_easy_setopt {ty = CURLOPTTYPE_LONG} (MkH h) opt v = pure $
  unsafeFromCode !(primIO $ prim_curl_easy_setopt_long h (toCode opt) v)
curl_easy_setopt {ty = CURLOPTTYPE_OBJECTPOINT} (MkH h) opt v = pure $
  unsafeFromCode !(primIO $ prim_curl_easy_setopt_objptr h (toCode opt) v)
curl_easy_setopt {ty = CURLOPTTYPE_OFF_T} (MkH h) opt v = pure $
  unsafeFromCode !(primIO $ prim_curl_easy_setopt_off_t h (toCode opt) v)
curl_easy_setopt {ty = CURLOPTTYPE_BLOB} (MkH h) opt v = pure $
  unsafeFromCode !(primIO $ prim_curl_easy_setopt_blob h (toCode opt) v)
curl_easy_setopt {ty = CURLOPTTYPE_STRINGPOINT} (MkH h) opt v = pure $
  unsafeFromCode !(primIO $ prim_curl_easy_setopt_string h (toCode opt) v)
curl_easy_setopt {ty = UnusedOptType} _ _ _ = pure CURLE_UNKNOWN_OPTION
--                      ^can't happen during normal use

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

%foreign "C:curl_easy_perform,libcurl,curl/curl.h"
prim_curl_easy_perform : Ptr HandlePtr -> PrimIO Int

export
curl_easy_perform : HasIO io => CurlHandle Easy -> io CurlECode
curl_easy_perform (MkH ptr) = unsafeFromCode <$> primIO (prim_curl_easy_perform ptr)

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

-- This String is allocated by curl but idris ffi should copy it so we should be
-- safe in the presence or lack of curl_free
-- TODO check this ^
-- TODO check for possible issues with \0
-- char *curl_easy_escape( CURL *curl, const char *string , int length );
%foreign "C:curl_easy_escape,libcurl,curl/curl.h"
prim_curl_easy_escape : Ptr HandlePtr -> (url : String)
                     -> (url_len : Int) -> PrimIO String

-- idris calls free after copying the PrimIO String it converts but curl wants you
-- to call curl_free, how can I reconcile this?
||| Escapes a String byte-by-byte without awareness of encoding.
||| String is expected to be free of \0 since strlen() is used by curl and so
||| will truncate on \0. This shouldn't be a problem in idris since the
||| primitive String already truncate on \0 in idris.
curl_easy_escape : HasIO io => CurlHandle ty -> String -> io String
curl_easy_escape (MkH h) str = primIO $ prim_curl_easy_escape h str 0
-- 0 is to tell curl to compute the length itself via strlen()

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

{-

-- This String is allocated by curl but idris ffi should copy it so we should be
-- safe in the presence or lack of curl_free.
-- TODO check this ^
-- char *curl_easy_unescape( CURL *curl, const char *url , int inlength, int *outlength );
%foreign "C:curl_easy_unescape,libcurl,curl/curl.h"
prim_curl_easy_unescape : Ptr HandlePtr -> (url : String) -> (url_len : Int)
                       -> (intptr : Buffer) -> PrimIO String

%foreign "C:curl_easy_unescape,libcurl,curl/curl.h"
prim_curl_easy_unescape' : Ptr HandlePtr -> (url : String) -> (url_len : Int)
                        -> Ptr Int -> PrimIO String

||| Unescapes a String byte-by-byte without awareness of encoding. When
||| encountering %00 or some other source of \0 it returns as much of the String
||| as it got to that point.
||| NB I'm not bothering with proper handling %00, if you need this I'll accept
||| a tested PR though. It's just that idris's \0 terminated Strings can make
||| this a hassle. I'll revisit this when/if I made a Text type since it won't
||| have a weakness to \0.
curl_easy_unescape : HasIO io => CurlHandle ty -> String -> io (Either String String)
curl_easy_unescape (MkH h) str
  = withAllocElems {a=Int} 1 $ \iptr => do
      str <- primIO $ prim_curl_easy_unescape h str 0 (unsafeForeignPtrToBuffer iptr)
      len <- peek iptr
      pure $ if len > 0 && cast (length str) /= len -- str contained %00
        then Left str -- This is where a Text type could help.
        else Right str

testo : IO ()
testo = do
  Just h <- curl_easy_init
    | _ => printLn "fuck"
  l <- curl_easy_escape h "fafodoba"
  Right m <- curl_easy_unescape h l
    | Left s => printLn s -- print remainder if there is one
  n <- curl_easy_escape h m
  printLn n
  Right m <- curl_easy_unescape h "gabbo%00nock"
    | Left s => printLn s -- print remainder if there is one
  printLn m

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

-}


text:
module Average

||| Calculate the average length of words in a string
||| @str a string containing words separated by whitespace
export
average : (str : String) -> Double
average str =
  let num_words = word_count str
      total_length = sum (word_lengths (words str))
  in cast total_length / cast num_words

  where
    word_count : String -> Nat
    word_count str = length (words str)

    word_lengths : List String -> List Nat
    word_lengths = map length

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Python.Lib.BeautifulSoup

import Python
import Python.Prim

%access public export
%default total

namespace Parsers

  LXML : String
  LXML = "lxml"

  HTML : String
  HTML = "html.parser"

Element : Signature
Element f = case f of
  "string"  => Attr $ Maybe String
  "strings" => Attr . Obj $ PyList String
  _ => Object f

Soup : Signature
Soup f = case f of
  "select" => [String] ~~> Obj (PyList $ Obj Element)
  _ => Object f

Bs4 : Signature
Bs4 f = case f of
  "BeautifulSoup" => [String, String] ~~> Obj Soup
  _ => Module f

import_ : PIO $ Obj Bs4
import_ = importModule "bs4"

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Rhone.Canvas.Style

import Data.SOP
import JS
import Text.CSS.Color
import Text.CSS.Render
import Web.Html

%default total

public export
data Style : Type where
  Fill      : Color -> Style
  Stroke    : Color -> Style
  LineWidth : Double -> Style

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

export
apply : CanvasRenderingContext2D -> Style -> JSIO ()
apply ctxt (Fill c)      = fillStyle ctxt   .= inject (render c)
apply ctxt (Stroke c)    = strokeStyle ctxt .= inject (render c)
apply ctxt (LineWidth v) = lineWidth ctxt   .= v


text:
module Node.FS.Stats

import Node.FS
import Node.Error

public export
data StatsReturnType
  = StatsBigInt
  | StatsInt

public export
statsReturnType : StatsReturnType -> Type
statsReturnType StatsBigInt = Integer
statsReturnType StatsInt = Int

export
data Stats : StatsReturnType -> Type where [external]

%foreign """
  node:lambda:
  (fs,rty,path) => {
    try {
      const result = fs.statSync(path, {
        bigint: rty.h == 0,
        throwIfNoEntry: true
      });

      return {
        h: 1, // Right
        a1: result
      };
    } catch(e) {
      return {
        h: 0, // Left
        a1: e
      };
    }
  }
  """
ffi_stat_sync : FS -> (r: StatsReturnType) -> String -> PrimIO (Either NodeError $ Stats r)

export
stat_sync : HasIO io => {auto fs : FS} -> (r : StatsReturnType) -> String -> io (Either NodeError $ Stats r)
stat_sync r path = primIO $ ffi_stat_sync fs r path

%foreign """
  node:lambda:
  (fs,rty,path,cb) => {
    fs.stat(path, {
      bigint: rty.h == 0
    }, function(err, value) {
      cb() (
        err
        ? {
            h: 0, // Left
            a1: err
          }
        : {
            h: 1, // Right
            a1: value
          }
      )
    })
  }
  """
ffi_stat : FS -> (r: StatsReturnType) -> String -> (Either NodeError (Stats r) -> PrimIO()) -> PrimIO ()

export
stat : HasIO io => {auto fs : FS} -> (r: StatsReturnType) -> String -> (Either NodeError (Stats r) -> IO ()) -> io ()
stat r path cb = primIO $ ffi_stat fs r path $ \either => toPrim $ cb either

%foreign "node:lambda: (ty, s)=>s.isBlockDevice()"
ffi_isBlockDevice : Stats r -> Int

export
(.isBlockDevice) : Stats r -> Bool
(.isBlockDevice) stats = 0 /= ffi_isBlockDevice stats

%foreign "node:lambda: (ty,s)=>s.isCharacterDevice() ? 1 : 0"
ffi_isCharacterDevice : Stats r -> Int

export
(.isCharacterDevice) : Stats r -> Bool
(.isCharacterDevice) stats = 0 /= ffi_isCharacterDevice stats

%foreign "node:lambda: (ty,s)=>s.isDirectory() ? 1 : 0"
ffi_isDirectory : Stats r -> Int

export
(.isDirectory) : Stats r -> Bool
(.isDirectory) stats = 0 /= ffi_isDirectory stats

%foreign "node:lambda: (ty,s)=>s.isFIFO() ? 1 : 0"
ffi_isFIFO : Stats r -> Int

export
(.isFIFO) : Stats r -> Bool
(.isFIFO) stats = 0 /= ffi_isFIFO stats

%foreign "node:lambda: (ty,s)=>s.isFile() ? 1 : 0"
ffi_isFile : Stats r -> Int

export
(.isFile) : Stats r -> Bool
(.isFile) stats = 0 /= ffi_isFile stats

%foreign "node:lambda: (ty,s)=>s.isSocket() ? 1 : 0"
ffi_isSocket : Stats r -> Int

export
(.isSocket) : Stats r -> Bool
(.isSocket) stats = 0 /= ffi_isSocket stats

%foreign "node:lambda: (ty,s)=>s.isSymbolicLink() ? 1 : 0"
ffi_isSymbolicLink : Stats r -> Int

export
(.isSymbolicLink) : Stats r -> Bool
(.isSymbolicLink) stats = 0 /= ffi_isSymbolicLink stats

%foreign "node:lambda: (rty,aty,s)=>s.size"
ffi_size : Stats r -> a

export
size : Stats r -> statsReturnType r
size stats = ffi_size stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.dev"
ffi_dev : Stats r -> a

export
dev : Stats r -> statsReturnType r
dev stats = ffi_dev stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.ino"
ffi_ino : Stats r -> a

export
ino : Stats r -> statsReturnType r
ino stats = ffi_ino stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.mode"
ffi_mode : Stats r -> a

export
mode : Stats r -> statsReturnType r
mode stats = ffi_mode stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.nlink"
ffi_nlink : Stats r -> a

export
nlink : Stats r -> statsReturnType r
nlink stats = ffi_nlink stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.uid"
ffi_uid : Stats r -> a

export
uid : Stats r -> statsReturnType r
uid stats = ffi_uid stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.gid"
ffi_gid : Stats r -> a

export
gid : Stats r -> statsReturnType r
gid stats = ffi_gid stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.rdev"
ffi_rdev : Stats r -> a

export
rdev : Stats r -> statsReturnType r
rdev stats = ffi_rdev stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.blksize"
ffi_blksize : Stats r -> a

export
blksize : Stats r -> statsReturnType r
blksize stats = ffi_blksize stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.blocks"
ffi_blocks : Stats r -> a

export
blocks : Stats r -> statsReturnType r
blocks stats = ffi_blocks stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.atimeMs"
ffi_atimeMs : Stats r -> a

export
atimeMs : Stats r -> statsReturnType r
atimeMs stats = ffi_atimeMs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.ctimeMs"
ffi_ctimeMs : Stats r -> a

%foreign "node:lambda: (rty,aty,s)=>s.mtimeMs"
ffi_mtimeMs : Stats r -> a

export
mtimeMs : Stats r -> statsReturnType r
mtimeMs stats = ffi_mtimeMs stats { a = statsReturnType r }

export
ctimeMs : Stats r -> statsReturnType r
ctimeMs stats = ffi_ctimeMs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.birthtimeMs"
ffi_birthtimeMs : Stats r -> a

export
birthtimeMs : Stats r -> statsReturnType r
birthtimeMs stats = ffi_birthtimeMs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.atimeNs"
ffi_atimeNs : Stats r -> a

export
atimeNs : Stats r -> statsReturnType r
atimeNs stats = ffi_atimeNs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.mtimeNs"
ffi_mtimeNs : Stats r -> a

export
mtimeNs : Stats r -> statsReturnType r
mtimeNs stats = ffi_mtimeNs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.ctimeNs"
ffi_ctimeNs : Stats r -> a

export
ctimeNs : Stats r -> statsReturnType r
ctimeNs stats = ffi_ctimeNs stats { a = statsReturnType r }

%foreign "node:lambda: (rty,aty,s)=>s.birthtimeNs"
ffi_birthtimeNs : Stats r -> a

export
birthtimeNs : Stats r -> statsReturnType r
birthtimeNs stats = ffi_birthtimeNs stats { a = statsReturnType r }

{-
Missing implementations for:
- atime
- mtime
- ctime
- birthtime
-}

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

import lib.Library1

main : IO ()
main = putStrLn salute


text:
module Personal

public export
record Personal where
  constructor CreatePersonal
  political : Integer
  langs : List String
  religion : String
  inspiredBy : String
  peopleMain : Integer
  lifeMain : Integer
  smoking : Integer
  alcohol : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module ParserHack
import Schema
import SQLiteTypes

%access export

people : String
people = "CREATE TABLE \"people\" (\"id\" INTEGER PRIMARY KEY  AUTOINCREMENT  NOT NULL  UNIQUE , \"name\" VARCHAR NOT NULL , \"age\" INTEGER)"

--quote : Char
--quote = '\"'

--createTable : Parser Char List ()
--createTable = str (unpack "CREATE") ~ many1 space ~ str (unpack "TABLE") ^^^ ()

-- schema : Parser String
-- schema = do createTable
--             many1 space
--             is quote
--             res <- many1 (isNot quote)
--             is quote
--             many1 space
--             return (pack res)
-- --            sequence_ [ is quote, many1 space, is '(']
-- --            return (pack res)

dropPrefixBy : (a -> a -> Bool) -> List a -> List a -> Maybe (List a)
dropPrefixBy p [] ys = Just ys
dropPrefixBy p (x::xs) [] = Nothing
dropPrefixBy p (x::xs) (y::ys) = if p x y then dropPrefixBy p xs ys else Nothing

getWhile : (a -> Bool) -> List a -> (List a, List a)
getWhile p [] = ([], [])
getWhile p (x::xs) with (p x)
  | True = let (ok, rest) = getWhile p xs
           in (x :: ok, rest)
  | False = ([], x::xs)

isPrefix : (Eq a) => List a -> List a -> Bool
isPrefix [] _ = True
isPrefix (x::xs) [] = False
isPrefix (x::xs) (y::ys) = x == y && isPrefix xs ys

subList : (Eq a) => List a -> List a -> Bool
subList [] _ = False
subList (x::xs) [] = False
subList (x::xs) (y::ys) = (x == y && isPrefix xs ys) || subList (x::xs) ys

isNullable : String -> Bool
isNullable = not . subList ["NOT", "NULL"] . split (==' ')

getType : String -> Maybe String
getType opts = List.find (isType . toUpper) (split (==' ') opts)
    where isType : String -> Bool
          isType x = List.elem x ["INTEGER", "VARCHAR", "TEXT", "INT" ]

colNameTypeNullable : String -> Maybe (String, String, Bool)
colNameTypeNullable col = case dropPrefixBy (==) [] (unpack (trim col)) of
                            Nothing   => Nothing
                            Just rest => let (name, rest') = (getWhile (/= ' ') rest)
                                         in case dropPrefixBy (==) [' '] rest' of
                                            Just rest'' => case getType (pack rest'') of
                                                             Just tp => Just (pack name, tp, isNullable (toUpper (pack rest'')))
                                                             Nothing => Nothing
                                            Nothing     => Nothing

nameCols : String -> Maybe (String, List String)
nameCols schema = case dropPrefixBy (\x,y => toLower x == toLower y) (unpack "create table ") (unpack schema) of
                    Nothing => Nothing
                    Just rest => let (name, rest') = (getWhile (/= ' ') rest)
                                 in case dropPrefixBy (==) [' ', '('] rest' of
                                      Just rest'' => case dropPrefixBy (==) [')'] (reverse rest'') of
                                                       Just rest''' =>
                                                         Just (pack name, split (==',') (pack (reverse rest''')))
                                                       Nothing => Nothing
                                      Nothing => Nothing

parse : String -> Maybe (String, List (String, String, Bool))
parse schema = case nameCols schema of
                 Just (n, cols) => case sequence {f=Maybe} (map colNameTypeNullable (filter isColumn cols)) of
                                     Just cols' => Just (n, cols')
                                     Nothing => Nothing
                 Nothing => Nothing
  where isColumn : String -> Bool
        isColumn col = not $ isPrefixOf "foreign" (toLower (trim col))
toSchema : List (String, String, Bool) -> Maybe Schema
toSchema [] = Just []
toSchema ((colName, colT, nullable)::cols) = do tp <- getType (toUpper colT) nullable
                                                rest <- toSchema cols
                                                return ((colName:::tp) :: rest)
    where getType : String -> Bool -> Maybe SQLiteType
          getType t         True  = map NULLABLE (getType t False)
          getType "VARCHAR" False = Just TEXT
          getType "TEXT"    False = Just TEXT
          getType "INTEGER" False = Just INTEGER
          getType "INT"     False = Just INTEGER
          getType "REAL"    False = Just REAL
          getType _         False = Nothing

getSchema : String -> Maybe (String, Schema)
getSchema str = do nameCols <- parse str
                   tableSchema <- toSchema (snd nameCols)
                   Just (fst nameCols, tableSchema)

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
-- Shape.idr
--
-- Demonstrate union data types

module Shape

||| Represents shapes
public export
data Shape = ||| A triangle, with its base and height
             Triangle Double Double
           | ||| A rectangle, with length and height
             Rectangle Double Double
           | ||| A circle, with radius
             Circle Double

%name Shape shape, shape1, shape2

||| Calculates area of given shape
export
area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Main

import Data.SortedMap
import FLK_bos
import FLK_ast
import Effects
import Effect.StdIO

evalPrint : (s ** CF s) -> { [STDIO] } Eff ()
evalPrint (MkSigma x pf) with (evalCF x pf)
  evalPrint (MkSigma x pf) | Nothing = putStrLn $ "No evaluation for:" ++ (show pf)
  evalPrint (MkSigma x pf) | (Just (MkSigma y z)) = putStrLn $ (show pf) ++ " evaluates to " ++ (show y) ++ "by\n\t: " ++ (show z)

main : IO ()
main = run $ evalPrint ycomb

max_stars_repo_name: ezrosent/FLK-Semantics

max_issues_repo_name: ezrosent/FLK-Semantics

max_forks_repo_name: ezrosent/FLK-Semantics


text:
module Web.Internal.StreamsTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace ReadableStreamReaderMode

  public export
  data ReadableStreamReaderMode = Byob

  public export
  Show ReadableStreamReaderMode where
    show Byob = "byob"

  public export
  Eq ReadableStreamReaderMode where
    (==) = (==) `on` show

  public export
  Ord ReadableStreamReaderMode where
    compare = compare `on` show

  public export
  read : String -> Maybe ReadableStreamReaderMode
  read "byob" = Just Byob
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ReadableStreamReaderMode.read s)}
             -> ReadableStreamReaderMode
  fromString s = fromJust $ read s

  export
  ToFFI ReadableStreamReaderMode String where
    toFFI = show

  export
  FromFFI ReadableStreamReaderMode String where
    fromFFI = read

namespace ReadableStreamType

  public export
  data ReadableStreamType = Bytes

  public export
  Show ReadableStreamType where
    show Bytes = "bytes"

  public export
  Eq ReadableStreamType where
    (==) = (==) `on` show

  public export
  Ord ReadableStreamType where
    compare = compare `on` show

  public export
  read : String -> Maybe ReadableStreamType
  read "bytes" = Just Bytes
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ReadableStreamType.read s)}
             -> ReadableStreamType
  fromString s = fromJust $ read s

  export
  ToFFI ReadableStreamType String where
    toFFI = show

  export
  FromFFI ReadableStreamType String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data ByteLengthQueuingStrategy : Type where [external]

export
ToFFI ByteLengthQueuingStrategy ByteLengthQueuingStrategy where toFFI = id

export
FromFFI ByteLengthQueuingStrategy ByteLengthQueuingStrategy where fromFFI = Just

export
SafeCast ByteLengthQueuingStrategy where
  safeCast = unsafeCastOnPrototypeName "ByteLengthQueuingStrategy"

export data CountQueuingStrategy : Type where [external]

export
ToFFI CountQueuingStrategy CountQueuingStrategy where toFFI = id

export
FromFFI CountQueuingStrategy CountQueuingStrategy where fromFFI = Just

export
SafeCast CountQueuingStrategy where
  safeCast = unsafeCastOnPrototypeName "CountQueuingStrategy"

export data ReadableByteStreamController : Type where [external]

export
ToFFI ReadableByteStreamController ReadableByteStreamController where toFFI = id

export
FromFFI ReadableByteStreamController ReadableByteStreamController where fromFFI = Just

export
SafeCast ReadableByteStreamController where
  safeCast = unsafeCastOnPrototypeName "ReadableByteStreamController"

export data ReadableStream : Type where [external]

export
ToFFI ReadableStream ReadableStream where toFFI = id

export
FromFFI ReadableStream ReadableStream where fromFFI = Just

export
SafeCast ReadableStream where
  safeCast = unsafeCastOnPrototypeName "ReadableStream"

export data ReadableStreamBYOBReader : Type where [external]

export
ToFFI ReadableStreamBYOBReader ReadableStreamBYOBReader where toFFI = id

export
FromFFI ReadableStreamBYOBReader ReadableStreamBYOBReader where fromFFI = Just

export
SafeCast ReadableStreamBYOBReader where
  safeCast = unsafeCastOnPrototypeName "ReadableStreamBYOBReader"

export data ReadableStreamBYOBRequest : Type where [external]

export
ToFFI ReadableStreamBYOBRequest ReadableStreamBYOBRequest where toFFI = id

export
FromFFI ReadableStreamBYOBRequest ReadableStreamBYOBRequest where fromFFI = Just

export
SafeCast ReadableStreamBYOBRequest where
  safeCast = unsafeCastOnPrototypeName "ReadableStreamBYOBRequest"

export data ReadableStreamDefaultController : Type where [external]

export
ToFFI ReadableStreamDefaultController ReadableStreamDefaultController where toFFI = id

export
FromFFI ReadableStreamDefaultController ReadableStreamDefaultController where fromFFI = Just

export
SafeCast ReadableStreamDefaultController where
  safeCast = unsafeCastOnPrototypeName "ReadableStreamDefaultController"

export data ReadableStreamDefaultReader : Type where [external]

export
ToFFI ReadableStreamDefaultReader ReadableStreamDefaultReader where toFFI = id

export
FromFFI ReadableStreamDefaultReader ReadableStreamDefaultReader where fromFFI = Just

export
SafeCast ReadableStreamDefaultReader where
  safeCast = unsafeCastOnPrototypeName "ReadableStreamDefaultReader"

export data TransformStream : Type where [external]

export
ToFFI TransformStream TransformStream where toFFI = id

export
FromFFI TransformStream TransformStream where fromFFI = Just

export
SafeCast TransformStream where
  safeCast = unsafeCastOnPrototypeName "TransformStream"

export data TransformStreamDefaultController : Type where [external]

export
ToFFI TransformStreamDefaultController TransformStreamDefaultController where toFFI = id

export
FromFFI TransformStreamDefaultController TransformStreamDefaultController where fromFFI = Just

export
SafeCast TransformStreamDefaultController where
  safeCast = unsafeCastOnPrototypeName "TransformStreamDefaultController"

export data WritableStream : Type where [external]

export
ToFFI WritableStream WritableStream where toFFI = id

export
FromFFI WritableStream WritableStream where fromFFI = Just

export
SafeCast WritableStream where
  safeCast = unsafeCastOnPrototypeName "WritableStream"

export data WritableStreamDefaultController : Type where [external]

export
ToFFI WritableStreamDefaultController WritableStreamDefaultController where toFFI = id

export
FromFFI WritableStreamDefaultController WritableStreamDefaultController where fromFFI = Just

export
SafeCast WritableStreamDefaultController where
  safeCast = unsafeCastOnPrototypeName "WritableStreamDefaultController"

export data WritableStreamDefaultWriter : Type where [external]

export
ToFFI WritableStreamDefaultWriter WritableStreamDefaultWriter where toFFI = id

export
FromFFI WritableStreamDefaultWriter WritableStreamDefaultWriter where fromFFI = Just

export
SafeCast WritableStreamDefaultWriter where
  safeCast = unsafeCastOnPrototypeName "WritableStreamDefaultWriter"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data QueuingStrategy : Type where [external]

export
ToFFI QueuingStrategy QueuingStrategy where toFFI = id

export
FromFFI QueuingStrategy QueuingStrategy where fromFFI = Just

export data QueuingStrategyInit : Type where [external]

export
ToFFI QueuingStrategyInit QueuingStrategyInit where toFFI = id

export
FromFFI QueuingStrategyInit QueuingStrategyInit where fromFFI = Just

export data ReadableStreamBYOBReadResult : Type where [external]

export
ToFFI ReadableStreamBYOBReadResult ReadableStreamBYOBReadResult where toFFI = id

export
FromFFI ReadableStreamBYOBReadResult ReadableStreamBYOBReadResult where fromFFI = Just

export data ReadableStreamDefaultReadResult : Type where [external]

export
ToFFI ReadableStreamDefaultReadResult ReadableStreamDefaultReadResult where toFFI = id

export
FromFFI ReadableStreamDefaultReadResult ReadableStreamDefaultReadResult where fromFFI = Just

export data ReadableStreamGetReaderOptions : Type where [external]

export
ToFFI ReadableStreamGetReaderOptions ReadableStreamGetReaderOptions where toFFI = id

export
FromFFI ReadableStreamGetReaderOptions ReadableStreamGetReaderOptions where fromFFI = Just

export data ReadableStreamIteratorOptions : Type where [external]

export
ToFFI ReadableStreamIteratorOptions ReadableStreamIteratorOptions where toFFI = id

export
FromFFI ReadableStreamIteratorOptions ReadableStreamIteratorOptions where fromFFI = Just

export data ReadableWritablePair : Type where [external]

export
ToFFI ReadableWritablePair ReadableWritablePair where toFFI = id

export
FromFFI ReadableWritablePair ReadableWritablePair where fromFFI = Just

export data StreamPipeOptions : Type where [external]

export
ToFFI StreamPipeOptions StreamPipeOptions where toFFI = id

export
FromFFI StreamPipeOptions StreamPipeOptions where fromFFI = Just

export data Transformer : Type where [external]

export
ToFFI Transformer Transformer where toFFI = id

export
FromFFI Transformer Transformer where fromFFI = Just

export data UnderlyingSink : Type where [external]

export
ToFFI UnderlyingSink UnderlyingSink where toFFI = id

export
FromFFI UnderlyingSink UnderlyingSink where fromFFI = Just

export data UnderlyingSource : Type where [external]

export
ToFFI UnderlyingSource UnderlyingSource where toFFI = id

export
FromFFI UnderlyingSource UnderlyingSource where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data GenericTransformStream : Type where [external]

export
ToFFI GenericTransformStream GenericTransformStream where toFFI = id

export
FromFFI GenericTransformStream GenericTransformStream where fromFFI = Just

export data ReadableStreamGenericReader : Type where [external]

export
ToFFI ReadableStreamGenericReader ReadableStreamGenericReader where toFFI = id

export
FromFFI ReadableStreamGenericReader ReadableStreamGenericReader where fromFFI = Just

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export data QueuingStrategySize : Type where [external]

export
ToFFI QueuingStrategySize QueuingStrategySize where toFFI = id

export
FromFFI QueuingStrategySize QueuingStrategySize where fromFFI = Just

export data TransformerFlushCallback : Type where [external]

export
ToFFI TransformerFlushCallback TransformerFlushCallback where toFFI = id

export
FromFFI TransformerFlushCallback TransformerFlushCallback where fromFFI = Just

export data TransformerStartCallback : Type where [external]

export
ToFFI TransformerStartCallback TransformerStartCallback where toFFI = id

export
FromFFI TransformerStartCallback TransformerStartCallback where fromFFI = Just

export data TransformerTransformCallback : Type where [external]

export
ToFFI TransformerTransformCallback TransformerTransformCallback where toFFI = id

export
FromFFI TransformerTransformCallback TransformerTransformCallback where fromFFI = Just

export data UnderlyingSinkAbortCallback : Type where [external]

export
ToFFI UnderlyingSinkAbortCallback UnderlyingSinkAbortCallback where toFFI = id

export
FromFFI UnderlyingSinkAbortCallback UnderlyingSinkAbortCallback where fromFFI = Just

export data UnderlyingSinkCloseCallback : Type where [external]

export
ToFFI UnderlyingSinkCloseCallback UnderlyingSinkCloseCallback where toFFI = id

export
FromFFI UnderlyingSinkCloseCallback UnderlyingSinkCloseCallback where fromFFI = Just

export data UnderlyingSinkStartCallback : Type where [external]

export
ToFFI UnderlyingSinkStartCallback UnderlyingSinkStartCallback where toFFI = id

export
FromFFI UnderlyingSinkStartCallback UnderlyingSinkStartCallback where fromFFI = Just

export data UnderlyingSinkWriteCallback : Type where [external]

export
ToFFI UnderlyingSinkWriteCallback UnderlyingSinkWriteCallback where toFFI = id

export
FromFFI UnderlyingSinkWriteCallback UnderlyingSinkWriteCallback where fromFFI = Just

export data UnderlyingSourceCancelCallback : Type where [external]

export
ToFFI UnderlyingSourceCancelCallback UnderlyingSourceCancelCallback where toFFI = id

export
FromFFI UnderlyingSourceCancelCallback UnderlyingSourceCancelCallback where fromFFI = Just

export data UnderlyingSourcePullCallback : Type where [external]

export
ToFFI UnderlyingSourcePullCallback UnderlyingSourcePullCallback where toFFI = id

export
FromFFI UnderlyingSourcePullCallback UnderlyingSourcePullCallback where fromFFI = Just

export data UnderlyingSourceStartCallback : Type where [external]

export
ToFFI UnderlyingSourceStartCallback UnderlyingSourceStartCallback where toFFI = id

export
FromFFI UnderlyingSourceStartCallback UnderlyingSourceStartCallback where fromFFI = Just


text:
-- For Sergey ;-)

module TypList

import Data.List.Elem

lst1 : List Type
lst1 = [Int]

lst2 : List Type
lst2 = [forall p. Num p => p]

au : Elem x xs => Elem x xs
au @{el} = el

f : Elem Int TypList.lst2
f = au

g : Elem (forall p. Num p => p) TypList.lst1
g = au

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module LightClick.IR.Channel.MicroSV.Update

import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DList.DeBruijn

import LightClick.IR.ModuleCentric
import LightClick.IR.Channel.MicroSV.Error

import Language.SystemVerilog.MetaTypes
import Language.SystemVerilog.Micro

%default covering -- this file has caused the totality checker to hang.

export
update : (newGlobal : Context)
      -> (expr : Expr local globalOld type)
      -> Either TError (Expr local newGlobal type)

updateKV : (newGlobal : Context)
        -> (String, Expr local globalOld type)
        -> Either TError (String, Expr local newGlobal type)
updateKV newGlobal (k,v) =
    do v' <- update newGlobal v
       pure (k,v')

updateKVs : (newGlobal : Context)
         -> (es : Vect n (String, Expr local global type))
         -> Either TError (Vect n (String, Expr local newGlobal type))
updateKVs newGlobal = traverse (updateKV newGlobal)

updateChans: (newGlobal : Context)
          -> (es : Vect (S (S n)) (Expr local global type))
          -> Either TError (Vect (S (S n)) (Expr local newGlobal type))
updateChans newGlobal = traverse (update newGlobal)

updateDecl : (newGlobal : Context)
          -> (expr : Expr local globalOld (PORT s))
         -> Either TError (Expr local newGlobal (PORT s))
updateDecl newGlobal = update newGlobal

updateMDecl : (newGlobal : Context)
         -> (ps : DList String (\s => Expr lctxt gctxt (PORT  s)) names)
         -> Either TError (DList String (\s => Expr lctxt newGlobal (PORT s)) names)
updateMDecl newGlobal [] = pure Nil
updateMDecl newGlobal (e :: rest) =
    do e' <- updateDecl newGlobal e
       es <- updateMDecl newGlobal rest
       pure (e' :: es)

update newGlobal End = pure End
update newGlobal (Local label x) = pure $ Local label x
update newGlobal (Global label {ty} x) with (isElem (label,ty) newGlobal)
  update newGlobal (Global label {ty} x) | (Yes idx) = Right (Global label (idx))

  update newGlobal (Global label {ty} x) | (No contra) = Left (IdentifierNotFound label)

update newGlobal (Let this beThis withType prf inThis) =
    do beThis' <- update newGlobal beThis
       wType'  <- update newGlobal withType
       inThis' <- update newGlobal inThis
       pure (Let this beThis' wType' prf inThis')
update newGlobal (Seq x y) =
    do x' <- update newGlobal x
       y' <- update newGlobal y
       pure (Seq x' y')

update newGlobal TYPE = pure TYPE
update newGlobal GATE = pure GATE

update newGlobal DataLogic = pure DataLogic
update newGlobal (DataArray type size) =
    do type' <- update newGlobal type
       pure (DataArray type' size)
update newGlobal (DataStruct xs) =
    do xs' <- updateKVs newGlobal xs
       pure (DataStruct xs')

update newGlobal (DataUnion xs) =
    do xs' <- updateKVs newGlobal xs
       pure (DataUnion xs')

update newGlobal (Port label dir type) =
    do type' <- update newGlobal type
       pure (Port label dir type')
update newGlobal (MDecl xs) =
    do xs' <- updateMDecl newGlobal xs
       pure (MDecl xs')

update newGlobal NewChan = pure NewChan

update newGlobal (NewModule xs) =
    do xs' <- traverse (updateKV newGlobal) xs
       pure (NewModule xs')

update newGlobal (Not o i) =
    do x' <- update newGlobal o
       y' <- update newGlobal i
       pure (Not x' y')

update newGlobal (Gate ty o xs) =
    do o' <- update newGlobal o
       xs' <- traverse (update newGlobal) xs
       pure (Gate ty o' xs')

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick