diff options
author | Robert Sloan <varomodt@google.com> | 2016-10-21 11:04:03 -0700 |
---|---|---|
committer | Robert Sloan <varomodt@google.com> | 2016-10-21 11:04:03 -0700 |
commit | cd5c85c08274b6d3cbb646247c3017c1639944e2 (patch) | |
tree | e3f4cbdcf8c99c33886b56bf706662fa7492cddd /src/Assembly/Pipeline.v | |
parent | ff878dbde61374e42235b10d85c5fec2ab22e7d1 (diff) |
committing unstable refactors to patch master
Diffstat (limited to 'src/Assembly/Pipeline.v')
-rw-r--r-- | src/Assembly/Pipeline.v | 81 |
1 files changed, 54 insertions, 27 deletions
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v index e7fc23e0a..472162716 100644 --- a/src/Assembly/Pipeline.v +++ b/src/Assembly/Pipeline.v @@ -21,19 +21,34 @@ Module Type Expression. Parameter width: Width bits. Parameter inputs: nat. Parameter ResultType: type. - Parameter hlProg: NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType). - Parameter inputBounds: list (Range N). + Parameter hlProg: NAry inputs Z (@HL.expr Z (@interp_type Z) ResultType). + Parameter inputBounds: list Z. End Expression. Module Pipeline (Input: Expression). Export Input. + Module Util. + 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. + End Util. + + Definition hlProg': NAry inputs Z (@HL.expr Z (@LL.arg Z Z) ResultType) := + liftN (HLConversions.mapVar (fun t => @LL.uninterp_arg_as_var _ _ t) + (fun t => @LL.interp_arg _ t)) hlProg. + Definition llProg: NAry inputs Z (@LL.expr Z Z ResultType) := - liftN CompileHL.compile hlProg. + liftN CompileHL.compile hlProg'. - 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). + Definition wordProg: NAry inputs Z (@CompileLL.WExpr bits ResultType) := + liftN (LLConversions.ZToWord (n := bits) Z) llProg. Definition qhasmProg := CompileLL.compile (w := width) wordProg. @@ -47,28 +62,22 @@ Module Pipeline (Input: Expression). Definition RWV: Type := option RangeWithValue. - 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). + Instance RWVEvaluable : Evaluable RWV := @RWVEvaluable bits. + + Existing Instance RWVEvaluable. - 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. + Definition rwvProg: @LL.expr RWV Z ResultType := + Util.applyProgOn (map (@Some _) inputBounds) ( + NArgMap (orElse 0%Z) ( + liftN (@convertExpr Z RWV (@ZEvaluable bits) _ _ _) + llProg)). Definition outputBounds := - applyProgOn (map (@Some _) (map from_range inputBounds)) ( - liftN (fun e => typeMap (option_map proj) (@LL.interp RWV (@RWVEval bits) _ e)) - rwvProg). + typeMap (option_map rwvToRange) ( + LL.interp' (fun x => Some (rwv 0%N (Z.to_N x) (Z.to_N x))) ( + rwvProg)). - Definition valid := - applyProgOn (map (@Some _) (map from_range inputBounds)) ( - liftN (@check bits _ RWV (@RWVEval bits)) rwvProg). + Definition valid := check (n := bits) rwvProg. End Pipeline. Module SimpleExample. @@ -80,13 +89,31 @@ 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 hlProg: NAry 1 Z (@HL.expr Z (@interp_type Z) TT) := + Eval vm_compute in (fun x => HL.Binop OPadd (HL.Var x) (HL.Const 5%Z)). - Definition inputBounds: list (Range N) := [ range N 0%N (Npow2 31) ]. + Definition inputBounds: list Z := [ (2^30)%Z ]. End SimpleExpression. Module SimplePipeline := Pipeline SimpleExpression. Export SimplePipeline. End SimpleExample. + +Eval cbv in SimpleExample.SimplePipeline.hlProg'. +Eval cbv in SimpleExample.SimplePipeline.llProg. +Eval cbv in (liftN (LL.interp' (fun x => NToWord 32 (Z.to_N x))) SimpleExample.SimplePipeline.wordProg). +Opaque toT fromT LLConversions.convertArg. +Arguments LLConversions.convertArg _ _ _ _ _ _ _ : clear implicits. +Eval cbn in SimpleExample.SimplePipeline.rwvProg. +Eval cbn in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg). + +Transparent toT fromT LLConversions.convertArg. +Eval cbv in (LL.interp' (fun x => Some (rwv 0 666 666)%Z) SimpleExample.SimplePipeline.rwvProg). + +Eval cbv in (LL.interp' LLConversions.rangeOf (LL.Return (LL.Var 2%Z))). + +Eval cbv in (LL.interp' LLConversions.rangeOf SimpleExample.SimplePipeline.rwvProg). + +Eval cbv in SimpleExample.SimplePipeline.outputBounds. +Eval cbv in SimpleExample.SimplePipeline.valid. |