From: Adam Megacz Date: Mon, 31 Oct 2011 05:50:48 +0000 (-0700) Subject: partial implementation of KappaAbs/KappaApp in Coq code X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=a2cbba71fc8af854b34dcf348392897504ad41b2;hp=-c partial implementation of KappaAbs/KappaApp in Coq code --- a2cbba71fc8af854b34dcf348392897504ad41b2 diff --git a/examples/Demo.hs b/examples/Demo.hs index bb3bf17..7a6aee8 100644 --- a/examples/Demo.hs +++ b/examples/Demo.hs @@ -3,11 +3,11 @@ module Demo (demo) where {- demo const mult = - <[ \y -> + <{ \y -> ~~mult (~~mult y y) (~~mult y y) - ]> + }> -} @@ -17,23 +17,23 @@ demo const mult = {- 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 - ]> + }> -} @@ -41,12 +41,12 @@ demo const mult = {- 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 - ]> + }> -} @@ -55,9 +55,9 @@ demo const mult = demo const mult = - <[ \y -> + <{ \y -> let foo = ~~mult (~~mult foo (~~mult y foo)) y - in foo ]> + in foo }> @@ -72,12 +72,12 @@ demo const mult = {- 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 - ]> + }> -} @@ -120,40 +120,40 @@ demo const mult = --- 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 }> -} {- @@ -161,11 +161,11 @@ demo const mult = demo' 3 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 diff --git a/examples/GArrowTikZ.hs b/examples/GArrowTikZ.hs index d3ae2e0..b090c85 100644 --- a/examples/GArrowTikZ.hs +++ b/examples/GArrowTikZ.hs @@ -204,7 +204,10 @@ mkdiag (GASPortShapeWrapper inp outp x) = mkdiag' x 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 diff --git a/examples/KappaDemo.hs b/examples/KappaDemo.hs new file mode 100644 index 0000000..43d29f4 --- /dev/null +++ b/examples/KappaDemo.hs @@ -0,0 +1,88 @@ +{-# 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 diff --git a/examples/Makefile b/examples/Makefile index f880d81..09e4b9c 100644 --- a/examples/Makefile +++ b/examples/Makefile @@ -5,6 +5,7 @@ open: open .build/test.pdf #sanity += BiGArrow.hs +sanity += KappaDemo.hs sanity += CircuitExample.hs sanity += CommandSyntaxExample.hs sanity += DotProduct.hs diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 88714c7..9f0fc1a 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -179,9 +179,11 @@ Section core2proof. 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 @@ -311,6 +313,8 @@ Section core2proof. (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) @@ -451,6 +455,8 @@ Section core2proof. 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) @@ -472,7 +478,7 @@ Section core2proof. 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)) @@ -483,7 +489,7 @@ Section core2proof. 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)) @@ -493,7 +499,7 @@ Section core2proof. 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)))) @@ -538,6 +544,8 @@ Section core2proof. : 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 => @@ -569,6 +577,10 @@ Section core2proof. do_skolemize hetmet_brak hetmet_esc + (* + hetmet_kappa + hetmet_kappa_app + *) uniqueSupply hetmet_PGArrow hetmet_PGArrow_unit diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 7669e5d..a287b20 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -28,6 +28,9 @@ Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant co 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))) >>= @@ -146,6 +149,32 @@ match ce with | _ => 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)) @@ -216,16 +245,38 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := 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 diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 4740acb..a7bd11a 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -66,6 +66,9 @@ Section Raw. | 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:κ.φ *) @@ -111,6 +114,7 @@ Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ]. 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 *) diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 077f7b5..9d39f44 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -31,6 +31,10 @@ Inductive WeakExpr := | 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 diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index c3e90a4..7d24277 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -84,6 +84,10 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := (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) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 0acc0af..f6dc701 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -489,6 +489,10 @@ Fixpoint doesWeakVarOccur (wev:WeakExprVar)(me:WeakExpr) : bool := | 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 =>