module Representation.BuildPlan

import Std.List

-- A small, target-neutral inspection surface.  Concrete system and hardware
-- packages retain their rich typed values; this record is their readable
-- pre-emission summary for people and tooling.
family BuildPlanEntry : Type 0
constructor BuildPlanEntryValue
field unrestricted buildPlanEntryName : Bytes
field unrestricted buildPlanEntryValue : Bytes

end-family

family SystemTargetBuildPlan : Type 0
constructor SystemTargetBuildPlanValue
field unrestricted systemTargetBuildPlanIdentity : Bytes
field unrestricted systemTargetBuildPlanCapabilityAccepted : Nat
field unrestricted systemTargetBuildPlanEntries : (family StdList (family BuildPlanEntry))

end-family

def buildPlanEmpty : (family StdList (family BuildPlanEntry)) =
  (constructor StdList StdListEmpty (family BuildPlanEntry))

def buildPlanCons =
  (lambda unrestricted name : Bytes .
    (lambda unrestricted value : Bytes .
      (lambda unrestricted rest : (family StdList (family BuildPlanEntry)) .
        (constructor
          StdList
          StdListCons
          (family BuildPlanEntry)
          (record BuildPlanEntry (buildPlanEntryName = name) (buildPlanEntryValue = value))
          rest))))

def renderBuildPlanEntry =
  (lambda unrestricted entry : (family BuildPlanEntry) .
    (eliminate
      BuildPlanEntry
      (lambda unrestricted current : (family BuildPlanEntry) . Bytes)
      entry
      (branch
        BuildPlanEntryValue
        name
        value
        .
        (bytes-append name (bytes-append b"=" (bytes-append value b"\n"))))))

def renderBuildPlanEntries =
  (lambda unrestricted entries : (family StdList (family BuildPlanEntry)) .
    (eliminate
      StdList
      (lambda unrestricted current : (family StdList (family BuildPlanEntry)) . Bytes)
      entries
      (branch StdListEmpty . b"")
      (branch
        StdListCons
        head
        tail
        induction
        .
        (bytes-append (renderBuildPlanEntry head) induction))))

def renderSystemTargetBuildPlan =
  (lambda unrestricted plan : (family SystemTargetBuildPlan) .
    (eliminate
      SystemTargetBuildPlan
      (lambda unrestricted current : (family SystemTargetBuildPlan) . Bytes)
      plan
      (branch
        SystemTargetBuildPlanValue
        identity
        accepted
        entries
        .
        (renderBuildPlanEntries entries))))

def systemTargetBuildPlanAccepted =
  (lambda unrestricted plan : (family SystemTargetBuildPlan) .
    (eliminate
      SystemTargetBuildPlan
      (lambda unrestricted current : (family SystemTargetBuildPlan) . Nat)
      plan
      (branch SystemTargetBuildPlanValue identity accepted entries . accepted)))