path: root/src/spec_analysis.ml

(**************************************************************************)
(*     Sail                                                               *)
(*                                                                        *)
(*  Copyright (c) 2013-2017                                               *)
(*    Kathyrn Gray                                                        *)
(*    Shaked Flur                                                         *)
(*    Stephen Kell                                                        *)
(*    Gabriel Kerneis                                                     *)
(*    Robert Norton-Wright                                                *)
(*    Christopher Pulte                                                   *)
(*    Peter Sewell                                                        *)
(*                                                                        *)
(*  All rights reserved.                                                  *)
(*                                                                        *)
(*  This software was developed by the University of Cambridge Computer   *)
(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
(*  SUCH DAMAGE.                                                          *)
(**************************************************************************)

open Ast
open Util
open Ast_util

module Nameset = Set.Make(String)

let mt = Nameset.empty

let set_to_string n = 
  let rec list_to_string = function
    | [] -> ""
    | [n] -> n
    | n::ns -> n ^ ", " ^ list_to_string ns in
  list_to_string (Nameset.elements n)


(*Query a spec for its default order if one is provided. Assumes Inc if not *)
(* let get_default_order_sp (DT_aux(spec,_)) =
  match spec with
  | DT_order (Ord_aux(o,_)) ->
    (match o with
     | Ord_inc -> Some {order = Oinc}
     | Ord_dec -> Some { order = Odec}
     | _ -> Some {order = Oinc})
  | _ -> None

let get_default_order_def = function
  | DEF_default def_spec -> get_default_order_sp def_spec
  | _ -> None

let rec default_order (Defs defs) =
  match defs with
  | [] -> { order = Oinc } (*When no order is specified, we assume that it's inc*)
  | def::defs ->
    match get_default_order_def def with
    | None -> default_order (Defs defs)
    | Some o -> o *)

(*Is within range*)

(* let check_in_range (candidate : big_int) (range : typ) : bool =
  match range.t with
  | Tapp("range", [TA_nexp min; TA_nexp max]) | Tabbrev(_,{t=Tapp("range", [TA_nexp min; TA_nexp max])}) ->
    let min,max = 
      match min.nexp,max.nexp with
      | (Nconst min, Nconst max)
      | (Nconst min, N2n(_, Some max))
      | (N2n(_, Some min), Nconst max)
      | (N2n(_, Some min), N2n(_, Some max))
        -> min, max
      | (Nneg n, Nconst max) | (Nneg n, N2n(_, Some max))->
        (match n.nexp with
         | Nconst abs_min | N2n(_,Some abs_min) ->
           (minus_big_int abs_min), max
         | _ -> assert false (*Put a better error message here*))
      | (Nconst min,Nneg n) | (N2n(_, Some min), Nneg n) ->
        (match n.nexp with
         | Nconst abs_max | N2n(_,Some abs_max) ->
           min, (minus_big_int abs_max)
         | _ -> assert false (*Put a better error message here*))
    | (Nneg nmin, Nneg nmax) ->
      ((match nmin.nexp with
          | Nconst abs_min | N2n(_,Some abs_min) -> (minus_big_int abs_min)
          | _ -> assert false (*Put a better error message here*)),
       (match nmax.nexp with
        | Nconst abs_max | N2n(_,Some abs_max) -> (minus_big_int abs_max)
        | _ -> assert false (*Put a better error message here*)))
    | _ -> assert false        
    in le_big_int min candidate && le_big_int candidate max
  | _ -> assert false

(*Rmove me when switch to zarith*)
let rec power_big_int b n =
  if eq_big_int n zero_big_int
  then unit_big_int
  else mult_big_int b (power_big_int b (sub_big_int n unit_big_int))

let unpower_of_2 b =
  let two = big_int_of_int 2 in
  let four = big_int_of_int 4 in
  let eight = big_int_of_int 8 in
  let sixteen = big_int_of_int 16 in
  let thirty_two = big_int_of_int 32 in
  let sixty_four = big_int_of_int 64 in
  let onetwentyeight = big_int_of_int 128 in
  let twofiftysix = big_int_of_int 256 in
  let fivetwelve = big_int_of_int 512 in
  let oneotwentyfour = big_int_of_int 1024 in
  let to_the_sixteen = big_int_of_int 65536 in
  let to_the_thirtytwo = big_int_of_string "4294967296" in
  let to_the_sixtyfour = big_int_of_string "18446744073709551616" in
  let ck i = eq_big_int b i in
  if      ck unit_big_int     then zero_big_int
  else if ck two              then unit_big_int
  else if ck four             then two
  else if ck eight            then big_int_of_int 3
  else if ck sixteen          then four
  else if ck thirty_two       then big_int_of_int 5
  else if ck sixty_four       then big_int_of_int 6
  else if ck onetwentyeight   then big_int_of_int 7
  else if ck twofiftysix      then eight
  else if ck fivetwelve       then big_int_of_int 9
  else if ck oneotwentyfour   then big_int_of_int 10
  else if ck to_the_sixteen   then sixteen
  else if ck to_the_thirtytwo then thirty_two
  else if ck to_the_sixtyfour then sixty_four
  else let rec unpower b power =
         if eq_big_int b unit_big_int
         then power
         else (unpower (div_big_int b  two) (succ_big_int power)) in
    unpower b zero_big_int

let is_within_range candidate range constraints =
  let candidate_actual = match candidate.t with
    | Tabbrev(_,t) -> t
    | _ -> candidate in
  match candidate_actual.t with
  | Tapp("atom", [TA_nexp n]) ->
    (match n.nexp with
     | Nconst i | N2n(_,Some i) -> if check_in_range i range then Yes else No
     | _ -> Maybe)
  | Tapp("range", [TA_nexp bot; TA_nexp top]) ->
    (match bot.nexp,top.nexp with
     | Nconst b, Nconst t | Nconst b, N2n(_,Some t) | N2n(_, Some b), Nconst t | N2n(_,Some b), N2n(_, Some t) ->
       let at_least_in = check_in_range b range in
       let at_most_in = check_in_range t range in
       if at_least_in && at_most_in
       then Yes
       else if at_least_in || at_most_in
       then Maybe
       else No
     | _ -> Maybe)
  | Tapp("vector", [_; TA_nexp size ; _; _]) ->
    (match size.nexp with
     | Nconst i | N2n(_, Some i) ->
       if check_in_range (power_big_int (big_int_of_int 2) i) range
       then Yes
       else No
     | _ -> Maybe)
  | _ -> Maybe

let is_within_machine64 candidate constraints = is_within_range candidate int64_t constraints *)
  
(************************************************************************************************)
(*FV finding analysis: identifies the free variables of a function, expression, etc *)

let conditional_add typ_or_exp bound used id =
  let known_list =
    if typ_or_exp (*true for typ*)
    then ["bit";"vector";"unit";"string";"int";"bool";"boolean"]
    else ["=="; "!="; "|";"~";"&";"add_int"] in
  let i = (string_of_id id) in
  if Nameset.mem i bound || List.mem i known_list
  then used
  else Nameset.add i used

let conditional_add_typ = conditional_add true
let conditional_add_exp = conditional_add false


let nameset_bigunion = List.fold_left Nameset.union mt


let rec free_type_names_t consider_var (Typ_aux (t, _)) = match t with
  | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt
  | Typ_id name -> Nameset.add (string_of_id name) mt
  | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1)
                                     (free_type_names_t consider_var t2)
  | Typ_tup ts -> free_type_names_ts consider_var ts
  | Typ_app (name,targs) -> Nameset.add (string_of_id name) (free_type_names_t_args consider_var targs)
  | Typ_wild -> mt
  | Typ_exist (kids,_,t') -> List.fold_left (fun s kid -> Nameset.remove (string_of_kid kid) s) (free_type_names_t consider_var t') kids
and free_type_names_ts consider_var ts = nameset_bigunion (List.map (free_type_names_t consider_var) ts)
and free_type_names_maybe_t consider_var = function
  | Some t -> free_type_names_t consider_var t
  | None -> mt
and free_type_names_t_arg consider_var = function
  | Typ_arg_aux (Typ_arg_typ t, _) -> free_type_names_t consider_var t
  | _ -> mt
and free_type_names_t_args consider_var targs =
  nameset_bigunion (List.map (free_type_names_t_arg consider_var) targs)


let rec free_type_names_tannot consider_var = function
  | None -> mt
  | Some (_, t, _) -> free_type_names_t consider_var t


let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t =
  match t with
  | Typ_wild -> used
  | Typ_var (Kid_aux (Var v,l)) ->
    if consider_var
    then conditional_add_typ bound used (Ast.Id_aux (Ast.Id v,l))
    else used
  | Typ_id id -> conditional_add_typ bound used id
  | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret
  | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used
  | Typ_app(id,targs) ->
     List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id)
  | Typ_exist (kids,_,t') -> fv_of_typ consider_var (List.fold_left (fun b (Kid_aux (Var v,_)) -> Nameset.add v b) bound kids) used t'

and fv_of_targ consider_var bound used (Ast.Typ_arg_aux(targ,_)) : Nameset.t = match targ with
  | Typ_arg_typ t -> fv_of_typ consider_var bound used t
  | Typ_arg_nexp n -> fv_of_nexp consider_var bound used n
  | _ -> used

and fv_of_nexp consider_var bound used (Ast.Nexp_aux(n,_)) = match n with
  | Nexp_id id -> conditional_add_typ bound used id
  | Nexp_var (Ast.Kid_aux (Ast.Var i,_)) ->
    if consider_var
    then conditional_add_typ bound used (Ast.Id_aux (Ast.Id i, Parse_ast.Unknown))
    else used
  | Nexp_times (n1,n2) | Ast.Nexp_sum (n1,n2) | Ast.Nexp_minus(n1,n2) ->
    fv_of_nexp consider_var bound (fv_of_nexp consider_var bound used n1) n2
  | Nexp_exp n | Ast.Nexp_neg n -> fv_of_nexp consider_var bound used n
  | _ -> used

let typq_bindings (TypQ_aux(tq,_)) = match tq with
  | TypQ_tq quants ->
    List.fold_right (fun (QI_aux (qi,_)) bounds ->
        match qi with
        | QI_id (KOpt_aux(k,_)) ->
          (match k with
           | KOpt_none (Kid_aux (Var s,_)) -> Nameset.add s bounds
           | KOpt_kind (_, Kid_aux (Var s,_)) -> Nameset.add s bounds)
        | _ -> bounds) quants mt
  | TypQ_no_forall -> mt  

let fv_of_typschm consider_var bound used (Ast.TypSchm_aux ((Ast.TypSchm_ts(typq,typ)),_)) =
  let ts_bound = if consider_var then typq_bindings typq else mt in
  ts_bound, fv_of_typ consider_var (Nameset.union bound ts_bound) used typ

let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
  let list_fv bound used ps = List.fold_right (fun p (b,n) -> pat_bindings consider_var b n p) ps (bound, used) in
  match p with
  | P_as(p,id) -> let b,ns = pat_bindings consider_var bound used p in
    Nameset.add (string_of_id id) b,ns
  | P_typ(t,p) ->
     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     let ns = fv_of_typ consider_var bound used t in pat_bindings consider_var bound ns p
  | P_id id ->
     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     Nameset.add (string_of_id id) bound,used
  | P_app(id,pats) ->
    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
    list_fv bound (Nameset.add (string_of_id id) used) pats
  | P_record(fpats,_) ->
    List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
        pat_bindings consider_var bound used p) fpats (bound,used)
  | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
  | P_vector_indexed ipats ->
    List.fold_right (fun (_,p) (b,n) -> pat_bindings consider_var b n p) ipats (bound,used)
  | _ -> bound,used

