0 | module Compiler.RefC.RefC

   2 | import Compiler.RefC.CC

   4 | import Compiler.Common

   5 | import Compiler.CompileExpr

   6 | import Compiler.ANF

   7 | import Compiler.Generated

   9 | import Core.Directory

  11 | import Idris.Syntax

  13 | import Libraries.Data.DList

  14 | import Data.SortedSet

  15 | import Data.SortedMap

  16 | import Data.Vect

  18 | import System

  19 | import System.File

  21 | import Protocol.Hex

  22 | import Libraries.Utils.Path

  24 | %default covering

  27 | showcCleanStringChar : Char -> String -> String

  28 | showcCleanStringChar ' ' = ("_" ++)

  29 | showcCleanStringChar '!' = ("_bang" ++)

  30 | showcCleanStringChar '"' = ("_quotation" ++)

  31 | showcCleanStringChar '#' = ("_number" ++)

  32 | showcCleanStringChar '$' = ("_dollar" ++)

  33 | showcCleanStringChar '%' = ("_percent" ++)

  34 | showcCleanStringChar '&' = ("_and" ++)

  35 | showcCleanStringChar '\'' = ("_tick" ++)

  36 | showcCleanStringChar '(' = ("_parenOpen" ++)

  37 | showcCleanStringChar ')' = ("_parenClose" ++)

  38 | showcCleanStringChar '*' = ("_star" ++)

  39 | showcCleanStringChar '+' = ("_plus" ++)

  40 | showcCleanStringChar ',' = ("_comma" ++)

  41 | showcCleanStringChar '-' = ("__" ++)

  42 | showcCleanStringChar '.' = ("_dot" ++)

  43 | showcCleanStringChar '/' = ("_slash" ++)

  44 | showcCleanStringChar ':' = ("_colon" ++)

  45 | showcCleanStringChar ';' = ("_semicolon" ++)

  46 | showcCleanStringChar '<' = ("_lt" ++)

  47 | showcCleanStringChar '=' = ("_eq" ++)

  48 | showcCleanStringChar '>' = ("_gt" ++)

  49 | showcCleanStringChar '?' = ("_question" ++)

  50 | showcCleanStringChar '@' = ("_at" ++)

  51 | showcCleanStringChar '[' = ("_bracketOpen" ++)

  52 | showcCleanStringChar '\\' = ("_backslash" ++)

  53 | showcCleanStringChar ']' = ("_bracketClose" ++)

  54 | showcCleanStringChar '^' = ("_hat" ++)

  55 | showcCleanStringChar '_' = ("_" ++)

  56 | showcCleanStringChar '`' = ("_backquote" ++)

  57 | showcCleanStringChar '{' = ("_braceOpen" ++)

  58 | showcCleanStringChar '|' = ("_or" ++)

  59 | showcCleanStringChar '}' = ("_braceClose" ++)

  60 | showcCleanStringChar '~' = ("_tilde" ++)

  61 | showcCleanStringChar c

  62 |    = if c < chr 32 || c > chr 126

  63 |         then (("u" ++ leftPad '0' 4 (asHex (cast c))) ++)

  64 |         else strCons c

  66 | showcCleanString : List Char -> String -> String

  67 | showcCleanString [] = id

  68 | showcCleanString (c ::cs) = (showcCleanStringChar c) . showcCleanString cs

  70 | cCleanString : String -> String

  71 | cCleanString cs = showcCleanString (unpack cs) ""

  74 | cUserName : UserName -> String

  75 | cUserName (Basic n) = cCleanString n

  76 | cUserName (Field n) = "rec__" ++ cCleanString n

  77 | cUserName Underscore = cCleanString "_"

  80 | cName : Name -> String

  81 | cName (NS ns n) = cCleanString (showNSWithSep "_" ns) ++ "_" ++ cName n

  82 | cName (UN n) = cUserName n

  83 | cName (MN n i) = cCleanString n ++ "_" ++ cCleanString (show i)

  84 | cName (PV n d) = "pat__" ++ cName n

  85 | cName (DN _ n) = cName n

  86 | cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n

  87 | cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)

  88 | cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)

  89 | cName (Resolved i) = "fn__" ++ cCleanString (show i)

  91 | escapeChar : Char -> String

  92 | escapeChar c = if isAlphaNum c || isNL c

  93 |                   then show c

  94 |                   else "(char)" ++ show (ord c)

  96 | cStringQuoted : String -> String

  97 | cStringQuoted cs = strCons '"' (showCString (unpack cs) "\"")

  99 |     showCChar : Char -> String -> String

 100 |     showCChar '\\' = ("\\\\" ++)

 101 |     showCChar c

 102 |        = if c < chr 32

 103 |             then (("\\x" ++ leftPad '0' 2 (asHex (cast c))) ++ "\"\"" ++)

 104 |             else if c < chr 127 then strCons c

 105 |             else if c < chr 65536 then (("\\u" ++ leftPad '0' 4 (asHex (cast c))) ++ "\"\"" ++)

 106 |             else (("\\U" ++ leftPad '0' 8 (asHex (cast c))) ++ "\"\"" ++)

 108 |     showCString : List Char -> String -> String

 109 |     showCString [] = id

 110 |     showCString ('"'::cs) = ("\\\"" ++) . showCString cs

 111 |     showCString (c ::cs) = (showCChar c) . showCString cs

 114 | showIntMin : Int -> String

 115 | showIntMin x = if x == -9223372036854775808

 116 |     then "INT64_MIN"

 117 |     else "INT64_C("++ show x ++")"

 119 | showInt64Min : Int64 -> String

 120 | showInt64Min x = if x == -9223372036854775808

 121 |     then "INT64_MIN"

 122 |     else "INT64_C("++ show x ++")"

 124 | cPrimType : PrimType -> String

 125 | cPrimType IntType = "Int64"

 126 | cPrimType Int8Type = "Int8"

 127 | cPrimType Int16Type = "Int16"

 128 | cPrimType Int32Type = "Int32"

 129 | cPrimType Int64Type = "Int64"

 130 | cPrimType IntegerType = "Integer"

 131 | cPrimType Bits8Type = "Bits8"

 132 | cPrimType Bits16Type = "Bits16"

 133 | cPrimType Bits32Type = "Bits32"

 134 | cPrimType Bits64Type = "Bits64"

 135 | cPrimType StringType = "string"

 136 | cPrimType CharType = "Char"

 137 | cPrimType DoubleType = "Double"

 138 | cPrimType WorldType = "void"

 141 | cOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> String

 142 | cOp (Neg ty)      [x]       = "idris2_negate_"  ++  cPrimType ty ++ "(" ++ x ++ ")"

 143 | cOp StrLength     [x]       = "stringLength(" ++ x ++ ")"

 144 | cOp StrHead       [x]       = "head(" ++ x ++ ")"

 145 | cOp StrTail       [x]       = "tail(" ++ x ++ ")"

 146 | cOp StrReverse    [x]       = "reverse(" ++ x ++ ")"

 147 | cOp (Cast i o)    [x]       = "idris2_cast_" ++ (cPrimType i) ++ "_to_" ++ (cPrimType o) ++ "(" ++ x ++ ")"

 148 | cOp DoubleExp     [x]       = "idris2_mkDouble(exp(idris2_vp_to_Double(" ++ x ++ ")))"

 149 | cOp DoubleLog     [x]       = "idris2_mkDouble(log(idris2_vp_to_Double(" ++ x ++ ")))"

 150 | cOp DoublePow     [x, y]    = "idris2_mkDouble(pow(idris2_vp_to_Double(" ++ x ++ "), idris2_vp_to_Double(" ++ y ++ ")))"

 151 | cOp DoubleSin     [x]       = "idris2_mkDouble(sin(idris2_vp_to_Double(" ++ x ++ ")))"

 152 | cOp DoubleCos     [x]       = "idris2_mkDouble(cos(idris2_vp_to_Double(" ++ x ++ ")))"

 153 | cOp DoubleTan     [x]       = "idris2_mkDouble(tan(idris2_vp_to_Double(" ++ x ++ ")))"

 154 | cOp DoubleASin    [x]       = "idris2_mkDouble(asin(idris2_vp_to_Double(" ++ x ++ ")))"

 155 | cOp DoubleACos    [x]       = "idris2_mkDouble(acos(idris2_vp_to_Double(" ++ x ++ ")))"

 156 | cOp DoubleATan    [x]       = "idris2_mkDouble(atan(idris2_vp_to_Double(" ++ x ++ ")))"

 157 | cOp DoubleSqrt    [x]       = "idris2_mkDouble(sqrt(idris2_vp_to_Double(" ++ x ++ ")))"

 158 | cOp DoubleFloor   [x]       = "idris2_mkDouble(floor(idris2_vp_to_Double(" ++ x ++ ")))"

 159 | cOp DoubleCeiling [x]       = "idris2_mkDouble(ceil(idris2_vp_to_Double(" ++ x ++ ")))"

 160 | cOp (Add ty)      [x, y]    = "idris2_add_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 161 | cOp (Sub ty)      [x, y]    = "idris2_sub_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 162 | cOp (Mul ty)      [x, y]    = "idris2_mul_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 163 | cOp (Div ty)      [x, y]    = "idris2_div_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 164 | cOp (Mod ty)      [x, y]    = "idris2_mod_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 165 | cOp (ShiftL ty)   [x, y]    = "idris2_shiftl_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 166 | cOp (ShiftR ty)   [x, y]    = "idris2_shiftr_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 167 | cOp (BAnd ty)     [x, y]    = "idris2_and_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 168 | cOp (BOr ty)      [x, y]    = "idris2_or_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 169 | cOp (BXOr ty)     [x, y]    = "idris2_xor_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 170 | cOp (LT ty)       [x, y]    = "idris2_lt_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 171 | cOp (GT ty)       [x, y]    = "idris2_gt_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 172 | cOp (EQ ty)       [x, y]    = "idris2_eq_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 173 | cOp (LTE ty)      [x, y]    = "idris2_lte_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 174 | cOp (GTE ty)      [x, y]    = "idris2_gte_" ++ cPrimType ty ++ "(" ++ x ++ ", " ++ y ++ ")"

 175 | cOp StrIndex      [x, i]    = "strIndex(" ++ x ++ ", " ++ i ++ ")"

 176 | cOp StrCons       [x, y]    = "strCons(" ++ x ++ ", " ++ y ++ ")"

 177 | cOp StrAppend     [x, y]    = "strAppend(" ++ x ++ ", " ++ y ++ ")"

 178 | cOp StrSubstr     [x, y, z] = "strSubstr(" ++ x ++ ", " ++ y  ++ ", " ++ z ++ ")"

 179 | cOp BelieveMe     [_, _, x] = "idris2_newReference(" ++ x ++ ")"

 180 | cOp Crash         [_, msg]  = "idris2_crash(" ++ msg ++ ");"

 181 | cOp fn args = show fn ++ "(" ++ (showSep ", " $ toList args) ++ ")"

 183 | varName : AVar -> String

 184 | varName (ALocal i) = "var_" ++ (show i)

 185 | varName (ANull)    = "NULL"

 187 | data ArgCounter : Type where

 188 | data EnvTracker : Type where

 189 | data FunctionDefinitions : Type where

 190 | data IndentLevel : Type where

 191 | data HeaderFiles : Type where

 192 | data ConstDef

 193 |   = CDI64 String

 194 |   | CDB64 String

 195 |   | CDDb  String

 196 |   | CDStr String

 198 | constantName : ConstDef -> String

 199 | constantName = \case

 200 |   CDI64 x => go "Int64" x

 201 |   CDB64 x => go "Bits64" x

 202 |   CDDb x  => go "Double" x

 203 |   CDStr x => go "String" x

 204 |   where go : String -> String -> String

 205 |         go x y = "idris2_constant_\{x}_\{y}"

 207 | ReuseMap = SortedMap Name String

 208 | Owned = SortedSet AVar

 214 | record Env where

 215 |   constructor MkEnv

 216 |   owned : Owned

 217 |   reuseMap : ReuseMap

 222 | data OutfileText : Type where

 224 | Output : Type

 225 | Output = DList String

 229 | getNextCounter : {auto a : Ref ArgCounter Nat} -> Core String

 230 | getNextCounter = do

 231 |     c <- get ArgCounter

 232 |     put ArgCounter (S c)

 233 |     pure $ show c

 235 | getNewVarThatWillNotBeFreedAtEndOfBlock : {auto a : Ref ArgCounter Nat} -> Core String

 236 | getNewVarThatWillNotBeFreedAtEndOfBlock = pure $ "tmp_" ++ !(getNextCounter)

 239 | maxLineLengthForComment : Nat

 240 | maxLineLengthForComment = 60

 242 | lJust : (line:String) -> (fillPos:Nat) -> (filler:Char) -> String

 243 | lJust line fillPos filler =

 244 |     let n = length line in

 245 |     case isLTE n fillPos of

 246 |         (Yes prf) =>

 247 |             let missing = minus fillPos n

 248 |                 fillBlock = pack (replicate missing filler)

 249 |             in

 250 |             line ++ fillBlock

 251 |         (No _) => line

 253 | increaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()

 254 | increaseIndentation = update IndentLevel S

 256 | decreaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()

 257 | decreaseIndentation = update IndentLevel pred

 259 | indentation : {auto il : Ref IndentLevel Nat} -> Core String

 260 | indentation = do

 261 |     iLevel <- get IndentLevel

 262 |     pure $ pack $ replicate (4 * iLevel) ' '

 265 |   : {auto oft : Ref OutfileText Output} ->

 266 |     {auto il : Ref IndentLevel Nat} ->

 267 |     FC -> String -> Core ()

 268 | emit EmptyFC line = do

 269 |     indent <- indentation

 270 |     update OutfileText (flip snoc (indent ++ line))

 271 | emit fc line = do

 272 |     let comment = "// " ++ show fc

 273 |     indent <- indentation

 274 |     let indentedLine = indent ++ line

 275 |     update OutfileText $ case isLTE (length indentedLine) maxLineLengthForComment of

 276 |         (Yes _) => flip snoc (lJust indentedLine maxLineLengthForComment ' ' ++ " " ++ comment)

 277 |         (No _)  => flip appendR [indentedLine, (lJust ""   maxLineLengthForComment ' ' ++ " " ++ comment)]

 279 | applyFunctionToVars : {auto oft : Ref OutfileText Output}

 280 |                     -> {auto il : Ref IndentLevel Nat}

 281 |                     -> String

 282 |                     -> List String

 283 |                     -> Core ()

 284 | applyFunctionToVars fun vars = traverse_ (\v => emit EmptyFC $ fun ++ "(" ++ v ++ ");" ) vars

 286 | removeVars : {auto oft : Ref OutfileText Output}

 287 |            -> {auto il : Ref IndentLevel Nat}

 288 |            -> List String

 289 |            -> Core ()

 290 | removeVars = applyFunctionToVars "idris2_removeReference"

 292 | dupVars : {auto oft : Ref OutfileText Output}

 293 |            -> {auto il : Ref IndentLevel Nat}

 294 |            -> List String

 295 |            -> Core ()

 296 | dupVars = applyFunctionToVars "idris2_newReference"

 299 | removeReuseConstructors : {auto oft : Ref OutfileText Output}

 300 |                         -> {auto il : Ref IndentLevel Nat}

 301 |                         -> List String

 302 |                         -> Core ()

 303 | removeReuseConstructors = applyFunctionToVars "idris2_removeReuseConstructor"

 305 | avarToC : Env -> AVar -> String

 306 | avarToC env var =

 307 |     if contains var env.owned then varName var

 308 |         -- case when the variable is borrowed

 309 |     else "idris2_newReference(" ++ varName var ++ ")"

 311 | avarsToC : Owned -> List AVar -> List String

 312 | avarsToC _ [] = []

 313 | avarsToC owned (v::vars) =

 314 |   let v' = varName v in

 315 |       if contains v owned

 316 |           then v'::avarsToC (delete v owned) vars

 317 |           else "idris2_newReference(\{v'})"::avarsToC owned vars -- when v is borrowed

 319 | moveFromOwnedToBorrowed : Env -> SortedSet AVar -> Env

 320 | moveFromOwnedToBorrowed env vars = { owned $= (`difference` vars) } env

 322 | fillArgs : {auto oft : Ref OutfileText Output}

 323 |          -> {auto il : Ref IndentLevel Nat}

 324 |          -> Env

 325 |          -> String

 326 |          -> List AVar

 327 |          -> Nat

 328 |          -> Core ()

 329 | fillArgs _ _ [] _ = pure ()

 330 | fillArgs env arglist (v :: vars) k = do

 331 |     let ownedVars = if contains v env.owned then singleton v else empty

 332 |     emit EmptyFC $ "\{arglist}[\{show k}] = \{avarToC env v};"

 333 |     fillArgs (moveFromOwnedToBorrowed env ownedVars) arglist vars (S k)

 335 | makeClosure : {auto a : Ref ArgCounter Nat}

 336 |             -> {auto oft : Ref OutfileText Output}

 337 |             -> {auto il : Ref IndentLevel Nat}

 338 |             -> {auto e : Ref EnvTracker Env}

 339 |             -> FC

 340 |             -> Name

 341 |             -> List AVar

 342 |             -> Nat

 343 |             -> Core String

 344 | makeClosure fc n args missing = do

 345 |     let closure = "closure_\{!(getNextCounter)}"

 346 |     let nargs = length args

 347 |     emit fc "Idris2_Value *\{closure} = (Idris2_Value *)idris2_mkClosure((Idris2_Value *(*)())\{cName n}, \{show $ nargs + missing}, \{show nargs});"

 348 |     fillArgs !(get EnvTracker) "((Idris2_Closure*)\{closure})->args" args 0

 349 |     pure closure

 354 | MaxExtractFunArgs : Nat

 355 | MaxExtractFunArgs = 16

 357 | integer_switch : List AConstAlt -> Bool

 358 | integer_switch [] = True

 359 | integer_switch (MkAConstAlt c _  :: _) =

 360 |     case c of

 361 |         (I x) => True

 362 |         (I8 x) => True

 363 |         (I16 x) => True

 364 |         (I32 x) => True

 365 |         (I64 x) => True

 366 |         (B8 x) => True

 367 |         (B16 x) => True

 368 |         (B32 x) => True

 369 |         (B64 x) => True

 370 |         (BI x) => True

 371 |         (Ch x) => True

 372 |         _ => False

 374 | const2Integer : Constant -> Integer -> String

 375 | const2Integer c i =

 376 |     case c of

 377 |         (I x) => showIntMin x

 378 |         (I8 x) => "INT8_C(\{show x})"

 379 |         (I16 x) => "INT16_C(\{show x})"

 380 |         (I32 x) => "INT32_C(\{show x})"

 381 |         (I64 x) => showInt64Min x

 382 |         (BI x) => show x

 383 |         (Ch x) => escapeChar x

 384 |         (B8 x) => "UINT8_C(\{show x})"

 385 |         (B16 x) => "UINT16_C(\{show x})"

 386 |         (B32 x) => "UINT32_C(\{show x})"

 387 |         (B64 x) => "UINT64_C(\{show x})"

 388 |         _ => show i

 390 | data TailPositionStatus = InTailPosition | NotInTailPosition

 394 | dropUnusedReuseCons : ReuseMap -> SortedSet Name -> (List String, ReuseMap)

 395 | dropUnusedReuseCons reuseMap usedCons =

 396 |     -- if there is no constructor named by that name, then the reuse constructor is deleted

 397 |     let dropReuseMap = differenceMap reuseMap usedCons in

 398 |     let actualReuseMap = intersectionMap reuseMap usedCons in

 399 |     (values dropReuseMap, actualReuseMap)

 403 | dropUnusedOwnedVars : Owned -> SortedSet AVar -> (List String, Owned)

 404 | dropUnusedOwnedVars owned usedVars =

 405 |     let actualOwned = intersection owned usedVars in

 406 |     let shouldDrop = difference owned actualOwned in

 407 |     (varName <$> Prelude.toList shouldDrop, actualOwned)

 410 | addReuseConstructor : {auto a : Ref ArgCounter Nat}

 411 |                     -> {auto oft : Ref OutfileText Output}

 412 |                     -> {auto il : Ref IndentLevel Nat}

 413 |                     -> ReuseMap

 414 |                     -> String

 415 |                     -> Name

 416 |                     -> List String

 417 |                     -> SortedSet Name

 418 |                     -> List String

 419 |                     -> SortedMap Name String

 420 |                     -> Core (List String, SortedMap Name String)

 421 | addReuseConstructor reuseMap sc conName conArgs consts shouldDrop actualReuseConsts =

 422 |     -- to avoid conflicts, we check that there is no constructor with the same name in reuse map

 423 |     -- we also check that the constructor will be used later and that the variable will be deleted

 424 |     if (isNothing $ SortedMap.lookup conName reuseMap)

 425 |        && contains conName consts

 426 |        && (isJust $ find (== sc) shouldDrop) then do

 427 |         let constr = "constructor_" ++ !(getNextCounter)

 428 |         emit EmptyFC $ "Idris2_Constructor* " ++ constr ++ " = NULL;"

 429 |         -- If the constructor variable is unique (has 1 reference), then assign it for reuse

 430 |         emit EmptyFC $ "if (idris2_isUnique(" ++ sc ++ ")) {"

 431 |         increaseIndentation

 432 |         emit EmptyFC $ constr ++ " = (Idris2_Constructor*)" ++ sc ++ ";"

 433 |         decreaseIndentation

 434 |         emit EmptyFC "}"

 435 |         -- Otherwise, delete and duplicate constructor variables

 436 |         emit EmptyFC "else {"

 437 |         increaseIndentation

 438 |         -- remove dup and remove if they are executed for the same argument

 439 |         dupVars (conArgs \\ shouldDrop)

 440 |         removeVars [sc]

 441 |         decreaseIndentation

 442 |         emit EmptyFC "}"

 443 |         pure (shouldDrop \\ (sc :: conArgs), insert conName constr actualReuseConsts)

 444 |     else do

 445 |         dupVars $ conArgs \\ shouldDrop

 446 |         pure (shouldDrop \\ conArgs, actualReuseConsts)

 449 |     concaseBody : {auto a : Ref ArgCounter Nat}

 450 |                  -> {auto e : Ref EnvTracker Env}

 451 |                  -> {auto oft : Ref OutfileText Output}

 452 |                  -> {auto il : Ref IndentLevel Nat}

 453 |                  -> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}

 454 |                  -> Env

 455 |                  -> String -> String -> List Int -> ANF -> TailPositionStatus

 456 |                  -> Core ()

 457 |     concaseBody env returnvar expr args body tailPosition = do

 458 |         increaseIndentation

 459 |         _ <- foldlC (\k, arg => do

 460 |             emit emptyFC "Idris2_Value *var_\{show arg} = ((Idris2_Constructor*)\{expr})->args[\{show k}];"

 461 |             pure (S k) ) 0 args

 463 |         let (shouldDrop, actualOwned) = dropUnusedOwnedVars env.owned (freeVariables body)

 464 |         let usedCons = usedConstructors body

 465 |         let (dropReuseCons, actualReuseMap) = dropUnusedReuseCons env.reuseMap usedCons

 466 |         put EnvTracker ({owned := actualOwned, reuseMap := actualReuseMap} env)

 467 |         removeVars shouldDrop

 468 |         removeReuseConstructors dropReuseCons

 469 |         emit emptyFC "\{returnvar} = \{!(cStatementsFromANF body tailPosition)};"

 470 |         decreaseIndentation

 472 |     cStatementsFromANF : {auto a : Ref ArgCounter Nat}

 473 |                       -> {auto oft : Ref OutfileText Output}

 474 |                       -> {auto il : Ref IndentLevel Nat}

 475 |                       -> {auto e : Ref EnvTracker Env}

 476 |                       -> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}

 477 |                       -> ANF

 478 |                       -> TailPositionStatus

 479 |                       -> Core String

 481 |     cStatementsFromANF (AV fc x) _ = pure $ avarToC !(get EnvTracker) x

 482 |     cStatementsFromANF (AAppName fc _ n args) tailPosition = do

 483 |         let nargs = length args

 484 |         case tailPosition of

 485 |             InTailPosition => makeClosure fc n args 0

 486 |             _ => if nargs > MaxExtractFunArgs

 487 |                 then pure "idris2_trampoline(\{!(makeClosure fc n args 0)})"

 488 |                 else do

 489 |                     env <- get EnvTracker

 490 |                     let args' = avarsToC env.owned args

 491 |                     pure "idris2_trampoline(\{cName n}(\{concat $ intersperse ", " args'}))"

 493 |     cStatementsFromANF (AUnderApp fc n missing args) _ = makeClosure fc n args missing

 494 |     cStatementsFromANF (AApp fc _ closure arg) tailPosition = do

 495 |        env <- get EnvTracker

 496 |        pure $ (case tailPosition of

 497 |            NotInTailPosition =>          "idris2_apply_closure"

 498 |            InTailPosition    => "idris2_tailcall_apply_closure") ++ "(\{avarToC env closure}, \{avarToC env arg})"

 500 |     cStatementsFromANF (ALet fc var value body) tailPosition = do

 501 |         env <- get EnvTracker

 502 |         let usedVars = freeVariables body

 503 |         let borrowVal = intersection env.owned (delete (ALocal var) usedVars)

 504 |         let owned' = if contains (ALocal var) usedVars then insert (ALocal var) borrowVal else borrowVal

 505 |         let usedCons = usedConstructors value

 506 |         -- When translating value into C, we borrow variables that will be used in body

 507 |         let valueEnv = { reuseMap $= (`intersectionMap` usedCons) } (moveFromOwnedToBorrowed env borrowVal)

 508 |         put EnvTracker valueEnv

 509 |         emit fc $ "Idris2_Value * var_\{show var} = \{!(cStatementsFromANF value NotInTailPosition)};"

 510 |         unless (contains (ALocal var) usedVars) $ emit fc $ "idris2_removeReference(var_\{show var});"

 511 |         put EnvTracker ({ owned := owned', reuseMap $= (`differenceMap` usedCons) } env)

 512 |         cStatementsFromANF body tailPosition

 514 |     cStatementsFromANF (ACon fc n coninfo tag args) _ = do

 515 |         if coninfo == NIL || coninfo == NOTHING || coninfo == ZERO || coninfo == UNIT

 516 |             then pure "(NULL /* \{show n} */)"

 517 |             else do

 518 |                 env <- get EnvTracker

 519 |                 let createNewConstructor = " = idris2_newConstructor("

 520 |                                  ++ (show (length args))

 521 |                                  ++ ", "  ++ maybe "-1" show tag  ++ ");"

 523 |                 emit fc " // constructor \{show n}"

 524 |                 constr <- case SortedMap.lookup n $ reuseMap env of

 525 |                     Just constr => do

 526 |                         emit fc "if (! \{constr}) {"

 527 |                         increaseIndentation

 528 |                         emit fc $ constr ++ createNewConstructor

 529 |                         decreaseIndentation

 530 |                         emit fc "}"

 531 |                         pure constr

 532 |                     Nothing => do

 533 |                         let constr = "constructor_\{!(getNextCounter)}"

 534 |                         emit fc $ "Idris2_Constructor* " ++ constr ++ createNewConstructor

 535 |                         when (Nothing == tag) $ emit fc "\{constr}->name = idris2_constr_\{cName n};"

 536 |                         pure constr

 537 |                 fillArgs env "\{constr}->args" args 0

 538 |                 pure "(Idris2_Value*)\{constr}"

 540 |     cStatementsFromANF (AOp fc _ op args) _ = do

 541 |         let resultVar = "primVar_" ++ !(getNextCounter)

 542 |         let argsVect : Env -> Vect ar AVar -> Vect ar String

 543 |             argsVect _ [] = []

 544 |             argsVect env (v :: vars) =

 545 |               let ownedVars = if contains v env.owned then singleton v else empty

 546 |               in (avarToC env v) :: argsVect (moveFromOwnedToBorrowed env ownedVars) vars

 548 |         emit fc $ "Idris2_Value *" ++ resultVar ++ " = " ++ cOp op (argsVect !(get EnvTracker) args) ++ ";"

 549 |         -- Removing arguments that apply to primitive functions

 550 |         removeVars $ toList $ map varName args

 551 |         pure resultVar

 553 |     cStatementsFromANF (AExtPrim fc _ p args) _ = do

 554 |         let prims : List String =

 555 |             ["prim__newIORef", "prim__readIORef", "prim__writeIORef", "prim__newArray",

 556 |              "prim__arrayGet", "prim__arraySet", "prim__getField", "prim__setField",

 557 |              "prim__os", "prim__codegen", "prim__onCollect", "prim__onCollectAny" ]

 558 |         case p of

 559 |             NS _ (UN (Basic pn)) =>

 560 |                unless (elem pn prims) $ throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p

 561 |             _ => throw $ InternalError $ "[refc] Unknown primitive: " ++ cName p

 562 |         emit fc $ "// call to external primitive " ++ cName p

 563 |         pure $ "idris2_\{cName p}("++ showSep ", " (map varName args) ++")"

 565 |     cStatementsFromANF (AConCase fc sc alts mDef) tailPosition = do

 566 |         let sc' = varName sc

 567 |         switchReturnVar <- getNewVarThatWillNotBeFreedAtEndOfBlock

 568 |         emit fc "Idris2_Value * \{switchReturnVar} = NULL;"

 569 |         env <- get EnvTracker

 570 |         _ <- foldlC (\els, (MkAConAlt name coninfo tag args body) => do

 571 |             let erased = coninfo == NIL || coninfo == NOTHING || coninfo == ZERO || coninfo == UNIT

 572 |             if erased then emit emptyFC "\{els}if (NULL == \{sc'} /* \{show name} \{show coninfo} */) {"

 573 |                 else if coninfo == CONS || coninfo == JUST || coninfo == SUCC

 574 |                 then emit emptyFC "\{els}if (NULL != \{sc'} /* \{show name} \{show coninfo} */) {"

 575 |                 else do

 576 |                     case tag of

 577 |                         Nothing   => emit emptyFC "\{els}if (! strcmp(((Idris2_Constructor *)\{sc'})->name, idris2_constr_\{cName name})) {"

 578 |                         Just tag' => emit emptyFC "\{els}if (((Idris2_Constructor *)\{sc'})->tag == \{show tag'} /* \{show name} */) {"

 580 |             let conArgs = ALocal <$> args

 581 |             let ownedWithArgs = union (fromList conArgs) $ if erased then delete sc env.owned else env.owned

 582 |             let (shouldDrop, actualOwned) = dropUnusedOwnedVars ownedWithArgs (freeVariables body)

 583 |             let usedCons = usedConstructors body

 584 |             let (dropReuseCons, actualReuseMap) = dropUnusedReuseCons env.reuseMap usedCons

 585 |             increaseIndentation

 586 |             _ <- foldlC (\k, arg => do

 587 |                 emit emptyFC "Idris2_Value *var_\{show arg} = ((Idris2_Constructor*)\{sc'})->args[\{show k}];"

 588 |                 pure (S k) ) 0 args

 589 |             (shouldDrop, actualReuseMap) <- addReuseConstructor env.reuseMap sc' name (varName <$> conArgs) usedCons shouldDrop actualReuseMap

 590 |             removeVars shouldDrop

 591 |             removeReuseConstructors dropReuseCons

 592 |             put EnvTracker ({owned := actualOwned, reuseMap := actualReuseMap} env)

 593 |             emit emptyFC "\{switchReturnVar} = \{!(cStatementsFromANF body tailPosition)};"

 594 |             decreaseIndentation

 595 |             pure "} else ") "" alts

 597 |         case mDef of

 598 |             Nothing => pure ()

 599 |             Just body => do

 600 |                 emit emptyFC "} else {"

 601 |                 concaseBody env switchReturnVar "" [] body tailPosition

 602 |         emit emptyFC "}"

 603 |         pure switchReturnVar

 605 |     cStatementsFromANF (AConstCase fc sc alts def) tailPosition = do

 606 |         let sc' = varName sc

 607 |         switchReturnVar <- getNewVarThatWillNotBeFreedAtEndOfBlock

 608 |         emit fc "Idris2_Value *\{switchReturnVar} = NULL;"

 609 |         env <- get EnvTracker

 610 |         case integer_switch alts of

 611 |             True => do

 612 |                 tmpint <- getNewVarThatWillNotBeFreedAtEndOfBlock

 613 |                 emit emptyFC "int64_t \{tmpint} = idris2_extractInt(\{sc'});"

 614 |                 _ <- foldlC (\els, (MkAConstAlt c body) => do

 615 |                     emit emptyFC "\{els}if (\{tmpint} == \{const2Integer c 0}) {"

 616 |                     concaseBody env switchReturnVar "" [] body tailPosition

 617 |                     pure "} else ") "" alts

 618 |                 pure ()

 620 |             False => do

 621 |                 _ <- foldlC (\els, (MkAConstAlt c body) => do

 622 |                     case c of

 623 |                         Str x => emit emptyFC "\{els}if (! strcmp(\{cStringQuoted x}, ((Idris2_String *)\{sc'})->str)) {"

 624 |                         Db  x => emit emptyFC "\{els}if (((Idris2_Double *)\{sc'})->d == \{show x}) {"

 625 |                         x => throw $ InternalError "[refc] AConstCase : unsupported type. \{show fc} \{show x}"

 626 |                     concaseBody env switchReturnVar "" [] body tailPosition

 627 |                     pure "} else ") "" alts

 628 |                 pure ()

 630 |         case def of

 631 |             Nothing => pure ()

 632 |             Just body => do

 633 |                 emit emptyFC "} else {"

 634 |                 concaseBody env switchReturnVar "" [] body tailPosition

 635 |         emit emptyFC "}"

 636 |         pure switchReturnVar

 638 |     cStatementsFromANF (APrimVal fc (I x)) tailPosition = cStatementsFromANF (APrimVal fc (I64 $ cast x)) tailPosition

 639 |     cStatementsFromANF (APrimVal fc c) _ = do

 640 |       constdefs <- get ConstDef

 641 |       case lookup c constdefs of

 642 |            Just cdef => pure "((Idris2_Value*)&\{constantName cdef})" -- the constant already booked.

 643 |            Nothing => dyngen

 644 |      where

 645 |         orStagen : ConstDef -> Core String

 646 |         orStagen cdef = do -- booking the constant to generate later

 647 |             constdefs <- get ConstDef

 648 |             put ConstDef $ insert c cdef constdefs

 649 |             pure "((Idris2_Value*)&\{constantName cdef})" -- the constant already booked.

 650 |         dyngen : Core String

 651 |         dyngen = case c of

 652 |             I x => if x >= 0 && x < 100

 653 |                 then pure "(Idris2_Value*)(&idris2_predefined_Int64[\{show x}])"

 654 |                 else orStagen $ CDI64 $ cCleanString $ show x

 655 |             I8 x  => pure "idris2_mkInt8(INT8_C(\{show x}))"

 656 |             I16 x => pure "idris2_mkInt16(INT16_C(\{show x}))"

 657 |             I32 x => pure "idris2_mkInt32(INT32_C(\{show x}))"

 658 |             I64 x => if x >= 0 && x < 100

 659 |                 then pure "(Idris2_Value*)(&idris2_predefined_Int64[\{show x}])"

 660 |                 else orStagen $ CDI64 $ cCleanString $ show x

 661 |             BI x => if x >= 0 && x < 100

 662 |                 then pure "idris2_getPredefinedInteger(\{show x})"

 663 |                 else pure "idris2_mkIntegerLiteral(\"\{show x}\")"

 664 |             B8 x  => pure "idris2_mkBits8(UINT8_C(\{show x}))"

 665 |             B16 x => pure "idris2_mkBits16(UINT16_C(\{show x}))"

 666 |             B32 x => pure "idris2_mkBits32(UINT32_C(\{show x}))"

 667 |             B64 x => if x >= 0 && x < 100

 668 |                then pure "(Idris2_Value*)(&idris2_predefined_Bits64[\{show x}])"

 669 |                else orStagen $ CDB64 $ show x

 670 |             Db x => orStagen $ CDDb $ cCleanString $ show x

 671 |             Ch x  => pure "idris2_mkChar(\{escapeChar x})"

 672 |             Str _ => orStagen $ CDStr !(getNextCounter)

 673 |             PrT t => pure $ cPrimType t

 674 |             WorldVal => pure "(NULL /* World */)"

 676 |     cStatementsFromANF (AErased fc) _ = pure "NULL"

 677 |     cStatementsFromANF (ACrash fc x) _ = pure "(NULL /* CRASH */)"

 679 | addCommaToList : List String -> List String

 680 | addCommaToList [] = []

 681 | addCommaToList (x :: xs) = ("  " ++ x) :: map (", " ++) xs

 684 | getArgsNrList : List ty -> Nat -> List Nat

 685 | getArgsNrList [] _ = []

 686 | getArgsNrList (x :: xs) k = k :: getArgsNrList xs (S k)

 689 | cTypeOfCFType : CFType -> String

 690 | cTypeOfCFType CFUnit          = "void"

 691 | cTypeOfCFType CFInt           = "int64_t"

 692 | cTypeOfCFType CFInt8          = "int8_t"

 693 | cTypeOfCFType CFInt16         = "int16_t"

 694 | cTypeOfCFType CFInt32         = "int32_t"

 695 | cTypeOfCFType CFInt64         = "int64_t"

 696 | cTypeOfCFType CFUnsigned8     = "uint8_t"

 697 | cTypeOfCFType CFUnsigned16    = "uint16_t"

 698 | cTypeOfCFType CFUnsigned32    = "uint32_t"

 699 | cTypeOfCFType CFUnsigned64    = "uint64_t"

 700 | cTypeOfCFType CFString        = "char *"

 701 | cTypeOfCFType CFDouble        = "double"

 702 | cTypeOfCFType CFChar          = "char"

 703 | cTypeOfCFType CFPtr           = "void *"

 704 | cTypeOfCFType CFGCPtr         = "void *"

 705 | cTypeOfCFType CFBuffer        = "void *"

 706 | cTypeOfCFType CFWorld         = "void *"

 707 | cTypeOfCFType (CFFun x y)     = "void *"

 708 | cTypeOfCFType (CFIORes x)     = "void *"

 709 | cTypeOfCFType (CFStruct x ys) = "void *"

 710 | cTypeOfCFType (CFUser x ys)   = "void *"

 711 | cTypeOfCFType n = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)

 713 | varNamesFromList : List ty -> Nat -> List String

 714 | varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)

 716 | createFFIArgList : List CFType

 717 |                 -> Core $ List (String, String, CFType)

 718 | createFFIArgList cftypeList = do

 719 |     let sList = map cTypeOfCFType cftypeList

 720 |     let varList = varNamesFromList cftypeList 1

 721 |     pure $ zip3 sList varList cftypeList

 723 | emitFDef : {auto oft : Ref OutfileText Output}

 724 |         -> {auto il : Ref IndentLevel Nat}

 725 |         -> (funcName:Name)

 726 |         -> (arglist:List (String, String, CFType))

 727 |         -> Core ()

 728 | emitFDef funcName [] = emit EmptyFC $ "Idris2_Value *" ++ cName funcName ++ "(void)"

 729 | emitFDef funcName ((varType, varName, varCFType) :: xs) = do

 730 |     emit EmptyFC $ "Idris2_Value *" ++ cName funcName

 731 |     emit EmptyFC "("

 732 |     increaseIndentation

 733 |     emit EmptyFC $ "  Idris2_Value *" ++ varName

 734 |     traverse_ (\(varType, varName, varCFType) => emit EmptyFC $ ", Idris2_Value *" ++ varName) xs

 735 |     decreaseIndentation

 736 |     emit EmptyFC ")"

 739 | data CLang = CLangC | CLangRefC

 741 | extractValue : (cLang : CLang) -> (cfType:CFType) -> (varName:String) -> String

 742 | extractValue _ CFUnit           varName = "NULL"

 743 | extractValue _ CFInt            varName = "(idris2_vp_to_Int64(" ++ varName ++ "))"

 744 | extractValue _ CFInt8           varName = "(idris2_vp_to_Int8(" ++ varName ++ "))"

 745 | extractValue _ CFInt16          varName = "(idris2_vp_to_Int16(" ++ varName ++ "))"

 746 | extractValue _ CFInt32          varName = "(idris2_vp_to_Int32(" ++ varName ++ "))"

 747 | extractValue _ CFInt64          varName = "(idris2_vp_to_Int64(" ++ varName ++ "))"

 748 | extractValue _ CFUnsigned8      varName = "(idris2_vp_to_Bits8(" ++ varName ++ "))"

 749 | extractValue _ CFUnsigned16     varName = "(idris2_vp_to_Bits16(" ++ varName ++ "))"

 750 | extractValue _ CFUnsigned32     varName = "(idris2_vp_to_Bits32(" ++ varName ++ "))"

 751 | extractValue _ CFUnsigned64     varName = "(idris2_vp_to_Bits64(" ++ varName ++ "))"

 752 | extractValue _ CFString         varName = "((Idris2_String*)" ++ varName ++ ")->str"

 753 | extractValue _ CFDouble         varName = "(idris2_vp_to_Double(" ++ varName ++ "))"

 754 | extractValue _ CFChar           varName = "(idris2_vp_to_Char(" ++ varName ++ "))"

 755 | extractValue _ CFPtr            varName = "((Idris2_Pointer*)" ++ varName ++ ")->p"

 756 | extractValue _ CFGCPtr          varName = "((Idris2_GCPointer*)" ++ varName ++ ")->p->p"

 757 | extractValue CLangC    CFBuffer varName = "((Idris2_Buffer*)" ++ varName ++ ")->buffer->data"

 758 | extractValue CLangRefC CFBuffer varName = "((Idris2_Buffer*)" ++ varName ++ ")->buffer"

 759 | extractValue _ CFWorld          _       = "(Idris2_Value *)NULL"

 760 | extractValue _ (CFFun x y)      varName = "(Idris2_Closure*)" ++ varName

 761 | extractValue c (CFIORes x)      varName = extractValue c x varName

 762 | extractValue _ (CFStruct x xs)  varName = assert_total $ idris_crash ("INTERNAL ERROR: Struct access not implemented: " ++ varName)

 764 | extractValue _ (CFUser x xs)    varName = "(Idris2_Value*)" ++ varName

 765 | extractValue _ n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)

 767 | packCFType : (cfType:CFType) -> (varName:String) -> String

 768 | packCFType CFUnit          varName = "((Idris2_Value *)NULL)"

 769 | packCFType CFInt           varName = "idris2_mkInt64(" ++ varName ++ ")"

 770 | packCFType CFInt8          varName = "idris2_mkInt8(" ++ varName ++ ")"

 771 | packCFType CFInt16         varName = "idris2_mkInt16(" ++ varName ++ ")"

 772 | packCFType CFInt32         varName = "idris2_mkInt32(" ++ varName ++ ")"

 773 | packCFType CFInt64         varName = "idris2_mkInt64(" ++ varName ++ ")"

 774 | packCFType CFUnsigned64    varName = "idris2_mkBits64(" ++ varName ++ ")"

 775 | packCFType CFUnsigned32    varName = "idris2_mkBits32(" ++ varName ++ ")"

 776 | packCFType CFUnsigned16    varName = "idris2_mkBits16(" ++ varName ++ ")"

 777 | packCFType CFUnsigned8     varName = "idris2_mkBits8(" ++ varName ++ ")"

 778 | packCFType CFString        varName = "idris2_mkString(" ++ varName ++ ")"

 779 | packCFType CFDouble        varName = "idris2_mkDouble(" ++ varName ++ ")"

 780 | packCFType CFChar          varName = "idris2_mkChar(" ++ varName ++ ")"

 781 | packCFType CFPtr           varName = "idris2_makePointer(" ++ varName ++ ")"

 782 | packCFType CFGCPtr         varName = "idris2_makePointer(" ++ varName ++ ")"

 783 | packCFType CFBuffer        varName = "idris2_makeBuffer(" ++ varName ++ ")"

 784 | packCFType CFWorld         _       = "(Idris2_Value *)NULL"

 785 | packCFType (CFFun x y)     varName = "makeFunction(" ++ varName ++ ")"

 786 | packCFType (CFIORes x)     varName = packCFType x varName

 787 | packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"

 788 | packCFType (CFUser x xs)   varName = varName

 789 | packCFType n _ = assert_total $ idris_crash ("INTERNAL ERROR: Unknown FFI type in C backend: " ++ show n)

 791 | discardLastArgument : List ty -> List ty

 792 | discardLastArgument [] = []

 793 | discardLastArgument xs@(_ :: _) = init xs

 795 | additionalFFIStub : Name -> List CFType -> CFType -> String

 796 | additionalFFIStub name argTypes (CFIORes retType) = additionalFFIStub name (discardLastArgument argTypes) retType

 797 | additionalFFIStub name argTypes retType =

 798 |     cTypeOfCFType retType ++

 799 |     " (*" ++ cName name ++ ")(" ++

 800 |     (concat $ intersperse ", " $ map cTypeOfCFType argTypes) ++ ") = (void*)idris2_missing_ffi;\n"

 802 | createCFunctions : {auto c : Ref Ctxt Defs}

 803 |                 -> {auto a : Ref ArgCounter Nat}

 804 |                 -> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}

 805 |                 -> {auto f : Ref FunctionDefinitions (List String)}

 806 |                 -> {auto oft : Ref OutfileText Output}

 807 |                 -> {auto il : Ref IndentLevel Nat}

 808 |                 -> {auto h : Ref HeaderFiles (SortedSet String)}

 809 |                 -> {default [] additionalFFILangs : List String}

 810 |                 -> Name

 811 |                 -> ANFDef

 812 |                 -> Core ()

 813 | createCFunctions n (MkAFun args anf) = do

 814 |     let nargs = length args

 815 |     let fn = "Idris2_Value *\{cName !(getFullName n)}"

 816 |             ++ (if nargs == 0 then "(void)"

 817 |                else if nargs > MaxExtractFunArgs then "(Idris2_Value *var_arglist[\{show nargs}])"

 818 |                else ("\n(\n" ++ (showSep "\n" $ addCommaToList (map (\i =>  "  Idris2_Value * var_" ++ (show i)) args))) ++ "\n)")

 819 |     update FunctionDefinitions $ \otherDefs => (fn ++ ";\n") :: otherDefs

 821 |     let argsVars = fromList $ ALocal <$> args

 822 |     let bodyFreeVars = freeVariables anf

 823 |     let shouldDrop = difference argsVars bodyFreeVars

 824 |     let argsNrs = getArgsNrList args Z

 825 |     emit EmptyFC fn

 826 |     emit EmptyFC "{"

 827 |     increaseIndentation

 828 |     when (nargs > MaxExtractFunArgs) $ do

 829 |       _ <- foldlC (\i, j => do

 830 |          emit EmptyFC "Idris2_Value *var_\{show j} = var_arglist[\{show i}];"

 831 |          pure $ i + 1) 0 args

 832 |       pure ()

 833 |     removeVars (varName <$> Prelude.toList shouldDrop)

 834 |     _ <- newRef EnvTracker (MkEnv bodyFreeVars empty)

 835 |     emit EmptyFC $ "return \{!(cStatementsFromANF anf InTailPosition)};"

 836 |     decreaseIndentation

 837 |     emit EmptyFC  "}\n"

 838 |     emit EmptyFC  ""

 839 |     pure ()

 842 | createCFunctions n (MkACon Nothing _ _) = do

 843 |   let n' = cName n

 844 |   update FunctionDefinitions $ \otherDefs => "char const idris2_constr_\{n'}[];" :: otherDefs

 845 |   emit EmptyFC "char const idris2_constr_\{n'}[] = \{cStringQuoted $ show n};"

 846 |   pure ()

 848 | createCFunctions n (MkACon tag arity nt) = do

 849 |   emit EmptyFC $ ( "// \{show n} Constructor tag " ++ show tag ++ " arity " ++ show arity) -- Nothing to compile here

 852 | createCFunctions n (MkAForeign ccs fargs ret) = do

 853 |   case parseCC (additionalFFILangs ++ ["RefC", "C"]) ccs of

 854 |       Just (lang, fctForeignName :: extLibOpts) => do

 855 |           let cLang = if lang == "RefC"

 856 |                          then CLangRefC

 857 |                          else CLangC

 858 |           let isStandardFFI = elem lang $ the (List String) ["RefC", "C"]

 859 |           let fctName = if isStandardFFI

 860 |                            then UN $ Basic $ fctForeignName

 861 |                            else NS (mkNamespace lang) n

 862 |           if isStandardFFI

 863 |              then case extLibOpts of

 864 |                       [lib, header] => update HeaderFiles $ insert header

 865 |                       _ => pure ()

 866 |              else emit EmptyFC $ additionalFFIStub fctName fargs ret

 867 |           let fnDef = "Idris2_Value *" ++ (cName n) ++ "(" ++ showSep ", " (replicate (length fargs) "Idris2_Value *") ++ ");"

 868 |           update FunctionDefinitions $ \otherDefs => (fnDef ++ "\n") :: otherDefs

 869 |           typeVarNameArgList <- createFFIArgList fargs

 871 |           emitFDef n typeVarNameArgList

 872 |           emit EmptyFC "{"

 873 |           increaseIndentation

 874 |           emit EmptyFC $ " // ffi call to " ++ cName fctName

 875 |           let removeVarsArgList = removeVars ((\(_, varName, _) => varName) <$> typeVarNameArgList)

 876 |           case ret of

 877 |               CFIORes CFUnit => do

 878 |                   emit EmptyFC $ cName fctName

 879 |                               ++ "("

 880 |                               ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) (discardLastArgument typeVarNameArgList))

 881 |                               ++ ");"

 882 |                   removeVarsArgList

 883 |                   emit EmptyFC "return NULL;"

 884 |               CFIORes ret => do

 885 |                   emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ cName fctName

 886 |                               ++ "("

 887 |                               ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) (discardLastArgument typeVarNameArgList))

 888 |                               ++ ");"

 889 |                   removeVarsArgList

 890 |                   emit EmptyFC $ "return (Idris2_Value*)" ++ packCFType ret "retVal" ++ ";"

 891 |               _ => do

 892 |                   emit EmptyFC $ cTypeOfCFType ret ++ " retVal = " ++ cName fctName

 893 |                               ++ "("

 894 |                               ++ showSep ", " (map (\(_, vn, vt) => extractValue cLang vt vn) typeVarNameArgList)

 895 |                               ++ ");"

 896 |                   removeVarsArgList

 897 |                   emit EmptyFC $ "return (Idris2_Value*)" ++ packCFType ret "retVal" ++ ";"

 899 |           decreaseIndentation

 900 |           emit EmptyFC "}"

 901 |       _ => throw $ InternalError "[refc] FFI not found for \{cName n}"

 902 |           -- not really total but this way this internal error does not contaminate everything else

 904 | createCFunctions n (MkAError exp) = throw $ InternalError "[refc] Error with expression: \{show exp}"

 908 | header : {auto f : Ref FunctionDefinitions (List String)}

 909 |       -> {auto o : Ref OutfileText Output}

 910 |       -> {auto il : Ref IndentLevel Nat}

 911 |       -> {auto h : Ref HeaderFiles (SortedSet String)}

 912 |       -> {auto _ : Ref ConstDef (SortedMap Constant ConstDef)}

 913 |       -> Core ()

 914 | header = do

 915 |     let initLines = """

 920 |     let headerFiles = Prelude.toList !(get HeaderFiles)

 921 |     fns <- get FunctionDefinitions

 922 |     update OutfileText $ appendL $

 923 |         [initLines] ++

 924 |         map (\h => "#include <\{h}>\n") headerFiles ++

 925 |         ["\n// function definitions"] ++

 926 |         fns ++

 927 |         ["\n// constant value definitions"] ++

 928 |         map (uncurry genConstant) (SortedMap.toList !(get ConstDef))

 929 |   where

 930 |     go : ConstDef -> String -> String -> String -> String

 931 |     go cdef ty tag v =

 932 |       "static Idris2_\{ty} const \{constantName cdef}"

 933 |         ++ " = { IDRIS2_STOCKVAL(\{tag}_TAG), \{v} };"