CurryInfo: call-analysis-3.2.0 / Analysis.matchDTerms

 
matchDTerms :: [Term] -> [DTerm] -> Maybe (Sub DTerm)
matchDTerms [] [] = Just []
matchDTerms [] (_:_) = Nothing
matchDTerms (_:_) [] = Nothing
matchDTerms (x:xs) (y:ys) = combineSubst (match x y) (matchDTerms 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 -> DTerm -> Maybe (Sub DTerm)
  match (Var v) t = Just [(v,t)]
  match (Func _ pf pargs) t = case t of
    DBot   -> Nothing
    CutVar -> Just (map (\v->(v,CutVar)) (concatMap varsOf pargs))
    DCons tf targs -> if pf==tf then matchDTerms pargs targs else Nothing

 arguments 1 2

 deterministic operation

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

 <FAILING>

 referentially transparent operation

 no fixity defined

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

 matchDTerms

 no precedence defined

 {Just,Nothing}

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

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term