(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Why
open Ident
open Term
open Decl
open Theory
open Pgm_itree

module E = Pgm_effect

let errorm = Pgm_typing.errorm

(* translation to intermediate trees and effect inference *)

let rec expr e =
  let ty = e.Pgm_ttree.expr_type in
  let loc = e.Pgm_ttree.expr_loc in
  let d, ef = expr_desc loc ty e.Pgm_ttree.expr_desc in
  { expr_desc = d; expr_type = ty; expr_effect = ef; expr_loc = loc }

and expr_desc _loc _ty = function
  | Pgm_ttree.Elogic _t ->
      assert false (*TODO*)
  | Pgm_ttree.Eapply _ as _e ->
      assert false (*TODO*)
  | Pgm_ttree.Efun (_bl, (_p, e, _q)) ->
      let _e = expr e in
      assert false (*TODO*)
  | _ -> 
      assert false (*TODO*)

and recfun _ =
  assert false (*TODO*)

(* weakest preconditions *)

let wp _l _e = f_true (* TODO *)

let wp_recfun _l _def = f_true (* TODO *)

let add_wp_decl uc l f =
  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
  let d = create_prop_decl Pgoal pr f in
  add_decl uc d

let decl uc = function
  | Pgm_ttree.Dlet (l, e) ->
      let e = expr e in
      let f = wp l e in
      add_wp_decl uc l f
  | Pgm_ttree.Dletrec dl ->
      let add_one uc (l, def) = 
	let def = recfun def in
	let f = wp_recfun l def in 
	add_wp_decl uc l f 
      in
      List.fold_left add_one uc dl
  | Pgm_ttree.Dparam _ ->
      uc

let file uc dl =
  let uc = List.fold_left decl uc dl in
  Theory.close_theory uc