Commit 530108cd authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Start implementing the mechanisms for extraction of terms into computational form

parent ba7c9391
......@@ -18,7 +18,7 @@ data-dir: data
data-files: prelude
library
exposed-modules: Algebra.Monad.Concatenative Data.CaPriCon CaPriCon.Run
exposed-modules: Algebra.Monad.Concatenative Data.CaPriCon CaPriCon.Run Data.CaPriCon.Extraction
default-extensions: RebindableSyntax, ViewPatterns, TupleSections, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, FunctionalDependencies, LambdaCase, TypeOperators, RankNTypes, GeneralizedNewtypeDeriving, TypeFamilies
build-depends: base >=4.8 && <4.10,definitive-base >=2.6 && <2.7,definitive-parser >=3.1 && <3.2
if !impl(haste)
......
......@@ -5,6 +5,7 @@ import Definitive
import Language.Format
import Algebra.Monad.Concatenative
import Data.CaPriCon
import Data.CaPriCon.Extraction (Algebraic(..),fromNode)
import GHC.Generics (Generic)
class Monad m => MonadSubIO io m where
......@@ -22,6 +23,7 @@ instance Monoid UniverseConstraints where zero = UniverseConstraints (repeat (re
data COCValue io str = COCExpr (ContextNode str)
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
| COCAlgebraic (Algebraic str)
| COCDir (NodeDir str ([str],StackVal str (COCBuiltin io str) (COCValue io str)))
deriving Generic
instance (ListSerializable s,ListSerializable b,ListSerializable a) => ListSerializable (StackStep s b a)
......@@ -52,6 +54,7 @@ showStackVal toRaw dir ctx = fix $ \go _x -> case _x of
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
COCConvertible conv -> fromString $ show conv
COCAlgebraic a -> fromString $ show a
StackSymbol s -> fromString $ show s
StackInt n -> fromString $ show n
StackList l -> "["+intercalate "," (map go l)+"]"
......@@ -75,7 +78,7 @@ data COCBuiltin io str = COCB_Print
| COCB_HypBefore | COCB_Subst | COCB_Rename
| COCB_ContextVars
| COCB_GetShowDir | COCB_SetShowDir | COCB_InsertNodeDir
| COCB_Format
| COCB_Format | COCB_Extract
deriving (Show,Generic)
data ReadImpl io str bytes = ReadImpl (str -> io (Maybe bytes))
data WriteImpl io str bytes = WriteImpl (str -> bytes -> io ())
......@@ -316,6 +319,12 @@ runCOCBuiltin COCB_ContextVars = do
ctx <- runExtraState (getl context)
runStackState $ modify (StackList (map (StackSymbol . fst) (freshContext ctx)):)
runCOCBuiltin COCB_Extract = do
ctx <- runExtraState (getl context)
runStackState $ modify $ \case
StackCOC (COCExpr (ContextNode d e)):t -> StackCOC (COCAlgebraic (fromNode e ([],takeLast d ctx))):t
st -> st
runCOCBuiltin COCB_GetShowDir = do
dir <- runExtraState (getl showDir)
runStackState $ modify $ (StackCOC (COCDir (map (\(c,l) -> (c,StackSymbol (intercalate " " $ map (id <|> head . flip drop c) l))) dir)):)
......@@ -391,15 +400,16 @@ cocDict version getResource getBResource writeResource writeBResource =
("term/universe" , Builtin_Extra COCB_Uni ),
("term/variable" , Builtin_Extra COCB_Var ),
("term/apply" , Builtin_Extra COCB_Ap ),
("term/lambda" , Builtin_Extra (COCB_Bind False Lambda )),
("term/forall" , Builtin_Extra (COCB_Bind False Prod ) ),
("term/lambda" , Builtin_Extra (COCB_Bind False Lambda)),
("term/forall" , Builtin_Extra (COCB_Bind False Prod )),
("term/mu" , Builtin_Extra COCB_Mu ),
("term/convertible" , Builtin_Extra COCB_Convertible ),
("term/extract" , Builtin_Extra COCB_Extract ),
("context/intro" , Builtin_Extra COCB_Hyp ),
("context/intro-before" , Builtin_Extra COCB_HypBefore ),
("context/extro-lambda" , Builtin_Extra (COCB_Bind True Lambda ) ),
("context/extro-forall" , Builtin_Extra (COCB_Bind True Prod ) ),
("context/extro-lambda" , Builtin_Extra (COCB_Bind True Lambda )),
("context/extro-forall" , Builtin_Extra (COCB_Bind True Prod )),
("context/rename" , Builtin_Extra COCB_Rename ),
("context/substitute" , Builtin_Extra COCB_Subst ),
("context/type" , Builtin_Extra COCB_TypeOf ),
......
{-# LANGUAGE DeriveGeneric #-}
module Data.CaPriCon.Extraction where
import Definitive
import Data.CaPriCon
import Language.Format
import GHC.Generics (Generic)
data Algebraic str = AFun str (AType str) (Algebraic str)
| AApply (Algebraic str) (Algebraic str)
| AVar Int
deriving (Generic)
data AType str = AArr (AType str) (AType str) | ATVar Int | AAny
deriving (Show,Generic)
par lvl d msg | d>lvl = "("+msg+")"
| otherwise = msg
instance IsCapriconString str => Show (Algebraic str) where
show = go 0 []
where go d env (AFun x tx e) = par 0 d $ "fun ("+toString x+" : "+go_t 0 tx+") => "+go 0 (x:env) e
go d env (AApply f x) = par 1 d $ go 1 env f+" "+go 2 env x
go _ env (AVar n) | v:_ <- drop n env = toString v
| otherwise = "__var_"+show n
go_t d (AArr a b) = par 0 d $ go_t 1 a + " -> " + go_t 0 b
go_t _ (ATVar n) = "'a"+show n
go_t _ AAny = "__"
instance Serializable bytes str => Serializable bytes (Algebraic str)
instance Serializable bytes str => Serializable bytes (AType str)
instance Format bytes str => Format bytes (Algebraic str)
instance Format bytes str => Format bytes (AType str)
fromNode :: (IsCapriconString str,MonadReader ([Bool],Env str) m) => Node str -> m (Algebraic str)
fromNode (Bind Lambda x tx e) = do
let isT = isTypeType tx
e' <- local ((not isT:)<#>((x,tx):)) (fromNode e)
if isT then return e'
else AFun x <$> fromTypeNode tx <*> pure e'
fromNode (Cons a) = fromApplication a
fromNode _ = error "Cannot produce a type-term in a language without first-class types"
fromApplication :: (IsCapriconString str, MonadReader ([Bool],Env str) m) => Application str -> m (Algebraic str)
fromApplication (Ap ah args) = do
(varKinds,env) <- ask
let concreteArgs = [arg | (arg,Just t) <- map (\x -> (x,(checkType x^..maybeT) env)) args
, not (isTypeType t)]
case ah of
Sym s -> foldl' (liftA2 AApply) (pure $ AVar $ sum [if isV then 1 else 0 | isV <- take s varKinds]) (map fromNode concreteArgs)
Mu _ _ a -> foldl' (liftA2 AApply) (fromApplication a) (map fromNode concreteArgs)
fromTypeNode :: MonadReader ([Bool],Env str) m => Node str -> m (AType str)
fromTypeNode (Bind Prod x tx e) = do
let isT = isTypeType tx
e' <- local ((not isT:)<#>((x,tx):)) (fromTypeNode e)
if isT then return e'
else AArr <$> fromTypeNode tx <*> pure e'
fromTypeNode (Cons (Ap (Sym s) [])) = do
(varKinds,_) <- ask
pure $ ATVar $ sum [if isV then 0 else 1 | isV <- take s varKinds]
fromTypeNode _ = pure AAny
isTypeType :: Node str -> Bool
isTypeType (Universe _) = True
isTypeType (Bind Prod _ _ e) = isTypeType e
isTypeType _ = False
......@@ -51,8 +51,10 @@
'viewMat Uniform
'projMat Uniform
"Creating window...\n" print
'tile "textures/Pebbles_006_COLOR.jpg" image def
'tileNormals "textures/Pebbles_006_NRM.jpg" image def
"Window created\n" print
'tileTexture Uniform , tile set-tileTexture
'tileTextureNormal Uniform , tileNormals set-tileTextureNormal
......@@ -76,6 +78,7 @@ identity set-modelMat
} each
] def
'refresh { [ 1 1 0 0 vcons translation => cue scene ] draw } def
'dxy vx vx 20 ** vy ++ normalize rotation def
......@@ -121,4 +124,5 @@ view-trans set-viewMat
'loop-body { lightVect east-west { dyz } { dzy } if ** set-lightVect refresh } def
'east-west true def
"press E" { 'east-west { 1 swap - } modify } bind-key
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