let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.t * Nameset.t * Nameset.t) =
  let list_fv b n s es = List.fold_right (fun e (b,n,s) -> fv_of_exp consider_var b n s e) es (b,n,s) in
  match e with
  | E_block es | Ast.E_nondet es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
    list_fv bound used set es
  | E_id id ->
     let used = conditional_add_exp bound used id in
     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     bound,used,set
  | E_cast (t,e) ->
    let u = fv_of_typ consider_var (if consider_var then bound else mt) used t in
    fv_of_exp consider_var bound u set e
  | E_app(id,es) ->
    let us = conditional_add_exp bound used id in
    list_fv bound us set es
  | E_app_infix(l,id,r) ->
    let us = conditional_add_exp bound used id in
    list_fv bound us set [l;r]
  | E_if(c,t,e) -> list_fv bound used set [c;t;e]
  | E_for(id,from,to_,by,_,body) ->
    let _,used,set = list_fv bound used set [from;to_;by] in
    fv_of_exp consider_var (Nameset.add (string_of_id id) bound) used set body
  | E_vector_indexed (es_i,(Ast.Def_val_aux(default,_))) ->
    let bound,used,set =
      List.fold_right
        (fun (_,e) (b,u,s) -> fv_of_exp consider_var b u s e) es_i (bound,used,set) in
    (match default with
     | Def_val_empty -> bound,used,set
     | Def_val_dec e -> fv_of_exp consider_var bound used set e)
  | E_vector_access(v,i) -> list_fv bound used set [v;i]
  | E_vector_subrange(v,i1,i2) -> list_fv bound used set [v;i1;i2]
  | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e]
  | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e]
  | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2]
  | E_record (FES_aux(FES_Fexps(fexps,_),_)) ->
     let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     List.fold_right
       (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set)
  | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
    let b,u,s = fv_of_exp consider_var bound used set e in
    List.fold_right
      (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (b,u,s)
  | E_field(e,_) -> fv_of_exp consider_var bound used set e
  | E_case(e,pes) ->
    let b,u,s = fv_of_exp consider_var bound used set e in
    fv_of_pes consider_var b u s pes
  | E_let(lebind,e) ->
    let b,u,s = fv_of_let consider_var bound used set lebind in
    fv_of_exp consider_var b u s e
  | E_assign(lexp,e) ->
    let b,u,s = fv_of_lexp consider_var bound used set lexp in
    let _,used,set = fv_of_exp consider_var bound u s e in
    b,used,set
  | E_exit e -> fv_of_exp consider_var bound used set e
  | E_assert(c,m) -> list_fv bound used set [c;m]
  | _ -> bound,used,set

and fv_of_pes consider_var bound used set pes =
  match pes with
  | [] -> bound,used,set
  | Pat_aux(Pat_exp (p,e),_)::pes ->
    let bound_p,us_p = pat_bindings consider_var bound used p in
    let bound_e,us_e,set_e = fv_of_exp consider_var bound_p us_p set e in
    fv_of_pes consider_var bound us_e set_e pes
  | Pat_aux(Pat_when (p,g,e),_)::pes ->
    let bound_p,us_p = pat_bindings consider_var bound used p in
    let bound_g,us_g,set_g = fv_of_exp consider_var bound_p us_p set g in
    let bound_e,us_e,set_e = fv_of_exp consider_var bound_g us_g set_g e in
    fv_of_pes consider_var bound us_e set_e pes
    
and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
  | LB_val_explicit(typsch,pat,exp) ->
    let bound_t,us_t = fv_of_typschm consider_var bound used typsch in
    let bound_p, us_p = pat_bindings consider_var (Nameset.union bound bound_t) used pat in
    let _,us_e,set_e = fv_of_exp consider_var (Nameset.union bound bound_t) used set exp in
    (Nameset.union bound_t bound_p),Nameset.union us_t (Nameset.union us_p us_e),set_e
  | LB_val_implicit(pat,exp) ->
    let bound_p, us_p = pat_bindings consider_var bound used pat in
    let _,us_e,set_e = fv_of_exp consider_var bound used set exp in
    bound_p,Nameset.union us_p us_e,set_e
    
and fv_of_lexp consider_var bound used set (LEXP_aux(lexp,(_,tannot))) =
  match lexp with
  | LEXP_id id ->
    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
    let i = string_of_id id in
    if Nameset.mem i bound
    then bound, used, Nameset.add i set
    else Nameset.add i bound, Nameset.add i used, set
  | LEXP_cast(typ,id) ->
    let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
    let i = string_of_id id in
    let used_t = fv_of_typ consider_var bound used typ in
    if Nameset.mem i bound
    then bound, used_t, Nameset.add i set
    else Nameset.add i bound, Nameset.add i used_t, set
  | LEXP_tup(tups) ->
    List.fold_right (fun l (b,u,s) -> fv_of_lexp consider_var b u s l) tups (bound,used,set)
  | LEXP_memory(id,args) ->
    let (bound,used,set) =
      List.fold_right
        (fun e (b,u,s) ->
          fv_of_exp consider_var b u s e) args (bound,used,set) in
    bound,Nameset.add (string_of_id id) used,set
  | LEXP_field(lexp,_) -> fv_of_lexp consider_var bound used set lexp
  | LEXP_vector(lexp,exp) ->
    let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in
    let _,used,set = fv_of_exp consider_var bound used set exp in
    bound_l,used,set
  | LEXP_vector_range(lexp,e1,e2) ->
    let bound_l,used,set = fv_of_lexp consider_var bound used set lexp in
    let _,used,set = fv_of_exp consider_var bound used set e1 in
    let _,used,set = fv_of_exp consider_var bound used set e2 in
    bound_l,used,set

let init_env s = Nameset.singleton s

let typ_variants consider_var bound tunions =
  List.fold_right
    (fun (Tu_aux(t,_)) (b,n) -> match t with
       | Tu_id id -> Nameset.add (string_of_id id) b,n
       | Tu_ty_id(t,id) -> Nameset.add (string_of_id id) b, fv_of_typ consider_var b n t)
    tunions
    (bound,mt)

let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
  | KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
  | KD_abbrev(_,id,_,typschm) ->
    init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
  | KD_record(_,id,_,typq,tids,_) ->
    let binds = init_env (string_of_id id) in
    let bounds = if consider_var then typq_bindings typq else mt in
    binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
  | KD_variant(_,id,_,typq,tunions,_) ->
    let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
    typ_variants consider_var bindings tunions
  | KD_enum(_,id,_,ids,_) ->
    Nameset.of_list (List.map string_of_id (id::ids)),mt
  | KD_register(_,id,n1,n2,_) ->
    init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2

let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
  | TD_abbrev(id,_,typschm) -> init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
  | TD_record(id,_,typq,tids,_) ->
    let binds = init_env (string_of_id id) in
    let bounds = if consider_var then typq_bindings typq else mt in
    binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
  | TD_variant(id,_,typq,tunions,_) ->
    let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
    typ_variants consider_var bindings tunions
  | TD_enum(id,_,ids,_) ->
    Nameset.of_list (List.map string_of_id (id::ids)),mt
  | TD_register(id,n1,n2,_) ->
    init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2

let fv_of_tannot_opt consider_var (Typ_annot_opt_aux (t,_)) =
  match t with
  | Typ_annot_opt_some (typq,typ) ->
    let bindings = if consider_var then typq_bindings typq else mt in
    let free = fv_of_typ consider_var bindings mt typ in
    (bindings,free)
  | Typ_annot_opt_none ->
    (mt, mt)

(*Unlike the other fv, the bound returns are the names bound by the pattern for use in the exp*)
let fv_of_funcl consider_var base_bounds (FCL_aux(FCL_Funcl(id,pat,exp),l)) =
  let pat_bs,pat_ns = pat_bindings consider_var base_bounds mt pat in
  let _, exp_ns, exp_sets = fv_of_exp consider_var pat_bs pat_ns mt exp in
  (pat_bs,exp_ns,exp_sets)

let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_)) =
  let fun_name = match funcls with
    | [] -> failwith "fv_of_fun fell off the end looking for the function name"
    | FCL_aux(FCL_Funcl(id,_,_),_)::_ -> string_of_id id in
  let base_bounds = match rec_opt with
    | Rec_aux(Ast.Rec_rec,_) -> init_env fun_name
    | _ -> mt in
  let base_bounds,ns_r = match tannot_opt with
    | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) ->
      let bindings = if consider_var then typq_bindings typq else mt in
      let bound = Nameset.union bindings base_bounds in
      bound, fv_of_typ consider_var bound mt typ
    | Typ_annot_opt_aux(Typ_annot_opt_none, _) ->
      base_bounds, mt in
  let ns = List.fold_right (fun (FCL_aux(FCL_Funcl(_,pat,exp),_)) ns ->
      let pat_bs,pat_ns = pat_bindings consider_var base_bounds ns pat in
      let _, exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in
      exp_ns) funcls mt in
  init_env fun_name,Nameset.union ns ns_r

