diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 44 | ||||
| -rw-r--r-- | src/ast_util.mli | 6 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 50 | ||||
| -rw-r--r-- | src/type_error.ml | 51 | ||||
| -rw-r--r-- | src/util.ml | 9 | ||||
| -rw-r--r-- | src/util.mli | 5 |
6 files changed, 154 insertions, 11 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index 3cd2f361..61bc9ba3 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -270,6 +270,47 @@ and nexp_simp_aux = function end | nexp -> nexp +let rec constraint_simp (NC_aux (nc_aux, l)) = + let nc_aux = match nc_aux with + | NC_equal (nexp1, nexp2) -> + let nexp1, nexp2 = nexp_simp nexp1, nexp_simp nexp2 in + if nexp_identical nexp1 nexp2 then + NC_true + else + NC_equal (nexp1, nexp2) + + | NC_and (nc1, nc2) -> + let nc1, nc2 = constraint_simp nc1, constraint_simp nc2 in + begin match nc1, nc2 with + | NC_aux (NC_true, _), NC_aux (nc, _) -> nc + | NC_aux (nc, _), NC_aux (NC_true, _) -> nc + | _, _ -> NC_and (nc1, nc2) + end + + | NC_or (nc1, nc2) -> + let nc1, nc2 = constraint_simp nc1, constraint_simp nc2 in + begin match nc1, nc2 with + | NC_aux (NC_false, _), NC_aux (nc, _) -> nc + | NC_aux (nc, _), NC_aux (NC_false, _) -> nc + | NC_aux (NC_true, _), NC_aux (nc, _) -> NC_true + | NC_aux (nc, _), NC_aux (NC_true, _) -> NC_true + | _, _ -> NC_or (nc1, nc2) + end + + | _ -> nc_aux + in + NC_aux (nc_aux, l) + +let rec constraint_conj (NC_aux (nc_aux, l) as nc) = + match nc_aux with + | NC_and (nc1, nc2) -> constraint_conj nc1 @ constraint_conj nc2 + | _ -> [nc] + +let rec constraint_disj (NC_aux (nc_aux, l) as nc) = + match nc_aux with + | NC_or (nc1, nc2) -> constraint_disj nc1 @ constraint_disj nc2 + | _ -> [nc] + let mk_typ typ = Typ_aux (typ, Parse_ast.Unknown) let mk_typ_arg arg = Typ_arg_aux (arg, Parse_ast.Unknown) let mk_kid str = Kid_aux (Var ("'" ^ str), Parse_ast.Unknown) @@ -618,9 +659,10 @@ and string_of_typ_aux = function | Typ_id id -> string_of_id id | Typ_var kid -> string_of_kid kid | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")" + | Typ_app (id, args) when Id.compare id (mk_id "atom") = 0 -> "int(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")" | Typ_fn ([typ_arg], typ_ret, eff) -> - string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff + string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff | Typ_fn (typ_args, typ_ret, eff) -> "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff diff --git a/src/ast_util.mli b/src/ast_util.mli index 1cd621b4..f55cdf16 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -138,6 +138,12 @@ val no_effect : effect val mk_effect : base_effect_aux list -> effect val nexp_simp : nexp -> nexp +val constraint_simp : n_constraint -> n_constraint + +(* If a constraint is a conjunction, return a list of all the top-level conjuncts *) +val constraint_conj : n_constraint -> n_constraint list +(* Same as constraint_conj but for disjunctions *) +val constraint_disj : n_constraint -> n_constraint list (* Utilities for building n-expressions *) val nconstant : Big_int.num -> nexp diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 7de4dd40..d71b32b2 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -52,6 +52,8 @@ open Ast open Ast_util open PPrint +let opt_use_heuristics = ref false + module Big_int = Nat_big_num let doc_op symb a b = infix 2 1 symb a b @@ -124,11 +126,26 @@ let doc_nc = | NC_set (kid, ints) -> separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)] | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps) - | _ -> 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 + | _ -> nc0 ~parenthesize:true nc + and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) = + (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if + we rewrite a disjunction as a set constraint, then we can + always omit the parens. *) + let parens' = if parenthesize then parens else (fun x -> x) in + let disjs = constraint_disj nc in + let collect_constants kid = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant c, _)), _) when Kid.compare kid kid' = 0 -> Some c + | _ -> None + in + match disjs with + | NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant c, _)), _) :: ncs -> + let constants = List.map (collect_constants kid) ncs in + begin match Util.option_all (List.map (collect_constants kid) ncs) with + | None | Some [] -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) + | Some cs -> + separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int (c :: cs))] + end + | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs) and nc1 (NC_aux (nc_aux, _) as nc) = match nc_aux with | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2] @@ -146,6 +163,7 @@ let rec doc_typ (Typ_aux (typ_aux, l)) = | 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) when Id.compare id (mk_id "atom") = 0 -> string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs) | 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 @@ -172,6 +190,12 @@ and doc_arg_typs = function | [typ] -> doc_typ typ | typs -> parens (separate_map (comma ^^ space) doc_typ typs) +let doc_kopt = function + | KOpt_aux (KOpt_none kid, _) -> doc_kid kid + | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt) + | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"]) + | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"]) + let doc_quants quants = let doc_qi_kopt (QI_aux (qi_aux, _)) = match qi_aux with @@ -193,14 +217,22 @@ let doc_quants quants = | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs) - - -let doc_binding (TypQ_aux (tq_aux, _), typ) = +let doc_binding ((TypQ_aux (tq_aux, _) as typq), 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 + if !opt_use_heuristics && String.length (string_of_typquant typq) > 60 then + let kopts, ncs = quant_split typq in + if ncs = [] then + string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ dot + ^//^ doc_typ typ + else + string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ comma + ^//^ (separate_map (space ^^ string "&" ^^ space) doc_nc ncs ^^ dot + ^^ hardline ^^ doc_typ typ) + else + string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ) diff --git a/src/type_error.ml b/src/type_error.ml index 39c22cde..ada8e16b 100644 --- a/src/type_error.ml +++ b/src/type_error.ml @@ -100,6 +100,56 @@ and nc_subst_nexp_aux l sv subst = function | NC_false -> NC_false | NC_true -> NC_true +type suggestion = + | Suggest_add_constraint of n_constraint + | Suggest_none + +(* Temporary hack while I work on using these suggestions in asl_parser *) +let rec analyze_unresolved_quant2 locals ncs = function + | QI_aux (QI_const nc, _) -> + let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in + if gen_kids = [] then + Suggest_add_constraint nc + else + (* If there are generated kind-identifiers in the constraint, + we don't want to make a suggestion based on them, so try to + look for generated kid free nexps in the set of constraints + that are equal to the generated identifier. This often + occurs due to how the type-checker introduces new type + variables. *) + let is_subst v = function + | NC_aux (NC_equal (Nexp_aux (Nexp_var v', _), nexp), _) + when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) -> + [(v, nexp)] + | NC_aux (NC_equal (nexp, Nexp_aux (Nexp_var v', _)), _) + when Kid.compare v v' = 0 && not (KidSet.exists is_kid_generated (tyvars_of_nexp nexp)) -> + [(v, nexp)] + | _ -> [] + in + let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_subst v nc) ncs)) gen_kids) in + let nc = List.fold_left (fun nc (v, nexp) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in + if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then + Suggest_add_constraint nc + else + (* If we have a really anonymous type-variable, try to find a + regular variable that corresponds to it. *) + let is_linked v = function + | (id, (Immutable, (Typ_aux (Typ_app (ty_id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var v', _)), _)]), _) as typ))) + when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 -> + [(v, nid id, typ)] + | (id, (mut, typ)) -> + [] + in + let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in + let nc = List.fold_left (fun nc (v, nexp, _) -> nc_subst_nexp v (unaux_nexp nexp) nc) nc substs in + if not (KidSet.exists is_kid_generated (tyvars_of_constraint nc)) then + Suggest_none + else + Suggest_none + + | QI_aux (QI_id kopt, _) -> + Suggest_none + let rec analyze_unresolved_quant locals ncs = function | QI_aux (QI_const nc, _) -> let gen_kids = List.filter is_kid_generated (KidSet.elements (tyvars_of_constraint nc)) in @@ -133,7 +183,6 @@ let rec analyze_unresolved_quant locals ncs = function when Id.compare ty_id (mk_id "atom") = 0 && Kid.compare v v' = 0 -> [(v, nid id, typ)] | (id, (mut, typ)) -> - prerr_endline (string_of_id id ^ " : " ^ string_of_typ typ); [] in let substs = List.concat (List.map (fun v -> List.concat (List.map (fun nc -> is_linked v nc) (Bindings.bindings locals))) gen_kids) in diff --git a/src/util.ml b/src/util.ml index e0366fe7..c0b88815 100644 --- a/src/util.ml +++ b/src/util.ml @@ -232,6 +232,15 @@ let rec option_these = function | None :: xs -> option_these xs | [] -> [] +let rec option_all = function + | [] -> Some [] + | None :: _ -> None + | Some x :: xs -> + begin match option_all xs with + | None -> None + | Some xs -> Some (x :: xs) + end + let changed2 f g x h y = match (g x, h y) with | (None,None) -> None diff --git a/src/util.mli b/src/util.mli index eb4b4bd2..5bb7c559 100644 --- a/src/util.mli +++ b/src/util.mli @@ -105,6 +105,11 @@ val option_get_exn : exn -> 'a option -> 'a wrapped in [Some]. *) val option_these : 'a option list -> 'a list +(** [option_all xs] extracts the elements of the list [xs] if all of + them are wrapped in Some. If any are None then the result is None is + None. [option_all []] is [Some []] *) +val option_all : 'a option list -> 'a list option + (** [changed2 f g x h y] applies [g] to [x] and [h] to [y]. If both function applications return [None], then [None] is returned. Otherwise [f] is applied to the results. For this |