Skip to Content.
Sympa Menu

coq-club - [Coq-Club] rewrite problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] rewrite problem


chronological Thread 
  • From: "M. Scott Doerrie" <mdoerri AT cs.jhu.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] rewrite problem
  • Date: Thu, 30 Sep 2010 18:22:22 -0400

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."  I'm running 8.2pl1.  Assuming that upgrading to 8.2pl2 doesn't fix the problem, what am I missing?

Relevant Hyps...

Hopt2 : Sem.S.RefMapS.find a s =
          Some (actor, actor_lbl, actor_type, actor_sched)

Hopt6 : option_map1 (fun o : Sem.S.O.t => Sem.SC.OC.getCap i_src o) None
            (option_map Sem.SC.tupleGetObj
               (Sem.S.RefMapS.find a
                  (fold_right
                     (fun (ixi : Sem.S.O.I.t * Sem.S.O.I.t) (s : Sem.S.t) =>
                      option_map1
                        (fun cap : Sem.S.O.C.t =>
                         Sem.SC.addCap (snd ixi) cap
                           (Sem.S.O.C.target invoked_cap) s) s
                        (option_map1
                           (fun o : Sem.S.O.t => Sem.SC.OC.getCap (fst ixi) o)
                           None
                           (option_map Sem.SC.tupleGetObj
                              (Sem.S.RefMapS.find a s))))
                     (option_map1
                        (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 t_cap

Yes, I used Set Printing All.  For those that want it. 

Here the error was:
Found no subterm matching "@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
                             s" in Hopt6.

  Hopt2 : @eq
            (option
               (prod
                  (prod
                     (prod (Sem.S.O.IndexMapS.t Sem.S.O.C.t)
                        ObjectLabels.ProjectedObjectLabel.t)
                     ObjectTypes.ProjectedObjectType.t)
                  ObjectSchedules.ProjectedObjectSchedule.t))
            (@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 s)

            (@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)

Hopt6 : @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
                                 (@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 s)
)))
                        (@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)

Scott Doerrie



Archive powered by MhonArc 2.6.16.

Top of Page