Changeset 2875 for src/ASM


Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret2.ma

    r2764 r2875  
    1717
    1818definition mk_fullexec_of_abstract_status:
    19  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
    20 ≝ λS,as_eval,as_init.
    21    mk_fullexec ?? unit (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
     19 ∀program: Type[0].
     20  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
     21≝ λprogram,S,as_eval,as_init.
     22   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
    2223    (λ_.return as_init).
    2324
    2425definition mk_preclassified_system_of_abstract_status:
    25  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
    26 ≝ λS,as_eval,as_init.
     26 ∀program: Type[0].
     27  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
     28≝ λprogram,S,as_eval,as_init.
    2729   mk_preclassified_system
    28     (mk_fullexec_of_abstract_status S as_eval as_init)
     30    (mk_fullexec_of_abstract_status program S as_eval as_init)
    2931    (λ_.λst. ¬(is_none … (as_label … st)))
    3032    (λ_.as_classify S)
     
    3941  let cm ≝ load_code_memory (oc c) in
    4042  mk_preclassified_system_of_abstract_status
     43   labelled_object_code
    4144   (ASM_abstract_status cm (costlabels c))
    4245   (λst. return (execute_1 … st))
Note: See TracChangeset for help on using the changeset viewer.