<commit_before>> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module Nat where

> import BwdFwd
> import Tm
> import Rules

> natd :: VAL
> natd = ARG (ENUMT (CONSE (TAG "czero") (CONSE (TAG "csuc") NILE))) 
>            (L $ H B0 
>                  "" 
>                  (N (switchOp :@ [CONSE (TAG "czero") 
>                                         (CONSE (TAG "csuc") NILE)
>                                  ,L $ K DESC
>                                  ,PAIR DONE (PAIR (IND UNIT DONE) VOID)
>                                  ,NV 0
>                                  ])))

> nat :: VAL
> nat = MU natd

> zero :: VAL
> zero = INTROS (PAIR ZE VOID)

> suc :: VAL
> suc = L $ H B0 "" (INTROS (PAIR (SU ZE) (PAIR (L $ K (NV 0)) VOID)))

> plus :: VAL -> VAL -> VAL
> plus m n = elimOp @@ [natd
>                      ,L $ K (ARR nat nat)
>                      ,eval [.nat.suc. L $ "" :. [.x. L $ "" :. [.ih. L $ "" :. [.n. N (switchOp :@ [CONSE (TAG "czero") (CONSE (TAG "csuc") NILE)
>                                                                                                    ,L $ K (NV nat)
>                                                                                                    ,PAIR (NV n) (PAIR (N (V suc :$ A (N (V ih :$ Fst :$ A (NV n))))) VOID)
>                                                                                                    ,N (V x :$ Fst)])]]]] $ B0 :< nat :< suc 
>                      ,m] $$ A n

> two :: VAL
> two = suc $$ A (suc $$ A zero) 

> four :: VAL
> four = suc $$ A (suc $$ A (suc $$ A (suc $$ A zero)))<commit_msg>2 + 2 = 4<commit_after>> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE TypeOperators, GADTs, KindSignatures,
>     TypeSynonymInstances, FlexibleInstances, ScopedTypeVariables #-}

> module Nat where

> import BwdFwd
> import Tm
> import Rules

> natd :: VAL
> natd = ARG (ENUMT (CONSE (TAG "czero") (CONSE (TAG "csuc") NILE))) natc

 natd = ARG (ENUMT (CONSE (TAG "czero") (CONSE (TAG "csuc") NILE))) 
            (L $ H B0 
                  "" 
                  (N (switchOp :@ [CONSE (TAG "czero") 
                                         (CONSE (TAG "csuc") NILE)
                                  ,L $ K DESC
                                  ,PAIR DONE (PAIR (IND UNIT DONE) VOID)
                                  ,NV 0
                                  ])))

> natc :: VAL
> natc = L $ H B0 
>              "" 
>              (N (switchOp :@ [CONSE (TAG "czero") 
>                                     (CONSE (TAG "csuc") NILE)
>                              ,L $ K DESC
>                              ,PAIR DONE (PAIR (IND UNIT DONE) VOID)
>                              ,NV 0
>                              ]))

> nat :: VAL
> nat = MU natd

> zero :: VAL
> zero = INTROS (PAIR ZE VOID)

> suc :: VAL
> suc = L $ H B0 "" (INTROS (PAIR (SU ZE) (PAIR (L $ K (NV 0)) VOID)))

> plus :: VAL -> VAL -> VAL
> plus m n = elimOp @@ [natd
>                      ,L $ K (ARR nat nat)
>                      ,eval [.nat.suc. L $ "" :. [.x.
>                         N $ splitOp :@ [ENUMT (CONSE (TAG "czero") (CONSE (TAG "csuc") NILE)) -- A
>                                        ,L $ "" :. [.t. undefined ]                            -- B
>                                        ,L $ "" :. [.y. undefined ]                            -- C
>                                        ,L $ "" :. [.t. N $ switchOp :@ [CONSE (TAG "czero") (CONSE (TAG "csuc") NILE) -- ls
>                                                                        ,undefined                                     -- f
>                                                                        ,PAIR (L $ K (L $ K (L $ "" :. [.n. NV n ])))  -- T 
>                                                                              (PAIR (L $ K (L $ "" :. [.ih. L $ "" :. [.n.
>                                                                                       N (V suc :$ A (N ((V ih :$ Fst) :$ A VOID :$ A (NV n))))]]))
>                                                                                    VOID)
>                                                                        ,NV t]]                                        -- t
>                                        ,NV x]]                                                -- x
>                            ] $ B0 :< nat :< suc
>                      ,m] $$ A n

> two :: VAL
> two = suc $$ A (suc $$ A zero) 

> four :: VAL
> four = suc $$ A (suc $$ A (suc $$ A (suc $$ A zero)))
{'fraction_non_alphanumeric': 0.1421770179614802, 'fraction_numerical': 0.003246050638389959, 'mean_word_length': 0.7580829212628376, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 87, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 59, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5232001', 'n_tokens_mistral': 1384, 'n_tokens_neox': 1310, 'n_words': 404}