From 91664481b4d43821ec8942cc9967837b8d7cc26f Mon Sep 17 00:00:00 2001
From: Robert Sloan <varomodt@gmail.com>
Date: Wed, 25 May 2016 17:53:35 -0400
Subject: MedialConversions done

---
 src/Assembly/PipelineExample.v | 29 +++++++++++------------------
 1 file changed, 11 insertions(+), 18 deletions(-)

(limited to 'src/Assembly')

diff --git a/src/Assembly/PipelineExample.v b/src/Assembly/PipelineExample.v
index 7afb3facb..d4cd4d142 100644
--- a/src/Assembly/PipelineExample.v
+++ b/src/Assembly/PipelineExample.v
@@ -12,6 +12,12 @@ Module Progs.
 
   Import C64.P.
 
+  Definition omap {A B} (f: A -> option B) (x: option A): option B :=
+    match x with
+    | Some v => f v
+    | None => None
+    end.
+
   Definition prog0: C64.P.Program.
     refine
       (PBin _ IPlus (PComb _ _ _
@@ -23,28 +29,15 @@ Module Progs.
     C64.PseudoConversion.convertProgram prog0.
 
   Definition prog2: option AlmostQhasm.Program :=
-    match prog1 with
-    | Some p => C64.MedialConversion.convertProgram p
-    | None => None
-    end.
+    omap C64.MedialConversion.convertProgram prog1.
 
   Definition prog3: option Qhasm.Program :=
-    match prog2 with
-    | Some p => AlmostConversion.convertProgram p
-    | None => None
-    end.
+    omap AlmostConversion.convertProgram prog2.
 
-  Definition prog4: string :=
-    match prog3 with
-    | Some p =>
-        match (StringConversion.convertProgram p) with
-        | Some s => s
-        | None => EmptyString
-        end
-    | None => EmptyString
-    end.
+  Definition prog4: option string :=
+    omap StringConversion.convertProgram prog3.
 
-  Definition result: string.
+  Definition result: option string.
     let res := eval vm_compute in prog4 in exact res.
   Defined.
 
-- 
cgit v1.2.3