b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuModule : $EmptyHeader$
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuDescription : <optional short description entry>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuCopyright : (c) <Authors or Affiliations>
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuMaintainer : <email>
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuStability : unstable | experimental | provisional | stable | frozen
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu ProdescuPortability : portable | non-portable (<reason>)
b87efd3db0d2dc41615ea28669faf80fc1b48d56Corneliu-Claudiu Prodescu<optional description>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Proof where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Structured
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport StaticAnalysis
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederprove :: LogicGraph -> Bool -> String -> [String] -> IO ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederprove logicGraph flat spec raw_goals =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski if flat then proveFlat th (getGoals th)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski else proveStruct th env (getGoals th)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski as = hetParse logicGraph spec
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just (env, th) = staticAnalysis as
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder getGoals (G_theory id (sig, ax)) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski map (G_sentence id . parse_sentence id sig) raw_goals
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski proveFlat th goals = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder res <- mapM (proveFlat1 th) goals
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder proveFlat1 (G_theory id (sig, ax)) (G_sentence _ goal) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prover id (sig, ax) (coerce1 goal)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder proveStruct (G_theory id (sig, ax)) env goals = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder res <- mapM (prove1 env) goals
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prove1 :: Env -> G_sentence -> IO Proof_status
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski prove1 env g@(G_sentence id goal) = case env of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Basic_env (G_theory id' (sig, ax)) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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