{-
* Module for converting vts90 objects into strings and vica-versa
-}
module Core_database where
import Dcore
import Sub_Core1
import Sub_Core2
import Sub_Core3
import Sub_Core4
import Vtslib
import Core_datatype
data Constant_tag
= BOOL_TAG | TRUE_TAG | FALSE_TAG | UNIV_TAG deriving (Eq)
data Declaration_tag
= SYMBOL_DEC_TAG | AXIOM_DEC_TAG | DEF_TAG | DATA_TAG |
DECPAIR_TAG deriving (Eq)
data Term_tag
= SYM_TAG | APP_TAG | PAIR_TAG | BINDER_TAG |
CONSTANT_TAG | UNARY_TAG | BINARY_TAG | COND_TAG |
CONST_TAG | RECURSE_TAG deriving (Eq)
data Signature_tag
= EMPTY_TAG | EXTEND_TAG | COMBINE_TAG | SHARE_TAG deriving (Eq)
trm_tag_list
= [SYM_TAG, APP_TAG, PAIR_TAG, BINDER_TAG,
CONSTANT_TAG, UNARY_TAG, BINARY_TAG, COND_TAG,
CONST_TAG, RECURSE_TAG]
dec_tag_list
= [SYMBOL_DEC_TAG, AXIOM_DEC_TAG, DEF_TAG, DATA_TAG, DECPAIR_TAG]
sgn_tag_list
= [EMPTY_TAG,EXTEND_TAG,COMBINE_TAG,SHARE_TAG]
con_tag_list
= [BOOL_TAG, TRUE_TAG, FALSE_TAG, UNIV_TAG]
unary_tag_list = [Not]
binary_tag_list
= [Eq',And,Or,Issubtype]
binder_tag_list
= [Forall,Exists,Imp,Lambda,Pi,Sigma,Subtype,Choose]
{-
(* Functions for encoding tags *)
(* Each function is of type *)
(* ???_tag -> string *)
-}
encode_trm_tag tag = toEnum (encode tag trm_tag_list)
encode_dec_tag tag = toEnum (encode tag dec_tag_list)
encode_sgn_tag tag = toEnum (encode tag sgn_tag_list)
encode_unary_tag tag = toEnum (encode tag unary_tag_list)
encode_binary_tag tag = toEnum (encode tag binary_tag_list)
encode_binder_tag tag = toEnum (encode tag binder_tag_list)
encode_con_tag tag = toEnum (encode tag con_tag_list)
{-
(* Functions for decoding strings *)
(* Each function is of type *)
(* string -> ???_tag *)
-}
decode_trm_tag i = trm_tag_list !! i
decode_dec_tag i = dec_tag_list !! i
decode_sgn_tag i = sgn_tag_list !! i
decode_unary_tag i = unary_tag_list !! i
decode_binary_tag i = binary_tag_list !! i
decode_binder_tag i = binder_tag_list !! i
decode_constant_tag i = con_tag_list !! i
{- turn a term into a string -}
trm_to_str tm
= s1 ++ s2 ++ s3
where
s1 = trm_to_str' tm -- the term
s2 = trmL_to_str (other_typ tm) -- its extra types
s3 = attL_to_str (get_trm_att tm []) -- its attributes
{- turn a declaration into a string -}
dec_to_str dc
= s1 ++ s2
where
s1 = dec_to_str' dc -- the declaration
s2 = attL_to_str (get_dec_att dc) -- its attributes
{- turn a signature into a string -}
sgn_to_str sg
= s1 ++ s2
where
s1 = sgn_to_str' sg -- the signature
s2 = attL_to_str (get_sgn_att sg) -- its attributes
{- turn a term into a string ignoring its extra types and its attributes -}
trm_to_str' (Sym i j _ _)
= encode_trm_tag SYM_TAG : int_to_str i ++ int_to_str j
trm_to_str' (App tm1 tm2 _ _)
= encode_trm_tag APP_TAG : trm_to_str tm1 ++ trm_to_str tm2
trm_to_str' (Pair tm1 tm2 tm3 _ _)
= encode_trm_tag PAIR_TAG : trm_to_str tm1 ++ trm_to_str tm2
trm_to_str' (Binder b dc tm _ _)
= encode_trm_tag BINDER_TAG : [ encode_binder_tag b ] ++
dec_to_str dc ++ trm_to_str tm
trm_to_str' (Constant c _ _)
= encode_trm_tag CONSTANT_TAG : constant_to_str c
trm_to_str' (Unary c tm _ _)
= encode_trm_tag UNARY_TAG : [encode_unary_tag c] ++ trm_to_str tm
trm_to_str' (Binary' c tm1 tm2 _ _)
= encode_trm_tag BINARY_TAG : [encode_binary_tag c] ++
trm_to_str tm1 ++ trm_to_str tm2
trm_to_str' (Cond dc tm1 tm2 _ _)
= encode_trm_tag COND_TAG : dec_to_str dc ++
trm_to_str tm1 ++ trm_to_str tm2
trm_to_str' (Const i j k _ _)
= encode_trm_tag CONST_TAG : int_to_str i ++
int_to_str j ++ int_to_str k
trm_to_str' (Recurse tmL tm _ _)
= encode_trm_tag RECURSE_TAG : trmL_to_str tmL ++ trm_to_str tm
{- turn a declaration into a string ignoring its attributes -}
dec_to_str' (Symbol_dec tm _)
= encode_dec_tag SYMBOL_DEC_TAG : trm_to_str tm
dec_to_str' (Axiom_dec tm _)
= encode_dec_tag AXIOM_DEC_TAG : trm_to_str tm
dec_to_str' (Def tm1 tm2 _)
= encode_dec_tag DEF_TAG : trm_to_str tm1 ++ trm_to_str tm2
dec_to_str' (Data dcL tmLL _)
= encode_dec_tag DATA_TAG : decL_to_str dcL ++ trmLL_to_str tmLL
dec_to_str' (Decpair dc1 dc2 _)
= encode_dec_tag DECPAIR_TAG : dec_to_str dc1 ++ dec_to_str dc2
{- turn a signature into a string ignoring its attributes -}
sgn_to_str' (Empty _)
= [ encode_sgn_tag EMPTY_TAG ]
sgn_to_str' (Extend dc sg _)
= encode_sgn_tag EXTEND_TAG : dec_to_str dc ++ sgn_to_str sg
sgn_to_str' (Combine sg1 sg2 i _ _)
= encode_sgn_tag COMBINE_TAG : sgn_to_str sg1 ++
sgn_to_str sg2 ++ int_to_str i
sgn_to_str' (Share sg i j k _ _)
= encode_sgn_tag SHARE_TAG : sgn_to_str sg ++
int_to_str i ++ int_to_str j ++ int_to_str k
trmL_to_str tmL
= int_to_str (length tmL) ++ concat (map trm_to_str tmL)
trmLL_to_str tmLL
= int_to_str (length tmLL) ++ concat (map trmL_to_str tmLL)
trmLLL_to_str tmLLL
= int_to_str (length tmLLL) ++ concat (map trmLL_to_str tmLLL)
decL_to_str dcL
= int_to_str (length dcL) ++ concat (map dec_to_str dcL)
attL_to_str attL
= int_to_str (length attL) ++ concat (map att_to_str attL)
{- TEMP FUNCTION -}
att_to_str _ = "*** att_to_str NOT IMPLEMENTED -- core_database ***"
constant_to_str T = [ encode_con_tag TRUE_TAG ]
constant_to_str F = [ encode_con_tag FALSE_TAG ]
constant_to_str Bool' = [ encode_con_tag BOOL_TAG ]
constant_to_str (Univ i) = encode_con_tag UNIV_TAG : int_to_str i
str_to_trm s
= (foldr add_type (set_trm_att tm [] attL) tmL , s3)
where
(tm,s1) = s_to_trm' s
(tmL,s2) = s_to_trmL s1
(attL,s3) = str_to_attL s2
str_to_dec s
= (set_dec_att dc attL,s2)
where
(dc,s1) = s_to_dec' s
(attL,s2) = str_to_attL s1
str_to_sgn s
= (set_sgn_att sg attL,s2)
where
(sg,s1) = s_to_sgn' s
(attL,s2) = str_to_attL s1
s_to_trm' (ch:s1)
= case decode_trm_tag ch of
SYM_TAG
-> (Sym i j [] [] ,s3)
where
(i,s2) = str_to_int s1
(j,s3) = str_to_int s2
APP_TAG
-> (App tm1 tm2 [] [] ,s3)
where
(tm1,s2) = str_to_trm s1
(tm2,s3) = str_to_trm s2
PAIR_TAG
-> (Pair tm1 tm2 tm3 [] [] ,s4)
where
(tm1,s2) = str_to_trm s1
(tm2,s3) = str_to_trm s2
(tm3,s4) = str_to_trm s3
BINDER_TAG
-> (Binder b dc tm [] [] ,s4)
where
(b,s2) = str_to_binder s1
(dc,s3) = str_to_dec s2
(tm,s4) = str_to_trm s3
CONSTANT_TAG
-> (Constant c [] [] ,s2)
where
(c,s2) = str_to_constant s1
UNARY_TAG
-> (Unary c tm [] [] ,s3)
where
(c,s2) = str_to_unary s1
(tm,s3) = str_to_trm s2
BINARY_TAG
-> (Binary' c tm1 tm2 [] [] ,s4)
where
(c,s2) = str_to_binary s1
(tm1,s3) = str_to_trm s2
(tm2,s4) = str_to_trm s3
COND_TAG
-> (Cond dc tm1 tm2 [] [] ,s4)
where
(dc,s2) = str_to_dec s1
(tm1,s3) = str_to_trm s2
(tm2,s4) = str_to_trm s3
CONST_TAG
-> (Const i j k [] [] ,s4)
where
(i,s2) = str_to_int s1
(j,s3) = str_to_int s2
(k,s4) = str_to_int s3
RECURSE_TAG
-> (Recurse tmL tm [] [] ,s3)
where
(tmL,s2) = s_to_trmL s1
(tm,s3) = str_to_trm s2
s_to_dec' (ch:s1)
= case decode_dec_tag ch of
SYMBOL_DEC_TAG
-> (Symbol_dec tm [] ,s2)
where
(tm,s2) = str_to_trm s1
AXIOM_DEC_TAG
-> (Axiom_dec tm [] ,s2)
where
(tm,s2) = str_to_trm s1
DEF_TAG
-> (Def tm1 tm2 [] ,s3)
where
(tm1,s2) = str_to_trm s1
(tm2,s3) = str_to_trm s2
DATA_TAG
-> (Data dcL tmLL [] ,s3)
where
(dcL,s2) = s_to_decL s1
(tmLL,s3) = s_to_trmLL s2
DECPAIR_TAG
-> (Decpair dc1 dc2 [] ,s3)
where
(dc1,s2) = str_to_dec s1
(dc2,s3) = str_to_dec s2
s_to_sgn' (ch:s1)
= case decode_sgn_tag ch of
EMPTY_TAG
-> (Empty [], s1)
EXTEND_TAG
-> (Extend dc sg [] ,s3)
where
(dc,s2) = str_to_dec s1
(sg,s3) = str_to_sgn s2
COMBINE_TAG
-> (Combine sg1 sg2 i (sm2 ++ map (\ j -> j + i) sm1) [] ,s4)
where
(sg1,s2) = str_to_sgn s1
(sg2,s3) = str_to_sgn s2
(i,s4) = str_to_int s3
sm1 = get_share_map sg1
sm2 = get_share_map sg2
SHARE_TAG
-> (Share sg i j k (addequivL i j k sm) [] ,s5)
where
(sg,s2) = str_to_sgn s1
(i,s3) = str_to_int s2
(j,s4) = str_to_int s3
(k,s5) = str_to_int s4
sm = get_share_map sg
s_to_trmL s = str_to_list str_to_trm s
s_to_trmLL s = str_to_list s_to_trmL s
s_to_trmLLL s = str_to_list s_to_trmLL s
s_to_decL s = str_to_list str_to_dec s
str_to_attL s = str_to_list str_to_att s
str_to_binder (ch:s1)
= (decode_binder_tag ch,s1)
str_to_unary (ch:s1)
= (decode_unary_tag ch,s1)
str_to_binary :: [Int] -> (Binary_conn, [Int])
str_to_binary (ch:s1)
= (decode_binary_tag ch,s1)
str_to_constant (ch:s1)
= case decode_constant_tag ch of
BOOL_TAG -> (Bool',s1)
TRUE_TAG -> (T,s1)
FALSE_TAG -> (F,s1)
UNIV_TAG -> (Univ i,s2)
where
(i,s2) = str_to_int s1
{-
temp function
-}
str_to_att ( a : x) = ( ( Name_Style , Symbol_Name ( Name [ toEnum a ]) ) , x )
|