Ignore:
Timestamp:
Jan 24, 2013, 7:52:38 PM (7 years ago)
Author:
piccolo
Message:

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2541 r2590  
    458458  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
    459459  | pm_node o' l' r' ⇒
    460     pm_node ? (choice o o')
     460    match (choice o o') with 
     461    [None ⇒
     462      match (merge … choice l l') with
     463      [pm_leaf ⇒ match (merge … choice r r') with
     464          [pm_leaf ⇒ pm_leaf ?
     465          |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     466          ]
     467      |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
     468      ]
     469   |Some x ⇒
     470    pm_node ? (Some ? x)
    461471      (merge … choice l l')
    462472      (merge … choice r r')
    463473  ]
    464 ].
     474]].
    465475
    466476lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     
    470480 #A#B#C#choice#a elim a
    471481[ normalize #b
    472 | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
    473 ]
    474 #p#choice_good >lookup_opt_map
     482| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
     483  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
     484      normalize /2 by /
     485  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
     486      cases (merge A B C choice r r') normalize /2 by /
     487  ]
     488]]
     489#p #choice_good >lookup_opt_map
    475490elim (lookup_opt ???)
    476491normalize //
    477 qed.
     492qed. 
    478493
    479494let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
Note: See TracChangeset for help on using the changeset viewer.