(* Verification Conditions Formulas *)

type ident = string

(* currently not enforced *)
type typeExpr = 
  | TypeVar of ident
  | TypeObjRef of string
  | TypeArray of typeExpr
  | TypeSet of typeExpr
  | TypeList of typeExpr
  | TypeFun of (typeExpr list * typeExpr)
  | TypeInt
  | TypeBool
  | TypeVoid
  | TypeUniverse (* must go away eventually! *)

type constValue =
    Eq | Sub | Elem 
  | Or | And | MetaAnd | Not | Impl | MetaImpl | Iff | Disjoint
  | Lt | Gt | LtEq | GtEq (* integer comparisons *)
  | Cardeq | Cardleq | Cardgeq (* set card constrs *)
  | ArrayRead | ArrayWrite | NewArray | ArraySize (* arrays *) 
  | FieldWrite | FieldRead
  | Cap | Cup | Diff (* sets *)
  | Plus | Minus | Mult | Div | Mod 
  | IntConst of int | BoolConst of bool | NullConst 
  | EmptysetConst | FiniteSetConst
  | Tuple

let string_of_const (c:constValue) = match c with
| Eq -> "=" | Sub -> "<="  | Elem -> ":"
| Or -> "|" | And -> "&" | MetaAnd -> ";" | Not -> "~" 
| Impl -> "-->" | MetaImpl -> "==>" | Iff -> "="
| Disjoint -> "disjoint"
| Lt -> "<" | Gt -> ">" | LtEq -> "<=" | GtEq -> ">="
| Cardeq -> "Cardeq" | Cardleq -> "Cardleq" | Cardgeq -> "Cardgeq"
| ArrayRead -> "arrayRead" | ArrayWrite -> "arrayWrite" 
| NewArray -> "newArray" | ArraySize  -> "arraySize"
| Cap -> "Int" | Cup -> "Un" | Diff -> "-" 
| Plus -> "+" | Minus -> "-" | Mult -> "*" | Div -> "div" | Mod -> "mod"
| IntConst k -> string_of_int k
| BoolConst true -> "true" | BoolConst false -> "false"
| NullConst -> "null" | EmptysetConst -> "{}"
| FieldWrite -> "fieldWrite" | FieldRead -> "fieldRead"
| FiniteSetConst -> "finiteSet"
| Tuple -> "tuple"

type typedVarIdent = ident * typeExpr

type binderKind =
  | Forall
  | Exists
  | Lambda
  | Comprehension

type form =
    App of form * form list (* fst must be function-typed *)
  | Var of ident
  | Binder of binderKind * (typedVarIdent list) * form
  | Const of constValue
  | TypedForm of form * typeExpr

(* variable-binding environments e.g. used in vc gen *)

(* let x = v in exp *)
type env = (typedVarIdent * form option) list

(* v....... preamble ...........v   v........ haveEnv(x) ...... *)
(* exists i1, ..., in. pre(x0,y0) & (x = f(x0, y0, i1, ..., in)) & 
                                    (y = g(x0, y0, i1, ..., in)) &
            constraint(x0, y, i1, ..., in) *)
         (* ^~~~~~~~~~ haveBody ~~~~~~~~~^ *)

type haveForm = {preamble:form; haveEnv: env; haveBody: form}

(* also have a global list of const binders *)
(* use this for type checking *)

