Fill out some missing cases in free variable calculation

In particular, some of these affected the topological sorting.

1 files changed, 54 insertions, 5 deletions

diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2c40b3ed..142cf6ed 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -147,6 +147,21 @@ and fv_of_nexp consider_var bound used (Ast.Nexp_aux(n,_)) = match n with
   | Nexp_exp n | Ast.Nexp_neg n -> fv_of_nexp consider_var bound used n
   | _ -> used
 
+and fv_of_nconstraint consider_var bound used (Ast.NC_aux(nc,_)) = match nc with
+  | NC_equal (n1,n2) | NC_bounded_ge (n1,n2) | NC_bounded_gt (n1, n2) | NC_bounded_le (n1,n2)
+  | NC_bounded_lt (n1,n2) | NC_not_equal (n1, n2) ->
+    fv_of_nexp consider_var bound (fv_of_nexp consider_var bound used n1) n2
+  | NC_set (Ast.Kid_aux (Ast.Var i,_), _)
+  | NC_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
+  | NC_or (nc1,nc2) | NC_and (nc1,nc2) ->
+     fv_of_nconstraint consider_var bound (fv_of_nconstraint consider_var bound used nc1) nc2
+  | NC_app (id, targs) ->
+     List.fold_right (fun ta n -> fv_of_targ consider_var bound n ta) targs (conditional_add_typ bound used id)
+  | NC_true | NC_false -> used
+
 let typq_bindings (TypQ_aux(tq,_)) = match tq with
   | TypQ_tq quants ->
     List.fold_right (fun (QI_aux (qi,_)) bounds ->
@@ -161,9 +176,27 @@ let fv_of_typschm consider_var bound used (Ast.TypSchm_aux ((Ast.TypSchm_ts(typq
   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 fv_of_typ_pat consider_var bound used (TP_aux (tp, _)) =
+  match tp with
+  | TP_wild -> bound, used
+  | TP_var (Kid_aux (Var v, l)) ->
+    Nameset.add (string_of_id (Ast.Id_aux (Ast.Id v,l))) bound, used
+  | TP_app (id, tps) ->
+     let u = conditional_add_typ bound used id in
+     List.fold_right (fun ta (b, u) -> fv_of_typ_pat consider_var b u ta) tps (bound, u)
+
 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_lit _ | P_wild -> bound,used
+  | P_or(p1,p2) ->
+    (* The typechecker currently drops bindings in disjunctions entirely *)
+    let _b1, u1 = pat_bindings consider_var bound used p1 in
+    let _b2, u2 = pat_bindings consider_var bound used p2 in
+    bound, Nameset.union u1 u2
+  | P_not p ->
+     let _b, u = pat_bindings consider_var bound used p in
+     bound, u
   | 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) ->
@@ -172,15 +205,22 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
   | P_id id ->
      let used = fv_of_tannot consider_var bound used tannot in
      Nameset.add (string_of_id id) bound,used
+  | P_var (p, typ_p) ->
+    let b, u = pat_bindings consider_var bound used p in
+    fv_of_typ_pat consider_var b u typ_p
   | P_app(id,pats) ->
      let used = fv_of_tannot consider_var bound used tannot in
     list_fv bound (Nameset.add (string_of_id id) used) pats
-  | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
-  | _ -> bound,used
+  | P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats | P_string_append pats -> list_fv bound used pats
+  | P_cons (p1,p2) ->
+    let b1, u1 = pat_bindings consider_var bound used p1 in
+    pat_bindings consider_var b1 u1 p2
 
 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_lit _
+  | E_internal_value _ -> bound,used,set
   | E_block es | Ast.E_tuple es | Ast.E_vector es | Ast.E_list es ->
     list_fv bound used set es
   | E_id id | E_ref id ->
@@ -219,7 +259,8 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     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) ->
+  | E_case(e,pes)
+  | E_try(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) ->
@@ -235,8 +276,16 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     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]
-  | E_return e -> fv_of_exp consider_var bound used set e
-  | _ -> bound,used,set
+  | E_sizeof ne -> bound, fv_of_nexp consider_var bound used ne, set
+  | E_return e
+  | E_throw e
+  | E_internal_return e ->
+     fv_of_exp consider_var bound used set e
+  | E_internal_plet (pat, exp1, exp2) ->
+     let bp,up = pat_bindings consider_var bound used pat in
+     let _,u1,s1 = fv_of_exp consider_var bound used set exp1 in
+     fv_of_exp consider_var bp (Nameset.union up u1) s1 exp2
+  | E_constraint nc -> bound, fv_of_nconstraint consider_var bound used nc, set
 
 and fv_of_pes consider_var bound used set pes =
   match pes with