let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with
  | VS_val_spec(ts,id) | VS_extern_no_rename (ts,id) | VS_extern_spec(ts,id,_)
  | VS_cast_spec(ts,id) ->
     init_env ("val:" ^ (string_of_id id)), snd (fv_of_typschm consider_var mt mt ts)

let rec find_scattered_of name = function
  | [] -> []
  | DEF_scattered (SD_aux(sda,_) as sd):: defs ->
    (match sda with
     | SD_scattered_function(_,_,_,id)
     | SD_scattered_funcl(FCL_aux(FCL_Funcl(id,_,_),_))
     | SD_scattered_unioncl(id,_) ->
       if name = string_of_id id
       then [sd] else []
     | _ -> [])@
    (find_scattered_of name defs)
  | _::defs -> find_scattered_of name defs

let rec fv_of_scattered consider_var consider_scatter_as_one all_defs (SD_aux(sd,_)) = match sd with
  | SD_scattered_function(_,tannot_opt,_,id) ->
    let b,ns = (match tannot_opt with
        | Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ),_) ->
          let bindings = if consider_var then typq_bindings typq else mt in
          bindings, fv_of_typ consider_var bindings mt typ
        | Typ_annot_opt_aux(Typ_annot_opt_none, _) ->
          mt, mt) in
    init_env (string_of_id id),ns
  | SD_scattered_funcl (FCL_aux(FCL_Funcl(id,pat,exp),_)) ->
    let pat_bs,pat_ns = pat_bindings consider_var mt mt pat in
    let _,exp_ns,_ = fv_of_exp consider_var pat_bs pat_ns Nameset.empty exp in
    let scattered_binds = match pat with
      | P_aux(P_app(pid,_),_) -> init_env ((string_of_id id) ^ "/" ^ (string_of_id pid))
      | _ -> mt in
    scattered_binds, exp_ns
  | SD_scattered_variant (id,_,_) ->
    let name = string_of_id id in
    let uses =
      if consider_scatter_as_one
      then
        let variant_defs = find_scattered_of name all_defs in
        let pieces_uses =
          List.fold_right (fun (binds,uses) all_uses -> Nameset.union uses all_uses)
            (List.map (fv_of_scattered consider_var false []) variant_defs) mt in
        Nameset.remove name pieces_uses
      else mt in
    init_env name, uses
  | SD_scattered_unioncl(id, type_union) ->
    let typ_name = string_of_id id in
    let b = init_env typ_name in
    let (b,r) = typ_variants consider_var b [type_union] in
    (Nameset.remove typ_name b, Nameset.add typ_name r)
  | SD_scattered_end id ->
    let name = string_of_id id in
    let uses = if consider_scatter_as_one
    (*Note: if this is a function ending, the dec is included *)
      then
        let scattered_defs = find_scattered_of name all_defs in
        List.fold_right (fun (binds,uses) all_uses -> Nameset.union (Nameset.union binds uses) all_uses)
          (List.map (fv_of_scattered consider_var false []) scattered_defs) (init_env name)
      else init_env name in
    init_env (name ^ "/end"), uses