type constBinding = (constValue * typeExpr) list
let globalEnv : constBinding = 
  [(And, TypeFun ([TypeBool; TypeBool], TypeBool));
   (Or, TypeFun ([TypeBool; TypeBool], TypeBool));
   (Impl, TypeFun ([TypeBool; TypeBool], TypeBool));
   (Iff, TypeFun ([TypeBool; TypeBool], TypeBool));
   (Not, TypeFun ([TypeBool], TypeBool));
   (Eq, TypeFun ([TypeUniverse; TypeUniverse], TypeBool));
   (Sub, TypeFun ([TypeUniverse; TypeUniverse], TypeBool));
(* integer stuff *)
   (Lt, TypeFun ([TypeInt; TypeInt], TypeBool));
   (LtEq, TypeFun ([TypeInt; TypeInt], TypeBool));
   (Gt, TypeFun ([TypeInt; TypeInt], TypeBool));
   (GtEq, TypeFun ([TypeInt; TypeInt], TypeBool));
(* arrays *)
   (ArrayRead, TypeFun ([TypeArray TypeUniverse; TypeInt], TypeUniverse));
   (ArrayWrite, TypeFun ([TypeArray TypeUniverse; 
                          TypeInt; 
                          TypeArray TypeUniverse], TypeUniverse));
   (NewArray, TypeFun ([TypeInt; TypeUniverse], TypeArray TypeUniverse));
(* need set types, like array types I guess, but should also be recursive *)
(* should also be capable of taking many arguments *)
   (Cup, TypeFun ([TypeList TypeUniverse], 
                  TypeSet TypeUniverse)); 
   (Cap, TypeFun ([TypeList TypeUniverse], 
                  TypeSet TypeUniverse));
   (Diff, TypeFun ([TypeSet TypeUniverse; TypeSet TypeUniverse], 
                  TypeSet TypeUniverse))]
(* also cardeq, cardleq, cardgeq, disjoint *)

