-- | Machine-specific properties.
--
-- Many embedded computers have their own special configuration needed
-- to use them. Rather than needing to hunt down documentation about the
-- kernel, bootloader, etc for a given machine, if there's a property
-- in here for your machine, you can simply use it.
--
-- Not all machine properties have been tested yet. If one flagged as
-- untested and you find it works, please let us know.
--
-- You will need to configure the `Host` with the right `Architecture`
-- for the machine. These properties do test at runtime that a supported
-- Architecture was selected.
--
-- Sometimes non-free firmware is needed to use a board. If the board won't
-- be functional at all without it, its property will include the non-free
-- firmware, but if the non-free firmware is only needed for non-critical
-- functionality, it won't be included.
-- 
-- Example: Building a disk image for a Marvell SheevaPlug 
--
-- This defines a Host "sheeva" that is a Marvell SheevaPlug.
-- A bootable disk image for "sheeva" is built on another machine
-- "darkstar", which can be eg an Intel laptop running Debian.
--
-- > import Propellor.Property.Machine
-- > import Propellor.Property.DiskImage
-- > 
-- > sheeva :: Host
-- > sheeva = host "sheeva.example.com" $ props
-- > 	& osDebian Unstable ARMEL
-- > 	& marvell_SheevaPlug Marvell_SheevaPlug_SDCard
-- >	& hasPartition
-- >		( partition EXT4
-- > 		`mountedAt` "/"
-- >		`addFreeSpace` MegaBytes 2048
-- >		)
-- >
-- > darkstar :: Host
-- > darkstar = host "darkstar.example.com" $ props
-- >	& imageBuiltFor sheeva
-- >		(RawDiskImage "/srv/sheeva-disk.img")
-- >		(Debootstrapped mempty)

module Propellor.Property.Machine (
	-- * ARM boards
	Marvell_SheevaPlug_BootDevice(..),
	marvell_SheevaPlug,
	cubietech_Cubietruck,
	olimex_A10_OLinuXino_LIME,
	lemaker_Banana_Pi,
	-- * ARM boards (untested)
	cubietech_Cubieboard,
	cubietech_Cubieboard2,
	lemaker_Banana_Pro,
	olimex_A10s_OLinuXino_Micro,
	olimex_A20_OLinuXino_LIME,
	olimex_A20_OLinuXino_LIME2,
	olimex_A20_OLinuXino_Micro,
	olimex_A20_SOM_EVB,
	linkSprite_pcDuino3_Nano,
) where

import Propellor.Base
import Propellor.Types.Core
import qualified Propellor.Property.Apt as Apt
import qualified Propellor.Property.FlashKernel as FlashKernel
import qualified Propellor.Property.Uboot as Uboot
import Propellor.Property.DiskImage.PartSpec

data Marvell_SheevaPlug_BootDevice
	= Marvell_SheevaPlug_SDCard
	| Marvell_SheevaPlug_ESATA

