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: [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 |
- [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.