Proof.hs revision da955132262baab309a50fdffe228c9efe68251d
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Proof where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Structured
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport StaticAnalysis
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiprove :: LogicGraph -> Bool -> String -> [String] -> IO()
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiprove logicGraph flat spec raw_goals = do
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski if flat then proveFlat th (getGoals th)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski else proveStruct th env (getGoals th)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski as = hetParse logicGraph spec
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just (env,th) = staticAnalysis as
da955132262baab309a50fdffe228c9efe68251dCui Jian getGoals (G_theory id (sig,ax)) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski map (G_sentence id . parse_sentence id sig) raw_goals
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski proveFlat th goals = do
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski res <- sequence (map (proveFlat1 th) goals)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski putStrLn (show res)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski proveFlat1 (G_theory id (sig,ax)) (G_sentence _ goal) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prover id (sig,ax) (coerce1 goal)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski proveStruct (G_theory id (sig,ax)) env goals = do
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski res <- sequence (map (prove1 env) goals)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski putStrLn (show res)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prove1 :: Env -> G_sentence -> IO Proof_status
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prove1 env g@(G_sentence id goal) = case env of
da955132262baab309a50fdffe228c9efe68251dCui Jian Basic_env (G_theory id' (sig,ax)) ->
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prover id' (sig,ax) (coerce1 goal)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Intra_Translation_env th env' (G_morphism id' mor) ->
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski let goal' = coerce1 goal in
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski case inv_map_sentence id' mor goal' of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just goal'' -> prove1 env' (G_sentence id' goal'')
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Nothing -> proveFlat1 th g
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Inter_Translation_env th env' (G_LTR tr) ->
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prove_aux (G_theory _ (sig,_)) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski case inv_tr_sen tr (coerce1 sig) (coerce1 goal) of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just goal'' -> prove1 env' (G_sentence (source tr) goal'')
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Nothing -> proveFlat1 th g
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Extension_env _ env1 env2 -> do
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski res <- prove1 env1 g
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Proved -> return Proved
da955132262baab309a50fdffe228c9efe68251dCui Jian _ -> prove1 env2 g