Better lem_ast tagging and interpreter tweaks

3 files changed, 21 insertions, 36 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 68f82ccb..e9533a2a 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -440,7 +440,8 @@ let rec interp_to_value_helper debug arg ivh_mode err_str instr direction regist
       (Ivh_error (Interp_interface.Internal_error ("Write memory value request in a " ^ errk_str)), events_out)
     | (Interp.Action (Interp.Write_memv_tagged _ _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Write memory value tagged request in a " ^ errk_str)), events_out)
-    | _ -> (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str)), events_out)
+    | (outcome, _, _) ->
+       (Ivh_error (Interp_interface.Internal_error ("Non expected action in a " ^ errk_str ^ " " ^ Interp.string_of_outcome outcome)), events_out)
 end
 
 let call_external_functions direction outcome = 
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 6978aeb9..81f0a5fd 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -433,7 +433,7 @@ let run
               (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
           show "nondeterministic evaluation begun" "" "" "";
           let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
               choose_order (false,mode,!track_dependencies,env'); in
           show "nondeterministic evaluation ended" "" "" "";
           (step next,env',next)
@@ -445,7 +445,7 @@ let run
           else begin
             show "undefined triggered a non_det" "" "" "";
             let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies true) next))
               choose_order (false,mode,!track_dependencies,env'); in
             (step i_state,env',i_state) end
         | Escape0(Some e,_) ->
@@ -462,11 +462,11 @@ let run
         | Write_memv1 _ -> assert false)
         (*| _ -> assert false*)
       in
-      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) next) in
+      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies true) next) in
   let mode = match mode with
   | None -> if eager_eval then Run else Step
   | Some m -> m in
-  let imode = make_mode eager_eval !track_dependencies false in
+  let imode = make_mode eager_eval !track_dependencies true in
   let (IState(instr_state,context)) = istate in
   let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
   interactf "%s: %s %s\n" (grey name) (blue "evaluate") 
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 65d99780..65fa5d25 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -281,45 +281,28 @@ let pp_format_lit_lem (L_aux(lit,l)) =
 let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
 
 
-let rec pp_format_nes nes =
-  "[" ^ (*
-  (list_format "; "
-     (fun ne -> match ne with
-       | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
-       | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
-       | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")"
-       | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) ->
-         "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])"
-       | InS(_,_,ns)  ->
-         "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"
-       | CondCons(_,nes_c,nes_t) ->
-         "(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"
-       | BranchCons(_,nes_b) ->
-         "(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"
-     )
-     nes) ^*) "]"
-
-let pp_format_annot = function
+let tag_id id env =
+  if Env.is_extern id env "lem_ast" then
+    "Tag_extern (Just \"" ^ Ast_util.string_of_id id ^ "\")"
+  else if Env.is_union_constructor id env then
+    "Tag_ctor"
+  else
+    "Tag_empty"
+
+let pp_format_annot ?tag:(t="Tag_empty") = function
   | None -> "Nothing"
   | Some (_, typ, eff) ->
      "(Just ("
      ^ pp_format_typ_lem typ ^ ", "
-     ^ "Tag_empty" ^ ", "
+     ^ t ^ ", "
      ^ "[], "
      ^ pp_format_effects_lem eff ^ ", "
      ^ pp_format_effects_lem eff
      ^ "))"
 
-(*
-  | NoTyp -> "Nothing"
-  | Base((_,t),tag,nes,efct,efctsum,_) ->
-    (*TODO print out bindings for use in pattern match in interpreter*)
-     "(Just (" ^ pp_format_t_lem t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^
-       pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))"
-  | Overload _ -> "Nothing" *)
-
 let pp_annot ppf ant = base ppf (pp_format_annot ant)
 
+let pp_annot_tag tag ppf ant = base ppf (pp_format_annot ~tag:tag ant)
 
 let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
   "(P_aux " ^
@@ -352,7 +335,8 @@ let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
         fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val" pp_lem_pat pat  pp_lem_exp exp in
   fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
 
-and pp_lem_exp ppf (E_aux(e,(l,annot))) =
+and pp_lem_exp ppf (E_aux(e,(l,annot)) as exp) =
+  let env = env_of exp in
   let print_e ppf e =
     match e with
     | E_block(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]"
@@ -363,13 +347,13 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
       kwd "(E_nondet"
       (list_pp pp_semi_lem_exp pp_lem_exp) exps
       kwd ")" pp_lem_l l pp_annot annot
-    | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot
+    | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l (pp_annot_tag (tag_id id env)) annot
     | E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot
     | E_cast(typ,exp) ->
       fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot
     | E_internal_cast((_,None),e) -> pp_lem_exp ppf e
     | E_app(f,args) -> fprintf ppf "@[<0>(E_aux (E_app %a [%a]) (%a, %a))@]"
-                         pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l pp_annot annot
+                         pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l (pp_annot_tag (tag_id f env)) annot
     | E_app_infix(l',op,r) -> fprintf ppf "@[<0>(E_aux (E_app_infix %a %a %a) (%a, %a))@]"
                                 pp_lem_exp l' pp_lem_id op pp_lem_exp r pp_lem_l l pp_annot annot
     | E_tuple(exps) -> fprintf ppf "@[<0>(E_aux (E_tuple [%a]) (%a, %a))@]"