open Types
open Paleprinter

let pale_name = "palemona"
let pale_aux_dir = "pale-aux-dir-tmp"

let ensure_pale_subdir () =
  try 
    let s = Unix.stat pale_aux_dir in
    match s.Unix.st_kind with
    | Unix.S_DIR -> ()
    | _ -> failwith
          ("non-directory '"^pale_aux_dir^"' in the way of auxiliary dir") 
  with Unix.Unix_error (Unix.ENOENT, _, _) ->
    Unix.mkdir pale_aux_dir 0o755
let mk_pale_filename fd =
  ensure_pale_subdir ();
  (pale_aux_dir ^ "/" ^ fd ^ ".pale")

let get_str_from_clause (c : string Aabsyn.clause) : string = 
  match c with
  | Aabsyn.FormulaClause s -> s
  | _ -> failwith
        "Only FormulaClause allowed in PALE plugin."

let write_clause (file : out_channel)
    (c : string Aabsyn.clause) : unit = 
  output_string file (get_str_from_clause c)

let copy_invariants (file : out_channel)  
(* writes 'invariant' declarations that begin with 
   'type', 'data', and 'pointer', but not the general formulas *)
    (mi : string Iabsyn.impl_module)
    (ab : string Aabsyn.abst_body) : unit =
  let fmat0 = List.hd mi.Iabsyn.formats in
  let f = fmat0.Iabsyn.format_name in
  let wr c =
    let str = get_str_from_clause c in begin
      if (String.sub str 0 4) = "type" then 
        let untilBracket = String.sub str 0 (String.length str - 2) in
        begin
          output_string file untilBracket;
          output_string file ("\ndata nextExternal : "^f^";\n"^
                              "pointer prevExternal : "^f^"\n"^
                              "[this^"^f^".nextExternal = {prevExternal}];\n"^
                              "bool isExternal;\n" ^
                              "bool isFresh;\n");
          output_string file "}\n\n"
        end
      else begin        
        if (String.sub str 0 4) = "data" || (String.sub str 0 7) = "pointer" then begin
          write_clause file c; output_string file "\n\n";
        end else begin
          () (* it's a proper invariant that needs to be extracted *)
        end
      end;
    end
  in List.iter wr ab.Aabsyn.invariants

let write_pred_defs (file : out_channel)
    (ma : string Aabsyn.abst_body) : unit = 
  let wr_def (d0: string Aabsyn.set_defn) =
    match (snd d0) with
    | Aabsyn.BaseForm d -> 
        let wr = output_string file in
        let set_name = Util.replace_dot_with_uscore (fst d0) in
        let pred_name = set_to_pred set_name in
        let bound_var = d.Aabsyn.x in
        let type_name = Util.replace_dot_with_uscore d.Aabsyn.xt in
        let defining_expr = d.Aabsyn.expr in
        begin
          wr "pred "; wr pred_name; 
          wr "(set "; wr set_name; wr ": "; wr type_name; wr ") =\n";
          wr "  allpos "; wr bound_var; wr " of "; wr type_name;
          wr ": "; wr bound_var; wr " in "; wr set_name; wr " <=> ";
          write_clause file defining_expr; wr ";\n"
        end
    | _ -> failwith "pale can't take cpd sets"
  in List.iter wr_def ma.Aabsyn.set_defns

let copy_global_bools (file : out_channel) (mi : string Iabsyn.impl_module) : unit =
  let wr s = output_string file s in
  let copy_global (v,t) = 
    match t with
    | TBool -> wr ("bool "^v^";\n");
    | _ -> () in
  List.iter copy_global mi.Iabsyn.references

let write_external_inv_def (file : out_channel)
    (ma : string Aabsyn.abst_body)
    (mi : string Iabsyn.impl_module) : unit =
  let wr s = output_string file s in
  let fmat = List.hd mi.Iabsyn.formats in
  let fmat_name = fmat.Iabsyn.format_name in
  let filter_obj_types = 
    function
      | (_, TObj _) -> true
      | _ -> false in
  let fmat_fields = List.map 
      (fun x -> (fst x).Id.f_name)
      (List.filter filter_obj_types
         fmat.Iabsyn.fields) in
  let (def_str, d) = match (List.hd ma.Aabsyn.set_defns) with
  | (_, Aabsyn.BaseForm d0) -> 
      (get_str_from_clause d0.Aabsyn.expr, d0)
  | _ -> failwith "can't write_external_inv_def of cpd" in
  let v = String.sub def_str (String.length def_str - 1) 1 in  
  let write_field_null s = wr (v^"."^s^"=null & ") in
  begin    
    wr ("data externals : "^fmat_name^";\n");
    wr ("data fresh : "^fmat_name^";\n\n");
    wr "pred externalInv1() = \n";
    wr ("  allpos "^v^" of " ^ fmat_name ^ ":\n");
    wr ("("^v^".isExternal =>\n");
    List.iter write_field_null fmat_fields;
    wr ("externals<nextExternal*>"^v^") &\n");
    wr ("((!"^v^".isExternal & !"^v^".isFresh) =>\n");
    wr (v^".nextExternal=null & "^v^".prevExternal=null & !externals<nextExternal*>"^v^");\n\n");

    wr "pred externalInv() = externalInv1() &\n  ";
    wr ("allpos "^v^" of "^ fmat_name^": ("^v^".isFresh =>\n");
    List.iter write_field_null fmat_fields;
    wr ("fresh<nextExternal*>"^v^")");
    wr ";\n\n";
  end

let wr_repdef file mi ms = begin
  let wr s = output_string file s in
  let fmat = List.hd mi.Iabsyn.formats in
  let fmt = fmat.Iabsyn.format_name in
  let global_sets = Spec.collect_sets_types ms in
  let setnames = List.map Util.replace_dot_with_uscore
      (List.map fst global_sets) in
  wr ("pred isRep(pointer n:" ^ fmt ^ ") = \n");
  wr ("existset S of " ^ fmt ^ ": " ^ set_to_pred (List.hd setnames) ^ "(S) &");
  wr "!(n in S) & !externals<nextExternal*>n & !fresh<nextExternal*>n;\n\n";
end

let write_header (file : out_channel)
    ((ma : string Aabsyn.abst_body),
     (ms : Sabsyn.spec_module),
     (mi : string Iabsyn.impl_module)) : unit = 
  begin
    copy_invariants file mi ma;
    copy_global_bools file mi;
    write_external_inv_def file ma mi;   
    wr_repdef file mi ms;
    write_pred_defs file ma;
    output_string file "\n";
  end

let pale_says_valid (file_name : string) : bool =
  let out_file = file_name ^ ".out" in
  let err_file = file_name ^ ".err" in
  begin
    (try Sys.remove out_file with Sys_error _ -> ());    
    (*
    ignore (Sys.command ("cat " ^ file_name));
     *)
    let result = Sys.command (pale_name ^ " " ^ file_name ^ " > " ^ out_file 
                              ^ ">&" ^ err_file) in
    (result==42)
  end

let analyze_proc 
    ((ab : string Aabsyn.abst_body),
     (ms : Sabsyn.spec_module),
     (mi : string Iabsyn.impl_module))
    (p : Sabsyn.proc_spec) : bool = 
  let file_name = mk_pale_filename 
      (p.Sabsyn.proc_name.Id.p_name ^ "-" ^ p.Sabsyn.proc_name.Id.p_module) in
  let file = open_out file_name in
  let wr = output_string file in
  let err s = Util.error s in
  let pname = p.Sabsyn.proc_name in
  let pi = Ast.fetch_impl_proc (Id.name_of_proc p.Sabsyn.proc_name) mi in

  let (global_refs : (string * string) list) =
    let pick_formats (v,t) = match t with
    | TObj format_name -> [(v,format_name)]
    | _ -> [] in        
    List.concat (List.map pick_formats mi.Iabsyn.references) in
  let _ = if global_refs = [] then err "no global references found" in
  let fmt = match (List.hd global_refs) with (v,t) -> t in
  let _ =
    if not (List.for_all (fun (v,t) -> t=fmt) global_refs) 
    then err ("All globals expected to be references of format " ^ fmt)
    else () in
  let global_refnames = 
    List.map Util.replace_dot_with_uscore
      (List.map fst global_refs) in

  let global_sets0 = Spec.collect_sets_types ms in
  let ab_defined_sets = 
    List.map fst ab.Aabsyn.set_defns in
  let global_sets = 
    if ab_defined_sets = [] then global_sets0 else
    List.filter 
      (fun (v,t) -> List.mem v ab_defined_sets) global_sets0 in
  let _ = 
    if not (List.for_all (fun (v,t) -> t=(TObj fmt)) global_sets) 
    then err ("All specification sets expected to be of format " ^ fmt)
    else () in
  let setnames = List.map Util.replace_dot_with_uscore
      (List.map fst global_sets) in
  
  let is_pointer fmt ((v,t) : (Id.var_t * value_type)) : bool = match t with
  | TObj fmt1 when fmt1=fmt -> true
  | _ -> false in
  
  let pointer_paramnames = List.map fst (List.filter (is_pointer fmt) p.Sabsyn.formals) in
  
  let ret = match p.Sabsyn.ret_val with
  | Some (v,(TObj fmt1)) when fmt1=fmt -> Some v
  | _ -> None in

  let retparam = match ret with
  | Some v -> [v]
  | None -> [] in

  let singletons = global_refnames @ pointer_paramnames in
  let obj_locals = Iabsyn.collect_obj_locals pi.Iabsyn.proc_body in

  let write_params() =
    let mk_param v = "pointer " ^ v ^ " : " ^ fmt in
    let printed = List.map mk_param pointer_paramnames in
    begin
      wr "proc ";
      wr pname.Id.p_name; wr "_"; wr pname.Id.p_module;
      wr "("; 
      wr (String.concat ";" printed); 
      wr "):";
      (match ret with
      | Some t -> wr fmt
      | None -> wr "void");
      wr "\n"
    end in

  let write_clause_conjunct (file : out_channel)
      (c : string Aabsyn.clause) : unit = 
    output_string file ("(" ^ (get_str_from_clause c) ^ ") & ") in

  let write_explicit_invariants() =
  (* writes 'invariant' declarations that DO NOT begin with
   'type', 'data', and 'pointer', so they are presumed to be formulas *)
    let wrinv c =
      let str = get_str_from_clause c in
      if not ((String.sub str 0 4) = "type" ||
      (String.sub str 0 4) = "data" || 
      (String.sub str 0 7) = "pointer") then
        write_clause_conjunct file c
    in List.iter wrinv ab.Aabsyn.invariants in

  let write_bools_init_eq_curent() =
    let copy_global (v,t) = 
      match t with
      | TBool -> wr ("(" ^v^"0 <=> "^v^") &");
      | _ -> () in
    List.iter copy_global mi.Iabsyn.references in      
  
  let write_precondition() =
    let wr_setdef s = begin
      wr (set_to_pred s); wr "(";
      wr s; wr ") &\n";
    end in
    let wr_external_general_case v =
      wr ("(!"^v^ " in " ^ 
          List.hd setnames ^  (* assumes first is data !!! *)
          " => "^v^".nextExternal!=null & "^v^".prevExternal!=null) & \n" ^
           "!"^v^".isFresh & ") in
    let get_param_name (v,t) = v in   
    begin
      wr "[externalInv() & ";
      wr ("(allpos n of " ^ fmt ^ ": (n in rep0 <=> isRep(n))) & ");
      wr "fresh != null & fresh.nextExternal!=null &";
      (if (p.Sabsyn.formals != []) then
        let v = get_param_name (List.hd p.Sabsyn.formals) in
        wr_external_general_case v);
      write_explicit_invariants();
      List.iter wr_setdef setnames;
      write_bools_init_eq_curent();
      wr (Paleba.pale_string fmt singletons p.Sabsyn.requires);
      wr "]\n{"
    end in

  let wr_no_exposure() =
    wr ("& (allpos obj of "^ fmt^": (isRep(obj) & !(obj in rep0) => obj.isFresh))")
  in

  let write_postcondition() =
    let wr_quant s = 
      wr ("existset " ^ primed s ^ " of " ^ fmt ^ ":") in
    let wr_setdef s = begin
      wr (set_to_pred s); wr "(";
      wr (primed s); wr ") &\n";
    end in
    let return_stat = match ret with
    | Some v -> "return "^v^";\n"
    | None -> "" in
    begin    
      wr "split [externalInv1() &";
      write_explicit_invariants();
      wr " (";
      List.iter wr_quant setnames;
      List.iter wr_setdef setnames;
      wr (Paleba.pale_string fmt (retparam @ singletons) p.Sabsyn.ensures);
      wr_no_exposure();
      wr ")];\n";
      wr return_stat;
      wr "}\n[true]\n"
    end in

  let return_param rv = 
    match rv with
    | Some (v,(TObj fmt1)) when fmt1=fmt -> "pointer "^v^" : "^fmt^";\n"
    | Some (v,TBool) -> "bool "^v^";\n"
    | _ -> "" in

  let write_initial_bools() =
    let copy_global (v,t) = 
      match t with
      | TBool -> wr ("bool "^v^"0;\n");
      | _ -> () in
    List.iter copy_global mi.Iabsyn.references in      

  let write_procedure() = 
    let wrset s = begin
      wr "set "; wr s;
      wr " : "; wr fmt; wr ";\n"
    end in
    begin
      wr "\n";
      write_params();
      List.iter wrset setnames;
      wrset "rep0";
      write_initial_bools();
      write_precondition();
      wr ("pointer prv77, nxt77 : " ^ fmt ^ ";\n");
      wr (return_param p.Sabsyn.ret_val);
      Paleprinter.print file (ab,ms,mi) (List.hd setnames, fmt,retparam,singletons, obj_locals) p pi;
      write_postcondition();
    end in
  
  begin
    Util.amsg ("Analyzing procedure " ^ p.Sabsyn.proc_name.Id.p_name ^"... ");
    write_header file (ab,ms,mi);
    Palestd.write_preds file (ab,ms,mi) p;
    write_procedure();
    close_out file;
    if pale_says_valid file_name then begin
      Util.msg (" procedure " ^ p.Sabsyn.proc_name.Id.p_name ^ " is ");
      Util.amsg ("valid.\n");
      true
    end else begin
      Util.msg (" procedure " ^ p.Sabsyn.proc_name.Id.p_name ^ " is ");
      Util.amsg ("invalid.\n");
      false
    end
  end

let neutral_procs ((ma, ms, mi):string Aabsyn.abst_body * 
       Sabsyn.spec_module * string Iabsyn.impl_module) =
  let mn = ms.Sabsyn.module_name in
  let extract_fields t form = 
    let rec extract_fields0 form : string list =
      match form with
        | Vcform.App (Vcform.Var fd, a) -> 
            (if (fd <> "rtrancl") then [fd] else []) @
              List.concat (List.map extract_fields0 a)
        | Vcform.App (f, a) -> 
            (List.concat ((extract_fields0 f) ::
                            (List.map extract_fields0 a)))
        | Vcform.Var _ -> []
        | Vcform.Binder (_, _, f) -> extract_fields0 f
        | Vcform.Const _ -> []
        | Vcform.TypedForm (f, _) -> extract_fields0 f in
      List.map (fun x -> (t, Id.fetch_field mn x)) (extract_fields0 form) in
(*
 * What we really need to do is to scan the abst module for
 * invariant declarations that contain 'type Foo = { data bar:X; }'
 * and extract all the 'bar' things.
  let ap = Util.remove_dups (List.concat (List.map (fun x -> 
                                                      match (snd x) with 
                                                        | Aabsyn.BaseForm bf -> 
                                                            (match bf.Aabsyn.expr with
                                                               | Aabsyn.FormulaClause f -> extract_fields bf.Aabsyn.xt f
                                                               | _ -> failwith "can't deal with formula in Bohne")
                                                        | _ -> failwith "not base")
                                            mab.Aabsyn.set_defns) @ 
                               (List.concat (List.map (fun x -> match x with 
                                                         | Aabsyn.FormulaClause f -> extract_fields "<unknown>" f
                                                         | _ -> failwith "can't deal with formula in PALE.") mab.Aabsyn.invariants))) in
    List.concat (List.map (fun p -> if (Typestate.proc_hits p ap) then [] else [p.proc_id]) mi.procs)
*)
    []

let analyze_module 
    (mn:string)
    ((ma : string Aabsyn.abst_body),
     (ms : Sabsyn.spec_module),
     (mi : string Iabsyn.impl_module))
    (pn:string list) : bool = 
  begin
    let procs = 
      List.filter (fun mm -> List.mem mm.Sabsyn.proc_name.Id.p_name pn) 
        ms.Sabsyn.procs in
    let results = List.map (analyze_proc (ma,ms,mi)) procs in
    List.fold_left (fun x y -> x & y) true results
  end