make sail-to-lem rewriting passes use dependency analysis, make dependency analysis include type information, small pp fix

4 files changed, 72 insertions, 15 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 0cc9e679..d53ee417 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2260,7 +2260,10 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
      | _ -> empty)
   | P_lit lit  -> doc_lit_lem true lit annot
   | P_wild -> underscore
-  | P_id id -> doc_id_lem id
+  | P_id id ->
+     begin match id with 
+     | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
+     | _ -> doc_id_lem id end
   | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ) 
   | P_vector pats ->
@@ -2389,7 +2392,6 @@ let doc_exp_lem, doc_let_lem =
            let [e1;e2] = args in
            let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
            if aexp_needed then parens (align epp) else epp
-        | Id_aux (Id "None",_) -> string "Nothing"
         | _ ->
            (match annot with
             | Base (_,Constructor _,_,_,_,_) ->
@@ -2643,7 +2645,8 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> separate space [string "exit"; expY e;]
     | E_assert (e1,e2) ->
-       separate space [string "assert'"; expY e1; expY e2]
+       let epp = separate space [string "assert'"; expY e1; expY e2] in
+       if aexp_needed then parens (align epp) else align epp
     | E_app_infix (e1,id,e2) ->
        (match annot with
         | Base((_,t),External(Some name),_,_,_,_) ->
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 155cfe2e..de551b6a 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2096,7 +2096,8 @@ let rewrite_defs_remove_e_assign =
     }
 
 
-let rewrite_defs_lem  =
+let rewrite_defs_lem =
+  top_sort_defs >>
   rewrite_defs_remove_vector_concat >>
   rewrite_defs_exp_lift_assign >> 
   rewrite_defs_remove_blocks >> 
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index ca005b4b..bddeb28c 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -151,7 +151,7 @@ let id_to_string (Ast.Id_aux (i,_)) = match i with
 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"]
+    then ["bit";"vector";"unit";"string";"int";"bool";"boolean"]
     else ["=="; "!="; "|";"~";"&";"add_int"] in
   let i = (id_to_string id) in
   if Nameset.mem i bound || List.mem i  known_list
@@ -161,6 +161,40 @@ let conditional_add typ_or_exp bound used id =
 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 {t = t} = match t with
+  | Tvar name -> if consider_var then Nameset.add name mt else mt
+  | Tid name -> Nameset.add name mt
+  | Tfn (t1,t2,_,_) -> Nameset.union (free_type_names_t consider_var t1)
+                                     (free_type_names_t consider_var t2)
+  | Ttup ts -> free_type_names_ts consider_var ts
+  | Tapp (name,targs) -> Nameset.add name (free_type_names_t_args consider_var targs)
+  | Tabbrev (t1,t2) -> Nameset.union (free_type_names_t consider_var t1)
+                                     (free_type_names_t consider_var t2)
+  | Toptions (t,m_t) -> Nameset.union (free_type_names_t consider_var t)
+                                      (free_type_names_maybe_t consider_var m_t)
+  | Tuvar _ -> 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
+  | TA_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
+  | NoTyp -> mt
+  | Base ((_,t),_ ,_,_,_,_) -> free_type_names_t consider_var t
+  | Overload (tannot,_,tannots) ->
+     nameset_bigunion (List.map (free_type_names_tannot consider_var) (tannot :: tannots))
+
+
 let rec fv_of_typ consider_var bound used (Typ_aux (t,_)) : Nameset.t =
   match t with
   | Typ_wild -> used
@@ -205,14 +239,19 @@ 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 pat_bindings consider_var bound used (P_aux(p,_)) =
+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 (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_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 (id_to_string 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 (id_to_string id) used) pats    
   | P_record(fpats,_) ->
     List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
@@ -222,12 +261,15 @@ let rec pat_bindings consider_var bound used (P_aux(p,_)) =
     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 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 -> bound,conditional_add_exp bound used id,set
+  | 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
@@ -254,8 +296,9 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,_)) : (Nameset.t * Names
   | 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)
+     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
@@ -294,14 +337,16 @@ and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
     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,_)) =
+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 = 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 used = Nameset.union (free_type_names_tannot consider_var tannot) used in
     let i = id_to_string id in
     let used_t = fv_of_typ consider_var bound used typ in
     if Nameset.mem i bound
@@ -399,7 +444,7 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_))
 
 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)
+     init_env ("val:" ^ (id_to_string id)), snd (fv_of_typschm consider_var mt mt ts)
 
 let rec find_scattered_of name = function
   | [] -> []
@@ -520,7 +565,7 @@ let rec topological_sort work_queue 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*)
+      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)
@@ -580,3 +625,9 @@ let restrict_defs defs name_list =
     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
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 6aeb711b..068b3778 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -30,3 +30,5 @@ val group_defs : bool -> tannot defs -> ((Nameset.t * Nameset.t) * (tannot def))
 (*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
+
+val top_sort_defs : tannot defs -> tannot defs