Commit 0be41cd1 authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Fix *OfSize being used where *UpToSize was intended

parent f855392c
......@@ -4,44 +4,14 @@ import Control.Applicative
import Comble
import Test.QuickCheck
data Term = TmVar Variable
| TmAbs Term Type
| TmApp Term Term
| TmTApp Term Type
| TmTAbs Term
| TmTop
| TmTuple Term Term
| TmInt Int
| TmCast Coercion Term
deriving(Show, Eq)
data Type = TyVar Variable
| TyArr Type Type
| TyAll Type
| TyInt
| TyTop
| TyProd Type Type
deriving(Show, Eq)
data Coercion = CoId
| CoTrans Coercion Coercion
| CoTop Type
| CoBot Type
| CoArrow Coercion Coercion
| CoTuple Coercion Coercion
| CoProj1 Type
| CoProj2 Type
| CoAll Coercion
| CoDistArrow
| CoTopArrow
| CoTopAll
| CoDistAll
deriving(Show, Eq)
data Variable = Z
| STermVar Variable
| STypeVar Variable
deriving(Show, Eq)
data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
data Term = TmVar Variable | TmAbs Term Type | TmApp Term Term | TmTApp Term Type | TmTAbs Term | TmTop | TmTuple Term Term | TmInt Int | TmCast Coercion Term deriving(Show, Eq)
data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyInt | TyTop | TyProd Type Type deriving(Show, Eq)
data Coercion = CoId | CoTrans Coercion Coercion | CoTop Type | CoBot Type | CoArrow Coercion Coercion | CoTuple Coercion Coercion | CoProj1 Type | CoProj2 Type | CoAll Coercion | CoDistArrow | CoTopArrow | CoTopAll | CoDistAll deriving(Show, Eq)
plus (Z) h = h
plus h (Z) = h
......@@ -160,12 +130,12 @@ termOfSize env 0 nType nCoercion = (empty)
termOfSize env 1 nType nCoercion = ((TmVar <$> (getTermVar env (Z)))
<|> (pure TmTop)
<|> (TmInt <$> (genInt)))
termOfSize env nTerm nType nCoercion = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType nCoercion) <*> (typeOfSize (typeEnv env) nType))
termOfSize env nTerm nType nCoercion = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType nCoercion) <*> (typeUpToSize (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (termOfSize (termEnv env) ((!!) l 0) nType nCoercion) <*> (termOfSize (termEnv env) ((!!) l 1) nType nCoercion))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType nCoercion) <*> (typeOfSize (typeEnv env) nType))
<|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType nCoercion) <*> (typeUpToSize (typeEnv env) nType))
<|> (TmTAbs <$> (termOfSize (termEnv (STypeVar env)) (nTerm - 1) nType nCoercion))
<|> (asum (map (\l -> (TmTuple <$> (termOfSize (termEnv env) ((!!) l 0) nType nCoercion) <*> (termOfSize (termEnv env) ((!!) l 1) nType nCoercion))) (splitn 2 (nTerm - 1))))
<|> (TmCast <$> (coercionOfSize (coercionEnv env) nCoercion nType) <*> (termOfSize (termEnv env) (nTerm - 1) nType nCoercion)))
<|> (TmCast <$> (coercionUpToSize (coercionEnv env) nCoercion nType) <*> (termOfSize (termEnv env) (nTerm - 1) nType nCoercion)))
termUpToSize env 0 nType nCoercion = (empty)
termUpToSize env nTerm nType nCoercion = ((termUpToSize env (nTerm - 1) nType nCoercion)
......@@ -203,10 +173,10 @@ forTypeWithSize env nType prop = (let c = (typeOfSize env nType)
coercionOfSize env 0 nType = (empty)
coercionOfSize env 1 nType = ((pure CoId)
<|> (CoTop <$> (typeOfSize (typeEnv env) nType))
<|> (CoBot <$> (typeOfSize (typeEnv env) nType))
<|> (CoProj1 <$> (typeOfSize (typeEnv env) nType))
<|> (CoProj2 <$> (typeOfSize (typeEnv env) nType))
<|> (CoTop <$> (typeUpToSize (typeEnv env) nType))
<|> (CoBot <$> (typeUpToSize (typeEnv env) nType))
<|> (CoProj1 <$> (typeUpToSize (typeEnv env) nType))
<|> (CoProj2 <$> (typeUpToSize (typeEnv env) nType))
<|> (pure CoDistArrow)
<|> (pure CoTopArrow)
<|> (pure CoTopAll)
......
......@@ -4,14 +4,12 @@ import Control.Applicative
import Comble
import Test.QuickCheck
data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
data FiTerm = TmVar Variable | TmInt Int | TmTop | TmAbs FiTerm FiType | TmApp FiTerm FiTerm | TmMerge FiTerm FiTerm | TmAnn FiTerm FiType | TmRecord FiTerm String | TmProj FiTerm String | TmAll FiType FiTerm | TypeApp FiTerm FiType deriving(Show, Eq)
data FiType = TyTop | TyBot | TyInt | TyArr FiType FiType | TyAnd FiType FiType | TyRecord FiType String | TyVar Variable | TyAll FiType FiType deriving(Show, Eq)
data Variable = Z
| STermVar Variable
| STypeVar Variable
deriving(Show, Eq)
plus (Z) h = h
plus h (Z) = h
......@@ -104,14 +102,14 @@ fiTermOfSize env 0 nFiType = (empty)
fiTermOfSize env 1 nFiType = ((TmVar <$> (getTermVar env (Z)))
<|> (TmInt <$> (genInt))
<|> (pure TmTop))
fiTermOfSize env nFiTerm nFiType = ((TmAbs <$> (fiTermOfSize (fiTermEnv (STermVar env)) (nFiTerm - 1) nFiType) <*> (fiTypeOfSize (fiTypeEnv env) nFiType))
fiTermOfSize env nFiTerm nFiType = ((TmAbs <$> (fiTermOfSize (fiTermEnv (STermVar env)) (nFiTerm - 1) nFiType) <*> (fiTypeUpToSize (fiTypeEnv env) nFiType))
<|> (asum (map (\l -> (TmApp <$> (fiTermOfSize (fiTermEnv env) ((!!) l 0) nFiType) <*> (fiTermOfSize (fiTermEnv env) ((!!) l 1) nFiType))) (splitn 2 (nFiTerm - 1))))
<|> (asum (map (\l -> (TmMerge <$> (fiTermOfSize (fiTermEnv env) ((!!) l 0) nFiType) <*> (fiTermOfSize (fiTermEnv env) ((!!) l 1) nFiType))) (splitn 2 (nFiTerm - 1))))
<|> (TmAnn <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (fiTypeOfSize (fiTypeEnv env) nFiType))
<|> (TmAnn <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (fiTypeUpToSize (fiTypeEnv env) nFiType))
<|> (TmRecord <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (genString))
<|> (TmProj <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (genString))
<|> (TmAll <$> (fiTypeOfSize (fiTypeEnv env) nFiType) <*> (fiTermOfSize (fiTermEnv (STypeVar env)) (nFiTerm - 1) nFiType))
<|> (TypeApp <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (fiTypeOfSize (fiTypeEnv env) nFiType)))
<|> (TmAll <$> (fiTypeUpToSize (fiTypeEnv env) nFiType) <*> (fiTermOfSize (fiTermEnv (STypeVar env)) (nFiTerm - 1) nFiType))
<|> (TypeApp <$> (fiTermOfSize (fiTermEnv env) (nFiTerm - 1) nFiType) <*> (fiTypeUpToSize (fiTypeEnv env) nFiType)))
fiTermUpToSize env 0 nFiType = (empty)
fiTermUpToSize env nFiTerm nFiType = ((fiTermUpToSize env (nFiTerm - 1) nFiType)
......
......@@ -82,9 +82,9 @@ freeVariablesType c (TyBase) = (nub (concat [[]]))
termOfSize env 0 nType = (empty)
termOfSize env 1 nType = (TmVar <$> (getTermVar env (Z)))
termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType) <*> (typeOfSize (typeEnv env) nType))
termOfSize env nTerm nType = ((TmAbs <$> (termOfSize (termEnv (STermVar env)) (nTerm - 1) nType) <*> (typeUpToSize (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (termOfSize (termEnv env) ((!!) l 0) nType) <*> (termOfSize (termEnv env) ((!!) l 1) nType))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType) <*> (typeOfSize (typeEnv env) nType))
<|> (TmTApp <$> (termOfSize (termEnv env) (nTerm - 1) nType) <*> (typeUpToSize (typeEnv env) nType))
<|> (TmTAbs <$> (termOfSize (termEnv (STypeVar env)) (nTerm - 1) nType)))
termUpToSize env 0 nType = (empty)
......@@ -182,9 +182,9 @@ memoTerm env nTe nType = memo env nTe
go :: Variable -> Integer -> Comble Term
go env 0 = (empty)
go env 1 = (TmVar <$> (getTermVar env (Z)))
go env nTerm = ((TmAbs <$> (memo (termEnv (STermVar env)) (nTerm - 1)) <*> (typeOfSize (typeEnv env) nType))
go env nTerm = ((TmAbs <$> (memo (termEnv (STermVar env)) (nTerm - 1)) <*> (typeUpToSize (typeEnv env) nType))
<|> (asum (map (\l -> (TmApp <$> (memo (termEnv env) ((!!) l 0)) <*> (memo (termEnv env) ((!!) l 1)))) (splitn 2 (nTerm - 1))))
<|> (TmTApp <$> (memo (termEnv env) (nTerm - 1)) <*> (typeOfSize (typeEnv env) nType))
<|> (TmTApp <$> (memo (termEnv env) (nTerm - 1)) <*> (typeUpToSize (typeEnv env) nType))
<|> (TmTAbs <$> (memo (termEnv (STypeVar env)) (nTerm - 1))))
forMemoTermWithSize env nTerm nType prop = (let c = (memoTerm env nTerm nType)
......
......@@ -290,22 +290,25 @@ generatorFunctions (nsd, sd, _, _) =
if countSorts csorts s > 1
then
FnCall "asum" [FnCall "map"
[LambdaExpr [VarParam "l"] $ AppConstrInst cname (ctorArgs 0 ns cattrs csorts ++ nativeArgs),
[LambdaExpr [VarParam "l"] $ AppConstrInst cname (ctorArgsMult 0 ns cattrs csorts ++ nativeArgs),
FnCall "splitn" [IntExpr $ countSorts csorts s, Minus (VarExpr $ "n" ++ sname) (IntExpr 1)]]]
else
AppConstrInst cname ([FnCall (aname ++ "OfSize") $
(envFor ns arg cattrs):(replaceArg (Minus (VarExpr $ "n" ++ sname) (IntExpr 1)) $ argsOf aname) | arg@(_, aname) <- csorts]
AppConstrInst cname ([FnCall (combleName aname) $
(envFor ns arg cattrs):(replaceArg (Minus (VarExpr $ "n" ++ sname) (IntExpr 1)) $ argsOf aname) | arg@(_, aname) <- csorts]
++ nativeArgs)
where
nativeArgs = [FnCall ("gen" ++ tname) [] | tname <- natives]
-- Generate the arguments of a comble with the correct variables and expressions as its arguments
ctorArgs :: Int -> NamespaceName -> [AttributeDef] -> [(IdenName, SortName)] -> [Expression]
ctorArgs _ _ _ [] = []
ctorArgs n ns attrs (arg@(_, aname):as) =
combleName aname = if aname == sname
then aname ++ "OfSize"
else aname ++ "UpToSize"
-- Generate the arguments of a recursive call where the current sort occurs more than once in the constructor.
ctorArgsMult :: Int -> NamespaceName -> [AttributeDef] -> [(IdenName, SortName)] -> [Expression]
ctorArgsMult _ _ _ [] = []
ctorArgsMult n ns attrs (arg@(_, aname):as) =
if aname == sname
then (FnCall (aname ++ "OfSize") $ env:(replaceArg (FnCall "(!!)" [VarExpr "l", IntExpr n]) args)) : ctorArgs (n+1) ns attrs as
else (FnCall (aname ++ "UpToSize") $ env:(argsOf aname)) : ctorArgs n ns attrs as
then (FnCall (aname ++ "OfSize") $ env:(replaceArg (FnCall "(!!)" [VarExpr "l", IntExpr n]) args)) : ctorArgsMult (n+1) ns attrs as
else (FnCall (aname ++ "UpToSize") $ env:(argsOf aname)) : ctorArgsMult n ns attrs as
where
env = envFor ns arg attrs
......
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