0 | module Compiler.Common

  3 | import Compiler.ANF

  4 | import Compiler.CompileExpr

  5 | import Compiler.Inline

  6 | import Compiler.LambdaLift

  7 | import Compiler.Opts.Constructor

  8 | import Compiler.Opts.CSE

  9 | import Compiler.VMCode

 11 | import Core.Binary.Prims

 12 | import Core.Directory

 13 | import Core.TTC

 15 | import Data.IOArray

 16 | import Data.String as String

 17 | import Libraries.Data.NameMap

 18 | import Libraries.Data.NatSet

 19 | import Libraries.Data.WithDefault

 20 | import Libraries.Utils.Scheme

 22 | import Idris.Syntax

 24 | import System.File

 25 | import System.Info

 27 | %default covering

 30 | public export

 31 | record Codegen where

 32 |   constructor MkCG

 33 |   ||| Compile an Idris 2 expression, saving it to a file.

 34 |   compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->

 35 |                 (tmpDir : String) -> (outputDir : String) ->

 36 |                 ClosedTerm -> (outfile : String) -> Core (Maybe String)

 37 |   ||| Execute an Idris 2 expression directly.

 38 |   executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo ->

 39 |                 (tmpDir : String) -> ClosedTerm -> Core ()

 40 |   ||| Incrementally compile definitions in the current module (toIR defs)

 46 |   incCompileFile : Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo ->

 47 |                           (sourcefile : String) ->

 48 |                           Core (Maybe (String, List String)))

 49 |   ||| If incremental compilation is supported, get the output file extension

 50 |   incExt : Maybe String

 54 | public export

 55 | data UsePhase = Cases | Lifted | ANF | VMCode

 57 | Eq UsePhase where

 58 |   (==) Cases Cases = True

 59 |   (==) Lifted Lifted = True

 60 |   (==) ANF ANF = True

 61 |   (==) VMCode VMCode = True

 62 |   (==) _ _ = False

 64 | Ord UsePhase where

 65 |   compare x y = compare (tag x) (tag y)

 66 |     where

 67 |       tag : UsePhase -> Int

 68 |       tag Cases = 0

 69 |       tag Lifted = 1

 70 |       tag ANF = 2

 71 |       tag VMCode = 3

 73 | public export

 74 | record CompileData where

 75 |   constructor MkCompileData

 76 |   mainExpr : ClosedCExp -- main expression to execute. This also appears in

 77 |                      -- the definitions below as MN "__mainExpression" 0

 78 |                      -- For incremental compilation and for compiling exported

 79 |                      -- names only, this can be set to 'erased'.

 80 |   exported : List (Name, String) -- names to be made accessible to the foreign

 81 |                      -- and what they should be called in that language

 82 |   namedDefs : List (Name, FC, NamedDef)

 83 |   lambdaLifted : List (Name, LiftedDef)

 84 |        -- ^ lambda lifted definitions, if required. Only the top level names

 85 |        -- will be in the context, and (for the moment...) I don't expect to

 86 |        -- need to look anything up, so it's just an alist.

 87 |   anf : List (Name, ANFDef)

 88 |        -- ^ lambda lifted and converted to ANF (all arguments to functions

 89 |        -- and constructors transformed to either variables or Null if erased)

 90 |   vmcode : List (Name, VMDef)

 91 |        -- ^ A much simplified virtual machine code, suitable for passing

 92 |        -- to a more low level target such as C

 98 | compile : {auto c : Ref Ctxt Defs} ->

 99 |           {auto s : Ref Syn SyntaxInfo} ->

100 |           Codegen ->

101 |           ClosedTerm -> (outfile : String) -> Core (Maybe String)

102 | compile {c} {s} cg tm out

103 |     = do d <- getDirs

104 |          let tmpDir = execBuildDir d

105 |          let outputDir = outputDirWithDefault d

106 |          ensureDirectoryExists tmpDir

107 |          ensureDirectoryExists outputDir

108 |          logTime 1 "Code generation overall" $

109 |              compileExpr cg c s tmpDir outputDir tm out

115 | execute : {auto c : Ref Ctxt Defs} ->

