Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit e3667cf8 authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Start defining an explicit representation of inductive Church encodings for the 'mu' combinator

parent 015640da
......@@ -11,7 +11,9 @@ module Data.CaPriCon(
StringPattern,NodeDir(..),AHDir(..),ApDir,
findPattern,freshContext,
-- * Showing nodes
ListBuilder(..),NodeDoc(..),doc2raw,doc2latex,doc2svg,showNode,showNode'
ListBuilder(..),NodeDoc(..),doc2raw,doc2latex,doc2svg,showNode,showNode',
-- * Wishful thinking
Prismatic(..),Ray(..),Reflection(..),toPrismatic
) where
import Definitive
......@@ -49,7 +51,9 @@ instance SerialStream ListStream where
encodeByte _ b = ListBuilder (b:)
toSerialStream (ListBuilder k) = k []
-- | Inductive types
-- | types
type UniverseSize = Int
type SymbolRef = Int
data BindType = Lambda | Prod
......@@ -66,6 +70,19 @@ data ApHead str a = Sym SymbolRef
data Application str a = Ap (ApHead str a) [Term str a]
deriving (Show,Generic)
data Prismatic str a = Prism_Lens (Ray UniverseSize str a) (Prismatic str a)
| Prism_Ray (Ray (SymbolRef,[Term str a]) str a) (Prismatic str a)
| Prism_Base SymbolRef [Term str a]
data Ray tail str a = Ray_Param (Reflection str a) (Ray tail str a)
| Ray_Tail tail
data Reflection str a = Refl_Base SymbolRef [Term str a]
| Refl_Param (Term str a) (Reflection str a)
| Refl_Rec (Ray (Term str a) str a) (Reflection str a)
-- | TODO : make this function return something
toPrismatic :: TypeTerm str a -> Maybe (Prismatic str a)
toPrismatic _ = Nothing
type ListSerializable a = (Serializable ListStream a)
type ListFormat a = (Format ListStream a)
instance ListSerializable BindType
......@@ -610,7 +627,6 @@ mu_type (raiseRefs 1 -> root_type) = yb maybeT $ go 0 root_type
| otherwise = (j,[])
]))
return $ Cons (Ap (Sym i) $ xs+[lastE])
go_col' d' recs (Universe u) = do
let tIH = bind Prod (telescope_adjustRefs second (+(d+d')) root_args) ihRoot
ihRoot = Cons (Ap (Sym (nargs-d-1)) [Cons $ Ap (Sym (j+nargs)) $
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment