Require Import Coq.Strings.String.
From stdpp Require Import gmap.
(* The Nix Expression Language *)
(** Selected operators from Dolsta and Löh, 2008. Newer definitions at
https://nixos.org/manual/nix/stable/language/operators *)
Variant op : Type :=
| O_Eq (* = *)
| O_Lt (* < *)
| O_Plus (* + *)
| O_Min (* - *)
| O_Div (* / *)
| O_Upd. (* // *)
Hint Constructors op : core.
Variant nonempty A := Ne_Cons (head : A) (tail : list A).
Arguments Ne_Cons {A} _ _.
Hint Constructors nonempty : core.
Inductive expr : Type :=
| X_V (v : value) (* v *)
| X_Id (x : string) (* x *)
| X_Attrset (bs : gmap string b_rhs) (* { bᵣ* } *)
| X_LetBinding (bs : gmap string b_rhs) (e : expr) (* let bᵣ* in e *)
| X_Select (e : expr) (xs : nonempty string) (* e.xs *)
| X_SelectOr (e : expr) (xs : nonempty string) (or : expr) (* e.xs or e *)
| X_Apply (e1 e2 : expr) (* e1 e2 *)
| X_Cond (e1 e2 e3 : expr) (* if e1 then e2 else e3 *)
| X_Incl (e1 e2 : expr) (* with e1; e2 *)
| X_Assert (e1 e2 : expr) (* assert e1; e2 *)
| X_Op (op : op) (e1 e2 : expr) (* e1 <op> e2 *)
| X_HasAttr (e1 : expr) (x : string) (* e ? x *)
| X_Force (e : expr) (* force e *)
| X_Closed (e : expr) (* closed(e) *)
| X_Placeholder (x : string) (e : expr) (* placeholderₓ(e) *)
with b_rhs :=
| B_Rec (e : expr) (* := e *)
| B_Nonrec (e : expr) (* :=ᵣ e *)
with matcher :=
| M_Matcher (ms : gmap string m_rhs) (strict : bool)
with m_rhs :=
| M_Mandatory
| M_Optional (e : expr) (* ? e *)
with value :=
| V_Bool (p : bool) : value (* true | false *)
| V_Null : value (* null *)
| V_Int (n : Z) : value (* n *)
| V_Str (s : string) : value (* s *)
| V_Fn (x : string) (e : expr) : value (* x: e *)
| V_AttrsetFn (m : matcher) (e : expr) : value (* { m }: e *)
| V_Attrset (bs : gmap string expr) : value. (* { b* } *)
Hint Constructors expr : core.
Instance Maybe_X_Attrset : Maybe X_Attrset := λ e,
match e with
| X_Attrset bs => Some bs
| _ => None
end.
Instance Maybe_X_V : Maybe X_V := λ e,
match e with
| X_V v => Some v
| _ => None
end.
Instance Maybe_B_Nonrec : Maybe B_Nonrec := λ rhs,
match rhs with
| B_Nonrec e => Some e
| _ => None
end.
Instance Maybe_B_Rec : Maybe B_Rec := λ rhs,
match rhs with
| B_Rec e => Some e
| _ => None
end.
Lemma maybe_b_rhs_excl b :
is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b) → False.
Proof. intros [e2 Hnonrec] [e1 Hrec]. simplify_option_eq. Qed.
Lemma no_b_nonrec__b_rec b :
¬ is_Some (maybe B_Nonrec b) → is_Some (maybe B_Rec b).
Proof.
destruct b; try by eauto.
simplify_eq/=. intros contra. apply is_Some_alt. eauto.
Qed.
Lemma no_b_rec__b_nonrec b :
¬ is_Some (maybe B_Rec b) → is_Some (maybe B_Nonrec b).
Proof.
destruct b; try by eauto.
simplify_eq/=. intros contra. apply is_Some_alt. eauto.
Qed.
Instance Maybe_V_Attrset : Maybe V_Attrset := λ e,
match e with
| V_Attrset bs => Some bs
| _ => None
end.
Instance Maybe_V_Bool : Maybe V_Bool := λ e,
match e with
| V_Bool p => Some p
| _ => None
end.
Global Instance B_Nonrec_inj : Inj (=) (=) B_Nonrec.
Proof. intros [] [] ?; by simplify_eq. Qed.
Definition matcher_keys (m : matcher) : gset string :=
match m with M_Matcher ms _ => dom ms end.
Definition matcher_map (f : expr → expr) (m : matcher) : matcher :=
let map_m_rhs := λ rhs,
match rhs with
| M_Optional e => M_Optional (f e)
| _ => rhs
end in
match m with
| M_Matcher ms strict => M_Matcher (map_m_rhs <$> ms) strict
end.
Local Definition map_delete_all {K V} `{Countable K}
(ks : gset K) (m : gmap K V) : gmap K V :=
set_fold (λ k m', map_delete k m') m ks.
Local Definition b_rhs_map (f g : expr → expr) (rhs : b_rhs) : b_rhs :=
match rhs with
| B_Rec e => B_Rec (f e)
| B_Nonrec e => B_Nonrec (g e)
end.
(* See Dolstra (2006), §4.3.3 and fig. 4.6 (p. 75, PDF: p. 83) *)
Fixpoint subst (subs : gmap string expr) (e : expr) : expr :=
let msubst subs' := b_rhs_map (subst subs') (subst subs) in
match e with
| X_V V_Null | X_V (V_Bool _) | X_V (V_Str _) | X_V (V_Int _) => e
| X_Id x | X_Placeholder x _ => default e (subs !! x)
| X_Attrset bs =>
let subs' := map_delete_all (dom bs) subs in
X_Attrset (msubst subs' <$> bs)
| X_V (V_Attrset bs) =>
X_V (V_Attrset (subst subs <$> bs))
| X_LetBinding bs e' =>
let subs' := map_delete_all (dom bs) subs in
X_LetBinding (msubst subs' <$> bs) (subst subs' e')
| X_Select e' x => X_Select (subst subs e') x
| X_SelectOr e' x or => X_SelectOr (subst subs e') x (subst subs or)
| X_V (V_Fn x e') =>
let subs' := map_delete x subs in
X_V (V_Fn x (subst subs' e'))
| X_V (V_AttrsetFn (M_Matcher ms _ as m) e') =>
let subs' := map_delete_all (matcher_keys m) subs in
X_V (V_AttrsetFn (matcher_map (subst subs') m) (subst subs' e'))
| X_Apply e1 e2 => X_Apply (subst subs e1) (subst subs e2)
| X_Cond e1 e2 e3 => X_Cond (subst subs e1) (subst subs e2) (subst subs e3)
| X_Incl e1 e2 => X_Incl (subst subs e1) (subst subs e2)
| X_Op op e1 e2 => X_Op op (subst subs e1) (subst subs e2)
| X_HasAttr e x => X_HasAttr (subst subs e) x
| X_Assert e1 e2 => X_Assert (subst subs e1) (subst subs e2)
| X_Closed e => X_Closed e
| X_Force e => X_Force (subst subs e)
end.
Definition closed (bs : gmap string expr) : gmap string expr :=
X_Closed <$> bs.
Definition placeholders (bs : gmap string expr) : gmap string expr :=
map_imap (λ (x : string) (e : expr), Some (X_Placeholder x e)) bs.
Definition nonempty_singleton {A} (a : A): nonempty A := Ne_Cons a nil.
Definition nonempty_cons {A} (a : A) (l : nonempty A) : nonempty A :=
match l with Ne_Cons head tail => Ne_Cons a (head :: tail) end.
Definition indirect (bs : gmap string b_rhs) : gmap string expr :=
map_imap (λ (x : string) (rhs : b_rhs),
Some (X_Select (X_Attrset bs) (nonempty_singleton x))) bs.
Definition rec_subst (bs : gmap string b_rhs) : gmap string expr :=
let subs := indirect bs
in (λ b, match b with
| B_Rec e => subst (closed subs) e
| B_Nonrec e => e
end) <$> bs.
Inductive strong_value : Type :=
| SV_Bool (b : bool)
| SV_Null
| SV_Int (n : Z)
| SV_Str (s : string)
| SV_Fn (x : string) (e : expr)
| SV_AttrsetFn (m : matcher) (e : expr)
| SV_Attrset (bs : gmap string strong_value).
Fixpoint value_from_strong_value (sv : strong_value) : value :=
match sv with
| SV_Null => V_Null
| SV_Bool b => V_Bool b
| SV_Int n => V_Int n
| SV_Str s => V_Str s
| SV_Fn x e => V_Fn x e
| SV_AttrsetFn m e => V_AttrsetFn m e
| SV_Attrset bs => V_Attrset (X_V ∘ value_from_strong_value <$> bs)
end.
Global Instance X_V_inj : Inj (=) (=) X_V.
Proof. intros [] [] ?; by simplify_eq. Qed.
Definition expr_from_strong_value : strong_value → expr :=
X_V ∘ value_from_strong_value.
(* Based on the fin_maps test from stdpp *)
Fixpoint sv_size (sv : strong_value) : nat :=
match sv with
| SV_Null | SV_Bool _ | SV_Int _ | SV_Str _
| SV_Fn _ _ | SV_AttrsetFn _ _ => 1
| SV_Attrset bs => S (map_fold (λ _ sv', plus (sv_size sv')) 0 bs)
end.
(* Based on the fin_maps test from stdpp *)
Lemma strong_value_ind' :
∀ P : strong_value → Prop,
P SV_Null →
(∀ b : bool, P (SV_Bool b)) →
(∀ n : Z, P (SV_Int n)) →
(∀ s : string, P (SV_Str s)) →
(∀ (x : string) (e : expr), P (SV_Fn x e)) →
(∀ (m : matcher) (e : expr), P (SV_AttrsetFn m e)) →
(∀ bs : gmap string strong_value,
map_Forall (λ i, P) bs → P (SV_Attrset bs)) →
∀ s : strong_value, P s.
Proof.
intros P PNull PBool PInt PStr PFn PAttrsetFn PAttrset sv.
remember (sv_size sv) as n eqn:Hn. revert sv Hn.
induction (lt_wf n) as [n _ IH]; intros [| | | | | | bs] ->; simpl in *; try done.
apply PAttrset. revert bs IH.
apply (map_fold_ind (λ r bs, (∀ n', n' < S r → _) → map_Forall (λ _, P) bs)).
- intros IH. apply map_Forall_empty.
- intros k sv bs r ? IHbs IHsv. apply map_Forall_insert; [done|]. split.
+ eapply IHsv; [|done]; lia.
+ eapply IHbs. intros; eapply IHsv; [|done]; lia.
Qed.
Coercion X_Id : string >-> expr.
Coercion V_Int : Z >-> value.
(* Leaving this out for now: would conflict with X_Id and
therefore cause ambiguity *)
(* Coercion X_StrVal : string >-> expr. *)
Coercion V_Bool : bool >-> value.
Coercion X_V : value >-> expr.
Coercion value_from_strong_value : strong_value >-> value.
