Commit b3b5f558 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename some proofmode stuff to be no longer primitive view shift specific.

parent d24b62fe
From iris.prelude Require Export strings.
Inductive spec_goal_kind := GoalStd | GoalPvs.
Inductive spec_goal_kind := GoalStd | GoalVs.
Inductive spec_pat :=
| SGoal : spec_goal_kind bool list string spec_pat
......@@ -18,7 +18,7 @@ Inductive token :=
| TPersistent : token
| TPure : token
| TForall : token
| TPvs : token.
| TVs : token.
Fixpoint cons_name (kn : string) (k : list token) : list token :=
match kn with "" => k | _ => TName (string_rev kn) :: k end.
......@@ -33,7 +33,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
| String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
| String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
| String "|" (String "=" (String "=" (String ">" s))) =>
tokenize_go s (TPvs :: cons_name kn k) ""
tokenize_go s (TVs :: cons_name kn k) ""
| String a s => tokenize_go s k (String a kn)
end.
Definition tokenize (s : string) : list token := tokenize_go s [] "".
......@@ -49,8 +49,8 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| TBracketL :: TPersistent :: TBracketR :: ts => parse_go ts (SGoalPersistent :: k)
| TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SGoalPure :: k)
| TBracketL :: ts => parse_goal ts GoalStd false [] k
| TPvs :: TBracketL :: ts => parse_goal ts GoalPvs false [] k
| TPvs :: ts => parse_go ts (SGoal GoalPvs true [] :: k)
| TVs :: TBracketL :: ts => parse_goal ts GoalVs false [] k
| TVs :: ts => parse_go ts (SGoal GoalVs true [] :: k)
| TPersistent :: TName s :: ts => parse_go ts (SName true s :: k)
| TForall :: ts => parse_go ts (SForall :: k)
| _ => None
......
......@@ -195,7 +195,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
|solve_to_wand H1
|match k with
| GoalStd => apply into_assert_default
| GoalPvs => apply _ || fail "iSpecialize: cannot generate pvs goal"
| GoalVs => apply _ || fail "iSpecialize: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
|(*goal*)
......@@ -762,7 +762,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
eapply tac_assert with _ _ _ lr Hs H Q _; (* (js:=Hs) (j:=H) (P:=Q) *)
[match k with
| GoalStd => apply into_assert_default
| GoalPvs => apply _ || fail "iAssert: cannot generate pvs goal"
| GoalVs => apply _ || fail "iAssert: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
|env_cbv; reflexivity|
......
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