Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Print terms that invented types when type_invention_error is set #88

Merged
merged 1 commit into from
Jan 13, 2024
Merged

Print terms that invented types when type_invention_error is set #88

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Help/type_invention_error.hlp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,8 @@ fails with an error message:
# type_invention_error := true;;
val it : unit = ()
# let tm = `x = x`;;
Exception: Failure "typechecking error (cannot infer type of variables)".
Exception:
Failure "typechecking error (cannot infer type of variables): =, x".
}
\noindent You can avoid the error by explicitly giving appropriate types or
type variables yourself:
Expand Down
55 changes: 36 additions & 19 deletions preterm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -393,41 +393,58 @@ let type_of_pretype,term_of_preterm,retypecheck =
in

(* ----------------------------------------------------------------------- *)
(* Flag to indicate that Stvs were translated to real type variables. *)
(* Pretype -> type conversion. The base function returns a flag if a *)
(* system type variable was translated to real type variable. *)
(* ----------------------------------------------------------------------- *)

let stvs_translated = ref false in
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

stvs_translated is removed in this patch. It is a local variable defined inside the outer function, so okay to be erased.


(* ----------------------------------------------------------------------- *)
(* Pretype <-> type conversion; -> flags system type variable translation. *)
(* ----------------------------------------------------------------------- *)

let rec type_of_pretype ty =
let rec type_of_pretype_base (ty:pretype): hol_type * bool =
match ty with
Stv n -> stvs_translated := true;
let s = "?"^(string_of_int n) in
mk_vartype(s)
| Utv(v) -> mk_vartype(v)
| Ptycon(con,args) -> mk_type(con,map type_of_pretype args) in
Stv n -> let s = "?"^(string_of_int n) in
(mk_vartype(s), true)
| Utv(v) -> (mk_vartype(v), false)
| Ptycon(con,args) ->
let args',translated = unzip (map type_of_pretype_base args) in
let translated = List.fold_left (||) false translated in
(mk_type(con,args'), translated) in

let type_of_pretype (ty:pretype): hol_type =
fst (type_of_pretype_base ty) in

(* ----------------------------------------------------------------------- *)
(* Maps preterms to terms. *)
(* ----------------------------------------------------------------------- *)

let term_of_preterm =
let rec term_of_preterm ptm =
let stvs_translated_terms:string list ref = ref [] in
let rec term_of_preterm (ptm:preterm): term =
match ptm with
Varp(s,pty) -> mk_var(s,type_of_pretype pty)
| Constp(s,pty) -> mk_mconst(s,type_of_pretype pty)
Varp(s,pty) ->
let ty, translated = type_of_pretype_base pty in
let v = mk_var(s,ty) in
let _ =
if translated && not (exists (fun s' -> s = s')
!stvs_translated_terms)
then stvs_translated_terms := s::!stvs_translated_terms
else () in v
| Constp(s,pty) ->
let ty, translated = type_of_pretype_base pty in
let c = mk_mconst(s,ty) in
let _ =
if translated && not (exists (fun s' -> s = s')
!stvs_translated_terms)
then stvs_translated_terms := s::!stvs_translated_terms
else () in c
| Combp(l,r) -> mk_comb(term_of_preterm l,term_of_preterm r)
| Absp(v,bod) -> mk_gabs(term_of_preterm v,term_of_preterm bod)
| Typing(ptm,pty) -> term_of_preterm ptm in
let report_type_invention () =
if !stvs_translated then
if !stvs_translated_terms <> [] then
if !type_invention_error
then failwith "typechecking error (cannot infer type of variables)"
then failwith
("typechecking error (cannot infer type of variables): " ^
String.concat ", " !stvs_translated_terms)
else warn !type_invention_warning "inventing type variables" in
fun ptm -> stvs_translated := false;
fun ptm -> stvs_translated_terms := [];
let tm = term_of_preterm ptm in
report_type_invention (); tm in

Expand Down
Loading