coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- To: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
- Cc: Adam Chlipala <adam AT chlipala.net>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] rewrite problem
- Date: Fri, 1 Oct 2010 17:59:04 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=kO2AYsYfYNpZEUiWOAMqGnb8d5NdgSWkW0CdDHwGyD3Y6zHlGub6OfFhaiKAWlA0p0 VLm9ZONQJEzTv/6pcku6B8+PVwBjpUPEB0hR0+2ACQhdgAjYEc3SlhW7zDZnQwx0luA5 /JgpuH59mKZqEZ8cpeAmy6diSaGfTZY6x/4Ms=
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:
>>>
>>> Why won't "rewrite Hopt2 in Hopt6" work. It fails with: Found no subterm
>>> matching "Sem.S.RefMapS.find a s" in Hopt6. It's clearly present, even
>>> when
>>> using "Set Printing All."
>>
>> Assuming that you've eyeballed the code properly and checked that the
>> 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. ;)
>
> Well, this handwriting the term Checks as type Prop. Still working the pl2
> 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.