mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 19:42:50 -06:00
simplify the Term again
This commit is contained in:
@@ -132,8 +132,6 @@ computeTermOpt rec gr = comput True where
|
|||||||
|
|
||||||
_ -> returnC $ P t' l
|
_ -> returnC $ P t' l
|
||||||
|
|
||||||
PI t l i -> comp g $ P t l -----
|
|
||||||
|
|
||||||
S t v -> do
|
S t v -> do
|
||||||
t' <- compTable g t
|
t' <- compTable g t
|
||||||
v' <- comp g v
|
v' <- comp g v
|
||||||
|
|||||||
@@ -131,7 +131,6 @@ inferLType gr g trm = case trm of
|
|||||||
Just x -> return x
|
Just x -> return x
|
||||||
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
|
_ -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
|
||||||
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
|
text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
|
||||||
PI t i _ -> inferLType gr g $ P t i
|
|
||||||
|
|
||||||
R r -> do
|
R r -> do
|
||||||
let (ls,fs) = unzip r
|
let (ls,fs) = unzip r
|
||||||
|
|||||||
@@ -436,7 +436,6 @@ term2term fun cgr env@(labels,untyps,typs) tr = case tr of
|
|||||||
R rs -> R [(mkLab i, (Nothing, t2t t)) |
|
R rs -> R [(mkLab i, (Nothing, t2t t)) |
|
||||||
(i,(l,(_,t))) <- zip [0..] (GM.sortRec (unlock rs))]
|
(i,(l,(_,t))) <- zip [0..] (GM.sortRec (unlock rs))]
|
||||||
P t l -> r2r tr
|
P t l -> r2r tr
|
||||||
PI t l i -> EInt $ toInteger i
|
|
||||||
|
|
||||||
T (TWild _) _ -> error $ (render (text "wild" <+> ppTerm Qualified 0 tr))
|
T (TWild _) _ -> error $ (render (text "wild" <+> ppTerm Qualified 0 tr))
|
||||||
T (TComp ty) cs -> t2t $ V ty $ map snd cs ---- should be elim'ed in tc
|
T (TComp ty) cs -> t2t $ V ty $ map snd cs ---- should be elim'ed in tc
|
||||||
|
|||||||
@@ -136,7 +136,6 @@ instance Binary Term where
|
|||||||
put (RecType x) = putWord8 16 >> put x
|
put (RecType x) = putWord8 16 >> put x
|
||||||
put (R x) = putWord8 17 >> put x
|
put (R x) = putWord8 17 >> put x
|
||||||
put (P x y) = putWord8 18 >> put (x,y)
|
put (P x y) = putWord8 18 >> put (x,y)
|
||||||
put (PI x y z) = putWord8 19 >> put (x,y,z)
|
|
||||||
put (ExtR x y) = putWord8 20 >> put (x,y)
|
put (ExtR x y) = putWord8 20 >> put (x,y)
|
||||||
put (Table x y) = putWord8 21 >> put (x,y)
|
put (Table x y) = putWord8 21 >> put (x,y)
|
||||||
put (T x y) = putWord8 22 >> put (x,y)
|
put (T x y) = putWord8 22 >> put (x,y)
|
||||||
@@ -173,7 +172,6 @@ instance Binary Term where
|
|||||||
16 -> get >>= \x -> return (RecType x)
|
16 -> get >>= \x -> return (RecType x)
|
||||||
17 -> get >>= \x -> return (R x)
|
17 -> get >>= \x -> return (R x)
|
||||||
18 -> get >>= \(x,y) -> return (P x y)
|
18 -> get >>= \(x,y) -> return (P x y)
|
||||||
19 -> get >>= \(x,y,z) -> return (PI x y z)
|
|
||||||
20 -> get >>= \(x,y) -> return (ExtR x y)
|
20 -> get >>= \(x,y) -> return (ExtR x y)
|
||||||
21 -> get >>= \(x,y) -> return (Table x y)
|
21 -> get >>= \(x,y) -> return (Table x y)
|
||||||
22 -> get >>= \(x,y) -> return (T x y)
|
22 -> get >>= \(x,y) -> return (T x y)
|
||||||
|
|||||||
@@ -131,7 +131,6 @@ data Term =
|
|||||||
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
|
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
|
||||||
| R [Assign] -- ^ record: @{ p = a ; ...}@
|
| R [Assign] -- ^ record: @{ p = a ; ...}@
|
||||||
| P Term Label -- ^ projection: @r.p@
|
| P Term Label -- ^ projection: @r.p@
|
||||||
| PI Term Label Int -- ^ index-annotated projection
|
|
||||||
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
|
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
|
||||||
|
|
||||||
| Table Term Term -- ^ table type: @P => A@
|
| Table Term Term -- ^ table type: @P => A@
|
||||||
|
|||||||
@@ -484,9 +484,6 @@ composOp co trm =
|
|||||||
P t i ->
|
P t i ->
|
||||||
do t' <- co t
|
do t' <- co t
|
||||||
return (P t' i)
|
return (P t' i)
|
||||||
PI t i j ->
|
|
||||||
do t' <- co t
|
|
||||||
return (PI t' i j)
|
|
||||||
ExtR a c ->
|
ExtR a c ->
|
||||||
do a' <- co a
|
do a' <- co a
|
||||||
c' <- co c
|
c' <- co c
|
||||||
|
|||||||
Reference in New Issue
Block a user