Changeset 797 for src/common/Values.ma


Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r751 r797  
    156156
    157157notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
    158 
     158(*
    159159let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
    160160match m return λx.res (x = n) with
     
    212212].
    213213   
    214 
     214*)
    215215(*
    216216(** The module [Val] defines a number of arithmetic and logical operations
     
    266266      ∀r. bool_of_val (Vnull r) true.
    267267
     268axiom ValueNotABoolean : String.
     269
    268270definition eval_bool_of_val : val → res bool ≝
    269271λv. match v with
     
    271273| Vnull _ ⇒ OK ? false
    272274| Vptr _ _ _ _ ⇒ OK ? true
    273 | _ ⇒ Error ?
     275| _ ⇒ Error ? (msg ValueNotABoolean)
    274276].
    275277
Note: See TracChangeset for help on using the changeset viewer.