{- |

Module : $EmptyHeader$

Description : <optional short description entry>

Copyright : (c) <Authors or Affiliations>

License : GPLv2 or higher, see LICENSE.txt

Maintainer : <email>

Stability : unstable | experimental | provisional | stable | frozen

Portability : portable | non-portable (<reason>)

<optional description>

-}

module Proof where

import Structured

import Parser

import StaticAnalysis

prove :: LogicGraph -> Bool -> String -> [String] -> IO ()

prove logicGraph flat spec raw_goals =

if flat then proveFlat th (getGoals th)

else proveStruct th env (getGoals th)

where

as = hetParse logicGraph spec

Just (env, th) = staticAnalysis as

getGoals (G_theory id (sig, ax)) =

map (G_sentence id . parse_sentence id sig) raw_goals

proveFlat th goals = do

res <- mapM (proveFlat1 th) goals

print res

proveFlat1 (G_theory id (sig, ax)) (G_sentence _ goal) =

prover id (sig, ax) (coerce1 goal)

proveStruct (G_theory id (sig, ax)) env goals = do

res <- mapM (prove1 env) goals

print res

where

prove1 :: Env -> G_sentence -> IO Proof_status

prove1 env g@(G_sentence id goal) = case env of

Basic_env (G_theory id' (sig, ax)) ->

prover id' (sig, ax) (coerce1 goal)

Intra_Translation_env th env' (G_morphism id' mor) ->

let goal' = coerce1 goal in

case inv_map_sentence id' mor goal' of

Just goal'' -> prove1 env' (G_sentence id' goal'')

Nothing -> proveFlat1 th g

Inter_Translation_env th env' (G_LTR tr) ->

prove_aux th

where

prove_aux (G_theory _ (sig, _)) =

case inv_tr_sen tr (coerce1 sig) (coerce1 goal) of

Just goal'' -> prove1 env' (G_sentence (source tr) goal'')

Nothing -> proveFlat1 th g

Extension_env _ env1 env2 -> do

res <- prove1 env1 g

case res of

Proved -> return Proved

_ -> prove1 env2 g