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

Successful build (on Thu May 2 01:25:27 CEST 2019)

parent aba21bbc
......@@ -15,12 +15,6 @@ instance MonadSubIO io m => MonadSubIO io (ConcatT st b o s m) where
liftSubIO ma = lift $ liftSubIO ma
type COCAxiom str = str
type MaxDelta = Int
type UniverseConstraint = [Maybe MaxDelta]
data UniverseConstraints = UniverseConstraints [UniverseConstraint]
instance Semigroup UniverseConstraints where
UniverseConstraints x + UniverseConstraints y = UniverseConstraints $ zipWith (zipWith (\_x _y -> zipWith max _x _y + _x + _y)) x y
instance Monoid UniverseConstraints where zero = UniverseConstraints (repeat (repeat Nothing))
data COCValue io str = COCExpr (ContextTerm str (COCAxiom str))
| COCNull | COCError str
| COCConvertible (Maybe (Int,Int))
......@@ -52,8 +46,8 @@ takeLast n l = drop (length l-n) l
showStackVal :: IsCapriconString str => (NodeDoc str -> str) -> NodeDir str (COCAxiom str) ([str],StringPattern str) -> [(str,Term str (COCAxiom str))] -> StackVal str (COCBuiltin io str) (COCValue io str) -> str
showStackVal toRaw dir ctx = fix $ \go _x -> case _x of
StackCOC _x -> case _x of
COCExpr (ContextTerm d uc e) -> -- "<"+show d+">:"+
fromString (show uc) + toRaw (showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e)
COCExpr (ContextTerm d (UniverseConstraints uc) e) -> -- "<"+show d+">:"+
fromString (show (take d uc)) + toRaw (showNode' dir (map (second snd) $ takeLast d (freshContext ctx)) e)
COCNull -> "(null)"
COCError e -> "<!"+e+"!>"
COCDir d -> fromString $ show d
......
{-# LANGUAGE UndecidableInstances, OverloadedStrings, NoMonomorphismRestriction, DeriveGeneric, ConstraintKinds #-}
module Data.CaPriCon(
-- * Expression nodes
IsCapriconString(..),BindType(..),Term(..),ApHead(..),Application(..),ContextTerm(..),Env,DependentLogic(..),
IsCapriconString(..),BindType(..),Term(..),ApHead(..),Application(..),ContextTerm(..),Env,UniverseConstraints(..),DependentLogic(..),
-- ** Managing De Bruijin indices
adjust_depth,adjust_telescope_depth,inc_depth,free_vars,is_free_in,
-- ** Expression directories
......@@ -150,6 +150,7 @@ shiftConstraints :: Int -> UniverseConstraints -> UniverseConstraints
shiftConstraints n (UniverseConstraints x) | n < 0 = UniverseConstraints (drop (-n) x)
| otherwise = UniverseConstraints (take n (repeat Nothing) + x)
data ContextTerm str a = ContextTerm SymbolRef UniverseConstraints (Term str a)
deriving (Show,Generic)
instance (ListSerializable a,ListSerializable str) => ListSerializable (ContextTerm str a)
......
Supports Markdown
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