Switch to new typechecker (almost)

Initial typecheck still uses previous typechecker

1 files changed, 0 insertions, 673 deletions

diff --git a/src/spec_analysis_new_tc.ml b/src/spec_analysis_new_tc.ml
deleted file mode 100644
index 10eb16f7..00000000
--- a/src/spec_analysis_new_tc.ml
+++ /dev/null
@@ -1,673 +0,0 @@
-(**************************************************************************)
-(*     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
-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)
-
-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
-    
-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