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 | data ControlFlow = Continue | Abort

 34 | public export

 35 | record Codegen where

 36 |   constructor MkCG

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

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

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

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

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

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

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

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

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

 51 |                           (sourcefile : String) ->

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

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

 54 |   incExt : Maybe String

 58 | public export

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

 61 | Eq UsePhase where

 62 |   (==) Cases Cases = True

 63 |   (==) Lifted Lifted = True

 64 |   (==) ANF ANF = True

 65 |   (==) VMCode VMCode = True

 66 |   (==) _ _ = False

 68 | Ord UsePhase where

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

 70 |     where

 71 |       tag : UsePhase -> Int

 72 |       tag Cases = 0

 73 |       tag Lifted = 1

 74 |       tag ANF = 2

 75 |       tag VMCode = 3

 77 | public export

 78 | record CompileData where

 79 |   constructor MkCompileData

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

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

 82 |                      -- For incremental compilation and for compiling exported

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

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

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

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

 87 |   lambdaLifted : List (Name, LiftedDef)

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

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

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

 91 |   anf : List (Name, ANFDef)

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

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

 94 |   vmcode : List (Name, VMDef)

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

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

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

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

104 |           Codegen ->

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

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

107 |     = do d <- getDirs

108 |          let tmpDir = execBuildDir d

109 |          let outputDir = outputDirWithDefault d

110 |          ensureDirectoryExists tmpDir

111 |          ensureDirectoryExists outputDir

112 |          logTime 1 "Code generation overall" $

113 |              compileExpr cg c s tmpDir outputDir tm out

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

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

121 |           Codegen -> ClosedTerm -> Core ()

122 | execute {c} {s} cg tm

123 |     = do d <- getDirs

124 |          let tmpDir = execBuildDir d

125 |          ensureDirectoryExists tmpDir

126 |          executeExpr cg c s tmpDir tm

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

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

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

132 | incCompile {c} {s} cg src

133 |     = do let Just inc = incCompileFile cg

134 |              | Nothing => pure Nothing

135 |          inc c s src

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

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

142 | getMinimalDef (Coded ns bin)

143 |     = do b <- newRef Bin bin

144 |          cdef <- fromBuf

145 |          refsRList <- fromBuf

146 |          let refsR = map fromList refsRList

147 |          fc <- fromBuf

148 |          mul <- fromBuf

149 |          name <- fromBuf

150 |          let def

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

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

153 |                            [] Nothing refsR False False True

154 |                            None cdef Nothing [] Nothing

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

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

160 |              List Name -> -- calls to check

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

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

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

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

165 |                             -- the full definition later.

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

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

168 |              Defs -> Core ()

169 | getAllDesc [] arr defs = pure ()

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

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

172 |            | Just _ => getAllDesc rest arr defs

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

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

175 |                           getAllDesc rest arr defs

176 |             Just (_, entry) =>

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

178 |                  ignore $ addDef n def

179 |                  let refs = refersToRuntime def

180 |                  if multiplicity def /= erased

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

182 |                             let refs = refersToRuntime def

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

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

185 |                     else do log "compile.execute" 20

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

187 |                             getAllDesc rest arr defs

188 | getAllDesc (n :: rest) arr defs

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

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

191 |        getAllDesc rest arr defs

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

194 | warnIfHole n (MkNmError _)

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

196 | warnIfHole n _ = pure ()

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

199 |             -> (Name,FC,CDef)

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

201 | getNamedDef (n,fc,cdef) =

202 |   let ndef = forgetDef cdef

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

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

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

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

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

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

211 | natHackNames : List Name

212 | natHackNames =

213 |     [ UN (Basic "prim__sub_Integer")

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

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

216 |     ]

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

219 | dumpIR fn lns

220 |     = do let cstrs = map dumpDef lns

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

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

223 |          pure ()

224 |   where

225 |     fullShow : Name -> String

226 |     fullShow (DN _ n) = show n

227 |     fullShow n = show n

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

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

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

235 |             Name -> Core Bool

236 | nonErased n

237 |     = do defs <- get Ctxt

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

239 |               | Nothing => pure True

240 |          pure (multiplicity gdef /= erased)

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

244 |              Name -> Core ()

245 | addForeignImpl n

246 |     = do defs <- get Ctxt

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

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

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

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

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

255 | getExported backend all

256 |     = mapMaybe isExp (toList all)

257 |   where

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

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

260 |     isExp (n, cs)

261 |         = do fn <- lookup backend cs

262 |              pure (n, fn)

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

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

270 |                      (doLazyAnnots : Bool) ->

271 |                      UsePhase -> ClosedTerm -> Core CompileData

272 | getCompileDataWith exports doLazyAnnots phase_in tm_in

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

274 |          sopts <- getSession

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

276 |                        [ Cases <$ dumpcases sopts

277 |                        , Lifted <$ dumplifted sopts

278 |                        , ANF <$ dumpanf sopts

279 |                        , VMCode <$ dumpvmcode sopts

280 |                        ]

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

283 |          -- Turn these into runtime errors.

284 |          let metas = addMetas True empty tm_in

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

286 |              do defs <- get Ctxt

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

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

289 |                                     [ "Couldn't find"

290 |                                     , show metanm

291 |                                     , "(probably impossible)"]

292 |                 let Hole _ _ = definition gdef

293 |                   | _ => pure ()

294 |                 let fulln = fullname gdef

295 |                 let cexp = MkError $ CCrash emptyFC

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

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

298 |                                         , namedcompexpr := Just (forgetDef cexp)

299 |                                         } gdef)

