<commit_before>\section{IDesc}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}

> module Features.IDesc where

%endif

\subsection{Extending the display language}

We introduce a special DIMu for display purposes. While its definition
is the same than |IMu|, its "typing" is not: the label of an |IMu| is
presented as a lambda-bound anchor. When we are displaying a
particular |IMu|, we precisely know at which index we are considering
it. Therefore, a |DIMu| takes an anchor directly. The distillation
rule takes care of taking applying the lambda-bound anchor to the
index of |IMu| to make a fully applied anchor |DIMu|.

> import -> DInTmConstructors where
>   DIMu :: Labelled (Id :*: Id) (DInTm p x) -> DInTm p x  -> DInTm p x 

> import -> DInTmTraverse where
>   traverseDTIN f (DIMu s i) = (|DIMu (traverse (traverseDTIN f) s) (traverseDTIN f i)|)

> import -> DInTmPretty where
>   pretty (DIMu (Just s :?=: _) _)  = pretty s

\subsection{Plugging Canonical terms in}

> import -> CanConstructors where
>   IMu     :: Labelled (Id :*: Id) t -> t -> Can t

> import -> CanTyRules where
>   canTy chev (Set :>: IMu (ml :?=: (Id ii :& Id x)) i)  = do
>     iiiiv@(ii :=>: iiv) <- chev (SET :>: ii)
>     mlv <- traverse (chev . (ARR iiv ANCHORS :>:)) ml
>     xxv@(x :=>: xv) <- chev (ARR iiv (idesc $$ A iiv) :>: x)
>     iiv <- chev (iiv :>: i)
>     return $ IMu (mlv :?=: (Id iiiiv :& Id xxv)) iiv
>   canTy chev (IMu tt@(_ :?=: (Id ii :& Id x)) i :>: Con y) = do
>     yyv <- chev (idescOp @@ [ ii
>                             , x $$ A i 
>                             , L $ "i" :. [.i. 
>                                 C (IMu (fmap (-$ []) tt) (NV i)) ]
>                             ] :>: y)
>     return $ Con yyv

> import -> CanCompile where

> import -> CanEtaExpand where

> import -> CanPats where
>   pattern IVARN     = ZE
>   pattern ICONSTN   = SU ZE
>   pattern IPIN      = SU (SU ZE)
>   pattern IFPIN     = SU (SU (SU ZE))
>   pattern ISIGMAN   = SU (SU (SU (SU ZE)))
>   pattern IFSIGMAN  = SU (SU (SU (SU (SU ZE))))
>   pattern IPRODN    = SU (SU (SU (SU (SU (SU ZE)))))

>   pattern IMU l ii x i  = C (IMu (l :?=: (Id ii :& Id x)) i) 
>   pattern IVAR i        = CON (PAIR IVARN     (PAIR i VOID))
>   pattern IPI s t       = CON (PAIR IPIN      (PAIR s (PAIR t VOID)))
>   pattern IFPI s t      = CON (PAIR IFPIN     (PAIR s (PAIR t VOID)))
>   pattern ISIGMA s t    = CON (PAIR ISIGMAN   (PAIR s (PAIR t VOID)))
>   pattern IFSIGMA s t   = CON (PAIR IFSIGMAN  (PAIR s (PAIR t VOID)))
>   pattern ICONST p      = CON (PAIR ICONSTN   (PAIR p VOID))
>   pattern IPROD u x y   = CON (PAIR IPRODN    (PAIR u (PAIR x (PAIR y VOID))))

> import -> CanDisplayPats where
>   pattern DIVARN     = DZE
>   pattern DICONSTN   = DSU DZE
>   pattern DIPIN      = DSU (DSU DZE)
>   pattern DIFPIN     = DSU (DSU (DSU DZE))
>   pattern DISIGMAN   = DSU (DSU (DSU (DSU DZE)))
>   pattern DIFSIGMAN  = DSU (DSU (DSU (DSU (DSU DZE))))
>   pattern DIPRODN    = DSU (DSU (DSU (DSU (DSU (DSU DZE)))))

