text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.DOM.Node

import IdrisScript

%access public export
%default total

||| The original specification can be found at
||| https://dom.spec.whatwg.org/#interface-documenttype
record DocumentType where
  constructor New
  name     : String
  publicId : String
  systemId : String
  self     : JSRef

||| documentTypeFromPointer is a helper function for easily creating
||| DocumentTypes from JavaScript references.
|||
||| @ ref a pointer to a documentType
documentTypeFromPointer : (ref : JSRef) -> JS_IO $ Maybe DocumentType
documentTypeFromPointer ref = let
    nameRef     = jscall "%0.name"     (JSRef -> JS_IO JSRef) ref
    publicIdRef = jscall "%0.publicId" (JSRef -> JS_IO JSRef) ref
    systemIdRef = jscall "%0.systemId" (JSRef -> JS_IO JSRef) ref
  in
    case !(IdrisScript.pack !nameRef) of
      (JSString ** name) => case !(IdrisScript.pack !publicIdRef) of
        (JSString ** pubId) => case !(IdrisScript.pack !systemIdRef) of
          (JSString ** sysId) => pure $ Just $
                                 New (fromJS name) (fromJS pubId) (fromJS sysId)
                                      ref
          _                   => pure Nothing
        _                   => pure Nothing
      _                  => pure Nothing

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module Compiler.ES.ES

import Compiler.ES.Imperative
import Utils.Hex
import Data.List1
import Data.Strings
import Data.SortedMap
import Data.String.Extra

import Core.Directory

data ESs : Type where

record ESSt where
  constructor MkESSt
  preamble : SortedMap String String
  ccTypes : List String

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) ++ "}"

esName : String -> String
esName x = "__esPrim_" ++ x

addToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> String -> Core String
addToPreamble name newName def =
  do
    s <- get ESs
    case lookup name (preamble s) of
      Nothing =>
        do
          put ESs (record { preamble = insert name def (preamble s) } s)
          pure newName
      Just x =>
        if x /= def then throw $ InternalError $ "two incompatible definitions for " ++ name ++ "<|" ++ x ++"|> <|"++ def ++ "|>"
                    else pure newName

addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String
addConstToPreamble name def =
  do
    let newName = esName name
    let v = "const " ++ newName ++ " = (" ++ def ++ ");"
    addToPreamble name newName v

requireSafe : String -> String
requireSafe = pack . map (\c => case c of
                                     '@' => '_'
                                     '/' => '_'
                                     '-' => '_'
                                     _ => c
                         ) . unpack
addRequireToPreamble : {auto c : Ref ESs ESSt} -> String -> Core String
addRequireToPreamble name =
  do
    let newName = "__require_" ++ requireSafe name
    let v = "const " ++ newName ++ " = require(" ++ jsString name ++ ");"
    addToPreamble name newName v

addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String
addSupportToPreamble name code =
  addToPreamble name name code

jsIdent : String -> String
jsIdent s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar c = if isAlphaNum c
                  then cast c
                  else "$" ++ the (String) (asHex (cast {to=Int} c))

keywordSafe : String -> String
keywordSafe "var" = "var_"
keywordSafe s = s

jsName : Name -> String
jsName (NS ns n) = showNSWithSep "_" ns ++ "_" ++ jsName n
jsName (UN n) = keywordSafe $ jsIdent 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

jsCrashExp : {auto c : Ref ESs ESSt} -> String -> Core String
jsCrashExp message  =
  do
    n <- addConstToPreamble "crashExp" "x=>{throw new IdrisError(x)}"
    pure $ n ++ "("++ message ++ ")"

jsIntegerOfString : {auto c : Ref ESs ESSt} -> String -> Core String
jsIntegerOfString x =
  do
    n <- addConstToPreamble "integerOfString" "s=>{const idx = s.indexOf('.'); return idx === -1 ? BigInt(s) : BigInt(s.slice(0, idx));}"
    pure $ n ++ "(" ++ x ++ ")"

nSpaces : Nat -> String
nSpaces n = pack $ List.replicate n ' '

binOp : String -> String -> String -> String
binOp o lhs rhs = "(" ++ lhs ++ " " ++ o ++ " " ++ rhs ++ ")"

toBigInt : String -> String
toBigInt e = "BigInt(" ++ e ++ ")"

fromBigInt : String -> String
fromBigInt e = "Number(" ++ e ++ ")"

makeIntBound : {auto c : Ref ESs ESSt} -> Int -> Core String
makeIntBound bits = addConstToPreamble ("int_bound_" ++ show bits) ("BigInt(2) ** BigInt("++ show bits ++") ")

boundedInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String
boundedInt bits e =
  do
    n <- makeIntBound bits
    pure $ "(" ++ e ++ " % " ++ n ++ ")"

boundedUInt : {auto c : Ref ESs ESSt} -> Int -> String -> Core String
boundedUInt bits e =
  do
    n <- makeIntBound bits
    fn <- addConstToPreamble ("truncToUInt"++show bits) ("x=>{const m = x%" ++ n ++ ";return m>0?m:m+" ++ n ++ "}")
    pure $ fn ++ "(" ++ e ++ ")"

boundedIntOp : {auto c : Ref ESs ESSt} -> Int -> String -> String -> String -> Core String
boundedIntOp bits o lhs rhs = boundedInt bits (binOp o lhs rhs)

boundedUIntOp : {auto c : Ref ESs ESSt} -> Int -> String -> String -> String -> Core String
boundedUIntOp bits o lhs rhs = boundedUInt bits (binOp o lhs rhs)

boolOp : String -> String -> String -> String
boolOp o lhs rhs = "(" ++ binOp o lhs rhs ++ " ? BigInt(1) : BigInt(0))"

jsConstant : {auto c : Ref ESs ESSt} -> Constant -> Core String
jsConstant (I i) = pure $ show i ++ "n"
jsConstant (BI i) = pure $ show i ++ "n"
jsConstant (Str s) = pure $ jsString s
jsConstant (Ch c) = pure $ jsString $ Data.Strings.singleton c
jsConstant (Db f) = pure $ show f
jsConstant WorldVal = addConstToPreamble "idrisworld" "Symbol('idrisworld')";
jsConstant (B8 i) = pure $ show i ++ "n"
jsConstant (B16 i) = pure $ show i ++ "n"
jsConstant (B32 i) = pure $ show i ++ "n"
jsConstant (B64 i) = pure $ show i ++ "n"
jsConstant ty = throw (InternalError $ "Unsuported constant " ++ show ty)

jsOp : {auto c : Ref ESs ESSt} -> PrimFn arity -> Vect arity String -> Core String
jsOp (Add IntType) [x, y] = pure $ !(boundedIntOp 63 "+" x y)
jsOp (Sub IntType) [x, y] = pure $ !(boundedIntOp 63 "-" x y)
jsOp (Mul IntType) [x, y] = pure $ !(boundedIntOp 63 "*" x y)
jsOp (Div IntType) [x, y] = pure $ !(boundedIntOp 63 "/" x y)
jsOp (Mod IntType) [x, y] = pure $ !(boundedIntOp 63 "%" x y)
jsOp (Add Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "+" x y)
jsOp (Sub Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "-" x y)
jsOp (Mul Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "*" x y)
jsOp (Div Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "/" x y)
jsOp (Mod Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "%" x y)
jsOp (Add Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "+" x y)
jsOp (Sub Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "-" x y)
jsOp (Mul Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "*" x y)
jsOp (Div Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "/" x y)
jsOp (Mod Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "%" x y)
jsOp (Add Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "+" x y)
jsOp (Sub Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "-" x y)
jsOp (Mul Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "*" x y)
jsOp (Div Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "/" x y)
jsOp (Mod Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "%" x y)
jsOp (Add Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "+" x y)
jsOp (Sub Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "-" x y)
jsOp (Mul Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "*" x y)
jsOp (Div Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "/" x y)
jsOp (Mod Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "%" x y)
jsOp (Add ty) [x, y] = pure $ binOp "+" x y
jsOp (Sub ty) [x, y] = pure $ binOp "-" x y
jsOp (Mul ty) [x, y] = pure $ binOp "*" x y
jsOp (Div ty) [x, y] = pure $ binOp "/" x y
jsOp (Mod ty) [x, y] = pure $ binOp "%" x y
jsOp (Neg ty) [x] = pure $ "(-(" ++ x ++ "))"
jsOp (ShiftL IntType) [x, y] = pure $ !(boundedUIntOp 63 "<<" x y)
jsOp (ShiftL Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 "<<" x y)
jsOp (ShiftL Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 "<<" x y)
jsOp (ShiftL Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 "<<" x y)
jsOp (ShiftL Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 "<<" x y)
jsOp (ShiftL ty) [x, y] = pure $ binOp "<<" x y
jsOp (ShiftR IntType) [x, y] = pure $ !(boundedUIntOp 63 ">>" x y)
jsOp (ShiftR Bits8Type) [x, y] = pure $ !(boundedUIntOp 8 ">>" x y)
jsOp (ShiftR Bits16Type) [x, y] = pure $ !(boundedUIntOp 16 ">>" x y)
jsOp (ShiftR Bits32Type) [x, y] = pure $ !(boundedUIntOp 32 ">>" x y)
jsOp (ShiftR Bits64Type) [x, y] = pure $ !(boundedUIntOp 64 ">>" x y)
jsOp (ShiftR ty) [x, y] = pure $ binOp ">>" 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 $ toBigInt $ x ++ ".length"
jsOp StrHead [x] = pure $ "(" ++ x ++ ".charAt(0))"
jsOp StrTail [x] = pure $ "(" ++ x ++ ".slice(1))"
jsOp StrIndex [x, y] = pure $ "(" ++ x ++ ".charAt(" ++ fromBigInt y ++ "))"
jsOp StrCons [x, y] = pure $ binOp "+" x y
jsOp StrAppend [x, y] = pure $ binOp "+" x y
jsOp StrReverse [x] =
  do
    n <- addConstToPreamble "strReverse" "x => x.split('').reverse().join('')"
    pure $ n ++ "(" ++ x ++ ")"
jsOp StrSubstr [offset, length, str] =
  pure $ str ++ ".slice(" ++ fromBigInt offset ++ ", " ++ fromBigInt offset ++ " + " ++ fromBigInt length ++ ")"
jsOp DoubleExp [x] = pure $ "Math.exp(" ++ x ++ ")"
jsOp DoubleLog [x] = pure $ "Math.log(" ++ x ++ ")"
jsOp DoubleSin [x] = pure $ "Math.sin(" ++ x ++ ")"
jsOp DoubleCos [x] = pure $ "Math.cos(" ++ x ++ ")"
jsOp DoubleTan [x] = pure $ "Math.tan(" ++ x ++ ")"
jsOp DoubleASin [x] = pure $ "Math.asin(" ++ x ++ ")"
jsOp DoubleACos [x] = pure $ "Math.acos(" ++ x ++ ")"
jsOp DoubleATan [x] = pure $ "Math.atan(" ++ x ++ ")"
jsOp DoubleSqrt [x] = pure $ "Math.sqrt(" ++ x ++ ")"
jsOp DoubleFloor [x] = pure $ "Math.floor(" ++ x ++ ")"
jsOp DoubleCeiling [x] = pure $ "Math.ceil(" ++ x ++ ")"
jsOp (Cast IntType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast IntegerType CharType) [x] = pure $ "String.fromCodePoint(" ++ fromBigInt x ++ ")"
jsOp (Cast CharType IntType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
jsOp (Cast CharType IntegerType) [x] = pure $ toBigInt $ x ++ ".codePointAt(0)"
jsOp (Cast DoubleType IntType) [x] = boundedInt 63 $ "BigInt(Math.floor(" ++ x ++ "))"
jsOp (Cast DoubleType IntegerType) [x] = pure $ "BigInt(Math.floor(" ++ x ++ "))"
jsOp (Cast StringType IntType) [x] = boundedInt 63 $ !(jsIntegerOfString x)
jsOp (Cast StringType IntegerType) [x] = jsIntegerOfString x
jsOp (Cast IntegerType IntType) [x] = boundedInt 63 x
jsOp (Cast IntType IntegerType) [x] = pure x
jsOp (Cast StringType DoubleType) [x] = pure $ "parseFloat(" ++ x ++ ")"

jsOp (Cast IntType Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast IntType Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast IntType Bits32Type) [x] = boundedUInt 32 x
jsOp (Cast IntType Bits64Type) [x] = boundedUInt 64 x

jsOp (Cast IntegerType Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast IntegerType Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast IntegerType Bits32Type) [x] = boundedUInt 32 x
jsOp (Cast IntegerType Bits64Type) [x] = boundedUInt 64 x

jsOp (Cast Bits8Type Bits16Type) [x] = pure x
jsOp (Cast Bits8Type Bits32Type) [x] = pure x
jsOp (Cast Bits8Type Bits64Type) [x] = pure x

jsOp (Cast Bits16Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits16Type Bits32Type) [x] = pure x
jsOp (Cast Bits16Type Bits64Type) [x] = pure x

jsOp (Cast Bits32Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits32Type Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast Bits32Type Bits64Type) [x] = pure x

jsOp (Cast Bits64Type Bits8Type) [x] = boundedUInt 8 x
jsOp (Cast Bits64Type Bits16Type) [x] = boundedUInt 16 x
jsOp (Cast Bits64Type Bits32Type) [x] = boundedUInt 32 x

jsOp (Cast ty StringType) [x] = pure $ "(''+" ++ x ++ ")"
jsOp (Cast ty ty2) [x] = jsCrashExp $ "invalid cast: + " ++ show ty ++ " + ' -> ' + " ++ show ty2
jsOp BelieveMe [_,_,x] = pure x
jsOp (Crash) [_, msg] = jsCrashExp msg

readCCPart : String -> (String, String)
readCCPart x =
  let (cc, def) = break (== ':') x
  in (cc, drop 1 def)

searchForeign : List String -> List String -> Maybe String
searchForeign prefixes [] = Nothing
searchForeign prefixes (x::xs) =
  let (cc, def) = readCCPart x
  in if cc `elem` prefixes then Just def
                           else searchForeign prefixes xs

makeForeign : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> String -> Core String
makeForeign n x =
  do
    let (ty, def) = readCCPart x
    case ty of
      "lambda" => pure $ "const " ++ jsName n ++ " = (" ++ def ++ ")\n"
      "lambdaRequire" =>
        do
          let (libs, def_) = readCCPart def
          traverseList1 addRequireToPreamble (split (==',') libs)
          pure $ "const " ++ jsName n ++ " = (" ++ def_ ++ ")\n"
      "support" =>
        do
          let (name, lib_) = break (== ',') def
          let lib = drop 1 lib_
          lib_code <- readDataFile ("js/" ++ lib ++ ".js")
          addSupportToPreamble lib lib_code
          pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n"

      _ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"lambdaRequire\", \"support\"")

