{-
demo const mult =
- <[ \y ->
+ <{ \y ->
~~mult
(~~mult y y)
(~~mult y y)
- ]>
+ }>
-}
{-
demo const mult =
- <[ \y ->
+ <{ \y ->
~~mult
(~~mult (~~mult y y) (~~mult y y))
(~~mult (~~mult y y) (~~mult y y))
- ]>
+ }>
-}
{-
demo const mult =
- <[ \y -> ~~(foo 4) ]>
+ <{ \y -> ~~(foo 4) }>
where
foo 0 = const (12::Int)
- foo n = <[ let bar = ~~(foo (n-1))
+ foo n = <{ let bar = ~~(foo (n-1))
in ~~mult bar bar
- ]>
+ }>
-}
{-
demo const mult =
- <[ \y -> ~~(foo 3) ]>
+ <{ \y -> ~~(foo 3) }>
where
foo 0 = const (12::Int)
- foo n = <[ let recurs = ~~(foo (n-1))
+ foo n = <{ let recurs = ~~(foo (n-1))
in ~~mult recurs recurs
- ]>
+ }>
-}
demo const mult =
- <[ \y ->
+ <{ \y ->
let foo = ~~mult (~~mult foo (~~mult y foo)) y
- in foo ]>
+ in foo }>
{-
demo const mult =
- <[ \y -> ~~(foo 2 <[y]>) ]>
+ <{ \y -> ~~(foo 2 <{y}>) }>
where
foo 0 y = const (12::Int)
- foo n y = <[ let recurs = ~~(foo (n-1) y)
+ foo n y = <{ let recurs = ~~(foo (n-1) y)
in ~~mult recurs recurs
- ]>
+ }>
-}
--- demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
--- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
+-- demo const mult = <{ \(y::Int) -> ~~mult y ~~(const 12) }>
+-- demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) }>
-- golden
{-
demo const mult =
- <[ \y ->
+ <{ \y ->
let twelve = ~~mult twelve y
- in twelve ]>
+ in twelve }>
-}
{-
demo const mult =
- <[ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) ]>
+ <{ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) }>
-}
{-
demo const mult =
- <[ \(y::Int) ->
+ <{ \(y::Int) ->
let four = ~~mult four ~~(const 4)
-- twelve = {- {- ~~mult four -} ~~(const 12) -} four
in four
- ]>
+ }>
-}
demo ::
forall c .
- (Int -> <[Int]>@c) ->
- <[Int -> Int -> Int]>@c ->
- <[Int -> Int]>@c
+ (Int -> <{Int}>@c) ->
+ <{Int -> Int -> Int}>@c ->
+ <{Int -> Int}>@c
{-
demo const mult =
- <[ let twelve = ~~(const (12::Int))
+ <{ let twelve = ~~(const (12::Int))
in let four = ~~(const (4::Int))
- in ~~mult four twelve ]>
+ in ~~mult four twelve }>
-}
{-
where
demo' 0 = const 12
demo' 1 = const 12
- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) ]>
+ demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) }>
-}
-- BUG
---demo const mult = <[ \y -> ~~(demo' 0) ]>
+--demo const mult = <{ \y -> ~~(demo' 0) }>
-- where
-- demo' 0 = const 4
-- demo' n = const 4
drawWires tp x1 x x2 x "black" ++
drawLine ((x1+x2)/2) (tp!lowermost x) x2 (tp!uppermost y) "gray!50" "dashed"
; return $ DiagramBox 2 top x r (TT x y) bot }
- mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp ; simpleDiag "drop" top x x bot [] }
+ mkdiag' GAS_drop = do { (top, x ,bot) <- alloc inp
+ ; (_, y ,_) <- alloc outp
+ ; constrainEq x y
+ ; simpleDiag "drop" top x y bot [] }
mkdiag' (GAS_const i) = do { (top, x ,bot) <- alloc inp
; (_, y ,_) <- alloc outp
; constrainEq x y
--- /dev/null
+{-# OPTIONS_GHC -XModalTypes -dcore-lint -XScopedTypeVariables -ddump-types -XTypeFamilies -XNoMonomorphismRestriction #-}
+module Demo (demo, demo2) where
+
+demo z = <[ \y -> ~~z ]>
+
+demo2 :: <[ (a,b) ~~> c ]>@d -> <[ () ~~> a ]>@d -> <[ b ~~>c ]>@d
+demo2 x y = <[ ~~x ~~y ]>
+
+swap :: <[ (a,(b,c)) ~~> d ]>@e -> <[ (b,(a,c)) ~~> d ]>@e
+swap f = <[ \x -> \y -> ~~f y x ]>
+
+-- bad = <[ \f -> \x -> f x ]>
+
+demo3 x y z q = <[ ~~q (~~x ~~y ~~z) ]>
+
+
+
+class BitSerialHardwarePrimitives g where
+ type Wire
+
+ <[ not ]> :: <[ (Wire,()) ~~> Wire ]>@g
+ <[ xor ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
+ <[ or ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
+ <[ and ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
+ <[ mux2 ]> :: <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
+ <[ maj3 ]> :: <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
+ <[ reg ]> :: <[ (Wire,()) ~~> Wire ]>@g
+ <[ zero ]> :: <[ () ~~> Wire ]>@g
+ <[ one ]> :: <[ () ~~> Wire ]>@g
+
+ loop :: [Bool] -> <[ () ~~> Wire ]>@g
+ <[ lfsr ]> :: Int -> [ <[ Wire ]>@g ]
+ <[ adder ]> :: <[ (Wire,(Wire,())) ~~> Wire ]>@g
+ fifo :: Int -> <[ (Wire,()) ~~> Wire ]>@g
+
+ <[ probe ]> :: Int -> <[ (Wire,()) ~~> Wire ]>@g
+ <[ oracle ]> :: Int -> <[ Wire ]>@g
+
+xor3 :: forall g . BitSerialHardwarePrimitives g => <[ (Wire,(Wire,(Wire,()))) ~~> Wire ]>@g
+xor3 = <[ \x -> \y -> \z -> xor (xor x y) z ]>
+
+adder =
+ <[ \in1 ->
+ \in2 ->
+ let firstBitMarker = ~~(loop [ i/=0 | i <- [0..31] ])
+ carry_out = reg (mux2 firstBitMarker zero carry_in)
+ carry_in = maj3 carry_out in1 in2
+ in ~~xor3 carry_out in1 in2
+ ]>
+
+
+rotRight n =
+ <[ \input ->
+ let sel = ~~(loop [ i >= 32-n | i<-[0..31] ])
+ fifo1 = ~~(fifo (32-n)) input
+ fifo2 = ~~(fifo 32 ) fifo1
+ in mux2 sel fifo1 fifo2
+ ]>
+
+sha256round =
+ <[ \load ->
+ \input ->
+ \k_plus_w ->
+ let a = ~~(fifo 32) (mux2 load a_in input)
+ b = ~~(fifo 32) a
+ c = ~~(fifo 32) b
+ d = ~~(fifo 32) c
+ e = ~~(fifo 32) (mux2 load e_in d)
+ f = ~~(fifo 32) e
+ g = ~~(fifo 32) f
+ h = ~~(fifo 32) g
+ s0 = ~~xor3
+ (~~(rotRight 2) a_in)
+ (~~(rotRight 13) a_in)
+ (~~(rotRight 22) a_in)
+ s1 = ~~xor3
+ (~~(rotRight 6) e_in)
+ (~~(rotRight 11) e_in)
+ (~~(rotRight 25) e_in)
+ a_in = adder t1 t2
+ e_in = adder t1 d
+ t1 = adder
+ (adder h s1)
+ (adder (mux2 e g f)
+ k_plus_w)
+ t2 = adder s0 (maj3 a b c)
+ in h
+ ]>
\ No newline at end of file
open .build/test.pdf
#sanity += BiGArrow.hs
+sanity += KappaDemo.hs
sanity += CircuitExample.hs
sanity += CommandSyntaxExample.hs
sanity += DotProduct.hs
Definition mkWeakExprVar (u:Unique)(t:WeakType) : WeakExprVar :=
weakExprVar (mkExVar (mkSystemName u "ev" O) (weakTypeToCoreType t)) t.
- Context (hetmet_brak : WeakExprVar).
- Context (hetmet_esc : WeakExprVar).
- Context (uniqueSupply : UniqSupply).
+ Context (hetmet_brak : WeakExprVar).
+ Context (hetmet_esc : WeakExprVar).
+ Context (hetmet_kappa : WeakExprVar).
+ Context (hetmet_kappa_app : WeakExprVar).
+ Context (uniqueSupply : UniqSupply).
Definition useUniqueSupply {T}(ut:UniqM T) : ???T :=
match ut with
(do_skolemize : bool)
(hetmet_brak : CoreVar)
(hetmet_esc : CoreVar)
+ (hetmet_kappa : WeakExprVar)
+ (hetmet_kappa_app : WeakExprVar)
(uniqueSupply : UniqSupply)
(lbinds:list (@CoreBind CoreVar))
(hetmet_PGArrowTyCon : TyFun)
Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak.
Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc.
+ Definition hetmet_kappa' := coreVarToWeakExprVarOrError hetmet_kappa.
+ Definition hetmet_kappa_app' := coreVarToWeakExprVarOrError hetmet_kappa_app.
Definition coreToCoreExpr' (cex:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) :=
addErrorMessage ("input CoreSyn: " +++ toString cex)
OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))
OK ((@proof2expr nat _ FreshNat _ _ τ nil _
(fun _ => Prelude_error "unbound unique") _ haskProof) O)
>>= fun e' => (snd e') >>= fun e'' =>
- strongExprToWeakExpr hetmet_brak' hetmet_esc'
+ strongExprToWeakExpr hetmet_brak' hetmet_esc' (*hetmet_kappa' hetmet_kappa_app'*)
mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply
(projT2 e'') INil
>>= fun q => OK (weakExprToCoreExpr q))))
: CoreM (list (@CoreBind CoreVar)) :=
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_brak" >>= fun hetmet_brak =>
dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_esc" >>= fun hetmet_esc =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa" >>= fun hetmet_kappa =>
+ dsLookupVar "GHC.HetMet.CodeTypes" "hetmet_kappa_app" >>= fun hetmet_kappa_app =>
dsLookupTyc "GHC.HetMet.Private" "PGArrow" >>= fun hetmet_PGArrow =>
dsLookupTyc "GHC.HetMet.GArrow" "GArrowUnit" >>= fun hetmet_PGArrow_unit =>
dsLookupTyc "GHC.HetMet.GArrow" "GArrowTensor" >>= fun hetmet_PGArrow_tensor =>
do_skolemize
hetmet_brak
hetmet_esc
+ (*
+ hetmet_kappa
+ hetmet_kappa_app
+ *)
uniqueSupply
hetmet_PGArrow
hetmet_PGArrow_unit
Variable hetmet_brak_name : CoreName. Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name".
Variable hetmet_csp_name : CoreName. Extract Inlined Constant hetmet_csp_name => "PrelNames.hetmet_csp_name".
+Variable hetmet_kappa_name : CoreName. Extract Inlined Constant hetmet_kappa_name => "PrelNames.hetmet_kappa_name".
+Variable hetmet_kappa_app_name: CoreName.
+Extract Inlined Constant hetmet_kappa_app_name => "PrelNames.hetmet_kappa_app_name".
Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
split_list lwt (length (fst (tyFunKind tf))) >>=
| _ => None
end.
+Definition isKappa (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3))
+ => if coreName_eq hetmet_kappa_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
+Definition isKappaApp (ce:@CoreExpr CoreVar) : bool :=
+match ce with
+ | (CoreEApp (CoreEApp
+ (CoreEApp
+ (CoreEApp
+ (CoreEVar v)
+ (CoreEType t1))
+ (CoreEType t2))
+ (CoreEType t3)) _)
+ => if coreName_eq hetmet_kappa_app_name (coreVarCoreName v) then true else false
+ | _ => false
+end.
+
Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
match ce with
| (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
coreExprToWeakExpr e2 >>= fun e' =>
coreTypeToWeakType t >>= fun t' =>
OK (WECSP v tv e' t')
- | None => coreExprToWeakExpr e1 >>= fun e1' =>
- match e2 with
- | CoreEType t =>
- coreTypeToWeakType t >>= fun t' =>
- OK (WETyApp e1' t')
- | _ => coreExprToWeakExpr e2
- >>= fun e2' => OK (WEApp e1' e2')
- end
- end
- end
+ | None =>
+ (*
+ if isKappa e1
+ then match e2 with
+ | CoreELam v e => match coreVarToWeakVar' v with
+ | OK (WExprVar ev) =>
+ coreExprToWeakExpr e >>= fun e' =>
+ OK (WEKappa ev e')
+ | _ => Error "bogus"
+ end
+ | _ => Error "bogus"
+ end
+ else if isKappaApp e1
+ then match e1 with
+ | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
+ coreExprToWeakExpr e1' >>= fun e1'' =>
+ coreExprToWeakExpr e2 >>= fun e2'' =>
+ OK (WEKappaApp e1'' e2'')
+ | _ => Error "bogus"
+ end
+ else
+ *)
+ coreExprToWeakExpr e1 >>= fun e1' =>
+ match e2 with
+ | CoreEType t =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WETyApp e1' t')
+ | _ => coreExprToWeakExpr e2
+ >>= fun e2' => OK (WEApp e1' e2')
+ end
+ end
+ end
end
| CoreELam v e => coreVarToWeakVar' v >>= fun v' => match v' with
| TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
| TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
| TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
+ (*
+ | TKappa : RawHaskType (★ ⇛★ ⇛★ ) (* (~~>) *)
+ *)
| TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
| TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
| TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
Implicit Arguments TAll [ [TV] ].
Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
+(*Notation "t1 ~~~> t2" := (fun TV env => (TApp (TApp TKappa (t1 TV env)) (t2 TV env))).*)
Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
(* Kind and Coercion Environments *)
| WETyApp : WeakExpr -> WeakType -> WeakExpr
| WECoApp : WeakExpr -> WeakCoercion -> WeakExpr
| WELam : WeakExprVar -> WeakExpr -> WeakExpr
+(*
+| WEKappa : WeakExprVar -> WeakExpr -> WeakExpr
+| WEKappaApp : WeakExpr -> WeakExpr -> WeakExpr
+*)
| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr
| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr
(weakExprToCoreExpr e)::
nil)
(CoreEVar v)
+ (*
+ | WEKappa v e => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappa"
+ | WEKappaApp e1 e2 => Prelude_error "FIXME: weakExprToCoreExpr case for WEKappaApp"
+ *)
| WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e)
| WECase vscrut escrut tbranches tc types alts =>
CoreECase (weakExprToCoreExpr escrut) vscrut (weakTypeToCoreType tbranches)
| WELet cv e1 e2 => doesWeakVarOccur wev e1 || (if eqd_dec (wev:CoreVar) (cv:CoreVar)then false else doesWeakVarOccur wev e2)
| WEApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
| WELam cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+(*
+ | WEKappaApp e1 e2 => doesWeakVarOccur wev e1 || doesWeakVarOccur wev e2
+ | WEKappa cv e => if eqd_dec (wev:CoreVar) (cv:CoreVar) then false else doesWeakVarOccur wev e
+*)
| WETyLam cv e => doesWeakVarOccur wev e
| WECoLam cv e => doesWeakVarOccur wev e
| WECase vscrut escrut tbranches tc avars alts =>
projects / coq-hetmet.git / commitdiff