| 1 | include "basics/lists/list.ma". |
|---|
| 2 | include "joint/joint_semantics.ma". |
|---|
| 3 | include "common/Executions.ma". |
|---|
| 4 | include "common/StructuredTraces.ma". |
|---|
| 5 | |
|---|
| 6 | inductive call_ud (p: params) (globals: list ident): Type [0] ≝ |
|---|
| 7 | | up: joint_internal_function p globals → call_ud p globals (* call *) |
|---|
| 8 | | down: joint_internal_function p globals → call_ud p globals. (* return *) |
|---|
| 9 | |
|---|
| 10 | let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g)) |
|---|
| 11 | (curr: nat) (max: nat) on fn_list: nat ≝ |
|---|
| 12 | match fn_list with |
|---|
| 13 | [ nil ⇒ max |
|---|
| 14 | | cons h t ⇒ match h with |
|---|
| 15 | [ up f ⇒ let new_stack ≝ curr + joint_if_stacksize … f in |
|---|
| 16 | if leb max new_stack |
|---|
| 17 | then max_stacksize … t new_stack new_stack |
|---|
| 18 | else max_stacksize … t new_stack max |
|---|
| 19 | | down f ⇒ let new_stack ≝ curr - joint_if_stacksize … f in |
|---|
| 20 | max_stacksize … t new_stack max |
|---|
| 21 | ] |
|---|
| 22 | ]. |
|---|
| 23 | |
|---|
| 24 | let rec extract_list_from_tlr (p: params) (g: list ident) |
|---|
| 25 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 26 | (S: abstract_status) (s,s':S) (tr: trace_label_return S s s') |
|---|
| 27 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
|---|
| 28 | match tr with |
|---|
| 29 | [ tlr_base s1 s2 tll ⇒ |
|---|
| 30 | extract_list_from_tll … lg top_f … tll res |
|---|
| 31 | | tlr_step s1 s2 s3 tll tlr ⇒ |
|---|
| 32 | let res' ≝ extract_list_from_tll … lg top_f … tll res in |
|---|
| 33 | extract_list_from_tlr … lg top_f … tlr res' |
|---|
| 34 | ] |
|---|
| 35 | and extract_list_from_tll (p: params) (g: list ident) |
|---|
| 36 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 37 | (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s') |
|---|
| 38 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
|---|
| 39 | match tr with |
|---|
| 40 | [ tll_base ends s1 s2 tal co ⇒ |
|---|
| 41 | extract_list_from_tal … lg top_f … tal res |
|---|
| 42 | ] |
|---|
| 43 | and extract_list_from_tal (p: params) (g: list ident) |
|---|
| 44 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 45 | (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s') |
|---|
| 46 | (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ |
|---|
| 47 | match tr with |
|---|
| 48 | [ tal_base_not_return s1 s2 ex cl co ⇒ res |
|---|
| 49 | | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res |
|---|
| 50 | | tal_base_call s1p s1s s2 ex cl ar tlr co ⇒ |
|---|
| 51 | extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr |
|---|
| 52 | (up ?? (lg (as_call_ident ? «s1p,cl»))::res) |
|---|
| 53 | | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒ |
|---|
| 54 | extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr |
|---|
| 55 | (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res) |
|---|
| 56 | | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ |
|---|
| 57 | let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr |
|---|
| 58 | (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in |
|---|
| 59 | extract_list_from_tal … lg top_f … tal res' |
|---|
| 60 | | tal_step_default end s1p s1i s1e ex tal cl co ⇒ |
|---|
| 61 | extract_list_from_tal … lg top_f … tal res |
|---|
| 62 | ]. |
|---|
| 63 | |
|---|
| 64 | let rec tlr_rel_extract_equal (p: params) (g: list ident) |
|---|
| 65 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 66 | S1 S2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 67 | tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → |
|---|
| 68 | ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res = |
|---|
| 69 | extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ |
|---|
| 70 | match t1 with |
|---|
| 71 | [ tlr_base st1 st1' tll1 ⇒ ? |
|---|
| 72 | | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? |
|---|
| 73 | ] |
|---|
| 74 | and tll_rel_extract_equal (p: params) (g: list ident) |
|---|
| 75 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 76 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 77 | t1 ≈ t2 → |
|---|
| 78 | ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res = |
|---|
| 79 | extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝ |
|---|
| 80 | match t1 with |
|---|
| 81 | [ tll_base ends st1 st1' tal1 co ⇒ ? |
|---|
| 82 | ] |
|---|
| 83 | and tal_rel_extract_equal (p: params) (g: list ident) |
|---|
| 84 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 85 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 86 | t1 ≈ t2 → |
|---|
| 87 | ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res = |
|---|
| 88 | extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝ |
|---|
| 89 | match t1 with |
|---|
| 90 | [ tal_base_not_return st1 st1' ex cl co ⇒ ? |
|---|
| 91 | | tal_base_return st1 st1' ex cl ⇒ ? |
|---|
| 92 | | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? |
|---|
| 93 | | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? |
|---|
| 94 | | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? |
|---|
| 95 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
|---|
| 96 | ]. |
|---|
| 97 | [ cases t2 |
|---|
| 98 | [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim) |
|---|
| 99 | | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs |
|---|
| 100 | ] |
|---|
| 101 | | cases t2 |
|---|
| 102 | [ #st2 #st2' #tll2 normalize #abs cases abs |
|---|
| 103 | | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res |
|---|
| 104 | >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res) |
|---|
| 105 | @(tlr_rel_extract_equal … (proj2 ?? Hsim)) |
|---|
| 106 | ] |
|---|
| 107 | | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2 |
|---|
| 108 | @(tal_rel_extract_equal … H2) |
|---|
| 109 | | cases t2 |
|---|
| 110 | [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % |
|---|
| 111 | | #st2 #st2' #ex' #cl' * #abs destruct (abs) |
|---|
| 112 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid * |
|---|
| 113 | #taa * #H * #G * #K inversion taa in ⊢ ?; |
|---|
| 114 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 115 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 116 | normalize #abs destruct (abs) |
|---|
| 117 | ] |
|---|
| 118 | | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid * |
|---|
| 119 | #taa * #H * #G * #K inversion taa in ⊢ ?; |
|---|
| 120 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 121 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 122 | normalize #abs destruct (abs) |
|---|
| 123 | ] |
|---|
| 124 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize * |
|---|
| 125 | #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; |
|---|
| 126 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 127 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 128 | normalize #abs destruct (abs) |
|---|
| 129 | ] |
|---|
| 130 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa |
|---|
| 131 | * #H * #G * #K inversion taa in ⊢ ?; |
|---|
| 132 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 133 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 134 | destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *) |
|---|
| 135 | cases daemon |
|---|
| 136 | ] |
|---|
| 137 | ] |
|---|
| 138 | | cases t2 |
|---|
| 139 | [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) |
|---|
| 140 | | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % |
|---|
| 141 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) |
|---|
| 142 | | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs) |
|---|
| 143 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
|---|
| 144 | normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; |
|---|
| 145 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 146 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 147 | normalize #abs destruct (abs) |
|---|
| 148 | ] |
|---|
| 149 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid |
|---|
| 150 | * #taa * #H * #G inversion taa in ⊢ ?; |
|---|
| 151 | [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) |
|---|
| 152 | | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 153 | destruct normalize #Hsim destruct (Hsim) |
|---|
| 154 | cases daemon (* use Hind again? *) |
|---|
| 155 | ] |
|---|
| 156 | ] |
|---|
| 157 | | cases t2 |
|---|
| 158 | [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa |
|---|
| 159 | * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1 |
|---|
| 160 | [ * * #H3 #H2 #H4 | #H2 ] |
|---|
| 161 | inversion taa in ⊢ ?; |
|---|
| 162 | [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3) |
|---|
| 163 | | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 164 | normalize in H3; destruct (H3) |
|---|
| 165 | | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) |
|---|
| 166 | | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 167 | normalize in H1; destruct (H1) |
|---|
| 168 | ] |
|---|
| 169 | | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) |
|---|
| 170 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G |
|---|
| 171 | * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L |
|---|
| 172 | [* #tl2] |
|---|
| 173 | inversion taa in ⊢ ?; |
|---|
| 174 | [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
|---|
| 175 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 176 | destruct normalize * * #abs destruct (abs) |
|---|
| 177 | | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res |
|---|
| 178 | >(tlr_rel_extract_equal p g lg … H2) destruct (H1) |
|---|
| 179 | >ident_eq % |
|---|
| 180 | | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 181 | destruct normalize * #abs destruct (abs) |
|---|
| 182 | ] |
|---|
| 183 | | (* tail call case *) cases daemon |
|---|
| 184 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize |
|---|
| 185 | * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] |
|---|
| 186 | #K * #tlr2' * #L [* #tl2] |
|---|
| 187 | inversion taa in ⊢ ?; |
|---|
| 188 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res |
|---|
| 189 | destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq |
|---|
| 190 | (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by |
|---|
| 191 | * not sure yet *) cases daemon |
|---|
| 192 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 193 | destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq |
|---|
| 194 | >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *) |
|---|
| 195 | ] |
|---|
| 196 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * |
|---|
| 197 | #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L |
|---|
| 198 | [* #tl2] |
|---|
| 199 | inversion taa in ⊢ ?; |
|---|
| 200 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res |
|---|
| 201 | destruct (H1) |
|---|
| 202 | |2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 203 | destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq |
|---|
| 204 | >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *) |
|---|
| 205 | ] |
|---|
| 206 | ] |
|---|
| 207 | | (* tail call case *) cases daemon |
|---|
| 208 | | cases t2 |
|---|
| 209 | [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa * |
|---|
| 210 | #st2mid' * #H * * [#_ | #st2mid''] * #K * #tlr2 * #L [2: * #tl2] |
|---|
| 211 | inversion taa in ⊢ ?; |
|---|
| 212 | [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) |
|---|
| 213 | |2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 214 | destruct normalize * * #H1 destruct (H1) |
|---|
| 215 | ] |
|---|
| 216 | | #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' |
|---|
| 217 | * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2 |
|---|
| 218 | inversion taa in ⊢ ?; |
|---|
| 219 | [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
|---|
| 220 | | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct |
|---|
| 221 | normalize * * #abs destruct (abs) |
|---|
| 222 | ] |
|---|
| 223 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G * |
|---|
| 224 | #ident_eq * #taa * #st2mid' * #H * * [ #_ | #st2mid'' ] * #K * #tlr2' * #L |
|---|
| 225 | [2: * #tl2] |
|---|
| 226 | inversion taa in ⊢ ?; |
|---|
| 227 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res |
|---|
| 228 | destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3) |
|---|
| 229 | cases tal1 in H2; |
|---|
| 230 | [ #ss #sf #ex'' #cl'' #co'' normalize #_ % |
|---|
| 231 | | #ss #sf #ex'' #cl'' normalize #abs cases abs |
|---|
| 232 | | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs |
|---|
| 233 | | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs |
|---|
| 234 | | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1' |
|---|
| 235 | normalize #abs cases abs |
|---|
| 236 | | #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize |
|---|
| 237 | cases daemon (* use induction here, but no *) |
|---|
| 238 | ] |
|---|
| 239 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 240 | destruct normalize * * #abs destruct (abs) |
|---|
| 241 | ] |
|---|
| 242 | | (* tail call case *) cases daemon |
|---|
| 243 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
|---|
| 244 | normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * |
|---|
| 245 | [ #H1 | #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; |
|---|
| 246 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res |
|---|
| 247 | destruct (H1) >ident_eq >(tal_rel_extract_equal … H2) |
|---|
| 248 | >(tlr_rel_extract_equal … H3) % |
|---|
| 249 | |2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 250 | destruct normalize * * #abs destruct (abs) |
|---|
| 251 | ] |
|---|
| 252 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G * |
|---|
| 253 | #ident_eq * #taa * #st2mid' * #H * * [ #He | #st2mid'' ] * #K * #tlr2' * #L |
|---|
| 254 | [2: * #tl2] inversion taa in ⊢ ?; |
|---|
| 255 | [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) |
|---|
| 256 | |2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 |
|---|
| 257 | destruct normalize * * #H1 #H2 #H3 #res destruct (H1) |
|---|
| 258 | >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon |
|---|
| 259 | (* look further here *) |
|---|
| 260 | ] |
|---|
| 261 | ] |
|---|
| 262 | | cases t2 |
|---|
| 263 | [ #st2 #st2' #ex' #cl' #co' |
|---|
| 264 | | #ss #fs #ex' #cl' |
|---|
| 265 | | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' |
|---|
| 266 | | #st2p #st2s #st2' #ex' #cl' #tlr2 |
|---|
| 267 | | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 |
|---|
| 268 | | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' |
|---|
| 269 | ] |
|---|
| 270 | normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) |
|---|
| 271 | ] |
|---|
| 272 | (* Another tailcall case escaped *) cases daemon |
|---|
| 273 | qed. |
|---|
| 274 | |
|---|
| 275 | let rec tlr_rel_max_equal (p: params) (g: list ident) |
|---|
| 276 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 277 | S1 S2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 278 | tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → |
|---|
| 279 | max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = |
|---|
| 280 | max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ |
|---|
| 281 | match t1 with |
|---|
| 282 | [ tlr_base st1 st1' tll1 ⇒ ? |
|---|
| 283 | | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? |
|---|
| 284 | ] |
|---|
| 285 | and tll_rel_max_equal (p: params) (g: list ident) |
|---|
| 286 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 287 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 288 | t1 ≈ t2 → |
|---|
| 289 | max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = |
|---|
| 290 | max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
|---|
| 291 | match t1 with |
|---|
| 292 | [ tll_base ends st1 st1' tal1 co ⇒ ? |
|---|
| 293 | ] |
|---|
| 294 | and tal_rel_max_equal (p: params) (g: list ident) |
|---|
| 295 | (lg: ident → joint_internal_function p g) (top_f: ident) |
|---|
| 296 | S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: |
|---|
| 297 | t1 ≈ t2 → |
|---|
| 298 | max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = |
|---|
| 299 | max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ |
|---|
| 300 | match t1 with |
|---|
| 301 | [ tal_base_not_return st1 st1' ex cl co ⇒ ? |
|---|
| 302 | | tal_base_return st1 st1' ex cl ⇒ ? |
|---|
| 303 | | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? |
|---|
| 304 | | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? |
|---|
| 305 | | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? |
|---|
| 306 | | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? |
|---|
| 307 | ]. |
|---|
| 308 | [1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) % |
|---|
| 309 | |3: #Hsim >(tll_rel_extract_equal … Hsim []) % |
|---|
| 310 | |*: #Hsim >(tal_rel_extract_equal … Hsim []) % |
|---|
| 311 | ] |
|---|
| 312 | qed. |
|---|
