diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast_util.ml | 7 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 17 | ||||
| -rw-r--r-- | src/type_check.ml | 54 |
4 files changed, 63 insertions, 17 deletions
diff --git a/src/ast_util.ml b/src/ast_util.ml index f0b6508b..037fd1a7 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -399,6 +399,13 @@ let mk_effect effs = let no_effect = mk_effect [] +let quant_add qi typq = + match qi, typq with + | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq + | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l) + | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l) + | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l) + let quant_items : typquant -> quant_item list = function | TypQ_aux (TypQ_tq qis, _) -> qis | TypQ_aux (TypQ_no_forall, _) -> [] diff --git a/src/ast_util.mli b/src/ast_util.mli index 2a303475..8f555744 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -175,6 +175,8 @@ val nc_int_set : kid -> int list -> n_constraint de-morgans to switch and to or and vice versa. *) val nc_negate : n_constraint -> n_constraint +(* Functions for working with type quantifiers *) +val quant_add : quant_item -> typquant -> typquant val quant_items : typquant -> quant_item list val quant_kopts : typquant -> kinded_id list val quant_split : typquant -> kinded_id list * n_constraint list diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index 93693339..31b1ed85 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -68,7 +68,7 @@ let doc_kid kid = string (Ast_util.string_of_kid kid) let doc_int n = string (Big_int.to_string n) let docstring (l, _) = match l with - | Parse_ast.Documented (str, _) -> string "/**" ^^ string str ^^ string "*/" ^^ hardline + | Parse_ast.Documented (str, _) -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline | _ -> empty let doc_ord (Ord_aux(o,_)) = match o with @@ -483,13 +483,14 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) = let doc_default (DT_aux (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_fundef (FD_aux (FD_function (r, typa, efa, funcls), annot)) = + docstring annot + ^^ 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 rec doc_mpat (MP_aux (mp_aux, _) as mpat) = match mp_aux with diff --git a/src/type_check.ml b/src/type_check.ml index e11505e5..aa2d3473 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -754,17 +754,52 @@ end = struct with | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id) + let ex_counter = ref 0 + + (* TODO: Currently this is duplicated with destruct_exist outside of Env and deals with val spec arguments only. *) + let fresh_existential ?name:(n="") () = + let fresh = Kid_aux (Var ("'all" ^ string_of_int !ex_counter ^ "#" ^ n), Parse_ast.Unknown) in + incr ex_counter; fresh + + let destruct_exist env typ = + match expand_synonyms env typ with + | Typ_aux (Typ_exist (kids, nc, typ), _) -> + 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) + | _ -> None + let rec update_val_spec id (typq, typ) env = - begin - let typ = expand_synonyms env typ in - let typq = expand_typquant_synonyms env typq in - typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); - let env = match typ with - | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env - | _ -> env - in - { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } + begin match expand_synonyms env typ with + | Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) -> + (* We perform some canonicalisation for function types where existentials appear on the left, so + ({'n, 'n >= 2, int('n)}, foo) -> bar + would become + forall 'n, 'n >= 2. (int('n), foo) -> bar + this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials) + *) + let typq = expand_typquant_synonyms env typq in + let base_args = List.map (destruct_exist env) arg_typs in + let existential_arg typq = function + | None -> typq + | Some (exs, nc, _) -> + List.fold_left (fun typq kid -> quant_add (mk_qi_id BK_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs + in + let typq = List.fold_left existential_arg typq base_args in + let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in + let typ = Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) in + typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); + { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } + + | Typ_aux (Typ_bidir (typ1, typ2), l) -> + let env = add_mapping id (typq, typ1, typ2) env in + typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ))); + { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs } + + | _ -> typ_error (id_loc id) "val definition must have a mapping or function type" end + and add_val_spec id (bind_typq, bind_typ) env = if not (Bindings.mem id env.top_val_specs) then update_val_spec id (bind_typq, bind_typ) env @@ -776,6 +811,7 @@ end = struct typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound as " ^ string_of_bind (existing_typq, existing_typ) ^ ", cannot rebind as " ^ string_of_bind (bind_typq, bind_typ)) else env + and add_mapping id (typq, typ1, typ2) env = begin typ_print (lazy (adding ^ "mapping " ^ string_of_id id)); |