Changeset 2661 for src

Timestamp:

Feb 12, 2013, 3:26:37 AM (7 years ago)

Author:

sacerdot

Message:

stacksize "repaired" by "considering" tailcalls
Some daemons added here and there since many are already in place.

Location:

src

Files:

• BACKEND_BROKEN_FILES (modified) (1 diff)
• joint/stacksize.ma (modified) (12 diffs)

src/BACKEND_BROKEN_FILES

@@ -4 +4 @@
   joint/lineariseProof.ma
   LTL/LTLToLIN.ma
-joint/stacksize.ma:               mancano tailcall
 
 LIN/joint_LTL_LIN_semantics.ma:   parametri

src/joint/stacksize.ma

@@ -51 +51 @@
     extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
       (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
+  | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒
+     extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr
+      (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res)
   | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 
     let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
@@ -88 +91 @@
   | tal_base_return st1 st1' ex cl ⇒ ?
   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
+  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
@@ -112 +116 @@
       normalize #abs destruct (abs)
     ]
+  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid *
+    #taa * #H * #G * #K inversion taa in ⊢ ?;
+    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 
+    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
+      normalize #abs destruct (abs)
+    ]
   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
     #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
@@ -130 +140 @@
   | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 
   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 
+  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs) 
   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
     normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
@@ -170 +181 @@
       destruct normalize * #abs destruct (abs)
     ]
+  | (* tail call case *) cases daemon
   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
     * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
@@ -192 +204 @@
       >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
     ]
-  ] 
+  ]
+| (* tail call case *) cases daemon 
 | cases t2
   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
@@ -218 +231 @@
       | #ss #sf #ex'' #cl'' normalize #abs cases abs
       | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
+      | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs
       | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
         normalize #abs cases abs
@@ -226 +240 @@
       destruct normalize * * #abs destruct (abs)
     ]
+  | (* tail call case *) cases daemon
   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
     normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
@@ -249 +264 @@
   | #ss #fs #ex' #cl'
   | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
+  | #st2p #st2s #st2' #ex' #cl' #tlr2
   | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' 
@@ -254 +270 @@
   normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 
 ]
+(* Another tailcall case escaped *) cases daemon
 qed.
 
@@ -285 +302 @@
   | tal_base_return st1 st1' ex cl ⇒ ?
   | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
+  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
   | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
@@ -292 +310 @@
 |*: #Hsim >(tal_rel_extract_equal … Hsim []) %
 ]
-qed. 
-     
-      
-      
-            
+qed.