-
Notifications
You must be signed in to change notification settings - Fork 15
/
input.urs
33 lines (24 loc) · 1.21 KB
/
input.urs
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
(* Widget to display some arbitrarily typed fields to a user, with the option to edit *)
functor Make(M : sig
con const :: {Type}
con given :: {Type}
con fixed :: {Type}
con chosen :: {(Type * Type * Type)}
constraint const ~ given
constraint (const ++ given) ~ fixed
constraint (const ++ given ++ fixed) ~ chosen
val const : $const
table tab : (const ++ given ++ fixed ++ map fst3 chosen)
val chosenLabels : $(map (fn _ => string) chosen)
val widgets : $(map Widget.t' chosen)
val constFl : folder const
val givenFl : folder given
val chosenFl : folder chosen
val constInj : $(map sql_injectable const)
val givenInj : $(map sql_injectable given)
val givenEq : $(map eq given)
val chosenInj : $(map (fn p => sql_injectable p.1) chosen)
val textLabel : string
(* Authentication *)
val amGiven : transaction (option $given)
end) : Ui.S where type input = $M.given