Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (8 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
File:
1 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) ≝
Note: See TracChangeset for help on using the changeset viewer.