validation.dhall/types.dhall at main · openmls/validation.dhall · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
let Prelude =
      https://prelude.dhall-lang.org/v22.0.0/package.dhall
        sha256:1c7622fdc868fe3a23462df3e6f533e50fdc12ecf3b42c0bb45c328ec8c4293e

let Status
    : Type
    = < Unknown | Missing | Partial | Complete >

let Status/show
    : Status -> Text
    = \(status : Status) ->
        merge
          { Unknown = "Unknown"
          , Missing = "Missing"
          , Partial = "Partial"
          , Complete = "Complete"
          }
          status

let Notes
    : Type
    = { notes : List Text }

let Notes/new
    : List Text -> Notes
    = \(notes : List Text) -> { notes }

let Notes/single
    : Text -> Notes
    = \(note : Text) -> Notes/new [ note ]

let Notes/empty
    : Notes
    = Notes/new ([] : List Text)

let Url
    : Type
    = Text

let Url/new
    : Text -> Url
    = \(url : Text) -> url

let RfcRef
    : Type
    = { text : Text, rfcFragments : List Text }

let RfcRef/single
    : Text -> Text -> RfcRef
    = \(text : Text) ->
      \(rfcFragment : Text) ->
        let rfcFragments = [ rfcFragment ] in { text, rfcFragments }

let RfcRef/new
    : Text -> List Text -> RfcRef
    = \(text : Text) -> \(rfcFragments : List Text) -> { text, rfcFragments }

let RfcRef/urls
    : RfcRef -> List Url
    = \(ref : RfcRef) ->
        Prelude.List.map
          Text
          Url
          ( \(fragment : Text) ->
              "https://www.rfc-editor.org/rfc/rfc9420.html#${fragment}"
          )
          ref.rfcFragments

let Check
    : Type
    = { id : Natural
      , desc : RfcRef
      , implStatus : Status
      , testStatus : Status
      , notes : Notes
      }

let Check/new
    : Natural -> RfcRef -> Status -> Status -> Notes -> Check
    = \(id : Natural) ->
      \(desc : RfcRef) ->
      \(implStatus : Status) ->
      \(testStatus : Status) ->
      \(notes : Notes) ->
        { id, desc, implStatus, testStatus, notes }

let CheckSet
    : Type
    = { id : Natural, name : Text, desc : RfcRef, checks : List Check }

let CheckSet/new
    : Natural -> Text -> RfcRef -> List Check -> CheckSet
    = \(id : Natural) ->
      \(name : Text) ->
      \(desc : RfcRef) ->
      \(checks : List Check) ->
        let checks =
              Prelude.List.map
                Check
                Check
                (\(check : Check) -> check with id = check.id + 100 * id)
                checks

        in  { id, name, desc, checks }

let Natural/equals
    {- tests whether two natural numbers are equal by testing whether both
    -- a-b and b-a (clamping!) are zero -}
    : Natural -> Natural -> Bool
    = \(a : Natural) ->
      \(b : Natural) ->
        let b_minus_a = Natural/subtract a b

        let a_minus_b = Natural/subtract b a

        let a_lte_b = Natural/isZero a_minus_b

        let b_lte_a = Natural/isZero b_minus_a

        in  a_lte_b && b_lte_a

let CheckSet/checkById
    : CheckSet -> Natural -> Optional Check
    = \(checkSet : CheckSet) ->
      \(id : Natural) ->
        Prelude.List.index
          0
          Check
          ( Prelude.List.filter
              Check
              ((\(check : Check) -> Natural/equals id check.id) : Check -> Bool)
              checkSet.checks
          )

in  { Notes
    , Notes/new
    , Notes/single
    , Notes/empty
    , Url
    , Url/new
    , RfcRef
    , RfcRef/single
    , RfcRef/new
    , RfcRef/urls
    , Check
    , Check/new
    , CheckSet
    , CheckSet/new
    , CheckSet/checkById
    , Status
    , Status/show
    }