foreignDecl : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> List String -> Core String
foreignDecl n ccs =
  do
    s <- get ESs
    case searchForeign (ccTypes s) ccs of
      Just x => makeForeign n x
      Nothing => throw (InternalError $ "No node or javascript definition found for " ++ show n ++ " in " ++ show ccs)

jsPrim : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Name -> List String -> Core String
jsPrim (NS _ (UN "prim__newIORef")) [_,v,_] = pure $ "({value: "++ v ++"})"
jsPrim (NS _ (UN "prim__readIORef")) [_,r,_] = pure $ "(" ++ r ++ ".value)"
jsPrim (NS _ (UN "prim__writeIORef")) [_,r,v,_] = pure $ "(" ++ r ++ ".value=" ++ v ++ ")"
jsPrim (NS _ (UN "prim__newArray")) [_,s,v,_] = pure $ "(Array(Number(" ++ s ++ ")).fill(" ++ v ++ "))"
jsPrim (NS _ (UN "prim__arrayGet")) [_,x,p,_] = pure $ "(" ++ x ++ "[" ++ p ++ "])"
jsPrim (NS _ (UN "prim__arraySet")) [_,x,p,v,_] = pure $ "(" ++ x ++ "[" ++ p ++ "] = " ++ v ++ ")"
jsPrim (NS _ (UN "prim__os")) [] =
  do
    os <- addRequireToPreamble "os"
    let oscalc = "(o => o === 'linux'?'unix':o==='win32'?'windows':o)"
    sysos <- addConstToPreamble "sysos" (oscalc ++ "(" ++ os ++ ".platform())")
    pure sysos
jsPrim (NS _ (UN "prim__unpack")) [str] = pure $ str ++ ".split('').reduceRight((acc, x) => ({h: 1, a1: x, a2: acc}), {h: 0})"
jsPrim x args = throw $ InternalError $ "prim not implemented: " ++ (show x)

tag2es : Either Int String -> String
tag2es (Left x) = show x
tag2es (Right x) = jsString x

mutual
  impExp2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> ImperativeExp -> Core String
  impExp2es (IEVar n) =
    pure $ jsName n
  impExp2es (IELambda args body) =
    pure $ "(" ++ showSep ", " (map jsName args) ++ ") => {" ++ !(imperative2es 0 body) ++ "}"
  impExp2es (IEApp f args) =
    pure $ !(impExp2es f) ++ "(" ++ showSep ", " !(traverse impExp2es args) ++ ")"
  impExp2es (IEConstant c) =
    jsConstant c
  impExp2es (IEPrimFn f args) =
    jsOp f !(traverseVect impExp2es args)
  impExp2es (IEPrimFnExt n args) =
    jsPrim n !(traverse impExp2es args)
  impExp2es (IEConstructorHead e) =
    pure $ !(impExp2es e) ++ ".h"
  impExp2es (IEConstructorTag x) =
    pure $ tag2es x
  impExp2es (IEConstructorArg i e) =
    pure $ !(impExp2es e) ++ ".a" ++ show i
  impExp2es (IEConstructor h args) =
    let argPairs = zipWith (\i,a => "a" ++ show i ++ ": " ++ a ) [1..length args] !(traverse impExp2es args)
    in pure $ "({" ++ showSep ", " (("h:" ++ tag2es h)::argPairs) ++ "})"
  impExp2es (IEDelay e) =
    pure $ "(()=>" ++ !(impExp2es e) ++ ")"
  impExp2es (IEForce e) =
    pure $ !(impExp2es e) ++ "()"
  impExp2es IENull =
    pure "undefined"

  imperative2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> ImperativeStatement -> Core String
  imperative2es indent DoNothing =
    pure ""
  imperative2es indent (SeqStatement x y) =
    pure $ !(imperative2es indent x) ++ "\n" ++ !(imperative2es indent y)
  imperative2es indent (FunDecl fc n args body) =
    pure $ nSpaces indent ++ "function " ++ jsName n ++ "(" ++ showSep ", " (map jsName args) ++ "){//"++ show fc ++"\n" ++
           !(imperative2es (indent+1) body) ++ "\n" ++ nSpaces indent ++ "}\n"
  imperative2es indent (ForeignDecl fc n path args ret) =
    pure $ !(foreignDecl n path) ++ "\n"
  imperative2es indent (ReturnStatement x) =
    pure $ nSpaces indent ++ "return " ++ !(impExp2es x) ++ ";"
  imperative2es indent (SwitchStatement e alts def) =
    do
      def <- case def of
                Nothing => pure ""
                Just x => pure $ nSpaces (indent+1) ++ "default:\n" ++ !(imperative2es (indent+2) x)
      let sw = nSpaces indent ++ "switch(" ++ !(impExp2es e) ++ "){\n"
      let alts = concat !(traverse (alt2es (indent+1)) alts)
      pure $ sw ++ alts ++ def ++ "\n" ++ nSpaces indent ++ "}"
  imperative2es indent (LetDecl x v) =
    case v of
      Nothing => pure $ nSpaces indent ++ "let " ++ jsName x ++ ";"
      Just v_ => pure $ nSpaces indent ++ "let " ++ jsName x ++ " = " ++ !(impExp2es v_) ++ ";"
  imperative2es indent (ConstDecl x v) =
    pure $ nSpaces indent ++ "const " ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";"
  imperative2es indent (MutateStatement x v) =
    pure $ nSpaces indent ++ jsName x ++ " = " ++ !(impExp2es v) ++ ";"
  imperative2es indent (ErrorStatement msg) =
    pure $ nSpaces indent ++ "throw new Error("++ jsString msg ++");"
  imperative2es indent (EvalExpStatement e) =
    pure $ nSpaces indent ++ !(impExp2es e) ++ ";"
  imperative2es indent (CommentStatement x) =
    pure $ "\n/*" ++ x ++ "*/\n"
  imperative2es indent (ForEverLoop x) =
    pure $ nSpaces indent ++ "while(true){\n" ++ !(imperative2es (indent+1) x) ++ "\n" ++ nSpaces indent ++ "}"

  alt2es : {auto d : Ref Ctxt Defs} -> {auto c : Ref ESs ESSt} -> Nat -> (ImperativeExp, ImperativeStatement) -> Core String
  alt2es indent (e, b) = pure $ nSpaces indent ++ "case " ++ !(impExp2es e) ++ ": {\n" ++
                                !(imperative2es (indent+1) b) ++ "\n" ++ nSpaces (indent+1) ++ "break; }\n"

static_preamble : List String
static_preamble =
  [ "class IdrisError extends Error { }"
  , "function __prim_idris2js_FArgList(x){if(x.h === 0){return []}else{return x.a2.concat(__prim_idris2js_FArgList(x.a3))}}"
  , "function __prim_js2idris_array(x){if(x.length ===0){return {h:0}}else{return {h:1,a1:x[0],a2: __prim_js2idris_array(x.slice(1))}}}"
  , "function __prim_idris2js_array(x){const result = Array();while (x.h != 0) {result.push(x.a1); x = x.a2;}return result;}"
  ]

export
compileToES : Ref Ctxt Defs -> ClosedTerm -> List String -> Core String
compileToES c tm ccTypes =
  do
    (impDefs, impMain) <- compileToImperative c tm
    s <- newRef ESs (MkESSt empty ccTypes)
    defs <- imperative2es 0 impDefs
    main_ <- imperative2es 0 impMain
    let main = "try{" ++ main_ ++ "}catch(e){if(e instanceof IdrisError){console.log('ERROR: ' + e.message)}else{throw e} }"
    st <- get ESs
    let pre = showSep "\n" $ static_preamble ++ (SortedMap.values $ preamble st)
    pure $ pre ++ "\n\n" ++ defs ++ main

ext: idr


text:
module Str2Float

export
str2float : String -> Double
str2float = cast

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module IntEqOrd

public export
Eq Int8 where
  x == y = intToBool (prim__eq_Int8 x y)

public export
Eq Int16 where
  x == y = intToBool (prim__eq_Int16 x y)

public export
Eq Int32 where
  x == y = intToBool (prim__eq_Int32 x y)

public export
Eq Int64 where
  x == y = intToBool (prim__eq_Int64 x y)

public export
Ord Int8 where
  compare x y = if x < y then LT else if x == y then EQ else GT

  (<) x y = intToBool (prim__lt_Int8 x y)
  (<=) x y = intToBool (prim__lte_Int8 x y)
  (>) x y = intToBool (prim__gt_Int8 x y)
  (>=) x y = intToBool (prim__gte_Int8 x y)

public export
Ord Int16 where
  compare x y = if x < y then LT else if x == y then EQ else GT

  (<) x y = intToBool (prim__lt_Int16 x y)
  (<=) x y = intToBool (prim__lte_Int16 x y)
  (>) x y = intToBool (prim__gt_Int16 x y)
  (>=) x y = intToBool (prim__gte_Int16 x y)

public export
Ord Int32 where
  compare x y = if x < y then LT else if x == y then EQ else GT

  (<) x y = intToBool (prim__lt_Int32 x y)
  (<=) x y = intToBool (prim__lte_Int32 x y)
  (>) x y = intToBool (prim__gt_Int32 x y)
  (>=) x y = intToBool (prim__gte_Int32 x y)

public export
Ord Int64 where
  compare x y = if x < y then LT else if x == y then EQ else GT

  (<) x y = intToBool (prim__lt_Int64 x y)
  (<=) x y = intToBool (prim__lte_Int64 x y)
  (>) x y = intToBool (prim__gt_Int64 x y)
  (>=) x y = intToBool (prim__gte_Int64 x y)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Core.Normalise.Convert

import public Core.Normalise.Eval
import public Core.Normalise.Quote

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Options
import Core.Primitives
import Core.TT
import Core.Value

import Libraries.Data.IntMap
import Data.List
import Data.Maybe
import Data.Nat
import Data.Vect

%default covering

public export
interface Convert tm where
  convert : {auto c : Ref Ctxt Defs} ->
            {vars : List Name} ->
            Defs -> Env Term vars ->
            tm vars -> tm vars -> Core Bool
  convertInf : {auto c : Ref Ctxt Defs} ->
               {vars : List Name} ->
               Defs -> Env Term vars ->
               tm vars -> tm vars -> Core Bool

  convGen : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Ref QVar Int ->
            Bool -> -- skip forced arguments (must have checked the type
                    -- elsewhere first)
            Defs -> Env Term vars ->
            tm vars -> tm vars -> Core Bool

  convert defs env tm tm'
      = do q <- newRef QVar 0
           convGen q False defs env tm tm'

  convertInf defs env tm tm'
      = do q <- newRef QVar 0
           convGen q True defs env tm tm'

