Support extracting length information into more functions

1 files changed, 14 insertions, 2 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index c500beb1..b0fdb2dc 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -383,7 +383,14 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
 	  | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" 
 	                               kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e))
           | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
-        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector"))
+	| Tapp("implicit",[TA_nexp r]) ->
+	  (match r.nexp with
+	    | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" 
+	                               kwd (string_of_big_int bi) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e))
+	    | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id %a) %a)) (%a,%a))@]"
+	                             kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e))
+	    | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const"))
+        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit"))
     | E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ ->  raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload")
   in
   print_e ppf e
@@ -906,7 +913,12 @@ let doc_exp, doc_let =
 	(match r.nexp with
 	  | Nconst bi -> utf8string (Big_int.string_of_big_int bi)
           | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length"))
-        | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector"))
+      | Tapp("implicit",[TA_nexp r]) ->
+	(match r.nexp with
+	  | Nconst bi -> utf8string (Big_int.string_of_big_int bi)
+	  | Nvar v -> utf8string v
+	  | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const"))
+      | _ ->  raise (Reporting_basic.err_unreachable l "Internal exp given non-vector, non-implicit"))
 
   (* XXX missing case
      AAA internal_cast should never have an overload, if it's been seen it's a bug *)