1178N/ADescription : <optional short description entry>
1178N/ACopyright : (c) <Authors or Affiliations>
1178N/AStability : unstable | experimental | provisional | stable | frozen
1178N/APortability : portable | non-portable (<reason>)
2362N/Aprove :: LogicGraph -> Bool -> String -> [String] -> IO()
2362N/Aprove logicGraph flat spec raw_goals = do
1178N/A if flat then proveFlat th (getGoals th)
2509N/A else proveStruct th env (getGoals th)
1178N/A as = hetParse logicGraph spec
1178N/A Just (env,th) = staticAnalysis as
1178N/A getGoals (G_theory id (sig,ax)) =
1178N/A map (G_sentence id . parse_sentence id sig) raw_goals
1178N/A res <- sequence (map (proveFlat1 th) goals)
1178N/A proveFlat1 (G_theory id (sig,ax)) (G_sentence _ goal) =
1178N/A prover id (sig,ax) (coerce1 goal)
1178N/A proveStruct (G_theory id (sig,ax)) env goals = do
1178N/A res <- sequence (map (prove1 env) goals)
1178N/A prove1 :: Env -> G_sentence -> IO Proof_status
1178N/A prove1 env g@(G_sentence id goal) = case env of
1178N/A Basic_env (G_theory id' (sig,ax)) ->
1178N/A prover id' (sig,ax) (coerce1 goal)
1178N/A Intra_Translation_env th env' (G_morphism id' mor) ->
1178N/A let goal' = coerce1 goal in
1178N/A case inv_map_sentence id' mor goal' of
1178N/A Just goal'' -> prove1 env' (G_sentence id' goal'')
1178N/A Inter_Translation_env th env' (G_LTR tr) ->
1178N/A prove_aux (G_theory _ (sig,_)) =
1178N/A case inv_tr_sen tr (coerce1 sig) (coerce1 goal) of
1178N/A Just goal'' -> prove1 env' (G_sentence (source tr) goal'')
1178N/A Extension_env _ env1 env2 -> do