hets/ATC/Grothendieck.hs

	Grothendieck.hs revision 503e836b34d3abed34520eb4a0a345b5e13f248d
{-
   File: ATC/Grothendieck.hs
   ShATermConvertible instances for the datatypes in Logic/Grothendieck.hs
   Author: Felix Reckers
   Year: 2003
-}

module ATC.Grothendieck where

import Logic.Grothendieck
import Common.ATerm.Lib
import Common.Result
import Comorphisms.LogicGraph
import Logic.Logic
import ATC.Comorphism
import ATC.Named
import Logic.Logic
import Logic.Comorphism
import ATC.Graph
import qualified Common.Lib.Set as Set

instance ATermConvertible G_basic_spec where
     toShATerm att0 (G_basic_spec lid basic_spec) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 basic_spec of { (att2,i2) ->
           addATerm (ShAAppl "G_basic_spec" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_basic_spec" [i1,i2] _) ->
		case fromShATerm (getATermByIndex1 i1 att) of { i1' ->
                case (getATermByIndex1 i2 att) of { att' ->
                case lookupLogic_in_LG
		      ("ATermConvertible G_basic_spec:") i1'  of {
		    Logic lid ->
			G_basic_spec lid (fromShATerm_basic_spec lid att')}}}
	    u     -> fromShATermError "G_basic_spec" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_basic_spec\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_basic_spec\""

instance ATermConvertible G_sentence where
     toShATerm att0 (G_sentence lid sentence) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 sentence of { (att2,i2) ->
           addATerm (ShAAppl "G_sentence" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_sentence" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
		    l = lookupLogic_in_LG ("ATerm_Convertible G_sentence:") i1'
                in case l of
                    Logic lid -> (G_sentence lid (fromShATerm_sentence lid att'))
	    u     -> fromShATermError "G_sentence" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_sentence\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_sentence\""

instance ATermConvertible G_l_sentence_list where
     toShATerm att0 (G_l_sentence lid n_sentence) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 n_sentence of { (att2,i2) ->
            addATerm (ShAAppl "G_l_sentence" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_l_sentence" [i1,i2] _) ->
	       case fromShATerm (getATermByIndex1 i1 att) of { i1' ->
               case getATermByIndex1 i2 att of { att' ->
               case lookupLogic_in_LG
                        ("ATermConvertible G_l_sentence_list") i1'  of {
                    Logic lid -> (G_l_sentence lid (fromShATerm_l_sentence_list lid att'))}}}
	    u     -> fromShATermError "G_l_sentence" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_l_sentence\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_l_sentence\""

instance ATermConvertible G_sign where
     toShATerm att0 (G_sign lid sign) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 sign of { (att2,i2) ->
           addATerm (ShAAppl "G_sign" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_sign" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_sign:") i1'
                in case l of
                    Logic lid -> (G_sign lid (fromShATerm_sign lid att'))
	    u     -> fromShATermError "G_sign" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_sign\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_sign\""

instance ATermConvertible G_ext_sign where
     toShATerm att0 (G_ext_sign lid sign _) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 sign of { (att2,i2) ->
           addATerm (ShAAppl "G_ext_sign" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_ext_sign" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_ext_sign:") i1'
                in case l of
                    Logic lid -> (G_ext_sign lid (fromShATerm_sign lid att') Set.empty)
	    u     -> fromShATermError "G_ext_sign" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_ext_sign\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_ext_sign\""

instance ATermConvertible G_sign_list where
     toShATerm att0 (G_sign_list lid signs) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 signs of { (att2,i2) ->
           addATerm (ShAAppl "G_sign_list" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_sign_list" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_sign_list:") i1'
                in case l of
                    Logic lid -> (G_sign_list lid (fromShATerm_sign_list lid att'))
	    u     -> fromShATermError "G_sign" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_sign_list\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_sign_list\""

instance ATermConvertible G_symbol where
     toShATerm att0 (G_symbol lid symbol) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 symbol of { (att2,i2) ->
           addATerm (ShAAppl "G_symbol" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_symbol" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_symbol:") i1'
                in case l of
                    Logic lid -> (G_symbol lid (fromShATerm_symbol lid att'))
	    u     -> fromShATermError "G_symbol" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_symbol\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_symbol\""

instance ATermConvertible G_symb_items_list where
     toShATerm att0 (G_symb_items_list lid symb_items) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 symb_items of { (att2,i2) ->
           addATerm (ShAAppl "G_symb_items_list" [i1,i2] []) att2 }}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_symb_items_list" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_symb_items_list:") i1'
                in case l of
                    Logic lid -> (G_symb_items_list lid (fromShATerm_symb_items_list lid att'))
	    u     -> fromShATermError "G_symb_items_list" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_symb_items_list\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_symb_items_list\""

instance ATermConvertible G_symb_map_items_list where
     toShATerm att0 (G_symb_map_items_list lid symb_map_items) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 symb_map_items of { (att2,i2) ->
           addATerm (ShAAppl "G_symb_map_items_list" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_symb_map_items_list" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_symb_map_items_list:") i1'
                in case l of
                    Logic lid -> (G_symb_map_items_list lid (fromShATerm_symb_map_items_list lid att'))
	    u     -> fromShATermError "G_symb_map_items_list" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_symb_map_items_list\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_symb_map_items_list\""

instance ATermConvertible G_diagram where
     toShATerm att0 (G_diagram lid diagram) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 diagram of { (att2,i2) ->
           addATerm (ShAAppl "G_diagram" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_diagram" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_diagram:") i1'
                in case l of
                    Logic lid -> (G_diagram lid (fromShATerm_diagram lid att'))
	    u     -> fromShATermError "G_diagram" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_diagram\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_diagram\""

instance ATermConvertible G_sublogics where
     toShATerm att0 (G_sublogics lid sublogics) =
	 case toShATerm att0 (language_name lid)  of { (att1,i1) ->
         case toShATerm att1 sublogics of { (att2,i2) ->
           addATerm (ShAAppl "G_sublogics" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_sublogics" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG
                          ("ATermConvertible G_sublogics:") i1'
                in case l of
                    Logic lid ->
                     (G_sublogics lid (fromShATerm_sublogics lid att'))
	    u     -> fromShATermError "G_sublogics" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_sublogic\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_sublogics\""

instance ATermConvertible G_morphism where
     toShATerm att0 (G_morphism lid morphism) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
         case toShATerm att1 morphism of { (att2,i2) ->
           addATerm (ShAAppl "G_morphism" [i1,i2] []) att2}}
     fromShATerm att =
         case aterm of
	    (ShAAppl "G_morphism" [i1,i2] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                    att' = getATermByIndex1 i2 att
                    l = lookupLogic_in_LG ("ATermConvertible G_morphism:") i1'
                in case l of
                    Logic lid -> (G_morphism lid (fromShATerm_morphism lid att'))
	    u     -> fromShATermError "G_morphism" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"G_morphism\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"G_morphism\""

---------------------------------------------------------------

instance ATermConvertible AnyComorphism where
     toShATerm att0 (Comorphism cid) =
	 case toShATerm att0 (language_name cid) of { (att1,i1) ->
           addATerm (ShAAppl "Comorphism" [i1] []) att1}
     fromShATerm att =
         case aterm of
	    (ShAAppl "Comorphism" [i1] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                in propagateErrors
                    $ lookupComorphism_in_LG i1'
	    u     -> fromShATermError "Comorphism" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"Comorphism\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"Comorphism\""

instance ATermConvertible GMorphism where
     toShATerm att0 (GMorphism cid sign1 morphism2) =
	 case toShATerm att0 (language_name cid) of { (att1,i1) ->
         case toShATerm att1 sign1 of { (att2,i2) ->
         case toShATerm att2 morphism2 of { (att3,i3) ->
           addATerm (ShAAppl "GMorphism" [i1,i2,i3] []) att3}}}
     fromShATerm att =
           case aterm of
	    (ShAAppl "GMorphism" [i1,i2,i3] _) ->
	 	let i1'  = fromShATerm (getATermByIndex1 i1 att)
                    c  =  propagateErrors $ lookupComorphism_in_LG i1'
                    att' = getATermByIndex1 i2 att
                    att'' = getATermByIndex1 i3 att
                in case c of
		     Comorphism cid ->
                       (GMorphism cid (fromShATerm_sign1 cid att')
                                      (fromShATerm_morphism2 cid att'') )
	    u     -> fromShATermError "GMorphism" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"GMorphism\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"GMorphism\""

instance ATermConvertible Grothendieck where
     toShATerm att0 Grothendieck =
	 addATerm (ShAAppl "Grothendieck" [] []) att0
     fromShATerm att = case aterm of
                      (ShAAppl "Grothendieck" [] _) -> Grothendieck
		      u     -> fromShATermError "Grothendiek" u
                     where aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"Grothendieck\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"Grothendieck\""


instance ATermConvertible AnyLogic where
     toShATerm att0 (Logic lid) =
	 case toShATerm att0 (language_name lid) of { (att1,i1) ->
           addATerm (ShAAppl "Logic" [i1] []) att1}
     fromShATerm att =
         case aterm of
	    (ShAAppl "Logic" [i1] _) ->
		let i1' = fromShATerm (getATermByIndex1 i1 att)
                in lookupLogic_in_LG ("ATermConvertible AnyLogic:") i1'
	    u     -> fromShATermError "AnyLogic" u
         where
         aterm = getATerm att
     fromATerm _ = error "function \"fromATerm\" not derived (implemented) for data type \"AnyLogic\""
     toATerm _ = error "function \"toATerm\" not derived (implemented) for data type \"AnyLogic\""