trueId = mkId [mkSimpleId trueS]
falseId = mkId [mkSimpleId falseS]
ifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])
whenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])
make these prefix identifier to allow "not def x" to be recognized
as "not (def x)" by giving def__ higher precedence then not__.
Simple identifiers usually have higher precedence then ____,
otherwise "def x" would be rejected. But with simple identifiers
"not def x" would be parsed as "(not def) x" because ____ is left
defId = mkId [mkSimpleId defS, placeTok]
notId = mkId [mkSimpleId notS, placeTok]
negId = mkId [mkSimpleId negS, placeTok]
builtinLogIds =
Set.fromList [andId, eqvId, implId, orId, infixIf, notId]
-- | add builtin identifiers
addBuiltins :: GlobalAnnos -> GlobalAnnos
[(applId, ALeft), (andId, ALeft), (orId, ALeft),
(implId, ARight), (infixIf, ALeft),
(((
Set.filter (\ i -> begPlace i || endPlace i) opIds
Set.\\ builtinRelIds) Set.\\ builtinLogIds)
logs = [(eqvId, implId), (implId, andId), (implId, orId),
(eqvId, infixIf), (infixIf, andId), (infixIf, orId),
(andId, notId), (orId, notId),
(andId, negId), (orId, negId)]
rels1 = map ( \ i -> (notId, i)) $
Set.toList builtinRelIds
rels1b = map ( \ i -> (negId, i)) $
Set.toList builtinRelIds
rels2 = map ( \ i -> (i, whenElse)) $
Set.toList builtinRelIds
ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
ops2 = map ( \ i -> (i, applId)) opIs
newPrecs = foldl (\ p (a, b) -> if
Rel.path b a p then p else
concat [logs, rels1, rels1b, rels2, ops1, ops2]
in case addGlobalAnnos ga { assoc_annos = newAss
map parseDAnno displayStrings of
Result _ (Just newGa) -> newGa
displayStrings :: [String]
[ "%display __\\/__ %LATEX __\\vee__"
, "%display __/\\__ %LATEX __\\wedge__"
, "%display __=>__ %LATEX __\\Rightarrow__"
, "%display __<=>__ %LATEX __\\Leftrightarrow__"
, "%display not__ %LATEX \\neg__"
parseDAnno :: String -> Annotation
parseDAnno str = case parse annotationL "" str of
Left _ -> error "parseDAnno"
aType = typeArgToType aTypeArg
bType = typeArgToType bTypeArg
cType = typeArgToType cTypeArg
lazyAType = mkLazyType aType
varToTypeArgK :: Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK i n v k = TypeArg i v (VarKind k) (toRaw k) n Other nullRange
varToTypeArg :: Id -> Int -> Variance -> TypeArg
varToTypeArg i n v = varToTypeArgK i n v universe
mkATypeArg :: Variance -> TypeArg
mkATypeArg = varToTypeArg aVar (-1)
aTypeArg = mkATypeArg NonVar
aTypeArgK :: Kind -> TypeArg
aTypeArgK = varToTypeArgK aVar (-1) NonVar
bTypeArg = varToTypeArg bVar (-2) NonVar
cTypeArg = varToTypeArg cVar (-3) NonVar
bindVarA :: TypeArg -> Type -> TypeScheme
bindVarA a t = TypeScheme [a] t nullRange
bindA :: Type -> TypeScheme
bindA = bindVarA aTypeArg
resType = TypeScheme [aTypeArg, bTypeArg]
(mkFunArrType (mkProductType [lazyAType, mkLazyType bType]) FunArr aType)
lazyLog = mkLazyType unitType
aPredType = TypeAbs (mkATypeArg ContraVar)
(mkFunArrType aType PFunArr unitType) nullRange
eqType = bindA $ mkFunArrType (mkProductType [lazyAType, lazyAType])
logType = simpleTypeScheme $ mkFunArrType
(mkProductType [lazyLog, lazyLog]) PFunArr unitType
notType = simpleTypeScheme $ mkFunArrType lazyLog PFunArr unitType
whenType = bindA $ mkFunArrType
(mkProductType [lazyAType, lazyLog, lazyAType]) PFunArr aType
unitTypeScheme :: TypeScheme
unitTypeScheme = simpleTypeScheme lazyLog
botId = mkId [mkSimpleId "bottom"]
predTypeId = mkId [mkSimpleId "Pred"]
logId = mkId [mkSimpleId "Logical"]
botType = let a = aTypeArgK cppoCl in bindVarA a $ mkLazyType $ typeArgToType a
defType = bindA $ mkFunArrType lazyAType PFunArr unitType
bList :: [(Id, TypeScheme)]
bList = (botId, botType) : (defId, defType) : (notId, notType) :
(negId, notType) : (whenElse, whenType) :
(trueId, unitTypeScheme) : (falseId, unitTypeScheme) :
(eqId, eqType) : (exEq, eqType) : (resId, resType) :
map ( \ o -> (o, logType)) [andId, orId, eqvId, implId, infixIf]
mkTypesEntry :: Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry i k cs s d =
funEntry :: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
mkTypesEntry (arrowId a) funKind (funKind : cs) (map arrowId s) NoTypeDefn
mkEntry :: Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry i k cs = mkTypesEntry i k cs []
pEntry :: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry i k = mkEntry i k [k]
-- | builtin data type map
: funEntry FunArr [PFunArr] []
: funEntry PContFunArr [PFunArr] [funKind3 cpoCl cpoCl cppoCl]
: funEntry ContFunArr [PContFunArr, FunArr]
[funKind3 cpoCl cpoCl cpoCl, funKind3 cpoCl cppoCl cppoCl]
: pEntry unitTypeId cppoCl NoTypeDefn
: pEntry predTypeId (FunKind ContraVar universe universe nullRange)
(AliasTypeDefn aPredType)
: pEntry lazyTypeId coKind NoTypeDefn
: pEntry logId universe (AliasTypeDefn $ mkLazyType unitType)
: map (\ n -> let k = prodKind n nullRange in
mkEntry (productId n nullRange) k
(k : map (prodKind1 n nullRange) [cpoCl, cppoCl]) NoTypeDefn)
cppoId = stringToId "Cppo"
cppoCl = ClassKind cppoId
-- | builtin function map
-- | environment with predefined names
preEnv = initialEnv { classMap = cpoMap, typeMap = bTypes, assumps = bOps }
mkQualOpInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst k i sc tys ps = QualOp Fun (PolyId i [] ps) sc tys k ps
mkQualOp :: Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp = mkQualOpInst Infer
mkTermInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTermInst k i sc tys ps t = ApplTerm (mkQualOpInst k i sc tys ps) t ps
mkTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm = mkTermInst Infer
mkBinTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm i sc tys ps t1 t2 = mkTerm i sc tys ps $ TupleTerm [t1, t2] ps
mkLogTerm :: Id -> Range -> Term -> Term -> Term
mkLogTerm i = mkBinTerm i logType []
mkEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm i ty = mkBinTerm i eqType [ty]
unitTerm :: Id -> Range -> Term
unitTerm i = mkQualOp i unitTypeScheme []
toBinJunctor :: Id -> [Term] -> Range -> Term
toBinJunctor i ts ps = case ts of
[] -> error "toBinJunctor"
t : rs -> mkLogTerm i ps t (toBinJunctor i rs ps)