Add free variable and dependency sorting functions, lifted from internal to external repository

2 files changed, 460 insertions, 0 deletions

diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 278243b8..ca005b4b 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -5,6 +5,16 @@ open Type_internal
 
 type typ = Type_internal.t
 
+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
@@ -132,3 +142,441 @@ let is_within_range candidate range constraints =
 
 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 id_to_string (Ast.Id_aux (i,_)) = match i with
+  | Ast.Id s | Ast.DeIid s -> s
+
+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"]
+    else ["=="; "!="; "|";"~";"&";"add_int"] in
+  let i = (id_to_string 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 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,_)) =
+  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 (id_to_string id) b,ns
+  | P_typ(t,p) -> let ns = fv_of_typ consider_var bound used t in pat_bindings consider_var bound ns p
+  | P_id id -> Nameset.add (id_to_string id) bound,used
+  | P_app(id,pats) ->
+    list_fv bound (Nameset.add (id_to_string 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,_)) : (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 -> bound,conditional_add_exp bound used id,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 (id_to_string 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,_),_)) ->
+    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,_)) =
+  match lexp with
+  | LEXP_id id ->
+    let i = id_to_string 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 i = id_to_string 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 (id_to_string 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 (id_to_string id) b,n
+       | Tu_ty_id(t,id) -> Nameset.add (id_to_string 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 (id_to_string id), fv_of_nexp consider_var mt mt nexp
+  | KD_abbrev(_,id,_,typschm) ->
+    init_env (id_to_string id), snd (fv_of_typschm consider_var mt mt typschm)
+  | KD_record(_,id,_,typq,tids,_) ->
+    let binds = init_env (id_to_string 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 (id_to_string 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 id_to_string (id::ids)),mt
+  | KD_register(_,id,n1,n2,_) ->
+    init_env (id_to_string 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 (id_to_string id), snd (fv_of_typschm consider_var mt mt typschm)
+  | TD_record(id,_,typq,tids,_) ->
+    let binds = init_env (id_to_string 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 (id_to_string 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 id_to_string (id::ids)),mt
+  | TD_register(id,n1,n2,_) ->
+    init_env (id_to_string 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)  
+
+(*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,_,_),_)::_ -> id_to_string 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 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,_)->
+    init_env (id_to_string 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 = id_to_string 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) in
+    init_env (id_to_string 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 ((id_to_string id) ^ "/" ^ (id_to_string pid))
+      | _ -> mt in
+    scattered_binds, exp_ns
+  | SD_scattered_variant (id,_,_) ->
+    let name = id_to_string 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 = id_to_string 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 = id_to_string 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 (id_to_string id), fv_of_typ consider_var mt mt t
+  | DEC_alias(id,alias) ->
+    init_env (id_to_string id),mt
+  | DEC_typ_alias(t,id,alias) ->
+    init_env (id_to_string 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_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.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
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 731bd822..6aeb711b 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -18,3 +18,15 @@ val default_order : tannot defs -> order
 *)
 val is_within_range: typ -> typ -> nexp_range list -> triple
 val is_within_machine64 : typ -> nexp_range list -> triple
+
+(* free variables and dependencies *)
+
+(*fv_of_def consider_ty_vars consider_scatter_as_one all_defs all_defs def -> (bound_by_def, free_in_def) *)
+val fv_of_def: bool -> bool -> (tannot def) list -> tannot def -> Nameset.t * Nameset.t
+
+(*group_defs consider_scatter_as_one all_defs -> ((bound_by_def, free_in_def), def) list *)
+val group_defs : bool -> tannot defs -> ((Nameset.t * Nameset.t) * (tannot def)) list
+
+(*reodering definitions, initial functions *)
+(* produce a new ordering for defs, limiting to those listed in the list, which respects dependencies *)
+val restrict_defs : tannot defs -> string list -> tannot defs