Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rewrite problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewrite problem


chronological Thread 
  • 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
>




Archive powered by MhonArc 2.6.16.

Top of Page