diff options
| author | Kathy Gray | 2014-09-09 14:21:30 +0100 |
|---|---|---|
| committer | Kathy Gray | 2014-09-09 14:21:30 +0100 |
| commit | d7f2ad0285fb20cf7c96cccffafdaa22211239c1 (patch) | |
| tree | 887d415d0614eecab0c2b0517b630149da4ad68c /src | |
| parent | 9760b76fde4184b1ff376b347e09fc936dc9bf59 (diff) | |
Get more constraints resolving in power.sail
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print.ml | 6 | ||||
| -rw-r--r-- | src/type_internal.ml | 4 | ||||
| -rw-r--r-- | src/type_internal.mli | 1 |
3 files changed, 10 insertions, 1 deletions
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 |