116 |           {auto s : Ref Syn SyntaxInfo} ->

117 |           Codegen -> ClosedTerm -> Core ()

118 | execute {c} {s} cg tm

119 |     = do d <- getDirs

120 |          let tmpDir = execBuildDir d

121 |          ensureDirectoryExists tmpDir

122 |          executeExpr cg c s tmpDir tm

125 | incCompile : {auto c : Ref Ctxt Defs} ->

126 |              {auto s : Ref Syn SyntaxInfo} ->

127 |              Codegen -> String -> Core (Maybe (String, List String))

128 | incCompile {c} {s} cg src

129 |     = do let Just inc = incCompileFile cg

130 |              | Nothing => pure Nothing

131 |          inc c s src

136 | getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe (Namespace, Binary))

137 | getMinimalDef (Decoded def) = pure (def, Nothing)

138 | getMinimalDef (Coded ns bin)

139 |     = do b <- newRef Bin bin

140 |          cdef <- fromBuf

141 |          refsRList <- fromBuf

142 |          let refsR = map fromList refsRList

143 |          fc <- fromBuf

144 |          mul <- fromBuf

145 |          name <- fromBuf

146 |          let def

147 |              = MkGlobalDef fc name (Erased fc Placeholder) NatSet.empty NatSet.empty NatSet.empty NatSet.empty mul

148 |                            Scope.empty (specified Public) (MkTotality Unchecked IsCovering) False

149 |                            [] Nothing refsR False False True

150 |                            None cdef Nothing [] Nothing

151 |          pure (def, Just (ns, bin))

155 | getAllDesc : {auto c : Ref Ctxt Defs} ->

156 |              List Name -> -- calls to check

157 |              IOArray (Int, Maybe (Namespace, Binary)) ->

158 |                             -- which nodes have been visited. If the entry is

159 |                             -- present, it's visited. Keep the binary entry, if

160 |                             -- we partially decoded it, so that we can put back

161 |                             -- the full definition later.