>   pattern DIMU l ii x i  = DIMu (l :?=: (Id ii :& Id x)) i
>   pattern DIVAR i        = DCON (DPAIR DIVARN     (DPAIR i DVOID))
>   pattern DIPI s t       = DCON (DPAIR DIPIN      (DPAIR s (DPAIR t DVOID)))
>   pattern DIFPI s t      = DCON (DPAIR DIFPIN     (DPAIR s (DPAIR t DVOID)))
>   pattern DISIGMA s t    = DCON (DPAIR DISIGMAN   (DPAIR s (DPAIR t DVOID)))
>   pattern DIFSIGMA s t   = DCON (DPAIR DIFSIGMAN  (DPAIR s (DPAIR t DVOID)))
>   pattern DICONST p      = DCON (DPAIR DICONSTN   (DPAIR p DVOID))
>   pattern DIPROD u x y   = DCON (DPAIR DIPRODN    (DPAIR (DPAIR x (DPAIR y DVOID))))


> import -> CanPretty where
>   pretty (IMu (Just l   :?=: _) i)  = wrapDoc
>       (pretty l AppSize <+> pretty i ArgSize)
>       AppSize
>   pretty (IMu (Nothing  :?=: (Id ii :& Id d)) i)  = wrapDoc
>       (kword KwIMu <+> pretty ii ArgSize <+> pretty d ArgSize <+> pretty i ArgSize)
>       AppSize

> import -> CanTraverse where
>   traverse f (IMu l i)     = (|IMu (traverse f l) (f i)|)

> import -> CanHalfZip where
>   halfZip (IMu l0 i0) (IMu l1 i1) = (|(\p -> IMu p (i0,i1)) (halfZip l0 l1)|)

> import -> Coerce where
>   -- coerce :: (Can (VAL,VAL)) -> VAL -> VAL -> Either NEU VAL
>   coerce (IMu (Just (l0,l1) :?=: 
>               (Id (iI0,iI1) :& Id (d0,d1))) (i0,i1)) q (CON x) = 
>     let ql  = CON $ q $$ Fst
>         qiI = CON $ q $$ Snd $$ Fst
>         qi  = CON $ q $$ Snd $$ Snd $$ Snd
>         qd = CON $ q $$ Snd $$ Snd $$ Fst
>         typ = <commit_msg>Fix typo in IDesc that was breaking the build<commit_after>\section{IDesc}

%if False