let fv_of_rd consider_var (DEC_aux (d,_)) = match d with
  | DEC_reg(t,id) ->
    init_env (string_of_id id), fv_of_typ consider_var mt mt t
  | DEC_alias(id,alias) ->
    init_env (string_of_id id),mt
  | DEC_typ_alias(t,id,alias) ->
    init_env (string_of_id id), mt

let fv_of_def consider_var consider_scatter_as_one all_defs = function
  | DEF_kind kdef -> fv_of_kind_def consider_var kdef
  | DEF_type tdef -> fv_of_type_def consider_var tdef
  | DEF_fundef fdef -> fv_of_fun consider_var fdef
  | DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind))
  | DEF_spec vspec -> fv_of_vspec consider_var vspec
  | DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids
  | DEF_default def -> mt,mt
  | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
  | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
  | DEF_comm _ -> mt,mt

let group_defs consider_scatter_as_one (Ast.Defs defs) =
  List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs

(*******************************************************************************
 * Reorder defs take 2
*)

(*remove all of ns1 instances from ns2*)
let remove_all ns1 ns2 =
  List.fold_right Nameset.remove (Nameset.elements ns1) ns2

let remove_from_all_uses bs dbts =
  List.map (fun ((b,uses),d) -> (b,remove_all bs uses),d) dbts

