Representation.BuildPlan

1module Representation.BuildPlan
2
3import Std.List
4
5-- A small, target-neutral inspection surface.  Concrete system and hardware
6-- packages retain their rich typed values; this record is their readable
7-- pre-emission summary for people and tooling.
8family BuildPlanEntry : Type 0
9constructor BuildPlanEntryValue
10field unrestricted buildPlanEntryName : Bytes
11field unrestricted buildPlanEntryValue : Bytes
12
13end-family
14
15family SystemTargetBuildPlan : Type 0
16constructor SystemTargetBuildPlanValue
17field unrestricted systemTargetBuildPlanIdentity : Bytes
18field unrestricted systemTargetBuildPlanCapabilityAccepted : Nat
19field unrestricted systemTargetBuildPlanEntries : (family StdList (family BuildPlanEntry))
20
21end-family
22
23def buildPlanEmpty : (family StdList (family BuildPlanEntry)) =
24  (constructor StdList StdListEmpty (family BuildPlanEntry))
25
26def buildPlanCons =
27  (lambda unrestricted name : Bytes .
28    (lambda unrestricted value : Bytes .
29      (lambda unrestricted rest : (family StdList (family BuildPlanEntry)) .
30        (constructor
31          StdList
32          StdListCons
33          (family BuildPlanEntry)
34          (record BuildPlanEntry (buildPlanEntryName = name) (buildPlanEntryValue = value))
35          rest))))
36
37def renderBuildPlanEntry =
38  (lambda unrestricted entry : (family BuildPlanEntry) .
39    (eliminate
40      BuildPlanEntry
41      (lambda unrestricted current : (family BuildPlanEntry) . Bytes)
42      entry
43      (branch
44        BuildPlanEntryValue
45        name
46        value
47        .
48        (bytes-append name (bytes-append b"=" (bytes-append value b"\n"))))))
49
50def renderBuildPlanEntries =
51  (lambda unrestricted entries : (family StdList (family BuildPlanEntry)) .
52    (eliminate
53      StdList
54      (lambda unrestricted current : (family StdList (family BuildPlanEntry)) . Bytes)
55      entries
56      (branch StdListEmpty . b"")
57      (branch
58        StdListCons
59        head
60        tail
61        induction
62        .
63        (bytes-append (renderBuildPlanEntry head) induction))))
64
65def renderSystemTargetBuildPlan =
66  (lambda unrestricted plan : (family SystemTargetBuildPlan) .
67    (eliminate
68      SystemTargetBuildPlan
69      (lambda unrestricted current : (family SystemTargetBuildPlan) . Bytes)
70      plan
71      (branch
72        SystemTargetBuildPlanValue
73        identity
74        accepted
75        entries
76        .
77        (renderBuildPlanEntries entries))))
78
79def systemTargetBuildPlanAccepted =
80  (lambda unrestricted plan : (family SystemTargetBuildPlan) .
81    (eliminate
82      SystemTargetBuildPlan
83      (lambda unrestricted current : (family SystemTargetBuildPlan) . Nat)
84      plan
85      (branch SystemTargetBuildPlanValue identity accepted entries . accepted)))