summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-10-04 11:37:28 +0100
committerAlasdair Armstrong2017-10-04 11:37:28 +0100
commita41d08d4f33f778eee98aa4094eaa4f94fc134c0 (patch)
tree94a07f1d1d8d70ec7ccf5e30528af809664f02d2 /src
parent34981979b4fac0e97e0e124616a3a36aa96ee6af (diff)
parentce905a7bd4b6a25f784f94fd926f818e8827d295 (diff)
Merge branch 'cleanup' into experiments
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml23
-rw-r--r--src/ast_util.ml25
-rw-r--r--src/ast_util.mli1
-rw-r--r--src/initial_check.ml141
-rw-r--r--src/monomorphise.ml36
-rw-r--r--src/ocaml_backend.ml8
-rw-r--r--src/parse_ast.ml21
-rw-r--r--src/parser.mly67
-rw-r--r--src/parser2.mly21
-rw-r--r--src/pretty_print_common.ml4
-rw-r--r--src/pretty_print_lem.ml72
-rw-r--r--src/pretty_print_lem_ast.ml61
-rw-r--r--src/pretty_print_ocaml.ml92
-rw-r--r--src/pretty_print_sail.ml65
-rw-r--r--src/rewriter.ml227
-rw-r--r--src/rewriter.mli7
-rw-r--r--src/sail.ml9
-rw-r--r--src/spec_analysis.ml32
-rw-r--r--src/type_check.ml118
19 files changed, 241 insertions, 789 deletions
diff --git a/src/ast.ml b/src/ast.ml
index 1728f492..7d29da93 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -168,11 +168,11 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
type
n_constraint_aux = (* constraint over kind $_$ *)
- NC_fixed of nexp * nexp
+ NC_equal of nexp * nexp
| NC_bounded_ge of nexp * nexp
| NC_bounded_le of nexp * nexp
| NC_not_equal of nexp * nexp
- | NC_nat_set_bounded of kid * (int) list
+ | NC_set of kid * (int) list
| NC_or of n_constraint * n_constraint
| NC_and of n_constraint * n_constraint
| NC_true
@@ -260,11 +260,10 @@ type
| P_as of 'a pat * id (* named pattern *)
| P_typ of typ * 'a pat (* typed pattern *)
| P_id of id (* identifier *)
- | P_var of kid (* bind identifier and type variable *)
+ | P_var of 'a pat * kid (* bind pattern to type variable *)
| P_app of id * ('a pat) list (* union constructor pattern *)
| P_record of ('a fpat) list * bool (* struct pattern *)
| P_vector of ('a pat) list (* vector pattern *)
- | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *)
| P_vector_concat of ('a pat) list (* concatenated vector pattern *)
| P_tup of ('a pat) list (* tuple pattern *)
| P_list of ('a pat) list (* list pattern *)
@@ -305,7 +304,6 @@ type
| E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* for loop *)
| E_loop of loop * 'a exp * 'a exp
| E_vector of ('a exp) list (* vector (indexed from 0) *)
- | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *)
| E_vector_access of 'a exp * 'a exp (* vector access *)
| E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *)
| E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *)
@@ -378,8 +376,7 @@ and 'a pexp =
Pat_aux of 'a pexp_aux * 'a annot
and 'a letbind_aux = (* Let binding *)
- LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+ LB_val of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
and 'a letbind =
LB_aux of 'a letbind_aux * 'a annot
@@ -495,21 +492,11 @@ type_def_aux = (* Type definition body *)
type
val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
- | VS_cast_spec of typschm * id
-
+ VS_val_spec of typschm * id * string option * bool
type
'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *)
KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
- | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
- | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
type
'a scattered_def_aux = (* Function and type union definitions that can be spread across
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 048fbb15..ecff4ff4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -61,6 +61,7 @@ let mk_exp exp_aux = E_aux (exp_aux, no_annot)
let unaux_exp (E_aux (exp_aux, _)) = exp_aux
let mk_pat pat_aux = P_aux (pat_aux, no_annot)
+let unaux_pat (P_aux (pat_aux, _)) = pat_aux
let mk_lexp lexp_aux = LEXP_aux (lexp_aux, no_annot)
@@ -85,7 +86,7 @@ let mk_fundef funcls =
DEF_fundef
(FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
-let mk_letbind pat exp = LB_aux (LB_val_implicit (pat, exp), no_annot)
+let mk_letbind pat exp = LB_aux (LB_val (pat, exp), no_annot)
let mk_val_spec vs_aux =
DEF_spec (VS_aux (vs_aux, no_annot))
@@ -183,8 +184,8 @@ let npow2 n = Nexp_aux (Nexp_exp n, Parse_ast.Unknown)
let nvar kid = Nexp_aux (Nexp_var kid, Parse_ast.Unknown)
let nid id = Nexp_aux (Nexp_id id, Parse_ast.Unknown)
-let nc_set kid ints = mk_nc (NC_nat_set_bounded (kid, ints))
-let nc_eq n1 n2 = mk_nc (NC_fixed (n1, n2))
+let nc_set kid ints = mk_nc (NC_set (kid, ints))
+let nc_eq n1 n2 = mk_nc (NC_equal (n1, n2))
let nc_neq n1 n2 = mk_nc (NC_not_equal (n1, n2))
let nc_lteq n1 n2 = NC_aux (NC_bounded_le (n1, n2), Parse_ast.Unknown)
let nc_gteq n1 n2 = NC_aux (NC_bounded_ge (n1, n2), Parse_ast.Unknown)
@@ -223,8 +224,6 @@ and map_exp_annot_aux f = function
| E_for (v, e1, e2, e3, o, e4) -> E_for (v, map_exp_annot f e1, map_exp_annot f e2, map_exp_annot f e3, o, map_exp_annot f e4)
| E_loop (loop_type, e1, e2) -> E_loop (loop_type, map_exp_annot f e1, map_exp_annot f e2)
| E_vector exps -> E_vector (List.map (map_exp_annot f) exps)
- | E_vector_indexed (iexps, opt_default) ->
- E_vector_indexed (List.map (fun (i, exp) -> (i, map_exp_annot f exp)) iexps, map_opt_default_annot f opt_default)
| E_vector_access (exp1, exp2) -> E_vector_access (map_exp_annot f exp1, map_exp_annot f exp2)
| E_vector_subrange (exp1, exp2, exp3) -> E_vector_subrange (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3)
| E_vector_update (exp1, exp2, exp3) -> E_vector_update (map_exp_annot f exp1, map_exp_annot f exp2, map_exp_annot f exp3)
@@ -272,20 +271,18 @@ and map_pat_annot_aux f = function
| P_as (pat, id) -> P_as (map_pat_annot f pat, id)
| P_typ (typ, pat) -> P_typ (typ, map_pat_annot f pat)
| P_id id -> P_id id
- | P_var kid -> P_var kid
+ | P_var (pat, kid) -> P_var (map_pat_annot f pat, kid)
| P_app (id, pats) -> P_app (id, List.map (map_pat_annot f) pats)
| P_record (fpats, b) -> P_record (List.map (map_fpat_annot f) fpats, b)
| P_tup pats -> P_tup (List.map (map_pat_annot f) pats)
| P_list pats -> P_list (List.map (map_pat_annot f) pats)
| P_vector_concat pats -> P_vector_concat (List.map (map_pat_annot f) pats)
- | P_vector_indexed ipats -> P_vector_indexed (List.map (fun (i, pat) -> (i, map_pat_annot f pat)) ipats)
| P_vector pats -> P_vector (List.map (map_pat_annot f) pats)
| P_cons (pat1, pat2) -> P_cons (map_pat_annot f pat1, map_pat_annot f pat2)
and map_fpat_annot f (FP_aux (FP_Fpat (id, pat), annot)) = FP_aux (FP_Fpat (id, map_pat_annot f pat), f annot)
and map_letbind_annot f (LB_aux (lb, annot)) = LB_aux (map_letbind_annot_aux f lb, f annot)
and map_letbind_annot_aux f = function
- | LB_val_explicit (typschm, pat, exp) -> LB_val_explicit (typschm, map_pat_annot f pat, map_exp_annot f exp)
- | LB_val_implicit (pat, exp) -> LB_val_implicit (map_pat_annot f pat, map_exp_annot f exp)
+ | LB_val (pat, exp) -> LB_val (map_pat_annot f pat, map_exp_annot f exp)
and map_lexp_annot f (LEXP_aux (lexp, annot)) = LEXP_aux (map_lexp_annot_aux f lexp, f annot)
and map_lexp_annot_aux f = function
| LEXP_id id -> LEXP_id id
@@ -395,7 +392,7 @@ and string_of_typ_arg_aux = function
| Typ_arg_typ typ -> string_of_typ typ
| Typ_arg_order o -> string_of_order o
and string_of_n_constraint = function
- | NC_aux (NC_fixed (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
+ | NC_aux (NC_equal (n1, n2), _) -> string_of_nexp n1 ^ " = " ^ string_of_nexp n2
| NC_aux (NC_not_equal (n1, n2), _) -> string_of_nexp n1 ^ " != " ^ string_of_nexp n2
| NC_aux (NC_bounded_ge (n1, n2), _) -> string_of_nexp n1 ^ " >= " ^ string_of_nexp n2
| NC_aux (NC_bounded_le (n1, n2), _) -> string_of_nexp n1 ^ " <= " ^ string_of_nexp n2
@@ -403,7 +400,7 @@ and string_of_n_constraint = function
"(" ^ string_of_n_constraint nc1 ^ " | " ^ string_of_n_constraint nc2 ^ ")"
| NC_aux (NC_and (nc1, nc2), _) ->
"(" ^ string_of_n_constraint nc1 ^ " & " ^ string_of_n_constraint nc2 ^ ")"
- | NC_aux (NC_nat_set_bounded (kid, ns), _) ->
+ | NC_aux (NC_set (kid, ns), _) ->
string_of_kid kid ^ " IN {" ^ string_of_list ", " string_of_int ns ^ "}"
| NC_aux (NC_true, _) -> "true"
| NC_aux (NC_false, _) -> "false"
@@ -509,7 +506,7 @@ and string_of_pat (P_aux (pat, l)) =
| P_lit lit -> string_of_lit lit
| P_wild -> "_"
| P_id v -> string_of_id v
- | P_var kid -> string_of_kid kid
+ | P_var (pat, kid) -> string_of_pat pat ^ " as " ^ string_of_kid kid
| P_typ (typ, pat) -> "(" ^ string_of_typ typ ^ ") " ^ string_of_pat pat
| P_tup pats -> "(" ^ string_of_list ", " string_of_pat pats ^ ")"
| P_app (f, pats) -> string_of_id f ^ "(" ^ string_of_list ", " string_of_pat pats ^ ")"
@@ -532,9 +529,7 @@ and string_of_lexp (LEXP_aux (lexp, _)) =
| _ -> "LEXP"
and string_of_letbind (LB_aux (lb, l)) =
match lb with
- | LB_val_implicit (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
- | LB_val_explicit (typschm, pat, exp) ->
- string_of_typschm typschm ^ " " ^ string_of_pat pat ^ " = " ^ string_of_exp exp
+ | LB_val (pat, exp) -> string_of_pat pat ^ " = " ^ string_of_exp exp
let rec string_of_index_range (BF_aux (ir, _)) =
match ir with
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 33d65ede..18223f4a 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -67,6 +67,7 @@ val mk_fexps : (unit fexp) list -> unit fexps
val mk_letbind : unit pat -> unit exp -> unit letbind
val unaux_exp : 'a exp -> 'a exp_aux
+val unaux_pat : 'a pat -> 'a pat_aux
val inc_ord : order
val dec_ord : order
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 83c79646..b7505391 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -311,10 +311,10 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
match c with
| Parse_ast.NC_aux(nc,l) ->
NC_aux( (match nc with
- | Parse_ast.NC_fixed(t1,t2) ->
+ | Parse_ast.NC_equal(t1,t2) ->
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
- NC_fixed(n1,n2)
+ NC_equal(n1,n2)
| Parse_ast.NC_not_equal(t1,t2) ->
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
@@ -327,8 +327,8 @@ and to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint)
let n1 = to_ast_nexp k_env t1 in
let n2 = to_ast_nexp k_env t2 in
NC_bounded_le(n1,n2)
- | Parse_ast.NC_nat_set_bounded(id,bounds) ->
- NC_nat_set_bounded(to_ast_var id, bounds)
+ | Parse_ast.NC_set(id,bounds) ->
+ NC_set(to_ast_var id, bounds)
| Parse_ast.NC_or (nc1, nc2) ->
NC_or (to_ast_nexp_constraint k_env nc1, to_ast_nexp_constraint k_env nc2)
| Parse_ast.NC_and (nc1, nc2) ->
@@ -418,7 +418,7 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
| Parse_ast.P_as(pat,id) -> P_as(to_ast_pat k_env def_ord pat,to_ast_id id)
| Parse_ast.P_typ(typ,pat) -> P_typ(to_ast_typ k_env def_ord typ,to_ast_pat k_env def_ord pat)
| Parse_ast.P_id(id) -> P_id(to_ast_id id)
- | Parse_ast.P_var kid -> P_var (to_ast_var kid)
+ | Parse_ast.P_var (pat, kid) -> P_var (to_ast_pat k_env def_ord pat, to_ast_var kid)
| Parse_ast.P_app(id,pats) ->
if pats = []
then P_id (to_ast_id id)
@@ -429,7 +429,6 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
FP_aux(FP_Fpat(to_ast_id id, to_ast_pat k_env def_ord fp),(l,())))
fpats, false)
| Parse_ast.P_vector(pats) -> P_vector(List.map (to_ast_pat k_env def_ord) pats)
- | Parse_ast.P_vector_indexed(ipats) -> P_vector_indexed(List.map (fun (i,pat) -> i,to_ast_pat k_env def_ord pat) ipats)
| Parse_ast.P_vector_concat(pats) -> P_vector_concat(List.map (to_ast_pat k_env def_ord) pats)
| Parse_ast.P_tup(pats) -> P_tup(List.map (to_ast_pat k_env def_ord) pats)
| Parse_ast.P_list(pats) -> P_list(List.map (to_ast_pat k_env def_ord) pats)
@@ -440,11 +439,8 @@ let rec to_ast_pat (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.P_aux(pa
let rec to_ast_letbind (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.LB_aux(lb,l) : Parse_ast.letbind) : unit letbind =
LB_aux(
(match lb with
- | Parse_ast.LB_val_explicit(typschm,pat,exp) ->
- let typsch, k_env, _ = to_ast_typschm k_env def_ord typschm in
- LB_val_explicit(typsch,to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
- | Parse_ast.LB_val_implicit(pat,exp) ->
- LB_val_implicit(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
+ | Parse_ast.LB_val(pat,exp) ->
+ LB_val(to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp)
), (l,()))
and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) : unit exp =
@@ -470,21 +466,9 @@ and to_ast_exp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l)
| Parse_ast.E_for(id,e1,e2,e3,atyp,e4) ->
E_for(to_ast_id id,to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2,
to_ast_exp k_env def_ord e3,to_ast_order k_env def_ord atyp, to_ast_exp k_env def_ord e4)
- | Parse_ast.E_loop(Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
- | Parse_ast.E_loop(Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
- | Parse_ast.E_vector(exps) ->
- (match to_ast_iexps false k_env def_ord exps with
- | Some([]) -> E_vector([])
- | Some(iexps) -> E_vector_indexed(iexps,
- Def_val_aux(Def_val_empty,(l,())))
- | None -> E_vector(List.map (to_ast_exp k_env def_ord) exps))
- | Parse_ast.E_vector_indexed(iexps,Parse_ast.Def_val_aux(default,dl)) ->
- (match to_ast_iexps true k_env def_ord iexps with
- | Some(iexps) -> E_vector_indexed (iexps,
- Def_val_aux((match default with
- | Parse_ast.Def_val_empty -> Def_val_empty
- | Parse_ast.Def_val_dec e -> Def_val_dec (to_ast_exp k_env def_ord e)),(dl,())))
- | _ -> raise (Reporting_basic.err_unreachable l "to_ast_iexps didn't throw error"))
+ | Parse_ast.E_loop (Parse_ast.While, e1, e2) -> E_loop (While, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
+ | Parse_ast.E_loop (Parse_ast.Until, e1, e2) -> E_loop (Until, to_ast_exp k_env def_ord e1, to_ast_exp k_env def_ord e2)
+ | Parse_ast.E_vector(exps) -> E_vector(List.map (to_ast_exp k_env def_ord) exps)
| Parse_ast.E_vector_access(vexp,exp) -> E_vector_access(to_ast_exp k_env def_ord vexp, to_ast_exp k_env def_ord exp)
| Parse_ast.E_vector_subrange(vex,exp1,exp2) ->
E_vector_subrange(to_ast_exp k_env def_ord vex, to_ast_exp k_env def_ord exp1, to_ast_exp k_env def_ord exp2)
@@ -580,31 +564,6 @@ and to_ast_record_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp
| _ ->
None,Some(l, "Expected a field assignment to be identifier = expression")
-and to_ast_iexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps:Parse_ast.exp list):(int * unit exp) list option =
- match exps with
- | [] -> Some([])
- | iexp::exps -> (match to_iexp_try k_env def_ord iexp with
- | Some(iexp),None ->
- (match to_ast_iexps fail_on_error k_env def_ord exps with
- | Some(iexps) -> Some(iexp::iexps)
- | _ -> None)
- | None,Some(l,msg) ->
- if fail_on_error
- then typ_error l msg None None None
- else None
- | _ -> None)
-and to_iexp_try (k_env:kind Envmap.t) (def_ord:order) (Parse_ast.E_aux(exp,l): Parse_ast.exp): ((int * unit exp) option * (l*string) option) =
- match exp with
- | Parse_ast.E_app_infix(left,op,r) ->
- (match left,op with
- | Parse_ast.E_aux(Parse_ast.E_lit(Parse_ast.L_aux (Parse_ast.L_num i,ll)),cl), Parse_ast.Id_aux(Parse_ast.Id("="),leq) ->
- Some(i,to_ast_exp k_env def_ord r),None
- | Parse_ast.E_aux(_,li), Parse_ast.Id_aux (Parse_ast.Id("="),leq) ->
- None,(Some(li,"Expected a constant number to begin this indexed vector assignemnt"))
- | Parse_ast.E_aux(_,cl), Parse_ast.Id_aux(_,leq) ->
- None,(Some(leq,"Expected an indexed vector assignment constant = expression")))
- | _ -> None,(Some(l,"Expected an indexed vector assignment: constant = expression"))
-
let to_ast_default (names, k_env, default_order) (default : Parse_ast.default_typing_spec) : (unit default_spec) envs_out =
match default with
| Parse_ast.DT_aux(df,l) ->
@@ -632,20 +591,9 @@ let to_ast_spec (names,k_env,default_order) (val_:Parse_ast.val_spec) : (unit va
match val_ with
| Parse_ast.VS_aux(vs,l) ->
(match vs with
- | Parse_ast.VS_val_spec(ts,id) ->
- (*let _ = Printf.eprintf "to_ast_spec called for internal spec: for %s\n" (id_to_string (to_ast_id id)) in*)
- let typsch,_,_ = to_ast_typschm k_env default_order ts in
- VS_aux(VS_val_spec(typsch,to_ast_id id),(l,())),(names,k_env,default_order)
- | Parse_ast.VS_extern_spec(ts,id,s) ->
- let typsch,_,_ = to_ast_typschm k_env default_order ts in
- VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,())),(names,k_env,default_order)
- | Parse_ast.VS_cast_spec(ts,id) ->
- let typsch,_,_ = to_ast_typschm k_env default_order ts in
- VS_aux(VS_cast_spec(typsch,to_ast_id id),(l,())),(names,k_env,default_order)
- | Parse_ast.VS_extern_no_rename(ts,id) ->
+ | Parse_ast.VS_val_spec(ts,id,ext,is_cast) ->
let typsch,_,_ = to_ast_typschm k_env default_order ts in
- VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,())),(names,k_env,default_order))
-
+ VS_aux(VS_val_spec(typsch,to_ast_id id,ext,is_cast),(l,())),(names,k_env,default_order))
let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) =
Name_sect_aux(
@@ -733,16 +681,6 @@ let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def)
let key = id_to_string id in
let (kind,k) = to_ast_kind k_env kind in
(match k.k with
- | K_Typ | K_Lam _ ->
- let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in
- let kd_abrv = KD_aux(KD_abbrev(kind,id,to_ast_namescm name_scm_opt,typschm),(l,())) in
- let typ = (match typschm with
- | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
- begin match (typquant_to_quantkinds k_env tq) with
- | [] -> {k = K_Typ}
- | typs -> {k= K_Lam(typs,{k=K_Typ})}
- end) in
- kd_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
| K_Nat ->
let kd_nabrv =
(match typschm with
@@ -753,47 +691,7 @@ let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (unit kind_def)
| _ -> typ_error l "Def with kind Nat cannot have universal quantification" None None None)) in
kd_nabrv,(names,Envmap.insert k_env (key, k),def_ord)
| _ -> assert false
- )
- | Parse_ast.KD_record(kind,id,name_scm_opt,typq,fields,_) ->
- let id = to_ast_id id in
- let key = id_to_string id in
- let (kind,k) = to_ast_kind k_env kind in
- let typq,k_env,_ = to_ast_typquant k_env typq in
- let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
- let kd_rec = KD_aux(KD_record(kind,id,to_ast_namescm name_scm_opt,typq,fields,false),(l,())) in
- let typ = (match (typquant_to_quantkinds k_env typq) with
- | [ ] -> {k = K_Typ}
- | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
- kd_rec, (names,Envmap.insert k_env (key,typ), def_ord)
- | Parse_ast.KD_variant(kind,id,name_scm_opt,typq,arms,_) ->
- let id = to_ast_id id in
- let key = id_to_string id in
- let kind,k = to_ast_kind k_env kind in
- let typq,k_env,_ = to_ast_typquant k_env typq in
- let arms = List.map (to_ast_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
- let kd_var = KD_aux(KD_variant(kind,id,to_ast_namescm name_scm_opt,typq,arms,false),(l,())) in
- let typ = (match (typquant_to_quantkinds k_env typq) with
- | [ ] -> {k = K_Typ}
- | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
- kd_var, (names,Envmap.insert k_env (key,typ), def_ord)
- | Parse_ast.KD_enum(kind,id,name_scm_opt,enums,_) ->
- let id = to_ast_id id in
- let key = id_to_string id in
- let kind,k = to_ast_kind k_env kind in
- let enums = List.map to_ast_id enums in
- let keys = List.map id_to_string enums in
- let kd_enum = KD_aux(KD_enum(kind,id,to_ast_namescm name_scm_opt,enums,false),(l,())) in (* Add check that all enums have unique names *)
- let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
- kd_enum, (names,k_env,def_ord)
- | Parse_ast.KD_register(kind,id,t1,t2,ranges) ->
- let id = to_ast_id id in
- let key = id_to_string id in
- let kind,k = to_ast_kind k_env kind in
- let n1 = to_ast_nexp k_env t1 in
- let n2 = to_ast_nexp k_env t2 in
- let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
- KD_aux(KD_register(kind,id,n1,n2,ranges),(l,())), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
-
+ ))
let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
Rec_aux((match r with
@@ -1016,15 +914,12 @@ let typschm_of_string order str =
let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
typschm
-let val_spec_of_string order id str = mk_val_spec (VS_extern_no_rename (typschm_of_string order str, id))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some str, false))
let val_spec_ids (Defs defs) =
let val_spec_id (VS_aux (vs_aux, _)) =
match vs_aux with
- | VS_val_spec (typschm, id) -> id
- | VS_extern_no_rename (typschm, id) -> id
- | VS_extern_spec (typschm, id, e) -> id
- | VS_cast_spec (typschm, id) -> id
+ | VS_val_spec (_, id, _, _) -> id
in
let rec vs_ids = function
| DEF_spec vs :: defs -> val_spec_id vs :: vs_ids defs
@@ -1072,19 +967,19 @@ let generate_undefineds vs_ids (Defs defs) =
let undefined_td = function
| TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
- [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id));
+ [mk_val_spec (VS_val_spec (typschm, prepend_id "undefined_" id, None, false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
(mk_pat (P_lit (mk_lit L_unit)))
(mk_exp (E_app (mk_id "internal_pick",
[mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
| TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
pat
(mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
| TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
- [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+ [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
(mk_pat (P_lit (mk_lit L_unit)))
(mk_exp (E_app (mk_id "internal_pick",
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index d9ee73b8..62b18042 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -177,7 +177,7 @@ let split_src_type id ty (TypQ_aux (q,ql)) =
in
let find_set (Kid_aux (Var nvar,_) as kid) =
match list_extract (function
- | QI_aux (QI_const (NC_aux (NC_nat_set_bounded (Kid_aux (Var nvar',_),vals),_)),_)
+ | QI_aux (QI_const (NC_aux (NC_set (Kid_aux (Var nvar',_),vals),_)),_)
-> if nvar = nvar' then Some vals else None
| _ -> None) qs with
| None ->
@@ -327,8 +327,6 @@ let nexp_subst_fns substs refinements =
| E_if (e1,e2,e3) -> re (E_if (s_exp e1, s_exp e2, s_exp e3))
| E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,s_exp e1,s_exp e2,s_exp e3,ord,s_exp e4))
| E_vector es -> re (E_vector (List.map s_exp es))
- | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,s_exp e)) ies,
- s_opt_default ed))
| E_vector_access (e1,e2) -> re (E_vector_access (s_exp e1,s_exp e2))
| E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (s_exp e1,s_exp e2,s_exp e3))
| E_vector_update (e1,e2,e3) -> re (E_vector_update (s_exp e1,s_exp e2,s_exp e3))
@@ -365,9 +363,7 @@ let nexp_subst_fns substs refinements =
Pat_aux (Pat_when ((*s_pat*) p, s_exp e1, s_exp e2),(l,(*s_tannot*) annot))
and s_letbind (LB_aux (lb,(l,annot))) =
match lb with
- | LB_val_explicit (tysch,p,e) ->
- LB_aux (LB_val_explicit ((*s_typschm*) tysch,(*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
- | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
+ | LB_val (p,e) -> LB_aux (LB_val ((*s_pat*) p,s_exp e), (l,(*s_tannot*) annot))
and s_lexp (LEXP_aux (e,(l,annot))) =
let re e = LEXP_aux (e,(l,(*s_tannot*) annot)) in
match e with
@@ -401,7 +397,6 @@ let bindings_from_pat p =
| P_list ps
-> List.concat (List.map aux_pat ps)
| P_record (fps,_) -> List.concat (List.map aux_fpat fps)
- | P_vector_indexed ips -> List.concat (List.map (fun (_,p) -> aux_pat p) ips)
| P_cons (p1,p2) -> aux_pat p1 @ aux_pat p2
and aux_fpat (FP_aux (FP_Fpat (_,p), _)) = aux_pat p
in aux_pat p
@@ -440,12 +435,6 @@ let rec deexist_exp (E_aux (e,(l,(annot : Type_check.tannot))) as exp) =
| E_for (id,e1,e2,e3,ord,e4) ->
re (E_for (id,deexist_exp e1,deexist_exp e2,deexist_exp e3,ord,deexist_exp e4))
| E_vector es -> re (E_vector (List.map deexist_exp es))
- | E_vector_indexed (ies,def) ->
- re (E_vector_indexed
- (List.map (fun (i,e) -> (i,deexist_exp e)) ies,
- match def with
- | Def_val_aux (Def_val_empty,(l,ann)) -> Def_val_aux (Def_val_empty,(l,ann))
- | Def_val_aux (Def_val_dec e,(l,ann)) -> Def_val_aux (Def_val_dec (deexist_exp e),(l,ann))))
| E_vector_access (e1,e2) -> re (E_vector_access (deexist_exp e1,deexist_exp e2))
| E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (deexist_exp e1,deexist_exp e2,deexist_exp e3))
| E_vector_update (e1,e2,e3) -> re (E_vector_update (deexist_exp e1,deexist_exp e2,deexist_exp e3))
@@ -469,8 +458,7 @@ and deexist_pexp (Pat_aux (pe,(l,annot))) =
| Pat_when (p,e1,e2) -> Pat_aux (Pat_when ((*Type_check.strip_pat*) p,deexist_exp e1,deexist_exp e2),(l,annot))
and deexist_letbind (LB_aux (lb,(l,annot))) =
match lb with (* TODO, drop tysc if there's an exist? Do they even appear here? *)
- | LB_val_explicit (tysc,p,e) -> LB_aux (LB_val_explicit (tysc,(*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
- | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
+ | LB_val (p,e) -> LB_aux (LB_val ((*Type_check.strip_pat*) p,deexist_exp e),(l,annot))
and deexist_lexp (LEXP_aux (le,(l,annot))) =
let re le = LEXP_aux (le,(l,annot)) in
match le with
@@ -719,8 +707,6 @@ let split_defs splits defs =
| _ -> re (E_if (e1',e2',e3')))
| E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3,ord,const_prop_exp (ISubst.remove id substs) e4))
| E_vector es -> re (E_vector (List.map (const_prop_exp substs) es))
- | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,const_prop_exp substs e)) ies,
- const_prop_opt_default substs ed))
| E_vector_access (e1,e2) -> re (E_vector_access (const_prop_exp substs e1,const_prop_exp substs e2))
| E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3))
| E_vector_update (e1,e2,e3) -> re (E_vector_update (const_prop_exp substs e1,const_prop_exp substs e2,const_prop_exp substs e3))
@@ -770,11 +756,8 @@ let split_defs splits defs =
Pat_aux (Pat_when (p, const_prop_exp substs' e1, const_prop_exp substs' e2),l)
and const_prop_letbind substs (LB_aux (lb,annot)) =
match lb with
- | LB_val_explicit (tysch,p,e) ->
- (LB_aux (LB_val_explicit (tysch,p,const_prop_exp substs e), annot),
- remove_bound substs p)
- | LB_val_implicit (p,e) ->
- (LB_aux (LB_val_implicit (p,const_prop_exp substs e), annot),
+ | LB_val (p,e) ->
+ (LB_aux (LB_val (p,const_prop_exp substs e), annot),
remove_bound substs p)
and const_prop_lexp substs ((LEXP_aux (e,annot)) as le) =
let re e = LEXP_aux (e,annot) in
@@ -828,7 +811,7 @@ let split_defs splits defs =
let lg = Generated l in
let id = match subi with Id_aux (i,l) -> Id_aux (i,lg) in
let p = P_aux (P_id id, subannot) in
- E_aux (E_let (LB_aux (LB_val_implicit (p,sube),(lg,annot)), exp),(lg,annot))
+ E_aux (E_let (LB_aux (LB_val (p,sube),(lg,annot)), exp),(lg,annot))
else
let substs = isubst_from_list [subst] in
let () = nexp_substs := [] in
@@ -950,8 +933,6 @@ let split_defs splits defs =
relist fpat (fun fps -> P_record (fps,flag)) fps
| P_vector ps ->
relist spl (fun ps -> P_vector ps) ps
- | P_vector_indexed ips ->
- relist ipat (fun ips -> P_vector_indexed ips) ips
| P_vector_concat ps ->
relist spl (fun ps -> P_vector_concat ps) ps
| P_tup ps ->
@@ -1039,8 +1020,6 @@ let split_defs splits defs =
| E_if (e1,e2,e3) -> re (E_if (map_exp e1, map_exp e2, map_exp e3))
| E_for (id,e1,e2,e3,ord,e4) -> re (E_for (id,map_exp e1,map_exp e2,map_exp e3,ord,map_exp e4))
| E_vector es -> re (E_vector (List.map map_exp es))
- | E_vector_indexed (ies,ed) -> re (E_vector_indexed (List.map (fun (i,e) -> (i,map_exp e)) ies,
- map_opt_default ed))
| E_vector_access (e1,e2) -> re (E_vector_access (map_exp e1,map_exp e2))
| E_vector_subrange (e1,e2,e3) -> re (E_vector_subrange (map_exp e1,map_exp e2,map_exp e3))
| E_vector_update (e1,e2,e3) -> re (E_vector_update (map_exp e1,map_exp e2,map_exp e3))
@@ -1105,8 +1084,7 @@ let split_defs splits defs =
) patnsubsts)
and map_letbind (LB_aux (lb,annot)) =
match lb with
- | LB_val_explicit (tysch,p,e) -> LB_aux (LB_val_explicit (tysch,check_single_pat p,map_exp e), annot)
- | LB_val_implicit (p,e) -> LB_aux (LB_val_implicit (check_single_pat p,map_exp e), annot)
+ | LB_val (p,e) -> LB_aux (LB_val (check_single_pat p,map_exp e), annot)
and map_lexp ((LEXP_aux (e,annot)) as le) =
let re e = LEXP_aux (e,annot) in
match e with
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 1e2c8bc6..38b3cc9d 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -150,7 +150,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
| _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
match lb_aux with
- | LB_val_implicit (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
+ | LB_val (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
| _ -> failwith "Ocaml: Explicit letbind found"
and ocaml_pexps ctx = function
| [pexp] -> ocaml_pexp ctx pexp
@@ -287,10 +287,8 @@ let ocaml_typedef ctx (TD_aux (td_aux, _)) =
let get_externs (Defs defs) =
let extern_id (VS_aux (vs_aux, _)) =
match vs_aux with
- | VS_val_spec (typschm, id) -> []
- | VS_extern_no_rename (typschm, id) -> [(id, id)]
- | VS_extern_spec (typschm, id, name) -> [(id, mk_id name)]
- | VS_cast_spec (typschm, id) -> []
+ | VS_val_spec (typschm, id, None, _) -> []
+ | VS_val_spec (typschm, id, Some ext, _) -> [(id, mk_id ext)]
in
let rec extern_ids = function
| DEF_spec vs :: defs -> extern_id vs :: extern_ids defs
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 6424d682..f38c2d3d 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -158,11 +158,11 @@ kinded_id_aux = (* optionally kind-annotated identifier *)
and
n_constraint_aux = (* constraint over kind $_$ *)
- NC_fixed of atyp * atyp
+ NC_equal of atyp * atyp
| NC_bounded_ge of atyp * atyp
| NC_bounded_le of atyp * atyp
| NC_not_equal of atyp * atyp
- | NC_nat_set_bounded of kid * (int) list
+ | NC_set of kid * (int) list
| NC_or of n_constraint * n_constraint
| NC_and of n_constraint * n_constraint
| NC_true
@@ -234,11 +234,10 @@ pat_aux = (* Pattern *)
| P_as of pat * id (* named pattern *)
| P_typ of atyp * pat (* typed pattern *)
| P_id of id (* identifier *)
- | P_var of kid
+ | P_var of pat * kid (* bind pat to type variable *)
| P_app of id * (pat) list (* union constructor pattern *)
| P_record of (fpat) list * bool (* struct pattern *)
| P_vector of (pat) list (* vector pattern *)
- | P_vector_indexed of ((int * pat)) list (* vector pattern (with explicit indices) *)
| P_vector_concat of (pat) list (* concatenated vector pattern *)
| P_tup of (pat) list (* tuple pattern *)
| P_list of (pat) list (* list pattern *)
@@ -269,7 +268,6 @@ exp_aux = (* Expression *)
| E_loop of loop * exp * exp
| E_for of id * exp * exp * exp * atyp * exp (* loop *)
| E_vector of (exp) list (* vector (indexed from 0) *)
- | E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *)
| E_vector_access of exp * exp (* vector access *)
| E_vector_subrange of exp * exp * exp (* subvector extraction *)
| E_vector_update of exp * exp * exp (* vector functional update *)
@@ -322,8 +320,7 @@ and pexp =
Pat_aux of pexp_aux * l
and letbind_aux = (* Let binding *)
- LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+ LB_val of pat * exp (* value binding, implicit type (pat must be total) *)
and letbind =
LB_aux of letbind_aux * l
@@ -427,20 +424,12 @@ type_def_aux = (* Type definition body *)
type
val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string
- | VS_cast_spec of typschm * id
+ VS_val_spec of typschm * id * string option * bool
type
kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *)
KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
- | KD_record of kind * id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
- | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | KD_register of kind * id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
-
type
dec_spec_aux = (* Register declarations *)
diff --git a/src/parser.mly b/src/parser.mly
index 0c3dbb03..a415801e 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -49,8 +49,15 @@ open Parse_ast
let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos())
let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
+let id_of_kid = function
+ | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
+
let idl i = Id_aux(i, loc())
+let string_of_id = function
+ | Id_aux (Id str, _) -> str
+ | Id_aux (DeIid str, _) -> str
+
let efl e = BE_aux(e, loc())
let ploc p = P_aux(p,loc ())
@@ -503,7 +510,7 @@ atomic_pat:
| id
{ ploc (P_app($1,[])) }
| tyvar
- { ploc (P_var $1) }
+ { ploc (P_var (ploc (P_id (id_of_kid $1)), $1)) }
| Lcurly fpats Rcurly
{ ploc (P_record((fst $2, snd $2))) }
| Lsquare comma_pats Rsquare
@@ -512,8 +519,6 @@ atomic_pat:
{ ploc (P_vector([$2])) }
| Lsquare Rsquare
{ ploc (P_vector []) }
- | Lsquare npats Rsquare
- { ploc (P_vector_indexed($2)) }
| Lparen comma_pats Rparen
{ ploc (P_tup($2)) }
| SquareBarBar BarBarSquare
@@ -604,8 +609,6 @@ atomic_exp:
{ eloc (E_vector([$2])) }
| Lsquare comma_exps Rsquare
{ eloc (E_vector($2)) }
- | Lsquare comma_exps Semi Default Eq exp Rsquare
- { eloc (E_vector_indexed($2,(Def_val_aux(Def_val_dec $6, locn 3 6)))) }
| Lsquare exp With atomic_exp Eq exp Rsquare
{ eloc (E_vector_update($2,$4,$6)) }
| Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
@@ -1006,12 +1009,7 @@ patsexp:
letbind:
| Let_ atomic_pat Eq exp
- { lbloc (LB_val_implicit($2,$4)) }
- | Let_ typquant atomic_typ atomic_pat Eq exp
- { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
-/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this
- | Let_ Lparen typ Rparen atomic_pat Eq exp
- { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */
+ { lbloc (LB_val($2,$4)) }
funcl:
| id atomic_pat Eq exp
@@ -1053,21 +1051,21 @@ fun_def:
val_spec:
| Val typquant typ id
- { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
+ { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4, None, false)) }
| Val typ id
- { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+ { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3, None, false)) }
| Val Cast typquant typ id
- { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, None, true)) }
| Val Cast typ id
- { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, None, true)) }
| Val Extern typquant typ id
- { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some (string_of_id $5), false)) }
| Val Extern typ id
- { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3, $4, Some (string_of_id $4), false)) }
| Val Extern typquant typ id Eq String
- { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
+ { vloc (VS_val_spec (mk_typschm $3 $4 3 4,$5, Some $7, false)) }
| Val Extern typ id Eq String
- { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
+ { vloc (VS_val_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, Some $6, false)) }
kinded_id:
| tyvar
@@ -1101,7 +1099,7 @@ nexp_constraint1:
nexp_constraint2:
| nexp_typ Eq nexp_typ
- { NC_aux(NC_fixed($1,$3), loc () ) }
+ { NC_aux(NC_equal($1,$3), loc () ) }
| nexp_typ ExclEq nexp_typ
{ NC_aux (NC_not_equal ($1, $3), loc ()) }
| nexp_typ GtEq nexp_typ
@@ -1109,9 +1107,9 @@ nexp_constraint2:
| nexp_typ LtEq nexp_typ
{ NC_aux(NC_bounded_le($1,$3), loc () ) }
| tyvar In Lcurly nums Rcurly
- { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+ { NC_aux(NC_set($1,$4), loc ()) }
| tyvar IN Lcurly nums Rcurly
- { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
+ { NC_aux(NC_set($1,$4), loc ()) }
| True
{ NC_aux (NC_true, loc ()) }
| False
@@ -1288,30 +1286,7 @@ ktype_def:
{ kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) }
| Def kind tid Eq Num
{ kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) }
- | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
- { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) }
- | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
- { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) }
- | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly
- { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
- | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly
- { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
- | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
- { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) }
- | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly
- { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
- | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly
- { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) }
- | Def kind tid Eq Const Union Lcurly union_body Rcurly
- { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
- | Def kind tid Eq Enumerate Lcurly enum_body Rcurly
- { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) }
- | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly
- { kdloc (KD_enum($2,$3,$4,$8,false)) }
- | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
- { kdloc (KD_register($2,$3, $8, $10, $13)) }
-
-
+
def:
| type_def
{ dloc (DEF_type($1)) }
diff --git a/src/parser2.mly b/src/parser2.mly
index 02a8f09c..09fe4b41 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -51,6 +51,9 @@ let loc n m = Range (m, n)
let mk_id i n m = Id_aux (i, loc m n)
let mk_kid str n m = Kid_aux (Var str, loc n m)
+let id_of_kid = function
+ | Kid_aux (Var v, l) -> Id_aux (Id (String.sub v 1 (String.length v - 1)), l)
+
let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
let mk_effect e n m = BE_aux (e, loc n m)
@@ -266,7 +269,7 @@ atomic_nc:
| False
{ mk_nc NC_false $startpos $endpos }
| typ Eq typ
- { mk_nc (NC_fixed ($1, $3)) $startpos $endpos }
+ { mk_nc (NC_equal ($1, $3)) $startpos $endpos }
| typ ExclEq typ
{ mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
| nc_lchain
@@ -276,7 +279,7 @@ atomic_nc:
| Lparen nc Rparen
{ $2 }
| kid In Lcurly num_list Rcurly
- { mk_nc (NC_nat_set_bounded ($1, $4)) $startpos $endpos }
+ { mk_nc (NC_set ($1, $4)) $startpos $endpos }
num_list:
| Num
@@ -481,7 +484,7 @@ atomic_typ:
{ let v = mk_kid "n" $startpos $endpos in
let atom_id = mk_id (Id "atom") $startpos $endpos in
let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in
- mk_typ (ATyp_exist ([v], NC_aux (NC_nat_set_bounded (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
+ mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, $2), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos }
| Lcurly kid_list Dot typ Rcurly
{ mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
| Lcurly kid_list Comma nc Dot typ Rcurly
@@ -604,7 +607,7 @@ atomic_pat:
| id
{ mk_pat (P_id $1) $startpos $endpos }
| kid
- { mk_pat (P_var $1) $startpos $endpos }
+ { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
| pat Colon typ
@@ -836,7 +839,7 @@ block:
%inline letbind:
| pat Eq exp
- { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
+ { LB_aux (LB_val ($1, $3), loc $startpos $endpos) }
atomic_exp:
| atomic_exp Colon atomic_typ
@@ -942,7 +945,13 @@ let_def:
val_spec_def:
| Val id Colon typschm
- { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
+ { mk_vs (VS_val_spec ($4, $2, None, false)) $startpos $endpos }
+ | Val Cast id Colon typschm
+ { mk_vs (VS_val_spec ($5, $3, None, true)) $startpos $endpos }
+ | Val id Eq String Colon typschm
+ { mk_vs (VS_val_spec ($6, $2, Some $4, false)) $startpos $endpos }
+ | Val Cast id Eq String Colon typschm
+ { mk_vs (VS_val_spec ($7, $3, Some $5, true)) $startpos $endpos }
register_def:
| Register id Colon typ
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 02cc3574..83c28a7d 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -217,11 +217,11 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
group (parens (nexp ne))
and nexp_constraint (NC_aux(nc,_)) = match nc with
- | NC_fixed(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
+ | NC_equal(n1,n2) -> doc_op equals (nexp n1) (nexp n2)
| NC_not_equal (n1, n2) -> doc_op (string "!=") (nexp n1) (nexp n2)
| NC_bounded_ge(n1,n2) -> doc_op (string ">=") (nexp n1) (nexp n2)
| NC_bounded_le(n1,n2) -> doc_op (string "<=") (nexp n1) (nexp n2)
- | NC_nat_set_bounded(v,bounds) ->
+ | NC_set(v,bounds) ->
doc_op (string "IN") (doc_var v)
(braces (separate_map comma_sp doc_int bounds))
| NC_or (nc1, nc2) ->
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index f6fec143..b97845fd 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -329,7 +329,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
begin match id with
| Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
| _ -> doc_id_lem id end
- | P_var kid -> doc_var_lem kid
+ | P_var(p,kid) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_var_lem kid])
| P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
| P_typ(typ,p) ->
let doc_p = doc_pat_lem sequential mwords true p in
@@ -349,7 +349,7 @@ let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) =
| _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
| P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
| P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
- | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *)
+ | P_record (_,_) -> empty (* TODO *)
let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
| Typ_tup ts -> List.exists contains_bitvector_typ ts
@@ -825,63 +825,6 @@ let doc_exp_lem, doc_let_lem =
else (epp,aexp_needed) in
if aexp_needed then parens (align epp) else epp
(* *)
- | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) ->
- let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
- let (start, len, order, etyp) =
- if is_vector_typ t then vector_typ_args_of t
- else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in
- let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
- let start = match simplify_nexp start with
- | Nexp_aux (Nexp_constant i, _) -> string_of_int i
- | _ -> if dir then "0" else string_of_int (List.length iexps) in
- let size = match simplify_nexp len with
- | Nexp_aux (Nexp_constant i, _)-> string_of_int i
- | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
- string_of_int (Util.power 2 i)
- | _ ->
- raise (Reporting_basic.err_unreachable l
- "trying to pretty-print indexed vector without constant size") in
- let default_string =
- match default with
- | Def_val_empty ->
- if is_bitvector_typ t then string "BU"
- else failwith "E_vector_indexed of non-bitvector type without default argument"
- | Def_val_dec e ->
- (*let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in
- match t with
- | Tapp ("register",
- [TA_typ ({t = rt})]) ->
- (* TODO: Does this case still occur with the new type checker? *)
- let n = match rt with
- | Tapp ("vector",TA_nexp {nexp = Nconst i} :: TA_nexp {nexp = Nconst j} ::_) ->
- abs_big_int (sub_big_int i j)
- | _ ->
- raise ((Reporting_basic.err_unreachable dl)
- ("not the right type information available to construct "^
- "undefined register")) in
- parens (string ("UndefinedRegister " ^ string_of_big_int n))
- | _ ->*) expY e in
- let iexp (i,e) = parens (doc_int i ^^ comma ^^ expN e) in
- let expspp =
- match iexps with
- | [] -> empty
- | e :: es ->
- let (expspp,_) =
- List.fold_left
- (fun (pp,count) e ->
- (pp ^^ semi ^^ (if count = 5 then break 1 else empty) ^^ iexp e),
- if count = 5 then 0 else count + 1)
- (iexp e,0) es in
- align (expspp) in
- let call = string "make_indexed_vector" in
- let epp =
- align (group (call ^//^ brackets expspp ^/^
- separate space [default_string;string start;string size;string dir_out])) in
- let (bepp, aexp_needed) =
- if is_bitvector_typ t && mwords
- then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem sequential mwords false t, true)
- else (epp, aexp_needed) in
- if aexp_needed then parens (align bepp) else bepp
| E_vector_update(v,e1,e2) ->
let t = typ_of full_exp in
let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
@@ -1070,8 +1013,7 @@ let doc_exp_lem, doc_let_lem =
raise (Reporting_basic.err_unreachable l
"unsupported internal expression encountered while pretty-printing")
and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with
- | LB_val_explicit(_,pat,e)
- | LB_val_implicit(pat,e) ->
+ | LB_val(pat,e) ->
prefix 2 1
(separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
(top_exp sequential mwords early_ret false e)
@@ -1572,13 +1514,7 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
| DEC_alias(id,alspec) -> empty
| DEC_typ_alias(typ,id,alspec) -> empty
-let doc_spec_lem mwords (VS_aux (valspec,annot)) =
- match valspec with
- | VS_extern_no_rename _
- | VS_extern_spec _ -> empty (* ignore these at the moment *)
- | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty
-(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *)
-
+let doc_spec_lem mwords (VS_aux (valspec,annot)) = empty
let rec doc_def_lem sequential mwords def = match def with
| DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 73f06d1a..2c9cf83c 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -215,7 +215,7 @@ and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
"(NC_aux " ^
(match nc with
- | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+ | NC_equal(n1,n2) -> "(NC_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
| NC_not_equal(n1,n2) -> "(NC_not_equal " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
@@ -223,7 +223,7 @@ and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
| NC_and(nc1,nc2) -> "(NC_and " ^ pp_format_nexp_constraint_lem nc1 ^ " " ^ pp_format_nexp_constraint_lem nc2 ^ ")"
| NC_true -> "NC_true"
| NC_false -> "NC_false"
- | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^
+ | NC_set(id,bounds) -> "(NC_set " ^
pp_format_var_lem id ^
" [" ^
list_format "; " string_of_int bounds ^
@@ -328,7 +328,7 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
| P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
| P_wild -> "P_wild"
| P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
- | P_var(kid) -> "(P_var " ^ pp_format_var_lem kid ^ ")"
+ | P_var(pat,kid) -> "(P_var " ^ pp_format_pat_lem pat ^ " " ^ pp_format_var_lem kid ^ ")"
| P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
| P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
| P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
@@ -338,8 +338,6 @@ let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
"(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats
^ "])"
| P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
- | P_vector_indexed(ipats) ->
- "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])"
| P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
| P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
| P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
@@ -351,10 +349,8 @@ let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
let print_lb ppf lb =
match lb with
- | LB_val_explicit(ts,pat,exp) ->
- fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
- | LB_val_implicit(pat,exp) ->
- fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in
+ | LB_val(pat,exp) ->
+ 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))) =
@@ -387,15 +383,6 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
| E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]"
kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
- | E_vector_indexed(iexps,(Def_val_aux (default, (dl,dannot)))) ->
- let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
- let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
- let default_string ppf _ = (match default with
- | Def_val_empty -> fprintf ppf "(Def_val_aux Def_val_empty (%a,%a))" pp_lem_l dl pp_annot dannot
- | Def_val_dec e -> fprintf ppf "(Def_val_aux (Def_val_dec %a) (%a,%a))"
- pp_lem_exp e pp_lem_l dl pp_annot dannot) in
- fprintf ppf "@[<0>(E_aux (%a [%a] %a) (%a, %a))@]" kwd "E_vector_indexed"
- (list_pp iformat lformat) iexps default_string () pp_lem_l l pp_annot annot
| E_vector_access(v,e) ->
fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]"
kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot
@@ -519,17 +506,17 @@ let pp_lem_default ppf (DT_aux(df,l)) =
in
fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
+(* FIXME *)
let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
let print_spec ppf v =
match v with
- | VS_val_spec(ts,id) ->
+ | VS_val_spec(ts,id,None,false) ->
fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
- | VS_extern_spec(ts,id,s) ->
+ | VS_val_spec(ts,id,Some s,false) ->
fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
- | VS_extern_no_rename(ts,id) ->
- fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
- | VS_cast_spec(ts,id) ->
- fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_cast_spec" pp_lem_typscm ts pp_lem_id id
+ | VS_val_spec(ts,id,None,true) ->
+ fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_cast_spec" pp_lem_typscm ts pp_lem_id id
+ | _ -> failwith "Invalid valspec"
in
fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
@@ -578,35 +565,9 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) =
let print_kd ppf kd =
match kd with
- | KD_abbrev(kind,id,namescm,typschm) ->
- fprintf ppf "@[<0>(KD_abbrev %a %a %a %a)@]"
- pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
| KD_nabbrev(kind,id,namescm,n) ->
fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]"
pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n
- | KD_record(kind,id,nm,typq,fs,_) ->
- let f_pp ppf (typ,id) =
- fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
- fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
- kwd "KD_record" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
- | KD_variant(kind,id,nm,typq,ar,_) ->
- let a_pp ppf (Tu_aux(typ_u,l)) =
- match typ_u with
- | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
- pp_lem_typ typ pp_lem_id id pp_lem_l l
- | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
- in
- fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
- kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
- | KD_enum(kind,id,ns,enums,_) ->
- let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
- fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
- kwd "KD_enum" pp_lem_kind kind pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
- | KD_register(kind,id,n1,n2,rs) ->
- let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
- let pp_rids = (list_pp pp_rid pp_rid) in
- fprintf ppf "@[<0>(%a %a %a %a %a [%a])@]"
- kwd "KD_register" pp_lem_kind kind pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
in
fprintf ppf "@[<0>(KD_aux %a (%a, %a))@]" print_kd kd pp_lem_l l pp_annot annot
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index b331a6cf..b1238f8a 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -198,7 +198,6 @@ let doc_pat_ocaml =
| P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*)
| P_cons (p,p') -> doc_op (string "::") (pat p) (pat p')
| P_record _ -> raise (Reporting_basic.err_unreachable l "unhandled record pattern")
- | P_vector_indexed _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_indexed pattern")
| P_vector_concat _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_concat pattern")
in pat
@@ -391,42 +390,6 @@ let doc_exp_ocaml, doc_let_ocaml =
parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps);
string start;
string dir_out])])
- | E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
- let (start, len, order, _) = vector_typ_args_of (Env.base_typ_of env typ) in
- (*match annot with
- | Base((_,t),_,_,_,_,_) ->
- match t.t with
- | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])
- | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])})
- | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) ->*)
- let call =
- if is_bitvector_typ (Env.base_typ_of env typ)
- then (string "make_indexed_bitv")
- else (string "make_indexed_v") in
- let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
- let start = match start with
- | Nexp_aux (Nexp_constant i, _) -> string_of_int i
- | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
- string_of_int (Util.power 2 i)
- | _ -> if dir then "0" else string_of_int (List.length iexps) in
- let size = match len with
- | Nexp_aux (Nexp_constant i, _) -> string_of_int i
- | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
- string_of_int (Util.power 2 i)
- | _ ->
- raise (Reporting_basic.err_unreachable l
- "indexed vector without known length") in
- let default_string =
- (match default with
- | Def_val_empty -> string "None"
- | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in
- let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in
- parens (separate space [call;
- (brackets (separate_map semi iexp iexps));
- default_string;
- string start;
- string size;
- string dir_out])
| E_vector_update(v,e1,e2) ->
(*Has never happened to date*)
brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2)))
@@ -476,11 +439,7 @@ let doc_exp_ocaml, doc_let_ocaml =
"internal expression should have been rewritten before pretty-printing")
| E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *)
and let_exp (LB_aux(lb,_)) = match lb with
- | LB_val_explicit(ts,pat,e) ->
- prefix 2 1
- (separate space [string "let"; doc_pat_ocaml pat; equals])
- (top_exp false e)
- | LB_val_implicit(pat,e) ->
+ | LB_val(pat,e) ->
prefix 2 1
(separate space [string "let"; doc_pat_ocaml pat; equals])
(top_exp false e)
@@ -639,55 +598,6 @@ let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with
doc_id_ocaml id;
equals;
doc_nexp nexp]
- | KD_abbrev(_,id,nm,typschm) ->
- doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm)
- | KD_record(_,id,nm,typq,fs,_) ->
- let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in
- let fs_doc = group (separate_map (break 1) f_pp fs) in
- doc_op equals
- (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc))
- | KD_variant(_,id,nm,typq,ar,_) ->
- let n = List.length ar in
- let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in
- doc_op equals
- (concat [string "type"; space; doc_id_ocaml_type id;])
- (if n > 246
- then brackets (space ^^(doc_typquant_ocaml typq ar_doc))
- else (doc_typquant_ocaml typq ar_doc))
- | KD_enum(_,id,nm,enums,_) ->
- let n = List.length enums in
- let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor) enums) in
- doc_op equals
- (concat [string "type"; space; doc_id_ocaml_type id;])
- (enums_doc)
- | KD_register(_,id,n1,n2,rs) ->
- let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in
- let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
- match n1,n2 with
- | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
- let dir = i1 < i2 in
- let size = if dir then i2-i1 +1 else i1-i2 in
- doc_op equals
- ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val"))
- (separate space [string "Vregister";
- (parens (separate comma_sp
- [parens (separate space
- [string "match init_val with";
- pipe;
- string "None";
- arrow;
- string "ref";
- string "(Array.make";
- doc_int size;
- string "Vzero)";
- pipe;
- string "Some init_val";
- arrow;
- string "ref init_val";]);
- doc_nexp n1;
- string (if dir then "true" else "false");
- string_lit (doc_id id);
- brackets doc_rids]))])
let doc_rec_ocaml (Rec_aux(r,_)) = match r with
| Rec_nonrec -> empty
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8299e9b5..ce887f72 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -41,6 +41,7 @@
(**************************************************************************)
open Ast
+open Ast_util
open PPrint
open Pretty_print_common
@@ -109,13 +110,14 @@ let doc_pat, doc_atomic_pat =
| P_lit lit -> doc_lit lit
| P_wild -> underscore
| P_id id -> doc_id id
- | P_var kid -> doc_var kid
+ | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
+ doc_var kid
+ | P_var(p,kid) -> parens (separate space [pat p; string "as"; doc_var kid])
| P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id id])
| P_typ(typ,p) -> separate space [parens (doc_typ typ); atomic_pat p]
| P_app(id,[]) -> doc_id id
| P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats)
| P_vector pats -> brackets (separate_map comma_sp atomic_pat pats)
- | P_vector_indexed ipats -> brackets (separate_map comma_sp npat ipats)
| P_tup pats -> parens (separate_map comma_sp atomic_pat pats)
| P_list pats -> squarebarbars (separate_map semi_sp atomic_pat pats)
| P_cons (pat1, pat2) -> separate space [atomic_pat pat1; coloncolon; pat pat2]
@@ -270,13 +272,6 @@ let doc_exp, doc_let =
((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst)
| _ -> assert false)) exps ""))
| _ -> default_print ()))
- | E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
- let default_string =
- (match default with
- | Def_val_empty -> string ""
- | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in
- let iexp (i,e) = doc_op equals (doc_int i) (exp e) in
- brackets (concat [(separate_map comma iexp iexps); default_string])
| E_vector_update(v,e1,e2) ->
brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2)))
| E_vector_update_subrange(v,e1,e2,e3) ->
@@ -356,17 +351,7 @@ let doc_exp, doc_let =
separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2]
| _ -> failwith ("Cannot print: " ^ Ast_util.string_of_exp expr)
and let_exp (LB_aux(lb,_)) = match lb with
- | LB_val_explicit(ts,pat,e) ->
- (match ts with
- | TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_no_forall,_),_),_) ->
- prefix 2 1
- (separate space [string "let"; parens (doc_typscm_atomic ts); doc_atomic_pat pat; equals])
- (atomic_exp e)
- | _ ->
- prefix 2 1
- (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
- (atomic_exp e))
- | LB_val_implicit(pat,e) ->
+ | LB_val(pat,e) ->
prefix 2 1
(separate space [string "let"; doc_atomic_pat pat; equals])
(atomic_exp e)
@@ -410,15 +395,14 @@ let doc_default (DT_aux(df,_)) = match df with
| DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
let doc_spec (VS_aux(v,_)) = match v with
- | VS_val_spec(ts,id) ->
+ | VS_val_spec(ts,id,None,false) ->
separate space [string "val"; doc_typscm ts; doc_id id]
- | VS_cast_spec (ts, id) ->
+ | VS_val_spec (ts, id,None,true) ->
separate space [string "val"; string "cast"; doc_typscm ts; doc_id id]
- | VS_extern_no_rename(ts,id) ->
- separate space [string "val"; string "extern"; doc_typscm ts; doc_id id]
- | VS_extern_spec(ts,id,s) ->
+ | VS_val_spec(ts,id,Some ext,false) ->
separate space [string "val"; string "extern"; doc_typscm ts;
- doc_op equals (doc_id id) (dquotes (string s))]
+ doc_op equals (doc_id id) (dquotes (string ext))]
+ | _ -> failwith "Invalid valspec"
let doc_namescm (Name_sect_aux(ns,_)) = match ns with
| Name_sect_none -> empty
@@ -461,37 +445,8 @@ let doc_typdef (TD_aux(td,_)) = match td with
])
let doc_kindef (KD_aux(kd,_)) = match kd with
- | KD_abbrev(kind,id,nm,typschm) ->
- doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_typscm typschm)
| KD_nabbrev(kind,id,nm,n) ->
doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n)
- | KD_record(kind,id,nm,typq,fs,_) ->
- let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in
- let fs_doc = group (separate_map (break 1) f_pp fs) in
- doc_op equals
- (concat [string "def"; space;doc_kind kind; space; doc_id id; doc_namescm nm])
- (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc))
- | KD_variant(kind,id,nm,typq,ar,_) ->
- let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in
- doc_op equals
- (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
- (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc))
- | KD_enum(kind,id,nm,enums,_) ->
- let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in
- doc_op equals
- (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
- (string "enumerate" ^^ space ^^ braces enums_doc)
- | KD_register(kind,id,n1,n2,rs) ->
- let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in
- let doc_rids = group (separate_map (break 1) doc_rid rs) in
- doc_op equals
- (string "def" ^^ space ^^ doc_kind kind ^^ space ^^ doc_id id)
- (separate space [
- string "register bits";
- brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2);
- braces doc_rids;
- ])
-
let doc_rec (Rec_aux(r,_)) = match r with
| Rec_nonrec -> empty
diff --git a/src/rewriter.ml b/src/rewriter.ml
index c2b8e618..1c02b161 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -132,9 +132,6 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| E_for (_,e1,e2,e3,_,e4) -> union_eff_exps [e1;e2;e3;e4]
| E_loop (_,e1,e2) -> union_eff_exps [e1;e2]
| E_vector es -> union_eff_exps es
- | E_vector_indexed (ies,opt_default) ->
- let (_,es) = List.split ies in
- union_effects (effect_of_opt_default opt_default) (union_eff_exps es)
| E_vector_access (e1,e2) -> union_eff_exps [e1;e2]
| E_vector_subrange (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
| E_vector_update (e1,e2,e3) -> union_eff_exps [e1;e2;e3]
@@ -216,8 +213,7 @@ let fix_eff_pexp (Pat_aux (pexp,((l,_) as annot))) = match snd annot with
let fix_eff_lb (LB_aux (lb,((l,_) as annot))) = match snd annot with
| Some (env, typ, eff) ->
let effsum = match lb with
- | LB_val_explicit (_,_,e) -> effect_of e
- | LB_val_implicit (_,e) -> effect_of e in
+ | LB_val (_,e) -> effect_of e in
LB_aux (lb, (l, Some (env, typ, effsum)))
| None ->
LB_aux (lb, (l, None))
@@ -364,7 +360,6 @@ let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
rewrap (P_record(List.map (fun (FP_aux(FP_Fpat(id,pat),pannot)) -> FP_aux(FP_Fpat(id, rewrite pat), pannot)) fpats,
false))
| P_vector pats -> rewrap (P_vector(List.map rewrite pats))
- | P_vector_indexed ipats -> rewrap (P_vector_indexed(List.map (fun (i,pat) -> (i, rewrite pat)) ipats))
| P_vector_concat pats -> rewrap (P_vector_concat (List.map rewrite pats))
| P_tup pats -> rewrap (P_tup (List.map rewrite pats))
| P_list pats -> rewrap (P_list (List.map rewrite pats))
@@ -392,11 +387,6 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot))) =
| E_loop (loop, e1, e2) ->
rewrap (E_loop (loop, rewrite e1, rewrite e2))
| E_vector exps -> rewrap (E_vector (List.map rewrite exps))
- | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
- let def = match default with
- | Def_val_empty -> default
- | Def_val_dec e -> Def_val_dec (rewrite e) in
- rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot)))
| E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
| E_vector_subrange (vec,i1,i2) ->
rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2))
@@ -545,11 +535,8 @@ let rewrite_let rewriters (LB_aux(letbind,(l,annot))) =
| None -> Some(m,s) (*Shouldn't happen*)
| Some new_m -> Some(new_m,s) in*)
match letbind with
- | LB_val_explicit (typschm, pat,exp) ->
- LB_aux(LB_val_explicit (typschm,rewriters.rewrite_pat rewriters pat,
- rewriters.rewrite_exp rewriters exp),(l,annot))
- | LB_val_implicit ( pat, exp) ->
- LB_aux(LB_val_implicit (rewriters.rewrite_pat rewriters pat,
+ | LB_val ( pat, exp) ->
+ LB_aux(LB_val (rewriters.rewrite_pat rewriters pat,
rewriters.rewrite_exp rewriters exp),(l,annot))
let rewrite_lexp rewriters (LEXP_aux(lexp,(l,annot))) =
@@ -625,11 +612,10 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_as : 'pat * id -> 'pat_aux
; p_typ : Ast.typ * 'pat -> 'pat_aux
; p_id : id -> 'pat_aux
- ; p_var : kid -> 'pat_aux
+ ; p_var : 'pat * kid -> 'pat_aux
; p_app : id * 'pat list -> 'pat_aux
; p_record : 'fpat list * bool -> 'pat_aux
; p_vector : 'pat list -> 'pat_aux
- ; p_vector_indexed : (int * 'pat) list -> 'pat_aux
; p_vector_concat : 'pat list -> 'pat_aux
; p_tup : 'pat list -> 'pat_aux
; p_list : 'pat list -> 'pat_aux
@@ -644,13 +630,12 @@ let rec fold_pat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a pat
| P_lit lit -> alg.p_lit lit
| P_wild -> alg.p_wild
| P_id id -> alg.p_id id
- | P_var kid -> alg.p_var kid
- | P_as (p,id) -> alg.p_as (fold_pat alg p,id)
+ | P_var (p, kid) -> alg.p_var (fold_pat alg p, kid)
+ | P_as (p,id) -> alg.p_as (fold_pat alg p, id)
| P_typ (typ,p) -> alg.p_typ (typ,fold_pat alg p)
| P_app (id,ps) -> alg.p_app (id,List.map (fold_pat alg) ps)
| P_record (ps,b) -> alg.p_record (List.map (fold_fpat alg) ps, b)
| P_vector ps -> alg.p_vector (List.map (fold_pat alg) ps)
- | P_vector_indexed ps -> alg.p_vector_indexed (List.map (fun (i,p) -> (i, fold_pat alg p)) ps)
| P_vector_concat ps -> alg.p_vector_concat (List.map (fold_pat alg) ps)
| P_tup ps -> alg.p_tup (List.map (fold_pat alg) ps)
| P_list ps -> alg.p_list (List.map (fold_pat alg) ps)
@@ -666,7 +651,7 @@ and fold_fpat_aux (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat_a
and fold_fpat (alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg) : 'a fpat -> 'fpat =
function
| FP_aux (fpat,annot) -> alg.fP_aux (fold_fpat_aux alg fpat,annot)
-
+
(* identity fold from term alg to term alg *)
let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
{ p_lit = (fun lit -> P_lit lit)
@@ -674,11 +659,10 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
; p_as = (fun (pat,id) -> P_as (pat,id))
; p_typ = (fun (typ,pat) -> P_typ (typ,pat))
; p_id = (fun id -> P_id id)
- ; p_var = (fun kid -> P_var kid)
+ ; p_var = (fun (pat,kid) -> P_var (pat,kid))
; p_app = (fun (id,ps) -> P_app (id,ps))
; p_record = (fun (ps,b) -> P_record (ps,b))
; p_vector = (fun ps -> P_vector ps)
- ; p_vector_indexed = (fun ps -> P_vector_indexed ps)
; p_vector_concat = (fun ps -> P_vector_concat ps)
; p_tup = (fun ps -> P_tup ps)
; p_list = (fun ps -> P_list ps)
@@ -703,7 +687,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
; e_loop : loop * 'exp * 'exp -> 'exp_aux
; e_vector : 'exp list -> 'exp_aux
- ; e_vector_indexed : (int * 'exp) list * 'opt_default -> 'exp_aux
; e_vector_access : 'exp * 'exp -> 'exp_aux
; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux
; e_vector_update : 'exp * 'exp * 'exp -> 'exp_aux
@@ -749,8 +732,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; pat_exp : 'pat * 'exp -> 'pexp_aux
; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
- ; lB_val_explicit : typschm * 'pat * 'exp -> 'letbind_aux
- ; lB_val_implicit : 'pat * 'exp -> 'letbind_aux
+ ; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
}
@@ -770,8 +752,6 @@ let rec fold_exp_aux alg = function
| E_loop (loop_type, e1, e2) ->
alg.e_loop (loop_type, fold_exp alg e1, fold_exp alg e2)
| E_vector es -> alg.e_vector (List.map (fold_exp alg) es)
- | E_vector_indexed (es,opt) ->
- alg.e_vector_indexed (List.map (fun (id,e) -> (id,fold_exp alg e)) es, fold_opt_default alg opt)
| E_vector_access (e1,e2) -> alg.e_vector_access (fold_exp alg e1, fold_exp alg e2)
| E_vector_subrange (e1,e2,e3) ->
alg.e_vector_subrange (fold_exp alg e1, fold_exp alg e2, fold_exp alg e3)
@@ -831,8 +811,7 @@ and fold_pexp_aux alg = function
| Pat_when (pat,e,e') -> alg.pat_when (fold_pat alg.pat_alg pat, fold_exp alg e, fold_exp alg e')
and fold_pexp alg (Pat_aux (pexp_aux,annot)) = alg.pat_aux (fold_pexp_aux alg pexp_aux, annot)
and fold_letbind_aux alg = function
- | LB_val_explicit (t,pat,e) -> alg.lB_val_explicit (t,fold_pat alg.pat_alg pat, fold_exp alg e)
- | LB_val_implicit (pat,e) -> alg.lB_val_implicit (fold_pat alg.pat_alg pat, fold_exp alg e)
+ | LB_val (pat,e) -> alg.lB_val (fold_pat alg.pat_alg pat, fold_exp alg e)
and fold_letbind alg (LB_aux (letbind_aux,annot)) = alg.lB_aux (fold_letbind_aux alg letbind_aux, annot)
let id_exp_alg =
@@ -848,7 +827,6 @@ let id_exp_alg =
; e_for = (fun (id,e1,e2,e3,order,e4) -> E_for (id,e1,e2,e3,order,e4))
; e_loop = (fun (lt, e1, e2) -> E_loop (lt, e1, e2))
; e_vector = (fun es -> E_vector es)
- ; e_vector_indexed = (fun (es,opt2) -> E_vector_indexed (es,opt2))
; e_vector_access = (fun (e1,e2) -> E_vector_access (e1,e2))
; e_vector_subrange = (fun (e1,e2,e3) -> E_vector_subrange (e1,e2,e3))
; e_vector_update = (fun (e1,e2,e3) -> E_vector_update (e1,e2,e3))
@@ -894,8 +872,7 @@ let id_exp_alg =
; pat_exp = (fun (pat,e) -> (Pat_exp (pat,e)))
; pat_when = (fun (pat,e,e') -> (Pat_when (pat,e,e')))
; pat_aux = (fun (pexp,a) -> (Pat_aux (pexp,a)))
- ; lB_val_explicit = (fun (typ,pat,e) -> LB_val_explicit (typ,pat,e))
- ; lB_val_implicit = (fun (pat,e) -> LB_val_implicit (pat,e))
+ ; lB_val = (fun (pat,e) -> LB_val (pat,e))
; lB_aux = (fun (lb,annot) -> LB_aux (lb,annot))
; pat_alg = id_pat_alg
}
@@ -913,14 +890,10 @@ let compute_pat_alg bot join =
; p_as = (fun ((v,pat),id) -> (v, P_as (pat,id)))
; p_typ = (fun (typ,(v,pat)) -> (v, P_typ (typ,pat)))
; p_id = (fun id -> (bot, P_id id))
- ; p_var = (fun kid -> (bot, P_var kid))
+ ; p_var = (fun ((v,pat),kid) -> (v, P_var (pat,kid)))
; p_app = (fun (id,ps) -> split_join (fun ps -> P_app (id,ps)) ps)
; p_record = (fun (ps,b) -> split_join (fun ps -> P_record (ps,b)) ps)
; p_vector = split_join (fun ps -> P_vector ps)
- ; p_vector_indexed = (fun ps ->
- let (is,ps) = List.split ps in
- let (vs,ps) = List.split ps in
- (join_list vs, P_vector_indexed (List.combine is ps)))
; p_vector_concat = split_join (fun ps -> P_vector_concat ps)
; p_tup = split_join (fun ps -> P_tup ps)
; p_list = split_join (fun ps -> P_list ps)
@@ -947,10 +920,6 @@ let compute_exp_alg bot join =
; e_loop = (fun (lt, (v1, e1), (v2, e2)) ->
(join_list [v1;v2], E_loop (lt, e1, e2)))
; e_vector = split_join (fun es -> E_vector es)
- ; e_vector_indexed = (fun (es,(v2,opt2)) ->
- let (is,es) = List.split es in
- let (vs,es) = List.split es in
- (join_list (vs @ [v2]), E_vector_indexed (List.combine is es,opt2)))
; e_vector_access = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_access (e1,e2)))
; e_vector_subrange = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_subrange (e1,e2,e3)))
; e_vector_update = (fun ((v1,e1),(v2,e2),(v3,e3)) -> (join_list [v1;v2;v3], E_vector_update (e1,e2,e3)))
@@ -1005,8 +974,7 @@ let compute_exp_alg bot join =
; pat_exp = (fun ((vp,pat),(v,e)) -> (join vp v, Pat_exp (pat,e)))
; pat_when = (fun ((vp,pat),(v,e),(v',e')) -> (join_list [vp;v;v'], Pat_when (pat,e,e')))
; pat_aux = (fun ((v,pexp),a) -> (v, Pat_aux (pexp,a)))
- ; lB_val_explicit = (fun (typ,(vp,pat),(v,e)) -> (join vp v, LB_val_explicit (typ,pat,e)))
- ; lB_val_implicit = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val_implicit (pat,e)))
+ ; lB_val = (fun ((vp,pat),(v,e)) -> (join vp v, LB_val (pat,e)))
; lB_aux = (fun ((vl,lb),annot) -> (vl,LB_aux (lb,annot)))
; pat_alg = compute_pat_alg bot join
}
@@ -1188,7 +1156,6 @@ let rewrite_sizeof (Defs defs) =
; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4')))
; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2')))
; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es'))
- ; e_vector_indexed = (fun (es,(opt2,opt2')) -> let (is, es) = List.split es in let (es, es') = List.split es in let (es, es') = (List.combine is es, List.combine is es') in (E_vector_indexed (es,opt2), E_vector_indexed (es',opt2')))
; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2')))
; e_vector_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3')))
; e_vector_update = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_update (e1,e2,e3), E_vector_update (e1',e2',e3')))
@@ -1234,8 +1201,7 @@ let rewrite_sizeof (Defs defs) =
; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e')))
; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2')))
; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a)))
- ; lB_val_explicit = (fun (typ,pat,(e,e')) -> (LB_val_explicit (typ,pat,e), LB_val_explicit (typ,pat,e')))
- ; lB_val_implicit = (fun (pat,(e,e')) -> (LB_val_implicit (pat,e), LB_val_implicit (pat,e')))
+ ; lB_val = (fun (pat,(e,e')) -> (LB_val (pat,e), LB_val (pat,e')))
; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot)))
; pat_alg = id_pat_alg
} in
@@ -1307,12 +1273,9 @@ let rewrite_sizeof (Defs defs) =
| DEF_val (LB_aux (lb, annot)) ->
begin
let lb' = match lb with
- | LB_val_explicit (typschm, pat, exp) ->
- let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
- LB_val_explicit (typschm, pat, exp')
- | LB_val_implicit (pat, exp) ->
+ | LB_val (pat, exp) ->
let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
- LB_val_implicit (pat, exp') in
+ LB_val (pat, exp') in
(params_map, defs @ [DEF_val (LB_aux (lb', annot))])
end
| def ->
@@ -1337,15 +1300,10 @@ let rewrite_sizeof (Defs defs) =
TypSchm_aux (TypSchm_ts (tq, typ'), l)
else ts in
match def with
- | DEF_spec (VS_aux (VS_val_spec (typschm, id), a)) ->
- DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id), a))
- | DEF_spec (VS_aux (VS_extern_no_rename (typschm, id), a)) ->
- DEF_spec (VS_aux (VS_extern_no_rename (rewrite_typschm typschm id, id), a))
- | DEF_spec (VS_aux (VS_extern_spec (typschm, id, e), a)) ->
- DEF_spec (VS_aux (VS_extern_spec (rewrite_typschm typschm id, id, e), a))
- | DEF_spec (VS_aux (VS_cast_spec (typschm, id), a)) ->
- DEF_spec (VS_aux (VS_cast_spec (rewrite_typschm typschm id, id), a))
- | _ -> def in
+ | DEF_spec (VS_aux (VS_val_spec (typschm, id, ext, is_cast), a)) ->
+ DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id, ext, is_cast), a))
+ | def -> def
+ in
let (params_map, defs) = List.fold_left rewrite_sizeof_def
(Bindings.empty, []) defs in
@@ -1383,11 +1341,10 @@ let remove_vector_concat_pat pat =
; p_wild = P_wild
; p_as = (fun (pat,id) -> P_as (pat true,id))
; p_id = (fun id -> P_id id)
- ; p_var = (fun kid -> P_var kid)
+ ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
; p_record = (fun (fpats,b) -> P_record (fpats, b))
; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
- ; p_vector_indexed = (fun ps -> P_vector_indexed (List.map (fun (i,p) -> (i,p false)) ps))
; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps))
; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps))
@@ -1461,7 +1418,7 @@ let remove_vector_concat_pat pat =
match typ_opt with
| Some typ -> P_aux (P_typ (typ, P_aux (P_id child,cannot)), cannot)
| None -> P_aux (P_id child,cannot) in
- let letbind = fix_eff_lb (LB_aux (LB_val_implicit (id_pat,subv),cannot)) in
+ let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
(letbind,
(fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))),
(rootname,childname)) in
@@ -1514,17 +1471,13 @@ let remove_vector_concat_pat pat =
; p_as = (fun ((pat,decls),id) -> (P_as (pat,id),decls))
; p_typ = (fun (typ,(pat,decls)) -> (P_typ (typ,pat),decls))
; p_id = (fun id -> (P_id id,[]))
- ; p_var = (fun kid -> (P_var kid, []))
+ ; p_var = (fun ((pat,decls),kid) -> (P_var (pat,kid),decls))
; p_app = (fun (id,ps) -> let (ps,decls) = List.split ps in
(P_app (id,ps),List.flatten decls))
; p_record = (fun (ps,b) -> let (ps,decls) = List.split ps in
(P_record (ps,b),List.flatten decls))
; p_vector = (fun ps -> let (ps,decls) = List.split ps in
(P_vector ps,List.flatten decls))
- ; p_vector_indexed = (fun ps -> let (is,ps) = List.split ps in
- let (ps,decls) = List.split ps in
- let ps = List.combine is ps in
- (P_vector_indexed ps,List.flatten decls))
; p_vector_concat = (fun ps -> let (ps,decls) = List.split ps in
(P_vector_concat ps,List.flatten decls))
; p_tup = (fun ps -> let (ps,decls) = List.split ps in
@@ -1648,13 +1601,9 @@ let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp,(l,annot)) as ful
let (pat,_,decls) = remove_vector_concat_pat pat in
Pat_aux (Pat_when (pat, decls (rewrite_rec guard), decls (rewrite_rec body)),annot') in
rewrap (E_case (rewrite_rec e, List.map aux ps))
- | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) ->
+ | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
let (pat,_,decls) = remove_vector_concat_pat pat in
- rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'),
- decls (rewrite_rec body)))
- | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) ->
- let (pat,_,decls) = remove_vector_concat_pat pat in
- rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'),
+ rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'),
decls (rewrite_rec body)))
| exp -> rewrite_base full_exp
@@ -1678,14 +1627,10 @@ let rewrite_defs_remove_vector_concat (Defs defs) =
let rewrite_def d =
let d = rewriters.rewrite_def rewriters d in
match d with
- | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) ->
+ | DEF_val (LB_aux (LB_val (pat,exp),a)) ->
let (pat,letbinds,_) = remove_vector_concat_pat pat in
let defvals = List.map (fun lb -> DEF_val lb) letbinds in
- [DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a))] @ defvals
- | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) ->
- let (pat,letbinds,_) = remove_vector_concat_pat pat in
- let defvals = List.map (fun lb -> DEF_val lb) letbinds in
- [DEF_val (LB_aux (LB_val_implicit (pat,exp),a))] @ defvals
+ [DEF_val (LB_aux (LB_val (pat,exp),a))] @ defvals
| d -> [d] in
Defs (List.flatten (List.map rewrite_def defs))
@@ -1750,10 +1695,6 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
(match subsumes_pat pat1 pat2, subsumes_pat pats1 pats2 with
| Some substs1, Some substs2 -> Some (substs1 @ substs2)
| _ -> None)
- | P_vector_indexed ips1, P_vector_indexed ips2 ->
- let (is1,ps1) = List.split ips1 in
- let (is2,ps2) = List.split ips2 in
- if is1 = is2 then subsumes_list subsumes_pat ps1 ps2 else None
| _ -> None
and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
if id1 = id2 then subsumes_pat pat1 pat2 else None
@@ -1792,8 +1733,6 @@ let rec pat_to_exp (P_aux (pat,(l,annot))) =
| P_tup pats -> rewrap (E_tuple (List.map pat_to_exp pats))
| P_list pats -> rewrap (E_list (List.map pat_to_exp pats))
| P_cons (p,ps) -> rewrap (E_cons (pat_to_exp p, pat_to_exp ps))
- | P_vector_indexed ipats -> raise (Reporting_basic.err_unreachable l
- "pat_to_exp not implemented for P_vector_indexed") (* TODO *)
and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
@@ -1863,7 +1802,7 @@ let bitwise_and_exp exp1 exp2 =
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
| P_as (pat,_) | P_typ (_,pat) -> contains_bitvector_pat pat
-| P_vector _ | P_vector_concat _ | P_vector_indexed _ ->
+| P_vector _ | P_vector_concat _ ->
let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
is_bitvector_typ typ
| P_app (_,pats) | P_tup pats | P_list pats ->
@@ -1887,11 +1826,10 @@ let remove_bitvector_pat pat =
; p_wild = P_wild
; p_as = (fun (pat,id) -> P_as (pat true,id))
; p_id = (fun id -> P_id id)
- ; p_var = (fun kid -> P_var kid)
+ ; p_var = (fun (pat,kid) -> P_var (pat true,kid))
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
; p_record = (fun (fpats,b) -> P_record (fpats, b))
; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
- ; p_vector_indexed = (fun ps -> P_vector_indexed (List.map (fun (i,p) -> (i,p false)) ps))
; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps))
; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps))
@@ -1903,8 +1841,6 @@ let remove_bitvector_pat pat =
let (l,_) = annot in
match pat, is_bitvector_typ t, contained_in_p_as with
| P_vector _, true, false
- | P_vector_indexed _, true, false ->
- P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot)
| _ -> P_aux (pat,annot)
)
; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
@@ -1967,7 +1903,7 @@ let remove_bitvector_pat pat =
let rannot = simple_annot l typ in
let elem = access_bit_exp (rootid,rannot) l idx in
let e = P_aux (P_id id, simple_annot l bit_typ) in
- let letbind = LB_aux (LB_val_implicit (e,elem), simple_annot l bit_typ) in
+ let letbind = LB_aux (LB_val (e,elem), simple_annot l bit_typ) in
let letexp = (fun body ->
let (E_aux (_,(_,bannot))) = body in
E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in
@@ -2050,17 +1986,13 @@ let remove_bitvector_pat pat =
; p_as = (fun ((pat,gdls),id) -> (P_as (pat,id), gdls))
; p_typ = (fun (typ,(pat,gdls)) -> (P_typ (typ,pat), gdls))
; p_id = (fun id -> (P_id id, (None, (fun b -> b), [])))
- ; p_var = (fun kid -> (P_var kid, (None, (fun b -> b), [])))
+ ; p_var = (fun ((pat,gdls),kid) -> (P_var (pat,kid), gdls))
; p_app = (fun (id,ps) -> let (ps,gdls) = List.split ps in
(P_app (id,ps), flatten_guards_decls gdls))
; p_record = (fun (ps,b) -> let (ps,gdls) = List.split ps in
(P_record (ps,b), flatten_guards_decls gdls))
; p_vector = (fun ps -> let (ps,gdls) = List.split ps in
(P_vector ps, flatten_guards_decls gdls))
- ; p_vector_indexed = (fun p -> let (is,p) = List.split p in
- let (ps,gdls) = List.split p in
- let ps = List.combine is ps in
- (P_vector_indexed ps, flatten_guards_decls gdls))
; p_vector_concat = (fun ps -> let (ps,gdls) = List.split ps in
(P_vector_concat ps, flatten_guards_decls gdls))
; p_tup = (fun ps -> let (ps,gdls) = List.split ps in
@@ -2075,8 +2007,6 @@ let remove_bitvector_pat pat =
(match pat, is_bitvector_typ t with
| P_as (P_aux (P_vector ps, _), id), true ->
(P_aux (P_id id, annot), collect_guards_decls ps id t)
- | P_as (P_aux (P_vector_indexed ips, _), id), true ->
- (P_aux (P_id id, annot), collect_guards_decls_indexed ips id t)
| _, _ -> (P_aux (pat,annot), gdls)))
; fP_aux = (fun ((fpat,gdls),annot) -> (FP_aux (fpat,annot), gdls))
; fP_Fpat = (fun (id,(pat,gdls)) -> (FP_Fpat (id,pat), gdls))
@@ -2104,13 +2034,9 @@ let rewrite_exp_remove_bitvector_pat rewriters (E_aux (exp,(l,annot)) as full_ex
| Some guard' -> Pat_aux (Pat_when (pat', bitwise_and_exp guard guard', body'), annot')
| None -> Pat_aux (Pat_when (pat', guard, body'), annot')) in
rewrap (E_case (e, List.map rewrite_pexp ps))
- | E_let (LB_aux (LB_val_explicit (typ,pat,v),annot'),body) ->
- let (pat,(_,decls,_)) = remove_bitvector_pat pat in
- rewrap (E_let (LB_aux (LB_val_explicit (typ,pat,rewrite_rec v),annot'),
- decls (rewrite_rec body)))
- | E_let (LB_aux (LB_val_implicit (pat,v),annot'),body) ->
+ | E_let (LB_aux (LB_val (pat,v),annot'),body) ->
let (pat,(_,decls,_)) = remove_bitvector_pat pat in
- rewrap (E_let (LB_aux (LB_val_implicit (pat,rewrite_rec v),annot'),
+ rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'),
decls (rewrite_rec body)))
| _ -> rewrite_base full_exp
@@ -2141,14 +2067,10 @@ let rewrite_defs_remove_bitvector_pats (Defs defs) =
let rewrite_def d =
let d = rewriters.rewrite_def rewriters d in
match d with
- | DEF_val (LB_aux (LB_val_explicit (t,pat,exp),a)) ->
- let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in
- let defvals = List.map (fun lb -> DEF_val lb) letbinds in
- [DEF_val (LB_aux (LB_val_explicit (t,pat',exp),a))] @ defvals
- | DEF_val (LB_aux (LB_val_implicit (pat,exp),a)) ->
+ | DEF_val (LB_aux (LB_val (pat,exp),a)) ->
let (pat',(_,_,letbinds)) = remove_bitvector_pat pat in
let defvals = List.map (fun lb -> DEF_val lb) letbinds in
- [DEF_val (LB_aux (LB_val_implicit (pat',exp),a))] @ defvals
+ [DEF_val (LB_aux (LB_val (pat',exp),a))] @ defvals
| d -> [d] in
(* FIXME See above in rewrite_sizeof *)
(* fst (check initial_env ( *)
@@ -2179,7 +2101,7 @@ let rewrite_exp_guarded_pats rewriters (E_aux (exp,(l,annot)) as full_exp) =
let (E_aux (_,(el,eannot))) = e in
let pat_e' = fresh_id_pat "p__" (el, Some (env_of e, typ_of e, no_effect)) in
let exp_e' = pat_to_exp pat_e' in
- let letbind_e = LB_aux (LB_val_implicit (pat_e',e), (el,eannot)) in
+ let letbind_e = LB_aux (LB_val (pat_e',e), (el,eannot)) in
let exp' = case_exp exp_e' (typ_of full_exp) clauses in
rewrap (E_let (letbind_e, exp'))
else case_exp e (typ_of full_exp) clauses
@@ -2447,13 +2369,13 @@ let rewrite_constraint =
and rewrite_nc_aux = function
| NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
| NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2))
- | NC_fixed (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
+ | NC_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2))
| NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2))
| NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2)
| NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2)
| NC_false -> E_lit (mk_lit L_true)
| NC_true -> E_lit (mk_lit L_false)
- | NC_nat_set_bounded (kid, ints) ->
+ | NC_set (kid, ints) ->
unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (nc_eq (nvar kid) (nconstant int))) nc_true ints))
in
let rewrite_e_aux (E_aux (e_aux, _) as exp) =
@@ -2493,10 +2415,7 @@ let rewrite_dec_spec_typs rw_typ (DEC_aux (ds, annot)) =
let rewrite_overload_cast (Defs defs) =
let remove_cast_vs (VS_aux (vs_aux, annot)) =
match vs_aux with
- | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
- | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (typschm, id), annot)
- | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (typschm, id, e), annot)
- | VS_cast_spec (typschm, id) -> VS_aux (VS_val_spec (typschm, id), annot)
+ | VS_val_spec (typschm, id, ext, _) -> VS_aux (VS_val_spec (typschm, id, ext, false), annot)
in
let simple_def = function
| DEF_spec vs -> DEF_spec (remove_cast_vs vs)
@@ -2573,10 +2492,7 @@ let rewrite_simple_types (Defs defs) =
in
let simple_vs (VS_aux (vs_aux, annot)) =
match vs_aux with
- | VS_val_spec (typschm, id) -> VS_aux (VS_val_spec (simple_typschm typschm, id), annot)
- | VS_extern_no_rename (typschm, id) -> VS_aux (VS_extern_no_rename (simple_typschm typschm, id), annot)
- | VS_extern_spec (typschm, id, e) -> VS_aux (VS_extern_spec (simple_typschm typschm, id, e), annot)
- | VS_cast_spec (typschm, id) -> VS_aux (VS_cast_spec (simple_typschm typschm, id), annot)
+ | VS_val_spec (typschm, id, ext, is_cast) -> VS_aux (VS_val_spec (simple_typschm typschm, id, ext, is_cast), annot)
in
let rec simple_lit (L_aux (lit_aux, l) as lit) =
match lit_aux with
@@ -2593,7 +2509,7 @@ let rewrite_simple_types (Defs defs) =
let simple_pat = {
id_pat_alg with
p_typ = (fun (typ, pat) -> P_typ (simple_typ typ, pat));
- p_var = (fun kid -> P_id (id_of_kid kid));
+ p_var = (fun (pat, kid) -> unaux_pat pat);
p_vector = (fun pats -> P_list pats)
} in
let simple_exp = {
@@ -2654,7 +2570,7 @@ let rewrite_defs_remove_blocks =
let annot_pat = (simple_annot l (typ_of v)) in
let annot_lb = (Parse_ast.Generated l, tannot) in
let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
- E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
+ E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
let rec f l = function
| [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ))
@@ -2691,7 +2607,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
let pat = P_aux (P_wild,annot_pat) in
- E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
+ E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
| Some (env, typ, eff) ->
let id = fresh_id "w__" l in
let annot_pat = simple_annot l (typ_of v) in
@@ -2702,7 +2618,7 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
let pat = P_aux (P_id id,annot_pat) in
- E_aux (E_let (LB_aux (LB_val_implicit (pat,v),annot_lb),body),annot_let)
+ E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
| None ->
raise (Reporting_basic.err_unreachable l "no type information")
@@ -2766,12 +2682,9 @@ let rewrite_defs_letbind_effects =
and n_lb (lb : 'a letbind) (k : 'a letbind -> 'a exp) : 'a exp =
let (LB_aux (lb,annot)) = lb in
match lb with
- | LB_val_explicit (typ,pat,exp1) ->
+ | LB_val (pat,exp1) ->
n_exp exp1 (fun exp1 ->
- k (fix_eff_lb (LB_aux (LB_val_explicit (typ,pat,exp1),annot))))
- | LB_val_implicit (pat,exp1) ->
- n_exp exp1 (fun exp1 ->
- k (fix_eff_lb (LB_aux (LB_val_implicit (pat,exp1),annot))))
+ k (fix_eff_lb (LB_aux (LB_val (pat,exp1),annot))))
and n_lexp (lexp : 'a lexp) (k : 'a lexp -> 'a exp) : 'a exp =
let (LEXP_aux (lexp_aux,annot)) = lexp in
@@ -2857,12 +2770,6 @@ let rewrite_defs_letbind_effects =
| E_vector exps ->
n_exp_nameL exps (fun exps ->
k (rewrap (E_vector exps)))
- | E_vector_indexed (exps,opt_default) ->
- let (is,exps) = List.split exps in
- n_exp_nameL exps (fun exps ->
- n_opt_default opt_default (fun opt_default ->
- let exps = List.combine is exps in
- k (rewrap (E_vector_indexed (exps,opt_default)))))
| E_vector_access (exp1,exp2) ->
n_exp_name exp1 (fun exp1 ->
n_exp_name exp2 (fun exp2 ->
@@ -2966,10 +2873,8 @@ let rewrite_defs_letbind_effects =
let rewrap lb = DEF_val (LB_aux (lb, annot)) in
begin
match lb with
- | LB_val_implicit (pat, exp) ->
- rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp))
- | LB_val_explicit (ts, pat, exp) ->
- rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp))
+ | LB_val (pat, exp) ->
+ rewrap (LB_val (pat, n_exp_term (effectful exp) exp))
end
| DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef)
| d -> d in
@@ -2993,13 +2898,12 @@ let rewrite_defs_effectful_let_expressions =
let e_let (lb,body) =
match lb with
- | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
+ | LB_aux (LB_val (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) ->
(* Rewrite assignments to local variables into let bindings *)
let (lhs, rhs) = rewrite_local_lexp le in
- E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
- | LB_aux (LB_val_explicit (_,pat,exp'),annot')
- | LB_aux (LB_val_implicit (pat,exp'),annot') ->
+ E_let (LB_aux (LB_val (pat_of_local_lexp lhs, rhs exp), annot), body)
+ | LB_aux (LB_val (pat,exp'),annot') ->
if effectful exp'
then E_internal_plet (pat,exp',body)
else E_let (lb,body) in
@@ -3011,7 +2915,7 @@ let rewrite_defs_effectful_let_expressions =
if effectful exp1 then
E_internal_plet (P_aux (P_id id,annot),exp1,exp2)
else
- let lb = LB_aux (LB_val_implicit (P_aux (P_id id,annot), exp1), annot) in
+ let lb = LB_aux (LB_val (P_aux (P_id id,annot), exp1), annot) in
E_let (lb, exp2)
| _ -> failwith "E_internal_let with unexpected lexp" in
@@ -3294,20 +3198,13 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| E_let (lb,body) ->
let body = rewrite_var_updates body in
let (eff,lb) = match lb with
- | LB_aux (LB_val_implicit (pat,v),lbannot) ->
+ | LB_aux (LB_val (pat,v),lbannot) ->
(match rewrite v pat with
| Added_vars (v,pat) ->
let (E_aux (_,(l,_))) = v in
let lbannot = (simple_annot l (typ_of v)) in
- (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
- | Same_vars v -> (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot)))
- | LB_aux (LB_val_explicit (typ,pat,v),lbannot) ->
- (match rewrite v pat with
- | Added_vars (v,pat) ->
- let (E_aux (_,(l,_))) = v in
- let lbannot = (simple_annot l (typ_of v)) in
- (effect_of v,LB_aux (LB_val_implicit (pat,v),lbannot))
- | Same_vars v -> (effect_of v,LB_aux (LB_val_explicit (typ,pat,v),lbannot))) in
+ (effect_of v,LB_aux (LB_val (pat,v),lbannot))
+ | Same_vars v -> (effect_of v,LB_aux (LB_val (pat,v),lbannot))) in
let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in
E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot))
| E_internal_let (lexp,v,body) ->
@@ -3323,7 +3220,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let bodyeff = effect_of body in
let pat = P_aux (P_id id, (simple_annot l vtyp)) in
let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in
- let lb = LB_aux (LB_val_implicit (pat,v),lbannot) in
+ let lb = LB_aux (LB_val (pat,v),lbannot) in
let exp = E_aux (E_let (lb,body),(Parse_ast.Generated l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
rewrite_var_updates exp
| E_internal_plet (pat,v,body) ->
@@ -3378,21 +3275,15 @@ let rewrite_defs_remove_superfluous_letbinds =
| E_let (lb,exp2) ->
begin match lb,exp2 with
(* 'let x = EXP1 in x' can be replaced with 'EXP1' *)
- | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+ | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
E_aux (E_id (Id_aux (id',_)),_)
- | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_)
- | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_id (Id_aux (id',_)),_)
- | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+ | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
E_aux (E_cast (_,E_aux (E_id (Id_aux (id',_)),_)),_)
when id = id' ->
exp1
(* "let x = EXP1 in return x" can be replaced with 'return (EXP1)', at
least when EXP1 is 'small' enough *)
- | LB_aux (LB_val_explicit (_,P_aux (P_id (Id_aux (id,_)),_),exp1),_),
- E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
- | LB_aux (LB_val_implicit (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
+ | LB_aux (LB_val (P_aux (P_id (Id_aux (id,_)),_),exp1),_),
E_aux (E_internal_return (E_aux (E_id (Id_aux (id',_)),_)),_)
when id = id' && small exp1 ->
let (E_aux (_,e1annot)) = exp1 in
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 11394ec6..4b667793 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -66,11 +66,10 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
; p_as : 'pat * id -> 'pat_aux
; p_typ : Ast.typ * 'pat -> 'pat_aux
; p_id : id -> 'pat_aux
- ; p_var : kid -> 'pat_aux
+ ; p_var : 'pat * kid -> 'pat_aux
; p_app : id * 'pat list -> 'pat_aux
; p_record : 'fpat list * bool -> 'pat_aux
; p_vector : 'pat list -> 'pat_aux
- ; p_vector_indexed : (int * 'pat) list -> 'pat_aux
; p_vector_concat : 'pat list -> 'pat_aux
; p_tup : 'pat list -> 'pat_aux
; p_list : 'pat list -> 'pat_aux
@@ -99,7 +98,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; e_for : id * 'exp * 'exp * 'exp * Ast.order * 'exp -> 'exp_aux
; e_loop : loop * 'exp * 'exp -> 'exp_aux
; e_vector : 'exp list -> 'exp_aux
- ; e_vector_indexed : (int * 'exp) list * 'opt_default -> 'exp_aux
; e_vector_access : 'exp * 'exp -> 'exp_aux
; e_vector_subrange : 'exp * 'exp * 'exp -> 'exp_aux
; e_vector_update : 'exp * 'exp * 'exp -> 'exp_aux
@@ -145,8 +143,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
; pat_exp : 'pat * 'exp -> 'pexp_aux
; pat_when : 'pat * 'exp * 'exp -> 'pexp_aux
; pat_aux : 'pexp_aux * 'a annot -> 'pexp
- ; lB_val_explicit : typschm * 'pat * 'exp -> 'letbind_aux
- ; lB_val_implicit : 'pat * 'exp -> 'letbind_aux
+ ; lB_val : 'pat * 'exp -> 'letbind_aux
; lB_aux : 'letbind_aux * 'a annot -> 'letbind
; pat_alg : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg
}
diff --git a/src/sail.ml b/src/sail.ml
index 2270e1ef..8083b26c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -50,6 +50,7 @@ let opt_print_verbose = ref false
let opt_print_lem_ast = ref false
let opt_print_lem = ref false
let opt_print_ocaml = ref false
+let opt_convert = ref false
let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
@@ -100,6 +101,9 @@ let options = Arg.align ([
( "-just_check",
Arg.Set opt_just_check,
" (experimental) terminate immediately after typechecking");
+ ( "-convert",
+ Arg.Set opt_convert,
+ " Convert sail to new syntax");
( "-ddump_tc_ast",
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
@@ -145,6 +149,11 @@ let main() =
List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes)
-> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in
let ast = convert_ast Ast_util.inc_ord ast in
+
+ if !opt_convert
+ then (Pretty_print_sail2.pp_defs stdout ast; exit 0)
+ else ();
+
let (ast, type_envs) = check_ast ast in
let (ast, type_envs) =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index d349037e..2e368c53 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -291,8 +291,6 @@ let rec pat_bindings consider_var bound used (P_aux(p,(_,tannot))) =
List.fold_right (fun (Ast.FP_aux(Ast.FP_Fpat(_,p),_)) (b,n) ->
pat_bindings consider_var bound used p) fpats (bound,used)
| P_vector pats | Ast.P_vector_concat pats | Ast.P_tup pats | Ast.P_list pats -> list_fv bound used pats
- | P_vector_indexed ipats ->
- List.fold_right (fun (_,p) (b,n) -> pat_bindings consider_var b n p) ipats (bound,used)
| _ -> bound,used
let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.t * Nameset.t * Nameset.t) =
@@ -317,13 +315,6 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
| E_for(id,from,to_,by,_,body) ->
let _,used,set = list_fv bound used set [from;to_;by] in
fv_of_exp consider_var (Nameset.add (string_of_id id) bound) used set body
- | E_vector_indexed (es_i,(Ast.Def_val_aux(default,_))) ->
- let bound,used,set =
- List.fold_right
- (fun (_,e) (b,u,s) -> fv_of_exp consider_var b u s e) es_i (bound,used,set) in
- (match default with
- | Def_val_empty -> bound,used,set
- | Def_val_dec e -> fv_of_exp consider_var bound used set e)
| E_vector_access(v,i) -> list_fv bound used set [v;i]
| E_vector_subrange(v,i1,i2) -> list_fv bound used set [v;i1;i2]
| E_vector_update(v,i,e) -> list_fv bound used set [v;i;e]
@@ -367,12 +358,7 @@ and fv_of_pes consider_var bound used set pes =
fv_of_pes consider_var bound us_e set_e pes
and fv_of_let consider_var bound used set (LB_aux(lebind,_)) = match lebind with
- | LB_val_explicit(typsch,pat,exp) ->
- let bound_t,us_t = fv_of_typschm consider_var bound used typsch in
- let bound_p, us_p = pat_bindings consider_var (Nameset.union bound bound_t) used pat in
- let _,us_e,set_e = fv_of_exp consider_var (Nameset.union bound bound_t) used set exp in
- (Nameset.union bound_t bound_p),Nameset.union us_t (Nameset.union us_p us_e),set_e
- | LB_val_implicit(pat,exp) ->
+ | LB_val(pat,exp) ->
let bound_p, us_p = pat_bindings consider_var bound used pat in
let _,us_e,set_e = fv_of_exp consider_var bound used set exp in
bound_p,Nameset.union us_p us_e,set_e
@@ -423,19 +409,6 @@ let typ_variants consider_var bound tunions =
let fv_of_kind_def consider_var (KD_aux(k,_)) = match k with
| KD_nabbrev(_,id,_,nexp) -> init_env (string_of_id id), fv_of_nexp consider_var mt mt nexp
- | KD_abbrev(_,id,_,typschm) ->
- init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
- | KD_record(_,id,_,typq,tids,_) ->
- let binds = init_env (string_of_id id) in
- let bounds = if consider_var then typq_bindings typq else mt in
- binds, List.fold_right (fun (t,_) n -> fv_of_typ consider_var bounds n t) tids mt
- | KD_variant(_,id,_,typq,tunions,_) ->
- let bindings = Nameset.add (string_of_id id) (if consider_var then typq_bindings typq else mt) in
- typ_variants consider_var bindings tunions
- | KD_enum(_,id,_,ids,_) ->
- Nameset.of_list (List.map string_of_id (id::ids)),mt
- | KD_register(_,id,n1,n2,_) ->
- init_env (string_of_id id), fv_of_nexp consider_var mt (fv_of_nexp consider_var mt mt n1) n2
let fv_of_type_def consider_var (TD_aux(t,_)) = match t with
| TD_abbrev(id,_,typschm) -> init_env (string_of_id id), snd (fv_of_typschm consider_var mt mt typschm)
@@ -487,8 +460,7 @@ let fv_of_fun consider_var (FD_aux (FD_function(rec_opt,tannot_opt,_,funcls),_))
init_env fun_name,Nameset.union ns ns_r
let fv_of_vspec consider_var (VS_aux(vspec,_)) = match vspec with
- | VS_val_spec(ts,id) | VS_extern_no_rename (ts,id) | VS_extern_spec(ts,id,_)
- | VS_cast_spec(ts,id) ->
+ | VS_val_spec(ts,id,_,_) ->
init_env ("val:" ^ (string_of_id id)), snd (fv_of_typschm consider_var mt mt ts)
let rec find_scattered_of name = function
diff --git a/src/type_check.ml b/src/type_check.ml
index 07d09f42..d5b3de0b 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -157,16 +157,16 @@ let rec nc_negate (NC_aux (nc, _)) =
match nc with
| NC_bounded_ge (n1, n2) -> nc_lt n1 n2
| NC_bounded_le (n1, n2) -> nc_gt n1 n2
- | NC_fixed (n1, n2) -> nc_neq n1 n2
+ | NC_equal (n1, n2) -> nc_neq n1 n2
| NC_not_equal (n1, n2) -> nc_eq n1 n2
| NC_and (n1, n2) -> mk_nc (NC_or (nc_negate n1, nc_negate n2))
| NC_or (n1, n2) -> mk_nc (NC_and (nc_negate n1, nc_negate n2))
| NC_false -> mk_nc NC_true
| NC_true -> mk_nc NC_false
- | NC_nat_set_bounded (kid, []) -> nc_false
- | NC_nat_set_bounded (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
- | NC_nat_set_bounded (kid, int :: ints) ->
- mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_nat_set_bounded (kid, ints)))))
+ | NC_set (kid, []) -> nc_false
+ | NC_set (kid, [int]) -> nc_neq (nvar kid) (nconstant int)
+ | NC_set (kid, int :: ints) ->
+ mk_nc (NC_and (nc_neq (nvar kid) (nconstant int), nc_negate (mk_nc (NC_set (kid, ints)))))
(* Utilities for constructing effect sets *)
@@ -230,15 +230,15 @@ and nexp_subst_aux sv subst = function
let rec nexp_set_to_or l subst = function
| [] -> typ_error l "Cannot substitute into empty nexp set"
- | [int] -> NC_fixed (subst, nconstant int)
- | (int :: ints) -> NC_or (mk_nc (NC_fixed (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
+ | [int] -> NC_equal (subst, nconstant int)
+ | (int :: ints) -> NC_or (mk_nc (NC_equal (subst, nconstant int)), mk_nc (nexp_set_to_or l subst ints))
let rec nc_subst_nexp sv subst (NC_aux (nc, l)) = NC_aux (nc_subst_nexp_aux l sv subst nc, l)
and nc_subst_nexp_aux l sv subst = function
- | NC_fixed (n1, n2) -> NC_fixed (nexp_subst sv subst n1, nexp_subst sv subst n2)
+ | NC_equal (n1, n2) -> NC_equal (nexp_subst sv subst n1, nexp_subst sv subst n2)
| NC_bounded_ge (n1, n2) -> NC_bounded_ge (nexp_subst sv subst n1, nexp_subst sv subst n2)
| NC_bounded_le (n1, n2) -> NC_bounded_le (nexp_subst sv subst n1, nexp_subst sv subst n2)
- | NC_nat_set_bounded (kid, ints) as set_nc ->
+ | NC_set (kid, ints) as set_nc ->
if Kid.compare kid sv = 0
then nexp_set_to_or l (mk_nexp subst) ints
else set_nc
@@ -781,11 +781,11 @@ end = struct
let rec wf_constraint env (NC_aux (nc, _)) =
match nc with
- | NC_fixed (n1, n2) -> wf_nexp env n1; wf_nexp env n2
+ | NC_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2
| NC_not_equal (n1, n2) -> wf_nexp env n1; wf_nexp env n2
| NC_bounded_ge (n1, n2) -> wf_nexp env n1; wf_nexp env n2
| NC_bounded_le (n1, n2) -> wf_nexp env n1; wf_nexp env n2
- | NC_nat_set_bounded (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
+ | NC_set (kid, ints) -> () (* MAYBE: We could demand that ints are all unique here *)
| NC_or (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2
| NC_and (nc1, nc2) -> wf_constraint env nc1; wf_constraint env nc2
| NC_true | NC_false -> ()
@@ -1069,12 +1069,12 @@ let rec nexp_constraint env var_of (Nexp_aux (nexp, l)) =
let rec nc_constraint env var_of (NC_aux (nc, l)) =
match nc with
- | NC_fixed (nexp1, nexp2) -> Constraint.eq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
+ | NC_equal (nexp1, nexp2) -> Constraint.eq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_not_equal (nexp1, nexp2) -> Constraint.neq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_bounded_ge (nexp1, nexp2) -> Constraint.gteq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
| NC_bounded_le (nexp1, nexp2) -> Constraint.lteq (nexp_constraint env var_of nexp1) (nexp_constraint env var_of nexp2)
- | NC_nat_set_bounded (_, []) -> Constraint.literal false
- | NC_nat_set_bounded (kid, (int :: ints)) ->
+ | NC_set (_, []) -> Constraint.literal false
+ | NC_set (kid, (int :: ints)) ->
List.fold_left Constraint.disj
(Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int int)))
(List.map (fun i -> Constraint.eq (nexp_constraint env var_of (nvar kid)) (Constraint.constant (big_int_of_int i))) ints)
@@ -1116,10 +1116,10 @@ let prove env (NC_aux (nc_aux, _) as nc) =
| _, _ -> false
in
match nc_aux with
- | NC_fixed (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
+ | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 = c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
| NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
| NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 >= c2) (nexp_simp nexp1) (nexp_simp nexp2) -> true
- | NC_fixed (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
+ | NC_equal (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 <> c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_bounded_le (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 > c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_bounded_ge (nexp1, nexp2) when compare_const (fun c1 c2 -> c1 < c2) (nexp_simp nexp1) (nexp_simp nexp2) -> false
| NC_true -> true
@@ -1179,7 +1179,7 @@ let rec subtyp_tnf env tnf1 tnf2 =
and tnf_args_eq env arg1 arg2 =
match arg1, arg2 with
- | Tnf_arg_nexp n1, Tnf_arg_nexp n2 -> prove env (NC_aux (NC_fixed (n1, n2), Parse_ast.Unknown))
+ | Tnf_arg_nexp n1, Tnf_arg_nexp n2 -> prove env (NC_aux (NC_equal (n1, n2), Parse_ast.Unknown))
| Tnf_arg_order ord1, Tnf_arg_order ord2 -> order_eq ord1 ord2
| Tnf_arg_typ tnf1, Tnf_arg_typ tnf2 -> subtyp_tnf env tnf1 tnf2 && subtyp_tnf env tnf2 tnf1
| _, _ -> assert false
@@ -1278,7 +1278,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
if KidSet.is_empty (KidSet.inter (nexp_frees nexp1) goals)
then
begin
- if prove env (NC_aux (NC_fixed (nexp1, nexp2), Parse_ast.Unknown))
+ if prove env (NC_aux (NC_equal (nexp1, nexp2), Parse_ast.Unknown))
then None
else unify_error l ("Nexp " ^ string_of_nexp nexp1 ^ " and " ^ string_of_nexp nexp2 ^ " are not equal")
end
@@ -1309,7 +1309,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1a, n2a), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1a, n2a), Parse_ast.Unknown)) ->
unify_nexps l env goals n1b n2b
| Nexp_constant c2 ->
begin
@@ -1324,7 +1324,7 @@ let rec unify_nexps l env goals (Nexp_aux (nexp_aux1, _) as nexp1) (Nexp_aux (ne
then
begin
match nexp_aux2 with
- | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_fixed (n1b, n2b), Parse_ast.Unknown)) ->
+ | Nexp_times (n2a, n2b) when prove env (NC_aux (NC_equal (n1b, n2b), Parse_ast.Unknown)) ->
unify_nexps l env goals n1a n2a
| _ -> unify_error l ("Cannot unify Nat expression " ^ string_of_nexp nexp1 ^ " with " ^ string_of_nexp nexp2)
end
@@ -1950,15 +1950,14 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
begin
match letbind with
- | LB_val_explicit (typschm, pat, bind) -> assert false
- | LB_val_implicit (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
+ | LB_val (P_aux (P_typ (ptyp, _), _) as pat, bind) ->
let checked_bind = crule check_exp env bind ptyp in
let tpat, env = bind_pat env pat ptyp in
- annot_exp (E_let (LB_aux (LB_val_implicit (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
- | LB_val_implicit (pat, bind) ->
+ annot_exp (E_let (LB_aux (LB_val (tpat, checked_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+ | LB_val (pat, bind) ->
let inferred_bind = irule infer_exp env bind in
let tpat, env = bind_pat env pat (typ_of inferred_bind) in
- annot_exp (E_let (LB_aux (LB_val_implicit (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
+ annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
end
| E_app_infix (x, op, y), _ when List.length (Env.get_overloads (deinfix op) env) > 0 ->
check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
@@ -2114,22 +2113,22 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
| Unification_error (l, m) -> typ_error l ("Unification error when pattern matching against union constructor: " ^ m)
end
end
- | P_var kid ->
+ | P_var (pat, kid) ->
+ let typ = Env.expand_synonyms env typ in
begin
- let v = id_of_kid kid in
- match Env.lookup_id v env with
- | Local (Immutable, _) | Unbound ->
- begin
- match destruct_exist env typ with
- | Some ([kid'], nc, typ) ->
- let env = Env.add_typ_var kid BK_nat env in
- let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in
- let env = Env.add_local v (Immutable, typ_subst_nexp kid' (Nexp_var kid) typ) env in
- annot_pat (P_var kid) typ, env
- | Some _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential")
- | None _ -> typ_error l ("Cannot bind type variable against non existential type")
- end
- | _ -> typ_error l ("Bad type identifer pattern: " ^ string_of_pat pat)
+ match destruct_exist env typ, typ with
+ | Some ([kid'], nc, ex_typ), _ ->
+ let env = Env.add_typ_var kid BK_nat env in
+ let ex_typ = typ_subst_nexp kid' (Nexp_var kid) ex_typ in
+ let env = Env.add_constraint (nc_subst_nexp kid' (Nexp_var kid) nc) env in
+ let typed_pat, env = bind_pat env pat ex_typ in
+ annot_pat (P_var (typed_pat, kid)) typ, env
+ | Some _, _ -> typ_error l ("Cannot bind type variable pattern against multiple argument existential")
+ | None, Typ_aux (Typ_id id, _) when Id.compare id (mk_id "int") == 0 ->
+ let env = Env.add_typ_var kid BK_nat env in
+ let typed_pat, env = bind_pat env pat (atom_typ (nvar kid)) in
+ annot_pat (P_var (typed_pat, kid)) typ, env
+ | None, _ -> typ_error l ("Cannot bind type variable against non existential type")
end
| P_wild -> annot_pat P_wild typ, env
| P_cons (hd_pat, tl_pat) ->
@@ -2958,7 +2957,9 @@ and propagate_pat_effect_aux = function
let p_pat = propagate_pat_effect pat in
P_typ (typ, p_pat), effect_of_pat p_pat
| P_id id -> P_id id, no_effect
- | P_var kid -> P_var kid, no_effect
+ | P_var (pat, kid) ->
+ let p_pat = propagate_pat_effect pat in
+ P_var (p_pat, kid), effect_of_pat p_pat
| P_app (id, pats) ->
let p_pats = List.map propagate_pat_effect pats in
P_app (id, p_pats), collect_effects_pat p_pats
@@ -2982,15 +2983,10 @@ and propagate_letbind_effect (LB_aux (lb, (l, annot))) =
| Some (typq, typ, eff) -> LB_aux (p_lb, (l, Some (typq, typ, eff))), eff
| None -> LB_aux (p_lb, (l, None)), eff
and propagate_letbind_effect_aux = function
- | LB_val_explicit (typschm, pat, exp) ->
+ | LB_val (pat, exp) ->
let p_pat = propagate_pat_effect pat in
let p_exp = propagate_exp_effect exp in
- LB_val_explicit (typschm, p_pat, p_exp),
- union_effects (effect_of_pat p_pat) (effect_of p_exp)
- | LB_val_implicit (pat, exp) ->
- let p_pat = propagate_pat_effect pat in
- let p_exp = propagate_exp_effect exp in
- LB_val_implicit (p_pat, p_exp),
+ LB_val (p_pat, p_exp),
union_effects (effect_of_pat p_pat) (effect_of p_exp)
and propagate_lexp_effect (LEXP_aux (lexp, annot)) =
@@ -3027,15 +3023,14 @@ and propagate_lexp_effect_aux = function
let check_letdef env (LB_aux (letbind, (l, _))) =
begin
match letbind with
- | LB_val_explicit (typschm, pat, bind) -> assert false
- | LB_val_implicit (P_aux (P_typ (typ_annot, pat), _), bind) ->
+ | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) ->
let checked_bind = crule check_exp env (strip_exp bind) typ_annot in
let tpat, env = bind_pat env (strip_pat pat) typ_annot in
- [DEF_val (LB_aux (LB_val_implicit (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env
- | LB_val_implicit (pat, bind) ->
+ [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+ | LB_val (pat, bind) ->
let inferred_bind = irule infer_exp env (strip_exp bind) in
let tpat, env = bind_pat env (strip_pat pat) (typ_of inferred_bind) in
- [DEF_val (LB_aux (LB_val_implicit (tpat, inferred_bind), (l, None)))], env
+ [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
end
let check_funcl env (FCL_aux (FCL_Funcl (id, pat, exp), (l, _))) typ =
@@ -3074,7 +3069,7 @@ let infer_funtyp l env tannotopt funcls =
end
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> typ_error l "Cannot infer function type for unannotated function"
-let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id), (Parse_ast.Unknown, None)))
+let mk_val_spec typq typ id = DEF_spec (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown), id, None, false), (Parse_ast.Unknown, None)))
let check_tannotopt env typq ret_typ = function
| Typ_annot_opt_aux (Typ_annot_opt_none, _) -> ()
@@ -3125,14 +3120,13 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
the difference is irrelevant for the typechecker. *)
let check_val_spec env (VS_aux (vs, (l, _))) =
let (id, quants, typ, env) = match vs with
- | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, env)
- | VS_cast_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id) -> (id, quants, typ, Env.add_cast id env)
- | VS_extern_no_rename (TypSchm_aux (TypSchm_ts (quants, typ), _), id) ->
- let env = Env.add_extern id (string_of_id id) env in
- (id, quants, typ, env)
- | VS_extern_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext) ->
- let env = Env.add_extern id ext env in
- (id, quants, typ, env) in
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, false) -> (id, quants, typ, env)
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, true) -> (id, quants, typ, Env.add_cast id env)
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, Some ext, false) ->
+ let env = Env.add_extern id ext env in
+ (id, quants, typ, env)
+ | _ -> typ_error l "Invalid valspec"
+ in
[DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env
let check_default env (DT_aux (ds, l)) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 19:06:03 +0000