From d7f2ad0285fb20cf7c96cccffafdaa22211239c1 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Tue, 9 Sep 2014 14:21:30 +0100
Subject: Get more constraints resolving in power.sail

---
 editors/sail.el       | 16 ++++++++++++++++
 src/pretty_print.ml   |  6 +++++-
 src/type_internal.ml  |  4 ++++
 src/type_internal.mli |  1 +
 4 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/editors/sail.el b/editors/sail.el
index a9963558..da13c695 100644
--- a/editors/sail.el
+++ b/editors/sail.el
@@ -1694,6 +1694,22 @@ reindent the line."
     (and electric
          (indent-according-to-mode))))
 
+(defun sail-electric-lt ()
+  "If inserting a > operator or a comment-end at beginning of line,
+reindent the line."
+  (interactive "*")
+  (let ((electric (and sail-electric-indent
+                       (or (sail-in-indentation-p)
+                           (char-equal ?* (preceding-char)))
+                       (not (sail-in-literal-p))
+                       (or (not (sail-in-comment-p))
+                           (save-excursion
+                             (back-to-indentation)
+                             (looking-at "\\*"))))))
+    (self-insert-command 1)
+    (and electric
+         (indent-according-to-mode))))
+
 (defun sail-electric-rc ()
   "If inserting a } operator at beginning of line, reindent the line."
   (interactive "*")
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index b0fdb2dc..714112ad 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -382,6 +382,8 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
 	  (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 vector without known length"))
 	| Tapp("implicit",[TA_nexp r]) ->
 	  (match r.nexp with
@@ -911,8 +913,10 @@ let doc_exp, doc_let =
     (match t.t with
       | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) ->
 	(match r.nexp with
+	  | Nvar v -> utf8string v
 	  | 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 vector without known length, instead given " ^ n_to_string r)))
       | Tapp("implicit",[TA_nexp r]) ->
 	(match r.nexp with
 	  | Nconst bi -> utf8string (Big_int.string_of_big_int bi)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index c4f009ac..dcbfd0fd 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -995,6 +995,10 @@ let initial_typ_env =
                                    (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))),
                     External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e)]));
     (* incorrect types for typechecking processed sail code; do we care? *)
+    ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]),
+		     (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m"))
+			          (mk_range (mk_nv "m") {nexp = Nconst zero}))),
+		    External (Some "length"),[],pure_e));
     ("to_num_inc",Base(([("a",{k=K_Typ})],({t= Tfn ({t=Tvar "a"},nat_typ,IP_length,pure_e)})),External None,[],pure_e));
     ("to_num_dec",Base(([("a",{k=K_Typ})],{t= Tfn ({t=Tvar "a"},nat_typ,IP_length,pure_e)}),External None,[],pure_e));
     ("mask",Base(((mk_typ_params ["a"])@(mk_nat_params["n";"m";"o";"p"])@(mk_ord_params["ord"]),
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 59fd7d87..63a18106 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -140,6 +140,7 @@ val bit_t : t
 val pure_e : effect
 
 val t_to_string : t -> string
+val n_to_string : nexp -> string
 val tannot_to_string : tannot -> string
 val t_to_typ : t -> Ast.typ
 
-- 
cgit v1.2.3