{- |

Module : $Header$

Copyright : (c) Christian Maeder, Uni Bremen 2005

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : maeder@tzi.de

Stability : provisional

Portability : portable

Description : Replace Sorted_term(s) with explicit injection functions.

Don't do this after simplification since crucial sort information may be missing

-}

module CASL.Inject where

import CASL.AS_Basic_CASL

import CASL.Sign

import CASL.Overload

import CASL.Fold

import Common.Id

import Common.DocUtils

-- | the name of injections

injName :: Id

injName = mkId [mkSimpleId $ genNamePrefix ++ "inj"]

inject :: Range -> TERM f -> SORT -> TERM f

inject pos argument result_type = let argument_type = term_sort argument in

if argument_type == result_type then argument else

Application (injOpSymb pos argument_type result_type) [argument] nullRange

injOpSymb :: Range -> SORT -> SORT -> OP_SYMB

injOpSymb pos s1 s2 =

Qual_op_name injName (Op_type Total [s1] s2 pos) pos

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 (inject ps) ts $ args_OP_TYPE ty) ps

_ -> error "injApplication"

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

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

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

(zipWith (inject 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 ::(Pretty f) => Sign f e -> [OP_SYMB] -> Sign f e

insertInjOps = foldl insOp

where insOp sign o =

case o of

(Qual_op_name i ot _)

| i == injName ->

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

| otherwise -> sign

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