Commit a61c87a0 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Support structs/unions with named fields in frontend.

parent 055b4432
...@@ -419,6 +419,9 @@ Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" := ...@@ -419,6 +419,9 @@ Notation "' ( x1 , x2 , x3 , x4 ) ← y ; z" :=
Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" := Notation "' ( x1 , x2 , x3 , x4 , x5 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z)) (y = (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope. (at level 65, next at level 35, only parsing, right associativity) : C_scope.
Notation "' ( x1 , x2 , x3 , x4 , x5 , x6 ) ← y ; z" :=
(y = (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Class MGuard (M : Type Type) := Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, (P M A) M A. mguard: P {dec : Decision P} {A}, (P M A) M A.
......
...@@ -199,14 +199,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := ...@@ -199,14 +199,16 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
repeat match goal with repeat match goal with
| _ => progress simplify_equality' | _ => progress simplify_equality'
| _ => progress simpl_option_monad by tac | _ => progress simpl_option_monad by tac
| H : mbind (M:=option) _ ?o = ?x |- _ => | H : mbind (M:=option) ?f ?o = ?x |- _ =>
match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
match x with Some _ => idtac | None => idtac | _ => fail 1 end; match x with Some _ => idtac | None => idtac | _ => fail 1 end;
destruct o eqn:? let y := fresh in destruct o as [y|] eqn:?;
| H : ?x = mbind (M:=option) _ ?o |- _ => [change (f y = x) in H|change (None = x) in H]
| H : ?x = mbind (M:=option) ?f ?o |- _ =>
match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
match x with Some _ => idtac | None => idtac | _ => fail 1 end; match x with Some _ => idtac | None => idtac | _ => fail 1 end;
destruct o eqn:? let y := fresh in destruct o as [y|] eqn:?;
[change (x = f y) in H|change (x = None) in H]
| H : fmap (M:=option) _ ?o = ?x |- _ => | H : fmap (M:=option) _ ?o = ?x |- _ =>
match o with Some _ => fail 1 | None => fail 1 | _ => idtac end; match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
match x with Some _ => idtac | None => idtac | _ => fail 1 end; match x with Some _ => idtac | None => idtac | _ => fail 1 end;
......
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