Changeset 2590 for src/common/PositiveMap.ma

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:

• src/common/PositiveMap.ma (modified) (2 diffs)

src/common/PositiveMap.ma

@@ -458 +458 @@
   [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
   | pm_node o' l' r' ⇒
-    pm_node ? (choice o o') 
+    match (choice o o') with  
+    [None ⇒ 
+      match (merge … choice l l') with
+      [pm_leaf ⇒ match (merge … choice r r') with
+          [pm_leaf ⇒ pm_leaf ?
+          |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
+          ]
+      |_ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r')
+      ]
+   |Some x ⇒ 
+    pm_node ? (Some ? x) 
       (merge … choice l l')
       (merge … choice r r')
   ]
-].
+]].
 
 lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
@@ -470 +480 @@
  #A#B#C#choice#a elim a
 [ normalize #b
-| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
-]
-#p#choice_good >lookup_opt_map
+| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
+  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r') 
+      normalize /2 by /
+  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
+      cases (merge A B C choice r r') normalize /2 by /
+  ]
+]]
+#p #choice_good >lookup_opt_map
 elim (lookup_opt ???)
 normalize //
-qed.
+qed. 
 
 let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