summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast.ml26
-rw-r--r--src/ast_util.ml35
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/constraint.ml82
-rw-r--r--src/constraint.mli9
-rw-r--r--src/gen_lib/sail_operators.lem20
-rw-r--r--src/gen_lib/sail_operators_mwords.lem14
-rw-r--r--src/gen_lib/sail_values.lem27
-rw-r--r--src/initial_check.ml168
-rw-r--r--src/lexer2.mll40
-rw-r--r--src/monomorphise.ml42
-rw-r--r--src/ocaml_backend.ml22
-rw-r--r--src/parse_ast.ml28
-rw-r--r--src/parser.mly69
-rw-r--r--src/parser2.mly154
-rw-r--r--src/pretty_print_common.ml4
-rw-r--r--src/pretty_print_lem.ml174
-rw-r--r--src/pretty_print_lem_ast.ml64
-rw-r--r--src/pretty_print_ocaml.ml92
-rw-r--r--src/pretty_print_sail.ml100
-rw-r--r--src/pretty_print_sail2.ml370
-rw-r--r--src/process_file.ml60
-rw-r--r--src/reporting_basic.ml18
-rw-r--r--src/rewriter.ml465
-rw-r--r--src/rewriter.mli11
-rw-r--r--src/sail.ml19
-rw-r--r--src/spec_analysis.ml32
-rw-r--r--src/type_check.ml314
-rw-r--r--src/type_check.mli3
29 files changed, 1383 insertions, 1081 deletions
diff --git a/src/ast.ml b/src/ast.ml
index 1728f492..6f702a78 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -57,7 +57,6 @@ base_kind_aux = (* base kind *)
BK_type (* kind of types *)
| BK_nat (* kind of natural number size expressions *)
| BK_order (* kind of vector order specifications *)
- | BK_effect (* kind of effect sets *)
type
@@ -168,11 +167,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 +259,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 +303,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 +375,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 +491,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
@@ -567,6 +553,7 @@ type
'a dec_spec =
DEC_aux of 'a dec_spec_aux * 'a annot
+type prec = Infix | InfixL | InfixR
type
'a dec_comm = (* Top-level generated comments *)
@@ -579,6 +566,7 @@ and 'a def = (* Top-level definition *)
| DEF_fundef of 'a fundef (* function definition *)
| DEF_val of 'a letbind (* value definition *)
| DEF_spec of 'a val_spec (* top-level type constraint *)
+ | DEF_fixity of prec * int * id (* fixity declaration *)
| DEF_overload of id * id list (* operator overload specification *)
| DEF_default of 'a default_spec (* default kind and type assumptions *)
| DEF_scattered of 'a scattered_def (* scattered function and type definition *)
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 048fbb15..daaf5725 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)
@@ -209,6 +210,13 @@ let quant_items : typquant -> quant_item list = function
| TypQ_aux (TypQ_tq qis, _) -> qis
| TypQ_aux (TypQ_no_forall, _) -> []
+let quant_kopts typq =
+ let qi_kopt = function
+ | QI_aux (QI_id kopt, _) -> [kopt]
+ | QI_aux _ -> []
+ in
+ quant_items typq |> List.map qi_kopt |> List.concat
+
let rec map_exp_annot f (E_aux (exp, annot)) = E_aux (map_exp_annot_aux f exp, f annot)
and map_exp_annot_aux f = function
| E_block xs -> E_block (List.map (map_exp_annot f) xs)
@@ -223,8 +231,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 +278,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
@@ -343,7 +347,6 @@ let string_of_base_kind_aux = function
| BK_type -> "Type"
| BK_nat -> "Nat"
| BK_order -> "Order"
- | BK_effect -> "Effect"
let string_of_base_kind (BK_aux (bk, _)) = string_of_base_kind_aux bk
@@ -395,7 +398,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 +406,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 +512,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 +535,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
@@ -654,6 +655,8 @@ let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
let rec is_number (Typ_aux (t,_)) =
match t with
+ | Typ_id (Id_aux (Id "int", _))
+ | Typ_id (Id_aux (Id "nat", _))
| Typ_app (Id_aux (Id "range", _),_)
| Typ_app (Id_aux (Id "implicit", _),_)
| Typ_app (Id_aux (Id "atom", _),_) -> true
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 33d65ede..7ab7807a 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
@@ -127,6 +128,7 @@ val nc_false : n_constraint
val nc_set : kid -> int list -> n_constraint
val quant_items : typquant -> quant_item list
+val quant_kopts : typquant -> kinded_id list
(* Functions to map over the annotations in sub-expressions *)
val map_exp_annot : ('a annot -> 'b annot) -> 'a exp -> 'b exp
diff --git a/src/constraint.ml b/src/constraint.ml
index e8252f2a..37d1fae9 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -212,7 +212,44 @@ let smtlib_of_constraint constr : string =
type t = nexp constraint_bool
-type smt_result = Unknown of t list | Unsat of t
+type smt_result = Unknown | Sat | Unsat
+
+module DigestMap = Map.Make(Digest)
+
+let known_problems = ref (DigestMap.empty)
+
+let load_digests_err () =
+ let in_chan = open_in_bin "z3_problems" in
+ let rec load () =
+ let digest = Digest.input in_chan in
+ let result = input_byte in_chan in
+ begin
+ match result with
+ | 0 -> known_problems := DigestMap.add digest Unknown !known_problems
+ | 1 -> known_problems := DigestMap.add digest Sat !known_problems
+ | 2 -> known_problems := DigestMap.add digest Unsat !known_problems
+ | _ -> assert false
+ end;
+ load ()
+ in
+ try load () with
+ | End_of_file -> close_in in_chan
+
+let load_digests () =
+ try load_digests_err () with
+ | Sys_error _ -> ()
+
+let save_digests () =
+ let out_chan = open_out_bin "z3_problems" in
+ let output digest result =
+ Digest.output out_chan digest;
+ match result with
+ | Unknown -> output_byte out_chan 0
+ | Sat -> output_byte out_chan 1
+ | Unsat -> output_byte out_chan 2
+ in
+ DigestMap.iter output !known_problems;
+ close_out out_chan
let rec call_z3 constraints : smt_result =
let problems = unbranch constraints in
@@ -235,24 +272,31 @@ let rec call_z3 constraints : smt_result =
end
in
- begin
- let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
- output_string tmp_chan z3_file;
- close_out tmp_chan;
- let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
- let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
- let _ = Unix.close_process_in z3_chan in
- Sys.remove input_file;
- try
- let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
- Unsat problem
- with
- | Not_found ->
- z3_output
- |> List.filter (fun (_, result) -> result = "unknown")
- |> List.map fst
- |> (fun unsolved -> Unknown unsolved)
- end
+ let digest = Digest.string z3_file in
+ try
+ let result = DigestMap.find digest !known_problems in
+ result
+ with
+ | Not_found ->
+ begin
+ let (input_file, tmp_chan) = Filename.open_temp_file "constraint_" ".sat" in
+ output_string tmp_chan z3_file;
+ close_out tmp_chan;
+ let z3_chan = Unix.open_process_in ("z3 -t:1000 -T:10 " ^ input_file) in
+ let z3_output = List.combine problems (input_lines z3_chan (List.length problems)) in
+ let _ = Unix.close_process_in z3_chan in
+ Sys.remove input_file;
+ try
+ let (problem, _) = List.find (fun (_, result) -> result = "unsat") z3_output in
+ known_problems := DigestMap.add digest Unsat !known_problems;
+ Unsat
+ with
+ | Not_found ->
+ let unsolved = List.filter (fun (_, result) -> result = "unknown") z3_output in
+ if unsolved == []
+ then (known_problems := DigestMap.add digest Sat !known_problems; Sat)
+ else (known_problems := DigestMap.add digest Unknown !known_problems; Unknown)
+ end
let string_of constr =
constr
diff --git a/src/constraint.mli b/src/constraint.mli
index 3fb3d2f6..ad75f453 100644
--- a/src/constraint.mli
+++ b/src/constraint.mli
@@ -1,12 +1,15 @@
type nexp
type t
-type smt_result = Unknown of t list | Unsat of t
-
+type smt_result = Unknown | Sat | Unsat
+
+val load_digests : unit -> unit
+val save_digests : unit -> unit
+
val call_z3 : t -> smt_result
val string_of : t -> string
-
+
val implies : t -> t -> t
val conj : t -> t -> t
val disj : t -> t -> t
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 32d06caf..30c7325e 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -5,7 +5,7 @@ open import Sail_values
(*** Bit vector operations *)
-let bvlength = length
+let bitvector_length = length
let set_bitvector_start = set_vector_start
let reset_bitvector_start = reset_vector_start
@@ -25,8 +25,10 @@ let vector_subrange_bl_dec = vector_subrange_bl
let bitvector_access_inc = vector_access_inc
let bitvector_access_dec = vector_access_dec
-let bitvector_update_pos_dec = update_pos
-let bitvector_update_subrange_dec = vector_update_dec
+let bitvector_update_pos_inc = vector_update_pos_inc
+let bitvector_update_pos_dec = vector_update_pos_dec
+let bitvector_update_subrange_inc = vector_update_subrange_inc
+let bitvector_update_subrange_dec = vector_update_subrange_dec
let extract_only_bit = extract_only_element
@@ -197,18 +199,8 @@ let extz_bl (start, len, bits) = Vector bits start false
let exts_bl (start, len, bits) = Vector bits start false
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
let (l',r') = (to_num sign l, to_num sign r) in
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem
index e0e66c3e..8fb158de 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail_operators_mwords.lem
@@ -5,7 +5,7 @@ open import Sail_values
(*** Bit vector operations *)
-let bvlength bs = integerFromNat (word_length bs)
+let bitvector_length bs = integerFromNat (word_length bs)
(*val set_bitvector_start : forall 'a. (integer * bitvector 'a) -> bitvector 'a
let set_bitvector_start (new_start, Bitvector bs _ is_inc) =
@@ -240,18 +240,8 @@ let extz_big (start, len, vec) = to_vec_big (unsigned_big vec)
let extz_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
let exts_bl (start, len, bits) = vec_to_bvec (Vector bits (integerFromNat (List.length bits - 1)) false)
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
(* TODO: this, and the definitions that use it, currently require Size for
to_vec, which I'd rather avoid in favour of library versions; the
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index b0de85e0..906b35a8 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -13,6 +13,26 @@ let pow m n = m ** (natFromInteger n)
let pow2 n = pow 2 n
+let add_int (l,r) = integerAdd l r
+let add_signed (l,r) = integerAdd l r
+let sub_int (l,r) = integerMinus l r
+let mult_int (l,r) = integerMult l r
+let quotient_int (l,r) = integerDiv l r
+let quotient_nat (l,r) = natDiv l r
+let power_int_nat (l,r) = integerPow l r
+let power_int_int (l, r) = integerPow l (natFromInteger r)
+let negate_int i = integerNegate i
+let min_int (l, r) = integerMin l r
+let max_int (l, r) = integerMax l r
+
+let add_real (l, r) = realAdd l r
+let sub_real (l, r) = realMinus l r
+let mult_real (l, r) = realMult l r
+let div_real (l, r) = realDiv l r
+let negate_real r = realNegate r
+let abs_real r = realAbs r
+let power_real (b, e) = realPowInteger b e
+
let bool_or (l, r) = (l || r)
let bool_and (l, r) = (l && r)
let bool_xor (l, r) = xor l r
@@ -226,8 +246,8 @@ val update : forall 'a. vector 'a -> integer -> integer -> vector 'a -> vector '
let update (Vector bs start is_inc) i j (Vector bs' _ _) =
Vector (update_aux is_inc start bs i j bs') start is_inc
-let vector_update_inc (start, v, i, j, v') = update v i j v'
-let vector_update_dec (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_inc (start, v, i, j, v') = update v i j v'
+let vector_update_subrange_dec (start, v, i, j, v') = update v i j v'
val access_aux : forall 'a. bool -> integer -> list 'a -> integer -> 'a
let access_aux is_inc start xs n =
@@ -244,6 +264,9 @@ val update_pos : forall 'a. vector 'a -> integer -> 'a -> vector 'a
let update_pos v n b =
update v n n (Vector [b] 0 false)
+let vector_update_pos_inc (start, v, i, x) = update_pos v i x
+let vector_update_pos_dec (start, v, i, x) = update_pos v i x
+
let extract_only_element (Vector elems _ _) = match elems with
| [] -> failwith "extract_only_element called for empty vector"
| [e] -> e
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 83c79646..a9201c1f 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -128,7 +128,6 @@ let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
| Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
| Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat }
| Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord }
- | Parse_ast.BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct }
let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) =
match klst with
@@ -311,10 +310,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 +326,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 +417,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 +428,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 +438,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 +465,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 +563,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 +590,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) ->
+ | Parse_ast.VS_val_spec(ts,id,ext,is_cast) ->
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) ->
- 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 +680,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 +690,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
@@ -868,12 +765,19 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
| Parse_ast.DEC_typ_alias(typ,id,e) ->
DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e)
),(l,()))
-
+
+let to_ast_prec = function
+ | Parse_ast.Infix -> Infix
+ | Parse_ast.InfixL -> InfixL
+ | Parse_ast.InfixR -> InfixR
+
let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,def_ord) in
match def with
| Parse_ast.DEF_overload(id,ids) ->
- ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+ ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+ | Parse_ast.DEF_fixity (prec, n, op) ->
+ ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs)
| Parse_ast.DEF_kind(k_def) ->
let kd,envs = to_ast_kdef envs k_def in
((Finished(DEF_kind(kd))),envs),partial_defs
@@ -1016,15 +920,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 (string_of_id id), 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
@@ -1063,32 +964,39 @@ let generate_undefineds vs_ids (Defs defs) =
gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
+ gen_vs (mk_id "undefined_nat") "unit -> nat effect {undef}";
+ gen_vs (mk_id "undefined_real") "unit -> real effect {undef}";
gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
(* FIXME: How to handle inc/dec order correctly? *)
gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
in
+ let undefined_tu = function
+ | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
+ | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
+ in
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));
+ 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, None, false));
mk_fundef [mk_funcl (prepend_id "undefined_" id)
- (mk_pat (P_lit (mk_lit L_unit)))
+ pat
(mk_exp (E_app (mk_id "internal_pick",
- [])))]]
+ [mk_exp (E_list (List.map undefined_tu tus))])))]]
| _ -> []
in
let rec undefined_defs = function
@@ -1117,9 +1025,11 @@ let generate_initialize_registers vs_ids (Defs defs) =
in
Defs (defs @ initialize_registers)
+let incremental_k_env = ref initial_kind_env
let process_ast order defs =
- let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
+ let ast, k_env, _= to_ast Nameset.empty !incremental_k_env order defs in
+ incremental_k_env := k_env;
if not !opt_undefined_gen
then ast
else
diff --git a/src/lexer2.mll b/src/lexer2.mll
index a1717d62..4acbd6e5 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -42,6 +42,7 @@
{
open Parser2
+open Parse_ast
module M = Map.Make(String)
exception LexError of string * Lexing.position
@@ -49,8 +50,6 @@ let r = fun s -> s (* Ulib.Text.of_latin1 *)
(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
-type prec = Infix | InfixL | InfixR
-
let mk_operator prec n op =
match prec, n with
| Infix, 0 -> Op0 op
@@ -100,17 +99,14 @@ let kw_table =
("by", (fun _ -> By));
("match", (fun _ -> Match));
("clause", (fun _ -> Clause));
- ("const", (fun _ -> Const));
("dec", (fun _ -> Dec));
- ("def", (fun _ -> Def));
- ("op", (fun _ -> Op));
+ ("operator", (fun _ -> Op));
("default", (fun _ -> Default));
("effect", (fun _ -> Effect));
- ("Effect", (fun _ -> EFFECT));
("end", (fun _ -> End));
("enum", (fun _ -> Enum));
("else", (fun _ -> Else));
- ("extern", (fun _ -> Extern));
+ ("exit", (fun _ -> Exit));
("cast", (fun _ -> Cast));
("false", (fun _ -> False));
("forall", (fun _ -> Forall));
@@ -123,13 +119,10 @@ let kw_table =
("if", (fun x -> If_));
("in", (fun x -> In));
("inc", (fun _ -> Inc));
- ("IN", (fun x -> IN));
("let", (fun x -> Let_));
- ("member", (fun x -> Member));
("Int", (fun x -> Int));
("Order", (fun x -> Order));
("pure", (fun x -> Pure));
- ("rec", (fun x -> Rec));
("register", (fun x -> Register));
("return", (fun x -> Return));
("scattered", (fun x -> Scattered));
@@ -144,13 +137,10 @@ let kw_table =
("union", (fun x -> Union));
("with", (fun x -> With));
("val", (fun x -> Val));
-
- ("div", (fun x -> Div_));
- ("mod", (fun x -> Mod));
- ("mod_s", (fun x -> ModUnderS));
- ("quot", (fun x -> Quot));
- ("quot_s", (fun x -> QuotUnderS));
- ("rem", (fun x -> Rem));
+ ("repeat", (fun _ -> Repeat));
+ ("until", (fun _ -> Until));
+ ("while", (fun _ -> While));
+ ("do", (fun _ -> Do));
("barr", (fun x -> Barr));
("depend", (fun x -> Depend));
@@ -180,8 +170,8 @@ let alphanum = letter|digit
let startident = letter|'_'
let ident = alphanum|['_''\'']
let tyvar_start = '\''
-let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
-let operator = oper_char+ ('_' ident)?
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|']
+let operator = (oper_char+ ('_' ident)?)
let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
rule token = parse
@@ -198,6 +188,9 @@ rule token = parse
| "," { Comma }
| ".." { DotDot }
| "." { Dot }
+ | "==" as op
+ { try M.find op !operators
+ with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
| "=" { (Eq(r"=")) }
| ">" { (Gt(r">")) }
| "-" { Minus }
@@ -223,19 +216,20 @@ rule token = parse
| "<=" { (LtEq(r"<=")) }
| "infix" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (Infix, int_of_string (Char.escaped p), op) }
| "infixl" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (InfixL, int_of_string (Char.escaped p), op) }
| "infixr" ws (digit as p) ws (operator as op)
{ operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators;
- token lexbuf }
+ Fixity (InfixR, int_of_string (Char.escaped p), op) }
| operator as op
{ try M.find op !operators
- with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
+ with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
| "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
| "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
| tyvar_start startident ident* as i { TyVar(r i) }
+ | "~" { Id(r"~") }
| startident ident* as i { if M.mem i kw_table then
(M.find i kw_table) ()
(* else if
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index cad2f6aa..42546ae0 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -46,11 +46,11 @@ let rec subst_nc substs (NC_aux (nc,l) as n_constraint) =
let snc nc = subst_nc substs nc in
let re nc = NC_aux (nc,l) in
match nc with
- | NC_fixed (n1,n2) -> re (NC_fixed (snexp n1, snexp n2))
+ | NC_equal (n1,n2) -> re (NC_equal (snexp n1, snexp n2))
| NC_bounded_ge (n1,n2) -> re (NC_bounded_ge (snexp n1, snexp n2))
| NC_bounded_le (n1,n2) -> re (NC_bounded_le (snexp n1, snexp n2))
| NC_not_equal (n1,n2) -> re (NC_not_equal (snexp n1, snexp n2))
- | NC_nat_set_bounded (kid,is) ->
+ | NC_set (kid,is) ->
begin
match KBindings.find kid substs with
| Nexp_aux (Nexp_constant i,_) ->
@@ -181,7 +181,7 @@ let extract_set_nc var (NC_aux (_,l) as nc) =
let rec aux (NC_aux (nc,l)) =
let re nc = NC_aux (nc,l) in
match nc with
- | NC_nat_set_bounded (id,is) when Kid.compare id var = 0 -> Some (is,re NC_true)
+ | NC_set (id,is) when Kid.compare id var = 0 -> Some (is,re NC_true)
| NC_and (nc1,nc2) ->
(match aux nc1, aux nc2 with
| None, None -> None
@@ -489,8 +489,6 @@ let nexp_subst_fns substs =
| 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_loop (loop,e1,e2) -> re (E_loop (loop,s_exp e1,s_exp e2))
| 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))
@@ -529,9 +527,7 @@ let nexp_subst_fns substs =
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
@@ -557,7 +553,7 @@ let bindings_from_pat p =
| P_typ (_,p) -> aux_pat p
| P_id id ->
if pat_id_is_variable env id then [id] else []
- | P_var kid -> [id_of_kid kid]
+ | P_var (p,kid) -> aux_pat p
| P_vector ps
| P_vector_concat ps
| P_app (_,ps)
@@ -565,7 +561,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
@@ -619,11 +614,11 @@ let can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases =
let checkpat = function
| P_aux (P_lit (L_aux (lit_p, _)),_) ->
if lit_match (lit_e,lit_p) then DoesMatch ([],[]) else DoesNotMatch
- | P_aux (P_var kid,_) ->
+ | P_aux (P_var (P_aux (P_id id,_), kid),_) ->
begin
match lit_e with
| L_num i ->
- DoesMatch ([id_of_kid kid, E_aux (e,(l,annot))],
+ DoesMatch ([id, E_aux (e,(l,annot))],
[kid,Nexp_aux (Nexp_constant i,Unknown)])
| _ ->
(Reporting_basic.print_err false true lit_l "Monomorphisation"
@@ -933,11 +928,6 @@ let split_defs splits defs =
| None -> re (E_vector es') assigns
| Some lit -> re (E_lit lit) assigns
end
- | E_vector_indexed (ies,(Def_val_aux (ed,edann))) ->
- let is,es = List.split ies in
- let es',assigns = non_det_exp_list (match ed with Def_val_empty -> es | Def_val_dec e -> e::es) in
- let ed',es' = match ed with Def_val_empty -> Def_val_empty,es' | x -> x,es' in
- re (E_vector_indexed (List.combine is es', Def_val_aux (ed',edann))) assigns
| E_vector_access (e1,e2) ->
let e1',e2',assigns = non_det_exp_2 e1 e2 in
re (E_vector_access (e1',e2')) assigns
@@ -989,17 +979,12 @@ let split_defs splits defs =
| E_let (lb,e2) ->
begin
match lb with
- | LB_aux (LB_val_explicit (tysch,p,e),annot) ->
- let substs' = remove_bound substs p in
- let e',assigns = const_prop_exp substs assigns e in
- let e2',assigns = const_prop_exp substs' assigns e2 in
- re (E_let (LB_aux (LB_val_explicit (tysch,p,e'), annot), e2')) assigns
- | LB_aux (LB_val_implicit (p,e), annot) ->
+ | LB_aux (LB_val (p,e), annot) ->
let e',assigns = const_prop_exp substs assigns e in
let substs' = remove_bound substs p in
let plain () =
let e2',assigns = const_prop_exp substs' assigns e2 in
- re (E_let (LB_aux (LB_val_implicit (p,e'), annot),
+ re (E_let (LB_aux (LB_val (p,e'), annot),
e2')) assigns in
if is_value e' && not (is_value e) then
match can_match e' [Pat_aux (Pat_exp (p,e2),(Unknown,None))] with
@@ -1245,8 +1230,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 ->
@@ -1279,7 +1262,7 @@ let split_defs splits defs =
begin
let kid,kid_annot =
match args with
- | [P_aux (P_var kid,ann)] -> kid,ann
+ | [P_aux (P_var (_,kid),ann)] -> kid,ann
| _ ->
raise (Reporting_basic.err_general l
"Pattern match not currently supported by monomorphisation")
@@ -1343,8 +1326,6 @@ let split_defs splits defs =
| 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_loop (loop,e1,e2) -> re (E_loop (loop,map_exp e1,map_exp e2))
| 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))
@@ -1409,8 +1390,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..dc8c056e 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -107,8 +107,13 @@ let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string
let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
match exp_aux with
+ | E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
- | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_app (f, xs) when Env.is_union_constructor f (env_of exp) ->
+ zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_app (f, xs) ->
+ zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) [exp1; exp2; exp3])
| E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
| E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
| E_cast (_, exp) -> ocaml_exp ctx exp
@@ -150,7 +155,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
@@ -176,9 +181,8 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
begin
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
- | Enum _ -> zencode_upper ctx id
+ | Enum _ | Union _ -> zencode_upper ctx id
| Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
- | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
end
| E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
| E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
@@ -255,8 +259,8 @@ let rec ocaml_fields ctx =
let rec ocaml_cases ctx =
let ocaml_case = function
- | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id]
- | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ]
+ | Tu_aux (Tu_id id, _) -> separate space [bar; zencode_upper ctx id]
+ | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
in
function
| [tu] -> ocaml_case tu
@@ -287,10 +291,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..cfd749ba 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -64,7 +64,6 @@ base_kind_aux = (* base kind *)
BK_type (* kind of types *)
| BK_nat (* kind of natural number size expressions *)
| BK_order (* kind of vector order specifications *)
- | BK_effect (* kind of effect sets *)
type
@@ -158,11 +157,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 +233,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 +267,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 +319,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 +423,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 *)
@@ -493,14 +481,18 @@ type
scattered_def =
SD_aux of scattered_def_aux * l
+type prec = Infix | InfixL | InfixR
-type
+type fixity_token = (prec * int * string)
+
+type
def = (* Top-level definition *)
DEF_kind of kind_def (* definition of named kind identifiers *)
| DEF_type of type_def (* type definition *)
| DEF_fundef of fundef (* function definition *)
| DEF_val of letbind (* value definition *)
| DEF_overload of id * id list (* operator overload specifications *)
+ | DEF_fixity of prec * int * id (* fixity declaration *)
| DEF_spec of val_spec (* top-level type constraint *)
| DEF_default of default_typing_spec (* default kind and type assumptions *)
| DEF_scattered of scattered_def (* scattered definition *)
diff --git a/src/parser.mly b/src/parser.mly
index 0c3dbb03..df4a273d 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 ())
@@ -302,8 +309,6 @@ atomic_kind:
{ bkloc BK_nat }
| Order
{ bkloc BK_order }
- | EFFECT
- { bkloc BK_effect }
kind_help:
| atomic_kind
@@ -503,7 +508,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 +517,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 +607,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 +1007,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 +1049,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 +1097,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 +1105,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 +1284,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..e6c63196 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -46,11 +46,14 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
open Parse_ast
-let loc n m = Range (m, n)
+let loc n m = Range (n, m)
-let mk_id i n m = Id_aux (i, loc m n)
+let mk_id i n m = Id_aux (i, loc n m)
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)
@@ -121,21 +124,19 @@ let rec desugar_rchain chain s e =
/*Terminals with no content*/
-%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Effect EFFECT End Op
-%token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
-%token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch
+%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op
+%token Enum Else False Forall Foreach Overload Function_ If_ In Inc Let_ Int Order Cast
+%token Pure Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef
+%token Undefined Union With Val Constraint Throw Try Catch Exit
%token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
+%token Repeat Until While Do
%nonassoc Then
%nonassoc Else
-%token Div_ Mod ModUnderS Quot Rem QuotUnderS
-
%token Bar Comma Dot Eof Minus Semi Under DotDot
%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare LcurlyBar RcurlyBar
-%token BarBar BarSquare BarBarSquare ColonEq ColonGt ColonSquare
-%token MinusGt LtBar LtColon SquareBar SquareBarBar
+%token MinusGt
/*Terminals with content*/
@@ -143,15 +144,17 @@ let rec desugar_rchain chain s e =
%token <int> Num
%token <string> String Bin Hex Real
-%token <string> Amp At Caret Div Eq Excl Gt Lt Plus Star EqGt Unit
+%token <string> Amp At Caret Eq Gt Lt Plus Star EqGt Unit
%token <string> Colon ExclEq
-%token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
-%token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar
+%token <string> GtEq
+%token <string> LtEq
%token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
%token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
%token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
+%token <Parse_ast.fixity_token> Fixity
+
%start file
%start typschm_eof
%type <Parse_ast.typschm> typschm_eof
@@ -198,6 +201,14 @@ id:
| Op Plus { mk_id (DeIid "+") $startpos $endpos }
| Op Minus { mk_id (DeIid "-") $startpos $endpos }
| Op Star { mk_id (DeIid "*") $startpos $endpos }
+ | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
+ | Op Lt { mk_id (DeIid "<") $startpos $endpos }
+ | Op Gt { mk_id (DeIid ">") $startpos $endpos }
+ | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
+ | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
+ | Op Amp { mk_id (DeIid "&") $startpos $endpos }
+ | Op Bar { mk_id (DeIid "|") $startpos $endpos }
+ | Op Caret { mk_id (DeIid "^") $startpos $endpos }
op0: Op0 { mk_id (Id $1) $startpos $endpos }
op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -266,7 +277,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 +287,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
@@ -434,16 +445,19 @@ typ8:
| typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ8l:
| typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ8l op8l typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ8r:
| typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| typ9 op8r typ8r { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
| TwoCaret typ9 { mk_typ (ATyp_exp $2) $startpos $endpos }
+ | Minus typ9 { mk_typ (ATyp_neg $2) $startpos $endpos}
| typ9 { $1 }
typ9:
@@ -481,7 +495,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
@@ -582,13 +596,25 @@ typschm_eof:
| typschm Eof
{ $1 }
-pat:
+pat1:
| atomic_pat
{ $1 }
- | atomic_pat As id
+ | atomic_pat At pat_concat
+ { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+
+pat_concat:
+ | atomic_pat
+ { [$1] }
+ | atomic_pat At pat_concat
+ { $1 :: $3 }
+
+pat:
+ | pat1
+ { $1 }
+ | pat1 As id
{ mk_pat (P_as ($1, $3)) $startpos $endpos }
- | Lparen pat Comma pat_list Rparen
- { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+ | pat1 As kid
+ { mk_pat (P_var ($1, $3)) $startpos $endpos }
pat_list:
| pat
@@ -604,13 +630,17 @@ 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
+ | atomic_pat Colon typ
{ mk_pat (P_typ ($3, $1)) $startpos $endpos }
| Lparen pat Rparen
{ $2 }
+ | Lparen pat Comma pat_list Rparen
+ { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+ | Lsquare pat_list Rsquare
+ { mk_pat (P_vector $2) $startpos $endpos }
lit:
| True
@@ -633,6 +663,8 @@ lit:
{ mk_lit (L_hex $1) $startpos $endpos }
| String
{ mk_lit (L_string $1) $startpos $endpos }
+ | Real
+ { mk_lit (L_real $1) $startpos $endpos }
exp:
| exp0
@@ -655,8 +687,39 @@ exp:
{ mk_exp (E_case ($2, $4)) $startpos $endpos }
| Try exp Catch Lcurly case_list Rcurly
{ mk_exp (E_try ($2, $5)) $startpos $endpos }
- | Lparen exp0 Comma exp_list Rparen
- { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" in foreach loop"));
+ mk_exp (E_for ($3, $5, $7, $9, $11, $13)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" && $6 <> "downto" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop"));
+ let order =
+ if $6 = "to"
+ then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6))
+ else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6))
+ in
+ mk_exp (E_for ($3, $5, $7, $9, order, $11)) $startpos $endpos }
+ | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp
+ { if $4 <> "from" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"from\" in foreach loop"));
+ if $6 <> "to" && $6 <> "downto" then
+ raise (Parse_error_locn (loc $startpos $endpos,"Missing \"to\" or \"downto\" in foreach loop"));
+ let step = mk_lit_exp (L_num 1) $startpos $endpos in
+ let ord =
+ if $6 = "to"
+ then ATyp_aux(ATyp_inc,loc $startpos($6) $endpos($6))
+ else ATyp_aux(ATyp_dec,loc $startpos($6) $endpos($6))
+ in
+ mk_exp (E_for ($3, $5, $7, step, ord, $9)) $startpos $endpos }
+ | Repeat exp Until exp
+ { mk_exp (E_loop (Until, $4, $2)) $startpos $endpos }
+ | While exp Do exp
+ { mk_exp (E_loop (While, $2, $4)) $startpos $endpos }
/* The following implements all nine levels of user-defined precedence for
operators in expressions, with both left, right and non-associative operators */
@@ -693,6 +756,7 @@ exp2:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp2l:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -701,12 +765,14 @@ exp2l:
exp2r:
| exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp3 { $1 }
exp3:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp3l:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -715,10 +781,16 @@ exp3l:
exp3r:
| exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4 { $1 }
exp4:
| exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+ | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp5 { $1 }
@@ -785,6 +857,7 @@ exp8:
| exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp8l op8l exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
| exp9 { $1 }
exp8l:
@@ -795,6 +868,7 @@ exp8l:
exp8r:
| exp9 op8 exp9 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
| exp9 op8r exp8r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+ | exp9 Caret exp8r { mk_exp (E_app_infix ($1, mk_id (Id "^") $startpos($2) $endpos($2), $3)) $startpos $endpos }
| TwoCaret exp9 { mk_exp (E_app (mk_id (Id "pow2") $startpos($1) $endpos($1), [$2])) $startpos $endpos }
| exp9 { $1 }
@@ -836,13 +910,15 @@ 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
{ mk_exp (E_cast ($3, $1)) $startpos $endpos }
| lit
{ mk_exp (E_lit $1) $startpos $endpos }
+ | atomic_exp Dot id
+ { mk_exp (E_field ($1, $3)) $startpos $endpos }
| id
{ mk_exp (E_id $1) $startpos $endpos }
| kid
@@ -851,10 +927,14 @@ atomic_exp:
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
{ mk_exp (E_app ($1, $3)) $startpos $endpos }
+ | Exit Lparen exp Rparen
+ { mk_exp (E_exit $3) $startpos $endpos }
| Sizeof Lparen typ Rparen
{ mk_exp (E_sizeof $3) $startpos $endpos }
| Constraint Lparen nc Rparen
{ mk_exp (E_constraint $3) $startpos $endpos }
+ | Assert Lparen exp Rparen
+ { mk_exp (E_assert ($3, mk_lit_exp (L_string "") $startpos($4) $endpos($4))) $startpos $endpos }
| Assert Lparen exp Comma exp Rparen
{ mk_exp (E_assert ($3, $5)) $startpos $endpos }
| atomic_exp Lsquare exp Rsquare
@@ -869,6 +949,8 @@ atomic_exp:
{ mk_exp (E_vector_update_subrange ($2, $4, $6, $8)) $startpos $endpos }
| Lparen exp Rparen
{ $2 }
+ | Lparen exp Comma exp_list Rparen
+ { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
exp_list:
| exp
@@ -880,11 +962,19 @@ funcl:
| id pat Eq exp
{ mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
+funcls:
+ | id pat Eq exp
+ { [mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos] }
+ | id pat Eq exp And funcls
+ { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos :: $6 }
+
type_def:
| Typedef id typquant Eq typ
{ mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
| Typedef id Eq typ
{ mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
+ | Struct id Eq Lcurly struct_fields Rcurly
+ { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $startpos $endpos }
| Struct id typquant Eq Lcurly struct_fields Rcurly
{ mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
| Enum id Eq enum_bar
@@ -933,8 +1023,8 @@ type_unions:
{ $1 :: $3 }
fun_def:
- | Function_ funcl
- { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
+ | Function_ funcls
+ { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
let_def:
| Let_ letbind
@@ -942,7 +1032,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
@@ -965,6 +1061,8 @@ scattered_def:
def:
| fun_def
{ DEF_fundef $1 }
+ | Fixity
+ { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) }
| val_spec_def
{ DEF_spec $1 }
| type_def
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 98f654a6..a890e039 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -74,6 +74,7 @@ let fix_id remove_tick name = match name with
| "try"
| "match"
| "with"
+ | "check"
| "field"
| "LT"
| "GT"
@@ -289,7 +290,22 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
(doc_tannot_lem sequential mwords false typ)))
| _ -> utf8string "(failwith \"undefined value of unsupported type\")")
| L_string s -> utf8string ("\"" ^ s ^ "\"")
- | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
+ | L_real s ->
+ (* Lem does not support decimal syntax, so we translate a string
+ of the form "x.y" into the ratio (x * 10^len(y) + y) / 10^len(y).
+ The OCaml library has a conversion function from strings to floats, but
+ not from floats to ratios. ZArith's Q library does have the latter, but
+ using this would require adding a dependency on ZArith to Sail. *)
+ let parts = Util.split_on_char '.' s in
+ let (num, denom) = match parts with
+ | [i] -> (big_int_of_string i, unit_big_int)
+ | [i;f] ->
+ let denom = power_int_positive_int 10 (String.length f) in
+ (add_big_int (mult_big_int (big_int_of_string i) denom) (big_int_of_string f), denom)
+ | _ ->
+ raise (Reporting_basic.Fatal_error
+ (Reporting_basic.Err_syntax_locn (l, "could not parse real literal"))) in
+ separate space (List.map string ["realFromFrac"; string_of_big_int num; string_of_big_int denom])
(* typ_doc is the doc for the type being quantified *)
let doc_quant_item (QI_aux (qi, _)) = match qi with
@@ -356,7 +372,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) -> doc_pat_lem sequential mwords true p
| 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
@@ -376,7 +392,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
@@ -533,12 +549,12 @@ let doc_exp_lem, doc_let_lem =
let [id;indices;body;e5] = args in
let varspp = match e5 with
| E_aux (E_tuple vars,_) ->
- let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+ let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in
begin match vars with
| [v] -> v
| _ -> parens (separate comma vars) end
- | E_aux (E_id (Id_aux (Id name,_)),_) ->
- string name
+ | E_aux (E_id id,_) ->
+ doc_id_lem id
| E_aux (E_lit (L_aux (L_unit,_)),_) ->
string "_" in
parens (
@@ -553,12 +569,12 @@ let doc_exp_lem, doc_let_lem =
let [is_while;cond;body;e5] = args in
let varspp = match e5 with
| E_aux (E_tuple vars,_) ->
- let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in
+ let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in
begin match vars with
| [v] -> v
| _ -> parens (separate comma vars) end
- | E_aux (E_id (Id_aux (Id name,_)),_) ->
- string name
+ | E_aux (E_id id,_) ->
+ doc_id_lem id
| E_aux (E_lit (L_aux (L_unit,_)),_) ->
string "_" in
parens (
@@ -593,7 +609,7 @@ let doc_exp_lem, doc_let_lem =
currently broken. *)
let [arg] = args in
let targ = typ_of arg in
- let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in
+ let call = if mwords && is_bitvector_typ targ then "bitvector_length" else "length" in
let epp = separate space [string call;expY arg] in
if aexp_needed then parens (align epp) else epp
(*)| Id_aux (Id "bool_not", _) ->
@@ -632,17 +648,19 @@ let doc_exp_lem, doc_let_lem =
end
| E_vector_access (v,e) ->
let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+ let (start, len, ord, etyp) = vector_typ_args_of vtyp in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ vtyp (*&& mwords*)
- then "bitvector_access" ^ ord_suffix
- else "vector_access" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
+ let call = bit_prefix ^ "vector_access" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e]) in
if aexp_needed then parens (align epp) else epp
(* raise (Reporting_basic.err_unreachable l
@@ -658,17 +676,19 @@ let doc_exp_lem, doc_let_lem =
if aexp_needed then parens (align epp) else epp*)
| E_vector_subrange (v,e1,e2) ->
let vtyp = Env.base_typ_of (env_of v) (typ_of v) in
- let (start, _, ord, etyp) = vector_typ_args_of vtyp in
+ let (start, len, ord, etyp) = vector_typ_args_of vtyp in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ vtyp (*&& mwords*)
- then "bitvector_subrange" ^ ord_suffix
- else "vector_subrange" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ vtyp then "bit" else "" in
+ let call = bit_prefix ^ "vector_subrange" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
if aexp_needed then parens (align epp) else epp
(* raise (Reporting_basic.err_unreachable l
@@ -852,91 +872,38 @@ 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
+ let t = typ_of v in
+ let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update_pos" ^ ord_suffix
- else "vector_update_pos" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ t then "bit" else "" in
+ let call = bit_prefix ^ "vector_update_pos" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp = string call ^^ space ^^ parens (separate comma_sp [start_idx;expY v;expY e1;expY e2]) in
if aexp_needed then parens (align epp) else epp
| E_vector_update_subrange(v,e1,e2,e3) ->
- let t = typ_of full_exp in
- let (start, _, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
+ let t = typ_of v in
+ let (start, len, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of full_exp) t) in
let ord_suffix = if is_order_inc ord then "_inc" else "_dec" in
- let call =
- if is_bitvector_typ t (*&& mwords*)
- then "bitvector_update_subrange" ^ ord_suffix
- else "vector_update_subrange" ^ ord_suffix in
+ let bit_prefix = if is_bitvector_typ t then "bit" else "" in
+ let call = bit_prefix ^ "vector_update_subrange" ^ ord_suffix in
let start_idx = match simplify_nexp (start) with
| Nexp_aux (Nexp_constant i, _) -> expN (simple_num l i)
| _ ->
- raise (Reporting_basic.err_unreachable l
- ("cannot pretty print expression " ^ (string_of_exp full_exp) ^ " with non-constant start index")) in
+ let nc = nc_eq start (nminus len (nconstant 1)) in
+ if prove (env_of full_exp) nc
+ then string (bit_prefix ^ "vector_length") ^^ space ^^ expY v
+ else raise (Reporting_basic.err_unreachable l
+ ("cannot pretty print expression " ^ (string_of_exp full_exp) ^
+ " with non-constant start index")) in
let epp =
align (string call ^//^
parens (separate comma_sp
@@ -1097,8 +1064,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)
@@ -1601,13 +1567,13 @@ let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
let doc_spec_lem sequential 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) ->
+ | VS_val_spec (typschm,id,None,_) ->
separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem sequential mwords true typschm] ^/^ hardline
+ | VS_val_spec (_,_,Some _,_) -> empty
-
-let rec doc_def_lem sequential mwords def = match def with
+let rec doc_def_lem sequential mwords def =
+ (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
+ match def with
| DEF_spec v_spec -> (empty,doc_spec_lem sequential mwords v_spec)
| DEF_overload _ -> (empty,empty)
| DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 73f06d1a..2e464a08 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -133,8 +133,7 @@ let pp_format_bkind_lem (BK_aux(k,l)) =
(match k with
| BK_type -> "BK_type"
| BK_nat -> "BK_nat"
- | BK_order -> "BK_order"
- | BK_effect -> "BK_effect") ^ " " ^
+ | BK_order -> "BK_order") ^ " " ^
(pp_format_l_lem l) ^ ")"
let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
@@ -215,7 +214,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 +222,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 +327,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 +337,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 +348,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 +382,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 +505,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 +564,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 2f38fe02..d346c801 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
@@ -52,8 +53,7 @@ let doc_bkind (BK_aux(k,_)) =
string (match k with
| BK_type -> "Type"
| BK_nat -> "Nat"
- | BK_order -> "Order"
- | BK_effect -> "Effect")
+ | BK_order -> "Order")
let doc_kind (K_aux(K_kind(klst),_)) =
separate_map (spaces arrow) doc_bkind klst
@@ -109,13 +109,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]
@@ -176,7 +177,8 @@ let doc_exp, doc_let =
and starstar_exp ((E_aux(e,_)) as expr) = match e with
| E_app_infix(l,(Id_aux(Id "**",_) as op),r) ->
doc_op (doc_id op) (starstar_exp l) (app_exp r)
- | E_if _ | E_for _ | E_let _ -> right_atomic_exp expr
+ | E_if _ | E_for _ | E_loop _ | E_let _
+ | E_internal_let _ | E_internal_plet _ -> right_atomic_exp expr
| _ -> app_exp expr
and right_atomic_exp ((E_aux(e,_)) as expr) = match e with
(* Special case: omit "else ()" when the else branch is empty. *)
@@ -186,7 +188,14 @@ let doc_exp, doc_let =
| E_if(c,t,e) ->
string "if" ^^ space ^^ group (exp c) ^/^
string "then" ^^ space ^^ group (exp t) ^/^
- string "else" ^^ space ^^ group (exp e)
+ string "else" ^^ space ^^ group (exp e)
+ | E_loop (While, c, e) ->
+ separate space [string "while"; atomic_exp c; string "do"] ^/^
+ exp e
+ | E_loop (Until, c, e) ->
+ (string "repeat"
+ ^/^ exp e)
+ ^/^ (string "until" ^^ space ^^ atomic_exp c)
| E_for(id,exp1,exp2,exp3,order,exp4) ->
string "foreach" ^^ space ^^
group (parens (
@@ -200,6 +209,18 @@ let doc_exp, doc_let =
)) ^/^
exp exp4
| E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
+ | E_internal_let (lexp, exp1, exp2) ->
+ let le =
+ prefix 2 1
+ (separate space [string "internal_let"; doc_lexp lexp; equals])
+ (exp exp1) in
+ doc_op (string "in") le (exp exp2)
+ | E_internal_plet (pat, exp1, exp2) ->
+ let le =
+ prefix 2 1
+ (separate space [string "internal_plet"; doc_pat pat; equals])
+ (exp exp1) in
+ doc_op (string "in") le (exp exp2)
| _ -> group (parens (exp expr))
and app_exp ((E_aux(e,_)) as expr) = match e with
| E_app(f,args) ->
@@ -263,13 +284,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) ->
@@ -301,7 +315,8 @@ let doc_exp, doc_let =
(* adding parens and loop for lower precedence *)
| E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
| E_cons (_, _)|E_field (_, _)|E_assign (_, _)
- | E_if _ | E_for _ | E_let _
+ | E_if _ | E_for _ | E_loop _ | E_let _
+ | E_internal_let _ | E_internal_plet _
| E_vector_append _
| E_app_infix (_,
(* for every app_infix operator caught at a higher precedence,
@@ -345,21 +360,11 @@ let doc_exp, doc_let =
| E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
| E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
*)
- | E_internal_let (lexp, exp1, exp2) ->
- separate space [string "internal let"; doc_lexp lexp; equals; exp exp1; string "in"; exp exp2]
+ | E_internal_return exp1 ->
+ separate space [string "internal_return"; exp exp1]
| _ -> 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)
@@ -403,15 +408,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
@@ -454,37 +458,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
@@ -565,6 +540,7 @@ let rec doc_def def = group (match def with
string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc
| DEF_comm (DC_comm s) -> comment (string s)
| DEF_comm (DC_comm_struct d) -> comment (doc_def d)
+ | DEF_fixity _ -> empty
) ^^ hardline
let doc_defs (Defs(defs)) =
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
new file mode 100644
index 00000000..3fa05132
--- /dev/null
+++ b/src/pretty_print_sail2.ml
@@ -0,0 +1,370 @@
+
+open Ast
+open Ast_util
+open PPrint
+
+let doc_op symb a b = infix 2 1 symb a b
+
+let doc_id (Id_aux (id_aux, _)) =
+ string (match id_aux with
+ | Id v -> v
+ | DeIid op -> "operator " ^ op)
+
+let doc_kid kid = string (Ast_util.string_of_kid kid)
+
+let doc_int n = string (string_of_int n)
+
+let doc_ord (Ord_aux(o,_)) = match o with
+ | Ord_var v -> doc_kid v
+ | Ord_inc -> string "inc"
+ | Ord_dec -> string "dec"
+
+let rec doc_nexp =
+ let rec atomic_nexp (Nexp_aux (n_aux, _) as nexp) =
+ match n_aux with
+ | Nexp_constant c -> string (string_of_int c)
+ | Nexp_id id -> doc_id id
+ | Nexp_var kid -> doc_kid kid
+ | _ -> parens (nexp0 nexp)
+ and nexp0 (Nexp_aux (n_aux, _) as nexp) =
+ match n_aux with
+ | Nexp_sum (n1, Nexp_aux (Nexp_neg n2, _)) | Nexp_minus (n1, n2) ->
+ separate space [nexp0 n1; string "-"; nexp1 n2]
+ | Nexp_sum (n1, Nexp_aux (Nexp_constant c, _)) when c < 0 ->
+ separate space [nexp0 n1; string "-"; doc_int (abs c)]
+ | Nexp_sum (n1, n2) -> separate space [nexp0 n1; string "+"; nexp1 n2]
+ | _ -> nexp1 nexp
+ and nexp1 (Nexp_aux (n_aux, _) as nexp) =
+ match n_aux with
+ | Nexp_times (n1, n2) -> separate space [nexp1 n1; string "*"; nexp2 n2]
+ | _ -> nexp2 nexp
+ and nexp2 (Nexp_aux (n_aux, _) as nexp) =
+ match n_aux with
+ | Nexp_neg n -> separate space [string "-"; atomic_nexp n]
+ | Nexp_exp n -> separate space [string "2"; string "^"; atomic_nexp n]
+ | _ -> atomic_nexp nexp
+ in
+ nexp0
+
+let doc_nc =
+ let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
+ let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
+ match nc_aux with
+ | NC_true -> string "true"
+ | NC_false -> string "false"
+ | NC_equal (n1, n2) -> nc_op "=" n1 n2
+ | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2
+ | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2
+ | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
+ | NC_set (kid, ints) ->
+ separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
+ | _ -> parens (nc0 nc)
+ and nc0 (NC_aux (nc_aux, _) as nc) =
+ match nc_aux with
+ | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2]
+ | _ -> nc1 nc
+ and nc1 (NC_aux (nc_aux, _) as nc) =
+ match nc_aux with
+ | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
+ | _ -> atomic_nc nc
+ in
+ nc0
+
+let rec doc_typ (Typ_aux (typ_aux, _)) =
+ match typ_aux with
+ | Typ_id id -> doc_id id
+ | Typ_app (id, []) -> doc_id id
+ | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
+ separate space [doc_typ_arg x; doc_typ_arg y]
+ (*
+ | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
+ string "bits" ^^ parens (doc_typ_arg len)
+ *)
+ | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+ | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
+ | Typ_var kid -> doc_kid kid
+ | Typ_wild -> assert false
+ (* Resugar set types like {|1, 2, 3|} *)
+ | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+ when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
+ enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
+ | Typ_exist (kids, nc, typ) ->
+ braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
+ | Typ_fn (typ1, typ2, eff) ->
+ separate space [doc_typ typ1; string "->"; doc_typ typ2]
+and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
+ match ta_aux with
+ | Typ_arg_typ typ -> doc_typ typ
+ | Typ_arg_nexp nexp -> doc_nexp nexp
+ | Typ_arg_order o -> doc_ord o
+
+let doc_quants quants =
+ let doc_qi_kopt (QI_aux (qi_aux, _)) =
+ match qi_aux with
+ | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
+ | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
+ | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
+ | QI_id kopt when is_order_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
+ | QI_const nc -> []
+ in
+ let qi_nc (QI_aux (qi_aux, _)) =
+ match qi_aux with
+ | QI_const nc -> [nc]
+ | _ -> []
+ in
+ let kdoc = separate space (List.concat (List.map doc_qi_kopt quants)) in
+ let ncs = List.concat (List.map qi_nc quants) in
+ match ncs with
+ | [] -> kdoc
+ | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
+ | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
+
+let doc_typschm (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) =
+ match tq_aux with
+ | TypQ_no_forall -> doc_typ typ
+ | TypQ_tq [] -> doc_typ typ
+ | TypQ_tq qs ->
+ string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
+
+let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ
+
+let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) =
+ match tq_aux with
+ | TypQ_no_forall -> None
+ | TypQ_tq [] -> None
+ | TypQ_tq qs -> Some (doc_quants qs)
+
+let doc_lit (L_aux(l,_)) =
+ utf8string (match l with
+ | L_unit -> "()"
+ | L_zero -> "bitzero"
+ | L_one -> "bitone"
+ | L_true -> "true"
+ | L_false -> "false"
+ | L_num i -> string_of_int i
+ | L_hex n -> "0x" ^ n
+ | L_bin n -> "0b" ^ n
+ | L_real r -> r
+ | L_undef -> "undefined"
+ | L_string s -> "\"" ^ String.escaped s ^ "\"")
+
+let rec doc_pat (P_aux (p_aux, _) as pat) =
+ match p_aux with
+ | P_id id -> doc_id id
+ | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
+ | P_app (id, pats) -> doc_id id ^^ lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
+ | P_typ (typ, pat) -> separate space [doc_pat pat; colon; doc_typ typ]
+ | P_lit lit -> doc_lit lit
+ (* P_var short form sugar *)
+ | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
+ doc_kid kid
+ | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid]
+ | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats)
+ | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
+ | P_wild -> string "_"
+ | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id]
+ | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
+ | _ -> string (string_of_pat pat)
+
+let rec doc_exp (E_aux (e_aux, _) as exp) =
+ match e_aux with
+ | E_block [exp] -> doc_exp exp
+ | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
+ | E_nondet exps -> assert false
+ (* This is mostly for the -convert option *)
+ | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
+ separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
+ | E_app_infix (x, id, y) -> separate space [doc_atomic_exp x; doc_id id; doc_atomic_exp y]
+ | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps)
+ | E_if (if_exp, then_exp, else_exp) ->
+ group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
+ | E_list exps -> string "E_list"
+ | E_cons (exp1, exp2) -> string "E_cons"
+ | E_record fexps -> string "E_record"
+ | E_loop (While, cond, exp) ->
+ separate space [string "while"; doc_exp cond; string "do"; doc_exp exp]
+ | E_loop (Until, cond, exp) ->
+ separate space [string "repeat"; doc_exp exp; string "until"; doc_exp cond]
+ | E_record_update (exp, fexps) -> string "E_record_update"
+ | E_vector_append (exp1, exp2) -> separate space [doc_atomic_exp exp1; string "@"; doc_atomic_exp exp2]
+ | E_case (exp, pexps) ->
+ separate space [string "match"; doc_exp exp; doc_pexps pexps]
+ | E_let (LB_aux (LB_val (pat, binding), _), exp) ->
+ separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
+ | E_assign (lexp, exp) ->
+ separate space [doc_lexp lexp; equals; doc_exp exp]
+ | E_for (id, exp1, exp2, exp3, order, exp4) ->
+ begin
+ let header =
+ string "foreach" ^^ space ^^
+ group (parens (separate (break 1)
+ [ doc_id id;
+ string "from " ^^ doc_atomic_exp exp1;
+ string "to " ^^ doc_atomic_exp exp2;
+ string "by " ^^ doc_atomic_exp exp3;
+ string "in " ^^ doc_ord order ]))
+ in
+ match exp4 with
+ | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4
+ | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4
+ | _ -> header ^//^ doc_exp exp4
+ end
+ (* Resugar an assert with an empty message *)
+ | E_throw exp -> assert false
+ | E_try (exp, pexps) -> assert false
+ | E_return exp -> string "return" ^^ parens (doc_exp exp)
+ | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
+ separate space [doc_int 2; string "^"; doc_atomic_exp exp]
+ | _ -> doc_atomic_exp exp
+and doc_atomic_exp (E_aux (e_aux, _) as exp) =
+ match e_aux with
+ | E_cast (typ, exp) ->
+ separate space [doc_atomic_exp exp; colon; doc_typ typ]
+ | E_lit lit -> doc_lit lit
+ | E_id id -> doc_id id
+ | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id
+ | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid
+ | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp)
+ (* Format a function with a unit argument as f() rather than f(()) *)
+ | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
+ | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
+ | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
+ | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
+ | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
+ | E_exit exp -> string "exit" ^^ parens (doc_exp exp)
+ | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2)
+ | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
+ | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps)
+ | E_vector_update (exp1, exp2, exp3) ->
+ brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
+ | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
+ brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
+ | _ -> parens (doc_exp exp)
+and doc_block = function
+ | [] -> string "()"
+ | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
+ separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
+ | [exp] -> doc_exp exp
+ | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps
+and doc_lexp (LEXP_aux (l_aux, _) as lexp) =
+ match l_aux with
+ | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+ | _ -> doc_atomic_lexp lexp
+and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
+ match l_aux with
+ | LEXP_id id -> doc_id id
+ | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen
+ | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
+ | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
+ | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2])
+ | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
+ | _ -> parens (doc_lexp lexp)
+and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace
+and doc_pexp (Pat_aux (pat_aux, _)) =
+ match pat_aux with
+ | Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp]
+ | Pat_when (pat, wh, exp) ->
+ separate space [doc_pat pat; string "if"; doc_exp wh; string "=>"; doc_exp exp]
+and doc_letbind (LB_aux (lb_aux, _)) =
+ match lb_aux with
+ | LB_val (pat, exp) ->
+ separate space [doc_pat pat; equals; doc_exp exp]
+
+let doc_funcl funcl = string "FUNCL"
+
+let doc_funcl (FCL_aux (FCL_Funcl (id, pat, exp), _)) =
+ group (separate space [doc_id id; doc_pat pat; equals; doc_exp exp])
+
+let doc_default (DT_aux(df,_)) = match df with
+ | DT_kind(bk,v) -> string "DT_kind" (* separate space [string "default"; doc_bkind bk; doc_var v] *)
+ | DT_typ(ts,id) -> separate space [string "default"; doc_typschm ts; doc_id id]
+ | DT_order(ord) -> separate space [string "default"; string "Order"; doc_ord ord]
+
+let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) =
+ match funcls with
+ | [] -> failwith "Empty function list"
+ | _ ->
+ let sep = hardline ^^ string "and" ^^ space in
+ let clauses = separate_map sep doc_funcl funcls in
+ string "function" ^^ space ^^ clauses
+
+let doc_dec (DEC_aux (reg,_)) =
+ match reg with
+ | DEC_reg (typ, id) -> separate space [string "register"; doc_id id; colon; doc_typ typ]
+ | DEC_alias(id,alspec) -> string "ALIAS"
+ | DEC_typ_alias(typ,id,alspec) -> string "ALIAS"
+
+let doc_field (typ, id) =
+ separate space [doc_id id; colon; doc_typ typ]
+
+let doc_typdef (TD_aux(td,_)) = match td with
+ | TD_abbrev (id, _, typschm) ->
+ begin
+ match doc_typschm_quants typschm with
+ | Some qdoc ->
+ doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm)
+ | None ->
+ doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
+ end
+ | TD_enum (id, _, ids, _) ->
+ separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
+ | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) ->
+ separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
+ | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) ->
+ separate space [string "struct"; doc_id id; doc_quants qs; equals;
+ surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
+ | _ -> string "TYPEDEF"
+
+let doc_spec (VS_aux(v,_)) =
+ let doc_extern = function
+ | Some s -> equals ^^ space ^^ utf8string ("\"" ^ String.escaped s ^ "\"") ^^ space
+ | None -> empty
+ in
+ match v with
+ | VS_val_spec(ts,id,ext,is_cast) ->
+ string "val" ^^ space
+ ^^ (if is_cast then (string "cast" ^^ space) else empty)
+ ^^ doc_id id ^^ space
+ ^^ doc_extern ext
+ ^^ colon ^^ space
+ ^^ doc_typschm ts
+
+let doc_prec = function
+ | Infix -> string "infix"
+ | InfixL -> string "infixl"
+ | InfixR -> string "infixr"
+
+let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) =
+ separate space [string "integer"; doc_id id; equals; doc_nexp nexp]
+
+let rec doc_scattered (SD_aux (sd_aux, _)) =
+ match sd_aux with
+ | SD_scattered_function (_, _, _, id) ->
+ string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id
+ | SD_scattered_funcl funcl ->
+ string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl
+ | SD_scattered_end id ->
+ string "end" ^^ space ^^ doc_id id
+ | _ -> string "SCATTERED"
+
+let rec doc_def def = group (match def with
+ | DEF_default df -> doc_default df
+ | DEF_spec v_spec -> doc_spec v_spec
+ | DEF_type t_def -> doc_typdef t_def
+ | DEF_kind k_def -> doc_kind_def k_def
+ | DEF_fundef f_def -> doc_fundef f_def
+ | DEF_val lbind -> string "let" ^^ space ^^ doc_letbind lbind
+ | DEF_reg_dec dec -> doc_dec dec
+ | DEF_scattered sdef -> doc_scattered sdef
+ | DEF_fixity (prec, n, id) ->
+ separate space [doc_prec prec; doc_int n; doc_id id]
+ | DEF_overload (id, ids) ->
+ separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
+ | DEF_comm (DC_comm s) -> string "TOPLEVEL"
+ | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL"
+ ) ^^ hardline
+
+let doc_defs (Defs(defs)) =
+ separate_map hardline doc_def defs
+
+let pp_defs f d = ToChannel.pretty 1. 80 f (doc_defs d)
diff --git a/src/process_file.ml b/src/process_file.ml
index 22f25f6e..d35ccf5e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -59,20 +59,25 @@ let get_lexbuf f =
lexbuf, in_chan
let parse_file (f : string) : Parse_ast.defs =
- let scanbuf, in_chan = get_lexbuf f in
- let type_names =
- try
- Pre_parser.file Pre_lexer.token scanbuf
- with
+ if not !opt_new_parser
+ then
+ let scanbuf, in_chan = get_lexbuf f in
+ let type_names =
+ try
+ Pre_parser.file Pre_lexer.token scanbuf
+ with
| Parsing.Parse_error ->
- let pos = Lexing.lexeme_start_p scanbuf in
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
+ let pos = Lexing.lexeme_start_p scanbuf in
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
| Parse_ast.Parse_error_locn(l,m) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
| Lexer.LexError(s,p) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
- let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in
- close_in in_chan;
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+ in
+ close_in in_chan;
+ Lexer.custom_type_names := !Lexer.custom_type_names @ type_names
+ else ();
+
let lexbuf, in_chan = get_lexbuf f in
try
let ast =
@@ -82,13 +87,16 @@ let parse_file (f : string) : Parse_ast.defs =
in
close_in in_chan; ast
with
- | Parsing.Parse_error ->
- let pos = Lexing.lexeme_start_p lexbuf in
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
- | Parse_ast.Parse_error_locn(l,m) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
- | Lexer.LexError(s,p) ->
- raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+ | Parser2.Error ->
+ let pos = Lexing.lexeme_start_p lexbuf in
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information")))
+ | Parsing.Parse_error ->
+ let pos = Lexing.lexeme_start_p lexbuf in
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
+ | Parse_ast.Parse_error_locn(l,m) ->
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+ | Lexer.LexError(s,p) ->
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
@@ -229,19 +237,27 @@ let output libpath out_arg files =
output1 libpath out_arg f defs)
files
-let rewrite_step defs rewriter =
+let rewrite_step defs (name,rewriter) =
let defs = rewriter defs in
let _ = match !(opt_ddump_rewrite_ast) with
| Some (f, i) ->
begin
- output "" Lem_ast_out [f ^ "_rewrite_" ^ string_of_int i ^ ".sail",defs];
+ let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in
+ output "" Lem_ast_out [filename, defs];
+ let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in
+ Pretty_print_sail.pp_defs ot defs;
+ close_output_with_check ext_ot;
opt_ddump_rewrite_ast := Some (f, i + 1)
end
| _ -> () in
defs
-let rewrite rewriters defs = List.fold_left rewrite_step defs rewriters
+let rewrite rewriters defs =
+ try List.fold_left rewrite_step defs rewriters with
+ | Type_check.Type_error (_, err) ->
+ prerr_endline (Type_check.string_of_type_error err);
+ exit 1
-let rewrite_ast = rewrite [Rewriter.rewrite_defs]
+let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index e552dca4..a47ee8ae 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -87,14 +87,6 @@
(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
(**************************************************************************)
-let format_pos ff p =
- let open Lexing in
- begin
- Format.fprintf ff "file \"%s\", line %d, character %d:\n"
- p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
- Format.pp_print_flush ff ()
- end
-
let rec skip_lines in_chan = function
| n when n <= 0 -> ()
| n -> input_line in_chan; skip_lines in_chan (n - 1)
@@ -126,6 +118,16 @@ let print_code1 ff fname lnum1 cnum1 cnum2 =
end
with _ -> ()
+let format_pos ff p =
+ let open Lexing in
+ begin
+ Format.fprintf ff "file \"%s\", line %d, character %d:\n\n"
+ p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
+ print_code1 ff p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (p.pos_cnum - p.pos_bol + 1);
+ Format.fprintf ff "\n\n";
+ Format.pp_print_flush ff ()
+ end
+
let print_code2 ff fname lnum1 cnum1 lnum2 cnum2 =
try
let in_chan = open_in fname in
diff --git a/src/rewriter.ml b/src/rewriter.ml
index c2b8e618..bcc4e60a 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -83,6 +83,15 @@ let simple_num l n = E_aux (
simple_annot (Parse_ast.Generated l)
(atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l))))
+let rec small (E_aux (exp,_)) = match exp with
+ | E_id _
+ | E_lit _ -> true
+ | E_cast (_,e) -> small e
+ | E_list es -> List.for_all small es
+ | E_cons (e1,e2) -> small e1 && small e2
+ | E_sizeof _ -> true
+ | _ -> false
+
let fresh_name_counter = ref 0
let fresh_name () =
@@ -132,9 +141,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]
@@ -153,7 +159,7 @@ let fix_eff_exp (E_aux (e,((l,_) as annot))) = match snd annot with
| E_exit e -> union_effects eff (effect_of e)
| E_return e -> union_effects eff (effect_of e)
| E_sizeof _ | E_sizeof_internal _ | E_constraint _ -> no_effect
- | E_assert (c,m) -> eff
+ | E_assert (c,m) -> union_eff_exps [c; m]
| E_comment _ | E_comment_struc _ -> no_effect
| E_internal_cast (_,e) -> effect_of e
| E_internal_exp _ -> no_effect
@@ -216,8 +222,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 +369,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 +396,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 +544,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))) =
@@ -574,7 +570,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
let rewrite_def rewriters d = match d with
- | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ -> d
+ | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d
| DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
@@ -625,11 +621,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 +639,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 +660,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 +668,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 +696,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 +741,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 +761,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 +820,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 +836,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 +881,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 +899,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 +929,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 +983,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
}
@@ -1146,7 +1123,10 @@ let rewrite_sizeof (Defs defs) =
if Bindings.mem f param_map then
(* Retrieve instantiation of the type variables of the called function
for the given parameters in the original environment *)
- let inst = instantiation_of orig_exp in
+ let inst =
+ try instantiation_of orig_exp with
+ | Type_error (l, err) ->
+ raise (Reporting_basic.err_typ l (string_of_type_error err)) in
(* Rewrite the inst using orig_kid so that each type variable has it's
original name rather than a mangled typechecker name *)
let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in
@@ -1157,7 +1137,9 @@ let rewrite_sizeof (Defs defs) =
match uvar with
| Some (U_nexp nexp) ->
let sizeof = E_aux (E_sizeof nexp, (l, Some (env, atom_typ nexp, no_effect))) in
- rewrite_trivial_sizeof_exp sizeof
+ (try rewrite_trivial_sizeof_exp sizeof with
+ | Type_error (l, err) ->
+ raise (Reporting_basic.err_typ l (string_of_type_error err)))
(* If the type variable is Not_found then it was probably
introduced by a P_var pattern, so it likely exists as
a variable in scope. It can't be an existential because the assert rules that out. *)
@@ -1188,7 +1170,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 +1215,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 +1287,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 +1314,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 +1355,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 +1432,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 +1485,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 +1615,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) ->
- 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) ->
+ | 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_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 +1641,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)) ->
- 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)) ->
+ | 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_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 +1709,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 +1747,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 +1816,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 +1840,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))
@@ -1902,8 +1854,7 @@ let remove_bitvector_pat pat =
let t = Env.base_typ_of env (typ_of_annot annot) in
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_vector _, true, false ->
P_aux (P_as (P_aux (pat,annot),fresh_id "b__" l), annot)
| _ -> P_aux (pat,annot)
)
@@ -1967,7 +1918,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 +2001,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 +2022,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 +2049,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) ->
+ | 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_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_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 +2082,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)) ->
+ | 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_explicit (t,pat',exp),a))] @ defvals
- | DEF_val (LB_aux (LB_val_implicit (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 +2116,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
@@ -2396,7 +2333,9 @@ let rewrite_defs_early_return =
| _ -> E_block es in
let e_if (e1, e2, e3) =
- if is_return e2 && is_return e3 then E_if (e1, get_return e2, get_return e3)
+ if is_return e2 && is_return e3 then
+ let (E_aux (_, annot)) = e2 in
+ E_return (E_aux (E_if (e1, get_return e2, get_return e3), annot))
else E_if (e1, e2, e3) in
let e_case (e, pes) =
@@ -2405,8 +2344,12 @@ let rewrite_defs_early_return =
let get_return_pexp (Pat_aux (pexp, a)) = match pexp with
| Pat_exp (p, e) -> Pat_aux (Pat_exp (p, get_return e), a)
| Pat_when (p, g, e) -> Pat_aux (Pat_when (p, g, get_return e), a) in
+ let annot = match pes with
+ | Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
+ | Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
+ | [] -> (Parse_ast.Unknown, None) in
if List.for_all is_return_pexp pes
- then E_return (E_aux (E_case (e, List.map get_return_pexp pes), (Parse_ast.Unknown, None)))
+ then E_return (E_aux (E_case (e, List.map get_return_pexp pes), annot))
else E_case (e, pes) in
let e_aux (exp, (l, annot)) =
@@ -2441,19 +2384,68 @@ let rewrite_defs_early_return =
rewrite_defs_base { rewriters_base with rewrite_fun = rewrite_fun_early_return }
+(* Propagate effects of functions, if effect checking and propagation
+ have not been performed already by the type checker. *)
+let rewrite_fix_fun_effs (Defs defs) =
+ let e_aux fun_effs (exp, (l, annot)) =
+ match fix_eff_exp (E_aux (exp, (l, annot))) with
+ | E_aux (E_app_infix (_, f, _) as exp, (l, Some (env, typ, eff)))
+ | E_aux (E_app (f, _) as exp, (l, Some (env, typ, eff)))
+ when Bindings.mem f fun_effs ->
+ let eff' = Bindings.find f fun_effs in
+ let env =
+ try
+ match Env.get_val_spec f env with
+ | (tq, Typ_aux (Typ_fn (args_t, ret_t, eff), a)) ->
+ Env.update_val_spec f (tq, Typ_aux (Typ_fn (args_t, ret_t, union_effects eff eff'), a)) env
+ | _ -> env
+ with
+ | _ -> env in
+ E_aux (exp, (l, Some (env, typ, union_effects eff eff')))
+ | e_aux -> e_aux in
+
+ let rewrite_exp fun_effs = fold_exp { id_exp_alg with e_aux = e_aux fun_effs } in
+
+ let rewrite_funcl (fun_effs, funcls) (FCL_aux (FCL_Funcl (id, pat, exp), (l, annot))) =
+ let exp = propagate_exp_effect (rewrite_exp fun_effs exp) in
+ let fun_eff =
+ try union_effects (effect_of exp) (Bindings.find id fun_effs)
+ with Not_found -> (effect_of exp) in
+ let annot =
+ match annot with
+ | Some (env, typ, eff) -> Some (env, typ, union_effects eff fun_eff)
+ | None -> None in
+ (Bindings.add id fun_eff fun_effs,
+ funcls @ [FCL_aux (FCL_Funcl (id, pat, exp), (l, annot))]) in
+
+ let rewrite_def (fun_effs, defs) = function
+ | DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effopt, funcls), a)) ->
+ let (fun_effs, funcls) = List.fold_left rewrite_funcl (fun_effs, []) funcls in
+ (* Repeat once for recursive functions:
+ propagates union of effects to all clauses *)
+ let (fun_effs, funcls) = List.fold_left rewrite_funcl (fun_effs, []) funcls in
+ (fun_effs, defs @ [DEF_fundef (FD_aux (FD_function (recopt, tannotopt, effopt, funcls), a))])
+ | DEF_val (LB_aux (LB_val (pat, exp), a)) ->
+ (fun_effs, defs @ [DEF_val (LB_aux (LB_val (pat, rewrite_exp fun_effs exp), a))])
+ | def -> (fun_effs, defs @ [def]) in
+
+ if !Type_check.opt_no_effects
+ then Defs (snd (List.fold_left rewrite_def (Bindings.empty, []) defs))
+ else Defs defs
+
(* Turn constraints into numeric expressions with sizeof *)
let rewrite_constraint =
let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux)
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 +2485,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 +2562,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 +2579,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 = {
@@ -2611,17 +2597,80 @@ let rewrite_simple_types (Defs defs) =
let defs = Defs (List.map simple_def defs) in
rewrite_defs_base simple_defs defs
+let rewrite_tuple_vector_assignments defs =
+ let assign_tuple e_aux annot =
+ let env = env_of_annot annot in
+ match e_aux with
+ | E_assign (LEXP_aux (LEXP_tup lexps, lannot), exp) ->
+ let typ = Env.base_typ_of env (typ_of exp) in
+ if is_vector_typ typ then
+ (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *)
+ let (start, _, ord, etyp) = vector_typ_args_of typ in
+ let len (LEXP_aux (le, lannot)) =
+ let ltyp = Env.base_typ_of env (typ_of_annot lannot) in
+ if is_vector_typ ltyp then
+ let (_, len, _, _) = vector_typ_args_of ltyp in
+ match simplify_nexp len with
+ | Nexp_aux (Nexp_constant len, _) -> len
+ | _ -> 1
+ else 1 in
+ let next i step =
+ if is_order_inc ord
+ then (i + step - 1, i + step)
+ else (i - step + 1, i - step) in
+ let i = match simplify_nexp start with
+ | (Nexp_aux (Nexp_constant i, _)) -> i
+ | _ -> if is_order_inc ord then 0 else List.length lexps - 1 in
+ let l = Parse_ast.Generated (fst annot) in
+ let exp' =
+ if small exp then strip_exp exp
+ else mk_exp (E_id (mk_id "split_vec")) in
+ let lexp_to_exp (i, exps) lexp =
+ let (j, i') = next i (len lexp) in
+ let i_exp = mk_exp (E_lit (mk_lit (L_num i))) in
+ let j_exp = mk_exp (E_lit (mk_lit (L_num j))) in
+ let sub = mk_exp (E_vector_subrange (exp', i_exp, j_exp)) in
+ (i', exps @ [sub]) in
+ let (_, exps) = List.fold_left lexp_to_exp (i, []) lexps in
+ let tup = mk_exp (E_tuple exps) in
+ let lexp = LEXP_aux (LEXP_tup (List.map strip_lexp lexps), (l, ())) in
+ let e_aux =
+ if small exp then mk_exp (E_assign (lexp, tup))
+ else mk_exp (
+ E_let (
+ mk_letbind (mk_pat (P_id (mk_id "split_vec"))) (strip_exp exp),
+ mk_exp (E_assign (lexp, tup)))) in
+ begin
+ try check_exp env e_aux unit_typ with
+ | Type_error (l, err) ->
+ raise (Reporting_basic.err_typ l (string_of_type_error err))
+ end
+ else E_aux (e_aux, annot)
+ | _ -> E_aux (e_aux, annot)
+ in
+ let assign_exp = {
+ id_exp_alg with
+ e_aux = (fun (e_aux, annot) -> assign_tuple e_aux annot)
+ } in
+ let assign_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp assign_exp) } in
+ rewrite_defs_base assign_defs defs
+
let rewrite_tuple_assignments defs =
let assign_tuple e_aux annot =
let env = env_of_annot annot in
match e_aux with
| E_assign (LEXP_aux (LEXP_tup lexps, _), exp) ->
+ (* let _ = Pretty_print_common.print stderr (Pretty_print_sail.doc_exp (E_aux (e_aux, annot))) in *)
let (_, ids) = List.fold_left (fun (n, ids) _ -> (n + 1, ids @ [mk_id ("tup__" ^ string_of_int n)])) (0, []) lexps in
let block_assign i lexp = mk_exp (E_assign (strip_lexp lexp, mk_exp (E_id (mk_id ("tup__" ^ string_of_int i))))) in
let block = mk_exp (E_block (List.mapi block_assign lexps)) in
let letbind = mk_letbind (mk_pat (P_tup (List.map (fun id -> mk_pat (P_id id)) ids))) (strip_exp exp) in
let let_exp = mk_exp (E_let (letbind, block)) in
- check_exp env let_exp unit_typ
+ begin
+ try check_exp env let_exp unit_typ with
+ | Type_error (l, err) ->
+ raise (Reporting_basic.err_typ l (string_of_type_error err))
+ end
| _ -> E_aux (e_aux, annot)
in
let assign_exp = {
@@ -2654,7 +2703,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))
@@ -2686,23 +2735,25 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
| Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" ->
let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) in
let body = body e in
+ let body_typ = try typ_of body with _ -> unit_typ in
let annot_pat = simple_annot l unit_typ in
let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
+ let annot_let = (Parse_ast.Generated l, Some (env, body_typ, 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
+ let annot_pat = simple_annot l typ in
let e_id = E_aux (E_id id, (Parse_ast.Generated l, Some (env, typ, no_effect))) in
let body = body e_id in
+ let body_typ = try typ_of body with _ -> unit_typ in
let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, typ_of body, union_eff_exps [v;body])) in
+ let annot_let = (Parse_ast.Generated l, Some (env, body_typ, 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 +2817,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
@@ -2805,7 +2853,7 @@ let rewrite_defs_letbind_effects =
let (E_aux (_,(l,tannot))) = exp in
let exp =
if newreturn then
- let typ = typ_of exp in
+ let typ = try typ_of exp with _ -> unit_typ in
E_aux (E_internal_return exp, simple_annot l typ)
else
exp in
@@ -2857,12 +2905,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 ->
@@ -2907,7 +2949,7 @@ let rewrite_defs_letbind_effects =
| E_case (exp1,pexps) ->
let newreturn =
List.fold_left
- (fun b pexp -> b || effectful_effs (effect_of_pexp pexp))
+ (fun b pexp -> b || (try effectful_effs (effect_of_pexp pexp) with _ -> false))
false pexps in
n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
@@ -2956,20 +2998,20 @@ let rewrite_defs_letbind_effects =
let newreturn =
List.fold_left
(fun b (FCL_aux (FCL_Funcl(id,pat,exp),(_,annot))) ->
- b || effectful_effs (effect_of_annot annot)) false funcls in
+ b || (try effectful exp with _ -> false)) false funcls in
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),annot)) =
let _ = reset_fresh_name_counter () in
FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in
- let rewrite_def rewriters = function
+ let rewrite_def rewriters def =
+ (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
+ match def with
| DEF_val (LB_aux (lb, annot)) ->
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 +3035,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 +3052,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 +3335,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 +3357,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) ->
@@ -3365,34 +3399,19 @@ let remove_reference_types exp =
let rewrite_defs_remove_superfluous_letbinds =
- let rec small (E_aux (exp,_)) = match exp with
- | E_id _
- | E_lit _ -> true
- | E_cast (_,e) -> small e
- | E_list es -> List.for_all small es
- | E_cons (e1,e2) -> small e1 && small e2
- | E_sizeof _ -> true
- | _ -> false in
-
let e_aux (exp,annot) = match exp with
| 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),_),
- 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),_),
+ | LB_aux (LB_val (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
@@ -3420,7 +3439,7 @@ let rewrite_defs_remove_superfluous_returns =
| _ -> false in
let e_aux (exp,annot) = match exp with
- | E_internal_plet (pat,exp1,exp2) ->
+ | E_internal_plet (pat,exp1,exp2) when effectful exp1 ->
begin match pat,exp2 with
| P_aux (P_lit (L_aux (lit,_)),_),
E_aux (E_internal_return (E_aux (E_lit (L_aux (lit',_)),_)),_)
@@ -3465,36 +3484,40 @@ let rewrite_defs_remove_e_assign =
let recheck_defs defs = fst (check initial_env defs)
-let rewrite_defs_lem =[
- top_sort_defs;
- rewrite_trivial_sizeof;
- rewrite_sizeof;
- rewrite_defs_remove_vector_concat;
- rewrite_defs_remove_bitvector_pats;
- rewrite_defs_guarded_pats;
- (* recheck_defs; *)
- rewrite_defs_early_return;
- rewrite_defs_exp_lift_assign;
- rewrite_defs_remove_blocks;
- rewrite_defs_letbind_effects;
- rewrite_defs_remove_e_assign;
- rewrite_defs_effectful_let_expressions;
- rewrite_defs_remove_superfluous_letbinds;
- rewrite_defs_remove_superfluous_returns
+let rewrite_defs_lem = [
+ ("top_sort_defs", top_sort_defs);
+ ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
+ ("tuple_assignments", rewrite_tuple_assignments);
+ (* ("simple_assignments", rewrite_simple_assignments); *)
+ ("constraint", rewrite_constraint);
+ ("trivial_sizeof", rewrite_trivial_sizeof);
+ ("sizeof", rewrite_sizeof);
+ ("remove_vector_concat", rewrite_defs_remove_vector_concat);
+ ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats);
+ ("guarded_pats", rewrite_defs_guarded_pats);
+ (* ("recheck_defs", recheck_defs); *)
+ ("early_return", rewrite_defs_early_return);
+ ("fix_fun_effs", rewrite_fix_fun_effs);
+ ("exp_lift_assign", rewrite_defs_exp_lift_assign);
+ ("remove_blocks", rewrite_defs_remove_blocks);
+ ("letbind_effects", rewrite_defs_letbind_effects);
+ ("remove_e_assign", rewrite_defs_remove_e_assign);
+ ("effectful_let_expressions", rewrite_defs_effectful_let_expressions);
+ ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
+ ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns)
]
let rewrite_defs_ocaml = [
- (* top_sort_defs; *)
- rewrite_undefined;
- rewrite_tuple_assignments;
- rewrite_simple_assignments;
- rewrite_defs_remove_vector_concat;
- rewrite_constraint;
- rewrite_trivial_sizeof;
- rewrite_sizeof;
- rewrite_simple_types;
- rewrite_overload_cast;
- rewrite_defs_exp_lift_assign;
- (* rewrite_defs_exp_lift_assign *)
- (* rewrite_defs_separate_numbs *)
+ (* ("top_sort_defs", top_sort_defs); *)
+ ("undefined", rewrite_undefined);
+ ("tuple_assignments", rewrite_tuple_assignments);
+ ("simple_assignments", rewrite_simple_assignments);
+ ("remove_vector_concat", rewrite_defs_remove_vector_concat);
+ ("constraint", rewrite_constraint);
+ ("trivial_sizeof", rewrite_trivial_sizeof);
+ ("sizeof", rewrite_sizeof);
+ ("simple_types", rewrite_simple_types);
+ ("overload_cast", rewrite_overload_cast);
+ ("exp_lift_assign", rewrite_defs_exp_lift_assign);
+ (* ("separate_numbs", rewrite_defs_separate_numbs) *)
]
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 11394ec6..1c3e8fae 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -56,8 +56,8 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp;
val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
val rewrite_defs : tannot defs -> tannot defs
-val rewrite_defs_ocaml : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_lem : (tannot defs -> tannot defs) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
+val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
(* the type of interpretations of pattern-matching expressions *)
type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
@@ -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 312a3c7c..ca121a79 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -50,6 +50,8 @@ 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_memo_z3 = ref false
let opt_libs_lem = ref ([]:string list)
let opt_libs_ocaml = ref ([]:string list)
let opt_file_arguments = ref ([]:string list)
@@ -103,6 +105,12 @@ 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");
+ ( "-memo_z3",
+ Arg.Set opt_memo_z3,
+ " Memoize calls to z3");
( "-ddump_tc_ast",
Arg.Set opt_ddump_tc_ast,
" (debug) dump the typechecked ast to stdout");
@@ -118,7 +126,7 @@ let options = Arg.align ([
( "-no_effects",
Arg.Set Type_check.opt_no_effects,
" turn off effect checking");
- ( "-undefined-gen",
+ ( "-undefined_gen",
Arg.Set Initial_check.opt_undefined_gen,
" generate undefined_type functions for types in the specification");
( "-v",
@@ -142,12 +150,18 @@ let main() =
if !(opt_print_version)
then Printf.printf "Sail private release \n"
else
+ if !opt_memo_z3 then Constraint.load_digests () else ();
let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in
let ast =
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) =
@@ -160,6 +174,9 @@ let main() =
let out_name = match !opt_file_out with
| None -> fst (List.hd parsed)
| Some f -> f ^ ".sail" in
+
+ if !opt_memo_z3 then Constraint.save_digests () else ();
+
(*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
begin
(if !(opt_print_verbose)
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 8dabbd30..3b13abb8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -70,6 +70,7 @@ type type_error =
coercions, the second is the errors encountered by all possible
coercions *)
| Err_no_casts of type_error * type_error list
+ | Err_no_overloading of id * (id * type_error) list
| Err_unresolved_quants of id * quant_item list
| Err_subtype of typ * typ * n_constraint list
| Err_no_num_ident of id
@@ -83,6 +84,9 @@ let pp_type_error err =
^/^ string "No possible coercions"
| Err_no_casts (trigger, errs) ->
(string "Tried performing type coerction because" ^//^ pp_err trigger)
+ | Err_no_overloading (id, errs) ->
+ string ("No overloadings for " ^ string_of_id id ^ ", tried:") ^//^
+ group (separate_map hardline (fun (id, err) -> string (string_of_id id) ^^ colon ^^ space ^^ pp_err err) errs)
| Err_subtype (typ1, typ2, []) ->
separate space [ string (string_of_typ typ1);
string "is not a subtype of";
@@ -153,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 *)
@@ -226,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
@@ -338,6 +342,7 @@ type lvar = Register of typ | Enum of typ | Local of mut * typ | Union of typqua
module Env : sig
type t
val add_val_spec : id -> typquant * typ -> t -> t
+ val update_val_spec : id -> typquant * typ -> t -> t
val get_val_spec : id -> t -> typquant * typ
val is_union_constructor : id -> t -> bool
val add_record : id -> typquant -> (typ * id) list -> t -> t
@@ -458,14 +463,16 @@ end = struct
with
| Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
+ let update_val_spec id bind env =
+ begin
+ typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind);
+ { env with top_val_specs = Bindings.add id bind env.top_val_specs }
+ end
+
let add_val_spec id bind env =
if Bindings.mem id env.top_val_specs
then typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound")
- else
- begin
- typ_print ("Adding val spec binding " ^ string_of_id id ^ " :: " ^ string_of_bind bind);
- { env with top_val_specs = Bindings.add id bind env.top_val_specs }
- end
+ else update_val_spec id bind env
let is_union_constructor id env =
let is_ctor id (Tu_aux (tu, _)) = match tu with
@@ -777,11 +784,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 -> ()
@@ -917,14 +924,14 @@ let initial_env =
let ex_counter = ref 0
-let fresh_existential () =
- let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter), Parse_ast.Unknown) in
+let fresh_existential ?name:(n="") () =
+ let fresh = Kid_aux (Var ("'ex" ^ string_of_int !ex_counter ^ "#" ^ n), Parse_ast.Unknown) in
incr ex_counter; fresh
let destruct_exist env typ =
match Env.expand_synonyms env typ with
| Typ_aux (Typ_exist (kids, nc, typ), _) ->
- let fresh_kids = List.map (fun kid -> (kid, fresh_existential ())) kids in
+ let fresh_kids = List.map (fun kid -> (kid, fresh_existential ~name:(string_of_id (id_of_kid kid)) ())) kids in
let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in
let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in
Some (List.map snd fresh_kids, nc, typ)
@@ -1065,12 +1072,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)
@@ -1101,9 +1108,9 @@ let prove_z3 env nc =
in
let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.negate (nc_constraint env var_of nc)) in
match Constraint.call_z3 constr with
- | Constraint.Unsat _ -> typ_debug "unsat"; true
- | Constraint.Unknown [] -> typ_debug "sat"; false
- | Constraint.Unknown _ -> typ_debug "unknown"; false
+ | Constraint.Unsat -> typ_debug "unsat"; true
+ | Constraint.Sat -> typ_debug "sat"; false
+ | Constraint.Unknown -> typ_debug "unknown"; false
let prove env (NC_aux (nc_aux, _) as nc) =
let compare_const f (Nexp_aux (n1, _)) (Nexp_aux (n2, _)) =
@@ -1112,10 +1119,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
@@ -1167,15 +1174,15 @@ let rec subtyp_tnf env tnf1 tnf2 =
let (prop1, prop2) = props_subst kid1 (Nexp_var kid3) prop1, props_subst kid2 (Nexp_var kid3) prop2 in
let constr = Constraint.conj (nc_constraints env var_of (Env.get_constraints env)) (Constraint.conj (pos_props prop1) (neg_props prop2)) in
match Constraint.call_z3 constr with
- | Constraint.Unsat _ -> typ_debug "unsat"; true
- | Constraint.Unknown [] -> typ_debug "sat"; false
- | Constraint.Unknown _ -> typ_debug "unknown"; false
+ | Constraint.Unsat -> typ_debug "unsat"; true
+ | Constraint.Sat -> typ_debug "sat"; false
+ | Constraint.Unknown -> typ_debug "unknown"; false
end
| _, _ -> false
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
@@ -1274,7 +1281,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
@@ -1305,7 +1312,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
@@ -1320,7 +1327,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
@@ -1653,22 +1660,41 @@ let destruct_atom_nexp env typ =
exception Not_a_constraint;;
-let rec assert_nexp (E_aux (exp_aux, l)) =
+let rec assert_nexp env (E_aux (exp_aux, _)) =
match exp_aux with
| E_sizeof nexp -> nexp
+ | E_id id ->
+ begin
+ match Env.lookup_id id env with
+ | Local (Immutable, typ) ->
+ begin
+ match destruct_atom_nexp env typ with
+ | Some nexp -> nexp
+ | None -> raise Not_a_constraint
+ end
+ | _ -> raise Not_a_constraint
+ end
| E_lit (L_aux (L_num n, _)) -> nconstant n
| _ -> raise Not_a_constraint
-let rec assert_constraint (E_aux (exp_aux, l)) =
+let rec assert_constraint env (E_aux (exp_aux, _) as exp) =
match exp_aux with
- | E_app_infix (x, op, y) when string_of_id op = "|" ->
- nc_or (assert_constraint x) (assert_constraint y)
- | E_app_infix (x, op, y) when string_of_id op = "&" ->
- nc_and (assert_constraint x) (assert_constraint y)
- | E_app_infix (x, op, y) when string_of_id op = "==" ->
- nc_eq (assert_nexp x) (assert_nexp y)
- | E_app_infix (x, op, y) when string_of_id op = ">=" ->
- nc_gteq (assert_nexp x) (assert_nexp y)
+ | E_app (op, [x; y]) when string_of_id op = "or_bool" ->
+ nc_or (assert_constraint env x) (assert_constraint env y)
+ | E_app (op, [x; y]) when string_of_id op = "and_bool" ->
+ nc_and (assert_constraint env x) (assert_constraint env y)
+ | E_app (op, [x; y]) when string_of_id op = "gteq_atom" ->
+ nc_gteq (assert_nexp env x) (assert_nexp env y)
+ | E_app (op, [x; y]) when string_of_id op = "lteq_atom" ->
+ nc_lteq (assert_nexp env x) (assert_nexp env y)
+ | E_app (op, [x; y]) when string_of_id op = "gt_atom" ->
+ nc_gt (assert_nexp env x) (assert_nexp env y)
+ | E_app (op, [x; y]) when string_of_id op = "lt_atom" ->
+ nc_lt (assert_nexp env x) (assert_nexp env y)
+ | E_app (op, [x; y]) when string_of_id op = "eq_atom" ->
+ nc_eq (assert_nexp env x) (assert_nexp env y)
+ | E_app (op, [x; y]) when string_of_id op = "neq_atom" ->
+ nc_neq (assert_nexp env x) (assert_nexp env y)
| _ -> nc_true
type flow_constraint =
@@ -1854,10 +1880,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
typ_print ("Adding constraint " ^ string_of_n_constraint nc ^ " for assert");
let inferred_exp = irule infer_exp env exp in
inferred_exp :: check_block l (Env.add_constraint nc env) exps typ
- | ((E_aux (E_assert (const_expr, assert_msg), _) as exp) :: exps) ->
+ | ((E_aux (E_assert (constr_exp, assert_msg), _) as exp) :: exps) ->
begin
try
- let nc = assert_constraint const_expr in
+ let constr_exp = crule check_exp env constr_exp bool_typ in
+ let nc = assert_constraint env constr_exp in
let cexp = annot_exp (E_constraint nc) bool_typ in
let checked_msg = crule check_exp env assert_msg string_typ in
let texp = annot_exp (E_assert (cexp, checked_msg)) unit_typ in
@@ -1873,7 +1900,13 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
end
| E_case (exp, cases), _ ->
let inferred_exp = irule infer_exp env exp in
- let check_case pat typ = match pat with
+ let rec check_case pat typ = match pat with
+ | Pat_aux (Pat_exp (P_aux (P_lit lit, _) as pat, case), annot) ->
+ let guard = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in
+ check_case (Pat_aux (Pat_when (mk_pat (P_id (mk_id "p#")), guard, case), annot)) typ
+ | Pat_aux (Pat_when (P_aux (P_lit lit, _) as pat, guard, case), annot) ->
+ let guard' = mk_exp (E_app_infix (mk_exp (E_id (mk_id "p#")), mk_id "==", mk_exp (E_lit lit))) in
+ check_case (Pat_aux (Pat_when (mk_pat (P_id (mk_id "p#")), mk_exp (E_app_infix (guard, mk_id "&", guard')), case), annot)) typ
| Pat_aux (Pat_exp (pat, case), (l, _)) ->
let tpat, env = bind_pat env pat (typ_of inferred_exp) in
Pat_aux (Pat_exp (tpat, crule check_exp env case typ), (l, None))
@@ -1946,17 +1979,16 @@ 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 ->
+ | E_app_infix (x, op, y), _ ->
check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
| E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 ->
if prove env nc
@@ -1964,14 +1996,16 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
else typ_error l ("Cannot prove " ^ string_of_n_constraint nc)
| E_app (f, xs), _ when List.length (Env.get_overloads f env) > 0 ->
let rec try_overload = function
- | [] -> typ_error l ("No valid overloading for " ^ string_of_exp exp)
- | (f :: fs) -> begin
+ | (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
+ | (errs, (f :: fs)) -> begin
typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with
- | Type_error (_, err) -> typ_print ("Error : " ^ string_of_type_error err); try_overload fs
+ | Type_error (_, err) ->
+ typ_print ("Error : " ^ string_of_type_error err);
+ try_overload (errs @ [(f, err)], fs)
end
in
- try_overload (Env.get_overloads f env)
+ try_overload ([], Env.get_overloads f env)
| E_return exp, _ ->
let checked_exp = match Env.get_ret_typ env with
| Some ret_typ -> crule check_exp env exp ret_typ
@@ -2108,22 +2142,33 @@ 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_aux (Typ_id id, _) when Id.compare id (mk_id "nat") == 0 ->
+ let env = Env.add_typ_var kid BK_nat env in
+ let env = Env.add_constraint (nc_gt (nvar kid) (nconstant 0)) 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_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp lo, _); Typ_arg_aux (Typ_arg_nexp hi, _)]), _)
+ when Id.compare id (mk_id "range") == 0 ->
+ let env = Env.add_typ_var kid BK_nat env in
+ let env = Env.add_constraint (nc_and (nc_lteq lo (nvar kid)) (nc_lteq (nvar kid) hi)) 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 or numeric type")
end
| P_wild -> annot_pat P_wild typ, env
| P_cons (hd_pat, tl_pat) ->
@@ -2388,20 +2433,49 @@ and bind_lexp env (LEXP_aux (lexp_aux, (l, ())) as lexp) typ =
in
annot_lexp (LEXP_tup tlexps) typ, env
(* This case is pretty much just for the PSTATE.<N,Z,C,V> := vector pattern which is really common in ASL. *)
+ (* Maybe this code can be made not horrible? *)
| Typ_app (id, _) when Id.compare id (mk_id "vector") == 0 ->
begin
match destruct_vector env typ with
| Some (_, vec_len, _, _) ->
- let bind_bit_tuple lexp (tlexps, env) =
- let tlexp, env = bind_lexp env lexp (lvector_typ env (nconstant 1) bit_typ) in
- tlexp :: tlexps, env
+ let bind_bits_tuple lexp (tlexps, env, llen) =
+ match lexp with
+ | LEXP_aux (LEXP_id v, _) ->
+ begin
+ match Env.lookup_id v env with
+ | Local (Immutable, _) | Enum _ ->
+ typ_error l ("Cannot modify let-bound constant or enumeration constructor " ^ string_of_id v)
+ | Unbound ->
+ typ_error l "Unbound variable in vector tuple assignment"
+ | Local (Mutable, vtyp) | Register vtyp ->
+ let llen' = match destruct_vector env vtyp with
+ | Some (_, llen', _, _) -> llen'
+ | None -> typ_error l "Variables in vector tuple assignment must be vectors"
+ in
+ let tlexp, env = bind_lexp env lexp vtyp in
+ tlexp :: tlexps, env, nsum llen llen'
+ end
+ | LEXP_aux (LEXP_field (LEXP_aux (LEXP_id v, _), fid), _) ->
+ (* FIXME: will only work for ASL *)
+ let rec_id =
+ match Env.lookup_id v env with
+ | Register (Typ_aux (Typ_id rec_id, _)) -> rec_id
+ | _ -> typ_error l (string_of_lexp lexp ^ " must be a record register here")
+ in
+ let typq, (Typ_aux (Typ_fn (_, vtyp, _), _)) = Env.get_accessor rec_id fid env in
+ let llen' = match destruct_vector env vtyp with
+ | Some (_, llen', _, _) -> llen'
+ | None -> typ_error l "Variables in vector tuple assignment must be vectors"
+ in
+ let tlexp, env = bind_lexp env lexp vtyp in
+ tlexp :: tlexps, env, nsum llen llen'
+ | _ -> typ_error l "bit vector assignment must only contain identifiers"
in
- if prove env (nc_eq vec_len (nconstant (List.length lexps)))
- then
- let (tlexps, env) = List.fold_right bind_bit_tuple lexps ([], env) in
- annot_lexp (LEXP_tup tlexps) typ, env
+ let tlexps, env, lexp_len = List.fold_right bind_bits_tuple lexps ([], env, nconstant 0) in
+ if prove env (nc_eq vec_len lexp_len)
+ then annot_lexp (LEXP_tup tlexps) typ, env
else typ_error l "Vector and tuple length must be the same in assignment"
- | None -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
+ | None -> typ_error l ("Malformed vector type " ^ string_of_typ typ)
end
| _ -> typ_error l ("Cannot bind tuple l-expression against non tuple or vector type " ^ string_of_typ typ)
end
@@ -2547,17 +2621,19 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| E_cast (typ, exp) ->
let checked_exp = crule check_exp env exp typ in
annot_exp (E_cast (typ, checked_exp)) typ
- | E_app_infix (x, op, y) when List.length (Env.get_overloads (deinfix op) env) > 0 -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
+ | E_app_infix (x, op, y) -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
| E_app (f, xs) when List.length (Env.get_overloads f env) > 0 ->
let rec try_overload = function
- | [] -> typ_error l ("No valid overloading for " ^ string_of_exp exp)
- | (f :: fs) -> begin
+ | (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
+ | (errs, (f :: fs)) -> begin
typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with
- | Type_error (_, err) -> typ_print ("Overload error"); try_overload fs
+ | Type_error (_, err) ->
+ typ_print ("Error : " ^ string_of_type_error err);
+ try_overload (errs @ [(f, err)], fs)
end
in
- try_overload (Env.get_overloads f env)
+ try_overload ([], Env.get_overloads f env)
| E_app (f, xs) -> infer_funapp l env f xs None
| E_loop (loop_type, cond, body) ->
let checked_cond = crule check_exp env cond bool_typ in
@@ -2667,7 +2743,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
let iuargs = List.map2 (fun utyp (n, uarg) -> (n, crule check_exp env uarg utyp)) utyps uargs in
(iuargs, ret_typ, env)
else typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants
- ^ " not resolved during application of " ^ string_of_id f)
+ ^ " not resolved during application of " ^ string_of_id f ^ " unresolved args: " ^ string_of_list ", " (fun (_, exp) -> string_of_exp exp) uargs)
end
| (utyps, (typ :: typs)), (uargs, ((n, arg) :: args))
when List.for_all (fun kid -> is_bound kid env) (KidSet.elements (typ_frees typ)) ->
@@ -2700,7 +2776,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
((n, iarg) :: iargs, ret_typ'', env)
with
| Unification_error (l, str) ->
- typ_debug ("Unification error: " ^ str);
+ typ_print ("Unification error: " ^ str);
instantiate env quants (typ :: utyps, typs) ret_typ ((n, arg) :: uargs, args)
end
| (_, []), _ -> typ_error l ("Function " ^ string_of_id f ^ " applied to too many arguments")
@@ -2827,6 +2903,30 @@ and propagate_exp_effect_aux = function
| E_vector xs ->
let p_xs = List.map propagate_exp_effect xs in
E_vector p_xs, collect_effects p_xs
+ | E_vector_access (v, i) ->
+ let p_v = propagate_exp_effect v in
+ let p_i = propagate_exp_effect i in
+ E_vector_access (p_v, p_i), collect_effects [p_v; p_i]
+ | E_vector_subrange (v, i, j) ->
+ let p_v = propagate_exp_effect v in
+ let p_i = propagate_exp_effect i in
+ let p_j = propagate_exp_effect i in
+ E_vector_subrange (p_v, p_i, p_j), collect_effects [p_v; p_i; p_j]
+ | E_vector_update (v, i, x) ->
+ let p_v = propagate_exp_effect v in
+ let p_i = propagate_exp_effect i in
+ let p_x = propagate_exp_effect x in
+ E_vector_update (p_v, p_i, p_x), collect_effects [p_v; p_i; p_x]
+ | E_vector_update_subrange (v, i, j, v') ->
+ let p_v = propagate_exp_effect v in
+ let p_i = propagate_exp_effect i in
+ let p_j = propagate_exp_effect j in
+ let p_v' = propagate_exp_effect v' in
+ E_vector_update_subrange (p_v, p_i, p_j, p_v'), collect_effects [p_v; p_i; p_j; p_v']
+ | E_vector_append (v1, v2) ->
+ let p_v1 = propagate_exp_effect v1 in
+ let p_v2 = propagate_exp_effect v2 in
+ E_vector_append (p_v1, p_v2), collect_effects [p_v1; p_v2]
| E_tuple xs ->
let p_xs = List.map propagate_exp_effect xs in
E_tuple p_xs, collect_effects p_xs
@@ -2950,7 +3050,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
@@ -2974,15 +3076,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)) =
@@ -3019,15 +3116,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 =
@@ -3066,7 +3162,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, _) -> ()
@@ -3117,14 +3213,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)) =
@@ -3233,6 +3328,7 @@ let rec check_def env def =
match def with
| DEF_kind kdef -> check_kinddef env kdef
| DEF_type tdef -> check_typedef env tdef
+ | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
| DEF_fundef fdef -> check_fundef env fdef
| DEF_val letdef -> check_letdef env letdef
| DEF_spec vs -> check_val_spec env vs
diff --git a/src/type_check.mli b/src/type_check.mli
index 838cab7d..b6b5e75e 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -49,6 +49,7 @@ val opt_no_effects : bool ref
type type_error =
| Err_no_casts of type_error * type_error list
+ | Err_no_overloading of id * (id * type_error) list
| Err_unresolved_quants of id * quant_item list
| Err_subtype of typ * typ * n_constraint list
| Err_no_num_ident of id
@@ -71,6 +72,8 @@ module Env : sig
val get_val_spec : id -> t -> typquant * typ
+ val update_val_spec : id -> typquant * typ -> t -> t
+
val get_register : id -> t -> typ
val get_regtyp : id -> t -> int * int * (index_range * id) list
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 00:08:05 +0000