You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hi,
I just noticed that preprocess_with does not deal well with records. A record constructor { x = 0; y = 1} generates a term like __dummy__ 0 1. If we inspect then re-pack that application, then they don't seem to be re-packed correctly.
Test case:
module Test.VisitRecord
module Tac = FStar.Tactics
type record = { x: int; y: int; }
[@@Tac.preprocess_with (Tac.visit_tm (fun i -> i))]
let visit_record_nok (add: int): record =
{ x = 0; y = 1 }
The above preprocess tactic should just be an identity transform, but I get the error:
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Invalid_argument("List.combine: list lengths differ")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from FStar_TypeChecker_TcTerm.tc_maybe_toplevel_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 3180, characters 20-106
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
Called from FStar_TypeChecker_TcTerm.tc_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 1674, characters 9-1023
...
I'm not certain, but it seems to be specific to the preprocessing. I have a splice that takes apart record applications and recreates them fine.
I can also recreate the problem without visit:
let rec tac_rec_inspect (t: Tac.term): Tac.Tac Tac.term =
match Tac.inspect t with
| Tac.Tv_Abs bv tm ->
Tac.print "+ abs";
let tm = tac_rec_inspect tm in
Tac.print "- abs";
Tac.pack (Tac.Tv_Abs bv tm)
| Tac.Tv_App hd (arg, q) ->
Tac.print "+ app";
let hd = tac_rec_inspect hd in
let arg = tac_rec_inspect arg in
Tac.print "- app";
Tac.pack (Tac.Tv_App hd (arg, q))
| ti ->
Tac.print ("leaf: " ^ Tac.term_to_string (quote ti));
ti
[@@Tac.preprocess_with (fun t -> tac_rec_inspect t)]
let inspect_record_nok (add: int) =
{ x = 0; y = 1 }
(Low priority for me, just wanted to log it before I forgot)
The text was updated successfully, but these errors were encountered:
Hi,
I just noticed that
preprocess_with
does not deal well with records. A record constructor{ x = 0; y = 1}
generates a term like__dummy__ 0 1
. If we inspect then re-pack that application, then they don't seem to be re-packed correctly.Test case:
The above preprocess tactic should just be an identity transform, but I get the error:
I'm not certain, but it seems to be specific to the preprocessing. I have a splice that takes apart record applications and recreates them fine.
I can also recreate the problem without visit:
(Low priority for me, just wanted to log it before I forgot)
The text was updated successfully, but these errors were encountered: