Commit eddaf56d authored by Dan Frumin's avatar Dan Frumin

Add [Hint Mode]s to the reification typeclasses.

parent f8cb4921
......@@ -3,6 +3,10 @@ From iris_c.vcgen Require Import vcg denv reification.
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
(** Splits a spatial environment [Γin] into a symbolic heap [m] and
the rest [Γout]. May collect additional [known_locs].
- Inputs: [E, Γin].
- Outputs: [E', Γout, m] *)
Class IntoDEnv `{cmonadG Σ} (E E' : known_locs) (Γin Γout : env (iProp Σ)) (m : denv) := {
into_denv : [] Γin [] Γout denv_interp E' m;
into_denv_env_wf : env_wf Γin env_wf Γout;
......@@ -10,6 +14,15 @@ Class IntoDEnv `{cmonadG Σ} (E E' : known_locs) (Γin Γout : env (iProp Σ)) (
into_denv_wf : denv_wf E' m;
into_denv_mono : E `prefix_of` E';
}.
Arguments IntoDEnv {_ _} _ _ _ _ _.
Hint Mode IntoDEnv - - + - + - - : typeclass_instances.
(** Given a proposition [Pin] and a symbolic heap [m] potentially adds
[Pin] to the symbolic heap (resulting in [m2]), replacing [Pin] with
[Pout].
- Inputs: [E, Pin, m1].
- Outptus: [E', Pout, m2].
*)
Class PropIntoDEnv `{cmonadG Σ} (E E' : known_locs) (Pin Pout : iProp Σ) (m1 m2 : denv) := {
prop_into_denv : denv_wf E m1 Pin denv_interp E m1 Pout denv_interp E' m2;
......@@ -17,6 +30,7 @@ Class PropIntoDEnv `{cmonadG Σ} (E E' : known_locs) (Pin Pout : iProp Σ) (m1 m
prop_into_denv_mono : E `prefix_of` E';
}.
Arguments PropIntoDEnv {_ _} _ _ _%I _%I _.
Hint Mode PropIntoDEnv - - + - + - + - : typeclass_instances.
Section tactics.
Context `{cmonadG Σ}.
......
From iris_c.vcgen Require Export dcexpr.
(** * Reification of C syntax *)
(** In this module we use type classes to perform reification. Because
we essentially use type classes as functions, we also declare [Hint
Mode]s that signal to Coq (and to whoever is reading this code) which
arguments of a type class are supposed to be treated as input and
which are supposed to be treated as output. *)
(** Here is a relevant excerpt from the Coq reference manual:
A mode specification is a list of n ‘+’, ‘!’
or ‘-’ items that specify if an argument of the identifier
is to be treated as an input (‘+’), if its head only is an
input (‘!’) or an output (‘-’) of the identifier. For a mode
to match a list of arguments, input terms and input heads
`must not' contain existential variables or be existential
variables respectively, while outputs can be any term.
*)
(** ** IntoDBool *)
Class IntoDBool (b : bool) (db : dbool) :=
into_dbool : b = dbool_interp db.
Hint Mode IntoDBool + - : typeclass_instances.
Instance into_dbool_true : IntoDBool true (dBoolKnown true).
Proof. done. Qed.
......@@ -15,6 +34,7 @@ Proof. done. Qed.
(** ** IntoDInt *)
Class NatIntoDInt (n : nat) (di : dint) :=
nat_into_dint : Z.of_nat n = dint_interp di.
Hint Mode NatIntoDInt + - : typeclass_instances.
Instance nat_into_dint_0 : NatIntoDInt 0 (dInt 0 None).
Proof. done. Qed.
......@@ -30,6 +50,7 @@ Proof. done. Qed.
Class ZIntoDInt (i : Z) (di : dint) :=
Z_into_dint : i = dint_interp di.
Hint Mode ZIntoDInt + - : typeclass_instances.
Instance Z_into_dint_nat n di : NatIntoDInt n di ZIntoDInt (Z.of_nat n) di | 0.
Proof. done. Qed.
......@@ -54,6 +75,7 @@ Class LocLookup (E E' : known_locs) (cl : cloc) (i : nat) := {
loc_lookup : E' !! i = Some cl;
loc_lookup_mono : E `prefix_of` E';
}.
Hint Mode LocLookup + - + - : typeclass_instances.
Instance loc_lookup_new cl : LocLookup [] [cl] cl 0.
Proof. split. done. by exists [cl]. Qed.
......@@ -69,6 +91,7 @@ Class IntoDLoc (E E' : known_locs) (cl : cloc) (dl : dloc) := {
into_dloc_wf : dloc_wf E' dl;
into_dloc_mono : E `prefix_of` E';
}.
Hint Mode IntoDLoc + - + - : typeclass_instances.
Instance into_dloc_lookup E E' cl i :
LocLookup E E' cl i IntoDLoc E E' cl (dLoc i (dInt 0 None)) | 10.
......@@ -89,6 +112,7 @@ Qed.
(** ** IntoDBaseLit *)
Class IntoDBaseLit (l : base_lit) (dl : dbase_lit) :=
into_dbase_lit : l = dbase_lit_interp dl.
Hint Mode IntoDBaseLit + - : typeclass_instances.
Instance into_dbase_lit_int i di :
ZIntoDInt i di IntoDBaseLit (LitInt i) (dLitInt di).
......@@ -107,6 +131,7 @@ Class IntoDVal (E E' : known_locs) (v : val) (dv : dval) := {
into_dval_wf : dval_wf E' dv;
into_dval_mono : E `prefix_of` E';
}.
Hint Mode IntoDVal + - + - : typeclass_instances.
Instance into_dval_base_lit E l dl :
IntoDBaseLit l dl IntoDVal E E (LitV l) (dLitV dl).
......@@ -133,6 +158,7 @@ Class IntoDExpr (E E' : known_locs) (e: expr) (de: dexpr) := {
into_dexpr_wf : dexpr_wf E' de;
into_dexpr_mono : E `prefix_of` E';
}.
Hint Mode IntoDExpr + - + - : typeclass_instances.
Instance into_dexpr_val E E' v dv :
IntoDVal E E' v dv IntoDExpr E E' (Val v) (dEVal dv).
......@@ -164,6 +190,7 @@ Class IntoDCExpr (E E' : known_locs) (e: expr) (de: dcexpr) := {
into_dcexpr_wf : dcexpr_wf E' de;
into_dcexpr_mono : E `prefix_of` E';
}.
Hint Mode IntoDCExpr + - + - : typeclass_instances.
Local Ltac solve_into_dcexpr2 :=
intros [-> ??] [-> ??]; split=> /=;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment