module StaticAnalysis where

import Logic

import Grothendieck

import Structured

import Data.Dynamic

staticAnalysis :: SPEC -> Maybe (Env, G_theory)

staticAnalysis sp = staticAna1 initial_theory sp

where

initial_theory = get_initial sp

get_initial sp = case sp of

Basic_spec (G_basic_spec logic _) ->

G_theory logic (empty_theory logic)

Intra_Translation sp _ -> get_initial sp

Inter_Translation sp _ -> get_initial sp

Extension sp _ -> get_initial sp

staticAna1 :: G_theory -> SPEC -> Maybe (Env, G_theory)

staticAna1 th@(G_theory id (sig, ax)) sp =

case sp of

Basic_spec (G_basic_spec _ b) ->

do b' <- coerce b

(sig1, ax1) <- basic_analysis id sig b'

let th' = G_theory id (sig1, ax1 ++ ax)

return (Basic_env th', th')

Intra_Translation sp (G_symbol_mapping_list _ symap) ->

do (env, G_theory id1 (sig1, ax1)) <- staticAna1 th sp

symap' <- coerce symap

mor <- stat_symbol_mapping id1 symap' sig1

tr_ax <- mapM (map_sentence id1 mor) ax1

let th' = G_theory id1 (cod id1 mor, tr_ax)

let env' = Intra_Translation_env th' env (G_morphism id1 mor)

return (env', th')

Inter_Translation sp (G_LTR tr) ->

do (env, G_theory id1 (sig1, ax1)) <- staticAna1 th sp

let id_tar = target tr

sig2 <- coerce sig1

ax2 <- coerce ax1

let tr_sig = tr_sign tr sig2

tr_ax <- mapM (tr_sen tr sig2) ax2

let th' = G_theory id_tar (tr_sig, tr_ax)

let env' = Inter_Translation_env th' env (G_LTR tr)

return (env', th')

Extension sp1 sp2 ->

do (env1, th1) <- staticAna1 th sp1

(env2, th2) <- staticAna1 th1 sp2

return (Extension_env th2 env1 env2, th2)