diff options
| -rw-r--r-- | editors/sail.el | 16 | ||||
| -rw-r--r-- | src/pretty_print.ml | 6 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
4 files changed, 26 insertions, 1 deletions
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 |