diff options
Diffstat (limited to 'src/Term')
| -rw-r--r-- | src/Term/Pretty.idr | 246 | ||||
| -rw-r--r-- | src/Term/Semantics.idr | 72 | ||||
| -rw-r--r-- | src/Term/Syntax.idr | 124 |
3 files changed, 414 insertions, 28 deletions
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr new file mode 100644 index 0000000..ed2dd45 --- /dev/null +++ b/src/Term/Pretty.idr @@ -0,0 +1,246 @@ +module Term.Pretty + +import public Text.PrettyPrint.Prettyprinter +import public Text.PrettyPrint.Prettyprinter.Render.Terminal + +import Data.Fin +import Data.Fin.Extra +import Data.Nat +import Data.Stream +import Data.String + +import Term +import Term.Syntax + +%prefix_record_projections off + +data Syntax = Bound | Keyword | Symbol | Literal + +symbol : Doc Syntax -> Doc Syntax +symbol = annotate Symbol + +keyword : Doc Syntax -> Doc Syntax +keyword = annotate Keyword + +bound : Doc Syntax -> Doc Syntax +bound = annotate Bound + +literal : Doc Syntax -> Doc Syntax +literal = annotate Literal + +rec_ : Doc Syntax +rec_ = keyword "rec" + +underscore : Doc Syntax +underscore = bound "_" + +plus : Doc Syntax +plus = symbol "+" + +arrow : Doc Syntax +arrow = symbol "=>" + +backslash : Doc Syntax +backslash = symbol Symbols.backslash + +lit : Nat -> Doc Syntax +lit = literal . pretty + +public export +interface Renderable (0 a : Type) where + fromSyntax : Syntax -> a + +export +Renderable AnsiStyle where + fromSyntax Bound = italic + fromSyntax Keyword = color Blue + fromSyntax Symbol = color BrightWhite + fromSyntax Literal = color Green + +startPrec, leftAppPrec, appPrec : Prec +startPrec = Open +leftAppPrec = Equal +appPrec = App + +data StrictThins : SnocList a -> SnocList a -> Type where + Empty : [<] `StrictThins` [<] + Drop : sx `StrictThins` sy -> sx `StrictThins` sy :< y + Keep : sx `StrictThins` sy -> sx :< z `StrictThins` sy :< z + +%name StrictThins thin + +record IsBound (ty : Ty) (ctx : SnocList Ty) (t : FullTerm ty' ctx') where + constructor MkBound + {0 bound : SnocList Ty} + {0 used : SnocList Ty} + thin : used `StrictThins` bound + 0 prfTy : ty = bound ~>* ty' + 0 prfCtx : ctx' = ctx ++ used + +%name IsBound isBound + +record Binding (ty : Ty) (ctx : SnocList Ty) where + constructor MkBinding + {0 ty' : Ty} + {0 ctx' : SnocList Ty} + term : FullTerm ty' ctx' + isBound : IsBound ty ctx term + +%name Binding bound + +getBinding : (t : FullTerm ty' ctx') -> IsBound ty ctx t -> Binding ty ctx +getBinding (Const t) isBound = + getBinding t (MkBound (Drop isBound.thin) isBound.prfTy isBound.prfCtx) +getBinding (Abs {ty} t) isBound = + getBinding t (MkBound (Keep isBound.thin) isBound.prfTy (cong (:< ty) isBound.prfCtx)) +getBinding t isBound = MkBinding t isBound + +isBoundRefl : (0 t : FullTerm ty ctx) -> IsBound ty ctx t +isBoundRefl t = MkBound {bound = [<]} Empty Refl Refl + +record Spline (ty : Ty) (ctx : SnocList Ty) where + constructor MkSpline + {0 tys : SnocList Ty} + head : Term (tys ~>* ty) ctx + args : All (flip Term ctx) tys + +%name Spline spline + +wkn : Spline ty ctx -> ctx `Thins` ctx' -> Spline ty ctx' +wkn spline thin = MkSpline (wkn spline.head thin) (mapProperty (flip wkn thin) spline.args) + +getSpline : FullTerm ty ctx -> Spline ty ctx +getSpline (App (MakePair (t `Over` thin) u _)) = + let rec = wkn (getSpline t) thin in + MkSpline rec.head (rec.args :< u) +getSpline t = MkSpline (t `Over` Id) [<] + +getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx)) +getSucs Zero = (0, Nothing) +getSucs (Suc t) = mapFst S (getSucs t) +getSucs t = (0, Just t) + +public export +data Len : SnocList a -> Type where + Z : Len [<] + S : Len sx -> Len (sx :< a) + +%name Len k + +lenToNat : Len sx -> Nat +lenToNat Z = 0 +lenToNat (S k) = S (lenToNat k) + +lenSrc : sx `StrictThins` sy -> Len sx +lenSrc Empty = Z +lenSrc (Drop thin) = lenSrc thin +lenSrc (Keep thin) = S (lenSrc thin) + +strictSrc : Len sz -> sx `StrictThins` sy -> Len (sz ++ sx) +strictSrc k Empty = k +strictSrc k (Drop thin) = strictSrc k thin +strictSrc k (Keep thin) = S (strictSrc k thin) + +extend : sx `Thins` sy -> Len sz -> sx ++ sz `Thins` sy ++ sz +extend thin Z = thin +extend thin (S k) = Keep (extend thin k) + +parameters (names : Stream String) + prettyTerm' : (len : Len ctx) => Prec -> Term ty ctx -> Doc Syntax + prettyFullTerm : (len : Len ctx) => Prec -> FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc Syntax + prettyBinding : (len : Len ctx) => Prec -> Binding ty ctx' -> ctx' `Thins` ctx -> Doc Syntax + prettySpline : (len : Len ctx) => Prec -> Spline ty ctx -> Doc Syntax + prettyArg : (len : Len ctx) => Term ty ctx' -> Doc Syntax + + prettyTerm' d (t `Over` thin) = prettyFullTerm d t thin + + prettyFullTerm d Var thin = + bound (pretty $ index (minus (lenToNat len) (S $ elemToNat $ index thin Here)) names) + prettyFullTerm d t@(Const _) thin = + prettyBinding d (assert_smaller t $ getBinding t $ isBoundRefl t) thin + prettyFullTerm d t@(Abs _) thin = + prettyBinding d (assert_smaller t $ getBinding t $ isBoundRefl t) thin + prettyFullTerm d t@(App _) thin = + prettySpline d (assert_smaller t $ wkn (getSpline t) thin) + prettyFullTerm d Zero thin = lit 0 + prettyFullTerm d (Suc t) thin = + let (n, t') = getSucs t in + case t' of + Just t' => + parenthesise (d >= appPrec) $ group $ + lit (S n) <++> plus <++> prettyFullTerm leftAppPrec (assert_smaller t t') thin + Nothing => lit (S n) + prettyFullTerm d t@(Rec _) thin = + prettySpline d (assert_smaller t $ wkn (getSpline t) thin) + + prettyBinding d (MkBinding t {ctx' = ctx'_} (MkBound thin' _ prfCtx)) thin = + parenthesise (d > startPrec) $ group $ align $ hang 2 $ + Pretty.backslash <+> snd (prettyThin (lenToNat len) thin') <++> arrow <+> line <+> + prettyFullTerm @{strictSrc len thin'} Open t + (rewrite prfCtx in extend thin $ lenSrc thin') + where + prettyThin : Nat -> sx `StrictThins` sy -> (Nat, Doc Syntax) + prettyThin n Empty = (n, neutral) + prettyThin n (Drop Empty) = (n, underscore) + prettyThin n (Keep Empty) = (S n, bound (pretty $ index n names)) + prettyThin n (Drop thin) = + let (k, doc) = prettyThin n thin in + (k, doc <+> comma <++> underscore) + prettyThin n (Keep thin) = + let (k, doc) = prettyThin n thin in + (S k, doc <+> comma <++> bound (pretty $ index k names)) + + prettySpline d + s@(MkSpline (Rec (MakePair t (MakePair u v _ `Over` thin2) _) `Over` thin1) args) = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + (rec_ <++> prettyTerm' appPrec (assert_smaller s $ wkn t thin1)) <+> line <+> + vsep + ([prettyTerm' appPrec (assert_smaller s $ wkn u (thin1 . thin2)) + , prettyTerm' appPrec (assert_smaller s $ wkn v (thin1 . thin2))] ++ + toList (forget $ mapProperty (assert_total $ prettyTerm' appPrec) args)) + prettySpline d s@(MkSpline t args) = + parenthesise (d >= appPrec) $ group $ align $ hang 2 $ + prettyTerm' leftAppPrec t <+> line <+> + vsep (toList $ forget $ mapProperty (assert_total $ prettyTerm' appPrec) args) + +finToChar : Fin 26 -> Char +finToChar 0 = 'x' +finToChar 1 = 'y' +finToChar 2 = 'z' +finToChar 3 = 'a' +finToChar 4 = 'b' +finToChar 5 = 'c' +finToChar 6 = 'd' +finToChar 7 = 'e' +finToChar 8 = 'f' +finToChar 9 = 'g' +finToChar 10 = 'h' +finToChar 11 = 'i' +finToChar 12 = 'j' +finToChar 13 = 'k' +finToChar 14 = 'l' +finToChar 15 = 'm' +finToChar 16 = 'n' +finToChar 17 = 'o' +finToChar 18 = 'p' +finToChar 19 = 'q' +finToChar 20 = 'r' +finToChar 21 = 's' +finToChar 22 = 't' +finToChar 23 = 'u' +finToChar 24 = 'v' +finToChar 25 = 'w' + +name : Nat -> List Char +name k = + case divMod k 26 of + Fraction k 26 0 r prf => [finToChar r] + Fraction k 26 (S q) r prf => finToChar r :: name (assert_smaller k q) + +export +canonicalNames : Stream String +canonicalNames = map (fastPack . name) nats + +export +prettyTerm : Renderable ann => (len : Len ctx) => Term ty ctx -> Doc ann +prettyTerm t = map fromSyntax (prettyTerm' canonicalNames Open t) diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr index eeb2210..2e61040 100644 --- a/src/Term/Semantics.idr +++ b/src/Term/Semantics.idr @@ -1,6 +1,8 @@ module Term.Semantics +import Control.Monad.Identity import Term + import public Data.SnocList.Quantifiers public export @@ -12,27 +14,55 @@ rec : Nat -> a -> (a -> a) -> a rec 0 x f = x rec (S k) x f = f (rec k x f) -fullSem : FullTerm ty ctx -> ctx `Thins` ctx' -> All TypeOf ctx' -> TypeOf ty -fullSem Var thin ctx = indexAll (index thin Here) ctx -fullSem (Const t) thin ctx = const (fullSem t thin ctx) -fullSem (Abs t) thin ctx = \v => fullSem t (Keep thin) (ctx :< v) -fullSem (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin ctx = - fullSem t (thin . thin1) ctx (fullSem u (thin . thin2) ctx) -fullSem Zero thin ctx = 0 -fullSem (Suc t) thin ctx = S (fullSem t thin ctx) -fullSem - (Rec (MakePair - (t `Over` thin1) - (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') - _)) - thin - ctx = - let thin' = thin . thin' in - rec - (fullSem t (thin . thin1) ctx) - (fullSem u (thin' . thin2) ctx) - (fullSem v (thin' . thin3) ctx) +%inline +init : All p (sx :< x) -> All p sx +init (psx :< px) = psx + +%inline +mapInit : (All p sx -> All p sy) -> All p (sx :< z) -> All p (sy :< z) +mapInit f (psx :< px) = f psx :< px + +restrict : Applicative m => sx `Thins` sy -> m (All p sy -> All p sx) +restrict Id = pure id +restrict Empty = pure (const [<]) +restrict (Drop thin) = [| restrict thin . [| init |] |] +restrict (Keep thin) = [| mapInit (restrict thin) |] + +%inline +indexVar : All p [<x] -> p x +indexVar [<px] = px + +%inline +sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty) +fullSem' : Monad m => FullTerm ty ctx -> m (All TypeOf ctx -> TypeOf ty) + +sem' (t `Over` thin) = [| fullSem' t . restrict thin |] + +fullSem' Var = pure indexVar +fullSem' (Const t) = do + t <- fullSem' t + pure (const . t) +fullSem' (Abs t) = do + t <- fullSem' t + pure (t .: (:<)) +fullSem' (App (MakePair t u _)) = do + t <- sem' t + u <- sem' u + pure (\ctx => t ctx (u ctx)) +fullSem' Zero = pure (const 0) +fullSem' (Suc t) = do + t <- fullSem' t + pure (S . t) +fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do + t <- sem' t + u <- sem' u + v <- sem' v + f <- restrict thin + pure + (\ctx => + let ctx' = f ctx in + rec (t ctx) (u ctx') (v ctx')) export sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty -sem (t `Over` thin) ctx = fullSem t thin ctx +sem t = runIdentity (sem' t) diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr index a990600..6a05271 100644 --- a/src/Term/Syntax.idr +++ b/src/Term/Syntax.idr @@ -3,6 +3,8 @@ module Term.Syntax import public Data.SnocList import public Term +%prefix_record_projections off + -- Combinators export @@ -32,16 +34,124 @@ Abs' : (Term ty (ctx :< ty) -> Term ty' (ctx :< ty)) -> Term (ty ~> ty') ctx Abs' f = Abs (f $ Var Here) export -App' : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx -App' (Const t `Over` thin) u = t `Over` thin -App' (Abs t `Over` thin) u = subst (t `Over` Keep thin) (Base Id :< u) -App' t u = App t u - -export App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty -> Term ty ctx App t [<] = t -App t (us :< u) = App' (App t us) u +App t (us :< u) = App (App t us) u export (.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx t . u = Abs (App (shift t) [<App (shift u) [<Var Here]]) + +-- Incomplete Evaluation + +data IsFunc : FullTerm (ty ~> ty') ctx -> Type where + ConstFunc : (t : FullTerm ty' ctx) -> IsFunc (Const t) + AbsFunc : (t : FullTerm ty' (ctx :< ty)) -> IsFunc (Abs t) + +isFunc : (t : FullTerm (ty ~> ty') ctx) -> Maybe (IsFunc t) +isFunc Var = Nothing +isFunc (Const t) = Just (ConstFunc t) +isFunc (Abs t) = Just (AbsFunc t) +isFunc (App x) = Nothing +isFunc (Rec x) = Nothing + +app : + (ratio : Double) -> + {ty : Ty} -> + (t : Term (ty ~> ty') ctx) -> + {auto 0 ok : IsFunc t.value} -> + Term ty ctx -> + Maybe (Term ty' ctx) +app ratio (Const t `Over` thin) u = Just (t `Over` thin) +app ratio (Abs t `Over` thin) u = + let uses = countUses (t `Over` Id) Here in + let sizeU = size u in + if cast (sizeU * uses) <= cast (S (sizeU + uses)) * ratio + then + Just (subst (t `Over` Keep thin) (Base Id :< u)) + else + Nothing + +App' : + {ty : Ty} -> + (ratio : Double) -> + Term (ty ~> ty') ctx -> + Term ty ctx -> + Maybe (Term ty' ctx) +App' ratio + (Rec (MakePair + t + (MakePair (u `Over` thin2) (Const v `Over` thin3) _ `Over` thin') + _) `Over` thin) + arg = + case (isFunc u, isFunc v) of + (Just ok1, Just ok2) => + let thinA = thin . thin' . thin2 in + let thinB = thin . thin' . thin3 in + case (app ratio (u `Over` thinA) arg , app ratio (v `Over` thinB) arg) + of + (Just u, Just v) => Just (Rec (wkn t thin) u (Const v)) + (Just u, Nothing) => Just (Rec (wkn t thin) u (Const $ App (v `Over` thinB) arg)) + (Nothing, Just v) => Just (Rec (wkn t thin) (App (u `Over` thinA) arg) (Const v)) + (Nothing, Nothing) => + Just (Rec (wkn t thin) (App (u `Over` thinA) arg) (Const $ App (v `Over` thinB) arg)) + _ => Nothing +App' ratio t arg = + case isFunc t.value of + Just _ => app ratio t arg + Nothing => Nothing + +Rec' : + {ty : Ty} -> + FullTerm N ctx' -> + ctx' `Thins` ctx -> + Term ty ctx -> + Term (ty ~> ty) ctx -> + Maybe (Term ty ctx) +Rec' Zero thin u v = Just u +Rec' (Suc t) thin u v = + let rec = maybe (Rec (t `Over` thin) u v) id (Rec' t thin u v) in + Just $ maybe (App v rec) id $ (App' 1 v rec) +Rec' t thin u v = Nothing + +eval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> Term ty ctx -> (Nat, Term ty ctx) +fullEval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> FullTerm ty ctx -> (Nat, Term ty ctx) + +eval' fuel r (t `Over` thin) = mapSnd (flip wkn thin) (fullEval' fuel r t) + +fullEval' 0 r t = (0, t `Over` Id) +fullEval' fuel@(S f) r Var = (fuel, Var `Over` Id) +fullEval' fuel@(S f) r (Const t) = mapSnd Const (fullEval' fuel r t) +fullEval' fuel@(S f) r (Abs t) = mapSnd Abs (fullEval' fuel r t) +fullEval' fuel@(S f) r (App (MakePair t u _)) = + case App' r t u of + Just t => (f, t) + Nothing => + let (fuel', t) = eval' f r t in + let (fuel', u) = eval' (assert_smaller fuel fuel') r u in + (fuel', App t u) +fullEval' fuel@(S f) r Zero = (fuel, Zero `Over` Id) +fullEval' fuel@(S f) r (Suc t) = mapSnd Suc (fullEval' fuel r t) +fullEval' fuel@(S f) r (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = + case Rec' t.value t.thin (wkn u thin) (wkn v thin) of + Just t => (f, t) + Nothing => + let (fuel', t) = eval' f r t in + let (fuel', u) = eval' (assert_smaller fuel fuel') r u in + let (fuel', v) = eval' (assert_smaller fuel fuel') r v in + (fuel', Rec t (wkn u thin) (wkn v thin)) + +export +eval : + {ty : Ty} -> + {default 1.5 ratio : Double} -> + {default 20000 fuel : Nat} -> + Term ty ctx -> + Term ty ctx +eval t = loop fuel t + where + loop : Nat -> Term ty ctx -> Term ty ctx + loop fuel t = + case eval' fuel ratio t of + (0, t) => t + (S f, t) => loop (assert_smaller fuel f) t |