let remove_local_or_lib_vars dbts =
  let bound_in_dbts = List.fold_right (fun ((b,_),_) bounds -> Nameset.union b bounds) dbts mt in
  let is_bound_in_defs s = Nameset.mem s bound_in_dbts in
  let rec remove_from_uses = function
    | [] -> []
    | ((b,uses),d)::defs ->
      ((b,(Nameset.filter is_bound_in_defs uses)),d)::remove_from_uses defs in
  remove_from_uses dbts

let compare_dbts ((_,u1),_) ((_,u2),_) = Pervasives.compare (Nameset.cardinal u1) (Nameset.cardinal u2)

let rec print_dependencies orig_queue work_queue names =
  match work_queue with
  | [] -> ()
  | ((binds,uses),_)::wq ->
    (if not(Nameset.is_empty(Nameset.inter names binds))
     then ((Printf.eprintf "binds of %s has uses of %s\n" (set_to_string binds) (set_to_string uses));
           print_dependencies orig_queue orig_queue uses));
    print_dependencies orig_queue wq names

let rec topological_sort work_queue defs =
  match work_queue with
  | [] -> List.rev defs
  | ((binds,uses),def)::wq ->
    (*Assumes work queue given in sorted order, invariant mantained on appropriate recursive calls*)
    if (Nameset.cardinal uses = 0)
    then (*let _ = Printf.eprintf "Adding def that binds %s to definitions\n" (set_to_string binds) in*)
      topological_sort (remove_from_all_uses binds wq) (def::defs)
    else if not(Nameset.is_empty(Nameset.inter binds uses))
    then topological_sort (((binds,(remove_all binds uses)),def)::wq) defs
    else
      match List.stable_sort compare_dbts work_queue with (*We wait to sort until there are no 0 dependency nodes on top*)
      | [] -> failwith "sort shrunk the list???"
      | (((n,uses),_)::_) as wq ->
        if (Nameset.cardinal uses = 0)
        then topological_sort wq defs
        else let _ = Printf.eprintf "Uses on failure are %s, binds are %s\n" (set_to_string uses) (set_to_string n)
          in let _ = print_dependencies wq wq uses in failwith "A dependency was unmet"

