Commit 5bbdcafd authored by Marc Coiffier's avatar Marc Coiffier
Browse files

Successful build (on Thu May 2 01:44:50 CEST 2019)

parent 43fed0d2
......@@ -3,7 +3,7 @@ module Data.CaPriCon(
-- * Expression nodes
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,
adjust_depth,adjust_telescope_depth,inc_depth,map_univs,free_vars,is_free_in,
-- ** Expression directories
StringPattern,NodeDir(..),AHDir(..),ApDir,
findPattern,freshContext,
......@@ -56,7 +56,9 @@ data Term str a = Bind BindType str (TypeTerm str a) (Term str a)
| Universe UniverseSize
deriving (Show,Generic)
type TypeTerm str a = Term str a
data ApHead str a = Sym SymbolRef | Mu [(str,TypeTerm str a,TypeTerm str a)] [Term str a] (Application str a) | Axiom (Term str a) a
data ApHead str a = Sym SymbolRef
| Mu [(str,TypeTerm str a,TypeTerm str a)] [Term str a] (Application str a)
| Axiom (Term str a) a
deriving (Show,Generic)
data Application str a = Ap (ApHead str a) [Term str a]
deriving (Show,Generic)
......@@ -323,6 +325,15 @@ adjust_depth f = go 0
(go_a (d+length env) a')) (map (go d) subs)
go_a d (Ap x@(Axiom _ _) subs) = Ap x (map (go d) subs)
map_univs f = go
where go (Bind t x tx e) = Bind t x (go tx) (go e)
go (Universe u) = Universe (f u)
go (Cons a) = Cons (go_a a)
go_a (Ap h subs) = Ap (go_ah h) (map go subs)
go_ah (Mu e t a) = Mu (map (\(x,y,z) -> (x,go y,go z)) e) (map go t) (go_a a)
go_ah (Axiom t a) = Axiom (go t) a
go_ah x = x
inc_depth 0 = \x -> x
inc_depth dx = adjust_depth (+dx)
adjust_telescope_depth field f = zipWith (field . adjust_depth . \i j -> if j<i then j else i+f (j-i)) [0..]
......
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