diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constant_fold.ml | 10 | ||||
| -rw-r--r-- | src/ocaml_backend.ml | 7 | ||||
| -rw-r--r-- | src/sail_lib.ml | 5 |
3 files changed, 14 insertions, 8 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml index e9efac68..407bd69a 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -183,15 +183,15 @@ let rec rewrite_constant_function_calls' ast = | E_if (E_aux (E_lit (L_aux (L_true, _)), _), then_exp, _) -> ok (); then_exp | E_if (E_aux (E_lit (L_aux (L_false, _)), _), _, else_exp) -> ok (); else_exp + (* We only propagate lets in the simple case where we know that + the id will have the inferred type of the argument. For more + complex let bindings trying to propagate them may result in + type errors due to how type variables are bound by let bindings + *) | E_let (LB_aux (LB_val (P_aux (P_id id, _), bind), _), exp) when is_constant bind -> ok (); subst id bind exp - | E_let (LB_aux (LB_val (P_aux (P_typ (typ, P_aux (P_id id, _)), annot), bind), _), exp) - when is_constant bind -> - ok (); - subst id (E_aux (E_cast (typ, bind), annot)) exp - | _ -> E_aux (e_aux, annot) in let rw_exp = { diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index 6e5eb774..0ed60e10 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -140,7 +140,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) = match typ_aux with | Typ_id id -> ocaml_typ_id ctx id | Typ_app (id, []) -> ocaml_typ_id ctx id - | Typ_app (id, typs) -> parens (separate_map (string " * ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id + | Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs) | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2] | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types") @@ -160,7 +160,7 @@ let ocaml_typquant typq = match quant_items typq with | [] -> empty | [qi] -> ocaml_qi qi - | qis -> parens (separate_map (string " * ") ocaml_qi qis) + | qis -> parens (separate_map (string ", ") ocaml_qi qis) let string_lit str = dquotes (string (String.escaped str)) @@ -199,6 +199,7 @@ let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) = | P_wild -> string "_" | P_as (pat, id) -> separate space [ocaml_pat ctx pat; string "as"; zencode ctx id] | P_app (id, pats) -> zencode_upper ctx id ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats) + | P_cons (hd_pat, tl_pat) -> ocaml_pat ctx hd_pat ^^ string " :: " ^^ ocaml_pat ctx tl_pat | _ -> string ("PAT<" ^ string_of_pat pat ^ ">") let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string "end") @@ -681,7 +682,7 @@ let ocaml_main spec sail_dir = @ [ " zinitializze_registers ();"; if !opt_trace_ocaml then " Sail_lib.opt_trace := true;" else " ();"; " Printexc.record_backtrace true;"; - " zmain ()\n";]) + " try zmain () with _ -> prerr_endline(\"Exiting due to uncaught exception\")\n";]) |> String.concat "\n" let ocaml_pp_defs f defs = diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 505227ef..f1203725 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -51,6 +51,8 @@ let trace_call str = type bit = B0 | B1 +let eq_anything (a, b) = a = b + let eq_bit (a, b) = a = b let and_bit = function @@ -540,6 +542,9 @@ let gteq_real (x, y) = Rational.geq x y let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *) let negate_real x = Rational.neg x +let print_real (str, r) = print_string "REAL\n" +let prerr_real (str, r) = prerr_string "REAL\n" + let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *) let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *) let quotient_real (x, y) = Rational.div x y |