(* get type of variable from variable-binding environement *)
let get_type x env =
  snd (fst (List.find (fun ((x', _), _) -> x = x') env))
  

let mk_true = Const (BoolConst true)
let mk_false = Const (BoolConst false)
let mk_int k = Const (IntConst k)
let mk_not f = App (Const Not, [f])
let mk_and cs = match cs with
| [] -> mk_true
| [f] -> f
| _ -> App (Const And, cs)
let mk_metaand cs = match cs with
| [] -> mk_true
| [f] -> f
| _ -> App (Const MetaAnd, cs)
let mk_or ds = match ds with
| [] -> mk_false
| [f] -> f
| _ -> App (Const Or, ds)
let mk_eq (lhs, rhs) = App (Const Eq, [lhs; rhs])
let mk_neq (lhs, rhs) = mk_not (mk_eq(lhs,rhs))
let mk_sub (lhs, rhs) = App (Const Sub, [lhs; rhs])
let mk_lt (lhs, rhs) = App (Const Lt, [lhs; rhs])
let mk_gt (lhs, rhs) = App (Const Gt, [lhs; rhs])
let mk_lteq (lhs, rhs) = App (Const LtEq, [lhs; rhs])
let mk_gteq (lhs, rhs) = App (Const GtEq, [lhs; rhs])
let mk_impl (lhs, rhs) = App (Const Impl, [lhs; rhs])
let mk_metaimpl (lhs, rhs) = App (Const MetaImpl, [lhs; rhs])
let mk_iff (lhs, rhs) = App (Const Iff, [lhs; rhs])
let mk_forall(v,t,f) = Binder(Forall,[(v,t)],f)
let mk_foralls(vts,f) = Binder(Forall,vts,f)
let mk_ex(v,t,f) = Binder(Exists,[(v,t)],f)
let mk_exists(vts,f) = Binder(Exists,vts,f)
let mk_var v = Var (Util.replace_dot_with_uscore v)

let mk_functionApply(func,arr,ind) = App(Const func,[arr;ind])
let mk_functionUpdate(func,base,index,vl) = App(Const func,[base;index;vl])
let mk_newArray(size,fill) = App(Const NewArray,[size;fill])
let mk_arraySize(arr) = App(Const ArraySize, [arr])

let mk_null = Const NullConst

let mk_plus (lhs, rhs) = App (Const Plus, [lhs; rhs])
let mk_minus (lhs, rhs) = App (Const Minus, [lhs; rhs])
let mk_mult (lhs, rhs) = App (Const Mult, [lhs; rhs])
let mk_div (lhs, rhs) = App (Const Div, [lhs; rhs])
let mk_mod (lhs, rhs) = App (Const Mod, [lhs; rhs])

let mk_elem(lhs,rhs) = App(Const Elem, [lhs;rhs])
let mk_notelem(lhs,rhs) = mk_not(mk_elem(lhs,rhs))

let mk_typedform(f,t) = TypedForm(f,t)
let mk_typevar id = TypeVar id

let mk_finite_set fs = App(Const FiniteSetConst, fs)
let mk_tuple fs = App(Const Tuple, fs)

(* ********************************************* *)
(*     free (non-type) variables of a formula    *)
(* ********************************************* *)

let fv (f:form) = 
  let add v bv acc = 
    if (List.mem v bv) || (List.mem v acc) 
    then acc
    else v::acc in
  let rec fv1 f bv acc = match f with
  | App(f1,fs) -> fv1 f1 bv (fv_list fs bv acc)
  | Binder(_,tvs,f1) -> fv1 f1 (List.rev_append (List.map fst tvs) bv) acc
  | Var v -> add v bv acc
  | Const _ -> acc
  | TypedForm(f1,t) -> fv1 f1 bv acc
  and fv_list fs bv acc = match fs with
  | [] -> acc
  | f::fs1 -> fv_list fs1 bv (fv1 f bv acc)
in fv1 f [] []


(* **************************************** *)
(*       substitution (ignores types)       *)
(* **************************************** *)

type substMap = (ident * form) list

(* naive substitution ignores var capture *)
let rec nsubst (m:substMap) (f:form) : form = 
  if m=[] then f else match f with
  | App(f1,fs) -> App(nsubst m f1, List.map (nsubst m) fs)
  | Binder(k,tvs,f1) -> 
      let not_bound (id,f) = not (List.mem_assoc id tvs) in
      let m1 = List.filter not_bound m in
      Binder(k,tvs,nsubst m1 f1)
  | Var v -> (try List.assoc v m with Not_found -> f)
  | Const _ -> f
  | TypedForm(f1,t) -> TypedForm(nsubst m f1,t)

(* free vars of a substitution *)
let fv_of_subst (m:substMap) =
  List.concat (List.map fv (List.map snd m))

let fresh_var_count = (ref 0 : int ref)
let fresh_var s = begin
  fresh_var_count := !fresh_var_count + 1; 
  s ^ (Printf.sprintf "__%d" !fresh_var_count)
end

let rec capture_avoid vars tvs subst_acc tvs_acc = match tvs with
| [] -> (List.rev tvs_acc, subst_acc)
| (v,t)::tvs1 when (List.mem v vars) ->
  let fresh_v = fresh_var v in
  capture_avoid vars tvs1 
                ((v,Var fresh_v)::subst_acc)
                ((fresh_v,t)::tvs_acc)
| (v,t)::tvs1 ->
  capture_avoid vars tvs1 
                subst_acc
                ((v,t)::tvs_acc)

let rec subst (m:substMap) (f:form) : form = 
  if m=[] then f else match f with
  | App(f1,fs) -> App(subst m f1, List.map (subst m) fs)
  | Binder(k,tvs,f1) -> 
      let not_bound (id,f) = not (List.mem_assoc id tvs) in
      let m1 = List.filter not_bound m in
      if m1=[] then f
      else 
        let (tvs1, renaming) = 
            capture_avoid (fv_of_subst m1) tvs [] [] in
        let f2 = if renaming=[] then f1 else nsubst renaming f1 in
        if tvs1=[] then f2 else
        Binder(k,tvs1,subst m1 f2)
  | Var v -> (try List.assoc v m with Not_found -> f)
  | Const _ -> f
  | TypedForm(f1,t) -> TypedForm(subst m f1,t)

(* **************************************** *)
(*       priming                            *)
(* **************************************** *)

let primed id = id^"'"

let prime_all (f:form) : form =
  let ids = fv f in
  let mk_primed id = (id,Var (primed id)) in
  subst (List.map mk_primed ids) f

(* **************************************** *)
(*       unpriming                          *)
(* **************************************** *)

let unprimed id =
  let len = String.length id in
  if (len > 0) && id.[len - 1] = '\'' then String.sub id 0 (len - 1)
  else id

let unprime_all (f:form) : form =
  let ids = fv f in
  let mk_unprimed id = (id,Var (unprimed id)) in
  subst (List.map mk_unprimed ids) f

(* **************************************** *)
(*             smart constructors           *)
(* **************************************** *)

let smk_not f =
  match f with
  | Const (BoolConst t) -> Const (BoolConst (not t))
  | App (Const Not, [f']) -> f'
  | _ -> mk_not f

let smk_forall (x,t,f) = 
  if List.mem x (fv f) then mk_forall(x,t,f)
  else f

let smk_foralls (xts,f) = 
  let fvs = fv f in
  let isfree (x,t) = List.mem x fvs in
  let useful = List.filter isfree xts in
  if useful=[] then f else mk_foralls(useful,f)

let smk_and fs = 
  let set_insert x xs = if List.mem x xs then xs else x::xs in
  let rec mkand1 fs acc = match fs with
  | [] -> (match acc with
    | [] -> Const (BoolConst true)
    | [f] -> f
    | _ -> mk_and (List.rev acc))
  | App(Const And,fs0) :: fs1 -> mkand1 (List.rev_append fs0 fs1) acc
  | Const (BoolConst true)::fs1 -> mkand1 fs1 acc
  | Const (BoolConst false)::fs1 -> Const (BoolConst false)
  | fs::fs1 -> mkand1 fs1 (set_insert fs acc)
in mkand1 fs []

let smk_metaand fs = 
  let set_insert x xs = if List.mem x xs then xs else x::xs in
  let rec mkand1 fs acc = match fs with
  | [] -> (match acc with
    | [] -> Const (BoolConst true)
    | [f] -> f
    | _ -> mk_metaand (List.rev acc))
  | App(Const And,fs0) :: fs1 -> mkand1 (List.rev_append fs0 fs1) acc
  | Const (BoolConst true)::fs1 -> mkand1 fs1 acc
  | Const (BoolConst false)::fs1 -> Const (BoolConst false)
  | fs::fs1 -> mkand1 fs1 (set_insert fs acc)
in mkand1 fs []

let smk_impl(f1,f2) = 
  match f1 with
  | Const (BoolConst false) -> Const (BoolConst true)
  | Const (BoolConst true) -> f2
  | _ -> (match f2 with
    | App(Const Impl,[f2a;f2b]) -> mk_impl(smk_and [f1;f2a], f2b)
    | Const (BoolConst false) -> mk_not f1
      | Const (BoolConst true) -> f2
      | _ -> mk_impl(f1,f2))

(* ********* Sequents ************** *)

type sequent = form list * form
let form_of_sequent (fs,f) = 
  if fs=[] then f else mk_metaimpl(smk_metaand fs,f)

(*************** DEBUG -- PRINTING *************************)

let nullConstName = "nullObj"

let isabelle_formula (f:form) = 
  let rec p s = "(" ^ s ^ ")" 
  and wr_int k = match k with
  | Const (IntConst i) -> Printf.sprintf "%d" i
  | _ -> failwith "vcprint.isa_form: non-constant cardinality constraint"
  and wr_form_list op fs = p (wr_form_list1 op fs)
  and infx f1 op f2 = p (wr_form f1 ^ op ^ wr_form f2)
  and wr_binder binder vts f = 
    p (binder ^ " " ^ String.concat " " (List.map fst vts) ^ ". " ^ wr_form f)
  and wr_type t = match t with
  | TypeVar id -> id
  | TypeObjRef str -> str ^ "-" ^ "OBJECT"
  | TypeArray t1 -> p (wr_type t1) ^ " array"
  | TypeSet t1 -> p (wr_type t1) ^ " set"
  | TypeList t1 -> p (wr_type t1) ^ " list"
  | TypeFun(ts,t1) -> p (wr_fun_type ts t1)
  | TypeInt -> "int"
  | TypeBool -> "bool"
  | TypeVoid -> "void"
  | TypeUniverse -> "universe"
  and wr_fun_type ts t1 = match ts with
  | [] -> wr_type t1
  | t2::ts2 -> wr_type t2 ^ " -> " ^ wr_fun_type ts2 t1
  and wr_form f =  match f with
  | Const (BoolConst true) -> "True"
  | Const (BoolConst false) -> "False"
  | App(Const Not, [f]) -> p ("~" ^ wr_form f)
  | App(Const Or,fs) -> wr_form_list " | " fs
  | App(Const And,fs) -> wr_form_list " & " fs
  | App(Const MetaAnd,fs) -> "[|" ^ wr_form_list1 ";\n" fs ^ "|]"
  | App(Const Impl,[f1;f2]) -> infx f1 " --> " f2
  | App(Const MetaImpl,[f1;f2]) -> infx f1 " ==>\n    " f2
  | App(Const Iff,[f1;f2]) -> infx f1 " = " f2

  | App(Const Eq,[f1;f2]) -> infx f1 " = " f2

  | Const EmptysetConst -> "{}"
  | App(Const Elem,[f1;f2]) -> infx f1 " : " f2
  | App(Const Sub,[f1;f2]) -> infx f1 " <= " f2
  | App(Const Cap,fs) -> wr_form_list " Int " fs
  | App(Const Cup,fs) -> wr_form_list " Un " fs
  | App(Const Diff,[f1;f2]) -> infx f1 " - " f2
  | App(Const Disjoint,fs) -> "handleDisjoint"
  | App(Const Cardeq,[f1;k]) -> "cardeq" ^ wr_int k ^ " " ^ wr_form f1
  | App(Const Cardleq,[f1;k]) -> "cardleq" ^ wr_int k ^ " " ^ wr_form f1
  | App(Const Cardgeq,[f1;k]) -> "cardgeq" ^ wr_int k ^ " " ^ wr_form f1

  | Const (IntConst k) -> Printf.sprintf "(%d::int)" k
  | App(Const Lt,[f1;f2]) -> infx f1 " < " f2
  | App(Const LtEq,[f1;f2]) -> infx f1 " <= " f2
  | App(Const Gt,[f1;f2]) -> infx f2 " < " f1
  | App(Const GtEq,[f1;f2]) -> infx f2 " <= " f1

  | App(Const Plus,[f1;f2]) -> infx f1 " + " f2
  | App(Const Minus,[f1;f2]) -> infx f1 " - " f2
  | App(Const Mult,[f1;f2]) -> infx f1 " * " f2
  | App(Const Div,[f1;f2]) -> infx f1 " div " f2
  | App(Const Mod,[f1;f2]) -> infx f1 " mod " f2

  | Const NullConst -> nullConstName
  | Const c -> string_of_const c 

  | Var v -> v
  | Binder(Forall,vts,f1) -> wr_binder "ALL" vts f1
  | Binder(Exists,vts,f1) -> wr_binder "EX" vts f1
  | Binder(Lambda,vts,f1) -> wr_binder "%" vts f1
  | Binder(Comprehension,[(v,t)],f1) ->
      "{" ^ v ^ ". " ^ wr_form f1 ^ "}"
  | Binder(Comprehension,_,f1) -> failwith "vcprint.isa: multivar comprehensions?"
  | TypedForm(f1,t) -> p (wr_form f1 ^ " :: " ^ wr_type t)
  | App(f1,fs) -> wr_form_list " " (f1::fs)
  and wr_form_list1 op fs = match fs with
  | [] -> ""
  | [f] -> wr_form f
  | f::fs1 -> wr_form f ^ op ^ wr_form_list1 op fs1
  in wr_form f

(* **************************************** *)
(*             simplification               *)
(* **************************************** *)

let rec simplify (f:form) = 
let res = (match f with
| App(f1,[]) -> simplify f1
| App(Const And,fs) -> smk_and (List.map simplify fs)
| App(Const Impl,[f1;f2]) -> smk_impl(simplify f1, simplify f2)
| Binder(Forall,vts,f1) -> smk_foralls(vts,f1)
| Var v -> f
| Const c -> f
| Binder(k,vts,f1) -> Binder(k,vts,simplify f1)
| App(f1,fs) -> App(simplify f1, List.map simplify fs)
| TypedForm(f1,t) -> TypedForm(simplify f1,t)) in
(* print_string ("Original formula:\n" ^ isabelle_formula f ^ "\n simplified formula:\n" ^ isabelle_formula res ^ "\n"); *)
res