Changeset 2645 for src/RTLabs/import.ma


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/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.