{-# OPTIONS_GHC -Wall #-} {-# LANGUAGE LambdaCase #-} module Database.Design.Ampersand.ADL1.P2A_Converters (pCtx2aCtx,pCpt2aCpt) where import Database.Design.Ampersand.ADL1.Disambiguate import Database.Design.Ampersand.Core.ParseTree -- (P_Context(..), A_Context(..)) import Database.Design.Ampersand.Input.ADL1.CtxError import Database.Design.Ampersand.ADL1.Lattices -- used for type-checking import Database.Design.Ampersand.Core.AbstractSyntaxTree hiding (sortWith, maxima, greatest) import Database.Design.Ampersand.Classes.ViewPoint hiding (gens) import Database.Design.Ampersand.Classes.ConceptStructure import Database.Design.Ampersand.Basics import Database.Design.Ampersand.Misc import Prelude hiding (sequence, mapM) import Control.Applicative import Data.Traversable import qualified Data.Set as Set import qualified Data.Map as Map import Data.Function import Data.Maybe import Data.List(nub) fatal :: Int -> String -> a fatal = fatalMsg "ADL1.P2A_Converters" newtype SignOrd = SignOrd Sign instance Ord SignOrd where compare (SignOrd (Sign a b)) (SignOrd (Sign c d)) = compare (name a,name b) (name c,name d) instance Eq SignOrd where (==) (SignOrd (Sign a b)) (SignOrd (Sign c d)) = (name a,name b) == (name c,name d) -- pCtx2aCtx has three tasks: -- 1) Disambiguate the structures. -- Disambiguation means replacing every "TermPrim" (the parsed expression) with the correct Expression (available through DisambPrim) -- This is done by using the function "disambiguate" on the outer-most structure. -- In order to do this, its data type must be polymorphic, as in "P_ViewSegmt a". -- After parsing, the type has TermPrim for the type variable. In our example: "P_ViewSegmt TermPrim". Note that "type P_ViewSegment = P_ViewSegmt TermPrim". -- After disambiguation, the type variable is (TermPrim, DisambPrim), as in "P_ViewSegmt (TermPrim, DisambPrim)" -- 2) Typecheck the structures. -- This changes the data-structure entirely, changing the P_ into the A_ -- A "Guarded" will be added on the outside, in order to catch both type errors and disambiguation errors. -- Using the Applicative operations <$> and <*> causes these errors to be in parallel -- 3) Check everything else on the A_-structure: interface references should not be cyclic, rules e.a. must have unique names, etc. -- Part 3 is done below, the other two are done in pCtx2aCtx' pCtx2aCtx :: Options -> P_Context -> Guarded A_Context pCtx2aCtx opts = checkOtherAtomsInSessionConcept . checkPurposes -- Check whether all purposes refer to existing objects . checkDanglingRulesInRuleRoles -- Check whether all rules in MAINTAIN statements are declared . checkInterfaceCycles -- Check that interface references are not cyclic . checkMultipleDefaultViews -- Check whether each concept has at most one default view . checkUnique udefrules -- Check uniquene names of: rules, . checkUnique patterns -- patterns, . checkUnique ctxvs -- view defs, . checkUnique ctxifcs -- and interfaces. . pCtx2aCtx' opts where checkUnique f gCtx = case gCtx of Checked ctx -> case uniqueNames (f ctx) of Checked () -> gCtx Errors err -> Errors err Errors err -> Errors err -- NOTE: Static checks like checkPurposes should ideally occur on the P-structure before type-checking, as it makes little -- sense to do type checking when there are static errors. However, in Ampersand all collect functions (e.g. in ViewPoint) -- only exist on the A-Structure, so we do it afterwards. Static purpose errors won't affect types, so in this case it is no problem. -- Check whether all purposes refer to existing objects. checkPurposes :: Guarded A_Context -> Guarded A_Context checkPurposes gCtx = case gCtx of Errors err -> Errors err Checked ctx -> let topLevelPurposes = ctxps ctx purposesInPatterns = concatMap ptxps (ctxpats ctx) allPurposes = topLevelPurposes ++ purposesInPatterns danglingPurposes = filter (isDanglingPurpose ctx) allPurposes in if null danglingPurposes then gCtx else Errors $ map mkDanglingPurposeError danglingPurposes -- Return True if the ExplObj in this Purpose does not exist. isDanglingPurpose :: A_Context -> Purpose -> Bool isDanglingPurpose ctx purp = case explObj purp of ExplConceptDef concDef -> let nm = name concDef in nm `notElem` map name (ctxcds ctx ) ExplDeclaration decl -> let nm = name decl in nm `notElem` map name (relsDefdIn ctx) -- is already covered by type checker ExplRule nm -> nm `notElem` map name (udefrules ctx) ExplIdentityDef nm -> nm `notElem` map name (identities ctx) ExplViewDef nm -> nm `notElem` map name (viewDefs ctx) ExplPattern nm -> nm `notElem` map name (ctxpats ctx) ExplInterface nm -> nm `notElem` map name (ctxifcs ctx) ExplContext nm -> ctxnm ctx /= nm && False -- HJO: This line is a workaround for the issue mentioned in https://github.com/AmpersandTarski/ampersand/issues/46 -- TODO: fix this when we pick up working on multiple contexts. -- Check that interface references are not cyclic checkInterfaceCycles :: Guarded A_Context -> Guarded A_Context checkInterfaceCycles gCtx = case gCtx of Errors err -> Errors err Checked ctx -> if null interfaceCycles then gCtx else Errors $ map mkInterfaceRefCycleError interfaceCycles where interfaceCycles = [ map lookupInterface iCycle | iCycle <- getCycles refsPerInterface ] refsPerInterface = [(name ifc, getDeepIfcRefs $ ifcObj ifc) | ifc <- ctxifcs ctx ] getDeepIfcRefs obj = case objmsub obj of Nothing -> [] Just (InterfaceRef nm) -> [nm] Just (Box _ _ objs) -> concatMap getDeepIfcRefs objs lookupInterface nm = case [ ifc | ifc <- ctxifcs ctx, name ifc == nm ] of [ifc] -> ifc _ -> fatal 124 "Interface lookup returned zero or more than one result" -- Check whether each concept has at most one default view checkMultipleDefaultViews :: Guarded A_Context -> Guarded A_Context checkMultipleDefaultViews gCtx = case gCtx of Errors err -> Errors err Checked ctx -> let conceptsWithMultipleViews = [ (c,vds)| vds@(Vd{vdcpt=c}:_:_) <- eqClass ((==) `on` vdcpt) $ filter vdIsDefault (ctxvs ctx) ] in if null conceptsWithMultipleViews then gCtx else Errors $ map mkMultipleDefaultError conceptsWithMultipleViews checkDanglingRulesInRuleRoles :: Guarded A_Context -> Guarded A_Context checkDanglingRulesInRuleRoles gCtx = case gCtx of Errors _ -> gCtx Checked ctx -> case [mkDanglingRefError "Rule" nm (arPos rr) | rr <- ctxrrules ctx , nm <- arRules rr , nm `notElem` map name (allRules ctx) ] of [] -> gCtx errs -> Errors errs checkOtherAtomsInSessionConcept :: Guarded A_Context -> Guarded A_Context checkOtherAtomsInSessionConcept gCtx = case gCtx of Errors _ -> gCtx Checked ctx -> case [mkOtherAtomInSessionError atom | pop@PCptPopu{popcpt =cpt} <- ctxpopus ctx , name cpt == "SESSION" , atom <- filter (/= "_SESSION") (popas pop) ] of [] -> gCtx errs -> Errors errs pCtx2aCtx' :: Options -> P_Context -> Guarded A_Context pCtx2aCtx' _ PCtx { ctx_nm = n1 , ctx_pos = n2 , ctx_lang = lang , ctx_markup = pandocf , ctx_thms = p_themes , ctx_pats = p_patterns , ctx_PPrcs = p_processes , ctx_rs = p_rules , ctx_ds = p_declarations , ctx_cs = p_conceptdefs , ctx_ks = p_identdefs , ctx_rrules = p_roleRules , ctx_rrels = p_roleRelations , ctx_vs = p_viewdefs , ctx_gs = p_gens , ctx_ifcs = p_interfaces , ctx_ps = p_purposes , ctx_pops = p_pops , ctx_sql = p_sqldefs , ctx_php = p_phpdefs , ctx_metas = p_metas } = (\pats rules identdefs viewdefs interfaces purposes udpops sqldefs phpdefs allRoleRelations -> ACtx{ ctxnm = n1 , ctxpos = n2 , ctxlang = deflangCtxt , ctxmarkup = deffrmtCtxt , ctxthms = p_themes , ctxpats = pats , ctxrs = rules , ctxds = ctxDecls , ctxpopus = nub (udpops++dclPops++mp1Pops rules++mp1Pops pats++mp1Pops identdefs++mp1Pops viewdefs++mp1Pops interfaces) , ctxcds = allConceptDefs , ctxks = identdefs , ctxrrules = allRoleRules , ctxRRels = allRoleRelations , ctxvs = viewdefs , ctxgs = map pGen2aGen p_gens , ctxgenconcs = map (map castConcept) (concGroups ++ map (:[]) soloConcs) , ctxifcs = interfaces , ctxps = purposes , ctxsql = sqldefs , ctxphp = phpdefs , ctxmetas = p_metas } ) <$> traverse pPat2aPat (p_patterns ++ p_processes) -- The patterns defined in this context <*> traverse (pRul2aRul n1) p_rules -- All user defined rules in this context, but outside patterns and outside processes <*> traverse pIdentity2aIdentity p_identdefs -- The identity definitions defined in this context, outside the scope of patterns <*> traverse pViewDef2aViewDef p_viewdefs -- The view definitions defined in this context, outside the scope of patterns <*> traverse pIfc2aIfc p_interfaceAndDisambObjs -- TODO: explain ... The interfaces defined in this context, outside the scope of patterns <*> traverse pPurp2aPurp p_purposes -- The purposes of objects defined in this context, outside the scope of patterns <*> traverse pPop2aPop p_pops -- [Population] <*> traverse pObjDef2aObjDef p_sqldefs -- user defined sqlplugs, taken from the Ampersand script <*> traverse pObjDef2aObjDef p_phpdefs -- user defined phpplugs, taken from the Ampersand script <*> traverse pRoleRelation2aRoleRelation (p_roleRelations ++ concatMap pt_RRels (p_patterns ++ p_processes)) where p_interfaceAndDisambObjs :: [(P_Interface, P_ObjDef (TermPrim, DisambPrim))] p_interfaceAndDisambObjs = [ (ifc, disambiguate termPrimDisAmb $ ifc_Obj ifc) | ifc <- p_interfaces ] -- story about genRules and genLattice -- the genRules is a list of equalities between concept sets, in which every set is interpreted as a conjunction of concepts -- the genLattice is the resulting optimized structure genRules = [ ( Set.singleton (name (gen_spc x)), Set.fromList (map name (gen_concs x))) | x <- p_gens ++ concatMap pt_gns (p_patterns ++ p_processes) ] genLattice :: Op1EqualitySystem String genLattice = optimize1 (foldr addEquality emptySystem genRules) concGroups :: [[String]] concGroups = getGroups genLattice allConcs :: Set.Set String allConcs = Set.fromList (map (name . source) decls ++ map (name . target) decls) soloConcs :: [String] soloConcs = filter (not . isInSystem genLattice) (Set.toList allConcs) deflangCtxt = lang -- take the default language from the top-level context deffrmtCtxt = fromMaybe ReST pandocf (decls,dclPops)= unzip dps (ctxDecls,_ ) = unzip ctxDecls' dps = ctxDecls'++patDecls ctxDecls' = [ pDecl2aDecl n1 deflangCtxt deffrmtCtxt pDecl | pDecl<-p_declarations ] -- The relations declared in this context, outside the scope of patterns patDecls = [ pDecl2aDecl (name pat) deflangCtxt deffrmtCtxt pDecl | pat<-p_patterns ++p_processes , pDecl<-pt_dcs pat ] -- The relations declared in all patterns within this context. -- In order to find declarations efficiently, a Map is constructed to search declarations by name. declMap = Map.map groupOnTp (Map.fromListWith (++) [(name d,[d]) | d <- decls]) where groupOnTp lst = Map.fromListWith accumDecl [(SignOrd$ sign d,d) | d <- lst] findDecls x = Map.findWithDefault Map.empty x declMap -- get all declarations with the same name as x findDecl o x = (getOneExactly o . Map.elems . findDecls) x findDeclsTyped x tp = Map.findWithDefault [] (SignOrd tp) (Map.map (:[]) (findDecls x)) findDeclTyped o x tp = getOneExactly o (findDeclsTyped x tp) -- accumDecl is the function that combines two relations into one -- meanings, for instance, two should get combined into a list of meanings, et cetera -- positions are combined -- TODO accumDecl :: Declaration -> Declaration -> Declaration accumDecl a _ = a pDecl2aDecl :: String -- The name of the pattern -> Lang -- The default language -> PandocFormat -- The default pandocFormat -> P_Declaration -> (Declaration, Population) pDecl2aDecl patNm defLanguage defFormat pd = let dcl = Sgn { decnm = dec_nm pd , decsgn = pSign2aSign (dec_sign pd) , decprps = dec_prps pd , decprps_calc = Nothing --decprps_calc in an A_Context are still the user-defined only. prps are calculated in adl2fspec. , decprL = dec_prL pd , decprM = dec_prM pd , decprR = dec_prR pd , decMean = pMean2aMean defLanguage defFormat (dec_Mean pd) , decfpos = dec_fpos pd , deciss = True , decusr = True , decpat = patNm , decplug = dec_plug pd } in (dcl, PRelPopu { popdcl = dcl, popps = dec_popu pd}) pSign2aSign :: P_Sign -> Sign pSign2aSign (P_Sign src tgt) = Sign (pCpt2aCpt src) (pCpt2aCpt tgt) pGen2aGen :: P_Gen -> A_Gen pGen2aGen pg@PGen{} = Isa{gengen = pCpt2aCpt (gen_gen pg) ,genspc = pCpt2aCpt (gen_spc pg) } pGen2aGen pg@P_Cy{} = IsE { genrhs = map pCpt2aCpt (gen_rhs pg) , genspc = pCpt2aCpt (gen_spc pg) } castSign :: String -> String -> Sign castSign a b = Sign (castConcept a) (castConcept b) leastConcept :: A_Concept -> String -> A_Concept leastConcept c str = case (name c `elem` leastConcepts, str `elem` leastConcepts) of (True, _) -> c (_, True) -> castConcept str (_, _) -> fatal 178 ("Either "++name c++" or "++str++" should be a subset of the other." ) where leastConcepts = findExact genLattice (Atom (name c) `Meet` (Atom str)) castConcept :: String -> A_Concept castConcept "ONE" = ONE castConcept x = PlainConcept { cptnm = x } pPop2aPop :: P_Population -> Guarded Population pPop2aPop P_CptPopu { p_cnme = cnm, p_popas = ps } = pure PCptPopu{ popcpt = castConcept cnm, popas = ps } pPop2aPop orig@(P_RelPopu { p_rnme = rnm, p_popps = ps }) = fmap (\dcl -> PRelPopu { popdcl = dcl, popps = ps}) (findDecl orig rnm) pPop2aPop orig@(P_TRelPop { p_rnme = rnm, p_type = tp, p_popps = ps }) = fmap (\dcl -> PRelPopu { popdcl = dcl, popps = ps}) (findDeclTyped orig rnm (pSign2aSign tp)) pObjDef2aObjDef :: P_ObjectDef -> Guarded ObjectDef pObjDef2aObjDef x = pObjDefDisamb2aObjDef $ disambiguate termPrimDisAmb x pObjDefDisamb2aObjDef :: P_ObjDef (TermPrim, DisambPrim) -> Guarded ObjectDef pObjDefDisamb2aObjDef x = fmap fst (typecheckObjDef x) pViewDef2aViewDef :: P_ViewDef -> Guarded ViewDef pViewDef2aViewDef x = typecheckViewDef tpda where tpda = disambiguate termPrimDisAmb x typecheckViewDef :: P_ViewD (TermPrim, DisambPrim) -> Guarded ViewDef typecheckViewDef o@(P_Vd { vd_pos = orig , vd_lbl = lbl -- String , vd_cpt = cpt -- Concept , vd_isDefault = isDefault , vd_html = mHtml -- Html template , vd_ats = pvs -- view segment }) = (\vdts -> Vd { vdpos = orig , vdlbl = lbl , vdcpt = pCpt2aCpt cpt , vdIsDefault = isDefault , vdhtml = mHtml , vdats = vdts }) <$> traverse (typeCheckViewSegment o) pvs typeCheckViewSegment :: (P_ViewD a) -> (P_ViewSegmt (TermPrim, DisambPrim)) -> Guarded ViewSegment typeCheckViewSegment o P_ViewExp{ vs_obj = ojd } = unguard $ (\(obj,b) -> case findExact genLattice (mIsc c (name (source (objctx obj)))) of [] -> mustBeOrdered o o (Src,(source (objctx obj)),obj) r -> if b || c `elem` r then pure (ViewExp obj{objctx = addEpsilonLeft' (head r) (objctx obj)}) else mustBeBound (origin obj) [(Tgt,objctx obj)]) <$> typecheckObjDef ojd where c = name (vd_cpt o) typeCheckViewSegment _ P_ViewText { vs_txt = txt } = pure$ ViewText txt typeCheckViewSegment _ P_ViewHtml { vs_htm = htm } = pure$ ViewHtml htm isa :: String -> String -> Bool isa c1 c2 = c1 `elem` findExact genLattice (Atom c1 `Meet` Atom c2) -- shouldn't this Atom be called a Concept? SJC: Answer: we're using the constructor "Atom" in the lattice sense, not in the relation-algebra sense. c1 and c2 are indeed Concepts here typecheckObjDef :: (P_ObjDef (TermPrim, DisambPrim)) -> Guarded (ObjectDef, Bool) typecheckObjDef o@(P_Obj { obj_nm = nm , obj_pos = orig , obj_ctx = ctx , obj_mView = mView , obj_msub = subs , obj_strs = ostrs }) = unguard $ (\ (objExpr,(srcBounded,tgtBounded)) -> (\case Just (newExpr,subStructures) -> obj (newExpr,srcBounded) (Just subStructures) Nothing -> obj (objExpr,srcBounded) Nothing ) <$> maybeOverGuarded (pSubi2aSubi objExpr tgtBounded o) subs <* typeCheckViewAnnotation objExpr mView ) <$> typecheckTerm ctx where lookupView :: String -> Maybe P_ViewDef lookupView viewId = case [ vd | vd <- p_viewdefs, vd_lbl vd == viewId ] of [] -> Nothing vd:_ -> Just vd -- return the first one, if there are more, this is caught later on by uniqueness static check typeCheckViewAnnotation :: Expression -> Maybe String -> Guarded () typeCheckViewAnnotation _ Nothing = pure () typeCheckViewAnnotation objExpr (Just viewId) = case lookupView viewId of Just vd -> let viewAnnCptStr = name $ target objExpr viewDefCptStr = name $ vd_cpt vd viewIsCompatible = viewAnnCptStr `isa` viewDefCptStr in if viewIsCompatible then pure () else Errors [mkIncompatibleViewError o viewId viewAnnCptStr viewDefCptStr] Nothing -> Errors [mkUndeclaredError "view" o viewId] obj (e,sr) s = ( Obj { objnm = nm , objpos = orig , objctx = e , objmView = mView , objmsub = s , objstrs = ostrs }, sr) addEpsilonLeft',addEpsilonRight' :: String -> Expression -> Expression -- TODO: why use primes here? addEpsilonLeft' a e = if a==name (source e) then e else EEps (leastConcept (source e) a) (castSign a (name (source e))) .:. e addEpsilonRight' a e = if a==name (target e) then e else e .:. EEps (leastConcept (target e) a) (castSign (name (target e)) a) addEpsilon :: String -> String -> Expression -> Expression addEpsilon s t e = addEpsilonLeft' s (addEpsilonRight' t e) pSubi2aSubi :: Expression -- Expression of the surrounding -> Bool -- Whether the surrounding is bounded -> P_ObjDef a -- name of where the error occured! -> P_SubIfc (TermPrim, DisambPrim) -- Subinterface to check -> Guarded ( Expression -- In the case of a "Ref", we do not change the type of the subinterface with epsilons, this is to change the type of our surrounding instead. In the case of "Box", this is simply the original expression (in such a case, epsilons are added to the branches instead) , SubInterface -- the subinterface ) pSubi2aSubi objExpr b o x = case x of P_InterfaceRef{si_str = ifcId} -> unguard $ (\(refIfcExpr,_) -> (\objExprEps -> (objExprEps,InterfaceRef ifcId)) <$> typeCheckInterfaceRef o ifcId objExpr refIfcExpr) <$> case lookupDisambIfcObj ifcId of Just disambObj -> typecheckTerm $ obj_ctx disambObj -- term is type checked twice, but otherwise we need a more complicated type check method to access already-checked interfaces. TODO: hide possible duplicate errors in a nice way (that is: via CtxError) Nothing -> Errors [mkUndeclaredError "interface" o ifcId] P_Box{} -> case si_box x of [] -> const undefined <$> hasNone ([]::[P_SubIfc a]) x -- error l -> (\lst -> (objExpr,Box (target objExpr) (si_class x) lst)) <$> traverse (unguard . fmap (matchWith (target objExpr)) . typecheckObjDef) l <* uniqueNames l where matchWith _ (ojd,exprBound) = if b || exprBound then ( case findExact genLattice (mIsc (name$ target objExpr) (name . source . objctx $ ojd)) of [] -> mustBeOrderedLst x [(source (objctx ojd),Src, ojd)] (r:_) -> pure (ojd{objctx=addEpsilonLeft' r (objctx ojd)}) ) else mustBeBound (origin ojd) [(Src,objctx ojd),(Tgt,objExpr)] typeCheckInterfaceRef :: P_ObjDef a -> String -> Expression -> Expression -> Guarded Expression typeCheckInterfaceRef objDef ifcRef objExpr ifcExpr = let expTarget = target objExpr expTargetStr = name expTarget ifcSource = source ifcExpr ifcSourceStr = name ifcSource refIsCompatible = expTargetStr `isa` ifcSourceStr || ifcSourceStr `isa` expTargetStr in if refIsCompatible then pure $ addEpsilonRight' ifcSourceStr objExpr else Errors [mkIncompatibleInterfaceError objDef expTarget ifcSource ifcRef ] lookupDisambIfcObj :: String -> Maybe (P_ObjDef (TermPrim, DisambPrim)) lookupDisambIfcObj ifcId = case [ disambObj | (vd,disambObj) <- p_interfaceAndDisambObjs, ifc_Name vd == ifcId ] of [] -> Nothing disambObj:_ -> Just disambObj -- return the first one, if there are more, this is caught later on by uniqueness static check typecheckTerm :: Term (TermPrim, DisambPrim) -> Guarded (Expression, (Bool, Bool)) typecheckTerm tct = case tct of Prim (t,v) -> (\x -> (x, case t of PVee _ -> (False,False) _ -> (True,True) )) <$> pDisAmb2Expr (t,v) PEqu _ a b -> unguard $ binary (.==.) (MBE (Src,fst) (Src,snd), MBE (Tgt,fst) (Tgt,snd)) <$> tt a <*> tt b PImp _ a b -> unguard $ binary (.|-.) (MBG (Src,snd) (Src,fst), MBG (Tgt,snd) (Tgt,fst)) <$> tt a <*> tt b PIsc _ a b -> unguard $ binary (./\.) (ISC (Src,fst) (Src,snd), ISC (Tgt,fst) (Tgt,snd)) <$> tt a <*> tt b PUni _ a b -> unguard $ binary (.\/.) (UNI (Src,fst) (Src,snd), UNI (Tgt,fst) (Tgt,snd)) <$> tt a <*> tt b PDif _ a b -> unguard $ binary (.-.) (MBG (Src,fst) (Src,snd), MBG (Tgt,fst) (Tgt,snd)) <$> tt a <*> tt b PLrs _ a b -> unguard $ binary' (./.) (MBG (Tgt,snd) (Tgt,fst)) ((Src,fst),(Src,snd)) Tgt Tgt <$> tt a <*> tt b PRrs _ a b -> unguard $ binary' (.\.) (MBG (Src,fst) (Src,snd)) ((Tgt,fst),(Tgt,snd)) Src Src <$> tt a <*> tt b PDia _ a b -> unguard $ binary' (.<>.) (ISC (Tgt,fst) (Src,snd)) ((Src,fst),(Tgt,snd)) Tgt Src <$> tt a <*> tt b -- MBE would have been correct, but too restrictive PCps _ a b -> unguard $ binary' (.:.) (ISC (Tgt,fst) (Src,snd)) ((Src,fst),(Tgt,snd)) Tgt Src <$> tt a <*> tt b PRad _ a b -> unguard $ binary' (.!.) (MBE (Tgt,fst) (Src,snd)) ((Src,fst),(Tgt,snd)) Tgt Src <$> tt a <*> tt b -- Using MBE instead of ISC allows the programmer to use De Morgan PPrd _ a b -> (\(x,(s,_)) (y,(_,t)) -> (x .*. y, (s,t))) <$> tt a <*> tt b PKl0 _ a -> unguard $ unary EKl0 (UNI (Src, id) (Tgt, id), UNI (Src, id) (Tgt, id)) <$> tt a PKl1 _ a -> unguard $ unary EKl1 (UNI (Src, id) (Tgt, id), UNI (Src, id) (Tgt, id)) <$> tt a PFlp _ a -> (\(x,(s,t)) -> ((EFlp x), (t,s))) <$> tt a PCpl _ a -> (\(x,_) -> (ECpl x,(False,False))) <$> tt a PBrk _ e -> (\(x,t) -> (EBrk x,t)) <$> tt e where o = origin (fmap fst tct) tt = typecheckTerm -- SJC: Here is what binary, binary' and unary do: -- (1) Create an expression, the combinator for this is given by its first argument -- (2) Fill in the corresponding type-checked terms to that expression -- (3) For binary' only: fill in the intermediate concept too -- (4) Fill in the type of the new expression -- For steps (3) and (4), you can use the `TT' data type to specify the new type, and what checks should occur: -- If you don't know what to use, try MBE: it is the strictest form. -- In the steps (3) and (4), different type errors may arise: -- If the type does not exist, this yields a type error. -- Some types may be generalized, while others may not. -- When a type may be generalized, that means that the value of the expression does not change if the type becomes larger -- When a type may not be generalized: -- the type so far is actually just an estimate -- it must be bound by the context to something smaller, or something as big -- a way to do this, is by using (V[type] /\ thingToBeBound) -- More details about generalizable types can be found by looking at "deriv1". binary :: (Expression -> Expression->Expression) -- combinator -> ( TT ( SrcOrTgt , ( (Expression, (Bool, Bool)) , (Expression, (Bool, Bool)) ) -> (Expression, (Bool, Bool)) ) , TT ( SrcOrTgt , ( (Expression, (Bool, Bool)) , (Expression, (Bool, Bool)) ) -> (Expression, (Bool, Bool)) ) ) -- simple instruction on how to derive the type -> (Expression,(Bool,Bool)) -> (Expression,(Bool,Bool)) -- expressions to feed into the combinator after translation -> Guarded (Expression,(Bool,Bool)) binary cbn tp e1 e2 = wrap (fst e1,fst e2) <$> deriv tp (e1,e2) where wrap (expr1,expr2) ((src,b1), (tgt,b2)) = (cbn (addEpsilon src tgt expr1) (addEpsilon src tgt expr2), (b1, b2)) unary cbn tp e1 = wrap (fst e1) <$> deriv tp e1 where wrap expr ((src,b1), (tgt,b2)) = (cbn (addEpsilon src tgt expr), (b1, b2)) binary' cbn preConcept tp side1 side2 e1 e2 = wrap (fst e1,fst e2) <$> deriv1 o (fmap (resolve (e1,e2)) preConcept) <*> deriv' tp (e1,e2) where wrap (expr1,expr2) (cpt,_) ((_,b1), (_,b2)) = (cbn (lrDecide side1 expr1) (lrDecide side2 expr2), (b1, b2)) where lrDecide side e = case side of Src -> addEpsilonLeft' cpt e; Tgt -> addEpsilonRight' cpt e deriv (t1,t2) es = (,) <$> deriv1 o (fmap (resolve es) t1) <*> deriv1 o (fmap (resolve es) t2) deriv1 o x' = case x' of (MBE a@(p1,(e1,b1)) b@(p2,(e2,b2))) -> if (b1 && b2) || (getConcept p1 e1 == getConcept p2 e2) then (\x -> (x,b1||b2)) <$> getExactType mjoin (p1, e1) (p2, e2) else mustBeBound o [(p,e) | (p,(e,False))<-[a,b]] (MBG (p1,(e1,b1)) (p2,(e2,b2))) -> (\x -> (x,b1)) <$> getAndCheckType mjoin (p1, True, e1) (p2, b2, e2) (UNI (p1,(e1,b1)) (p2,(e2,b2))) -> (\x -> (x,b1 && b2)) <$> getAndCheckType mjoin (p1, b1, e1) (p2, b2, e2) (ISC (p1,(e1,b1)) (p2,(e2,b2))) -> (\x -> (x,b1 || b2)) <$> getAndCheckType mIsc (p1, b1, e1) (p2, b2, e2) where getExactType flf (p1,e1) (p2,e2) = case findExact genLattice (flf (getConcept p1 e1) (getConcept p2 e2)) of [] -> mustBeOrdered o (p1,e1) (p2,e2) r -> pure$ head r getAndCheckType flf (p1,b1,e1) (p2,b2,e2) = case findSubsets genLattice (flf (getConcept p1 e1) (getConcept p2 e2)) of -- note: we could have used GetOneGuarded, but this is more specific [] -> mustBeOrdered o (p1,e1) (p2,e2) [r] -> case (b1 || Set.member (getConcept p1 e1) r,b2 || Set.member (getConcept p2 e2) r ) of (True,True) -> pure (head (Set.toList r)) (a,b) -> mustBeBound o [(p,e) | (False,p,e)<-[(a,p1,e1),(b,p2,e2)]] lst -> mustBeOrderedConcLst o (p1,e1) (p2,e2) (map (map castConcept . Set.toList) lst) termPrimDisAmb :: TermPrim -> (TermPrim, DisambPrim) termPrimDisAmb x = (x, case x of PI _ -> Ident Pid _ conspt-> Known (EDcI (pCpt2aCpt conspt)) Patm _ s Nothing -> Mp1 s Patm _ s (Just conspt) -> Known (EMp1 s (pCpt2aCpt conspt)) PVee _ -> Vee Pfull _ a b -> Known (EDcV (Sign (pCpt2aCpt a) (pCpt2aCpt b))) PNamedR nr -> Rel $ disambNamedRel nr ) disambNamedRel (PNamedRel _ r Nothing) = [EDcD dc | dc <- (Map.elems $ findDecls r)] disambNamedRel (PNamedRel _ r (Just s)) = [EDcD dc | dc <- (findDeclsTyped r (pSign2aSign s))] namedRel2Decl :: P_NamedRel -> Guarded Declaration namedRel2Decl o@(PNamedRel _ r Nothing) = getOneExactly o [ dc | dc <- (Map.elems $ findDecls r)] namedRel2Decl o@(PNamedRel _ r (Just s)) = getOneExactly o [ dc | dc <- (findDeclsTyped r (pSign2aSign s))] pIfc2aIfc :: (P_Interface, P_ObjDef (TermPrim, DisambPrim)) -> Guarded Interface pIfc2aIfc (P_Ifc { ifc_Params = tps , ifc_Class = iclass , ifc_Args = args , ifc_Roles = rols , ifc_Obj = _ , ifc_Pos = orig -- , ifc_Name = nm , ifc_Prp = prp }, objDisamb) = (\ tps' obj' -> Ifc { ifcParams = tps' , ifcClass = iclass , ifcArgs = args , ifcRoles = rols , ifcObj = obj' , ifcEcas = [] -- to be enriched in Adl2fSpec with ECA-rules , ifcControls = [] -- to be enriched in Adl2fSpec with rules to be checked , ifcPos = orig , ifcPrp = prp }) <$> traverse namedRel2Decl tps <*> pObjDefDisamb2aObjDef objDisamb pRoleRelation2aRoleRelation :: P_RoleRelation -> Guarded A_RoleRelation pRoleRelation2aRoleRelation prr = (\ ds' -> RR { rrRoles = rr_Roles prr , rrRels = ds' , rrPos = rr_Pos prr }) <$> traverse namedRel2Decl (rr_Rels prr) pRoleRule2aRoleRule :: P_RoleRule -> A_RoleRule pRoleRule2aRoleRule prr = A_RoleRule { arRoles = mRoles prr , arRules = mRules prr , arPos = mPos prr } pPat2aPat :: P_Pattern -> Guarded Pattern pPat2aPat ppat = f <$> traverse (pRul2aRul (name ppat)) (pt_rls ppat) <*> traverse pIdentity2aIdentity (pt_ids ppat) <*> traverse pPop2aPop (pt_pop ppat) <*> traverse pViewDef2aViewDef (pt_vds ppat) <*> traverse pPurp2aPurp (pt_xps ppat) where f rules' keys' pops' views' xpls = let (decls',dPops) = unzip [ pDecl2aDecl (name ppat) deflangCtxt deffrmtCtxt pDecl | pDecl<-pt_dcs ppat ] in A_Pat { ptnm = name ppat , ptpos = pt_pos ppat , ptend = pt_end ppat , ptrls = rules' , ptgns = map pGen2aGen (pt_gns ppat) , ptdcs = decls' , ptups = pops' ++ [ dp | dp@PRelPopu{}<-dPops, (not.null.popps) dp ] ++ [ cp | cp@PCptPopu{}<-dPops, (not.null.popas) cp ] , ptids = keys' , ptvds = views' , ptxps = xpls } pRul2aRul :: String -- environment name (pattern / proc name) -> (P_Rule TermPrim) -> Guarded Rule pRul2aRul env = typeCheckRul env . disambiguate termPrimDisAmb typeCheckRul :: String -- environment name (pattern / proc name) -> (P_Rule (TermPrim, DisambPrim)) -> Guarded Rule typeCheckRul env P_Ru { rr_nm = nm , rr_exp = expr , rr_fps = orig , rr_mean = meanings , rr_msg = msgs , rr_viol = viols } = unguard $ (\ (exp',_) -> (\ vls -> Ru { rrnm = nm , rrexp = exp' , rrfps = orig , rrmean = pMean2aMean deflangCtxt deffrmtCtxt meanings , rrmsg = map (pMess2aMess deflangCtxt deffrmtCtxt) msgs , rrviol = vls , rrtyp = sign exp' , rrdcl = Nothing , r_env = env , r_usr = UserDefined , isSignal = not . null . concatMap arRoles . filter (\x -> nm `elem` arRules x) $ allRoleRules }) <$> maybeOverGuarded (typeCheckPairView orig exp') viols) <$> typecheckTerm expr pIdentity2aIdentity :: P_IdentDef -> Guarded IdentityDef pIdentity2aIdentity pidt = case disambiguate termPrimDisAmb pidt of P_Id { ix_lbl = lbl , ix_ats = isegs } -> (\isegs' -> Id { idPos = orig , idLbl = lbl , idCpt = conc , identityAts = isegs' }) <$> traverse pIdentSegment2IdentSegment isegs where conc = pCpt2aCpt (ix_cpt pidt) orig = ix_pos pidt pIdentSegment2IdentSegment :: P_IdentSegmnt (TermPrim, DisambPrim) -> Guarded IdentitySegment pIdentSegment2IdentSegment (P_IdentExp ojd) = unguard $ (\o -> case findExact genLattice $ name (source $ objctx o) `mjoin` name conc of [] -> mustBeOrdered orig (Src, origin ojd, objctx o) pidt _ -> pure $ IdentityExp o{objctx = addEpsilonLeft' (name conc) (objctx o)} ) <$> pObjDefDisamb2aObjDef ojd typeCheckPairView :: Origin -> Expression -> PairView (Term (TermPrim, DisambPrim)) -> Guarded (PairView Expression) typeCheckPairView o x (PairView lst) = PairView <$> traverse (typeCheckPairViewSeg o x) lst typeCheckPairViewSeg :: Origin -> Expression -> (PairViewSegment (Term (TermPrim, DisambPrim))) -> Guarded (PairViewSegment Expression) typeCheckPairViewSeg _ _ (PairViewText orig x) = pure (PairViewText orig x) typeCheckPairViewSeg o t (PairViewExp orig s x) = unguard $ (\(e,(b,_)) -> case (findSubsets genLattice (mjoin (name (source e)) (getConcept s t))) of [] -> mustBeOrdered o (Src, (origin (fmap fst x)), e) (s,t) lst -> if b || and (map (name (source e) `elem`) lst) then pure (PairViewExp orig s e) else mustBeBound (origin (fmap fst x)) [(Src, e)]) <$> typecheckTerm x pPurp2aPurp :: PPurpose -> Guarded Purpose pPurp2aPurp PRef2 { pexPos = orig -- :: Origin , pexObj = objref -- :: PRefObj , pexMarkup = pmarkup -- :: P_Markup , pexRefIDs = refIds -- :: [String] } = (\ obj -> Expl { explPos = orig , explObj = obj , explMarkup = pMarkup2aMarkup deflangCtxt deffrmtCtxt pmarkup , explUserdefd = True , explRefIds = refIds }) <$> pRefObj2aRefObj objref pRefObj2aRefObj :: PRef2Obj -> Guarded ExplObj pRefObj2aRefObj (PRef2ConceptDef s ) = pure$ ExplConceptDef (lookupConceptDef s) pRefObj2aRefObj (PRef2Declaration tm) = ExplDeclaration <$> (namedRel2Decl tm) pRefObj2aRefObj (PRef2Rule s ) = pure$ ExplRule s pRefObj2aRefObj (PRef2IdentityDef s ) = pure$ ExplIdentityDef s pRefObj2aRefObj (PRef2ViewDef s ) = pure$ ExplViewDef s pRefObj2aRefObj (PRef2Pattern s ) = pure$ ExplPattern s pRefObj2aRefObj (PRef2Interface s ) = pure$ ExplInterface s pRefObj2aRefObj (PRef2Context s ) = pure$ ExplContext s pRefObj2aRefObj (PRef2Fspc s ) = pure$ ExplContext s lookupConceptDef :: String -> ConceptDef lookupConceptDef s = case filter (\cd -> name cd == s) allConceptDefs of [] -> Cd{cdpos=OriginUnknown, cdcpt=s, cdplug=True, cddef="", cdtyp="", cdref="", cdfrom=n1} (x:_) -> x allConceptDefs :: [ConceptDef] allConceptDefs = p_conceptdefs++concatMap pt_cds (p_patterns++p_processes) allRoleRules :: [A_RoleRule] allRoleRules = map pRoleRule2aRoleRule (p_roleRules ++ concatMap pt_RRuls (p_patterns++p_processes)) pDisAmb2Expr :: (TermPrim, DisambPrim) -> Guarded Expression pDisAmb2Expr (_,Known x) = pure x pDisAmb2Expr (_,Rel [x]) = pure x pDisAmb2Expr (o,Rel rs) = cannotDisambRel o rs pDisAmb2Expr (o,_) = cannotDisamb o pMean2aMean :: Lang -- The default language -> PandocFormat -- The default pandocFormat -> [PMeaning] -> AMeaning pMean2aMean defLanguage defFormat pmeanings = AMeaning [ pMarkup2aMarkup defLanguage defFormat pmarkup | PMeaning pmarkup <-pmeanings ] pMess2aMess :: Lang -- The default language -> PandocFormat -- The default pandocFormat -> PMessage -> A_Markup pMess2aMess defLanguage defFormat (PMessage x) = pMarkup2aMarkup defLanguage defFormat x pMarkup2aMarkup :: Lang -- The default language -> PandocFormat -- The default pandocFormat -> P_Markup -> A_Markup pMarkup2aMarkup defLanguage defFormat P_Markup { mLang = ml , mFormat = mpdf , mString = str } = A_Markup { amLang = fromMaybe defLanguage ml -- The language is always defined; if not by the user, then by default. , amFormat = fmt , amPandoc = string2Blocks fmt str } where fmt = fromMaybe defFormat mpdf -- The pandoc format is always defined; if not by the user, then by default. -- helpers for generating a lattice, not having to write `Atom' all the time -- TODO: Names are inconsistent: maybe call these either mUnion & mIsc or mJoin & mMeet? Or even lJoin and lMeet to denote the lattice. mjoin,mIsc :: a -> a -> FreeLattice a mjoin a b = Join (Atom a) (Atom b) mIsc a b = Meet (Atom a) (Atom b) -- intended for finding the right expression on terms like (Src,fst) resolve :: t -> (SrcOrTgt, t -> (t1, (t2, t2))) -> (SrcOrTgt, (t1, t2)) resolve es (p,f) = case (p,f es) of (Src,(e,(b,_))) -> (Src,(e,b)) (Tgt,(e,(_,b))) -> (Tgt,(e,b)) maybeOverGuarded :: Applicative f => (t -> f a) -> Maybe t -> f (Maybe a) maybeOverGuarded _ Nothing = pure Nothing maybeOverGuarded f (Just x) = Just <$> f x data TT a -- (In order of increasing strictness. If you are unsure which to pick: just use MBE, it'll usually work fine) = UNI a a -- find the union of these types, return it. | ISC a a -- find the intersection of these types, return it. | MBE a a -- must be equal: must be (made) of equal type. If these types are comparable, it returns the greatest. | MBG a a -- The first of these types must be the greatest, if so, return it (error otherwise) -- SJC: difference between UNI and MBE -- in general, UNI is less strict than MBE: -- suppose A ≤ C, B ≤ C, and C is the least such concept (e.g. if A≤D and B≤D then C≤D) -- in this case UNI A B will yield C (if both A and B are generalizable), while MBE A B will give an error -- note that in case of A ≤ C, B ≤ C, A ≤ D, B ≤ D (and there is no order between C and D), both will give an error -- the error message, however, should be different: -- for MBE it says that A and B must be of the same type, and suggests adding an order between A and B -- for UNI it says that it cannot decide whether A \/ B is of type C or D, and suggests adding an order between C and D -- In addition, MBE requires that both sides are not generalizable. UNI does not, and simply propagates this property. -- MBG is like MBE, but will only try to generalize the right hand side (when allowed) deriv' :: (Applicative f) => ((SrcOrTgt, t -> (Expression, (Bool, Bool))), (SrcOrTgt, t -> (Expression, (Bool, Bool)))) -> t -> f ((String, Bool), (String, Bool)) deriv' (a,b) es = let (sourceOrTarget1, (e1, t1)) = resolve es a (sourceOrTarget2, (e2, t2)) = resolve es b in pure ((getConcept sourceOrTarget1 e1, t1), (getConcept sourceOrTarget2 e2, t2)) instance Functor TT where fmap f (UNI a b) = UNI (f a) (f b) fmap f (ISC a b) = ISC (f a) (f b) fmap f (MBE a b) = MBE (f a) (f b) fmap f (MBG a b) = MBG (f a) (f b) -- TODO: would probably be better to return an A_Concept getConcept :: SrcOrTgt -> Expression -> String getConcept Src = name . source getConcept Tgt = name . target