162 |                             -- (We only need to decode the case tree IR, and

163 |                             -- it's expensive to decode the whole thing)

164 |              Defs -> Core ()

165 | getAllDesc [] arr defs = pure ()

166 | getAllDesc (n@(Resolved i) :: rest) arr defs

167 |   = do Nothing <- coreLift $ readArray arr i

168 |            | Just _ => getAllDesc rest arr defs

169 |        case !(lookupContextEntry n (gamma defs)) of

170 |             Nothing => do log "compile.execute" 20 $ "Couldn't find " ++ show n

171 |                           getAllDesc rest arr defs

172 |             Just (_, entry) =>

173 |               do (def, bin) <- getMinimalDef entry

174 |                  ignore $ addDef n def

175 |                  let refs = refersToRuntime def

176 |                  if multiplicity def /= erased

177 |                     then do coreLift_ $ writeArray arr i (i, bin)

178 |                             let refs = refersToRuntime def

179 |                             refs' <- traverse toResolvedNames (keys refs)

180 |                             getAllDesc (refs' ++ rest) arr defs

181 |                     else do log "compile.execute" 20

182 |                                $ "Dropping " ++ show n ++ " because it's erased"

183 |                             getAllDesc rest arr defs

184 | getAllDesc (n :: rest) arr defs

185 |   = do log "compile.execute" 20 $

186 |          "Ignoring " ++ show n ++ " because it's not a Resolved name"

187 |        getAllDesc rest arr defs

189 | warnIfHole : Name -> NamedDef -> Core ()

190 | warnIfHole n (MkNmError _)

191 |     = coreLift $ putStrLn $ "Warning: compiling hole " ++ show n

192 | warnIfHole n _ = pure ()

194 | getNamedDef :  {auto c : Ref Ctxt Defs}

195 |             -> (Name,FC,CDef)

196 |             -> Core (Name, FC, NamedDef)

197 | getNamedDef (n,fc,cdef) =

198 |   let ndef = forgetDef cdef

199 |    in warnIfHole n ndef >> pure (n,fc,ndef)

201 | replaceEntry : {auto c : Ref Ctxt Defs} ->

202 |                (Int, Maybe (Namespace, Binary)) -> Core ()

203 | replaceEntry (i, Nothing) = pure ()

204 | replaceEntry (i, Just (ns, b))

205 |     = ignore $ addContextEntry ns (Resolved i) b

207 | natHackNames : List Name

208 | natHackNames =

209 |     [ UN (Basic "prim__sub_Integer")

210 |     , NS typesNS (UN $ Basic "prim__integerToNat")

211 |     , NS eqOrdNS (UN $ Basic "compareInteger")

212 |     ]

214 | dumpIR : Show def => String -> List (Name, def) -> Core ()

215 | dumpIR fn lns

216 |     = do let cstrs = map dumpDef lns

217 |          Right () <- coreLift $ writeFile fn (fastConcat cstrs)

218 |                | Left err => throw (FileErr fn err)

219 |          pure ()

220 |   where

221 |     fullShow : Name -> String

222 |     fullShow (DN _ n) = show n

223 |     fullShow n = show n

225 |     dumpDef : (Name, def) -> String

226 |     dumpDef (n, d) = fullShow n ++ " = " ++ show d ++ "\n"

230 | nonErased : {auto c : Ref Ctxt Defs} ->

231 |             Name -> Core Bool

232 | nonErased n

233 |     = do defs <- get Ctxt

234 |          Just gdef <- lookupCtxtExact n (gamma defs)

235 |               | Nothing => pure True

236 |          pure (multiplicity gdef /= erased)

239 | addForeignImpl : {auto c : Ref Ctxt Defs} ->

240 |              Name -> Core ()

241 | addForeignImpl n

242 |     = do defs <- get Ctxt

243 |          Just def <- lookupCtxtExact n (gamma defs)        | Nothing => pure ()

244 |          let Just (MkForeign cs atys retty) = compexpr def | _ => pure ()

245 |          let xs = map snd $ filter (\x => fst x == n) defs.options.foreignImpl

246 |          setCompiled n (MkForeign (xs ++ cs) atys retty)

250 | getExported : String -> NameMap (List (String, String)) -> List (Name, String)

251 | getExported backend all

252 |     = mapMaybe isExp (toList all)

253 |   where

254 |     -- If the name/convention pair matches the backend, keep the name

255 |     isExp : (Name, List (String, String)) -> Maybe (Name, String)

256 |     isExp (n, cs)

257 |         = do fn <- lookup backend cs

258 |              pure (n, fn)

264 | getCompileDataWith : {auto c : Ref Ctxt Defs} ->

265 |                      List String -> -- which FFI(s), if compiling foreign exports

266 |                      (doLazyAnnots : Bool) ->

267 |                      UsePhase -> ClosedTerm -> Core CompileData

268 | getCompileDataWith exports doLazyAnnots phase_in tm_in

269 |     = do log "compile.execute" 10 $ "Getting compiled data for: " ++ show tm_in

270 |          sopts <- getSession

271 |          let phase = foldl {t=List} (flip $ maybe id max) phase_in $

272 |                        [ Cases <$ dumpcases sopts

273 |                        , Lifted <$ dumplifted sopts

274 |                        , ANF <$ dumpanf sopts

275 |                        , VMCode <$ dumpvmcode sopts

276 |                        ]

278 |          -- When we compile a REPL expression, there may be leftovers holes in it.

279 |          -- Turn these into runtime errors.

280 |          let metas = addMetas True empty tm_in

281 |          for_ (keys metas) $ \ metanm =>

282 |              do defs <- get Ctxt

283 |                 Just gdef <- lookupCtxtExact metanm (gamma defs)

284 |                   | Nothing => log "compile.execute" 50 $ unwords

285 |                                     [ "Couldn't find"

286 |                                     , show metanm

287 |                                     , "(probably impossible)"]

288 |                 let Hole _ _ = definition gdef

289 |                   | _ => pure ()

290 |                 let fulln = fullname gdef

291 |                 let cexp = MkError $ CCrash emptyFC

292 |                          $ "Encountered unimplemented hole " ++ show fulln

293 |                 ignore $ addDef metanm ({ compexpr := Just cexp

294 |                                         , namedcompexpr := Just (forgetDef cexp)

295 |                                         } gdef)

297 |          defs <- get Ctxt

298 |          let refs  = getRefs (Resolved (-1)) tm_in

299 |          exported <- if isNil exports

300 |                  then pure []

301 |                  else getExports defs

302 |          log "compile.export" 25 "exporting: \{show $ map fst exported}"

303 |          let ns = keys (mergeWith const metas refs) ++ map fst exported

304 |          log "compile.execute" 70 $

305 |            "Found names: " ++ concat (intersperse ", " $ map show $ ns)

306 |          tm <- toFullNames tm_in

307 |          natHackNames' <- traverse toResolvedNames natHackNames

308 |          -- make an array of Bools to hold which names we've found (quicker

309 |          -- to check than a NameMap!)

310 |          asize <- getNextEntry

311 |          arr <- coreLift $ newArray asize

313 |          defs <- get Ctxt

314 |          logTime 2 "Get names" $ getAllDesc (natHackNames' ++ ns) arr defs

316 |          let entries = catMaybes !(coreLift (toList arr))

317 |          let allNs = map (Resolved . fst) entries

318 |          cns <- traverse toFullNames allNs

319 |          log "compile.execute" 30 $

320 |            "All names: " ++ concat (intersperse ", " $ map show $ zip allNs cns)

322 |          -- Do a round of merging/arity fixing for any names which were

323 |          -- unknown due to cyclic modules (i.e. declared in one, defined in

324 |          -- another)

325 |          rcns <- filterM nonErased cns

326 |          log "compile.execute" 40 $

327 |            "Kept: " ++ concat (intersperse ", " $ map show rcns)

329 |          logTime 2 "Merge lambda" $ traverse_ mergeLamDef rcns

330 |          logTime 2 "Fix arity" $ traverse_ fixArityDef rcns

331 |          logTime 2 "Fix foreign bindings" $ traverse_ addForeignImpl rcns

332 |          compiledtm <- fixArityExp !(compileExp tm)

334 |          (cseDefs, csetm) <- logTime 2 "CSE" $ cse rcns compiledtm

336 |          -- Add intrinsic constructors (see Compiler.Opts.Constructor)

337 |          let cseDefs = intrinsicCons ++ cseDefs

339 |          namedDefs <- logTime 2 "Forget names" $

340 |            traverse getNamedDef cseDefs

342 |          let mainname = MN "__mainExpression" 0

343 |          (liftedtm, ldefs) <- liftBody {doLazyAnnots} mainname csetm

345 |          lifted_in <- if phase >= Lifted

346 |                          then logTime 2 "Lambda lift" $

347 |                               traverse (lambdaLift doLazyAnnots) cseDefs

348 |                          else pure []

350 |          let lifted = (mainname, MkLFun Scope.empty Scope.empty liftedtm) ::

351 |                       (ldefs ++ concat lifted_in)

353 |          anf <- if phase >= ANF

354 |                    then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted

355 |                    else pure []

356 |          vmcode <- if phase >= VMCode

357 |                       then logTime 2 "Get VM Code" $ pure (allDefs anf)

358 |                       else pure []

360 |          defs <- get Ctxt

361 |          whenJust (dumpcases sopts) $ \ f =>

362 |             do coreLift $ putStrLn $ "Dumping case trees to " ++ f

363 |                dumpIR f (map (\(n, _, def) => (n, def)) namedDefs)

365 |          whenJust (dumplifted sopts) $ \ f =>

366 |             do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f

367 |                dumpIR f lifted

369 |          whenJust (dumpanf sopts) $ \ f =>

370 |             do coreLift $ putStrLn $ "Dumping ANF defs to " ++ f

371 |                dumpIR f anf

373 |          whenJust (dumpvmcode sopts) $ \ f =>

374 |             do coreLift $ putStrLn $ "Dumping VM defs to " ++ f

375 |                dumpIR f vmcode

377 |          -- We're done with our minimal context now, so put it back the way

378 |          -- it was. Back ends shouldn't look at the global context, because

379 |          -- it'll have to decode the definitions again.

380 |          traverse_ replaceEntry entries

381 |          pure (MkCompileData csetm exported namedDefs lifted anf vmcode)

382 |   where

383 |     lookupBackend :

384 |         List String ->

385 |         (Name, List (String, String)) ->

386 |         Maybe (Name, String)

387 |     lookupBackend [] _ = Nothing

388 |     lookupBackend (b :: bs) (n, exps) = case find (\(b', _) => b == b') exps of

389 |         Just (_, exp) => Just (n, exp)

390 |         Nothing => lookupBackend bs (n, exps)

392 |     getExports : Defs -> Core (List (Name, String))

393 |     getExports defs = traverse (\(n, exp) => pure (!(resolved defs.gamma n), exp)) $

394 |         mapMaybe (lookupBackend exports) (toList defs.foreignExports)

400 | getCompileData : {auto c : Ref Ctxt Defs} ->

401 |                  (doLazyAnnots : Bool) ->

402 |                  UsePhase -> ClosedTerm -> Core CompileData

403 | getCompileData = getCompileDataWith []

406 | compileTerm : {auto c : Ref Ctxt Defs} ->

407 |               ClosedTerm -> Core ClosedCExp

408 | compileTerm tm_in

409 |     = do tm <- toFullNames tm_in

410 |          fixArityExp !(compileExp tm)

412 | compDef : {auto c : Ref Ctxt Defs} -> Name -> Core (Maybe (Name, FC, CDef))

413 | compDef n = do

414 |   defs <- get Ctxt

415 |   Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure Nothing

416 |   let Just cexpr =  compexpr def             | Nothing => pure Nothing

417 |   pure $ Just (n, location def, cexpr)

420 | getIncCompileData : {auto c : Ref Ctxt Defs} ->

421 |                     (doLazyAnnots : Bool) ->

422 |                     UsePhase -> Core CompileData

423 | getIncCompileData doLazyAnnots phase

424 |     = do defs <- get Ctxt

425 |          -- Compile all the names in 'toIR', since those are the ones defined

426 |          -- in the current source file

427 |          let ns = keys (toIR defs)

428 |          cns <- traverse toFullNames ns

429 |          rcns <- filterM nonErased cns

430 |          cseDefs <- catMaybes <$> traverse compDef rcns

432 |          namedDefs <- traverse getNamedDef cseDefs

434 |          lifted_in <- if phase >= Lifted

435 |                          then logTime 2 "Lambda lift" $

436 |                               traverse (lambdaLift doLazyAnnots) cseDefs

437 |                          else pure []

438 |          let lifted = concat lifted_in

439 |          anf <- if phase >= ANF

440 |                    then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted

441 |                    else pure []

442 |          vmcode <- if phase >= VMCode

443 |                       then logTime 2 "Get VM Code" $ pure (allDefs anf)

444 |                       else pure []

445 |          pure (MkCompileData (CErased emptyFC) [] namedDefs lifted anf vmcode)

452 | exists : String -> IO Bool

453 | exists f

454 |     = do Right ok <- openFile f Read

455 |              | Left err => pure False

456 |          closeFile ok

457 |          pure True

469 | parseCC : List String -> List String -> Maybe (String, List String)

470 | parseCC [] _ = Nothing

471 | parseCC (target::ts) strs = findTarget target strs <|> parseCC ts strs

472 |   where

473 |     getOpts : String -> List String

474 |     getOpts "" = []

475 |     getOpts str

476 |         = case span (/= ',') str of

477 |                (opt, "") => [opt]

478 |                (opt, rest) => opt :: getOpts (assert_total (strTail rest))

479 |     hasTarget : String -> String -> Bool

480 |     hasTarget target str = case span (/= ':') str of

481 |                             (targetSpec, _) => targetSpec == target

482 |     findTarget : String -> List String -> Maybe (String, List String)

483 |     findTarget target [] = Nothing

484 |     findTarget target (s::xs) = if hasTarget target s

485 |                                   then case span (/= ':') s of

486 |                                         (t, "") => Just (trim t, [])

487 |                                         (t, opts) => Just (trim t, map trim (getOpts

488 |                                                                   (assert_total (strTail opts))))

489 |                                   else findTarget target xs

492 | dylib_suffix : String

494 |     = cond [(elem os $ the (List String) ["windows", "mingw32", "cygwin32"], "dll"),

495 |             (os == "darwin", "dylib")]

496 |            "so"

499 | locate : {auto c : Ref Ctxt Defs} ->

500 |          String -> Core (String, String)

501 | locate libspec

502 |     = do -- Attempt to turn libspec into an appropriate filename for the system

503 |          let fname

504 |               = case words libspec of

505 |                      [] => ""

506 |                      [fn] => if '.' `elem` unpack fn

507 |                                 then fn -- full filename given

508 |                                 else -- add system extension

509 |                                      fn ++ "." ++ dylib_suffix

510 |                      (fn :: ver :: _) =>

511 |                           -- library and version given, build path name as

512 |                           -- appropriate for the system

513 |                           cond [(dylib_suffix == "dll",

514 |                                       fn ++ "-" ++ ver ++ ".dll"),

515 |                                 (dylib_suffix == "dylib",

516 |                                       fn ++ "." ++ ver ++ ".dylib")]

517 |                                 (fn ++ "." ++ dylib_suffix ++ "." ++ ver)

519 |          fullname <- catch (findLibraryFile fname)

520 |                            (\err => -- assume a system library so not

521 |                                     -- in our library path

522 |                                     pure fname)

523 |          pure (fname, fullname)

526 | copyLib : (String, String) -> Core ()

527 | copyLib (lib, fullname)

528 |     = if lib == fullname

529 |          then pure ()

530 |          else do Right bin <- coreLift $ readFromFile fullname

531 |                     | Left err => pure () -- assume a system library installed globally

532 |                  Right _ <- coreLift $ writeToFile lib bin

533 |                     | Left err => throw (FileErr lib err)

534 |                  pure ()

540 | getExtraRuntime : List String -> Core String

541 | getExtraRuntime directives

542 |     = do fileContents <- traverse Core.readFile paths

543 |          pure $ concat $ intersperse "\n" fileContents

544 |   where

545 |     getArg : String -> Maybe String

546 |     getArg directive =

547 |       let (k,v) = break (== '=') directive

548 |       in

549 |         if (trim k) == "extraRuntime"

550 |           then Just $ trim $ substr 1 (length v) v

551 |           else Nothing

553 |     paths : List String

554 |     paths = nub $ mapMaybe getArg $ reverse directives

561 | getWeakMemoLazy : List String -> Bool

562 | getWeakMemoLazy = elem "lazy=weakMemo"

568 | public export

569 | record ConstantPrimitives' str where

570 |   constructor MkConstantPrimitives

571 |   charToInt    : IntKind -> str -> Core str

572 |   intToChar    : IntKind -> str -> Core str

573 |   stringToInt  : IntKind -> str -> Core str

574 |   intToString  : IntKind -> str -> Core str

575 |   doubleToInt  : IntKind -> str -> Core str

576 |   intToDouble  : IntKind -> str -> Core str

577 |   intToInt     : IntKind -> IntKind -> str -> Core str

579 | public export

580 | ConstantPrimitives : Type

581 | ConstantPrimitives = ConstantPrimitives' String

586 | castInt :  ConstantPrimitives' str

587 |         -> PrimType

588 |         -> PrimType

589 |         -> str

590 |         -> Core str

591 | castInt p from to x =

592 |   case ((from, intKind from), (to, intKind to)) of

593 |        ((CharType, _)  , (_, Just k)) => p.charToInt k x

594 |        ((StringType, _), (_, Just k)) => p.stringToInt k x

595 |        ((DoubleType, _), (_, Just k)) => p.doubleToInt k x

596 |        ((_, Just k), (CharType, _))   => p.intToChar k x

597 |        ((_, Just k), (StringType, _)) => p.intToString k x

598 |        ((_, Just k), (DoubleType, _)) => p.intToDouble k x

599 |        ((_, Just k1), (_, Just k2))   => p.intToInt k1 k2 x

600 |        _ => throw $ InternalError $ "invalid cast: + " ++ show from ++ " + ' -> ' + " ++ show to