1 files changed, 88 insertions, 40 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index e7fc23e0a..40d5abca9 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -20,55 +20,101 @@ Module Type Expression.
   Parameter bits: nat.
   Parameter width: Width bits.
   Parameter inputs: nat.
+  Parameter inputBounds: list Z.
   Parameter ResultType: type.
-  Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType).
-  Parameter inputBounds: list (Range N).
+
+  Parameter prog: NAry inputs Z (@HL.Expr Z ResultType).
 End Expression.
 
 Module Pipeline (Input: Expression).
-  Export Input.
+  Definition bits := Input.bits.
+  Definition inputs := Input.inputs.
+  Definition ResultType := Input.ResultType.
+
+  Hint Unfold bits inputs ResultType.
+  Definition width: Width bits := Input.width.
+
+  Definition W: Type := word bits.
+  Definition R: Type := option RangeWithValue.
+  Definition B: Type := option (@BoundedWord bits).
+
+  Instance ZEvaluable : Evaluable Z := ZEvaluable.
+  Instance WEvaluable : Evaluable W := @WordEvaluable bits.
+  Instance REvaluable : Evaluable R := @RWVEvaluable bits.
+  Instance BEvaluable : Evaluable B := @BoundedEvaluable bits.
+
+  Existing Instances ZEvaluable WEvaluable REvaluable BEvaluable.
+
+  Module Util.
+    Fixpoint applyProgOn {A B k} (d: A) ins (f: NAry k A B): B :=
+      match k as k' return NAry k' A B -> B with
+      | O => id
+      | S m => fun f' =>
+        match ins with
+        | cons x xs => @applyProgOn A B m d xs (f' x)
+        | nil => @applyProgOn A B m d nil (f' d)
+        end
+      end f.
+  End Util.
+
+  Module HL.
+    Definition progZ: NAry inputs Z (@HL.Expr Z ResultType) :=
+      Input.prog.
+
+    Definition progR: NAry inputs Z (@HL.Expr R ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z R _ _ _ (x v)) Input.prog.
 
-  Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) :=
-    liftN CompileHL.compile hlProg.
+    Definition progW: NAry inputs Z (@HL.Expr W ResultType) :=
+      liftN (fun x v => @HLConversions.convertExpr Z W _ _ _ (x v)) Input.prog.
+  End HL.
 
-  Definition wordProg: NAry inputs (@CompileLL.WArg bits TT) (@LL.expr _ _ ResultType) :=
-    NArgMap (fun x => Z.of_N (wordToN (LL.interp_arg (t := TT) x))) (
-      liftN (LLConversions.convertZToWord bits) llProg).
+  Module LL.
+    Definition progZ: NAry inputs Z (@LL.expr Z Z ResultType) :=
+      liftN CompileHL.Compile HL.progZ.
 
-  Definition qhasmProg := CompileLL.compile (w := width) wordProg.
+    Definition progR: NAry inputs Z (@LL.expr R R ResultType) :=
+      liftN CompileHL.Compile HL.progR.
 
-  Definition qhasmString : option string :=
-    match qhasmProg with
-    | Some (p, _) => StringConversion.convertProgram p
-    | None => None
-    end.
+    Definition progW: NAry inputs Z (@LL.expr W W ResultType) :=
+      liftN CompileHL.Compile HL.progW.
+  End LL.
 
-  Import LLConversions.
+  Module AST.
+    Definition progZ: NAry inputs Z (@interp_type Z ResultType) :=
+      liftN LL.interp LL.progZ.
 
-  Definition RWV: Type := option RangeWithValue.
+    Definition progR: NAry inputs Z (@interp_type R ResultType) :=
+      liftN LL.interp LL.progR.
 
-  Definition rwvProg: NAry inputs RWV (@LL.expr RWV RWV ResultType) :=
-    NArgMap (fun x => orElse 0%Z (option_map (fun v => Z.of_N (value v)) x) ) (
-      liftN (@convertExpr Z RWV ZEvaluable (RWVEval (n := bits)) _) llProg).
+    Definition progW: NAry inputs Z (@interp_type W ResultType) :=
+      liftN LL.interp LL.progW.
+  End AST.
 
-  Fixpoint applyProgOn {A B k} ins (f: NAry k (option A) B): B :=
-    match k as k' return NAry k' (option A) B -> B with
-    | O => id
-    | S m => fun f' =>
-      match ins with
-      | cons x xs => @applyProgOn A B m xs (f' x)
-      | nil => @applyProgOn A B m nil (f' None)
-      end
-    end f.
+  Module Qhasm.
+    Definition pair :=
+      @CompileLL.compile bits width ResultType _ LL.progW.
 
-  Definition outputBounds :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-      liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e))
-        rwvProg).
+    Definition prog := option_map (@fst _ _) pair.
 
-  Definition valid :=
-    applyProgOn (map (@Some _) (map from_range inputBounds)) (
-     liftN (@check bits _ RWV (@RWVEval bits)) rwvProg).
+    Definition outputRegisters := option_map (@snd _ _) pair.
+
+    Definition code := option_map StringConversion.convertProgram prog.
+  End Qhasm.
+
+  Module Bounds.
+    Definition input := map (fun x => range N 0%N (Z.to_N x)) Input.inputBounds.
+
+    Definition upper := Z.of_N (wordToN (wones bits)).
+
+    Definition prog :=
+      Util.applyProgOn upper Input.inputBounds LL.progR.
+
+    Definition valid := LLConversions.check (n := bits) (f := id) prog.
+
+    Definition output :=
+      typeMap (option_map (fun x => range N (rwv_low x) (rwv_high x)))
+              (LL.interp prog).
+  End Bounds.
 End Pipeline.
 
 Module SimpleExample.
@@ -80,13 +126,15 @@ Module SimpleExample.
     Definition inputs: nat := 1.
     Definition ResultType := TT.
 
-    Definition hlProg: NAry 1 Z (@HL.expr Z (@LL.arg Z Z) TT) :=
-        Eval vm_compute in (fun x => HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)).
+    Definition inputBounds: list Z := [ (2^30)%Z ].
 
-    Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ].
+    Existing Instance ZEvaluable.
+
+    Definition prog: NAry 1 Z (@HL.Expr Z TT).
+      intros x var.
+      refine (HL.Binop OPadd (HL.Const x) (HL.Const 5%Z)).
+    Defined.
   End SimpleExpression.
 
   Module SimplePipeline := Pipeline SimpleExpression.
-
-  Export SimplePipeline.
 End SimpleExample.