-- | Marvell SheevaPlug
--
-- This includes a small EXT2 formatted /boot partition.
--
-- Note that u-boot may need to be upgraded manually, and will need to be
-- configured to boot from the SD card or eSATA. See
-- https://www.cyrius.com/debian/kirkwood/sheevaplug/install/
marvell_SheevaPlug :: Marvell_SheevaPlug_BootDevice -> Property (HasInfo + DebianLike)
marvell_SheevaPlug :: Marvell_SheevaPlug_BootDevice -> Property (HasInfo + DebianLike)
marvell_SheevaPlug Marvell_SheevaPlug_BootDevice
bd = Property
  (MetaTypes
     '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish])
fk
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
marvell
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` PartSpec PartLocation -> Property (HasInfo + UnixLike)
hasPartition PartSpec PartLocation
bootpart
  where
	fk :: Property (HasInfo + DebianLike)
fk = case Marvell_SheevaPlug_BootDevice
bd of
		Marvell_SheevaPlug_BootDevice
Marvell_SheevaPlug_SDCard ->
			Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Marvell SheevaPlug Reference Board"
		Marvell_SheevaPlug_BootDevice
Marvell_SheevaPlug_ESATA ->
			Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Marvell eSATA SheevaPlug Reference Board"
	-- The boot loader needs an EXT2 boot partition, which comes
	-- first. Add some free space to allow for additional kernel images
	-- and initrds.
	bootpart :: PartSpec PartLocation
	bootpart :: PartSpec PartLocation
bootpart = forall t. Monoid t => Fs -> PartSpec t
partition Fs
EXT2
		forall t. PartSpec t -> Machine -> PartSpec t
`mountedAt` Machine
"/boot"
		PartSpec PartLocation -> PartLocation -> PartSpec PartLocation
`partLocation` PartLocation
Beginning
		forall t. PartSpec t -> PartSize -> PartSpec t
`addFreeSpace` Integer -> PartSize
MegaBytes Integer
150

-- | Cubietech Cubietruck
-- 
-- Wifi needs non-free firmware-brcm80211, which is not installed by
-- this property. Also, see https://bugs.debian.org/844056
cubietech_Cubietruck :: Property (HasInfo + DebianLike)
cubietech_Cubietruck :: Property (HasInfo + DebianLike)
cubietech_Cubietruck = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Cubietech Cubietruck"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Cubietruck"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | Cubietech Cubieboard (untested)
cubietech_Cubieboard :: Property (HasInfo + DebianLike)
cubietech_Cubieboard :: Property (HasInfo + DebianLike)
cubietech_Cubieboard = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Cubietech Cubieboard"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Cubieboard"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
armmp

-- | Cubietech Cubieboard2 (untested)
cubietech_Cubieboard2 :: Property (HasInfo + DebianLike)
cubietech_Cubieboard2 :: Property (HasInfo + DebianLike)
cubietech_Cubieboard2 = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Cubietech Cubieboard2"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Cubieboard2"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | LeMaker Banana Pi
lemaker_Banana_Pi :: Property (HasInfo + DebianLike)
lemaker_Banana_Pi :: Property (HasInfo + DebianLike)
lemaker_Banana_Pi = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"LeMaker Banana Pi"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Bananapi"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | LeMaker Banana Pro (untested)
lemaker_Banana_Pro :: Property (HasInfo + DebianLike)
lemaker_Banana_Pro :: Property (HasInfo + DebianLike)
lemaker_Banana_Pro = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"LeMaker Banana Pro"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Bananapro"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | Olimex A10-OLinuXino-LIME
olimex_A10_OLinuXino_LIME :: Property (HasInfo + DebianLike)
olimex_A10_OLinuXino_LIME :: Property (HasInfo + DebianLike)
olimex_A10_OLinuXino_LIME = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A10-OLinuXino-LIME"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A10-OLinuXino-Lime"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
armmp

-- | Olimex A10s-Olinuxino Micro (untested)
olimex_A10s_OLinuXino_Micro :: Property (HasInfo + DebianLike)
olimex_A10s_OLinuXino_Micro :: Property (HasInfo + DebianLike)
olimex_A10s_OLinuXino_Micro = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A10s-Olinuxino Micro"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A10s-OLinuXino-M"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
armmp

-- | Olimex A20-OlinuXino-LIME (untested)
olimex_A20_OLinuXino_LIME :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_LIME :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_LIME = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A20-OLinuXino-LIME"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A20-OLinuXino-Lime"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | Olimex A20-OlinuXino-LIME2 (untested)
olimex_A20_OLinuXino_LIME2 :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_LIME2 :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_LIME2 = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A20-OLinuXino-LIME2"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A20-OLinuXino-Lime2"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | Olimex A20-Olinuxino Micro (untested)
olimex_A20_OLinuXino_Micro :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_Micro :: Property (HasInfo + DebianLike)
olimex_A20_OLinuXino_Micro = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A20-Olinuxino Micro"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A20-OLinuXino-MICRO"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | Olimex A20-SOM-EVB (untested)
olimex_A20_SOM_EVB :: Property (HasInfo + DebianLike)
olimex_A20_SOM_EVB :: Property (HasInfo + DebianLike)
olimex_A20_SOM_EVB = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"Olimex A20-Olimex-SOM-EVB"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"A20-Olimex-SOM-EVB"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

-- | LinkSprite pcDuino Nano (untested)
--
-- Needs non-free firmware, see
-- https://wiki.debian.org/InstallingDebianOn/Allwinner
linkSprite_pcDuino3_Nano :: Property (HasInfo + DebianLike)
linkSprite_pcDuino3_Nano :: Property (HasInfo + DebianLike)
linkSprite_pcDuino3_Nano = Machine -> Property (HasInfo + DebianLike)
FlashKernel.installed Machine
"LinkSprite pcDuino3 Nano"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Machine -> Property (HasInfo + DebianLike)
sunixi Machine
"Linksprite_pcDuino3"
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` Property DebianLike
lpae

sunixi :: Uboot.BoardName -> Property (HasInfo + DebianLike)
sunixi :: Machine -> Property (HasInfo + DebianLike)
sunixi Machine
boardname = Machine -> Property (HasInfo + DebianLike)
Uboot.sunxi Machine
boardname
	forall x y. Combines x y => x -> y -> CombinedType x y
`requires` [Machine] -> Property DebianLike
Apt.installed
		[ Machine
"firmware-linux-free"
		, Machine
"sunxi-tools"
		]

armmp :: Property DebianLike
armmp :: Property DebianLike
armmp = [Architecture] -> Property DebianLike -> Property DebianLike
checkArchitecture [Architecture
ARMHF, Architecture
ARMEL] forall a b. (a -> b) -> a -> b
$
	[Machine] -> Property DebianLike
Apt.installed [Machine
"linux-image-armmp"]

lpae :: Property DebianLike
lpae :: Property DebianLike
lpae = [Architecture] -> Property DebianLike -> Property DebianLike
checkArchitecture [Architecture
ARMHF, Architecture
ARMEL] forall a b. (a -> b) -> a -> b
$ 
	[Machine] -> Property DebianLike
Apt.installed [Machine
"linux-image-armmp-lpae"]

marvell :: Property DebianLike
marvell :: Property DebianLike
marvell = [Architecture] -> Property DebianLike -> Property DebianLike
checkArchitecture [Architecture
ARMEL] forall a b. (a -> b) -> a -> b
$
	[Machine] -> Property DebianLike
Apt.installed [Machine
"linux-image-marvell"]

checkArchitecture :: [Architecture] -> Property DebianLike -> Property DebianLike
checkArchitecture :: [Architecture] -> Property DebianLike -> Property DebianLike
checkArchitecture [Architecture]
as Property DebianLike
p = forall {k} (metatypes :: k).
SingI metatypes =>
Machine
-> (OuterMetaTypesWitness metatypes
    -> Maybe System -> Propellor Result)
-> Property (MetaTypes metatypes)
withOS (forall p. IsProp p => p -> Machine
getDesc Property DebianLike
p) forall a b. (a -> b) -> a -> b
$ \OuterMetaTypesWitness
  '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
w Maybe System
o -> case Maybe System
o of
	(Just (System Distribution
_ Architecture
arch)) | Architecture
arch forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Architecture]
as -> forall (inner :: [MetaType]) (outer :: [MetaType]).
EnsurePropertyAllowed inner outer =>
OuterMetaTypesWitness outer
-> Property (MetaTypes inner) -> Propellor Result
ensureProperty OuterMetaTypesWitness
  '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish]
w Property DebianLike
p
	Maybe System
_ -> forall a. HasCallStack => Machine -> a
error forall a b. (a -> b) -> a -> b
$ Machine
"Machine needs architecture to be one of: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> Machine
show [Architecture]
as