0cd45e749d5c847c9652afdd0617a18488a94d1fChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : Replace Sorted_term(s) with explicit injection functions.

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiCopyright : (c) Christian Maeder, Uni Bremen 2005

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiStability : provisional

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiPortability : portable

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiReplace Sorted_term(s) with explicit injection functions. Don't do this after

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski simplification since crucial sort information may be missing

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski -}

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskimodule CASL.Inject where

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport CASL.AS_Basic_CASL

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport CASL.Sign

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport CASL.Fold

881f43de18aeae879886be203cd32e90051799c0Till Mossakowskiimport Common.Id

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder

881f43de18aeae879886be203cd32e90051799c0Till MossakowskimakeInjOrProj :: (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> SORT

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder -> TERM f

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeInjOrProj mkName fk pos argument to =

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski let from = sortOfTerm argument

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski t = Op_type fk [from] to pos

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski in if to == from then argument else

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder Application (Qual_op_name (mkName t) t pos) [argument] pos

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

2bbf88585fe313af8585da0288880310cc1b027dChristian MaederinjectUnique :: Range -> TERM f -> SORT -> TERM f

da955132262baab309a50fdffe228c9efe68251dCui JianinjectUnique = makeInjOrProj uniqueInjName Total

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski

2bbf88585fe313af8585da0288880310cc1b027dChristian MaederuniqueInjName :: OP_TYPE -> Id

881f43de18aeae879886be203cd32e90051799c0Till MossakowskiuniqueInjName t = case t of

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski Op_type _ [from] to _ -> mkUniqueInjName from to

881f43de18aeae879886be203cd32e90051799c0Till Mossakowski _ -> error "CASL.Inject.uniqueInjName"

2bbf88585fe313af8585da0288880310cc1b027dChristian Maeder

injRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)

injRecord mf = (mapRecord mf)

{ foldApplication = \ _ o ts ps -> case o of

Qual_op_name _ ty _ -> Application o

(zipWith (injectUnique ps) ts $ args_OP_TYPE ty) ps

_ -> error "injApplication"

, foldSorted_term = \ _ st s ps -> injectUnique ps st s

, foldPredication = \ _ p ts ps -> case p of

Qual_pred_name _ (Pred_type s _) _ -> Predication p

(zipWith (injectUnique ps) ts s) ps

_ -> error "injPredication" }

injTerm :: (f -> f) -> TERM f -> TERM f

injTerm = foldTerm . injRecord

injFormula :: (f -> f) -> FORMULA f -> FORMULA f

injFormula = foldFormula . injRecord

-- | takes a list of OP_SYMB generated by

-- 'CASL.AS_Basic_CASL.recover_Sort_gen_ax' and inserts these operations into

-- the signature; unqualified OP_SYMBs yield an error

insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e

insertInjOps = foldl insOp

where insOp sign o =

case o of

(Qual_op_name i ot _)

| isInjName i ->

sign { opMap = addOpTo i (toOpType ot) (opMap sign)}

| otherwise -> sign

_ -> error "CASL.Inject.insertInjOps: Wrong constructor."