Proof.hs revision da955132262baab309a50fdffe228c9efe68251d
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maedermodule Proof where
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maederimport Structured
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport StaticAnalysis
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederprove :: LogicGraph -> Bool -> String -> [String] -> IO()
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederprove logicGraph flat spec raw_goals = do
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder if flat then proveFlat th (getGoals th)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder else proveStruct th env (getGoals th)
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder as = hetParse logicGraph spec
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder Just (env,th) = staticAnalysis as
08faa81d4dd8409cd923b334064f64f802ecc33dChristian Maeder getGoals (G_theory id (sig,ax)) =
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder map (G_sentence id . parse_sentence id sig) raw_goals
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder proveFlat th goals = do
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder res <- sequence (map (proveFlat1 th) goals)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder putStrLn (show res)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder proveFlat1 (G_theory id (sig,ax)) (G_sentence _ goal) =
7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder prover id (sig,ax) (coerce1 goal)
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder proveStruct (G_theory id (sig,ax)) env goals = do
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder res <- sequence (map (prove1 env) goals)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder putStrLn (show res)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder prove1 :: Env -> G_sentence -> IO Proof_status
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder prove1 env g@(G_sentence id goal) = case env of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Basic_env (G_theory id' (sig,ax)) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder prover id' (sig,ax) (coerce1 goal)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Intra_Translation_env th env' (G_morphism id' mor) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let goal' = coerce1 goal in
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case inv_map_sentence id' mor goal' of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just goal'' -> prove1 env' (G_sentence id' goal'')
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> proveFlat1 th g
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder Inter_Translation_env th env' (G_LTR tr) ->
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder prove_aux (G_theory _ (sig,_)) =
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder case inv_tr_sen tr (coerce1 sig) (coerce1 goal) of
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder Just goal'' -> prove1 env' (G_sentence (source tr) goal'')
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder Nothing -> proveFlat1 th g
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder Extension_env _ env1 env2 -> do
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder res <- prove1 env1 g
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder Proved -> return Proved
94ceeb2edbd25b4697ddd9f63c94377924352cf4Christian Maeder _ -> prove1 env2 g