summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast_util.mli2
-rw-r--r--src/initial_check.ml6
-rw-r--r--src/lexer2.mll2
-rw-r--r--src/parser2.mly57
-rw-r--r--src/reporting_basic.ml59
-rw-r--r--src/type_check.ml80
-rw-r--r--src/type_check.mli4
7 files changed, 127 insertions, 83 deletions
diff --git a/src/ast_util.mli b/src/ast_util.mli
index e6823ee9..6164fc17 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,6 +44,8 @@
open Ast
+val no_annot : unit annot
+
val mk_id : string -> id
val mk_kid : string -> kid
val mk_ord : order_aux -> order
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4c0a0db4..1f7840d0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -1010,7 +1010,7 @@ let initial_kind_env =
]
let typschm_of_string order str =
- let typschm = Parser2.typschm Lexer2.token (Lexing.from_string str) in
+ let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in
let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
typschm
@@ -1057,14 +1057,14 @@ let generate_undefineds vs_ids (Defs defs) =
if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
in
let undefined_builtins = List.concat
- [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}";
+ [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
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_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_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_td = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index f5350ea8..a1717d62 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -235,8 +235,6 @@ rule token = parse
with Not_found -> raise (LexError ("Operator fixity undeclared", 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) ":" { TyDecl(r i) }
- | (startident ident* as i) ":" { Decl(r i) }
| tyvar_start startident ident* as i { TyVar(r i) }
| startident ident* as i { if M.mem i kw_table then
(M.find i kw_table) ()
diff --git a/src/parser2.mly b/src/parser2.mly
index 42e13721..02a8f09c 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -139,7 +139,7 @@ let rec desugar_rchain chain s e =
/*Terminals with content*/
-%token <string> Id TyVar Decl TyDecl
+%token <string> Id TyVar
%token <int> Num
%token <string> String Bin Hex Real
@@ -153,9 +153,8 @@ let rec desugar_rchain chain s e =
%token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
%start file
-%start typschm
-%type <Parse_ast.typschm> typschm
-%type <Parse_ast.defs> defs
+%start typschm_eof
+%type <Parse_ast.typschm> typschm_eof
%type <Parse_ast.defs> file
%%
@@ -233,10 +232,6 @@ op7r: Op7r { mk_id (Id $1) $startpos $endpos }
op8r: Op8r { mk_id (Id $1) $startpos $endpos }
op9r: Op9r { mk_id (Id $1) $startpos $endpos }
-decl:
- | Decl
- { mk_id (Id $1) $startpos $endpos }
-
id_list:
| id
{ [$1] }
@@ -247,10 +242,6 @@ kid:
| TyVar
{ mk_kid $1 $startpos $endpos }
-tydecl:
- | TyDecl
- { mk_kid $1 $startpos $endpos }
-
kid_list:
| kid
{ [$1] }
@@ -515,8 +506,6 @@ kind:
{ K_aux (K_kind [$1], loc $startpos $endpos) }
kopt:
- | tydecl kind
- { KOpt_aux (KOpt_kind ($2, $1), loc $startpos $endpos) }
| Lparen kid Colon kind Rparen
{ KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) }
| kid
@@ -589,6 +578,10 @@ typschm:
| Forall typquant Dot typ MinusGt typ Effect effect_set
{ (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
+typschm_eof:
+ | typschm Eof
+ { $1 }
+
pat:
| atomic_pat
{ $1 }
@@ -612,14 +605,10 @@ atomic_pat:
{ mk_pat (P_id $1) $startpos $endpos }
| kid
{ mk_pat (P_var $1) $startpos $endpos }
- | tydecl typ
- { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos }
| id Lparen pat_list Rparen
{ mk_pat (P_app ($1, $3)) $startpos $endpos }
| pat Colon typ
{ mk_pat (P_typ ($3, $1)) $startpos $endpos }
- | decl typ
- { mk_pat (P_typ ($2, mk_pat (P_id $1) $startpos $endpos($1))) $startpos $endpos }
| Lparen pat Rparen
{ $2 }
@@ -646,27 +635,21 @@ lit:
{ mk_lit (L_string $1) $startpos $endpos }
exp:
- | cast_exp Colon typ
- { mk_exp (E_cast ($3, $1)) $startpos $endpos }
- | cast_exp
- { $1 }
-
-cast_exp:
| exp0
{ $1 }
- | atomic_exp Eq cast_exp
+ | atomic_exp Eq exp
{ mk_exp (E_assign ($1, $3)) $startpos $endpos }
- | Let_ letbind In cast_exp
+ | Let_ letbind In exp
{ mk_exp (E_let ($2, $4)) $startpos $endpos }
| Lcurly block Rcurly
{ mk_exp (E_block $2) $startpos $endpos }
- | Return cast_exp
+ | Return exp
{ mk_exp (E_return $2) $startpos $endpos }
- | Throw cast_exp
+ | Throw exp
{ mk_exp (E_throw $2) $startpos $endpos }
- | If_ exp Then cast_exp Else cast_exp
+ | If_ exp Then exp Else exp
{ mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
- | If_ exp Then cast_exp
+ | If_ exp Then exp
{ mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos }
| Match exp Lcurly case_list Rcurly
{ mk_exp (E_case ($2, $4)) $startpos $endpos }
@@ -856,12 +839,14 @@ block:
{ LB_aux (LB_val_implicit ($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 }
- | decl atomic_typ
- { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos }
| id
{ mk_exp (E_id $1) $startpos $endpos }
+ | kid
+ { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
| id Unit
{ mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
| id Lparen exp_list Rparen
@@ -922,8 +907,6 @@ enum:
{ $1 :: $3 }
struct_field:
- | decl typ
- { ($2, $1) }
| id Colon typ
{ ($3, $1) }
@@ -936,8 +919,6 @@ struct_fields:
{ $1 :: $3 }
type_union:
- | decl typ
- { Tu_aux (Tu_ty_id ($2, $1), loc $startpos $endpos) }
| id Colon typ
{ Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
| id
@@ -960,14 +941,10 @@ let_def:
{ $2 }
val_spec_def:
- | Val decl typschm
- { mk_vs (VS_val_spec ($3, $2)) $startpos $endpos }
| Val id Colon typschm
{ mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
register_def:
- | Register decl typ
- { mk_reg_dec (DEC_reg ($3, $2)) $startpos $endpos }
| Register id Colon typ
{ mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 69c5c084..2bd5d5bc 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -87,19 +87,48 @@
(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
(**************************************************************************)
-let format_pos ff p = (
- Format.fprintf ff "File \"%s\", line %d, character %d:\n"
- p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol);
- Format.pp_print_flush ff ())
-
-
-let format_pos2 ff p1 p2 = (
- Format.fprintf ff "File \"%s\", line %d, character %d to line %d, character %d"
- p1.Lexing.pos_fname
- p1.Lexing.pos_lnum (p1.Lexing.pos_cnum - p1.Lexing.pos_bol + 1)
- p2.Lexing.pos_lnum (p2.Lexing.pos_cnum - p2.Lexing.pos_bol);
- Format.pp_print_flush ff ()
-)
+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)
+
+let termcode n = "\x1B[" ^ string_of_int n ^ "m"
+
+let print_code ff fname lnum1 cnum1 cnum2 =
+ try
+ let in_chan = open_in fname in
+ begin
+ try
+ skip_lines in_chan (lnum1 - 1);
+ let line = input_line in_chan in
+ Format.fprintf ff "%s%s%s%s%s"
+ (Str.string_before line cnum1)
+ (termcode 41)
+ (Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1))
+ (termcode 49)
+ (Str.string_after line cnum2);
+ close_in in_chan
+ with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e))
+ end
+ with _ -> ()
+
+let format_pos2 ff p1 p2 =
+ let open Lexing in
+ begin
+ Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n"
+ p1.pos_fname
+ p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
+ p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
+ print_code ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol);
+ Format.pp_print_flush ff ()
+ end
(* reads the part between p1 and p2 from the file *)
@@ -171,12 +200,12 @@ let loc_to_string l =
type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
let print_err_internal fatal verb_loc p_l m1 m2 =
+ Format.eprintf "%s at " m1;
let _ = (match p_l with Pos p -> print_err_pos p
| Loc l -> print_err_loc l
| LocD (l1,l2) ->
print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
- let m12 = if String.length m2 = 0 then "" else ": " in
- Format.eprintf " %s%s%s\n" m1 m12 m2;
+ Format.eprintf "%s\n" m2;
if verb_loc then (match p_l with Loc l ->
format_loc_source Format.err_formatter l;
Format.pp_print_newline Format.err_formatter (); | _ -> ());
diff --git a/src/type_check.ml b/src/type_check.ml
index 636d4049..f952d0d6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -65,9 +65,47 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ m) el
let typ_warning m = prerr_endline ("Warning: " ^ m)
-exception Type_error of l * string;;
+type type_error =
+ (* First parameter is the error that caused us to start doing type
+ coercions, the second is the errors encountered by all possible
+ coerctions *)
+ | Err_no_casts of type_error * type_error list
+ | Err_subtype of typ * typ * n_constraint list
+ | Err_other of string
+
+let pp_type_error err =
+ let open PPrint in
+ let rec pp_err = function
+ | Err_no_casts (trigger, []) ->
+ (string "Tried performing type coercion because" ^//^ pp_err trigger)
+ ^/^ string "No possible coercions"
+ | Err_no_casts (trigger, errs) ->
+ (string "Tried performing type coerction because" ^//^ pp_err trigger)
+ | Err_subtype (typ1, typ2, []) ->
+ separate space [ string (string_of_typ typ1);
+ string "is not a subtype of";
+ string (string_of_typ typ2) ]
+ | Err_subtype (typ1, typ2, constrs) ->
+ separate space [ string (string_of_typ typ1);
+ string "is not a subtype of";
+ string (string_of_typ typ2) ]
+ ^/^ string "in context"
+ ^//^ string (string_of_list ", " string_of_n_constraint constrs)
+ | Err_other str -> string str
+ in
+ pp_err err
+
+let rec string_of_type_error err =
+ let open PPrint in
+ let b = Buffer.create 20 in
+ ToBuffer.pretty 1. 120 b (pp_type_error err);
+ "\n" ^ Buffer.contents b
+
+exception Type_error of l * type_error;;
+
+let typ_error l m = raise (Type_error (l, Err_other m))
-let typ_error l m = raise (Type_error (l, m))
+let typ_raise l err = raise (Type_error (l, err))
let deinfix = function
| Id_aux (Id v, l) -> Id_aux (DeIid v, l)
@@ -1447,9 +1485,7 @@ let rec subtyp l env typ1 typ2 =
| _, None ->
if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2)
then ()
- else typ_error l (string_of_typ typ1
- ^ " is not a subtype of " ^ string_of_typ typ2
- ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
+ else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
let typ_equality l env typ1 typ2 =
subtyp l env typ1 typ2; subtyp l env typ2 typ1
@@ -1782,7 +1818,7 @@ let crule r env exp typ =
let checked_exp = r env exp typ in
decr depth; checked_exp
with
- | Type_error (l, m) -> decr depth; typ_error l m
+ | Type_error (l, err) -> decr depth; typ_raise l err
let irule r env exp =
incr depth;
@@ -1792,7 +1828,7 @@ let irule r env exp =
decr depth;
inferred_exp
with
- | Type_error (l, m) -> decr depth; typ_error l m
+ | Type_error (l, err) -> decr depth; typ_raise l err
let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
@@ -1928,7 +1964,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| (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 (_, m) -> typ_print ("Error : " ^ m); try_overload fs
+ | Type_error (_, err) -> typ_print ("Error : " ^ string_of_type_error err); try_overload fs
end
in
try_overload (Env.get_overloads f env)
@@ -1991,15 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
- let rec try_casts m = function
- | [] -> typ_error l ("No valid casts:\n" ^ m)
+ let rec try_casts trigger errs = function
+ | [] -> typ_raise l (Err_no_casts (trigger, errs))
| (cast :: casts) -> begin
typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
try
let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in
annot_exp (E_cast (typ, checked_cast)) typ
with
- | Type_error (_, m) -> try_casts m casts
+ | Type_error (_, err) -> try_casts trigger (err :: errs) casts
end
in
begin
@@ -2007,10 +2043,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ);
subtyp l env (typ_of annotated_exp) typ; annotated_exp
with
- | Type_error (_, m) when Env.allow_casts env ->
+ | Type_error (_, trigger) when Env.allow_casts env ->
let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
- try_casts "" casts
- | Type_error (l, m) -> typ_error l ("Subtype error " ^ m)
+ try_casts trigger [] casts
+ | Type_error (l, err) -> typ_error l "Subtype error"
end
(* type_coercion_unify env exp typ attempts to coerce exp to a type
@@ -2021,8 +2057,8 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
- let rec try_casts m = function
- | [] -> unify_error l ("No valid casts resulted in unification:\n" ^ m)
+ let rec try_casts = function
+ | [] -> unify_error l "No valid casts resulted in unification"
| (cast :: casts) -> begin
typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification");
try
@@ -2030,8 +2066,8 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
let ityp = typ_of inferred_cast in
annot_exp (E_cast (ityp, inferred_cast)) ityp, unify l env typ ityp
with
- | Type_error (_, m) -> try_casts m casts
- | Unification_error (_, m) -> try_casts m casts
+ | Type_error (_, err) -> try_casts casts
+ | Unification_error (_, err) -> try_casts casts
end
in
begin
@@ -2041,7 +2077,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
with
| Unification_error (_, m) when Env.allow_casts env ->
let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
- try_casts "" casts
+ try_casts casts
end
and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
@@ -2497,7 +2533,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
| (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 (_, m) -> typ_print ("Error: " ^ m); try_overload fs
+ | Type_error (_, err) -> typ_print ("Overload error"); try_overload fs
end
in
try_overload (Env.get_overloads f env)
@@ -3125,7 +3161,7 @@ let mk_synonym typq typ =
typ_subst_typ (kopt_kid kopt) (unaux_typ arg) typ, ncs
| kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt ->
let typ, ncs = subst_args kopts args in
- typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs
+ typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs
| [], [] -> typ, ncs
| _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
| _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments"
@@ -3193,4 +3229,4 @@ let rec check' env (Defs defs) =
let check env defs =
try check' env defs with
- | Type_error (l, m) -> raise (Reporting_basic.err_typ l m)
+ | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
diff --git a/src/type_check.mli b/src/type_check.mli
index fa75b156..ca2fb90c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -47,7 +47,9 @@ open Ast_util
val opt_tc_debug : int ref
val opt_no_effects : bool ref
-exception Type_error of l * string;;
+type type_error
+
+exception Type_error of l * type_error;;
type mut = Immutable | Mutable
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 12:31:18 +0000