source: src/joint/Traces.ma @ 2286

Last change on this file since 2286 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 2.2 KB
Line 
1include "joint/semantics.ma".
2
3record evaluation_params : Type[1] ≝
4 { globals: list ident
5 ; sparams:> sem_params
6 ; exit: cpointer
7 ; ev_genv: genv sparams globals
8 ; io_env : state sparams → ∀o:io_out.res (io_in o)
9 } .
10
11(*record classifier_params : Type[1] ≝
12  { cl_pars :> evaluation_parameters
13  ; cl_ext_step : ext_step cl_pars → status_class
14  ; cl_ext_fin_stmt : ext_fin_stmt cl_pars → status_class
15  }.*)
16
17
18definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
19*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
20[ #EQ destruct % #H %
21| * #NEQ % #ABS destruct elim (NEQ ?) %
22]
23qed.
24
25let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
26  match c with
27  [ Value x ⇒ OK … x
28  | Interact o f ⇒
29    ! i ← env o ;
30    io_evaluate O I X env (f i)
31  | Wrong e ⇒ Error … e
32  ].
33
34definition cost_label_of_stmt :
35  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
36  λp,s.match s with
37  [ sequential s _ ⇒
38    match s with
39    [ step_seq s ⇒
40      match s with
41      [ COST_LABEL lbl ⇒ Some ? lbl
42      | _ ⇒ None ?
43      ]
44    | _ ⇒ None ?
45    ]
46  | _ ⇒ None ?
47  ].
48
49definition joint_abstract_status :
50 ∀p : evaluation_params.
51 abstract_status ≝
52 λp.
53 mk_abstract_status
54   (* as_status ≝ *) (state_pc p)
55   (* as_execute ≝ *)
56    (λs1,s2.io_evaluate … (io_env p s1) (eval_state … p (ev_genv p) s1) = return s2)
57   (* as_pc ≝ *) cpointerDeq
58   (* as_pc_of ≝ *) (pc …)
59   (* as_classifier ≝ *)
60    (λs,cl.∃fn,stmt.fetch_statement ? p … (ev_genv p) (pc … s) = return 〈fn,stmt〉 ∧
61     stmt_classifier … stmt = cl)
62   (* as_label_of_pc ≝ *)
63    (λpc.
64      match fetch_statement ? p … (ev_genv p) pc with
65      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
66      | _ ⇒ None ?
67      ])
68   (* as_after_return ≝ *)
69    (λs1,s2.
70      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
71      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
72      succ_pc p p (pc … s1) nxt = return pc … s2)
73   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?).
Note: See TracBrowser for help on using the repository browser.