301 |          defs <- get Ctxt

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

303 |          exported <- if isNil exports

304 |                  then pure []

305 |                  else getExports defs

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

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

308 |          log "compile.execute" 70 $

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

310 |          tm <- toFullNames tm_in

311 |          natHackNames' <- traverse toResolvedNames natHackNames

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

313 |          -- to check than a NameMap!)

314 |          asize <- getNextEntry

315 |          arr <- coreLift $ newArray asize

317 |          defs <- get Ctxt

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

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

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

322 |          cns <- traverse toFullNames allNs

323 |          log "compile.execute" 30 $

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

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

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

328 |          -- another)

329 |          rcns <- filterM nonErased cns

330 |          log "compile.execute" 40 $

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

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

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

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

336 |          compiledtm <- fixArityExp !(compileExp tm)

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

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

341 |          let cseDefs = intrinsicCons ++ cseDefs

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

344 |            traverse getNamedDef cseDefs

346 |          let mainname = MN "__mainExpression" 0

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

349 |          lifted_in <- if phase >= Lifted

350 |                          then logTime 2 "Lambda lift" $

351 |                               traverse (lambdaLift doLazyAnnots) cseDefs

352 |                          else pure []

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

355 |                       (ldefs ++ concat lifted_in)

357 |          anf <- if phase >= ANF

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

359 |                    else pure []

360 |          vmcode <- if phase >= VMCode

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

362 |                       else pure []

364 |          defs <- get Ctxt

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

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

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

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

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

371 |                dumpIR f lifted

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

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

375 |                dumpIR f anf

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

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

379 |                dumpIR f vmcode

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

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

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

384 |          traverse_ replaceEntry entries

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

386 |   where

387 |     lookupBackend :

388 |         List String ->

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

390 |         Maybe (Name, String)

391 |     lookupBackend [] _ = Nothing

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

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

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

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

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

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

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

405 |                  (doLazyAnnots : Bool) ->

406 |                  UsePhase -> ClosedTerm -> Core CompileData

407 | getCompileData = getCompileDataWith []

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

411 |               ClosedTerm -> Core ClosedCExp

412 | compileTerm tm_in

413 |     = do tm <- toFullNames tm_in

414 |          fixArityExp !(compileExp tm)

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

417 | compDef n = do

418 |   defs <- get Ctxt

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

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

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

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

425 |                     (doLazyAnnots : Bool) ->

426 |                     UsePhase -> Core CompileData

427 | getIncCompileData doLazyAnnots phase

428 |     = do defs <- get Ctxt

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

430 |          -- in the current source file

431 |          let ns = keys (toIR defs)

432 |          cns <- traverse toFullNames ns

433 |          rcns <- filterM nonErased cns

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

436 |          namedDefs <- traverse getNamedDef cseDefs

438 |          lifted_in <- if phase >= Lifted

439 |                          then logTime 2 "Lambda lift" $

440 |                               traverse (lambdaLift doLazyAnnots) cseDefs

441 |                          else pure []

442 |          let lifted = concat lifted_in

443 |          anf <- if phase >= ANF

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

445 |                    else pure []

446 |          vmcode <- if phase >= VMCode

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

448 |                       else pure []

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

456 | exists : String -> IO Bool

457 | exists f

458 |     = do Right ok <- openFile f Read

459 |              | Left err => pure False

460 |          closeFile ok

461 |          pure True

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

474 | parseCC [] _ = Nothing

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

476 |   where

477 |     getOpts : String -> List String

478 |     getOpts "" = []

479 |     getOpts str

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

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

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

483 |     hasTarget : String -> String -> Bool

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

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

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

487 |     findTarget target [] = Nothing

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

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

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

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

492 |                                                                   (assert_total (strTail opts))))

493 |                                   else findTarget target xs

496 | dylib_suffix : String

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

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

500 |            "so"

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

504 |          String -> Core (String, String)

505 | locate libspec

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

507 |          let fname

508 |               = case words libspec of

509 |                      [] => ""

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

511 |                                 then fn -- full filename given

512 |                                 else -- add system extension

513 |                                      fn ++ "." ++ dylib_suffix

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

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

516 |                           -- appropriate for the system

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

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

519 |                                 (dylib_suffix == "dylib",

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

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

523 |          fullname <- catch (findLibraryFile fname)

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

525 |                                     -- in our library path

526 |                                     pure fname)

527 |          pure (fname, fullname)

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

531 | copyLib (lib, fullname)

532 |     = if lib == fullname

533 |          then pure ()

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

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

536 |                  Right _ <- coreLift $ writeToFile lib bin

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

538 |                  pure ()

544 | getExtraRuntime : List String -> Core String

545 | getExtraRuntime directives

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

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

548 |   where

549 |     getArg : String -> Maybe String

550 |     getArg directive =

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

552 |       in

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

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

555 |           else Nothing

557 |     paths : List String

558 |     paths = nub $ mapMaybe getArg $ reverse directives

565 | getWeakMemoLazy : List String -> Bool

566 | getWeakMemoLazy = elem "lazy=weakMemo"

572 | public export

573 | record ConstantPrimitives' str where

574 |   constructor MkConstantPrimitives

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

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

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

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

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

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

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

583 | public export

584 | ConstantPrimitives : Type

585 | ConstantPrimitives = ConstantPrimitives' String

590 | castInt :  ConstantPrimitives' str

591 |         -> PrimType

592 |         -> PrimType

593 |         -> str

594 |         -> Core str

595 | castInt p from to x =

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

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

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

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

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

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

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

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

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