Changeset 1515 for src/LTL


Ignore:
Timestamp:
Nov 18, 2011, 1:03:14 PM (8 years ago)
Author:
campbell
Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1379 r1515  
    2020let rec visit
    2121  (globals: list ident) (g: label → option (ltl_statement globals))
    22   (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     22  (required: identifier_set LabelTag) (visited: identifier_set LabelTag)
    2323  (generated: list (lin_statement globals)) (l: label) (n: nat)
    24     on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
     24    on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
    2525  match n with
    2626  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    2727  | S n' ⇒
    28     if set_member … (word_of_identifier … l) visited then
    29      〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
     28    if mem_set … visited l then
     29     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
    31      let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
    32      match g (an_identifier LabelTag (word_of_identifier … l)) with
     31     let visited' ≝ add_set ? visited l in
     32     match g l with
    3333     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
    3434     | Some statement ⇒
     
    4141            let 〈required', generated''〉 ≝
    4242             visit globals g required visited' generated' l2 n' in
    43             let required'' ≝ set_insert ? (word_of_identifier ? l1) required' in
    44              if set_member … (word_of_identifier … l1) visited' then
     43            let required'' ≝ add_set ? required' l1 in
     44             if mem_set … visited' l1 then
    4545               〈required', generated''〉
    4646             else
     
    6262 λglobals,entry,labels_upper_bound,g.
    6363  let g ≝ branch_compress ? g in
    64   let visited ≝ set_empty ? in
    65   let required ≝ set_insert ? (word_of_identifier … entry) (set_empty ?) in
     64  let visited ≝ in
     65  let required ≝ { (entry) } in
    6666  let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
    6767  let reversed ≝ rev ? translated in
     
    7171       [ None ⇒ 〈None …,x〉
    7272       | Some l ⇒
    73           〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
     73          〈if mem_set … required' l then Some ? l else None ?,
    7474           x〉])
    7575    reversed.
     
    8383  mk_joint_internal_function globals (lin_params globals)
    8484   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    85     (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
     85    (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f)))
    8686     (lookup ?? (joint_if_code … f)))
    8787    ??.
Note: See TracChangeset for help on using the changeset viewer.