CurryInfo: call-analysis-3.2.0 / Analysis.matchCTerms

 
matchCTerms :: [Term] -> [CTerm] -> Maybe (Sub CTerm)
matchCTerms []     []     = Just []
matchCTerms []     (_:_)  = Nothing
matchCTerms (_:_)  []     = Nothing
matchCTerms (x:xs) (y:ys) = combineSubst (match x y) (matchCTerms xs ys)
 where
  combineSubst Nothing   _         = Nothing
  combineSubst (Just _ ) Nothing   = Nothing
  combineSubst (Just s1) (Just s2) = Just (s1++s2)

  -- match a linear pattern against a term with disjoint variables:
  match :: Term -> CTerm -> Maybe (Sub CTerm)
  match (Var v) t = Just [(v,t)]
  match (Func _ pf pargs) t = case t of
    CBot           -> Nothing
    CVar _         -> Nothing
    CCons tf targs -> if pf==tf then matchCTerms pargs targs else Nothing

 arguments 1 2

 deterministic operation

 
pairwise matching of a list of patterns against a list of terms

 (_, _)

 referentially transparent operation

 no fixity defined

 {({[]},{[]}) |-> {Just} || ({[]},{:}) |-> {Nothing} || ({:},{[]}) |-> {Nothing} || ({:},{:}) |-> {Just,Nothing}}

 matchCTerms

 no precedence defined

 {Just,Nothing}

 [TRS.Term] -> [CTerm] -> Prelude.Maybe [(Prelude.Int, CTerm)]

 operation might suspend on free variables

 possibly non-terminating

 reducible on all ground data terms