> {-# OPTIONS_GHC -F -pgmF she #-}

> module Features.IDesc where

%endif

\subsection{Extending the display language}

We introduce a special DIMu for display purposes. While its definition
is the same than |IMu|, its "typing" is not: the label of an |IMu| is
presented as a lambda-bound anchor. When we are displaying a
particular |IMu|, we precisely know at which index we are considering
it. Therefore, a |DIMu| takes an anchor directly. The distillation
rule takes care of taking applying the lambda-bound anchor to the
index of |IMu| to make a fully applied anchor |DIMu|.

> import -> DInTmConstructors where
>   DIMu :: Labelled (Id :*: Id) (DInTm p x) -> DInTm p x  -> DInTm p x 

> import -> DInTmTraverse where
>   traverseDTIN f (DIMu s i) = (|DIMu (traverse (traverseDTIN f) s) (traverseDTIN f i)|)

> import -> DInTmPretty where
>   pretty (DIMu (Just s :?=: _) _)  = pretty s

\subsection{Plugging Canonical terms in}

> import -> CanConstructors where
>   IMu     :: Labelled (Id :*: Id) t -> t -> Can t

> import -> CanTyRules where
>   canTy chev (Set :>: IMu (ml :?=: (Id ii :& Id x)) i)  = do
>     iiiiv@(ii :=>: iiv) <- chev (SET :>: ii)
>     mlv <- traverse (chev . (ARR iiv ANCHORS :>:)) ml
>     xxv@(x :=>: xv) <- chev (ARR iiv (idesc $$ A iiv) :>: x)
>     iiv <- chev (iiv :>: i)
>     return $ IMu (mlv :?=: (Id iiiiv :& Id xxv)) iiv
>   canTy chev (IMu tt@(_ :?=: (Id ii :& Id x)) i :>: Con y) = do
>     yyv <- chev (idescOp @@ [ ii
>                             , x $$ A i 
>                             , L $ "i" :. [.i. 
>                                 C (IMu (fmap (-$ []) tt) (NV i)) ]
>                             ] :>: y)
>     return $ Con yyv

> import -> CanCompile where

> import -> CanEtaExpand where

> import -> CanPats where
>   pattern IVARN     = ZE
>   pattern ICONSTN   = SU ZE
>   pattern IPIN      = SU (SU ZE)
>   pattern IFPIN     = SU (SU (SU ZE))
>   pattern ISIGMAN   = SU (SU (SU (SU ZE)))
>   pattern IFSIGMAN  = SU (SU (SU (SU (SU ZE))))
>   pattern IPRODN    = SU (SU (SU (SU (SU (SU ZE)))))

>   pattern IMU l ii x i  = C (IMu (l :?=: (Id ii :& Id x)) i) 
>   pattern IVAR i        = CON (PAIR IVARN     (PAIR i VOID))
>   pattern IPI s t       = CON (PAIR IPIN      (PAIR s (PAIR t VOID)))
>   pattern IFPI s t      = CON (PAIR IFPIN     (PAIR s (PAIR t VOID)))
>   pattern ISIGMA s t    = CON (PAIR ISIGMAN   (PAIR s (PAIR t VOID)))
>   pattern IFSIGMA s t   = CON (PAIR IFSIGMAN  (PAIR s (PAIR t VOID)))
>   pattern ICONST p      = CON (PAIR ICONSTN   (PAIR p VOID))
>   pattern IPROD u x y   = CON (PAIR IPRODN    (PAIR u (PAIR x (PAIR y VOID))))

> import -> CanDisplayPats where
>   pattern DIVARN     = DZE
>   pattern DICONSTN   = DSU DZE
>   pattern DIPIN      = DSU (DSU DZE)
>   pattern DIFPIN     = DSU (DSU (DSU DZE))
>   pattern DISIGMAN   = DSU (DSU (DSU (DSU DZE)))
>   pattern DIFSIGMAN  = DSU (DSU (DSU (DSU (DSU DZE))))
>   pattern DIPRODN    = DSU (DSU (DSU (DSU (DSU (DSU DZE)))))

>   pattern DIMU l ii x i  = DIMu (l :?=: (Id ii :& Id x)) i
>   pattern DIVAR i        = DCON (DPAIR DIVARN     (DPAIR i DVOID))
>   pattern DIPI s t       = DCON (DPAIR DIPIN      (DPAIR s (DPAIR t DVOID)))
>   pattern DIFPI s t      = DCON (DPAIR DIFPIN     (DPAIR s (DPAIR t DVOID)))
>   pattern DISIGMA s t    = DCON (DPAIR DISIGMAN   (DPAIR s (DPAIR t DVOID)))
>   pattern DIFSIGMA s t   = DCON (DPAIR DIFSIGMAN  (DPAIR s (DPAIR t DVOID)))
>   pattern DICONST p      = DCON (DPAIR DICONSTN   (DPAIR p DVOID))
>   pattern DIPROD u x y   = DCON (DPAIR DIPRODN    (DPAIR u (DPAIR x (DPAIR y DVOID))))


> import -> CanPretty where
>   pretty (IMu (Just l   :?=: _) i)  = wrapDoc
>       (pretty l AppSize <+> pretty i ArgSize)
>       AppSize
>   pretty (IMu (Nothing  :?=: (Id ii :& Id d)) i)  = wrapDoc
>       (kword KwIMu <+> pretty ii ArgSize <+> pretty d ArgSize <+> pretty i ArgSize)
>       AppSize

> import -> CanTraverse where
>   traverse f (IMu l i)     = (|IMu (traverse f l) (f i)|)

> import -> CanHalfZip where
>   halfZip (IMu l0 i0) (IMu l1 i1) = (|(\p -> IMu p (i0,i1)) (halfZip l0 l1)|)

> import -> Coerce where
>   -- coerce :: (Can (VAL,VAL)) -> VAL -> VAL -> Either NEU VAL
>   coerce (IMu (Just (l0,l1) :?=: 
>               (Id (iI0,iI1) :& Id (d0,d1))) (i0,i1)) q (CON x) = 
>     let ql  = CON $ q $$ Fst
>         qiI = CON $ q $$ Snd $$ Fst
>         qi  = CON $ q $$ Snd $$ Snd $$ Snd
>         qd = CON $ q $$ Snd $$ Snd $$ Fst
>         typ = 
{'fraction_non_alphanumeric': 0.14535398230088495, 'fraction_numerical': 0.0035398230088495575, 'mean_word_length': 2.249820273184759, 'pattern_counts': {'":': 0, '<': 21, '<?xml version=': 0, '>': 227, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '477068', 'n_tokens_mistral': 3739, 'n_tokens_neox': 3662, 'n_words': 1261}