Changeset 797 for src/RTLabs/import.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/RTLabs/import.ma

    r765 r797  
    4949                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    5050
     51axiom MissingRegister : String.
     52axiom MissingLabel : String.
     53
    5154definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
    5255λpre_f.
     
    6366  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
    6467  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
    65   let rmap ≝ λn. opt_to_res … (rmap4 n) in
     68  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap4 n) in
    6669  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    6770  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
    68   let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
     71  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    6972  do graph ← foldr ?? (λp,g0. do g ← g0;
    7073                              let 〈l,s〉 ≝ p in
Note: See TracChangeset for help on using the changeset viewer.