module Compiler.Common import Compiler.ANFimport Compiler.CompileExprimport Compiler.Inlineimport Compiler.LambdaLiftimport Compiler.VMCode import Core.Contextimport Core.Directoryimport Core.Optionsimport Core.TTimport Core.TTCimport Utils.Binary import Data.IOArrayimport Data.NameMap import System.Info %include C "sys/stat.h" ||| Generic interface to some code generatorpublic exportrecord Codegen where  constructor MkCG  ||| Compile an Idris 2 expression, saving it to a file.  compileExpr : Ref Ctxt Defs -> (execDir : String) ->                ClosedTerm -> (outfile : String) -> Core (Maybe String)  ||| Execute an Idris 2 expression directly.  executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () -- Say which phase of compilation is the last one to use - it saves time if -- you only ask for what you need.public exportdata UsePhase = Cases | Lifted | ANF | VMCode Eq UsePhase where  (==) Cases Cases = True  (==) Lifted Lifted = True  (==) ANF ANF = True  (==) VMCode VMCode = True  (==) _ _ = False Ord UsePhase where  compare x y = compare (tag x) (tag y)    where      tag : UsePhase -> Int      tag Cases = 0      tag Lifted = 0      tag ANF = 0      tag VMCode = 0 public exportrecord CompileData where  constructor MkCompileData  mainExpr : CExp [] -- main expression to execute. This also appears in                     -- the definitions below as MN "__mainExpression" 0  namedDefs : List (Name, FC, NamedDef)  lambdaLifted : List (Name, LiftedDef)       -- ^ lambda lifted definitions, if required. Only the top level names       -- will be in the context, and (for the moment...) I don't expect to       -- need to look anything up, so it's just an alist.  anf : List (Name, ANFDef)       -- ^ lambda lifted and converted to ANF (all arguments to functions       -- and constructors transformed to either variables or Null if erased)  vmcode : List (Name, VMDef)       -- ^ A much simplified virtual machine code, suitable for passing       -- to a more low level target such as C ||| compile||| Given a value of type Codegen, produce a standalone function||| that executes the `compileExpr` method of the Codegenexportcompile : {auto c : Ref Ctxt Defs} ->          Codegen ->          ClosedTerm -> (outfile : String) -> Core (Maybe String)compile {c} cg tm out    = do makeExecDirectory         d <- getDirs         logTime "Code generation overall" $             compileExpr cg c (exec_dir d) tm out ||| execute||| As with `compile`, produce a functon that executes||| the `executeExpr` method of the given Codegenexportexecute : {auto c : Ref Ctxt Defs} ->          Codegen -> ClosedTerm -> Core ()execute {c} cg tm    = do makeExecDirectory         d <- getDirs         executeExpr cg c (exec_dir d) tm         pure () -- If an entry isn't already decoded, get the minimal entry we need for-- compilation, and record the Binary so that we can put it back when we're-- done (so that we don't obliterate the definition)getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe Binary)getMinimalDef (Decoded def) = pure (def, Nothing)getMinimalDef (Coded bin)    = do b <- newRef Bin bin         cdef <- fromBuf b         refsRList <- fromBuf b         let refsR = map fromList refsRList         fc <- fromBuf b         mul <- fromBuf b         name <- fromBuf b         let def             = MkGlobalDef fc name (Erased fc False) [] [] [] [] mul                           [] Public (MkTotality Unchecked IsCovering)                           [] Nothing refsR False False True                           None cdef Nothing []         pure (def, Just bin) -- ||| Recursively get all calls in a function definitiongetAllDesc : {auto c : Ref Ctxt Defs} ->             List Name -> -- calls to check             IOArray (Int, Maybe Binary) ->                            -- which nodes have been visited. If the entry is                            -- present, it's visited. Keep the binary entry, if                            -- we partially decoded it, so that we can put back                            -- the full definition later.                            -- (We only need to decode the case tree IR, and                            -- it's expensive to decode the whole thing)             Defs -> Core ()getAllDesc [] arr defs = pure ()getAllDesc (n@(Resolved i) :: rest) arr defs  = do Nothing <- coreLift $ readArray arr i           | Just _ => getAllDesc rest arr defs       case !(lookupContextEntry n (gamma defs)) of            Nothing => getAllDesc rest arr defs            Just (_, entry) =>              do (def, bin) <- getMinimalDef entry                 addDef n def                  let refs = refersToRuntime def                 if multiplicity def /= erased                    then do coreLift $ writeArray arr i (i, bin)                            let refs = refersToRuntime def                            refs' <- traverse toResolvedNames (keys refs)                            getAllDesc (refs' ++ rest) arr defs                    else getAllDesc rest arr defsgetAllDesc (n :: rest) arr defs  = getAllDesc rest arr defs getNamedDef : {auto c : Ref Ctxt Defs} ->              Name -> Core (Maybe (Name, FC, NamedDef))getNamedDef n    = do defs <- get Ctxt         case !(lookupCtxtExact n (gamma defs)) of              Nothing => pure Nothing              Just def => case namedcompexpr def of                               Nothing => pure Nothing                               Just d => pure (Just (n, location def, d)) replaceEntry : {auto c : Ref Ctxt Defs} ->               (Int, Maybe Binary) -> Core ()replaceEntry (i, Nothing) = pure ()replaceEntry (i, Just b)    = do addContextEntry (Resolved i) b         pure () natHackNames : List NamenatHackNames    = [UN "prim__add_Integer",       UN "prim__sub_Integer",       UN "prim__mul_Integer",       NS ["Prelude"] (UN "natToInteger"),       NS ["Prelude"] (UN "integerToNat")] exportfastAppend : List String -> StringfastAppend xs    = let len = cast (foldr (+) 0 (map length xs)) in          unsafePerformIO $             do b <- newStringBuffer (len+1)                build b xs                getStringFromBuffer b  where    build : StringBuffer -> List String -> IO ()    build b [] = pure ()    build b (x :: xs) = do addToStringBuffer b x                           build b xs -- Hmm, these dump functions are all very similar aren't they...dumpCases : Defs -> String -> List Name ->            Core ()dumpCases defs fn cns    = do cstrs <- traverse dumpCase cns         Right () <- coreLift $ writeFile fn (fastAppend cstrs)               | Left err => throw (FileErr fn err)         pure ()  where    fullShow : Name -> String    fullShow (DN _ n) = show n    fullShow n = show n     dumpCase : Name -> Core String    dumpCase n        = case !(lookupCtxtExact n (gamma defs)) of               Nothing => pure ""               Just d =>                    case namedcompexpr d of                         Nothing => pure ""                         Just def => pure (fullShow n ++ " = " ++ show def ++ "\n") dumpLifted : String -> List (Name, LiftedDef) -> Core ()dumpLifted fn lns    = do let cstrs = map dumpDef lns         Right () <- coreLift $ writeFile fn (fastAppend cstrs)               | Left err => throw (FileErr fn err)         pure ()  where    fullShow : Name -> String    fullShow (DN _ n) = show n    fullShow n = show n     dumpDef : (Name, LiftedDef) -> String    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" dumpANF : String -> List (Name, ANFDef) -> Core ()dumpANF fn lns    = do let cstrs = map dumpDef lns         Right () <- coreLift $ writeFile fn (fastAppend cstrs)               | Left err => throw (FileErr fn err)         pure ()  where    fullShow : Name -> String    fullShow (DN _ n) = show n    fullShow n = show n     dumpDef : (Name, ANFDef) -> String    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" dumpVMCode : String -> List (Name, VMDef) -> Core ()dumpVMCode fn lns    = do let cstrs = map dumpDef lns         Right () <- coreLift $ writeFile fn (fastAppend cstrs)               | Left err => throw (FileErr fn err)         pure ()  where    fullShow : Name -> String    fullShow (DN _ n) = show n    fullShow n = show n     dumpDef : (Name, VMDef) -> String    dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n" -- Find all the names which need compiling, from a given expression, and compile-- them to CExp form (and update that in the Defs).-- Return the names, the type tags, and a compiled version of the expressionexportgetCompileData : {auto c : Ref Ctxt Defs} ->                 UsePhase -> ClosedTerm -> Core CompileDatagetCompileData phase tm_in    = do defs <- get Ctxt         sopts <- getSession         let ns = getRefs (Resolved (-1)) tm_in         tm <- toFullNames tm_in         natHackNames' <- traverse toResolvedNames natHackNames         -- make an array of Bools to hold which names we've found (quicker         -- to check than a NameMap!)         asize <- getNextEntry         arr <- coreLift $ newArray asize         logTime "Get names" $ getAllDesc (natHackNames' ++ keys ns) arr defs          let entries = mapMaybe id !(coreLift (toList arr))         let allNs = map (Resolved . fst) entries         cns <- traverse toFullNames allNs          -- Do a round of merging/arity fixing for any names which were         -- unknown due to cyclic modules (i.e. declared in one, defined in         -- another)         rcns <- filterM nonErased cns         logTime "Merge lambda" $ traverse_ mergeLamDef rcns         logTime "Fix arity" $ traverse_ fixArityDef rcns         logTime "Forget names" $ traverse_ mkForgetDef rcns          compiledtm <- fixArityExp !(compileExp tm)         let mainname = MN "__mainExpression" 0         (liftedtm, ldefs) <- liftBody mainname compiledtm          namedefs <- traverse getNamedDef rcns         lifted_in <- if phase >= Lifted                         then logTime "Lambda lift" $ traverse lambdaLift rcns                         else pure []          let lifted = (mainname, MkLFun [] [] liftedtm) ::                      ldefs ++ concat lifted_in          anf <- if phase >= ANF                   then logTime "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted                   else pure []         vmcode <- if phase >= VMCode                      then logTime "Get VM Code" $ pure (allDefs anf)                      else pure []          defs <- get Ctxt         maybe (pure ())               (\f => do coreLift $ putStrLn $ "Dumping case trees to " ++ f                         dumpCases defs f rcns)               (dumpcases sopts)         maybe (pure ())               (\f => do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f                         dumpLifted f lifted)               (dumplifted sopts)         maybe (pure ())               (\f => do coreLift $ putStrLn $ "Dumping ANF defs to " ++ f                         dumpANF f anf)               (dumpanf sopts)         maybe (pure ())               (\f => do coreLift $ putStrLn $ "Dumping VM defs to " ++ f                         dumpVMCode f vmcode)               (dumpvmcode sopts)          -- We're done with our minimal context now, so put it back the way         -- it was. Back ends shouldn't look at the global context, because         -- it'll have to decode the definitions again.         traverse_ replaceEntry entries         pure (MkCompileData compiledtm                             (mapMaybe id namedefs)                             lifted anf vmcode)  where    nonErased : Name -> Core Bool    nonErased n        = do defs <- get Ctxt             Just gdef <- lookupCtxtExact n (gamma defs)                  | Nothing => pure True             pure (multiplicity gdef /= erased) -- Some things missing from Prelude.File ||| check to see if a given file existsexportexists : String -> IO Boolexists f    = do Right ok <- openFile f Read             | Left err => pure False         closeFile ok         pure True ||| generate a temporary file/nameexporttmpName : IO StringtmpName = foreign FFI_C "tmpnam" (Ptr -> IO String) null ||| change the access rights for a fileexportchmod : String -> Int -> IO ()chmod f m = foreign FFI_C "chmod" (String -> Int -> IO ()) f m -- Parse a calling convention into a backend/target for the call, and-- a comma separated list of any other location data.-- e.g. "scheme:display" - call the scheme function 'display'--      "C:puts,libc,stdio.h" - call the C function 'puts' which is in--      the library libc and the header stdio.h-- Returns Nothing if the string is empty (which a backend can interpret-- however it likes)exportparseCC : String -> Maybe (String, List String)parseCC "" = NothingparseCC str    = case span (/= ':') str of           (target, "") => Just (trim target, [])           (target, opts) => Just (trim target,                                   map trim (getOpts                                       (assert_total (strTail opts))))  where    getOpts : String -> List String    getOpts "" = []    getOpts str        = case span (/= ',') str of               (opt, "") => [opt]               (opt, rest) => opt :: getOpts (assert_total (strTail rest)) exportdylib_suffix : Stringdylib_suffix    = cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"),            (os == "darwin", "dylib")]           "so" exportlocate : {auto c : Ref Ctxt Defs} ->         String -> Core (String, String)locate libspec    = do -- Attempt to turn libspec into an appropriate filename for the system         let fname              = case words libspec of                     [] => ""                     [fn] => if '.' `elem` unpack fn                                then fn -- full filename given                                else -- add system extension                                     fn ++ "." ++ dylib_suffix                     (fn :: ver :: _) =>                          -- library and version given, build path name as                          -- appropriate for the system                          cond [(dylib_suffix == "dll",                                      fn ++ "-" ++ ver ++ ".dll"),                                (dylib_suffix == "dylib",                                      fn ++ "." ++ ver ++ ".dylib")]                                (fn ++ "." ++ dylib_suffix ++ "." ++ ver)          fullname <- catch (findLibraryFile fname)                           (\err => -- assume a system library so not                                    -- in our library path                                    pure fname)         pure (fname, fullname) exportcopyLib : (String, String) -> Core ()copyLib (lib, fullname)    = if lib == fullname         then pure ()         else do Right bin <- coreLift $ readFromFile fullname                    | Left err => throw (FileErr fullname err)                 Right _ <- coreLift $ writeToFile lib bin                    | Left err => throw (FileErr lib err)                 pure ()