From 73df1945b31c0beee88cf4476df4ccd09d31403b Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 26 Jun 2024 20:50:18 +0200 Subject: Import Coq project --- expr.v | 250 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 250 insertions(+) create mode 100644 expr.v (limited to 'expr.v') diff --git a/expr.v b/expr.v new file mode 100644 index 0000000..11c0737 --- /dev/null +++ b/expr.v @@ -0,0 +1,250 @@ +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 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_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. -- cgit v1.2.3