coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] rewrite problem
- Date: Fri, 01 Oct 2010 13:56:08 -0400
You're right, and I'm feeling terribly foolish for not having noticed the binding long ago.
Michael Doerrie
On 10/01/2010 11:59 AM, Alexandre Pilkiewicz wrote:
Hi
I think the problem is :
(fun (ixi : Sem.S.O.I.t * Sem.S.O.I.t) (s : Sem.S.t) =>
you rebind s, so it's not the same one!
Hope this helps
Alexandre
2010/10/1 M. Scott
Doerrie<mdoerri AT cs.jhu.edu>:
Adam Chlipala wrote:
M. Scott Doerrie wrote:Well, this handwriting the term Checks as type Prop. Still working the pl2
Why won't "rewrite Hopt2 in Hopt6" work. It fails with: Found no subtermAssuming that you've eyeballed the code properly and checked that the
matching "Sem.S.RefMapS.find a s" in Hopt6. It's clearly present, even when
using "Set Printing All."
terms really match (which I haven't done), the problem could be that [Hopt6]
would no longer be well-typed after the rewrite. I suggest running [Check
P], where [P] is a hand-rewritten version of the term. If this fails, then
you'll have the culprit. The [rewrite] error message for cases like this
could definitely be improved. ;)
upgrade angle.
Check @eq (option Sem.S.O.C.t)
(@option_map1 Sem.S.O.t (option Sem.S.O.C.t)
(fun o : Sem.S.O.t => Sem.SC.OC.getCap i_src o)
(@None Sem.S.O.C.t)
(@option_map
(prod
(prod
(prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t)
ObjectSchedules.ProjectedObjectSchedule.t)
(Sem.S.O.IndexMapS.t Sem.S.O.C.t) Sem.SC.tupleGetObj
(@Sem.S.RefMapS.find
(prod
(prod
(prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t)
ObjectSchedules.ProjectedObjectSchedule.t) a
(@fold_right Sem.S.t (prod Sem.S.O.I.t Sem.S.O.I.t)
(fun (ixi : prod Sem.S.O.I.t Sem.S.O.I.t)
(s : Sem.S.t) =>
@option_map1 Sem.S.O.C.t Sem.S.t
(fun cap : Sem.S.O.C.t =>
Sem.SC.addCap (@snd Sem.S.O.I.t Sem.S.O.I.t ixi)
cap (Sem.S.O.C.target invoked_cap) s) s
(@option_map1 Sem.S.O.t
(option Sem.S.O.C.t)
(fun o : Sem.S.O.t =>
Sem.SC.OC.getCap
(@fst Sem.S.O.I.t Sem.S.O.I.t ixi) o)
(@None Sem.S.O.C.t)
(@option_map
(prod
(prod
(prod
(Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t)
ObjectSchedules.ProjectedObjectSchedule.t)
(Sem.S.O.IndexMapS.t Sem.S.O.C.t)
Sem.SC.tupleGetObj
(@Some
(prod
(prod
(prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t)
ObjectSchedules.ProjectedObjectSchedule.t)
(@pair
(prod
(prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t)
ObjectSchedules.ProjectedObjectSchedule.t
(@pair
(prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t)
ObjectTypes.ProjectedObjectType.t
(@pair (Sem.S.O.IndexMapS.t
Sem.S.O.C.t)
ObjectLabels.ProjectedObjectLabel.t
actor actor_lbl)
actor_type) actor_sched)))))
(@option_map1 Sem.S.O.I.t Sem.S.t
(fun i : Sem.S.O.I.t =>
Sem.SC.addCap i
(Sem.S.O.C.mkCap a
(AccessRights.AccessRightFSet.singleton
AccessRights.send))
(Sem.S.O.C.target invoked_cap) s) s opt_i)
ixi_list)))) (@Some Sem.S.O.C.t t_cap).
Michael Doerrie
- [Coq-Club] rewrite problem, M. Scott Doerrie
- Re: [Coq-Club] rewrite problem,
Adam Chlipala
- Re: [Coq-Club] rewrite problem,
M. Scott Doerrie
- Re: [Coq-Club] rewrite problem,
Alexandre Pilkiewicz
- Re: [Coq-Club] rewrite problem, M. Scott Doerrie
- Re: [Coq-Club] rewrite problem, Alexandre Pilkiewicz
- Re: [Coq-Club] rewrite problem, M. Scott Doerrie
- Re: [Coq-Club] rewrite problem,
Alexandre Pilkiewicz
- Re: [Coq-Club] rewrite problem,
M. Scott Doerrie
- Re: [Coq-Club] rewrite problem,
Adam Chlipala
Archive powered by MhonArc 2.6.16.