tryUpdate : {vars, vars' : _} ->
            List (Var vars, Var vars') ->
            Term vars -> Maybe (Term vars')
tryUpdate ms (Local fc l idx p)
    = do MkVar p' <- findIdx ms idx
         pure $ Local fc l _ p'
  where
    findIdx : List (Var vars, Var vars') -> Nat -> Maybe (Var vars')
    findIdx [] _ = Nothing
    findIdx ((MkVar {i} _, v) :: ps) n
        = if i == n then Just v else findIdx ps n
tryUpdate ms (Ref fc nt n) = pure $ Ref fc nt n
tryUpdate ms (Meta fc n i args) = pure $ Meta fc n i !(traverse (tryUpdate ms) args)
tryUpdate ms (Bind fc x b sc)
    = do b' <- tryUpdateB b
         pure $ Bind fc x b' !(tryUpdate (map weakenP ms) sc)
  where
    tryUpdatePi : PiInfo (Term vars) -> Maybe (PiInfo (Term vars'))
    tryUpdatePi Explicit = pure Explicit
    tryUpdatePi Implicit = pure Implicit
    tryUpdatePi AutoImplicit = pure AutoImplicit
    tryUpdatePi (DefImplicit t) = pure $ DefImplicit !(tryUpdate ms t)

    tryUpdateB : Binder (Term vars) -> Maybe (Binder (Term vars'))
    tryUpdateB (Lam fc r p t) = pure $ Lam fc r !(tryUpdatePi p) !(tryUpdate ms t)
    tryUpdateB (Let fc r v t) = pure $ Let fc r !(tryUpdate ms v) !(tryUpdate ms t)
    tryUpdateB (Pi fc r p t) = pure $ Pi fc r !(tryUpdatePi p) !(tryUpdate ms t)
    tryUpdateB _ = Nothing

    weakenP : {n : _} -> (Var vars, Var vars') ->
              (Var (n :: vars), Var (n :: vars'))
    weakenP (v, vs) = (weaken v, weaken vs)
tryUpdate ms (App fc f a) = pure $ App fc !(tryUpdate ms f) !(tryUpdate ms a)
tryUpdate ms (As fc s a p) = pure $ As fc s !(tryUpdate ms a) !(tryUpdate ms p)
tryUpdate ms (TDelayed fc r tm) = pure $ TDelayed fc r !(tryUpdate ms tm)
tryUpdate ms (TDelay fc r ty tm) = pure $ TDelay fc r !(tryUpdate ms ty) !(tryUpdate ms tm)
tryUpdate ms (TForce fc r tm) = pure $ TForce fc r !(tryUpdate ms tm)
tryUpdate ms (PrimVal fc c) = pure $ PrimVal fc c
tryUpdate ms (Erased fc i) = pure $ Erased fc i
tryUpdate ms (TType fc) = pure $ TType fc

mutual
  allConvNF : {auto c : Ref Ctxt Defs} ->
              {vars : _} ->
              Ref QVar Int -> Bool -> Defs -> Env Term vars ->
              List (NF vars) -> List (NF vars) -> Core Bool
  allConvNF q i defs env [] [] = pure True
  allConvNF q i defs env (x :: xs) (y :: ys)
      = do ok <- allConvNF q i defs env xs ys
           if ok then convGen q i defs env x y
                 else pure False
  allConvNF q i defs env _ _ = pure False

  -- return False if anything differs at the head, to quickly find
  -- conversion failures without going deeply into all the arguments.
  -- True means they might still match
  quickConv : List (NF vars) -> List (NF vars) -> Bool
  quickConv [] [] = True
  quickConv (x :: xs) (y :: ys) = quickConvArg x y && quickConv xs ys
    where
      quickConvHead : NHead vars -> NHead vars -> Bool
      quickConvHead (NLocal _ _ _) (NLocal _ _ _) = True
      quickConvHead (NRef _ n) (NRef _ n') = n == n'
      quickConvHead (NMeta n _ _) (NMeta n' _ _) = n == n'
      quickConvHead _ _ = False

      quickConvArg : NF vars -> NF vars -> Bool
      quickConvArg (NBind{}) _ = True -- let's not worry about eta here...
      quickConvArg _ (NBind{}) = True
      quickConvArg (NApp _ h _) (NApp _ h' _) = quickConvHead h h'
      quickConvArg (NDCon _ _ t _ _) (NDCon _ _ t' _ _) = t == t'
      quickConvArg (NTCon _ n _ _ _) (NTCon _ n' _ _ _) = n == n'
      quickConvArg (NAs _ _ _ t) (NAs _ _ _ t') = quickConvArg t t'
      quickConvArg (NDelayed _ _ t) (NDelayed _ _ t') = quickConvArg t t'
      quickConvArg (NDelay _ _ _ _) (NDelay _ _ _ _) = True
      quickConvArg (NForce _ _ t _) (NForce _ _ t' _) = quickConvArg t t'
      quickConvArg (NPrimVal _ c) (NPrimVal _ c') = c == c'
      quickConvArg (NType _) (NType _) = True
      quickConvArg (NErased _ _) _ = True
      quickConvArg _ (NErased _ _) = True
      quickConvArg _ _ = False
  quickConv _ _ = False

  allConv : {auto c : Ref Ctxt Defs} ->
            {vars : _} ->
            Ref QVar Int -> Bool -> Defs -> Env Term vars ->
            List (Closure vars) -> List (Closure vars) -> Core Bool
  allConv q i defs env xs ys
      = do xsnf <- traverse (evalClosure defs) xs
           ysnf <- traverse (evalClosure defs) ys
           if quickConv xsnf ysnf
              then allConvNF q i defs env xsnf ysnf
              else pure False

  -- If the case trees match in structure, get the list of variables which
  -- have to match in the call
  getMatchingVarAlt : {auto c : Ref Ctxt Defs} ->
                      {args, args' : _} ->
                      Defs ->
                      List (Var args, Var args') ->
                      CaseAlt args -> CaseAlt args' ->
                      Core (Maybe (List (Var args, Var args')))
  getMatchingVarAlt defs ms (ConCase n tag cargs t) (ConCase n' tag' cargs' t')
      = if n == n'
           then do let Just ms' = extend cargs cargs' ms
                        | Nothing => pure Nothing
                   Just ms <- getMatchingVars defs ms' t t'
                        | Nothing => pure Nothing
                   -- drop the prefix from cargs/cargs' since they won't
                   -- be in the caller
                   pure (Just (mapMaybe (dropP cargs cargs') ms))
           else pure Nothing
    where
      weakenP : {c, c', args, args' : _} ->
                (Var args, Var args') ->
                (Var (c :: args), Var (c' :: args'))
      weakenP (v, vs) = (weaken v, weaken vs)

      extend : (cs : List Name) -> (cs' : List Name) ->
               (List (Var args, Var args')) ->
               Maybe (List (Var (cs ++ args), Var (cs' ++ args')))
      extend [] [] ms = pure ms
      extend (c :: cs) (c' :: cs') ms
          = do rest <- extend cs cs' ms
               pure ((MkVar First, MkVar First) :: map weakenP rest)
      extend _ _ _ = Nothing

      dropV : forall args .
              (cs : List Name) -> Var (cs ++ args) -> Maybe (Var args)
      dropV [] v = Just v
      dropV (c :: cs) (MkVar First) = Nothing
      dropV (c :: cs) (MkVar (Later x))
          = dropV cs (MkVar x)

      dropP : (cs : List Name) -> (cs' : List Name) ->
              (Var (cs ++ args), Var (cs' ++ args')) ->
              Maybe (Var args, Var args')
      dropP cs cs' (x, y) = pure (!(dropV cs x), !(dropV cs' y))

  getMatchingVarAlt defs ms (ConstCase c t) (ConstCase c' t')
      = if c == c'
           then getMatchingVars defs ms t t'
           else pure Nothing
  getMatchingVarAlt defs ms (DefaultCase t) (DefaultCase t')
      = getMatchingVars defs ms t t'
  getMatchingVarAlt defs _ _ _ = pure Nothing

  getMatchingVarAlts : {auto c : Ref Ctxt Defs} ->
                       {args, args' : _} ->
                       Defs ->
                       List (Var args, Var args') ->
                       List (CaseAlt args) -> List (CaseAlt args') ->
                       Core (Maybe (List (Var args, Var args')))
  getMatchingVarAlts defs ms [] [] = pure (Just ms)
  getMatchingVarAlts defs ms (a :: as) (a' :: as')
      = do Just ms <- getMatchingVarAlt defs ms a a'
                | Nothing => pure Nothing
           getMatchingVarAlts defs ms as as'
  getMatchingVarAlts defs _ _ _ = pure Nothing

  getMatchingVars : {auto c : Ref Ctxt Defs} ->
                    {args, args' : _} ->
                    Defs ->
                    List (Var args, Var args') ->
                    CaseTree args -> CaseTree args' ->
                    Core (Maybe (List (Var args, Var args')))
  getMatchingVars defs ms (Case _ p _ alts) (Case _ p' _ alts')
      = getMatchingVarAlts defs ((MkVar p, MkVar p') :: ms) alts alts'
  getMatchingVars defs ms (STerm i tm) (STerm i' tm')
      = do let Just tm'' = tryUpdate ms tm
               | Nothing => pure Nothing
           if !(convert defs (mkEnv (getLoc tm) args') tm'' tm')
              then pure (Just ms)
              else pure Nothing
  getMatchingVars defs ms (Unmatched _) (Unmatched _) = pure (Just ms)
  getMatchingVars defs ms Impossible Impossible = pure (Just ms)
  getMatchingVars _ _ _ _ = pure Nothing

  chkSameDefs : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                Name -> Name ->
                List (Closure vars) -> List (Closure vars) -> Core Bool
  chkSameDefs q i defs env n n' nargs nargs'
     = do Just (PMDef _ args ct rt _) <- lookupDefExact n (gamma defs)
               | _ => pure False
          Just (PMDef _ args' ct' rt' _) <- lookupDefExact n' (gamma defs)
               | _ => pure False

          -- If the two case blocks match in structure, get which variables
          -- correspond. If corresponding variables convert, the two case
          -- blocks convert.
          Just ms <- getMatchingVars defs [] ct ct'
               | Nothing => pure False
          convertMatches ms
     where
       -- We've only got the index into the argument list, and the indices
       -- don't match up, which is annoying. But it'll always be there!
       getArgPos : Nat -> List (Closure vars) -> Maybe (Closure vars)
       getArgPos _ [] = Nothing
       getArgPos Z (c :: cs) = pure c
       getArgPos (S k) (c :: cs) = getArgPos k cs

       convertMatches : {vs, vs' : _} ->
                        List (Var vs, Var vs') ->
                        Core Bool
       convertMatches [] = pure True
       convertMatches ((MkVar {i=ix} p, MkVar {i=iy} p') :: vs)
          = do let Just varg = getArgPos ix nargs
                   | Nothing => pure False
               let Just varg' = getArgPos iy nargs'
                   | Nothing => pure False
               pure $ !(convGen q i defs env varg varg') &&
                      !(convertMatches vs)

  -- If two names are standing for case blocks, check the blocks originate
  -- from the same place, and have the same scrutinee
  chkConvCaseBlock : {auto c : Ref Ctxt Defs} ->
                     {vars : _} ->
                     FC -> Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                     NHead vars -> List (Closure vars) ->
                     NHead vars -> List (Closure vars) -> Core Bool
  chkConvCaseBlock fc q i defs env (NRef _ n) nargs (NRef _ n') nargs'
      = do NS _ (CaseBlock _ _) <- full (gamma defs) n
              | _ => pure False
           NS _ (CaseBlock _ _) <- full (gamma defs) n'
              | _ => pure False
           False <- chkSameDefs q i defs env n n' nargs nargs'
              | True => pure True
           -- both case operators. Due to the way they're elaborated, two
           -- blocks might arise from the same source but have different
           -- names. So we consider them the same if the scrutinees convert,
           -- and the functions are defined at the same location. This is a
           -- bit of a hack - and relies on the location being stored in the
           -- term accurately - but otherwise it's a quick way to find out!
           Just def <- lookupCtxtExact n (gamma defs)
                | _ => pure False
           Just def' <- lookupCtxtExact n' (gamma defs)
                | _ => pure False
           let PMDef _ _ tree _ _ = definition def
                | _ => pure False
           let PMDef _ _ tree' _ _ = definition def'
                | _ => pure False
           let Just scpos = findArgPos tree
                | Nothing => pure False
           let Just scpos' = findArgPos tree'
                | Nothing => pure False
           let Just sc = getScrutinee scpos nargs
                | Nothing => pure False
           let Just sc' = getScrutinee scpos' nargs'
                | Nothing => pure False
           ignore $ convGen q i defs env sc sc'
           pure (location def == location def')
    where
      -- Need to find the position of the scrutinee to see if they are the
      -- same
      findArgPos : CaseTree as -> Maybe Nat
      findArgPos (Case idx p _ _) = Just idx
      findArgPos _ = Nothing

      getScrutinee : Nat -> List (Closure vs) -> Maybe (Closure vs)
      getScrutinee Z (x :: xs) = Just x
      getScrutinee (S k) (x :: xs) = getScrutinee k xs
      getScrutinee _ _ = Nothing
  chkConvCaseBlock _ _ _ _ _ _ _ _ _ = pure False

  chkConvHead : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                NHead vars -> NHead vars -> Core Bool
  chkConvHead q i defs env (NLocal _ idx _) (NLocal _ idx' _) = pure $ idx == idx'
  chkConvHead q i defs env (NRef _ n) (NRef _ n') = pure $ n == n'
  chkConvHead q inf defs env (NMeta n i args) (NMeta n' i' args')
     = if i == i'
          then allConv q inf defs env args args'
          else pure False
  chkConvHead q i defs env _ _ = pure False

  convBinders : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                Ref QVar Int -> Bool -> Defs -> Env Term vars ->
                Binder (Closure vars) -> Binder (Closure vars) -> Core Bool
  convBinders q i defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
      = if cx /= cy
           then pure False
           else convGen q i defs env tx ty
  convBinders q i defs env (Lam _ cx ix tx) (Lam _ cy iy ty)
      = if cx /= cy
           then pure False
           else convGen q i defs env tx ty
  convBinders q i defs env bx by
      = if multiplicity bx /= multiplicity by
           then pure False
           else convGen q i defs env (binderType bx) (binderType by)

  export
  Convert NF where
    convGen q i defs env (NBind fc x b sc) (NBind _ x' b' sc')
        = do var <- genName "conv"
             let c = MkClosure defaultOpts [] env (Ref fc Bound var)
             bok <- convBinders q i defs env b b'
             if bok
                then do bsc <- sc defs c
                        bsc' <- sc' defs c
                        convGen q i defs env bsc bsc'
                else pure False

    convGen q i defs env tmx@(NBind fc x (Lam fc' c ix tx) scx) tmy
        = do empty <- clearDefs defs
             etay <- nf defs env
                        (Bind fc x (Lam fc' c !(traverse (quote empty env) ix) !(quote empty env tx))
                           (App fc (weaken !(quote empty env tmy))
                                (Local fc Nothing _ First)))
             convGen q i defs env tmx etay
    convGen q i defs env tmx tmy@(NBind fc y (Lam fc' c iy ty) scy)
        = do empty <- clearDefs defs
             etax <- nf defs env
                        (Bind fc y (Lam fc' c !(traverse (quote empty env) iy) !(quote empty env ty))
                           (App fc (weaken !(quote empty env tmx))
                                (Local fc Nothing _ First)))
             convGen q i defs env etax tmy

    convGen q inf defs env (NApp fc val args) (NApp _ val' args')
        = if !(chkConvHead q inf defs env val val')
             then do i <- getInfPos val
                     allConv q inf defs env (dropInf 0 i args1) (dropInf 0 i args2)
             else chkConvCaseBlock fc q inf defs env val args1 val' args2
        where
          getInfPos : NHead vars -> Core (List Nat)
          getInfPos (NRef _ n)
              = if inf
                   then do Just gdef <- lookupCtxtExact n (gamma defs)
                                | _ => pure []
                           pure (inferrable gdef)
                   else pure []
          getInfPos _ = pure []

          dropInf : Nat -> List Nat -> List a -> List a
          dropInf _ [] xs = xs
          dropInf _ _ [] = []
          dropInf i ds (x :: xs)
              = if i `elem` ds
                   then dropInf (S i) ds xs
                   else x :: dropInf (S i) ds xs

          -- Discard file context information irrelevant for conversion checking
          args1 : List (Closure vars)
          args1 = map snd args

          args2 : List (Closure vars)
          args2 = map snd args'

    convGen q i defs env (NDCon _ nm tag _ args) (NDCon _ nm' tag' _ args')
        = if tag == tag'
             then allConv q i defs env (map snd args) (map snd args')
             else pure False
    convGen q i defs env (NTCon _ nm tag _ args) (NTCon _ nm' tag' _ args')
        = if nm == nm'
             then allConv q i defs env (map snd args) (map snd args')
             else pure False
    convGen q i defs env (NAs _ _ _ tm) (NAs _ _ _ tm')
        = convGen q i defs env tm tm'

    convGen q i defs env (NDelayed _ r arg) (NDelayed _ r' arg')
        = if compatible r r'
             then convGen q i defs env arg arg'
             else pure False
    convGen q i defs env (NDelay _ r _ arg) (NDelay _ r' _ arg')
        = if compatible r r'
             then do -- if it's codata, don't reduce the argument or we might
                     -- go for ever, if it's infinite
                     adefs <- case r of
                                   LLazy => pure defs
                                   _ => clearDefs defs
                     convGen q i adefs env arg arg'
             else pure False
    convGen q i defs env (NForce _ r arg args) (NForce _ r' arg' args')
        = if compatible r r'
             then if !(convGen q i defs env arg arg')
                     then allConv q i defs env (map snd args) (map snd args')
                     else pure False
             else pure False

    convGen q i defs env (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
    convGen q i defs env (NErased _ _) _ = pure True
    convGen q i defs env _ (NErased _ _) = pure True
    convGen q i defs env (NType _) (NType _) = pure True
    convGen q i defs env x y = pure False

  export
  Convert Term where
    convGen q i defs env x y
        = convGen q i defs env !(nf defs env x) !(nf defs env y)

  export
  Convert Closure where
    convGen q i defs env x y
        = convGen q i defs env !(evalClosure defs x) !(evalClosure defs y)


text:
module Prelude.Basics

import Builtin

import Prelude.Ops

%default total

public export
Not : Type -> Type
Not x = x -> Void

-----------------------
-- UTILITY FUNCTIONS --
-----------------------

||| Manually assign a type to an expression.
||| @ a the type to assign
||| @ x the element to get the type
public export %inline
the : (0 a : Type) -> (x : a) -> a
the _ x = x

||| Identity function.
public export %inline
id : (x : a) -> a
id x = x

||| Function that duplicates its input
public export
dup : a -> (a, a)
dup x = (x, x)

||| Constant function.  Ignores its second argument.
public export %inline
const : a -> b -> a
const x = \value => x

||| Function composition.
public export %inline
(.) : (b -> c) -> (a -> b) -> a -> c
(.) f g = \x => f (g x)

||| Composition of a two-argument function with a single-argument one.
||| `(.:)` is like `(.)` but the second argument and the result are two-argument functions.
||| This operator is also known as "blackbird operator".
public export %inline
(.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
(.:) = (.) . (.)

||| `on b u x y` runs the binary function b on the results of applying
||| unary function u to two arguments x and y. From the opposite perspective,
||| it transforms two inputs and combines the outputs.
|||
||| ```idris example
||| ((+) `on` f) x y = f x + f y
||| ```
|||
||| Typical usage:
|||
||| ```idris example
||| sortBy (compare `on` fst).
||| ```
public export
on : (b -> b -> c) -> (a -> b) -> a -> a -> c
on f g = \x, y => g x `f` g y

infixl 0 `on`

||| Takes in the first two arguments in reverse order.
||| @ f the function to flip
public export
flip : (f : a -> b -> c) -> b -> a -> c
flip f x y = f y x

||| Function application.
public export
apply : (a -> b) -> a -> b
apply f a = f a

public export
curry : ((a, b) -> c) -> a -> b -> c
curry f a b = f (a, b)

public export
uncurry : (a -> b -> c) -> (a, b) -> c
uncurry f (a, b) = f a b

-- $ is compiled specially to shortcut any tricky unification issues, but if
-- it did have a type this is what it would be, and it might be useful to
-- use directly sometimes (e.g. in higher order functions)
public export
($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
($) f a = f a

-------------------
-- PROOF HELPERS --
-------------------

||| Equality is a congruence.
public export
cong : (0 f : t -> u) -> (p : a = b) -> f a = f b
cong f Refl = Refl

||| Two-holed congruence.
export
-- These are natural in equational reasoning.
cong2 : (0 f : t1 -> t2 -> u) -> (p1 : a = b) -> (p2 : c = d) -> f a c = f b d
cong2 f Refl Refl = Refl

||| Irrelevant equalities can always be made relevant
export
irrelevantEq : (0 _ : a === b) -> a === b
irrelevantEq Refl = Refl

--------------
-- BOOLEANS --
--------------

||| Boolean Data Type.
public export
data Bool = False | True

||| Boolean NOT.
%inline
public export
not : (b : Bool) -> Bool
not True = False
not False = True

||| Boolean AND only evaluates the second argument if the first is `True`.
%inline
public export
(&&) : (b : Bool) -> Lazy Bool -> Bool
(&&) True x = x
(&&) False x = False

||| Boolean OR only evaluates the second argument if the first is `False`.
%inline
public export
(||) : (b : Bool) -> Lazy Bool -> Bool
(||) True x = True
(||) False x = x

||| Non-dependent if-then-else
%inline
public export
ifThenElse : (b : Bool) -> Lazy a -> Lazy a -> a
ifThenElse True l r = l
ifThenElse False l r = r

%inline
public export
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True

--------------
-- LISTS    --
--------------

||| Generic lists.
public export
data List a =
  ||| Empty list
  Nil

  | ||| A non-empty list, consisting of a head element and the rest of the list.
  (::) a (List a)

%name List xs, ys, zs

||| Snoc lists.
public export
data SnocList a =
  ||| Empty snoc-list
  Lin

  | ||| A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
  (:<) (SnocList a) a

%name SnocList sx, sy, sz


text:
> module Double.Predicates

> import Data.So

> %default total
> %access public export
> %auto_implicits on

* EQ

> |||
> data EQ : Double -> Double -> Type where
>   MkEQ : {x : Double} -> {y : Double} -> So (x == y) -> EQ x y

* LT

> |||
> data LT : Double -> Double -> Type where
>   MkLT : {x : Double} -> {y : Double} -> So (x < y) -> LT x y

* LTE

> |||
> data LTE : Double -> Double -> Type where
>   MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y

* Non-negative, positive

> -- |||
> -- data NonNegative : Double -> Type where
> --   MkNonNegative : {x : Double} -> So (0.0 <= x) -> NonNegative x

> -- |||
> -- data Positive : Double -> Type where
> --   MkPositive : {x : Double} -> So (0.0 < x) -> Positive x

> |||
> NonNegative : (x : Double) -> Type
> NonNegative x = 0.0 `LTE` x

> |||
> Positive : (x : Double) -> Type
> Positive x = 0.0 `LT` x

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module IntegerArith

import IntegerOrdering
import IntegerGroupTheory

{-
Strategy (<) type:

To handle case a (-a)
autogen a type which is either a<b or a>b and a proof of it.
match on the with of the generating function, so that you can have distinct cases of the inequality treated as creating different assumptions about the values a and b.
use this pattern matching structure in the definition of gcdBigInt itself.
Reflection shouldn't be needed, then, except maybe for gcdBigInt a 0.

We can implement this inequality type (which mirrors LTE for Nats) using recursion, even though we aren't given a fixed enumeration of Integer, because we have decEq.

	decEq 5 3 = No ( _ 5 3 ) : Dec (5 = 3)
	decEq 5 5 = Yes Refl : (5=5)

Although actually, a case expression on (decEq a b) may be enough instead of a dependent pattern match, because the case matched on itself has a proof, and one might be able to reuse that...

=======

Strategy rewrite case argument:

If the function you're trying to prove matches an equality has a case expression or equivalent in it, we can show that the function can be computed by assuming this has a particular value, and thus when we can take the case expression outside the equality and the cases being matched on include a proof of something which determines the value of the case argument, we can apply a function using this proof to obtain a proof that the case argument is the required value.

So if our case argument is (decLT (a*b) 0) then we can get a

	(decLT (a*b) 0 = Yes pr)

from the (Yes pr : DecLT (a*b) 0) that one is pattern matching on when trying to generate the equality of gcdBigInt with its definition, by a function which manually constructs the proof from (pr) if Refl won't be recognized.

Once that (decLT (a*b) 0 = Yes pr) is used to rewrite the case argument of the equality-with-definition generator from (decLT (a*b) 0) to one of the cases (Yes _) of the case expressions in the gcdBigInt definition, we should be able to use compute to collapse the case expression and obtain the desired equality.

=======

Strategy recursion:

gcdBigInt can probably be reduced to a single case expression step followed by the usual gcd on nonnegative numbers, which by not having a case expression can be proved total just like gcd can. So gcdBigInt could be proved total simply by factorization.

-}

{-
-- IntegerArith.gcdBigInt is possibly not total due to recursive path IntegerArith.gcdBigInt
-- %reflection
total
gcdBigInt : Integer -> Integer -> Integer
gcdBigInt a 0 = a
gcdBigInt a b = if a*b<0 then gcdBigInt (abs a) (abs b) else assert_total (gcdBigInt b (modBigInt a b))
-}

{-
-- IntegerArith.gcdBigInt is possibly not total due to: IntegerArith.case block in gcdBigInt

total
gcdBigInt : Integer -> Integer -> Integer
gcdBigInt a 0 = a
gcdBigInt a b = case ( decLT (a*b) 0 ) of
		Yes pr => gcdBigInt (abs a) (abs b)
		otherwise => gcdBigInt b (modBigInt a b)
-}

{-
-- IntegerArith.gcdBigInt is possibly not total due to: with block in IntegerArith.gcdBigInt

total
gcdBigInt : Integer -> Integer -> Integer
gcdBigInt a 0 = a
gcdBigInt a b with ( decLT (a*b) 0 )
	| Yes pr = gcdBigInt (abs a) (abs b)
	| otherwise = gcdBigInt b (modBigInt a b)
-}

{-
%reflection
total
gcdType : Integer -> Integer -> Type
gcdType a 0 = ( gcdBigInt a 0 = a )
gcdType a b with (decEq a (-b))
	| Yes pr =
	| No pr =
-}
{-
gcdType a b = ( gcdBigInt a b = if a*b<0 then gcdBigInt (abs a) (abs b) else assert_total (gcdBigInt b (modBigInt a b)) )
-}
{-
gcdType a b = if a*b<0 then ( gcdBigInt a b = gcdBigInt (abs a) (abs b) ) else ( gcdBigInt a b = gcdBigInt b (modBigInt a b) )
-}

{-
gcddefBigInt : (a : Integer) -> (b : Integer) -> gcdType a b
gcddefBigInt a 0 = Refl
gcddefBigInt a b = if a*b<0 then the ( gcdBigInt a b = gcdBigInt (abs a) (abs b) ) gcddefBigIntZeroPr else gcddefBigIntPr -- believe_me "by definition"
	where
		gcddefBigIntZeroPr = ?gcddefBigIntZeroPr'
		gcddefBigIntPr = ?gcddefBigIntPr'
-}

total
modBigInt_total : Integer -> Integer -> Integer
modBigInt_total a 0 = a
-- This is wrong too, in fact (div 5 (-2) = -3), so not even close.
-- I suspect we must define remainders as coset representatives or by long division.
modBigInt_total a b = a - div a b

{-
Would have said

	modBigInt_total a b = prim__sremBigInt a b

but need to be able to prove modEqBigInt.
If we can't prove this, we might as well switch to a definition of div in.
-}
modEqRem : (a : Integer) -> (b : Integer) -> (nzpr : Not (b=0)) -> (a - div a b = prim__sremBigInt a b)

{-
modeqBigInt : (a : Integer) -> (b : Integer) -> (nzpr : Not (b=0))
	-> mod a b + (div (a - mod a b) b)*b = a
-}

modeqBigInt : (a : Integer) -> (b : Integer) -> (nzpr : Not (b=0))
	-> modBigInt_total a b + (div (a - modBigInt_total a b) b)*b = a
modeqBigInt a b pr = ?modeqBigIntHole


text:
module Types

import public Builtins
import public Prelude.Basics
import public Prelude.Either
import public Prelude.Nat
import public Prelude.Bool
import public Prelude.List
import public Prelude.Functor
import public Prelude.Foldable
import public Prelude.Interfaces

%access public export

max_stars_repo_name: cwgoes/ibc-idris-ref

max_issues_repo_name: cwgoes/ibc-idris-ref

max_forks_repo_name: cwgoes/ibc-idris-ref


text:
> module NonNegDouble.BasicOperations

> import Data.So

> import Double.Predicates
> import Double.Postulates
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import Pairs.Operations

> %default total
> %access public export

> |||
> mkNonNegDouble : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
> mkNonNegDouble x {prf} = Element x prf

> |||
> cast : (x : Double) -> {auto prf : 0.0 `LTE` x} -> NonNegDouble
> cast = mkNonNegDouble

> |||
> toDouble : NonNegDouble -> Double
> toDouble = getWitness

> |||
> fromDouble : (x : Double) -> NonNegative x -> NonNegDouble
> fromDouble x prf = Element x prf

> {-

> ---}


text:
module Commons.Config.JSON.Model

import Data.PList

%default total
%access public export

data JTy = DOC | ARRAY | MAP | VALUE

data JPred : JTy -> Type where
  ValidMap : JPred MAP
  ValidArr : JPred ARRAY
  ValidVal : JPred VALUE

data JSONDoc : JTy -> Type where
  JStr : String -> JSONDoc VALUE
  JNum : Double  -> JSONDoc VALUE
  JBool : Bool  -> JSONDoc VALUE

  JNull : JSONDoc VALUE

  JArray : PList JTy JSONDoc JPred as prfs -> JSONDoc ARRAY
  JMap : PList JTy (\ty => (String, JSONDoc ty)) JPred as prfs -> JSONDoc MAP

  JDoc : (ty : JTy) -> JSONDoc ty -> JSONDoc DOC

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
import Data.Nat
import Data.Vect
import Language.Reflection

%language ElabReflection

fc : FC
fc = EmptyFC

quoteTest : TTImp -> TTImp -> List Decl
quoteTest f arg = `[ myFunc : ~(IApp fc f arg) ]

axes : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Vect n String
axes 1 = ["x"]
axes 2 = "y" :: axes 1
axes 3 = "z" :: axes 2
axes 4  = "w" :: axes 3
axes (S (S (S (S (S _))))) {lte} = absurd lte

mkPoint : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Decl
mkPoint n
    = let type = "Point" ++ show n ++ "D" in
      let mkMainUN = NS (MkNS ["Main"]) . UN . Basic in
      IRecord emptyFC Nothing Public
      (MkRecord emptyFC (mkMainUN type) [] (mkMainUN ("Mk" ++ type))
        (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN (Field axis)) `(Double)) (axes n)))

logDecls : TTImp -> Elab (Int -> Int)
logDecls v
    = do declare [IClaim EmptyFC MW Public []
                 (MkTy EmptyFC EmptyFC `{ Main.foo }
                               `(Int -> Int -> Int) )]

         declare `[ foo x y = x + y ]

         declare [ mkPoint 3 ]

         declare `[ multBy : Int -> Int
                    multBy x = x * ~(v) ]
         declare `[ myplus : Nat -> Nat -> Nat
                    myplus Z y = y
                    myplus (S k) y = S (myplus k y) ]
         check `( multBy )

mkMult : Int -> Int
mkMult = %runElab logDecls `(4)

point : Point3D
point = MkPoint3D 1.0 2.0 3.0


text:
module Main

import Data.String
import Data.Vect
import System.REPL

infixr 5 .+.

data Schema = SString | SInt | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

addToStore : (d : DataStore) -> SchemaType (schema d) -> DataStore
addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
  where
    addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
    addToData [] = [newitem]
    addToData (x :: xs) = x :: addToData xs

data Command : Schema -> Type where
     Add : SchemaType schema -> Command schema
     Get : Integer -> Command schema
     Quit : Command schema

parseCommand : String -> String -> Maybe (Command schema)
parseCommand "add" rest = Just (Add (?parseBySchema rest))
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                          (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) ->
           Maybe (String, DataStore)
getEntry pos store
    = let store_items = items store in
          case integerToFin pos (size store) of
               Nothing => Just ("Out of range\n", store)
               Just id => Just (?display (index id (items store)) ++ "\n", store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
    = case parse (schema store) input of
           Nothing => Just ("Invalid command\n", store)
           Just (Add item) =>
              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
           Just (Get pos) => getEntry pos store
           Just Quit => Nothing

main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput


text:
module Algebra.Semigroup

%default total

||| This interface is a witness that for a
||| type `a` the axioms of a semigroup hold: `(<+>)` is associative.
|||
||| Note: If the type is actually a monoid, use `Data.Algebra.LMonoid` instead.
public export
interface Semigroup a => LSemigroup a where
  0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z

||| This interface is a witness that for a
||| type `a` the axioms of a commutative semigroup hold:
||| `(<+>)` is commutative.
public export
interface LSemigroup a => CommutativeSemigroup a where
  0 appendCommutative : {x,y : a} -> x <+> y === y <+> x


text:
||| Test if :typeat correctly shows types inside lambdas
||| and for lambda arguments

-- Simple lambda
f1 : Nat -> Nat
f1 = (\x => x)

-- Lambda with two arguments
f2 : Nat -> Bool -> (Nat, Bool)
f2 = (\x, b => (x, b))

-- Mixing arguments to the function and to the lambda
f3 : Bool -> Nat -> Int -> (Bool, Nat, Int)
f3 b = (\n, i => (b, n, i))

-- Pattern matching
partial
f4 : Bool -> Nat
f4 = (\True => r)
  where
    -- Create a variable just to test inside the lambda
    r : Nat
    r = 0

-- Pattern matching with pattern variables
partial
f5 : Maybe Bool -> (Bool, Nat)
f5 = (\(Just x) => (x, r))
  where
    r : Nat
    r = 0


text:
module B

import Control.Monad.State

import A

public export
X : Type -> Type
X = State AFoo


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3

main : IO ()
main = do
    let width = 400
    let height = 300

    a <- mkNode "a"
    b <- mkNode "b"
    c <- mkNode "c"
    d <- mkNode "d"
    nodesArr <- mkArray [a, b, c, d]

    ab <- mkLink a b ()
    bc <- mkLink b c ()
    ac <- mkLink a c ()
    ad <- mkLink a d ()
    linksArr <- mkArray [ab, bc, ac, ad]

    fl <- mkForceLayout width height
    fl ?? linkDistanceL 120 >=>
      chargeL (-300)

    putNodes fl nodesArr
    putLinks fl linksArr

    svg <- d3 ?? select "body" >=>
             append "svg" >=>
             attr "width" (show width) >=>
             attr "height" (show height) >=>
             style "border" "1px solid blue"

    -- Style for arrows.
    svg ?? append "svg:defs" >=>
      append "svg:marker" >=>
      attr "id" "arrow" >=>
      attr "viewBox" "0 -7 16 14" >=>
      attr "refX" "50" >=>
      attr "markerWidth" "14" >=>
      attr "markerHeight" "16" >=>
      attr "orient" "auto" >=>
      attr "fill" "green" >=>
      append "svg:path" >=>
      attr "d" "M0 -7 L16 0 L0 7"

    linkLayer <- svg ?? append "svg:g"
    nodeLayer <- svg ?? append "svg:g"

    nodes <- nodeLayer ?? selectAll "text" >=>
               bind nodesArr
    nodes ?? enter >=>
      append "svg:text" >=>
      makeDraggableL fl >=>
      text' (const . getNData)

    links <- linkLayer ?? selectAll "line" >=>
               bind linksArr
    links ?? enter >=>
      append "svg:line" >=>
      style "stroke" "red" >=>
      style "stroke-width" "1px" >=>
      attr "marker-end" "url(#arrow)"

    fl `onTickL` tickHandler nodes links
    startL fl

    return ()
  where
    tickHandler :
      Sel NoData (Node String) ->
      Sel NoData (Link String ()) ->
      () -> IO ()
    tickHandler nodes links () = do
      nodes ??
        attr' "x" (\d, i => pure show <$> getX d) >=>
        attr' "y" (\d, i => pure show <$> getY d)
      links ??
        attr' "x1" (\d, i => getSource d >>= getX >>= pure . show) >=>
        attr' "y1" (\d, i => getSource d >>= getY >>= pure . show) >=>
        attr' "x2" (\d, i => getTarget d >>= getX >>= pure . show) >=>
        attr' "y2" (\d, i => getTarget d >>= getY >>= pure . show)
      return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Lens

import Control.Category

%access public export

-- Store comonad

data Store s a = MkStore (s -> a) s

interface Functor w => Comonad (w : Type -> Type) where
  extract : w a -> a
  extend : (w a -> b) -> w a -> w b

interface Comonad w => VerifiedComonad (w : Type -> Type) where
  comonadLaw1 : (wa : w a) ->
                extend extract wa = wa
  comonadLaw2 : (f : w a -> b) ->
                (wa : w a) ->
                extract (extend f wa) = f wa
  comonadLaw3 : (f : w b -> c) ->
                (g : w a -> b) ->
                (wa : w a) ->
                extend f (extend g wa) = extend (\d => f (extend g d)) wa

Functor (Store s) where
  map f (MkStore g a) = MkStore (f . g) a

Comonad (Store s) where
  extract (MkStore f a) = f a
  extend f (MkStore g a) = MkStore (\b => f (MkStore g b)) a

-- VerifiedComonad (Store s) where
--   comonadLaw1 (MkStore f a) = ?storeIdentityProof
--   comonadLaw2 f (MkStore g a) = Refl
--   comonadLaw3 f g (MkStore h a) = Refl

-- -- TODO: This is evil.
-- -- Supposedly (jonsterling) this definition used to work without the believe_me.
-- private
-- eta : (f : a -> b) -> f = (\c => f c)
-- eta g = believe_me Refl {g}

-- storeIdentityProof = proof
--   intros
--   rewrite eta f
--   trivial

pos : Store s a -> s
pos (MkStore _ s) = s

peek : s -> Store s a -> a
peek s (MkStore f _) = f s

peeks : (s -> s) -> Store s a -> a
peeks f (MkStore g s) = g (f s)

-- Lenses

data Lens a b = MkLens (a -> Store b a)

Category Lens where
  id = MkLens (MkStore id)
  (.) (MkLens f) (MkLens g) = MkLens (\a => case g a of
    MkStore ba b => case f b of
      MkStore cb c => MkStore (Prelude.Basics.(.) ba cb) c)

lens : (a -> b) -> (b -> a -> a) -> Lens a b
lens f g = MkLens (\a => MkStore (\b => g b a) (f a))

iso : (a -> b) -> (b -> a) -> Lens a b
iso f g = MkLens (\a => MkStore g (f a))

getL : Lens a b -> a -> b
getL (MkLens f) a = pos (f a)

setL : Lens a b -> b -> a -> a
setL (MkLens f) b = peek b . f

modL : Lens a b -> (b -> b) -> a -> a
modL (MkLens f) g = peeks g . f

mergeL : Lens a c -> Lens b c -> Lens (Either a b) c
mergeL (MkLens f) (MkLens g) = MkLens $ either (\a => map Left $ f a)
                                               (\b => map Right $ g b)

infixr 0 ^$
(^$) : Lens a b -> a -> b
(^$) = getL

infixr 4 ^=
(^=) : Lens a b -> b -> a -> a
(^=) = setL

infixr 4 ^%=
(^%=) : Lens a b -> (b -> b) -> a -> a
(^%=) = modL

fstLens : Lens (a,b) a
fstLens = MkLens $ \(a,b) => MkStore (\ a' => (a', b)) a

sndLens : Lens (a,b) b
sndLens = MkLens $ \(a,b) => MkStore (\ b' => (a, b')) b

-- Partial lenses

data PLens a b = MkPLens (a -> Maybe (Store b a))

Category PLens where
  id = MkPLens (Just . MkStore id)
  (.) (MkPLens f) (MkPLens g) = MkPLens (\a => do
    MkStore wba b <- g a
    MkStore wcb c <- f b
    pure (MkStore (wba . wcb) c))

plens : (a -> Either a (Store b a)) -> PLens a b
plens f = MkPLens $ either (const Nothing) Just . f

getPL : PLens a b -> a -> Maybe b
getPL (MkPLens f) a = map pos (f a)

justPL : PLens (Maybe a) a
justPL = MkPLens (\ma => do
  a <- ma
  pure (MkStore Just a))

max_stars_repo_name: idris-hackers/idris-lens

max_issues_repo_name: idris-hackers/idris-lens

max_forks_repo_name: idris-hackers/idris-lens


text:
module Idris.Codegen.ExtSTG.ADTMap

import Libraries.Data.IntMap
import Libraries.Data.StringMap
import Data.List
import Data.Strings
import Core.Context
import Core.Core
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.Core

||| Names of the data constructors must be associated with their STyCons, this information
||| is needed for the code generator when we generate STG case expressions
namespace DataConstructorsToTypeDefinitions
  ||| Datatypes annotation for Ref
  export
  data ADTs : Type where

  ||| Associates the resolved names or internal names with the TyCon.
  export
  ADTMap : Type
  ADTMap = (IntMap STyCon, StringMap STyCon)

  ||| Create the ADTs reference
  export
  mkADTs : Core (Ref ADTs ADTMap)
  mkADTs = newRef ADTs (empty, empty)

  ||| Gets the Int identifies through its Resolved name.
  export
  resolvedNameId
    :  {auto _ : Ref Ctxt Defs}
    -> String
    -> Core.Name.Name
    -> Core Int
  resolvedNameId ctx n = do
    (Resolved r) <- toResolvedNames n
      | _ => coreFail $ InternalError $ show n ++ " doesn't have resolved id when " ++ ctx
    pure r

  resolvedNameIdOpt
    :  {auto _ : Ref Ctxt Defs}
    -> Core.Name.Name
    -> Core (Either Int String)
  resolvedNameIdOpt n =
    pure $ case !(toResolvedNames n) of
            (Resolved r) => Left r
            _            => Right $ show n

  ||| Register the consturctor name for the STyCon
  export
  registerDataConToTyCon
    :  {auto _ : Ref ADTs ADTMap}
    -> {auto _ : Ref Ctxt Defs}
    -> STyCon
    -> Core.Name.Name
    -> Core ()
  registerDataConToTyCon s n = do
    r <- resolvedNameId "registering type constructor" n
    (m,i) <- get ADTs
    let k = show n
    case (lookup r m <+> lookup k i) of
      Just st
        => coreFail $ InternalError
                    $ show !(toFullNames n) ++ " is already registered for " ++ STyCon.Name st
      Nothing => do
        put ADTs (insert r s m, i)

  export
  registerInternalDataConToTyCon
    : Ref ADTs ADTMap
    => STyCon -> Core.Name.Name
    -> Core ()
  registerInternalDataConToTyCon s n = do
    (m,i) <- get ADTs
    let k = show n
    case lookup k i of
      Just st => coreFail
               $ InternalError
               $ show n ++ " is already registered for " ++ STyCon.Name st
      Nothing => do
        put ADTs (m, insert k s i)

  ||| Lookup if there is an ADT defined for the given name either for type name or data con name.
  export
  lookupTyCon
    :  {auto _ : Ref ADTs ADTMap}
    -> {auto _ : Ref Ctxt Defs}
    -> Core.Name.Name
    -> Core (Maybe STyCon)
  lookupTyCon n = do
    (resMap, internalMap) <- get ADTs
    pure $ case !(resolvedNameIdOpt n) of
      Left i  => lookup i resMap
      Right m => lookup m internalMap

||| Global definition mapping for types and data constructors.
namespace TConsAndDCons

  ||| Label for TAC reference
  data TAC : Type where

  ||| Types and data constructors
  ||| Maps Resolved identifiers to GlobalDefinitions
  record TyAndCnstrs where
    constructor MkTyAndCnstrs
    Types : IntMap GlobalDef
    Cntrs : IntMap GlobalDef

  mkTACRef : Core (Ref TAC TyAndCnstrs)
  mkTACRef = newRef TAC (MkTyAndCnstrs empty empty)

  addTypeOrCnst
    :  {auto _ : Ref TAC TyAndCnstrs}
    -> {auto _ : Ref Ctxt Defs}
    -> GlobalDef
    -> Core ()
  addTypeOrCnst g = case definition g of
    TCon _ _ _ _ _ _ _ _ => do
      r <- resolvedNameId "looking up TCon in definition" (fullname g)
      MkTyAndCnstrs t c <- get TAC
      -- TODO: Check if resolved named already in
      let t1 = insert r g t
      put TAC (MkTyAndCnstrs t1 c)
    DCon _ _ _ => do
      r <- resolvedNameId "looking up DCon in definition" (fullname g)
      MkTyAndCnstrs t c <- get TAC
      let c1 = insert r g c
      put TAC (MkTyAndCnstrs t c1)
    _ => pure ()

  ||| Learn the TCons and DCons from the Defs context.
  ||| This is a helper to define datatypes
  learnTConsAndCons
    :  {auto _ : Ref Ctxt Defs}
    -> {auto _ : Ref TAC TyAndCnstrs}
    -> Core ()
  learnTConsAndCons = do
    context <- gamma <$> get Ctxt
    traverse_
      (\n => do
        mdef <- lookupCtxtExactI n context
        case mdef of
          Nothing => pure ()
          Just (_, def) => addTypeOrCnst def)
      !(allNames context)

  createSTGDataConDesc : GlobalDef -> Core (STG.Name, DataConRep, SrcSpan)
  createSTGDataConDesc g = do
    let fullName = fullname g
    (DCon _ arity _) <- pure $ definition g
      | other => coreFail $ InternalError $ "createSTGDataCon found other than DCon: " ++ show other
    let arity' : Int = (cast arity) - cast (length (eraseArgs g))
    if arity' < 0
      then coreFail $ InternalError $ unlines
            [ "Negative arity after erased arguments:"
            , show fullName
            , "Full arity: " ++ show arity
            , "Erased arity: " ++ show arity'
            , "Erasable arguments: " ++ show (eraseArgs g)
            ]
      else pure
            ( show fullName -- -- TODO: Idris.Name -> STG.Name
            , (AlgDataCon (replicate (fromInteger (cast arity')) LiftedRep))
            , mkSrcSpan (location g)
            )

  ||| Create an STG data definition from a TCon definition
  createSTGTyConDesc : GlobalDef -> Core (STG.Name, SrcSpan)
  createSTGTyConDesc g = do
    let fullName = fullname g
    (TCon _ _ _ _ _ _ _ _) <- pure $ definition g
      | other => coreFail $ InternalError $ "createSTGTyCon found other than TCon: " ++ show other
    pure (show fullName, (mkSrcSpan (location g)))

  ||| Compiles the learned TCons and their DCons
  defineDataTypes
    :  {auto _ : UniqueMapRef}
    -> {auto _ : Ref Counter Int}
    -> {auto _ : Ref Ctxt Defs}
    -> {auto _ : DataTypeMapRef}
    -> {auto _ : Ref ADTs ADTMap}
    -> {auto _ : Ref TAC TyAndCnstrs}
    -> Core ()
  defineDataTypes = do
    MkTyAndCnstrs types constructors <- get TAC
    -- TODO: Write check if all the constructors are used.
    traverse_
      (\(r, g) =>
        case definition g of
          -- TODO: Add datatype with constructors and remove the constructors from the cnstrs list
          def@(TCon tag arity parampos detpos flags mutwith datacons detaggable) => do
            -- Create DataCons, looking up resolved IDs
            resolveds <- traverse (resolvedNameId "when defining data types") datacons
            sTyCon <- createSTyCon (show (fullname g), mkSrcSpan (location g)) -- TODO, IdrisName -> STG.Name
                        !(traverse (\rd => case lookup rd constructors of
                                      Nothing => coreFail
                                               $ InternalError
                                               $ "defineDatatypes: Data constructor is not found: "
                                                  ++ show !(toFullNames (Resolved rd))
                                      Just dg => createSTGDataConDesc dg)
                                   resolveds)
            traverse_ (registerDataConToTyCon sTyCon . Resolved) resolveds
            defineDataType (MkUnitId MAIN_UNIT) (MkModuleName MAIN_MODULE) sTyCon
            pure ()
          _ => pure ())
      (toList types)

  ||| Create STG datatypes from filtering out the TCon and DCon definitions from Defs
  export
  createDataTypes
    :  {auto _ : UniqueMapRef}
    -> {auto _ : Ref Counter Int}
    -> {auto _ : Ref Ctxt Defs}
    -> {auto _ : DataTypeMapRef}
    -> {auto _ : Ref ADTs ADTMap}
    -> Core ()
  createDataTypes = do
    tac <- mkTACRef
    learnTConsAndCons
    defineDataTypes

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module ListExt3

%default total
%access public export

||| A "full" or non-empty list
FList : Type -> Type
FList a = (xs : List a ** NonEmpty xs)

infixr 5 :::

(:::) : a -> List a -> FList a
(:::) x xs = ((x :: xs) ** IsNonEmpty)

||| Proof that the first list is an improper prefix of the second list, with the
||| third list as the remainder.
data IsPrefixOf : FList a -> FList a -> List a -> Type where
  SingletonPrefix : IsPrefixOf (x ::: []) (x ::: rem) rem
  SuccPrefix : IsPrefixOf (xs ** _) (ys ** _) rem
             -> IsPrefixOf (x ::: xs) (x ::: ys) rem

interface PartialOrder (a : Type) (r : a -> a -> Type) where
  reflexive : (x : a) -> r x x
  antisymmetrical : (x : a) -> (y : a) -> r x y -> r y x -> x = y
  transitive : (x : a) -> (y : a) -> (z : a) -> r x y -> r y z -> r x z

prefixRefl : (xs : FList a) -> IsPrefixOf xs xs []
prefixRefl ((x :: []) ** IsNonEmpty) = SingletonPrefix
prefixRefl ((x :: (y :: xs)) ** IsNonEmpty) =
  -- TODO do whatever is needed to make Idris happy rather than assert_total
  SuccPrefix $ assert_total $ prefixRefl (y ::: xs)

prefixAntisym : (xs : FList a) -> (ys : FList a) -> (zs : List a)
              -> IsPrefixOf xs ys zs -> IsPrefixOf ys xs zs
              -> (xs = ys, zs = [])
prefixAntisym (xs ** xpf) (ys ** ypf) [] SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) [] (SuccPrefix _) _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) (SuccPrefix _) _ impossible

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
module TTImp.Elab

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.UnifyState
import Core.Unify
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Elab.Term
import TTImp.TTImp
import TTImp.Unelab

import Data.List
import Data.Maybe
import Libraries.Data.IntMap
import Libraries.Data.NameMap

%default covering

findPLetRenames : {vars : _} ->
                  Term vars -> List (Name, (RigCount, Name))
findPLetRenames (Bind fc n (PLet _ c (Local _ _ idx p) ty) sc)
    = case nameAt p of
           x@(MN _ _) => (x, (c, n)) :: findPLetRenames sc
           _ => findPLetRenames sc
findPLetRenames (Bind fc n _ sc) = findPLetRenames sc
findPLetRenames tm = []

doPLetRenames : {vars : _} ->
                List (Name, (RigCount, Name)) ->
                List Name -> Term vars -> Term vars
doPLetRenames ns drops (Bind fc n b@(PLet _ _ _ _) sc)
    = if n `elem` drops
         then subst (Erased fc False) (doPLetRenames ns drops sc)
         else Bind fc n b (doPLetRenames ns drops sc)
doPLetRenames ns drops (Bind fc n b sc)
    = case lookup n ns of
           Just (c, n') =>
             Bind fc n' (setMultiplicity b (c `lub` (multiplicity b)))
                     (doPLetRenames ns (n' :: drops) (renameTop n' sc))
           Nothing => Bind fc n b (doPLetRenames ns drops sc)
doPLetRenames ns drops sc = sc

getRigNeeded : ElabMode -> RigCount
getRigNeeded InType = erased -- unrestricted usage in types
getRigNeeded (InLHS r) = if isErased r then erased
                                     else linear
getRigNeeded _ = linear

-- Make sure the types of holes have the references to solved holes normalised
-- away (since solved holes don't get written to .tti)
export
normaliseHoleTypes : {auto c : Ref Ctxt Defs} ->
                     {auto u : Ref UST UState} ->
                     Core ()
normaliseHoleTypes
    = do ust <- get UST
         let hs = keys (holes ust)
         defs <- get Ctxt
         traverse_ (normaliseH defs) hs
  where
    updateType : Defs -> Int -> GlobalDef -> Core ()
    updateType defs i def
        = do ty' <- catch (tryNormaliseSizeLimit defs 10 [] (type def))
                          (\err => normaliseHoles defs [] (type def))
             ignore $ addDef (Resolved i) (record { type = ty' } def)

    normaliseH : Defs -> Int -> Core ()
    normaliseH defs i
        = whenJust !(lookupCtxtExact (Resolved i) (gamma defs)) $ \ gdef =>
            case definition gdef of
              Hole _ _ => updateType defs i gdef
              _ => pure ()

export
addHoleToSave : {auto c : Ref Ctxt Defs} ->
                Name -> Core ()
addHoleToSave n
    = do defs <- get Ctxt
         Just ty <- lookupTyExact n (gamma defs)
              | Nothing => pure ()
         let ms = keys (getMetas ty)
         addToSave n
         traverse_ addToSave ms

export
elabTermSub : {inner, vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              Int -> ElabMode -> List ElabOpt ->
              NestedNames vars -> Env Term vars ->
              Env Term inner -> SubVars inner vars ->
              RawImp -> Maybe (Glued vars) ->
              Core (Term vars, Glued vars)
elabTermSub {vars} defining mode opts nest env env' sub tm ty
    = do let incase = elem InCase opts
         let inPE = elem InPartialEval opts
         let inTrans = elem InTrans opts

         -- Record the current hole state; we only check the list of current
         -- holes is completely solved so this needs to be accurate.
         oldhs <- if not incase
                     then saveHoles
                     else pure empty
         ust <- get UST
         let olddelayed = delayedElab ust
         put UST (record { delayedElab = [] } ust)
         constart <- getNextEntry

         defs <- get Ctxt
         e <- newRef EST (initEStateSub defining env' sub)
         let rigc = getRigNeeded mode

         (chktm, chkty) <- check {e} rigc (initElabInfo mode) nest env tm ty
         -- Final retry of constraints and delayed elaborations
         -- - Solve any constraints, then retry any delayed elaborations
         -- - Finally, last attempts at solving constraints, but this
         --   is most likely just to be able to display helpful errors
         let solvemode = case mode of
                              InLHS _ => inLHS
                              _ => inTerm
         solveConstraints solvemode Normal
         logTerm "elab" 5 "Looking for delayed in " chktm
         ust <- get UST
         catch (retryDelayed solvemode
                             (sortBy (\x, y => compare (fst x) (fst y))
                                       (delayedElab ust)))
                 (\err =>
                    do ust <- get UST
                       put UST (record { delayedElab = olddelayed } ust)
                       throw err)
         ust <- get UST
         put UST (record { delayedElab = olddelayed } ust)
         solveConstraintsAfter constart solvemode MatchArgs

         -- As long as we're not in the RHS of a case block,
         -- finish off constraint solving
         -- On the LHS the constraint solving is used to handle overloading
         when (not incase || isJust (isLHS mode)) $
           -- resolve any default hints
           do log "elab" 5 "Resolving default hints"
              solveConstraintsAfter constart solvemode Defaults
              -- perhaps resolving defaults helps...
              -- otherwise, this last go is most likely just to give us more
              -- helpful errors.
              solveConstraintsAfter constart solvemode LastChance

         dumpConstraints "elab" 4 False
         defs <- get Ctxt
         chktm <- if inPE -- Need to fully normalise holes in partial evaluation
                          -- because the holes don't have types saved to ttc
                     then normaliseHoles defs env chktm
                     else normaliseArgHoles defs env chktm

         -- Linearity and hole checking.
         -- on the LHS, all holes need to have been solved
         chktm <- case mode of
              InLHS _ => do when (not incase) $ checkUserHolesAfter constart True
                            pure chktm
              InTransform => do when (not incase) $ checkUserHolesAfter constart True
                                pure chktm
              -- elsewhere, all unification problems must be
              -- solved, though we defer that if it's a case block since we
              -- might learn a bit more later.
              _ => if (not incase)
                      then do checkUserHolesAfter constart (inTrans || inPE)
                              linearCheck (getFC tm) rigc False env chktm
                          -- Linearity checking looks in case blocks, so no
                          -- need to check here.
                      else pure chktm
         normaliseHoleTypes
         -- Put the current hole state back to what it was (minus anything
         -- which has been solved in the meantime)
         when (not incase) $
           do hs <- getHoles
              restoreHoles (addHoles empty hs (toList oldhs))

         -- Make a note to save all the user holes and the things they
         -- reference
         est <- get EST
         traverse_ addHoleToSave (keys (saveHoles est))

         -- On the LHS, finish by tidying up the plets (changing things that
         -- were of the form x@_, where the _ is inferred to be a variable,
         -- to just x)
         case mode of
              InLHS _ =>
                 do let vs = findPLetRenames chktm
                    let ret = doPLetRenames vs [] chktm
                    pure (ret, gnf env (doPLetRenames vs [] !(getTerm chkty)))
              _ => do dumpConstraints "elab" 2 False
                      pure (chktm, chkty)
  where
    addHoles : (acc : IntMap (FC, Name)) ->
               (allHoles : IntMap (FC, Name)) ->
               List (Int, (FC, Name)) ->
               IntMap (FC, Name)
    addHoles acc allhs [] = acc
    addHoles acc allhs ((n, x) :: hs)
        = case lookup n allhs of
               Nothing => addHoles acc allhs hs
               Just _ => addHoles (insert n x acc) allhs hs

export
elabTerm : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           Int -> ElabMode -> List ElabOpt ->
           NestedNames vars -> Env Term vars ->
           RawImp -> Maybe (Glued vars) ->
           Core (Term vars, Glued vars)
elabTerm defining mode opts nest env tm ty
    = elabTermSub defining mode opts nest env env SubRefl tm ty

export
checkTermSub : {inner, vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               Int -> ElabMode -> List ElabOpt ->
               NestedNames vars -> Env Term vars ->
               Env Term inner -> SubVars inner vars ->
               RawImp -> Glued vars ->
               Core (Term vars)
checkTermSub defining mode opts nest env env' sub tm ty
    = do defs <- case mode of
                      InType => branch -- might need to backtrack if there's
                                       -- a case in the type
                      _ => get Ctxt
         ust <- get UST
         mv <- get MD
         res <-
            catch {t = Error}
                  (elabTermSub defining mode opts nest
                               env env' sub tm (Just ty))
                  $ \case
                    TryWithImplicits loc benv ns
                      => do put Ctxt defs
                            put UST ust
                            put MD mv
                            tm' <- bindImps loc benv ns tm
                            elabTermSub defining mode opts nest
                                        env env' sub
                                        tm' (Just ty)
                    err => throw err
         case mode of
              InType => commit -- bracket the 'branch' above
              _ => pure ()

         pure (fst res)
  where
    bindImps' : {vs : _} ->
                FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->
                Core RawImp
    bindImps' loc env [] ty = pure ty
    bindImps' loc env ((n, ty) :: ntys) sc
        = pure $ IPi loc erased Implicit (Just n)
                     (Implicit loc True) !(bindImps' loc env ntys sc)

    bindImps : {vs : _} ->
               FC -> Env Term vs -> List (Name, Term vs) -> RawImp ->
               Core RawImp
    bindImps loc env ns (IBindHere fc m ty)
        = pure $ IBindHere fc m !(bindImps' loc env ns ty)
    bindImps loc env ns ty = bindImps' loc env ns ty

export
checkTerm : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            Int -> ElabMode -> List ElabOpt ->
            NestedNames vars -> Env Term vars ->
            RawImp -> Glued vars ->
            Core (Term vars)
checkTerm defining mode opts nest env tm ty
    = checkTermSub defining mode opts nest env env SubRefl tm ty


text:
module IdrisJvm.Core.ControlFlow

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.Core.Constant
import IdrisJvm.IR.Types
import Data.SortedMap

%access public export

isIntCase : SAlt -> Bool
isIntCase (SConCase _ _ _ _ _)    = True
isIntCase (SDefaultCase _)        = True
isIntCase (SConstCase (I _) _)    = True
isIntCase (SConstCase (B8 _) _)   = True
isIntCase (SConstCase (B16 _) _)  = True
isIntCase (SConstCase (Ch _) _)   = True
isIntCase (SConstCase TheWorld _) = True
isIntCase (SConstCase x _)        = isTypeConst x
isIntCase _                       = False

isIntSwitchCases : List SAlt -> Bool
isIntSwitchCases alts = all isIntSwitchCase alts where
    isIntSwitchCase : SAlt -> Bool
    isIntSwitchCase (SConstCase (I _) _)    = True
    isIntSwitchCase (SConstCase (B8 _) _)   = True
    isIntSwitchCase (SConstCase (B16 _) _)  = True
    isIntSwitchCase (SConstCase TheWorld _) = True
    isIntSwitchCase (SConstCase x _)        = isTypeConst x
    isIntSwitchCase (SDefaultCase _)        = True
    isIntSwitchCase _ = False

isCharSwitchCases : List SAlt -> Bool
isCharSwitchCases alts = all isCharSwitchCase alts where
    isCharSwitchCase : SAlt -> Bool
    isCharSwitchCase (SConstCase (Ch _) _)   = True
    isCharSwitchCase (SDefaultCase _)        = True
    isCharSwitchCase _ = False

isConstructorSwitchCases : List SAlt -> Bool
isConstructorSwitchCases alts = all isConstructorSwitchCase alts where
    isConstructorSwitchCase : SAlt -> Bool
    isConstructorSwitchCase (SConCase _ _ _ _ _)    = True
    isConstructorSwitchCase (SDefaultCase _)        = True
    isConstructorSwitchCase _ = False

mutual
  cgSwitch : (InferredType -> Asm ())
          -> ((InferredType -> Asm ()) -> SExp -> Asm ())
          -> LVar
          -> List SAlt
          -> Asm ()
  cgSwitch ret cgBody e alts
    = if all isIntCase alts
        then do
          switchIndex <- FreshSwitchIndex
          let switch = csWithLbls switchIndex alts
          let switchVar = locIndex e
          let nonDefaultCases = filter (\(_, _, alt) => not (defaultCase alt)) switch
          let labels = (\(lbl, _, _) => lbl) <$> nonDefaultCases
          let exprs = catMaybes $ (\(_, expr, _) => expr) <$> nonDefaultCases
          let switchEndLbl = switchEndLabel switchIndex
          let hasDefault = any defaultCase alts
          let switchDefaultLbl = if hasDefault then defaultLabel switchIndex else switchEndLbl
          let isConstructorSwitch = any conCase alts
          let caseToAlt = \(label, _, alt) => cgAlt ret cgBody label switchIndex switchVar alt
          sequence_ $ (CreateLabel . fst) <$> switch
          CreateLabel switchEndLbl

          if isConstructorSwitch
            then switchConstructorExpr switchVar
            else switchIntExpr e

          LookupSwitch switchDefaultLbl labels exprs
          sequence_ $ the (List (Asm ())) $ caseToAlt <$> switch
          LabelStart (switchEndLabel switchIndex)
          Frame FSame 0 [] 0 []
        else cgIf ret cgBody e nalts where
                f : SAlt -> SAlt -> Bool
                f (SDefaultCase _) (SDefaultCase _) = True
                f _ _                               = False
                nalts : List SAlt
                nalts = nubBy f alts

  cgIf : (InferredType -> Asm ())
      -> ((InferredType -> Asm ()) -> SExp -> Asm ())
      -> LVar
      -> List SAlt
      -> Asm ()
  cgIf ret cgBody e alts = do
       ifIndex <- FreshIfIndex
       let ifExpr = ifCasesWithLbls ifIndex alts
       let fallbackLabels = drop 1 ((\(lbl, _, _) => lbl) <$> ifExpr) ++ [ifEndLabel ifIndex]
       sequence_ $ CreateLabel . (\(lbl, _, _) => lbl) <$> ifExpr
       CreateLabel $ ifEndLabel ifIndex
       sequence_ $ gen ifIndex ret cgBody e <$> zip fallbackLabels ifExpr
       LabelStart (ifEndLabel ifIndex)
       Frame FSame 0 [] 0 []
     where
        gen : Nat
           -> (InferredType -> Asm ())
           -> ((InferredType -> Asm ()) -> SExp -> Asm ())
           -> LVar
           -> (String, String, Maybe (Asm ()), SAlt)
           -> Asm ()
        gen ifIndex ret cgBody e (nextLabel, label, ifExpr, expr)
          = maybe (cgElseCase ifIndex ret cgBody e nextLabel label expr)
                (\condition => cgIfElseIfCase ifIndex ret cgBody e nextLabel label condition expr)
                ifExpr

  cgIfElseIfCase : Nat
                -> (InferredType -> Asm ())
                -> ((InferredType -> Asm ()) -> SExp -> Asm ())
                -> LVar
                -> String
                -> String
                -> Asm ()
                -> SAlt
                -> Asm ()
  cgIfElseIfCase ifIndex ret cgBody e nextLabel label ifExpr (SConstCase _ expr) = do
    LabelStart label
    addFrame
    aload $ locIndex e
    ifExpr
    InvokeMethod InvokeStatic utilClass "equals" "(Ljava/lang/Object;Ljava/lang/Object;)Z" False
    Ifeq nextLabel
    cgBody ret expr
    Goto $ ifEndLabel ifIndex

  cgElseCase : Nat
            -> (InferredType -> Asm ())
            -> ((InferredType -> Asm ()) -> SExp -> Asm ())
            -> LVar
            -> String
            -> String
            -> SAlt
            -> Asm ()
  cgElseCase ifIndex ret cgBody _ _ label (SDefaultCase expr) = do
    cgCase ret cgBody label expr
    Goto $ ifEndLabel ifIndex

  cgCase : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> Label -> SExp -> Asm ()
  cgCase ret cgBody label expr = do
    LabelStart label
    addFrame
    cgBody ret expr

  cgAltNonConCase : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> Label -> Nat -> SExp -> Asm ()
  cgAltNonConCase ret cgBody label si expr = do
    cgCase ret cgBody label expr
    Goto $ switchEndLabel si

  cgConCase : (InferredType -> Asm ())
            -> ((InferredType -> Asm ()) -> SExp -> Asm ())
            -> Int
            -> Int
            -> List String
            -> SExp
            -> Asm ()
  cgConCase ret cgBody idrisObject lv args expr = do
      extractConParams lv
      cgBody ret expr
    where
      project : Nat -> Nat -> Asm ()
      project i v = do
        idrisObjectProperty idrisObject (cast i)
        storeVarWithWordSize Astore (Loc $ cast v)

      argsLength : Nat
      argsLength = length args

      extractConParams : Int -> Asm ()
      extractConParams lv = go 0 lv where
        go : Int -> Int -> Asm ()
        go i v =
            if i == cast argsLength then
                pure ()
            else do
                project (cast i) (cast v)
                go (i + 1) (v + 1)

  cgAlt : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> Label -> Nat -> Int -> SAlt -> Asm ()
  cgAlt ret cgBody label si _ (SConstCase _ expr) = cgAltNonConCase ret cgBody label si expr

  cgAlt ret cgBody label si _ (SDefaultCase expr) = cgAltNonConCase ret cgBody label si expr

  cgAlt ret cgBody label si sv (SConCase lv _ _ args expr) = do
      LabelStart label
      addFrame
      cgConCase ret cgBody sv lv args expr
      Goto $ switchEndLabel si

  conCase : SAlt -> Bool
  conCase (SConCase _ _ _ _ _) = True
  conCase _           = False

  defaultCase : SAlt -> Bool
  defaultCase (SDefaultCase _) = True
  defaultCase _                = False

  csWithLbls : Nat -> List SAlt -> List (String, Maybe Int, SAlt)
  csWithLbls si alts = sortBy compareCase $ List.zipWith label cs [0 .. (pred $ length cs)] where

    cs : List (Maybe Int, SAlt)
    cs = zip (caseExpr <$> alts) alts

    label : (Maybe Int, SAlt) -> Nat -> (String, Maybe Int, SAlt)
    label (Just expr, alt) i = (labelName si i, Just expr, alt)
    label (Nothing, alt) _   = (defaultLabel si, Nothing, alt)

    compareCase (_, Just c1, _) (_, Just c2, _) = compare c1 c2
    compareCase (_, Just _, _) (_, Nothing, _)  = LT
    compareCase (_, Nothing, _) (_, Just _, _)  = GT
    compareCase _ _                             = EQ

  ifCasesWithLbls : Nat -> List SAlt -> List (String, Maybe (Asm ()), SAlt)
  ifCasesWithLbls si alts = sortBy compareCase $ zipWith label cs [0 .. (pred $ length cs)] where

    cs : List (Maybe (Asm ()), SAlt)
    cs = zip (ifCaseExpr <$> alts) alts

    label : (Maybe (Asm ()), SAlt) -> Nat -> (String, Maybe (Asm ()), SAlt)
    label (Just expr, alt) i = (ifLabelName si i, Just expr, alt)
    label (Nothing, alt) _   = (ifDefaultLabel si, Nothing, alt)

    compareCase (_, Just _, _) (_, Nothing, _) = LT
    compareCase (_, Nothing, _) (_, Just _, _) = GT
    compareCase _ _                            = EQ

  switchEndLabel : Nat -> String
  switchEndLabel switchIndex = "$switch" ++ show switchIndex ++ "$end"

  labelName : Nat -> Nat -> String
  labelName switchIndex labelIndex
    = "$switch" ++ show switchIndex ++ "$label" ++ show labelIndex

  defaultLabel : Nat -> String
  defaultLabel switchIndex = "$switch" ++ show switchIndex ++ "$defaultLabel"

  ifEndLabel : Nat -> String
  ifEndLabel ifIndex = "$if" ++ show ifIndex ++ "$end"

  ifLabelName : Nat -> Nat -> String
  ifLabelName ifIndex labelIndex = "$if" ++ show ifIndex ++ "$label" ++ show labelIndex

  ifDefaultLabel : Nat -> String
  ifDefaultLabel ifIndex = "$if" ++ show ifIndex ++ "$defaultLabel"

  switchConstructorExpr : Int -> Asm ()
  switchConstructorExpr varIndex = do
   aload varIndex
   InvokeMethod InvokeStatic (rtClass "Runtime") "constructorIndex" "(Ljava/lang/Object;)I" False

  switchIntExpr : LVar -> Asm ()
  switchIntExpr var = do
    locTypes <- GetFunctionLocTypes
    let varTy = getLocTy locTypes var
    loadVar locTypes varTy IInt var

  caseExpr : SAlt -> Maybe Int
  caseExpr (SConstCase t _) = Just $ constCaseExpr t where
    constCaseExpr : Const -> Int
    constCaseExpr (I i) = i
    constCaseExpr (B8 i) = prim__zextB8_Int i
    constCaseExpr (B16 i) = prim__zextB16_Int i
    constCaseExpr (Ch c) = ord c
    constCaseExpr TheWorld = 0
    constCaseExpr x = if isTypeConst x then 0 else jerror $ "Constant " ++ show x ++ " cannot be compiled to 'Switch'."

  caseExpr (SConCase _ t _ _ _) = Just t
  caseExpr (SDefaultCase _) = Nothing

  ifCaseExpr : SAlt -> Maybe (Asm ())
  ifCaseExpr (SConstCase t _) = Just $ constCaseExpr t where
    constCaseExpr : Const -> Asm ()
    constCaseExpr (I x) = jerror $ "Constant int expected to be compiled to 'switch'"
    constCaseExpr (BI i) = newBigInteger i
    constCaseExpr (Fl x) = jerror $ "Constant float expected to be compiled to 'switch'"
    constCaseExpr (Ch x) = jerror $ "Constant char expected to be compiled to 'switch'"
    constCaseExpr (Str s) = Ldc $ StringConst s
    constCaseExpr (B8 x) = jerror $ "Constant b8 expected to be compiled to 'switch'"
    constCaseExpr (B16 x) = jerror $ "Constant b16 expected to be compiled to 'switch'"
    constCaseExpr (B32 x) = jerror $ "Constant b32 cannot be compiled to 'if' yet"
    constCaseExpr (B64 x) = jerror $ "Constant b64 cannot be compiled to 'if' yet"
    constCaseExpr (AType x) = jerror $ "Constant AType cannot be compiled to 'if' yet"
    constCaseExpr StrType = jerror "Constant StrType cannot be compiled to 'if' yet"
    constCaseExpr WorldType = jerror "Constant WorldType cannot be compiled to 'if' yet"
    constCaseExpr TheWorld = jerror "Constant TheWorld cannot be compiled to 'if' yet"
    constCaseExpr VoidType = jerror "Constant VoidType cannot be compiled to 'if' yet"
    constCaseExpr Forgot = jerror "Constant Forgot cannot be compiled to 'if' yet"
  ifCaseExpr _ = Nothing

cgIfElse : (InferredType -> Asm ())
        -> ((InferredType -> Asm ()) -> SExp -> Asm ())
        -> LVar
        -> (Label -> Asm ())
        -> Maybe Int
        -> SExp
        -> SExp
        -> Asm ()
cgIfElse ret cgBody e condition valueStore case1 case2 = do
    ifIndex <- FreshIfIndex
    let ifLabel = ifLabelName ifIndex 0
    let elseLabel = ifLabelName ifIndex 1
    let endLabel = ifEndLabel ifIndex
    CreateLabel ifLabel
    CreateLabel elseLabel
    CreateLabel endLabel
    condition elseLabel
    LabelStart ifLabel
    maybe (pure ()) store valueStore
    cgBody ret case1
    Goto endLabel
    LabelStart elseLabel
    addFrame
    cgBody ret case2
    LabelStart endLabel
    Frame FSame 0 [] 0 []
  where
    store : Int -> Asm ()
    store loc = do
       aload $ locIndex e
       storeVarWithWordSize Astore (Loc loc)

cgIfNonNull : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> LVar -> Int -> SExp -> SExp -> Asm ()
cgIfNonNull ret cgBody e loc ifExp elseExp = cgIfElse ret cgBody e condition (Just loc) ifExp elseExp where
  condition : Label -> Asm ()
  condition label = do
    aload $ locIndex e
    Ifnull label

cgIfNull : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> LVar -> SExp -> SExp -> Asm ()
cgIfNull ret cgBody e ifExp elseExp = cgIfElse ret cgBody e condition Nothing ifExp elseExp where
  condition : Label -> Asm ()
  condition label = do
    aload $ locIndex e
    Ifnonnull label

cgIfTrueElse : (InferredType -> Asm ()) -> ((InferredType -> Asm ()) -> SExp -> Asm ()) -> LVar -> SExp -> SExp -> Asm ()
cgIfTrueElse ret cgBody e ifExp elseExp = cgIfElse ret cgBody e condition Nothing ifExp elseExp where
  condition : Label -> Asm ()
  condition elseLabel = do
    locTypes <- GetFunctionLocTypes
    let conditionVarTy = getLocTy locTypes e
    loadVar locTypes conditionVarTy IBool e
    Ifeq elseLabel