Changes to semantics of deeply embedded ATL#5
Changes to semantics of deeply embedded ATL#5OwenConoly wants to merge 5 commits intoChezJrk:mainfrom
Conversation
* change the type of size_of from ATLexpr -> list Zexpr -> Prop to ATLexpr -> valuation -> list nat -> Prop * remove unnecessary SizeOfSum hypotheses * get rid of "sh" parameter of eval_expr * have one Lbind case instead of two in eval_expr * remove unnecessary hypothesis of EvalSplit * no more Var in Sexprs; only use Get
There was a problem hiding this comment.
I deleted this file, since it was a duplicate of inferpad/InferPad.v
| (*Uncommenting the folllowing code will cause blur_tiles_guarded pad inference | ||
| to take a very very long time. idk if it goes into an infinite loop, but i | ||
| let it run for 30 minutes and nothing happened.*) | ||
| (*solve [ eapply HasPadConcat with | ||
| (x:=0) (y:=0) (a:=0) (b:=0) | ||
| (l1:=0) (r1:=0) (l1:=0) (r2:=0); | ||
| [ repeat (econstructor; autounfold; try intros; simpl ); | ||
| try list_eq; eauto | | ||
| repeat (econstructor; autounfold; try intros; simpl ); | ||
| try list_eq; eauto | | ||
| (l1:=0) (r1:=0) (r2:=0); | ||
| [ infer_size_of | | ||
| infer_size_of | | ||
| autounfold; simpl; intros; try lia; | ||
| infer_pad 0%Z 0%Z | | ||
| autounfold; simpl; intros; try lia; | ||
| infer_pad 0%Z 0%Z | | ||
| arith | | ||
| arith | | ||
| arith | | ||
| arith ] ] | | ||
| arith ] ] |*) |
There was a problem hiding this comment.
Should I delete this case?
There was a problem hiding this comment.
I should mention: originally, this case had a typo that made it always fail. I think the problem was that the l1 argument was passed twice. When I fixed the typo, it began causing the infinite-or-very-long loop.
| Definition stack := fmap string R. | ||
|
|
||
| Inductive Sexpr := | ||
| | Var (v : string) |
There was a problem hiding this comment.
Deleting this seemed reasonable, since my reification tactic always outputs Get x [] rather than Var x, and having only one way to express a variable seems to make things simpler.
| | Div (x y : Sexpr) | ||
| | Sub (x y : Sexpr) | ||
| | Lit (r : R). | ||
| | Lit (r : Q). |
There was a problem hiding this comment.
This change allows writing functions ATLexpr -> _ that do something nontrivial with the value of a literal.
| Inductive eval_Zexprlist : valuation -> list Zexpr -> list Z -> Prop := | ||
| | EvalZNil : forall v, eval_Zexprlist v [] [] | ||
| | EvalZCons : forall v x xs z zs, | ||
| eval_Zexpr v x z -> | ||
| eval_Zexprlist v xs zs -> | ||
| eval_Zexprlist v (x::xs) (z::zs). | ||
| #[export] Hint Constructors eval_Zexprlist. | ||
| Notation eval_Zexprlist v := (Forall2 (eval_Zexpr v)). | ||
|
|
||
| Lemma eval_Zexprlist_app : forall l1 v l1z, | ||
| eval_Zexprlist v l1 l1z -> | ||
| forall l2 l2z, | ||
| eval_Zexprlist v l2 l2z -> | ||
| eval_Zexprlist v (l1++l2) (l1z++l2z). | ||
| Proof. | ||
| induct 1; intros. | ||
| - repeat rewrite app_nil_l. auto. | ||
| - repeat rewrite <- app_comm_cons. | ||
| econstructor. auto. | ||
| auto. | ||
| Qed. | ||
|
|
||
| Definition eq_Z_index_list (l1 l2 : list Zexpr) := | ||
| length l1 = length l2 /\ | ||
| Forall (fun t => eq_zexpr (fst t) (snd t)) | ||
| (combine l1 l2). | ||
| Definition eq_Z_index_list := | ||
| Forall2 eq_zexpr. | ||
| Hint Unfold eq_Z_index_list : core. |
There was a problem hiding this comment.
I am not actually sure why I changed these two definitions. Defining them as Forall2 something seems reasonable enough, but making eval_Zexprlist a notation seems like a very questionable decision. Thoughts?
| all: fail. | ||
| Abort. |
There was a problem hiding this comment.
Apparently this lemma is not used anywhere. Should I delete it?
OwenConoly
force-pushed
the
semantics_changes
branch
from
bd4b3db to
77eb2f0
Compare
1 participant
A few changes to the semantics of deeply embedded ATL, as described in the commit message 2f81c15.
Most of the changes were made because I subjectively judged them to be simplifications, or because they seemed to make my life easier. Exceptions:
size_ofin a not-just-aesthetic way by removing some hypotheses of theSizeOfSumconstructor. These hypotheses were unnecessary.eval_exprin a not-just-aesthetic way by removing a hypothesis of theEvalSplitconstructor. This hypothesis made it inconsistent with the semantics of shallowly embedded ATL.