Changeset 2645 for src/RTLabs


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_semantics.ma

    r2608 r2645  
    5959  update RegisterTag val locals reg v.
    6060
    61 axiom WrongNumberOfParameters : String.
    62 
    6361let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    6462match rs with
     
    7068] ].
    7169
    72 axiom BadRegister : String.
    7370
    7471definition reg_retrieve : register_env ? → register → res val ≝
    7572λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    76 
    77 axiom FailedOp : String.
    78 axiom MissingSymbol : String.
    79 
    80 axiom MissingStatement : String.
    81 axiom FailedConstant : String.
    82 axiom FailedLoad : String.
    83 axiom FailedStore : String.
    84 axiom BadFunction : String.
    85 axiom BadJumpTable : String.
    86 axiom BadJumpValue : String.
    87 axiom FinalState : String.
    88 axiom ReturnMismatch : String.
    8973
    9074definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
  • src/RTLabs/import.ma

    r2601 r2645  
    22include "RTLabs/RTLabs_semantics.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
     4let rec n_idents (n:nat) (tag:identifierTag) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
    55match n with
    66[ O ⇒ 〈[[ ]], g〉
     
    4242                    let 〈mg,rs'〉 ≝ make_register m rs ty g in
    4343                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    44 
    45 axiom MissingRegister : String.
    46 axiom MissingLabel : String.
    4744
    4845(* Doesn't check for identifier overflow, but don't really need to care here. *)
     
    124121.
    125122
    126 axiom TypeMismatch : String.
    127 
    128123(* duplicated from Clight/toCminor.ma. *)
    129124definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
Note: See TracChangeset for help on using the changeset viewer.