mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-21 00:52:51 -06:00
the construct lin C t now replaces lock fields (in source code; still tempor used internally); lock fields removed from english resource as an example
This commit is contained in:
@@ -3,13 +3,11 @@
|
|||||||
resource MakeStructuralEng = open CatEng, ParadigmsEng, ResEng, MorphoEng, Prelude in {
|
resource MakeStructuralEng = open CatEng, ParadigmsEng, ResEng, MorphoEng, Prelude in {
|
||||||
|
|
||||||
oper
|
oper
|
||||||
-- mkConj : Str -> Str -> Number -> Conj = \x,y,n ->
|
|
||||||
-- {s1 = x ; s2 = y ; n = n ; lock_Conj = <>} ;
|
|
||||||
mkSubj : Str -> Subj = \x ->
|
mkSubj : Str -> Subj = \x ->
|
||||||
{s = x ; lock_Subj = <>} ;
|
lin Subj {s = x} ;
|
||||||
mkNP : Str -> Number -> NP = \s,n ->
|
mkNP : Str -> Number -> NP = \s,n ->
|
||||||
regNP s n ** {lock_NP = <>} ;
|
lin NP (regNP s n) ;
|
||||||
mkIDet : Str -> Number -> IDet = \s,n ->
|
mkIDet : Str -> Number -> IDet = \s,n ->
|
||||||
{s = s ; n = n ; lock_IDet = <>} ;
|
lin IDet {s = s ; n = n} ;
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -321,7 +321,7 @@ oper
|
|||||||
|
|
||||||
--2 Other categories
|
--2 Other categories
|
||||||
|
|
||||||
mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
mkSubj : Str -> Subj = \s -> lin Subj {s = s} ;
|
||||||
|
|
||||||
--.
|
--.
|
||||||
--2 Definitions of paradigms
|
--2 Definitions of paradigms
|
||||||
@@ -373,11 +373,11 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
mk4N man men (man + "'s") mens ;
|
mk4N man men (man + "'s") mens ;
|
||||||
|
|
||||||
mk4N = \man,men,man's,men's ->
|
mk4N = \man,men,man's,men's ->
|
||||||
mkNoun man man's men men's ** {g = Neutr ; lock_N = <>} ;
|
lin N (mkNoun man man's men men's ** {g = Neutr}) ;
|
||||||
|
|
||||||
genderN g man = {s = man.s ; g = g ; lock_N = <>} ;
|
genderN g man = lin N {s = man.s ; g = g} ;
|
||||||
|
|
||||||
compoundN s n = {s = \\x,y => s ++ n.s ! x ! y ; g=n.g ; lock_N = <>} ;
|
compoundN s n = lin N {s = \\x,y => s ++ n.s ! x ! y ; g=n.g} ;
|
||||||
|
|
||||||
mkPN = overload {
|
mkPN = overload {
|
||||||
mkPN : Str -> PN = regPN ;
|
mkPN : Str -> PN = regPN ;
|
||||||
@@ -392,10 +392,10 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
mkN2 : Str -> N2 = \s -> prepN2 (regN s) (mkPrep "of")
|
mkN2 : Str -> N2 = \s -> prepN2 (regN s) (mkPrep "of")
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
prepN2 = \n,p -> n ** {lock_N2 = <> ; c2 = p.s} ;
|
prepN2 = \n,p -> lin N2 (n ** {c2 = p.s}) ;
|
||||||
regN2 n = prepN2 (regN n) (mkPrep "of") ;
|
regN2 n = prepN2 (regN n) (mkPrep "of") ;
|
||||||
|
|
||||||
mkN3 = \n,p,q -> n ** {lock_N3 = <> ; c2 = p.s ; c3 = q.s} ;
|
mkN3 = \n,p,q -> lin N3 (n ** {c2 = p.s ; c3 = q.s}) ;
|
||||||
|
|
||||||
--3 Relational common noun phrases
|
--3 Relational common noun phrases
|
||||||
--
|
--
|
||||||
@@ -406,39 +406,39 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
cnN3 : CN -> Prep -> Prep -> N3 ;
|
cnN3 : CN -> Prep -> Prep -> N3 ;
|
||||||
|
|
||||||
-- This is obsolete.
|
-- This is obsolete.
|
||||||
cnN2 = \n,p -> n ** {lock_N2 = <> ; c2 = p.s} ;
|
cnN2 = \n,p -> lin N2 (n ** {c2 = p.s}) ;
|
||||||
cnN3 = \n,p,q -> n ** {lock_N3 = <> ; c2 = p.s ; c3 = q.s} ;
|
cnN3 = \n,p,q -> lin N3 (n ** {c2 = p.s ; c3 = q.s}) ;
|
||||||
|
|
||||||
regPN n = regGenPN n human ;
|
regPN n = regGenPN n human ;
|
||||||
regGenPN n g = {s = table {Gen => n + "'s" ; _ => n} ;
|
regGenPN n g = lin PN {s = table {Gen => n + "'s" ; _ => n} ; g = g} ;
|
||||||
g = g ; lock_PN = <>} ;
|
nounPN n = lin PN {s = n.s ! singular ; g = n.g} ;
|
||||||
nounPN n = {s = n.s ! singular ; g = n.g ; lock_PN = <>} ;
|
|
||||||
|
|
||||||
mkQuant = overload {
|
mkQuant = overload {
|
||||||
mkQuant : (this, these : Str) -> Quant = \sg,pl -> mkQuantifier sg pl sg pl;
|
mkQuant : (this, these : Str) -> Quant = \sg,pl -> mkQuantifier sg pl sg pl;
|
||||||
mkQuant : (no_sg, no_pl, none_sg, non_pl : Str) -> Quant = mkQuantifier;
|
mkQuant : (no_sg, no_pl, none_sg, non_pl : Str) -> Quant = mkQuantifier;
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
mkQuantifier : Str -> Str -> Str -> Str -> Quant = \sg,pl,sg',pl' -> {
|
mkQuantifier : Str -> Str -> Str -> Str -> Quant =
|
||||||
|
\sg,pl,sg',pl' -> lin Quant {
|
||||||
s = \\_ => table { Sg => sg ; Pl => pl } ;
|
s = \\_ => table { Sg => sg ; Pl => pl } ;
|
||||||
sp = \\_ => table { Sg => regGenitiveS sg' ; Pl => regGenitiveS pl' } ;
|
sp = \\_ => table { Sg => regGenitiveS sg' ; Pl => regGenitiveS pl'}
|
||||||
lock_Quant = <>
|
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
mkOrd : Str -> Ord = \x -> { s = regGenitiveS x; lock_Ord = <> };
|
mkOrd : Str -> Ord = \x -> lin Ord { s = regGenitiveS x};
|
||||||
|
|
||||||
mk2A a b = mkAdjective a a a b ** {lock_A = <>} ;
|
mk2A a b = lin A (mkAdjective a a a b) ;
|
||||||
regA a = case a of {
|
regA a = case a of {
|
||||||
_ + ("a" | "e" | "i" | "o" | "u" | "y") + ? + _ +
|
_ + ("a" | "e" | "i" | "o" | "u" | "y") + ? + _ +
|
||||||
("a" | "e" | "i" | "o" | "u" | "y") + ? + _ => compoundADeg (regADeg a) ;
|
("a" | "e" | "i" | "o" | "u" | "y") + ? + _ =>
|
||||||
_ => regADeg a
|
lin A (compoundADeg (regADeg a)) ;
|
||||||
} ** {lock_A = <>} ;
|
_ => lin A (regADeg a)
|
||||||
|
} ;
|
||||||
|
|
||||||
prepA2 a p = a ** {c2 = p.s ; lock_A2 = <>} ;
|
prepA2 a p = lin A2 (a ** {c2 = p.s}) ;
|
||||||
|
|
||||||
ADeg = A ; ----
|
ADeg = A ; ----
|
||||||
|
|
||||||
mkADeg a b c d = mkAdjective a b c d ** {lock_A = <>} ;
|
mkADeg a b c d = lin A (mkAdjective a b c d) ;
|
||||||
|
|
||||||
regADeg happy =
|
regADeg happy =
|
||||||
let
|
let
|
||||||
@@ -466,15 +466,15 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
|
|
||||||
adegA a = a ;
|
adegA a = a ;
|
||||||
|
|
||||||
mkAdv x = ss x ** {lock_Adv = <>} ;
|
mkAdv x = lin Adv (ss x) ;
|
||||||
mkAdV x = ss x ** {lock_AdV = <>} ;
|
mkAdV x = lin AdV (ss x) ;
|
||||||
mkAdA x = ss x ** {lock_AdA = <>} ;
|
mkAdA x = lin AdA (ss x) ;
|
||||||
mkAdN x = ss x ** {lock_AdN = <>} ;
|
mkAdN x = lin AdN (ss x) ;
|
||||||
|
|
||||||
mkPrep p = ss p ** {lock_Prep = <>} ;
|
mkPrep p = lin Prep (ss p) ;
|
||||||
noPrep = mkPrep [] ;
|
noPrep = mkPrep [] ;
|
||||||
|
|
||||||
mk5V a b c d e = mkVerb a b c d e ** {s1 = [] ; lock_V = <>} ;
|
mk5V a b c d e = lin V (mkVerb a b c d e ** {s1 = []}) ;
|
||||||
|
|
||||||
regV cry =
|
regV cry =
|
||||||
let
|
let
|
||||||
@@ -505,10 +505,10 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
} ;
|
} ;
|
||||||
|
|
||||||
irregV x y z = let reg = (regV x).s in
|
irregV x y z = let reg = (regV x).s in
|
||||||
mk5V x (reg ! VPres) y z (reg ! VPresPart) ** {s1 = [] ; lock_V = <>} ;
|
mk5V x (reg ! VPres) y z (reg ! VPresPart) ** {s1 = []} ;
|
||||||
|
|
||||||
irreg4V x y z w = let reg = (regV x).s in
|
irreg4V x y z w = let reg = (regV x).s in
|
||||||
mk5V x (reg ! VPres) y z w ** {s1 = [] ; lock_V = <>} ;
|
mk5V x (reg ! VPres) y z w ** {s1 = []} ;
|
||||||
|
|
||||||
irregDuplV fit y z =
|
irregDuplV fit y z =
|
||||||
let
|
let
|
||||||
@@ -516,40 +516,41 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
in
|
in
|
||||||
mk5V fit (fit + "s") y z fitting ;
|
mk5V fit (fit + "s") y z fitting ;
|
||||||
|
|
||||||
partV v p = {s = \\f => v.s ! f ++ p ; isRefl = v.isRefl ; lock_V = <>} ;
|
partV v p = lin V {s = \\f => v.s ! f ++ p ; isRefl = v.isRefl} ;
|
||||||
reflV v = {s = v.s ; part = v.part ; lock_V = v.lock_V ; isRefl = True} ;
|
reflV v = lin V {s = v.s ; part = v.part ; isRefl = True} ;
|
||||||
|
|
||||||
prepV2 v p = v ** {s = v.s ; s1 = v.s1 ; c2 = p.s ; lock_V2 = <>} ;
|
prepV2 v p = lin V2 {s = v.s ; s1 = v.s1 ; c2 = p.s ; isRefl = v.isRefl} ;
|
||||||
dirV2 v = prepV2 v noPrep ;
|
dirV2 v = prepV2 v noPrep ;
|
||||||
|
|
||||||
prepPrepV3 v p q = v ** {s = v.s ; s1 = v.s1 ; c2 = p.s ; c3 = q.s ; lock_V3 = <>} ;
|
prepPrepV3 v p q =
|
||||||
|
lin V3 {s = v.s ; s1 = v.s1 ; c2 = p.s ; c3 = q.s ; isRefl = v.isRefl} ;
|
||||||
dirV3 v p = prepPrepV3 v noPrep p ;
|
dirV3 v p = prepPrepV3 v noPrep p ;
|
||||||
dirdirV3 v = dirV3 v noPrep ;
|
dirdirV3 v = dirV3 v noPrep ;
|
||||||
|
|
||||||
mkVS v = v ** {lock_VS = <>} ;
|
mkVS v = lin VS v ;
|
||||||
mkVV v = {
|
mkVV v = lin VV {
|
||||||
s = table {VVF vf => v.s ! vf ; _ => v.s ! VInf} ;
|
s = table {VVF vf => v.s ! vf ; _ => v.s ! VInf} ;
|
||||||
--- variants {}} ; not used
|
--- variants {}} ; not used
|
||||||
isAux = False ; lock_VV = <>
|
isAux = False
|
||||||
} ;
|
} ;
|
||||||
mkVQ v = v ** {lock_VQ = <>} ;
|
mkVQ v = v ;
|
||||||
|
|
||||||
V0 : Type = V ;
|
V0 : Type = V ;
|
||||||
-- V2S, V2V, V2Q : Type = V2 ;
|
-- V2S, V2V, V2Q : Type = V2 ;
|
||||||
AS, A2S, AV : Type = A ;
|
AS, A2S, AV : Type = A ;
|
||||||
A2V : Type = A2 ;
|
A2V : Type = A2 ;
|
||||||
|
|
||||||
mkV0 v = v ** {lock_V = <>} ;
|
mkV0 v = v ;
|
||||||
mkV2S v p = prepV2 v p ** {lock_V2S = <>} ;
|
mkV2S v p = prepV2 v p ;
|
||||||
mkV2V v p t = prepV2 v p ** {isAux = False ; lock_V2V = <>} ;
|
mkV2V v p t = lin V2V (prepV2 v p ** {isAux = False}) ;
|
||||||
mkVA v = v ** {lock_VA = <>} ;
|
mkVA v = v ;
|
||||||
mkV2A v p = prepV2 v p ** {lock_V2A = <>} ;
|
mkV2A v p = prepV2 v p ;
|
||||||
mkV2Q v p = prepV2 v p ** {lock_V2Q = <>} ;
|
mkV2Q v p = prepV2 v p ;
|
||||||
|
|
||||||
mkAS v = v ** {lock_A = <>} ;
|
mkAS v = v ;
|
||||||
mkA2S v p = prepA2 v p ** {lock_A = <>} ;
|
mkA2S v p = prepA2 v p ;
|
||||||
mkAV v = v ** {lock_A = <>} ;
|
mkAV v = v ;
|
||||||
mkA2V v p = prepA2 v p ** {lock_A2 = <>} ;
|
mkA2V v p = prepA2 v p ;
|
||||||
|
|
||||||
|
|
||||||
-- pre-overload API and overload definitions
|
-- pre-overload API and overload definitions
|
||||||
@@ -583,9 +584,9 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
mkA = overload {
|
mkA = overload {
|
||||||
mkA : Str -> A = regA ;
|
mkA : Str -> A = regA ;
|
||||||
mkA : (fat,fatter : Str) -> A = \fat,fatter ->
|
mkA : (fat,fatter : Str) -> A = \fat,fatter ->
|
||||||
mkAdjective fat fatter (init fatter + "st") (fat + "ly") ** {lock_A = <>} ;
|
mkAdjective fat fatter (init fatter + "st") (fat + "ly") ;
|
||||||
mkA : (good,better,best,well : Str) -> A = \a,b,c,d ->
|
mkA : (good,better,best,well : Str) -> A = \a,b,c,d ->
|
||||||
mkAdjective a b c d ** {lock_A = <>}
|
mkAdjective a b c d
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
compoundA = compoundADeg ;
|
compoundA = compoundADeg ;
|
||||||
@@ -655,7 +656,8 @@ mkSubj : Str -> Subj = \s -> {s = s ; lock_Subj = <>} ;
|
|||||||
mkConj : Str -> Str -> Number -> Conj = mk2Conj ;
|
mkConj : Str -> Str -> Number -> Conj = mk2Conj ;
|
||||||
} ;
|
} ;
|
||||||
|
|
||||||
mk2Conj : Str -> Str -> Number -> Conj = \x,y,n -> sd2 x y ** { n = n; lock_Conj = <> } ;
|
mk2Conj : Str -> Str -> Number -> Conj = \x,y,n ->
|
||||||
|
lin Conj (sd2 x y ** {n = n}) ;
|
||||||
|
|
||||||
---- obsolete
|
---- obsolete
|
||||||
|
|
||||||
|
|||||||
@@ -38,7 +38,7 @@ import GF.Grammar.Predef
|
|||||||
import GF.Grammar.Macros
|
import GF.Grammar.Macros
|
||||||
import GF.Grammar.PatternMatch
|
import GF.Grammar.PatternMatch
|
||||||
import GF.Grammar.AppPredefined
|
import GF.Grammar.AppPredefined
|
||||||
import GF.Grammar.Lockfield (isLockLabel)
|
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
import GF.Infra.CheckM
|
import GF.Infra.CheckM
|
||||||
@@ -396,6 +396,10 @@ computeLType gr t = do
|
|||||||
let fs' = sortRec fs
|
let fs' = sortRec fs
|
||||||
liftM RecType $ mapPairsM comp fs'
|
liftM RecType $ mapPairsM comp fs'
|
||||||
|
|
||||||
|
ELincat c t -> do
|
||||||
|
t' <- comp t
|
||||||
|
checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
|
||||||
|
|
||||||
_ | ty == typeTok -> return typeStr
|
_ | ty == typeTok -> return typeStr
|
||||||
_ | isPredefConstant ty -> return ty
|
_ | isPredefConstant ty -> return ty
|
||||||
|
|
||||||
@@ -599,6 +603,11 @@ inferLType gr trm = case trm of
|
|||||||
ty <- inferPatt p
|
ty <- inferPatt p
|
||||||
return (trm, EPattType ty)
|
return (trm, EPattType ty)
|
||||||
|
|
||||||
|
ELin c trm -> do
|
||||||
|
(trm',ty) <- infer trm
|
||||||
|
ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
|
||||||
|
return $ (ELin c trm', ty')
|
||||||
|
|
||||||
_ -> prtFail "cannot infer lintype of" trm
|
_ -> prtFail "cannot infer lintype of" trm
|
||||||
|
|
||||||
where
|
where
|
||||||
@@ -861,6 +870,10 @@ checkLType env trm typ0 = do
|
|||||||
(def',ty) <- infer def -- tries to infer type of local constant
|
(def',ty) <- infer def -- tries to infer type of local constant
|
||||||
check (Let (x,(Just ty,def')) body) typ
|
check (Let (x,(Just ty,def')) body) typ
|
||||||
|
|
||||||
|
ELin c tr -> do
|
||||||
|
tr1 <- checkErr $ unlockRecord c tr
|
||||||
|
check tr1 typ
|
||||||
|
|
||||||
_ -> do
|
_ -> do
|
||||||
(trm',ty') <- infer trm
|
(trm',ty') <- infer trm
|
||||||
termWith trm' $ checkEq typ ty' trm'
|
termWith trm' $ checkEq typ ty' trm'
|
||||||
@@ -886,7 +899,14 @@ checkLType env trm typ0 = do
|
|||||||
Just (_,t) -> do
|
Just (_,t) -> do
|
||||||
(t',ty') <- check t ty
|
(t',ty') <- check t ty
|
||||||
return (l,(Just ty',t'))
|
return (l,(Just ty',t'))
|
||||||
_ -> raise $ "cannot find value for label" +++ prt l +++ "in" +++ prt_ (R rms)
|
_ -> raise $
|
||||||
|
if isLockLabel l
|
||||||
|
then
|
||||||
|
let cat = drop 5 (prt l) in
|
||||||
|
prt_ (R rms) +++ "is not in the lincat of" +++ cat ++
|
||||||
|
"; try wrapping it with lin " ++ cat
|
||||||
|
else
|
||||||
|
"cannot find value for label" +++ prt l +++ "in" +++ prt_ (R rms)
|
||||||
|
|
||||||
checkCase arg val (p,t) = do
|
checkCase arg val (p,t) = do
|
||||||
cont <- pattContext env arg p
|
cont <- pattContext env arg p
|
||||||
|
|||||||
@@ -26,7 +26,7 @@ import GF.Grammar.Macros
|
|||||||
import GF.Grammar.Lookup
|
import GF.Grammar.Lookup
|
||||||
import GF.Compile.Refresh
|
import GF.Compile.Refresh
|
||||||
import GF.Grammar.PatternMatch
|
import GF.Grammar.PatternMatch
|
||||||
import GF.Grammar.Lockfield (isLockLabel) ----
|
import GF.Grammar.Lockfield (isLockLabel,unlockRecord) ----
|
||||||
|
|
||||||
import GF.Grammar.AppPredefined
|
import GF.Grammar.AppPredefined
|
||||||
|
|
||||||
@@ -219,6 +219,10 @@ computeTermOpt rec gr = comput True where
|
|||||||
(RecType rs, RecType ss) -> plusRecType r' s'
|
(RecType rs, RecType ss) -> plusRecType r' s'
|
||||||
_ -> return $ ExtR r' s'
|
_ -> return $ ExtR r' s'
|
||||||
|
|
||||||
|
ELin c r -> do
|
||||||
|
r' <- comp g r
|
||||||
|
unlockRecord c r'
|
||||||
|
|
||||||
T _ _ -> compTable g t
|
T _ _ -> compTable g t
|
||||||
V _ _ -> compTable g t
|
V _ _ -> compTable g t
|
||||||
|
|
||||||
|
|||||||
@@ -148,6 +148,8 @@ instance Binary Term where
|
|||||||
put (FV x) = putWord8 35 >> put x
|
put (FV x) = putWord8 35 >> put x
|
||||||
put (Alts x) = putWord8 36 >> put x
|
put (Alts x) = putWord8 36 >> put x
|
||||||
put (Strs x) = putWord8 37 >> put x
|
put (Strs x) = putWord8 37 >> put x
|
||||||
|
put (ELin x y) = putWord8 38 >> put (x,y)
|
||||||
|
|
||||||
get = do tag <- getWord8
|
get = do tag <- getWord8
|
||||||
case tag of
|
case tag of
|
||||||
0 -> get >>= \x -> return (Vr x)
|
0 -> get >>= \x -> return (Vr x)
|
||||||
@@ -186,6 +188,7 @@ instance Binary Term where
|
|||||||
35 -> get >>= \x -> return (FV x)
|
35 -> get >>= \x -> return (FV x)
|
||||||
36 -> get >>= \x -> return (Alts x)
|
36 -> get >>= \x -> return (Alts x)
|
||||||
37 -> get >>= \x -> return (Strs x)
|
37 -> get >>= \x -> return (Strs x)
|
||||||
|
38 -> get >>= \(x,y) -> return (ELin x y)
|
||||||
_ -> decodingError
|
_ -> decodingError
|
||||||
|
|
||||||
instance Binary Patt where
|
instance Binary Patt where
|
||||||
|
|||||||
@@ -147,6 +147,9 @@ data Term =
|
|||||||
| EPatt Patt -- ^ pattern (in macro definition): # p
|
| EPatt Patt -- ^ pattern (in macro definition): # p
|
||||||
| EPattType Term -- ^ pattern type: pattern T
|
| EPattType Term -- ^ pattern type: pattern T
|
||||||
|
|
||||||
|
| ELincat Ident Term -- ^ boxed linearization type of Ident
|
||||||
|
| ELin Ident Term -- ^ boxed linearization of type Ident
|
||||||
|
|
||||||
| FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@
|
| FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@
|
||||||
|
|
||||||
| Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
|
| Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
|
||||||
|
|||||||
@@ -36,8 +36,10 @@ lockRecType c t = plusRecType t $ RecType [(lockLabel c, RecType [])]
|
|||||||
unlockRecord :: Ident -> Term -> Err Term
|
unlockRecord :: Ident -> Term -> Err Term
|
||||||
unlockRecord c ft = do
|
unlockRecord c ft = do
|
||||||
let (xs,t) = termFormCnc ft
|
let (xs,t) = termFormCnc ft
|
||||||
t' <- plusRecord t $ R [(lockLabel c, (Just (RecType []),R []))]
|
let lock = R [(lockLabel c, (Just (RecType []),R []))]
|
||||||
return $ mkAbs xs t'
|
case plusRecord t lock of
|
||||||
|
Ok t' -> return $ mkAbs xs t'
|
||||||
|
_ -> return $ mkAbs xs (ExtR t lock)
|
||||||
|
|
||||||
lockLabel :: Ident -> Label
|
lockLabel :: Ident -> Label
|
||||||
lockLabel c = LIdent $! BS.append lockPrefix (ident2bs c)
|
lockLabel c = LIdent $! BS.append lockPrefix (ident2bs c)
|
||||||
|
|||||||
@@ -634,6 +634,14 @@ composOp co trm =
|
|||||||
do ty' <- co ty
|
do ty' <- co ty
|
||||||
return (EPattType ty')
|
return (EPattType ty')
|
||||||
|
|
||||||
|
ELincat c ty ->
|
||||||
|
do ty' <- co ty
|
||||||
|
return (ELincat c ty')
|
||||||
|
|
||||||
|
ELin c ty ->
|
||||||
|
do ty' <- co ty
|
||||||
|
return (ELin c ty')
|
||||||
|
|
||||||
_ -> return trm -- covers K, Vr, Cn, Sort, EPatt
|
_ -> return trm -- covers K, Vr, Cn, Sort, EPatt
|
||||||
|
|
||||||
getTableType :: TInfo -> Err Type
|
getTableType :: TInfo -> Err Type
|
||||||
|
|||||||
File diff suppressed because one or more lines are too long
@@ -423,6 +423,8 @@ Exp4
|
|||||||
| 'strs' '{' ListExp '}' { Strs $3 }
|
| 'strs' '{' ListExp '}' { Strs $3 }
|
||||||
| '#' Patt2 { EPatt $2 }
|
| '#' Patt2 { EPatt $2 }
|
||||||
| 'pattern' Exp5 { EPattType $2 }
|
| 'pattern' Exp5 { EPattType $2 }
|
||||||
|
| 'lincat' Ident Exp5 { ELincat $2 $3 }
|
||||||
|
| 'lin' Ident Exp5 { ELin $2 $3 }
|
||||||
| Exp5 { $1 }
|
| Exp5 { $1 }
|
||||||
|
|
||||||
Exp5 :: { Term }
|
Exp5 :: { Term }
|
||||||
|
|||||||
Reference in New Issue
Block a user