Changeset 1056 for src/RTLabs


Ignore:
Timestamp:
Jul 5, 2011, 4:25:41 PM (8 years ago)
Author:
campbell
Message:

Switch to delayed identifier error scheme.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r898 r1056  
    22include "RTLabs/semantics.ma".
    33
    4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝
     4let rec n_idents (n:nat) (tag:String) (g:universe tag) : Vector (identifier tag) n × (universe tag) ≝
    55match n with
    6 [ O ⇒ OK ? 〈[[ ]], g〉
    7 | S m ⇒ do 〈ls, g'〉 ← n_idents m tag g;
    8         do 〈l, g''〉 ← fresh ? g';
    9         OK ? 〈l:::ls, g''〉
     6[ O ⇒ 〈[[ ]], g〉
     7| S m ⇒ let 〈ls, g'〉 ≝ n_idents m tag g in
     8        let 〈l, g''〉 ≝ fresh ? g' in
     9        〈l:::ls, g''〉
    1010].
    1111
     
    2424definition make_register :
    2525  (pre_register → option register) → pre_register → universe RegisterTag →
    26   res ((nat → option register) × (universe RegisterTag) × register)
     26  (nat → option register) × (universe RegisterTag) × register
    2727λm,reg,g.
    2828  match m reg with
    29   [ Some r' ⇒ OK ? 〈〈m,g〉,r'〉
    30   | None ⇒ do 〈r',g'〉 ← fresh ? g;
    31            OK ? 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     29  [ Some r' ⇒ 〈〈m,g〉,r'〉
     30  | None ⇒ let 〈r',g'〉 ≝ fresh ? g in
     31             〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
    3232  ]
    3333.
     
    3535definition make_registers_list :
    3636  (nat → option register) → list (pre_register × typ) → universe RegisterTag →
    37   res ((nat → option register) × (universe RegisterTag) × (list (register×typ))) ≝
     37    (nat → option register) × (universe RegisterTag) × (list (register×typ)) ≝
    3838λm,lrs,g.
    39 foldr ?? (λrst,acc. do 〈acc',l〉 ← acc;
    40                    let 〈rs,ty〉 ≝ rst in
    41                    let 〈m,g〉 ≝ acc' in
    42                    do 〈mg,rs'〉 ← make_register m rs g;
    43                    OK ? 〈mg,〈rs',ty〉::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
     39foldr ?? (λrst,acc. let 〈acc',l〉 ≝ acc in
     40                    let 〈rs,ty〉 ≝ rst in
     41                    let 〈m,g〉 ≝ acc' in
     42                    let 〈mg,rs'〉 ≝ make_register m rs g in
     43                      〈mg,〈rs',ty〉::l〉) 〈〈m,g〉,[ ]〉 lrs.
    4444
    4545axiom MissingRegister : String.
    4646axiom MissingLabel : String.
    4747
     48(* Doesn't check for identifier overflow, but don't really need to care here. *)
    4849definition make_internal_function : pre_internal_function → res (fundef internal_function) ≝
    4950λpre_f.
    5051  let rgen0 ≝ new_universe RegisterTag in
    51   do 〈rmapgen1, result〉 ← match pf_result pre_f with
    52                           [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
    53                           | Some rt ⇒ do 〈x,y〉 ← make_register (λ_.None ?) (\fst rt) rgen0; OK ? 〈x,Some ? 〈y,\snd rt〉〉
    54                           ];
     52  let 〈rmapgen1, result〉 ≝ match pf_result pre_f with
     53                           [ None ⇒ 〈〈λ_.None ?, rgen0〉, None ?〉
     54                           | Some rt ⇒ let 〈x,y〉 ≝ make_register (λ_.None ?) (\fst rt) rgen0 in 〈x,Some ? 〈y,\snd rt〉〉
     55                           ] in
    5556  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
    56   do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
     57  let 〈rmapgen2, params〉 ≝ make_registers_list rmap1 (pf_params pre_f) rgen1 in
    5758  let 〈rmap2, rgen2〉 ≝ rmapgen2 in
    58   do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
     59  let 〈rmapgen3, locals〉 ≝ make_registers_list rmap2 (pf_locals pre_f) rgen2 in
    5960  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
    6061  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
    6162  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    62   do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
     63  let 〈labels, gen〉 ≝ n_idents (S max_stmt) ? (new_universe LabelTag) in
    6364  let get_label ≝ λn. opt_to_res … (msg MissingLabel) (get_index_weak_v ?? labels n) in
    6465  do graph ← foldr ?? (λp:nat × ((pre_register → res register) → (nat → res label) → res statement).λg0.
  • src/RTLabs/syntax.ma

    r1051 r1056  
    1313| St_skip : label → statement
    1414| St_cost : costlabel → label → statement
    15 | St_const : register → cast → label → statement
     15| St_const : register → constant → label → statement
    1616| St_op1 : unary_operation → register → register → label → statement
    1717| St_op2 : binary_operation → register → register → register → label → statement
Note: See TracChangeset for help on using the changeset viewer.