blob: ef35bcb21a594271cdb054c5b19e18e9b260e32f (
about) (
plain) (
blame)
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
|
Require Import Coq.Numbers.DecimalString ExtrOcamlBasic ExtrOcamlString.
From stdpp Require Import strings stringmap gmap.
From mininix Require Import nix.interp.
Definition attr_set_insert (x : string) (α : attr) (αs : gmap string attr) : gmap string attr :=
<[x:=α]> αs.
Definition attr_set_contains (x : string) (αs : gmap string attr) : bool :=
bool_decide (x ∈ dom αs).
Definition attr_set_fold {A} (f : string → attr → A → A) (init : A) (αs : gmap string attr) : A :=
map_fold f init αs.
Definition attr_set_empty : gmap string attr := ∅.
Definition env_fold {A} (f : string → (kind * thunk) → A → A) (init : A) (E : env) : A :=
map_fold f init E.
Definition env_insert_abs (x : string) (t : thunk) (E : env) : env :=
<[x:=(ABS,t)]> E.
Definition thunk_map_fold {A} (f : string → thunk → A → A) (init : A) (bs : gmap string thunk) : A :=
map_fold f init bs.
Definition thunk_map_insert (x : string) (t : thunk) (bs : gmap string thunk) : gmap string thunk :=
<[x:=t]> bs.
Definition thunk_map_empty : gmap string thunk := ∅.
Definition matcher := gmap string (option expr).
Definition matcher_empty : matcher := ∅.
Definition matcher_insert (x : string) (me : option expr) (ms : matcher) : matcher :=
<[x:=me]> ms.
Definition matcher_fold {A} (f : string → option expr → A → A) (init : A) (ms : matcher) : A :=
map_fold f init ms.
Definition env_empty : env := ∅.
Definition string_of_Z (x : Z) : string :=
NilZero.string_of_int (Z.to_int x).
Definition string_to_Z (s : string) : option Z :=
Z.of_int <$> NilZero.int_of_string s.
Separate Extraction
attr_set_insert env_insert_abs matcher_insert thunk_map_insert
attr_set_contains attr_set_fold env_fold matcher_fold thunk_map_fold
env_empty attr_set_empty matcher_empty thunk_map_empty string_of_Z
string_to_Z interp' forallb.
|
