    module Propellor.Property.Uboot where

    import Propellor.Base
    import Propellor.Types.Info
    import Propellor.Types.Bootloader
    import Propellor.Types.Container
    import Propellor.Property.Mount
    import qualified Propellor.Property.Apt as Apt

    -- | Name of a board.
    type BoardName = String

    -- | Installs u-boot for Allwinner/sunxi platforms.
    --
    -- This includes writing it to the boot sector.
    sunxi :: BoardName -> Property (HasInfo + DebianLike)
    sunxi :: BoardName -> Property (HasInfo + DebianLike)
    sunxi boardname :: BoardName
    boardname = Property Linux
    -> Info
    -> Property
         (MetaTypes
            '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
               'Targeting 'OSArchLinux])
    forall k (metatypes' :: k) metatypes.
    (MetaTypes metatypes' ~ (HasInfo + metatypes), SingI metatypes') =>
    Property metatypes -> Info -> Property (MetaTypes metatypes')
    setInfoProperty (Propellor Bool -> Property Linux -> Property Linux
    forall (p :: * -> *) i (m :: * -> *).
    (Checkable p i, LiftPropellor m) =>
    m Bool -> p i -> Property i
    check (Bool -> Bool
    not (Bool -> Bool) -> Propellor Bool -> Propellor Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ContainerCapability -> Propellor Bool
    hasContainerCapability ContainerCapability
    FilesystemContained) Property Linux
    go) Info
    info
    	Property
      (MetaTypes
         '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
            'Targeting 'OSArchLinux])
    -> Property DebianLike
    -> CombinedType
         (Property
            (MetaTypes
               '[ 'WithInfo, 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
                  'Targeting 'OSArchLinux]))
         (Property DebianLike)
    forall x y. Combines x y => x -> y -> CombinedType x y
    `requires` [BoardName] -> Property DebianLike
    Apt.installed ["u-boot", "u-boot-sunxi"]
      where
    	go :: Property Linux
    	go :: Property Linux
    go = BoardName
    -> (OuterMetaTypesWitness
          '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
             'Targeting 'OSArchLinux]
        -> Propellor Result)
    -> Property Linux
    forall k (metatypes :: k).
    SingI metatypes =>
    BoardName
    -> (OuterMetaTypesWitness metatypes -> Propellor Result)
    -> Property (MetaTypes metatypes)
    property' "u-boot installed" ((OuterMetaTypesWitness
        '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
           'Targeting 'OSArchLinux]
      -> Propellor Result)
     -> Property Linux)
    -> (OuterMetaTypesWitness
          '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
             'Targeting 'OSArchLinux]
        -> Propellor Result)
    -> Property Linux
    forall a b. (a -> b) -> a -> b
    $ \w :: OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
         'Targeting 'OSArchLinux]
    w -> do
    		Maybe BoardName
    v <- IO (Maybe BoardName) -> Propellor (Maybe BoardName)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe BoardName) -> Propellor (Maybe BoardName))
    -> IO (Maybe BoardName) -> Propellor (Maybe BoardName)
    forall a b. (a -> b) -> a -> b
    $ BoardName -> IO (Maybe BoardName)
    getMountContaining "/boot"
    		case Maybe BoardName
    v of
    			Nothing -> BoardName -> Propellor Result
    forall a. HasCallStack => BoardName -> a
    error "unable to determine boot device"
    			Just dev :: BoardName
    dev -> OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
         'Targeting 'OSArchLinux]
    -> Property Linux -> Propellor Result
    forall (inner :: [MetaType]) (outer :: [MetaType]).
    EnsurePropertyAllowed inner outer =>
    OuterMetaTypesWitness outer
    -> Property (MetaTypes inner) -> Propellor Result
    ensureProperty OuterMetaTypesWitness
      '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
         'Targeting 'OSArchLinux]
    w (BoardName -> BoardName -> Property Linux
    dd BoardName
    dev "/")
    	dd :: FilePath -> FilePath -> Property Linux
    	dd :: BoardName -> BoardName -> Property Linux
    dd dev :: BoardName
    dev prefix :: BoardName
    prefix = Property
      (MetaTypes
         '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
            'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    -> Property Linux
    forall (p :: * -> *) (untightened :: [MetaType])
           (tightened :: [MetaType]).
    (TightenTargets p, TightenTargetsAllowed untightened tightened,
     SingI tightened) =>
    p (MetaTypes untightened) -> p (MetaTypes tightened)
    tightenTargets (Property
       (MetaTypes
          '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
             'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
     -> Property Linux)
    -> Property
         (MetaTypes
            '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
               'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    -> Property Linux
    forall a b. (a -> b) -> a -> b
    $ BoardName
    -> [BoardName]
    -> UncheckedProperty
         (MetaTypes
            '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
               'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    cmdProperty "dd"
    		[ "conv=fsync,notrunc"
    		, "if=" BoardName -> BoardName -> BoardName
    forall a. [a] -> [a] -> [a]
    ++ BoardName
    prefix BoardName -> BoardName -> BoardName
    forall a. [a] -> [a] -> [a]
    ++ "/usr/lib/u-boot/"
    			BoardName -> BoardName -> BoardName
    forall a. [a] -> [a] -> [a]
    ++ BoardName
    boardname BoardName -> BoardName -> BoardName
    forall a. [a] -> [a] -> [a]
    ++ "/u-boot-sunxi-with-spl.bin"
    		, "of=" BoardName -> BoardName -> BoardName
    forall a. [a] -> [a] -> [a]
    ++ BoardName
    dev
    		, "bs=1024"
    		, "seek=8"
    		]
    		UncheckedProperty
      (MetaTypes
         '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
            'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    -> Result
    -> Property
         (MetaTypes
            '[ 'Targeting 'OSDebian, 'Targeting 'OSBuntish,
               'Targeting 'OSArchLinux, 'Targeting 'OSFreeBSD])
    forall (p :: * -> *) i.
    Checkable p i =>
    p i -> Result -> Property i
    `assume` Result
    NoChange
    	info :: Info
    info = [BootloaderInstalled] -> Info
    forall v. IsInfo v => v -> Info
    toInfo [(BoardName -> BoardName -> Property Linux) -> BootloaderInstalled
    UbootInstalled BoardName -> BoardName -> Property Linux
    dd]