{-# OPTIONS_GHC -Wall -XFlexibleInstances -XDataKinds #-}
{-# LANGUAGE RelaxedPolyRec #-}
module DatabaseDesign.Ampersand.ADL1.P2A_Converters ( pCtx2aCtx, showErr, Guarded(..) )
where
import DatabaseDesign.Ampersand.ADL1.Disambiguate
import DatabaseDesign.Ampersand.Core.ParseTree -- (P_Context(..), A_Context(..))
import DatabaseDesign.Ampersand.Input.ADL1.CtxError
import DatabaseDesign.Ampersand.ADL1.Lattices
import DatabaseDesign.Ampersand.Core.AbstractSyntaxTree hiding (sortWith, maxima, greatest)
import DatabaseDesign.Ampersand.Classes.ViewPoint hiding (interfaces,gens)
import DatabaseDesign.Ampersand.Classes.ConceptStructure
import DatabaseDesign.Ampersand.Basics (Identified(name), fatalMsg)
import DatabaseDesign.Ampersand.Misc
import Prelude hiding (head, sequence, mapM)
import Control.Applicative
import Data.Traversable
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
import Data.List(nub)

head :: [a] -> a
head [] = fatal 30 "head must not be used on an empty list!"
head (a:_) = a

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 :: P_Context -> Guarded A_Context
pCtx2aCtx pCtx = finalChecksOnAContext <?> pCtx2aCtx' pCtx 
  where 
    finalChecksOnAContext :: A_Context -> Guarded A_Context
    finalChecksOnAContext ctx = checkUniqueRuleNames
      where
        checkUniqueRuleNames 
          = case uniqueNames (udefrules ctx) of 
              Checked _   -> Checked ctx
              Errors err  -> Errors err


pCtx2aCtx' :: P_Context -> Guarded A_Context
pCtx2aCtx' 
 PCtx { ctx_nm     = n1
      , ctx_pos    = n2
      , ctx_lang   = lang
      , ctx_markup = pandocf
      , ctx_thms   = p_themes       --  The themes that are specified by the user to be documented.
      , ctx_pats   = p_patterns     --  The patterns defined in this context
      , ctx_PPrcs  = p_processes    --  The processes as defined by the parser
      , ctx_rs     = p_rules        --  All user defined rules in this context, but outside patterns and outside processes
      , ctx_ds     = p_declarations --  The relations declared in this context, outside the scope of patterns
      , ctx_cs     = p_conceptdefs  --  The concept definitions defined in this context, outside the scope of patterns
      , ctx_ks     = p_identdefs    --  The identity definitions defined in this context, outside the scope of patterns
      , ctx_vs     = p_viewdefs     --  The view definitions defined in this context, outside the scope of patterns
      , ctx_gs     = p_gens         --  The gen definitions defined in this context, outside the scope of patterns
      , ctx_ifcs   = p_interfaces   --  The interfaces defined in this context, outside the scope of patterns
      , ctx_ps     = p_purposes     --  The purposes defined in this context, outside the scope of patterns
      , ctx_pops   = p_pops         --  The populations defined in this context, but outside patterns and outside processes
      , ctx_sql    = p_sqldefs      --  user defined sqlplugs, taken from the Ampersand script
      , ctx_php    = p_phpdefs      --  user defined phpplugs, taken from the Ampersand script
      , ctx_metas  = p_metas        --  generic meta information (name/value pairs) that can be used for experimenting without having to modify the adl syntax
      }
 = (\pats procs rules identdefs viewdefs interfaces purposes udpops sqldefs phpdefs
     -> ACtx{ ctxnm = n1
            , ctxpos = n2
            , ctxlang = deflangCtxt
            , ctxmarkup = deffrmtCtxt
            , ctxthms = p_themes
            , ctxpats = pats
            , ctxprocs = procs
            , ctxrs = rules
            , ctxds = ctxDecls
            , ctxpopus = nub (udpops++dclPops++mp1Pops rules++mp1Pops pats++mp1Pops procs++mp1Pops identdefs++mp1Pops viewdefs++mp1Pops interfaces)
            , ctxcds = allConceptDefs
            , ctxks = identdefs
            , 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            --  The patterns defined in this context
      <*> traverse pProc2aProc p_processes         --  The processes 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_interfaces          --  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
  where
    -- 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 ++ concatMap procGens 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 = fromMaybe English lang  -- explanation: if lang==Nothing, then English, if lang==Just l then l
    deffrmtCtxt = fromMaybe ReST pandocf

    (decls,dclPops)= unzip dps
    (ctxDecls,_ ) = unzip ctxDecls'
    dps = ctxDecls'++patDecls++patProcs
    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, pDecl<-pt_dcs pat ] --  The relations declared in all patterns within this context.
    patProcs  = [ pDecl2aDecl (name prc) deflangCtxt deffrmtCtxt pDecl | prc<-p_processes, pDecl<-procDcls prc ] --  The relations declared in all processes within this context.
      
    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
    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)

{- SJ20140216: The function castConcept is used in the type system, but looks similar to pCpt2aCpt.
   However, castConcept makes an erroneous concept, which we should prevent in the first place.
   So it seems castConcept should be removed if possible, and pCpt2aCpt should be doing all the work. 
-}
    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}

    pCpt2aCpt :: P_Concept -> A_Concept
    pCpt2aCpt pc
        = case pc of
            PCpt{} -> PlainConcept { cptnm = p_cptnm pc}
            P_Singleton -> ONE   

    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 = fmap fst (typecheckObjDef tpda)
     where tpda = disambiguate termPrimDisAmb 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_ats = pvs -- view segment
            })
     = (\vdts
        -> Vd { vdpos = orig
              , vdlbl = lbl
              , vdcpt = pCpt2aCpt cpt
              , vdats = vdts
              })
       <$> traverse (typeCheckViewSegment o) pvs
    
    typeCheckViewSegment :: (P_ViewD a) -> (P_ViewSegmt (TermPrim, DisambPrim)) -> Guarded ViewSegment
    typeCheckViewSegment o P_ViewExp{ vs_obj = ojd }
     = (\(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 c r (name (source (objctx obj))) (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
    
    typecheckObjDef :: (P_ObjDef (TermPrim, DisambPrim)) -> Guarded (ObjectDef, Bool)
    typecheckObjDef o@(P_Obj { obj_nm = nm
                             , obj_pos = orig
                             , obj_ctx = ctx
                             , obj_msub = subs
                             , obj_strs = ostrs
                             })
     = (\(expr,subi)
        -> case subi of
            Nothing -> pure (obj expr Nothing)
            Just (InterfaceRef s) -> pure (obj expr (Just$InterfaceRef s)) --TODO: check type!
            Just b@(Box c _)
              -> case findExact genLattice (mjoin (name c) (gc Tgt (fst expr))) of
                    [] -> mustBeOrdered o (Src,c,((\(Just x)->x) subs)) (Tgt,target (fst expr),(fst expr))
                    r  -> if (name c) `elem` r
                          then pure (obj (addEpsilonRight' (name c) (fst expr), snd expr) (Just$ b))
                          else mustBeBound (origin o) [(Tgt,fst expr)]
       ) <?> ((,) <$> typecheckTerm ctx <*> maybeOverGuarded pSubi2aSubi subs)
     where
      obj (e,(sr,_)) s
       = ( Obj { objnm = nm
               , objpos = orig
               , objctx = e
               , objmsub = s
               , objstrs = ostrs
               }, sr)
    addEpsilonLeft :: String -> [String] -> String -> Expression -> Expression
    addEpsilonLeft a b c e
     = if a==c then (if c `elem` b then e else fatal 200 "b == c must hold: the concept of the epsilon relation should be equal to the intersection of its source and target")
               else if c/=name (source e) then fatal 202 ("addEpsilonLeft glues erroneously: c="++show c++"  and e="++show e++".")
                    else EEps (castConcept (head b)) (castSign a c) .:. e
    addEpsilonLeft',addEpsilonRight' :: String -> Expression -> Expression
    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
     = (if s==name (source e) then id else (EEps (leastConcept (source e) s) (castSign s (name (source e))) .:.)) $
       (if t==name (target e) then id else (.:. EEps (leastConcept (target e) t) (castSign (name (target e)) t))) e
    
    pSubi2aSubi :: (P_SubIfc (TermPrim, DisambPrim)) -> Guarded SubInterface
    pSubi2aSubi (P_InterfaceRef _ s) = pure (InterfaceRef s)
    pSubi2aSubi o@(P_Box _ []) = hasNone [] o
    pSubi2aSubi o@(P_Box _ l)
     = (\lst -> case findExact genLattice (foldr1 Join (map (Atom . name . source . objctx . fst) lst)) of
                  [] -> mustBeOrderedLst o [(source (objctx a),Src, a) | (a,_) <- lst]
                  r -> case [ objctx a
                            | (a,False) <- lst
                            , not ((name . source . objctx $ a) `elem` r)
                            ] of
                            [] -> pure (Box (castConcept (head r)) (map fst lst))
                            lst' -> mustBeBound (origin o) [(Src,expr)| expr<-lst']
       ) <?> (traverse typecheckObjDef l <* uniqueNames l)
    
    
    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 -> binary  (.==.) (MBE (Src,fst) (Src,snd), MBE (Tgt,fst) (Tgt,snd)) <?> ((,)<$>tt a<*>tt b) 
         Pimp _ a b -> binary  (.|-.) (MBG (Src,snd) (Src,fst), MBG (Tgt,snd) (Tgt,fst)) <?> ((,)<$>tt a<*>tt b)
         PIsc _ a b -> binary  (./\.) (ISC (Src,fst) (Src,snd), ISC (Tgt,fst) (Tgt,snd)) <?> ((,)<$>tt a<*>tt b)
         PUni _ a b -> binary  (.\/.) (UNI (Src,fst) (Src,snd), UNI (Tgt,fst) (Tgt,snd)) <?> ((,)<$>tt a<*>tt b)
         PDif _ a b -> binary  (.-.)  (MBG (Src,fst) (Src,snd), MBG (Tgt,fst) (Tgt,snd)) <?> ((,)<$>tt a<*>tt b)
         PLrs _ a b -> binary' (./.)  (MBG (Tgt,snd) (Tgt,fst)) ((Src,fst),(Src,snd)) Tgt Tgt <?> ((,)<$>tt a<*>tt b)
         PRrs _ a b -> binary' (.\.)  (MBG (Src,fst) (Src,snd)) ((Tgt,fst),(Tgt,snd)) Src Src <?> ((,)<$>tt a<*>tt b)
         PDia _ a b -> 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 -> binary' (.:.)  (ISC (Tgt,fst) (Src,snd)) ((Src,fst),(Tgt,snd)) Tgt Src <?> ((,)<$>tt a<*>tt b)
         PRad _ a b -> 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   -> unary   EKl0   (UNI (Src, id) (Tgt, id), UNI (Src, id) (Tgt, id)) <?> tt a
         PKl1 _ a   -> 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) || (gc p1 e1 == gc 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 (gc p1 e1) (gc 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 (gc p1 e1) (gc 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 (gc p1 e1) r,b2 || Set.member (gc 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)
       where head' [] =fatal 321 ("empty list on expressions "++show ((p1,b1,e1),(p2,b2,e2)))
             head' (a:_) = a
    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)))
           Prel _ r    -> Rel [EDcD dc | dc <- (Map.elems $ findDecls r)]
           PTrel _ r s -> Rel [EDcD dc | dc <- (findDeclsTyped r (pSign2aSign s))]
        )
    
    termPrim2Decl :: TermPrim -> Guarded Declaration
    termPrim2Decl o@(Prel _ r   ) = getOneExactly o [ dc | dc <- (Map.elems $ findDecls r)]
    termPrim2Decl o@(PTrel _ r s) = getOneExactly o [ dc | dc <- (findDeclsTyped r (pSign2aSign s))]
    termPrim2Decl _ = fatal 231 "Expecting Declaration"
    termPrim2Expr :: TermPrim -> Guarded Expression
    termPrim2Expr = pDisAmb2Expr . termPrimDisAmb
    
    pIfc2aIfc :: P_Interface -> Guarded Interface
    pIfc2aIfc P_Ifc { ifc_Params = tps
                    , ifc_Args = args
                    , ifc_Roles = rols
                    , ifc_Obj = obj
                    , ifc_Pos = orig
                    -- , ifc_Name = nm
                    , ifc_Prp = prp
                    }
        = (\ tps' obj'
             -> Ifc { ifcParams = tps'
                    , ifcArgs = args
                    , ifcRoles = rols
                    , ifcObj = obj'
                    , ifcPos = orig
                    , ifcPrp = prp
                    }) <$> traverse termPrim2Expr tps
                       <*> pObjDef2aObjDef obj
    pProc2aProc :: P_Process -> Guarded Process
    pProc2aProc P_Prc { procNm = nm
                      , procPos = orig
                      , procEnd = posEnd
                      , procRules = ruls
                      , procGens = gens
                      , procDcls = dcls
                      , procRRuls = rolruls
                      , procRRels = rolrels
                      , procCds = _cdefs -- SJ2013: the underscore means that this argument is not used.
                      , procIds = idefs
                      , procVds = viewdefs
                      , procXps = purposes
                      , procPop = pops
                      }
     = (\ ruls' rels' pops' idefs' viewdefs' purposes'
         ->  let (decls',dPops) = unzip [ pDecl2aDecl nm deflangCtxt deffrmtCtxt pDecl | pDecl<-dcls ]
             in Proc { prcNm = nm
                     , prcPos = orig
                     , prcEnd = posEnd
                     , prcRules = map snd ruls'
                     , prcGens = map pGen2aGen gens
                     , prcDcls = decls'
                     , prcUps = pops' ++ [ dp | dp@PRelPopu{}<-dPops, (not.null.popps) dp ] ++ [ cp | cp@PCptPopu{}<-dPops, (not.null.popas) cp ]
                     , prcRRuls = [(rol,r)|(rols,r)<-ruls',rol<-rols]
                     , prcRRels = [(rol,r)|(rols,rs)<-rels',rol<-rols,r<-rs]
                     , prcIds = idefs'
                     , prcVds = viewdefs'
                     , prcXps = purposes'
                     }
       ) <$> traverse (\x -> pRul2aRul' [rol | rr <- rolruls, rul <- mRules rr, name x == rul, rol <- mRoles rr] nm x) ruls
         <*> sequenceA [(\x -> (rr_Roles prr,x)) <$> (traverse termPrim2Decl $ rr_Rels prr) | prr <- rolrels]
         <*> traverse pPop2aPop pops
         <*> traverse pIdentity2aIdentity idefs
         <*> traverse pViewDef2aViewDef viewdefs
         <*> traverse pPurp2aPurp purposes
    
    pPat2aPat :: P_Pattern -> Guarded Pattern
    pPat2aPat ppat
     = f <$> parRuls ppat <*> parKeys ppat <*> parPops ppat <*> parViews ppat <*> parPrps ppat <*> sequenceA rrels
       where
        f prules keys' pops' views' xpls rrels'
           = 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 = map snd prules
                      , ptgns = agens'
                      , ptdcs = decls'
                      , ptups = pops' ++ [ dp | dp@PRelPopu{}<-dPops, (not.null.popps) dp ] ++ [ cp | cp@PCptPopu{}<-dPops, (not.null.popas) cp ]
                      , ptrruls = [(rol,r)|(rols,r)<-prules,rol<-rols]
                      , ptrrels = [(rol,dcl)|rr<-rrels', rol<-rrRoles rr, dcl<-rrRels rr]  -- The assignment of roles to Relations.
                      , ptids = keys'
                      , ptvds = views'
                      , ptxps = xpls
                      }
        agens'   = map pGen2aGen (pt_gns ppat)
        parRuls  = traverse (\x -> pRul2aRul' [rol | prr <- pt_rus ppat, rul<-mRules prr, name x == rul, rol<-mRoles prr] (name ppat) x) . pt_rls
        rrels :: [Guarded RoleRelation]
        rrels =  [(\x -> RR (rr_Roles prr) x (origin prr)) <$> (traverse termPrim2Decl $ rr_Rels prr) | prr <- pt_res ppat]
        parKeys  = traverse pIdentity2aIdentity . pt_ids
        parPops  = traverse pPop2aPop . pt_pop
        parViews = traverse pViewDef2aViewDef . pt_vds
        parPrps  = traverse pPurp2aPurp . pt_xps
    
    pRul2aRul':: [String] -- list of roles for this rule
              -> String -- environment name (pattern / proc name)
              -> (P_Rule TermPrim) -> Guarded ([String],Rule)  -- roles in the lhs
    pRul2aRul' a b c = fmap ((,) a) (pRul2aRul a b c)
    pRul2aRul :: [String] -- list of roles for this rule
              -> String -- environment name (pattern / proc name)
              -> (P_Rule TermPrim) -> Guarded Rule
    pRul2aRul rol env = typeCheckRul rol env . disambiguate termPrimDisAmb
    typeCheckRul :: [String] -- list of roles for this rule
              -> String -- environment name (pattern / proc name)
              -> (P_Rule (TermPrim, DisambPrim)) -> Guarded Rule
    typeCheckRul sgl env P_Ru { rr_nm = nm
                       , rr_exp = expr
                       , rr_fps = orig
                       , rr_mean = meanings
                       , rr_msg = msgs
                       , rr_viol = viols
                       }
     = (\ (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 sgl)
             , srrel = Sgn{ decnm   = nm
                          , decsgn  = (sign exp')
                          , decprps = []
                          , decprps_calc = Nothing
                          , decprL  = ""
                          , decprM  = ""
                          , decprR  = ""
                          , decMean = pMean2aMean deflangCtxt deffrmtCtxt meanings
                          , decfpos = orig
                          , deciss  = True
                          , decusr  = False
                          , decpat  = env
                          , decplug = False
                          }
             }
             ) <$> maybeOverGuarded (typeCheckPairView orig exp') viols
          ) <?> typecheckTerm expr
    pIdentity2aIdentity :: P_IdentDef -> Guarded IdentityDef
    pIdentity2aIdentity
            P_Id { ix_pos = orig
                 , ix_lbl = lbl
                 , ix_cpt = pconc
                 , ix_ats = isegs
                 }
     = (\isegs' ->
       Id { idPos = orig
          , idLbl = lbl
          , idCpt = pCpt2aCpt pconc
          , identityAts = isegs'
          }) <$> traverse pIdentSegment2IdentSegment isegs
    pIdentSegment2IdentSegment :: P_IdentSegment -> Guarded IdentitySegment
    pIdentSegment2IdentSegment (P_IdentExp ojd)
     = IdentityExp <$> pObjDef2aObjDef 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 x) = pure (PairViewText x)
    typeCheckPairViewSeg o t (PairViewExp s x)
     = (\(e,(b,_)) -> case (findSubsets genLattice (mjoin (name (source e)) (gc s t))) of
                        [] -> mustBeOrdered o (Src,e) (s,t)
                        lst -> if b || and (map (name (source e) `elem`) lst)
                               then pure (PairViewExp s e)
                               else mustBeBound o [(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 <$> (termPrim2Decl 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 (PRef2Process     s ) = pure$ ExplProcess s
    pRefObj2aRefObj (PRef2Interface   s ) = pure$ ExplInterface s
    pRefObj2aRefObj (PRef2Context     s ) = pure$ ExplContext s
    pRefObj2aRefObj (PRef2Fspc        s ) = pure$ ExplContext s
    lookupConceptDef :: String -> ConceptDef
    lookupConceptDef s
     = if null cs
       then Cd{cdpos=OriginUnknown, cdcpt=s, cdplug=True, cddef="", cdtyp="", cdref="", cdfrom=n1}
       else head cs
       where cs = [cd | cd<-allConceptDefs, name cd==s]
    allConceptDefs :: [ConceptDef]
    allConceptDefs = p_conceptdefs++concatMap pt_cds p_patterns++concatMap procCds p_processes
    
pDisAmb2Expr :: (TermPrim, DisambPrim) -> Guarded Expression
-- SJ 20140211 @SJC: TODO graag een typefout genereren voor een SESSION atoom anders dan _SESSION.
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
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 ((gc sourceOrTarget1 e1, t1), (gc 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)