qualifier.ml

(*
 * Copyright © 2009-11 The Regents of the University of California. 
 * All rights reserved. 
 *
 * Permission is hereby granted, without written agreement and without 
 * license or royalty fees, to use, copy, modify, and distribute this 
 * software and its documentation for any purpose, provided that the 
 * above copyright notice and the following two paragraphs appear in 
 * all copies of this software. 
 * 
 * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY 
 * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES 
 * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN 
 * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY 
 * OF SUCH DAMAGE. 
 * 
 * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, 
 * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY 
 * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS 
 * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION 
 * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
 *
 *)

(**
 * This module implements a module for representing and manipulating Qualifiers.
 * *)

module F = Format

module P  = Ast.Predicate
module E  = Ast.Expression
module Sy = Ast.Symbol
module So = Ast.Sort
module Su = Ast.Subst
module SM = Sy.SMap
module SS = Sy.SSet
module IM = Misc.IntMap

open Misc.Ops
open Ast

let mydebug = false

(**************************************************************************)
(***************************** Qualifiers *********************************)
(**************************************************************************)
 
type q = { name    : Sy.t 
         ; vvar    : Sy.t
         ; vsort   : So.t
         ; params  : (Sy.t * So.t) list
         ; pred    : pred
         ; args    : expr list option 
           (* when args = Some es, es = vv'::[e1;...;en]
              where vv' is the applied vv and e1...en are the args applied to ~A1,...,~An *)
         }

type t = q      (* to appease the functor gods. *)

let rename          = fun n -> fun q -> {q with name = n} 
let name_of_t       = fun q -> q.name
let vv_of_t         = fun q -> q.vvar
let sort_of_t       = fun q -> q.vsort
let pred_of_t       = fun q -> q.pred
let params_of_t     = fun q -> q.params
let all_params_of_t = fun q -> (q.vvar, q.vsort) :: q.params

let args_of_t q  =
  let xs = all_params_of_t q |> List.map fst in
  let es = match q.args with
           | Some es -> es
           | None    -> List.map eVar xs
  in Misc.combine "Qualifier.args_of_t" xs es

let print_param ppf (x, t) =
  F.fprintf ppf "%a:%a" Sy.print x So.print t 

let print_params ppf args =
  F.fprintf ppf "%a" (Misc.pprint_many false ", " print_param) args

let print_args ppf q =
  q |> args_of_t |> List.map snd 
    |> F.fprintf ppf "%a(%a)" Sy.print q.name (Misc.pprint_many false ", " E.print) 
 
(* API *) 
let print ppf q = 
  F.fprintf ppf "qualif %a(%a):%a" 
    Sy.print q.name
    print_params (all_params_of_t q) 
    P.print q.pred

  
(**********************************************************************)
(****************** Canonizing Wildcards (e.g. _ ---> ~A) *************)
(**********************************************************************)

let is_free params x = Misc.list_assoc_maybe x params |> Misc.maybe_bool |> not

let canonizer params =
  let fresh = Misc.mk_string_factory "~AA" |> fst |> (fun f -> f <+> Sy.of_string <+> eVar) in
  let memo  = Hashtbl.create 7 in
  function
    | (Var x, _) when is_free params x && Hashtbl.mem memo x -> 
        Hashtbl.find memo x
    | (Var x, _) when is_free params x && Sy.is_wild_fresh x ->
        fresh () 
    | (Var x, _) when is_free params x && Sy.is_wild_any x -> 
        fresh () >> Hashtbl.replace memo x 
    | e -> e 

(**************************************************************************)
(*************** Expanding Away Sets of Ops and Rels **********************)
(**************************************************************************)
 
let expand_with_list f g =
  List.map f <+> Misc.cross_flatten <+> Misc.map g

let expand_with_pair f g =
  Misc.map_pair f <+> Misc.uncurry Misc.cross_product <+> Misc.map g

let crunchExpr f e1s xs e2s =
  List.map begin fun e1 -> 
    List.map begin fun e2 ->
      List.map begin fun x ->
        f (e1, x, e2)
      end xs
    end e2s
  end e1s
  |> List.flatten |> List.flatten

let rec expand_p ((p,_) as pred) = match p with 
   | And ps             -> expand_ps pAnd ps
   | Or ps              -> expand_ps pOr ps
   | Not p              -> expand_p p |> List.map pNot 
   | Imp (p1,p2)        -> expand_pp pImp (p1, p2)
   | Iff (p1,p2)        -> expand_pp pIff (p1, p2)
   | Forall(qs, p)      -> expand_p p |> List.map (fun p -> pForall (qs, p))
   | Bexp e             -> expand_e e |> List.map pBexp
   | MAtom (e1, rs, e2) -> let (e1s, e2s) = Misc.map_pair expand_e (e1,e2) in
                           crunchExpr pAtom e1s rs e2s
   | Atom (e1, r, e2)   -> let (e1s, e2s) = Misc.map_pair expand_e (e1,e2) in
                           crunchExpr pAtom e1s [r] e2s
   | _                  -> [pred]

and expand_e ((e,_) as expr) = match e with
   | MExp es            -> Misc.flap expand_e es
   | App (f, es)        -> expand_es (fun es -> eApp (f, es)) es
   | Bin (e1, op, e2)   -> expand_ep (fun (e1,e2) -> eBin (e1, op, e2)) (e1, e2) 
   | MBin (e1, ops, e2) -> let e1s, e2s = Misc.map_pair expand_e (e1, e2) in
                           crunchExpr eBin e1s ops e2s
   | Fld (s, e)         -> expand_e e |> List.map (fun e -> eFld (s,e))
   | Cst (e, t)         -> expand_e e |> List.map (fun e -> eCst (e,t))
   | Ite (p,e1,e2)      -> let e1s, e2s = Misc.map_pair expand_e (e1, e2) in
                           let ps       = expand_p p in 
                           List.map begin fun e1 ->
                             List.map begin fun e2 ->
                               List.map begin fun p ->
                                 eIte (p, e1, e2)
                               end ps
                             end e2s
                           end e1s
                           |> List.flatten |> List.flatten
   | _ -> [expr]

and expand_ps x = expand_with_list expand_p x
and expand_pp x = expand_with_pair expand_p x
and expand_es x = expand_with_list expand_e x
and expand_ep x = expand_with_pair expand_e x

(* API *)
let expand_qual q = 
  expand_p q.pred
  |> List.map (fun p -> {q with pred = p})

(**************************************************************************)
(*************** Expanding Away Sets of Ops and Rels **********************)
(**************************************************************************)

let make_def_deps qnames q = 
  let res = ref [] in
  let p' : pred  = P.map begin function 
                         | Bexp (App (f, args),_), _ 
                           when SS.mem f qnames -> res := (f, args) :: !res; pTrue 
                         | p -> p 
                         end id q.pred  
  in (q.name, !res) 
(*  >> (fun (n, xs) ->  F.printf "qdep %a = %a \n" Sy.print n (Misc.pprint_many false ", " Sy.print) (List.map fst xs) )
  *)

let check_def_deps qm = 
  List.iter begin fun (n, fargs) ->
      List.iter begin fun (f, args) ->
        match SM.finds f qm with
        | [q] -> asserts (List.length args = 1 + List.length q.params) 
                 "Malformed Qualifier: %s with incorrect application of %s"
                 (Sy.to_string n) (Sy.to_string f)
        | _::_::_ -> assertf "Malformed Qualifier: %s refers to multiply defined %s" 
                 (Sy.to_string n) (Sy.to_string f)
        | _   -> ()     
(*      | []  -> assertf "Malformed Qualifier: %s refers to unknown %s" 
                 (Sy.to_string n) (Sy.to_string f) *)
 
      end fargs
  end

let order_by_defs qm qs = 
  let _    = print_now "Q.order_by_defs 1 \n" in
  let is   = Misc.range 0 (List.length qs)                                      in
  let _    = print_now "Q.order_by_defs 2 \n" in
  let qis  = List.combine qs is                                                 in
  let _    = print_now "Q.order_by_defs 3 \n" in
  let i2q  = qis  |>: Misc.swap |> IM.of_list  |> Misc.flip IM.find             in
  let _    = print_now "Q.order_by_defs 4 \n" in
  let i2s  = i2q <+> name_of_t <+> Sy.to_string                                 in  
  let _    = print_now "Q.order_by_defs 5 \n" in
  let n2i  = qis  |>: Misc.app_fst name_of_t |> SM.of_list 
             |> (fun m n -> SM.safeFind n m "order_by_defs") in
   
  let _    = print_now "Q.order_by_defs 6 \n" in
  let qnams= qs |>: name_of_t |> SS.of_list in
  let deps = qs |>: make_def_deps qnams >> check_def_deps qm                       in
  let _    = print_now "Q.order_by_defs 7 \n" in
  let ijs  = deps |> Misc.flap (fun (n, fargs) -> fargs |>: (fun (f,_) -> (n, f)))   
                  |> List.map (Misc.map_pair n2i)                               in
  let _    = print_now "Q.order_by_defs 8 \n" in
  let irs  = Fcommon.scc_rank "qualifier-deps" i2s is ijs                       in 
  let _    = print_now "Q.order_by_defs 9 \n" in
  Misc.fsort snd irs 
  |>: (fst <+> i2q)
(*   >> (F.printf "ORDERED QUALS:\n%a\n" (Misc.pprint_many true "\n" print)) *)

let expand_def qm p = match p with 
  | Bexp (App (f, args),_), _ -> begin
    match SM.finds f qm with
    | _::_::_ -> assertf "Ambiguous Qualifier: %s" (Sy.to_string f)
    | [q]     -> q |> all_params_of_t
                   |> List.map fst
                   |> Misc.flip (Misc.combine ("Q.expand_def "^ (P.to_string p))) args
                   |> Su.of_list
                   |> substs_pred q.pred
    | []      -> p (* assertf "Unknown Qualifier: %s"   (Sy.to_string f)  *)
    end
  | _ -> p
    
(* this MUST precede any renaming as renaming can screw up name resolution *)
let compile_definitions qs = 
  let _    = print_now "Q.compile_definitions 0 \n" in
  let qm   = List.fold_left (fun qm q -> SM.adds q.name [q] qm) SM.empty qs in
  let _    = print_now "Q.compile_definitions 1 \n" in
  let qs'  = order_by_defs qm qs                                       in 
  let _    = print_now "Q.compile_definitions 2 \n" in
  List.fold_left begin fun qm q -> 
    let q' = {q with pred = P.map (expand_def qm) id q.pred } in
    SM.adds q.name [q'] qm
  end SM.empty qs'
  >> (fun _ -> print_now "Q.compile_definitions 3\n")
  |> SM.range |> Misc.flatten

(**************************************************************************)
(************************* Normalize Qualifier Sets ***********************)
(**************************************************************************)

let remove_duplicates qs = 
  qs |> Misc.kgroupby (all_params_of_t <*> pred_of_t)
     |> List.map (fun (_,x::_) -> x)

let rename_qual q i = 
  {q with name = Sy.suffix q.name (string_of_int i)}

let uniquely_rename qs =
  Misc.mapfold begin fun m q ->
    if SM.mem q.name m then
      let i = SM.safeFind q.name m "uniquelyRename" in
      (SM.add q.name (i+1) m, rename_qual q i)
    else 
      (SM.add q.name 0 m, q)
  end SM.empty qs 
  |> snd

(* API *)
let normalize qs =
  qs >> (fun _ -> print_now "Q.normalize 0\n")
     |> Misc.flap expand_qual
     >> (fun _ -> print_now "Q.normalize 1\n")
     |> compile_definitions
     >> (fun _ -> print_now "Q.normalize 2\n")
     |> remove_duplicates
     >> (fun _ -> print_now "Q.normalize 3\n")
     |> uniquely_rename
     >> (fun _ -> print_now "Q.normalize 4\n")


(**************************************************************************)
(********************************** Create ********************************)
(**************************************************************************)
 
(* Rename to ensure unique names 
let subst_vv v' q =
  { q with vvar = v' ; pred = P.subst q.pred q.vvar (eVar v')} 
*)

let close_params vts p =
  p |> P.support
    |> List.filter (Sy.is_wild <&&> is_free vts) 
    |> List.map (fun x -> (x, So.t_int (* t_generic 0 causes blowup? *)))
    |> (@) vts (* Sy.SMap.of_list *)

(* API *)
let create n v t vts p =
  let p    = P.map id (canonizer vts) p in
  let vts  = close_params vts p         in 
  let _    = asserts (Misc.distinct vts) "Error: Q.create duplicate params %s \n" (Sy.to_string n)
  in { name   = n 
     ; vvar   = v
     ; vsort  = t
     ; pred   = p
     ; params = vts 
     ; args   = None }

(* DEBUG ONLY *)
let printb ppf (x, e) =
  F.fprintf ppf "%a:%a" Sy.print x E.print e 
let printbs ppf args =
  F.fprintf ppf "%a" (Misc.pprint_many false ", " printb) args

(* API *)
let inst q args =
  let _   = if mydebug then F.printf "\nQ.inst with <<%a>>\n" printbs args in 
  let xes = try q |> all_params_of_t |> List.map (fun (x,_) -> (x, List.assoc x args)) 
            with Not_found -> 
              let _ = F.printf "Error: Q.inst with bad args %a <<%a>>" print q printbs args 
              in assertf "Error: Q.inst with bad args \n" 
  in
  let v   = match xes with (_, (Var v, _)) :: _ -> v | _ -> assertf "Error: Q.inst with non-vvar arg" in
  let p   = xes |> Su.of_list |> Ast.substs_pred q.pred in
  { q with vvar = v; pred = p; args = Some (List.map snd xes)}


module QSet = Misc.ESet (struct
  type t = q
  let compare q1 q2 = 
    if (q1.name = q2.name) 
    then compare q1.args q2.args 
    else compare q1.name q2.name 
end)