let rec add_to_partial_order ((binds,uses),def) = function
  | [] ->
(*    let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n Eol case.\n" (set_to_string binds) (set_to_string uses) in*)
    [(binds,uses),def]
  | (((bf,uf),deff)::defs as full_defs) ->
    (*let _ = Printf.eprintf "add_to_partial_order for def with bindings %s, uses %s.\n None eol case. With first def binding %s, uses %s\n" (set_to_string binds) (set_to_string uses) (set_to_string bf) (set_to_string uf) in*)
    if Nameset.is_empty uses
    then ((binds,uses),def)::full_defs
    else if Nameset.subset binds uf (*deff relies on def, so def must be defined first*)
    then ((binds,uses),def)::((bf,(remove_all binds uf)),deff)::defs
    else if Nameset.subset bf uses (*def relies at least on deff, but maybe more, push in*)
    then ((bf,uf),deff)::(add_to_partial_order ((binds,(remove_all bf uses)),def) defs)
    else (*These two are unrelated but new def might need to go further in*)
      ((bf,uf),deff)::(add_to_partial_order ((binds,uses),def) defs)

let rec gather_defs name already_included def_bind_triples =
  match def_bind_triples with
  | [] -> [],already_included,mt
  | ((binds,uses),def)::def_bind_triples ->
    let (defs,already_included,requires) = gather_defs name already_included def_bind_triples in
    let bound_names = Nameset.elements binds in
    if List.mem name already_included || List.exists (fun b -> List.mem b already_included) bound_names 
    then (defs,already_included,requires)
    else
      let uses = List.fold_right Nameset.remove already_included uses in
      if Nameset.mem name binds
      then (def::defs,(bound_names@already_included), Nameset.remove name (Nameset.union uses requires))
      else (defs,already_included,requires)

let rec gather_all names already_included def_bind_triples =
  let rec gather ns already_included defs reqs = match ns with
    | [] -> defs,already_included,reqs
    | name::ns ->
      if List.mem name already_included
      then gather ns already_included defs (Nameset.remove name reqs)
      else
        let (new_defs,already_included,new_reqs) = gather_defs name already_included def_bind_triples in
        gather ns already_included (new_defs@defs) (Nameset.remove name (Nameset.union new_reqs reqs))
  in
  let (defs,already_included,reqs) = gather names already_included [] mt in
  if Nameset.is_empty reqs
  then defs
  else (gather_all (Nameset.elements reqs) already_included def_bind_triples)@defs
    
let restrict_defs defs name_list =
  let defsno = gather_all name_list [] (group_defs false defs) in
  let rdbts = group_defs true (Defs defsno) in
  (*let partial_order =
    List.fold_left (fun po d -> add_to_partial_order d po) [] rdbts in
    let defs = List.map snd partial_order in*)
  let defs = topological_sort (List.sort compare_dbts (remove_local_or_lib_vars rdbts)) [] in
  Defs defs


let top_sort_defs defs =
  let rdbts = group_defs true defs in
  let defs = topological_sort (List.stable_sort compare_dbts (remove_local_or_lib_vars rdbts)) [] in
  Defs defs