Changeset 2795

Timestamp:

Mar 7, 2013, 9:31:40 AM (8 years ago)

Author:

sacerdot

Message:

Added new function Measurable.observe_all_in_measurable to be used to
debug the extracted code. It takes a classified system, a state, a number s
(that in the extracted code can be a lazy infinite value) and it computes
the stream of intensional observables from that state.

Location:

src/common

Files:

• ErrorMessages.ma (modified) (1 diff)
• Measurable.ma (modified) (1 diff)

src/common/ErrorMessages.ma

@@ -69 +69 @@
  | TerminatedEarly : ErrorMessage
  | BadCostLabelling : ErrorMessage
- | RepeatedCostLabel : ErrorMessage.
+ | RepeatedCostLabel : ErrorMessage
+ | NotTerminated : ErrorMessage.

src/common/Measurable.ma

@@ -400 +400 @@
   return 〈prefix', \snd (intensional_trace_of_trace C' cs interesting)〉.
 
+(* CSC: Main debug function for the extracted code.
+   It returns the list of all observed states and their observables,
+   the last state and the reason for stopping execution. If the last
+   state is final, it also returns the exit value. *)
+let rec observe_all_in_measurable (n:nat) (fx:classified_system)
+ (observe: intensional_event → unit) (callstack: list ident)
+ (s:state … fx (cs_global fx)) :
+ list intensional_event × (res int) ≝
+match n with
+[ O ⇒
+  let res ≝
+   match is_final … fx (cs_global … fx) s with
+   [ Some r ⇒ OK … r
+   | None ⇒ Error … (msg NotTerminated) ]
+  in
+   〈[ ],res〉
+| S m ⇒
+  match is_final … fx (cs_global … fx) s with
+  [ Some r ⇒ 〈[ ],OK … r〉
+  | None ⇒
+    match step … fx (cs_global … fx) s with
+    [ Value trs ⇒
+        let costevents ≝ flatten ? (map … intensional_event_of_event (\fst trs)) in
+        let 〈callstack,callevent〉 ≝
+         match cs_classify fx s
+         return λy. (match y with [cl_call ⇒ True | _ ⇒ False] → ident) →
+                 list ident × (list intensional_event)
+         with
+         [ cl_call ⇒
+            λcallee. let id ≝ callee I in
+            〈id::callstack,[IEVcall id]〉
+         | cl_return ⇒ λ_.
+            match callstack with
+            [ nil ⇒ 〈[ ],[ ]〉
+            | cons id tl ⇒ 〈tl,[IEVret id]〉]
+         | _ ⇒ λ_. 〈callstack, [ ]〉
+         ] (cs_callee fx s) in
+        let events ≝ costevents@callevent in
+        let dummy : list unit ≝ map ?? observe events in
+        let 〈tl,res〉 ≝
+         observe_all_in_measurable m fx observe callstack (\snd trs) in
+         〈events@tl,res〉
+    | Interact _ _ ⇒ 〈[ ],Error … (msg UnexpectedIO)〉
+    | Wrong m ⇒ 〈[ ],Error … m〉
+    ]
+  ]
+].