From 2848ccd2693f486e153eef4d8731f6baff35060a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 27 Nov 2023 20:57:00 -0800 Subject: [PATCH 1/2] src/tactics: more use of typeclasses --- src/basic/FStar.Compiler.Range.Ops.fst | 4 + src/basic/FStar.Compiler.Range.Ops.fsti | 3 + src/basic/FStar.Ident.fst | 9 ++ src/basic/FStar.Ident.fsti | 5 + src/syntax/FStar.Syntax.Print.fst | 16 ++- src/syntax/FStar.Syntax.Print.fsti | 12 +- src/tactics/FStar.Tactics.CtrlRewrite.fst | 11 +- src/tactics/FStar.Tactics.Embedding.fst | 7 +- src/tactics/FStar.Tactics.Hooks.fst | 45 +++--- src/tactics/FStar.Tactics.Monad.fst | 15 +- src/tactics/FStar.Tactics.Printing.fst | 16 +-- src/tactics/FStar.Tactics.V1.Basic.fst | 129 +++++++++--------- src/tactics/FStar.Tactics.V1.InterpFuns.fst | 8 +- src/tactics/FStar.Tactics.V1.Interpreter.fst | 7 +- src/tactics/FStar.Tactics.V2.Basic.fst | 92 ++++++------- src/tactics/FStar.Tactics.V2.InterpFuns.fst | 8 +- src/tactics/FStar.Tactics.V2.Interpreter.fst | 45 +++--- src/typechecker/FStar.TypeChecker.Common.fst | 4 + src/typechecker/FStar.TypeChecker.Common.fsti | 11 +- 19 files changed, 244 insertions(+), 203 deletions(-) diff --git a/src/basic/FStar.Compiler.Range.Ops.fst b/src/basic/FStar.Compiler.Range.Ops.fst index 5edcd6bcb1e..b08a5ffe172 100644 --- a/src/basic/FStar.Compiler.Range.Ops.fst +++ b/src/basic/FStar.Compiler.Range.Ops.fst @@ -120,3 +120,7 @@ let json_of_def_range r = (file_of_range r) (start_of_range r) (end_of_range r) + +instance show_range = { + show = string_of_range; +} diff --git a/src/basic/FStar.Compiler.Range.Ops.fsti b/src/basic/FStar.Compiler.Range.Ops.fsti index 019bb12f36e..84f6500ddde 100644 --- a/src/basic/FStar.Compiler.Range.Ops.fsti +++ b/src/basic/FStar.Compiler.Range.Ops.fsti @@ -17,6 +17,7 @@ module FStar.Compiler.Range.Ops open FStar.Compiler.Range.Type open FStar.Compiler.Effect +open FStar.Class.Show val union_rng: rng -> rng -> rng val union_ranges: range -> range -> range @@ -45,3 +46,5 @@ val extend_to_end_of_line: range -> range val json_of_pos : pos -> Json.json val json_of_use_range : range -> Json.json val json_of_def_range : range -> Json.json + +instance val show_range : showable range diff --git a/src/basic/FStar.Ident.fst b/src/basic/FStar.Ident.fst index 89eb1edead5..c2a785cc131 100644 --- a/src/basic/FStar.Ident.fst +++ b/src/basic/FStar.Ident.fst @@ -73,3 +73,12 @@ let qual_id lid id = set_lid_range (lid_of_ids (lid.ns @ [lid.ident;id])) (range_of_id id) let nsstr (l:lid) : string = l.nsstr + +(* Showable instances *) +instance showable_ident = { + show = string_of_id; +} + +instance showable_lident = { + show = string_of_lid; +} diff --git a/src/basic/FStar.Ident.fsti b/src/basic/FStar.Ident.fsti index 3d43429dadb..ab256cd8ec2 100644 --- a/src/basic/FStar.Ident.fsti +++ b/src/basic/FStar.Ident.fsti @@ -16,6 +16,7 @@ module FStar.Ident open FStar.Compiler.Range +open FStar.Class.Show (** A (short) identifier for a local name. * e.g. x in `fun x -> ...` *) @@ -130,3 +131,7 @@ val text_of_path : path -> string (* Similar to string_of_lid, but separates with "_" instead of "." *) val ml_path_of_lid : lident -> string + +(* Showable instances *) +instance val showable_ident : showable ident +instance val showable_lident : showable lident diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index 74535a2939f..8d44e1eabec 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -987,9 +987,13 @@ let sigelt_to_doc t = then Pprint.arbitrary_string (sigelt_to_string t) else Pretty.sigelt_to_doc t -instance pretty_sigelt = { pp = sigelt_to_doc; } -instance pretty_comp = { pp = comp_to_doc; } -instance pretty_term = { pp = term_to_doc; } - -instance showable_sigelt : showable sigelt = { show = sigelt_to_string; } -instance showable_term : showable term = { show = term_to_string; } +instance pretty_sigelt = { pp = sigelt_to_doc; } +instance pretty_comp = { pp = comp_to_doc; } +instance pretty_term = { pp = term_to_doc; } + +instance showable_sigelt = { show = sigelt_to_string; } +instance showable_term = { show = term_to_string; } +instance showable_bv = { show = bv_to_string; } +instance showable_binder = { show = binder_to_string; } +instance showable_uvar = { show = uvar_to_string; } +instance showable_ctxu = { show = ctx_uvar_to_string; } diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti index c4312543057..577a69ef414 100644 --- a/src/syntax/FStar.Syntax.Print.fsti +++ b/src/syntax/FStar.Syntax.Print.fsti @@ -92,9 +92,13 @@ val term_to_doc : term -> Pprint.document val comp_to_doc : comp -> Pprint.document val sigelt_to_doc : sigelt -> Pprint.document -instance val pretty_term : pretty term -instance val pretty_comp : pretty comp -instance val pretty_sigelt : pretty sigelt +instance val pretty_term : pretty term +instance val pretty_comp : pretty comp +instance val pretty_sigelt : pretty sigelt -instance val showable_term : showable term +instance val showable_term : showable term instance val showable_sigelt : showable sigelt +instance val showable_bv : showable bv +instance val showable_binder : showable binder +instance val showable_uvar : showable uvar +instance val showable_ctxu : showable ctx_uvar diff --git a/src/tactics/FStar.Tactics.CtrlRewrite.fst b/src/tactics/FStar.Tactics.CtrlRewrite.fst index f98b583c689..25ec8a11ee2 100644 --- a/src/tactics/FStar.Tactics.CtrlRewrite.fst +++ b/src/tactics/FStar.Tactics.CtrlRewrite.fst @@ -30,6 +30,7 @@ open FStar.Tactics.Types open FStar.Tactics.Monad open FStar.Tactics.Common open FStar.Syntax.Syntax +open FStar.Class.Show module Print = FStar.Syntax.Print module BU = FStar.Compiler.Util @@ -117,7 +118,7 @@ let __do_rewrite in if_verbose (fun () -> BU.print2 "do_rewrite: making equality\n\t%s ==\n\t%s\n" - (Print.term_to_string tm) (Print.term_to_string ut)) ;! + (show tm) (show ut)) ;! add_irrelevant_goal g0 "do_rewrite.eq" @@ -130,8 +131,8 @@ let __do_rewrite let ut = N.reduce_uvar_solutions env ut in if_verbose (fun () -> BU.print2 "rewrite_rec: succeeded rewriting\n\t%s to\n\t%s\n" - (Print.term_to_string tm) - (Print.term_to_string ut)) ;! + (show tm) + (show ut)) ;! ret ut end @@ -427,12 +428,12 @@ let ctrl_rewrite dismiss_all ;! let gt = (goal_type g) in if_verbose (fun () -> - BU.print1 "ctrl_rewrite starting with %s\n" (Print.term_to_string gt)) ;! + BU.print1 "ctrl_rewrite starting with %s\n" (show gt)) ;! let! gt' = do_ctrl_rewrite g dir controller rewriter (goal_env g) gt in if_verbose (fun () -> - BU.print1 "ctrl_rewrite seems to have succeded with %s\n" (Print.term_to_string gt')) ;! + BU.print1 "ctrl_rewrite seems to have succeded with %s\n" (show gt')) ;! push_goals gs ;! let g = V2.Basic.goal_with_type g gt' in diff --git a/src/tactics/FStar.Tactics.Embedding.fst b/src/tactics/FStar.Tactics.Embedding.fst index d954c8ee3c0..01e7d97566b 100644 --- a/src/tactics/FStar.Tactics.Embedding.fst +++ b/src/tactics/FStar.Tactics.Embedding.fst @@ -24,6 +24,7 @@ open FStar.Syntax.Syntax open FStar.Syntax.Embeddings open FStar.Compiler.Util open FStar.Compiler.List +open FStar.Class.Show open FStar.Tactics.Common open FStar.Tactics.Types @@ -152,7 +153,7 @@ let unfold_lazy_goal (i : lazyinfo) : term = (* On that note, we use this (inefficient, FIXME) hack in this module *) let mkFV fv us ts = NBETerm.mkFV fv (List.rev us) (List.rev ts) let mkConstruct fv us ts = NBETerm.mkConstruct fv (List.rev us) (List.rev ts) -let fv_as_emb_typ fv = S.ET_app (FStar.Ident.string_of_lid fv.fv_name.v, []) +let fv_as_emb_typ fv = S.ET_app (show fv.fv_name.v, []) let e_proofstate_nbe = let embed_proofstate _cb (ps:proofstate) : NBETerm.t = @@ -235,7 +236,7 @@ let e_exn : embedding exn = unembed_exn t_exn (fun _ -> "(exn)") - (ET_app (PC.exn_lid |> Ident.string_of_lid, [])) + (ET_app (show PC.exn_lid, [])) let e_exn_nbe = let embed_exn cb (e:exn) : NBET.t = @@ -298,7 +299,7 @@ let e_result (ea : embedding 'a) = unembed_result (t_result_of (type_of ea)) (fun _ -> "") - (ET_app (fstar_tactics_result.lid |> Ident.string_of_lid, [emb_typ_of ea])) + (ET_app (show fstar_tactics_result.lid, [emb_typ_of ea])) let e_result_nbe (ea : NBET.embedding 'a) = let embed_result cb (res:__result 'a) : NBET.t = diff --git a/src/tactics/FStar.Tactics.Hooks.fst b/src/tactics/FStar.Tactics.Hooks.fst index f247787da69..7aeeb112ca2 100644 --- a/src/tactics/FStar.Tactics.Hooks.fst +++ b/src/tactics/FStar.Tactics.Hooks.fst @@ -29,6 +29,7 @@ open FStar.TypeChecker.Common open FStar.Tactics.Types open FStar.Tactics.V1.Interpreter open FStar.Tactics.V2.Interpreter +open FStar.Class.Show module BU = FStar.Compiler.Util module Range = FStar.Compiler.Range @@ -301,7 +302,7 @@ let preprocess (env:Env.env) (goal:term) : list (Env.env * term * O.optionstate) if !tacdbg then BU.print2 "About to preprocess %s |= %s\n" (Env.all_binders env |> Print.binders_to_string ",") - (Print.term_to_string goal); + (show goal); let initial = (1, []) in // This match should never fail let (t', gs) = @@ -313,19 +314,19 @@ let preprocess (env:Env.env) (goal:term) : list (Env.env * term * O.optionstate) if !tacdbg then BU.print2 "Main goal simplified to: %s |- %s\n" (Env.all_binders env |> Print.binders_to_string ", ") - (Print.term_to_string t'); + (show t'); let s = initial in let s = List.fold_left (fun (n,gs) g -> let phi = match getprop (goal_env g) (goal_type g) with | None -> Err.raise_error (Err.Fatal_TacticProofRelevantGoal, - (BU.format1 "Tactic returned proof-relevant goal: %s" (Print.term_to_string (goal_type g)))) env.range + (BU.format1 "Tactic returned proof-relevant goal: %s" (show (goal_type g)))) env.range | Some phi -> phi in if !tacdbg then - BU.print2 "Got goal #%s: %s\n" (string_of_int n) (Print.term_to_string (goal_type g)); + BU.print2 "Got goal #%s: %s\n" (show n) (show (goal_type g)); let label = - "Could not prove goal #" ^ string_of_int n ^ + "Could not prove goal #" ^ show n ^ (if get_label g = "" then "" else " (" ^ get_label g ^ ")") in let gt' = TcUtil.label label (goal_range g) phi in @@ -403,7 +404,7 @@ let rec traverse_for_spinoff let spinoff t = match pol with | StrictlyPositive -> - if debug then BU.print1 "Spinning off %s\n" (Print.term_to_string t); + if debug then BU.print1 "Spinning off %s\n" (show t); Simplified (FStar.Syntax.Util.t_true, [label_goal (e,t)]) | _ -> @@ -490,15 +491,15 @@ let rec traverse_for_spinoff if debug_any then FStar.Errors.diag (Env.get_range env) - (BU.format2 "Failed to split match term because %s (%s)" msg (Print.term_to_string t)); + (BU.format2 "Failed to split match term because %s (%s)" msg (show t)); None | Inr res -> if debug_any then FStar.Errors.diag (Env.get_range env) (BU.format2 "Rewrote match term\n%s\ninto %s\n" - (Print.term_to_string t) - (Print.term_to_string res)); + (show t) + (show res)); Some res) | _ -> None @@ -623,7 +624,7 @@ let pol_to_string = function let spinoff_strictly_positive_goals (env:Env.env) (goal:term) : list (Env.env * term) = let debug = Env.debug env (O.Other "SpinoffAll") in - if debug then BU.print1 "spinoff_all called with %s\n" (Print.term_to_string goal); + if debug then BU.print1 "spinoff_all called with %s\n" (show goal); Errors.with_ctx "While spinning off all goals" (fun () -> let initial = (1, []) in // This match should never fail @@ -645,7 +646,7 @@ let spinoff_strictly_positive_goals (env:Env.env) (goal:term) then ( let msg = BU.format2 "Main goal simplified to: %s |- %s\n" (Env.all_binders env |> Print.binders_to_string ", ") - (Print.term_to_string t) in + (show t) in FStar.Errors.diag (Env.get_range env) (BU.format1 @@ -676,12 +677,12 @@ let spinoff_strictly_positive_goals (env:Env.env) (goal:term) | Trivial -> None | NonTrivial t -> if debug - then BU.print1 "Got goal: %s\n" (Print.term_to_string t); + then BU.print1 "Got goal: %s\n" (show t); Some (env, t)) in FStar.Errors.diag (Env.get_range env) - (BU.format1 "Split query into %s sub-goals" (BU.string_of_int (List.length gs))); + (BU.format1 "Split query into %s sub-goals" (show (List.length gs))); main_goal@gs ) @@ -704,7 +705,7 @@ let synthesize (env:Env.env) (typ:typ) (tau:term) : term = | Some vc -> begin if !tacdbg then - BU.print1 "Synthesis left a goal: %s\n" (Print.term_to_string vc); + BU.print1 "Synthesis left a goal: %s\n" (show vc); let guard = { guard_f = NonTrivial vc ; deferred_to_tac = [] ; deferred = [] @@ -729,7 +730,7 @@ let solve_implicits (env:Env.env) (tau:term) (imps:Env.implicits) : unit = // TODO: It would be nicer to combine all of these into a guard and return // that to TcTerm, but the varying environments make it awkward. if Options.profile_enabled None "FStar.TypeChecker" - then BU.print1 "solve_implicits produced %s goals\n" (BU.string_of_int (List.length gs)); + then BU.print1 "solve_implicits produced %s goals\n" (show (List.length gs)); Options.with_saved_options (fun () -> let _ = Options.set_options "--no_tactics" in @@ -739,7 +740,7 @@ let solve_implicits (env:Env.env) (tau:term) (imps:Env.implicits) : unit = | Some vc -> begin if !tacdbg then - BU.print1 "Synthesis left a goal: %s\n" (Print.term_to_string vc); + BU.print1 "Synthesis left a goal: %s\n" (show vc); if not (Options.admit_smt_queries()) then ( let guard = { guard_f = NonTrivial vc @@ -803,7 +804,7 @@ let handle_smt_goal env goal = match getprop (goal_env g) (goal_type g) with | Some vc -> if !tacdbg then - BU.print1 "handle_smt_goals left a goal: %s\n" (Print.term_to_string vc); + BU.print1 "handle_smt_goals left a goal: %s\n" (show vc); (goal_env g), vc | None -> Err.raise_error (Err.Fatal_OpenGoalsInSynthesis, "Handling an SMT goal by tactic left non-prop open goals") @@ -882,7 +883,7 @@ let splice (env:Env.env) (is_typed:bool) (lids:list Ident.lident) (tau:term) (rn | Some vc -> begin if !tacdbg then - BU.print1 "Splice left a goal: %s\n" (Print.term_to_string vc); + BU.print1 "Splice left a goal: %s\n" (show vc); let guard = { guard_f = NonTrivial vc ; deferred_to_tac = [] ; deferred = [] @@ -902,14 +903,12 @@ let splice (env:Env.env) (is_typed:bool) (lids:list Ident.lident) (tau:term) (rn Err.raise_error (Errors.Fatal_SplicedUndef, BU.format2 "Splice declared the name %s but it was not defined.\nThose defined were: %s" - (Ident.string_of_lid lid) - (String.concat ", " <| List.map Ident.string_of_lid lids')) rng + (show lid) (show lids')) rng | _ -> () ) lids; if !tacdbg then - BU.print1 "splice: got decls = {\n\n%s\n\n}\n" - (FStar.Common.string_of_list Print.sigelt_to_string sigelts); + BU.print1 "splice: got decls = {\n\n%s\n\n}\n" (show sigelts); (* Check for bare Sig_datacon and Sig_inductive_typ, and abort if so. Also set range. *) let sigelts = sigelts |> List.map (fun se -> @@ -971,7 +970,7 @@ let postprocess (env:Env.env) (tau:term) (typ:term) (tm:term) : term = | Some vc -> begin if !tacdbg then - BU.print1 "Postprocessing left a goal: %s\n" (Print.term_to_string vc); + BU.print1 "Postprocessing left a goal: %s\n" (show vc); let guard = { guard_f = NonTrivial vc ; deferred_to_tac = [] ; deferred = [] diff --git a/src/tactics/FStar.Tactics.Monad.fst b/src/tactics/FStar.Tactics.Monad.fst index 68ff98b353d..273f06767ce 100644 --- a/src/tactics/FStar.Tactics.Monad.fst +++ b/src/tactics/FStar.Tactics.Monad.fst @@ -28,6 +28,7 @@ open FStar.Tactics.Types open FStar.Tactics.Result open FStar.Tactics.Printing open FStar.Tactics.Common +open FStar.Class.Show module O = FStar.Options module BU = FStar.Compiler.Util @@ -66,14 +67,14 @@ let register_goal (g:goal) = if Allow_untyped? (U.ctx_uvar_should_check g.goal_ctx_uvar) then () else let env = {env with gamma = uv.ctx_uvar_gamma } in if Env.debug env <| Options.Other "CoreEq" - then BU.print1 "(%s) Registering goal\n" (BU.string_of_int i); + then BU.print1 "(%s) Registering goal\n" (show i); let should_register = is_goal_safe_as_well_typed g in if not should_register then ( if Env.debug env <| Options.Other "Core" || Env.debug env <| Options.Other "RegisterGoal" then BU.print1 "(%s) Not registering goal since it has unresolved uvar deps\n" - (BU.string_of_int i); + (show i); () ) @@ -81,8 +82,8 @@ let register_goal (g:goal) = if Env.debug env <| Options.Other "Core" || Env.debug env <| Options.Other "RegisterGoal" then BU.print2 "(%s) Registering goal for %s\n" - (BU.string_of_int i) - (Print.ctx_uvar_to_string uv); + (show i) + (show uv); let goal_ty = U.ctx_uvar_typ uv in match FStar.TypeChecker.Core.compute_term_type_handle_guards env goal_ty (fun _ _ -> true) with @@ -90,7 +91,7 @@ let register_goal (g:goal) = | Inr err -> let msg = BU.format2 "Failed to check initial tactic goal %s because %s" - (Print.term_to_string (U.ctx_uvar_typ uv)) + (show (U.ctx_uvar_typ uv)) (FStar.TypeChecker.Core.print_error_short err) in Errors.log_issue uv.ctx_uvar_range @@ -217,7 +218,7 @@ let check_valid_goal g = | None -> () | Some (bv, e) -> if not (Env.closed e bv.sort) then - raise (Bad ("bv: " ^ Print.bv_to_string bv)); + raise (Bad ("bv: " ^ show bv)); aux e in aux env @@ -263,7 +264,7 @@ let cur_goal : tac goal = | Some t -> BU.print2 "!!!!!!!!!!!! GOAL IS ALREADY SOLVED! %s\nsol is %s\n" (goal_to_string_verbose hd) - (Print.term_to_string t); + (show t); ret hd) let remove_solved_goals : tac unit = diff --git a/src/tactics/FStar.Tactics.Printing.fst b/src/tactics/FStar.Tactics.Printing.fst index ebdf2cad2cc..92790499d68 100644 --- a/src/tactics/FStar.Tactics.Printing.fst +++ b/src/tactics/FStar.Tactics.Printing.fst @@ -25,6 +25,7 @@ open FStar.Syntax.Syntax open FStar.TypeChecker.Common open FStar.TypeChecker.Env open FStar.Tactics.Types +open FStar.Class.Show module BU = FStar.Compiler.Util module Range = FStar.Compiler.Range @@ -42,18 +43,17 @@ let term_to_string (e:Env.env) (t:term) : string = let goal_to_string_verbose (g:goal) : string = BU.format2 "%s%s\n" - (Print.ctx_uvar_to_string g.goal_ctx_uvar) + (show g.goal_ctx_uvar) (match check_goal_solved' g with | None -> "" | Some t -> BU.format1 "\tGOAL ALREADY SOLVED!: %s" (term_to_string (goal_env g) t)) let unshadow (bs : binders) (t : term) : binders * term = (* string name of a bv *) - let s b = (string_of_id b.ppname) in let sset bv s = S.gen_bv s (Some (range_of_id bv.ppname)) bv.sort in let fresh_until b f = let rec aux i = - let t = b ^ "'" ^ string_of_int i in + let t = b ^ "'" ^ show i in if f t then t else aux (i+1) in if f b then b else aux 0 @@ -67,7 +67,7 @@ let unshadow (bs : binders) (t : term) : binders * term = | _ -> failwith "impossible: unshadow subst_binders" in let (bv0, q) = b.binder_bv, b.binder_qual in - let nbs = fresh_until (s bv0) (fun s -> not (List.mem s seen)) in + let nbs = fresh_until (show bv0.ppname) (fun s -> not (List.mem s seen)) in let bv = sset bv0 nbs in let b = S.mk_binder_with_attrs bv q b.binder_positivity b.binder_attrs in go (nbs::seen) (subst @ [NT (bv0, S.bv_to_name bv)]) bs (b :: bs') t @@ -85,7 +85,7 @@ let goal_to_string (kind : string) (maybe_num : option (int * int)) (ps:proofsta in let num = match maybe_num with | None -> "" - | Some (i, n) -> BU.format2 " %s/%s" (string_of_int i) (string_of_int n) + | Some (i, n) -> BU.format2 " %s/%s" (show i) (show n) in let maybe_label = match g.label with @@ -127,14 +127,12 @@ let goal_to_string (kind : string) (maybe_num : option (int * int)) (ps:proofsta (* Note: we use def ranges. In tactics we keep the position in there, while the * use range is the original position of the assertion / synth / splice. *) let ps_to_string (msg, ps) = - let p_imp imp = - Print.uvar_to_string imp.imp_uvar.ctx_uvar_head - in + let p_imp imp = show imp.imp_uvar.ctx_uvar_head in let n_active = List.length ps.goals in let n_smt = List.length ps.smt_goals in let n = n_active + n_smt in String.concat "" - ([BU.format2 "State dump @ depth %s (%s):\n" (string_of_int ps.depth) msg; + ([BU.format2 "State dump @ depth %s (%s):\n" (show ps.depth) msg; (if ps.entry_range <> Range.dummyRange then BU.format1 "Location: %s\n" (Range.string_of_def_range ps.entry_range) else ""); diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst index e26ad555559..a54b5bc802c 100644 --- a/src/tactics/FStar.Tactics.V1.Basic.fst +++ b/src/tactics/FStar.Tactics.V1.Basic.fst @@ -32,6 +32,7 @@ open FStar.Tactics.Monad open FStar.Tactics.Printing open FStar.Syntax.Syntax open FStar.VConfig +open FStar.Class.Show friend FStar.Pervasives (* to use Delta below *) @@ -84,10 +85,10 @@ let core_check env sol t must_tot | Inr err -> debug (fun _ -> BU.print5 "(%s) Core checking failed (%s) on term %s and type %s\n%s\n" - (Range.string_of_range (Env.get_range env)) + (show (Env.get_range env)) (Core.print_error_short err) - (Print.term_to_string sol) - (Print.term_to_string t) + (show sol) + (show t) (Core.print_error err)); Inr err @@ -268,12 +269,12 @@ let proc_guard' (simplify:bool) (reason:string) (e : env) (g : guard_t) (sc_opt: push_goals [g]) | SMT -> - mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (show f)) (fun () -> let! g = goal_of_guard reason e f sc_opt rng in push_smt_goals [g]) | SMTSync -> - mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (show f)) (fun () -> Rel.force_trivial_guard e g; ret ()) @@ -325,9 +326,9 @@ let tc_unifier_solved_implicits env (must_tot:bool) (allow_guards:bool) (uvs:lis && NonTrivial? guard.guard_f then ( fail3 "Could not typecheck unifier solved implicit %s to %s since it produced a guard and guards were not allowed;guard is\n%s" - (Print.uvar_to_string u.ctx_uvar_head) - (Print.term_to_string sol) - (Print.term_to_string g) + (show u.ctx_uvar_head) + (show sol) + (show g) ) else ( proc_guard' false "guard for implicit" env guard (Some sc) u.ctx_uvar_range ;! @@ -337,8 +338,8 @@ let tc_unifier_solved_implicits env (must_tot:bool) (allow_guards:bool) (uvs:lis | Inr failed -> fail3 "Could not typecheck unifier solved implicit %s to %s because %s" - (Print.uvar_to_string u.ctx_uvar_head) - (Print.term_to_string sol) + (show u.ctx_uvar_head) + (show sol) (Core.print_error failed) in if env.phase1 //phase1 is untrusted @@ -366,8 +367,8 @@ let __do_unify_wflags (env:env) (t1:term) (t2:term) : tac (option guard_t) = if dbg then - BU.print2 "%%%%%%%%do_unify %s =? %s\n" (Print.term_to_string t1) - (Print.term_to_string t2); + BU.print2 "%%%%%%%%do_unify %s =? %s\n" (show t1) + (show t2); let all_uvars = (match check_side with @@ -389,8 +390,8 @@ let __do_unify_wflags if dbg then BU.print3 "%%%%%%%%do_unify (RESULT %s) %s =? %s\n" (FStar.Common.string_of_option (Rel.guard_to_string env) res) - (Print.term_to_string t1) - (Print.term_to_string t2); + (show t1) + (show t2); match res with | None -> @@ -406,7 +407,7 @@ let __do_unify_wflags end | Errors.Error (_, msg, r, _) -> begin mlog (fun () -> BU.print2 ">> do_unify error, (%s) at (%s)\n" - (Errors.rendermsg msg) (Range.string_of_range r)) (fun _ -> + (Errors.rendermsg msg) (show r)) (fun _ -> ret None) end ) @@ -523,8 +524,8 @@ let trysolve (goal : goal) (solution : term) : tac bool = let solve (goal : goal) (solution : term) : tac unit = let e = goal_env goal in - mlog (fun () -> BU.print2 "solve %s := %s\n" (Print.term_to_string (goal_witness goal)) - (Print.term_to_string solution)) (fun () -> + mlog (fun () -> BU.print2 "solve %s := %s\n" (show (goal_witness goal)) + (show solution)) (fun () -> bind (trysolve goal solution) (fun b -> if b then bind dismiss (fun () -> remove_solved_goals) @@ -589,7 +590,7 @@ let curms () : tac Z.t = (* Annoying duplication here *) let __tc (e : env) (t : term) : tac (term * typ * guard_t) = bind get (fun ps -> - mlog (fun () -> BU.print1 "Tac> __tc(%s)\n" (Print.term_to_string t)) (fun () -> + mlog (fun () -> BU.print1 "Tac> __tc(%s)\n" (show t)) (fun () -> let e = {e with uvar_subtyping=false} in try ret (TcTerm.typeof_tot_or_gtot_term e t true) with | Errors.Err (_, msg, _) @@ -601,7 +602,7 @@ let __tc (e : env) (t : term) : tac (term * typ * guard_t) = let __tc_ghost (e : env) (t : term) : tac (term * typ * guard_t) = bind get (fun ps -> - mlog (fun () -> BU.print1 "Tac> __tc_ghost(%s)\n" (Print.term_to_string t)) (fun () -> + mlog (fun () -> BU.print1 "Tac> __tc_ghost(%s)\n" (show t)) (fun () -> let e = {e with uvar_subtyping=false} in let e = {e with letrecs=[]} in try let t, lc, g = TcTerm.tc_tot_or_gtot_term e t in @@ -616,7 +617,7 @@ let __tc_ghost (e : env) (t : term) : tac (term * typ * guard_t) = let __tc_lax (e : env) (t : term) : tac (term * lcomp * guard_t) = bind get (fun ps -> mlog (fun () -> BU.print2 "Tac> __tc_lax(%s)(Context:%s)\n" - (Print.term_to_string t) + (show t) (Env.all_binders e |> Print.binders_to_string ", ")) (fun () -> let e = {e with uvar_subtyping=false} in let e = {e with lax = true} in @@ -715,11 +716,11 @@ let intro () : tac binder = wrap_err "intro" <| ( then fail "Codomain is effectful" else let typ' = U.comp_result c in //BU.print1 "[intro]: current goal is %s" (goal_to_string goal); - //BU.print1 "[intro]: current goal witness is %s" (Print.term_to_string (goal_witness goal)); - //BU.print1 "[intro]: with goal type %s" (Print.term_to_string (goal_type goal)); + //BU.print1 "[intro]: current goal witness is %s" (show (goal_witness goal)); + //BU.print1 "[intro]: with goal type %s" (show (goal_type goal)); //BU.print2 "[intro]: with binder = %s, new goal = %s" // (Print.binders_to_string ", " [b]) - // (Print.term_to_string typ'); + // (show typ'); let! body, ctx_uvar = new_uvar "intro" env' typ' (Some (should_check_goal_uvar goal)) @@ -727,10 +728,10 @@ let intro () : tac binder = wrap_err "intro" <| ( (rangeof goal) in let sol = U.abs [b] body (Some (U.residual_comp_of_comp c)) in //BU.print1 "[intro]: solution is %s" - // (Print.term_to_string sol); + // (show sol); //BU.print1 "[intro]: old goal is %s" (goal_to_string goal); //BU.print1 "[intro]: new goal is %s" - // (Print.ctx_uvar_to_string ctx_uvar); + // (show ctx_uvar); //ignore (FStar.Options.set_options "--debug_level Rel"); (* Suppose if instead of simply assigning `?u` to the lambda term on the RHS, we tried to unify `?u` with the `(fun (x:t) -> ?v @ [NM(x, 0)])`. @@ -786,7 +787,7 @@ let intro_rec () : tac (binder * binder) = let norm (s : list Pervasives.norm_step) : tac unit = let! goal = cur_goal in - if_verbose (fun () -> BU.print1 "norm: witness = %s\n" (Print.term_to_string (goal_witness goal))) ;! + if_verbose (fun () -> BU.print1 "norm: witness = %s\n" (show (goal_witness goal))) ;! // Translate to actual normalizer steps let steps = [Env.Reify; Env.UnfoldTac]@(Cfg.translate_norm_steps s) in //let w = normalize steps (goal_env goal) (goal_witness goal) in @@ -796,12 +797,12 @@ let norm (s : list Pervasives.norm_step) : tac unit = let norm_term_env (e : env) (s : list Pervasives.norm_step) (t : term) : tac term = wrap_err "norm_term" <| ( let! ps = get in - if_verbose (fun () -> BU.print1 "norm_term_env: t = %s\n" (Print.term_to_string t)) ;! + if_verbose (fun () -> BU.print1 "norm_term_env: t = %s\n" (show t)) ;! // only for elaborating lifts and all that, we don't care if it's actually well-typed let! t, _, _ = __tc_lax e t in let steps = [Env.Reify; Env.UnfoldTac]@(Cfg.translate_norm_steps s) in let t = normalize steps ps.main_context t in - if_verbose (fun () -> BU.print1 "norm_term_env: t' = %s\n" (Print.term_to_string t)) ;! + if_verbose (fun () -> BU.print1 "norm_term_env: t' = %s\n" (show t)) ;! ret t ) @@ -836,11 +837,11 @@ let __exact_now set_expected_typ (t:term) : tac unit = in let! t, typ, guard = __tc env t in if_verbose (fun () -> BU.print2 "__exact_now: got type %s\n__exact_now: and guard %s\n" - (Print.term_to_string typ) + (show typ) (Rel.guard_to_string (goal_env goal) guard)) ;! proc_guard "__exact typing" (goal_env goal) guard (Some (should_check_goal_uvar goal)) (rangeof goal) ;! - if_verbose (fun () -> BU.print2 "__exact_now: unifying %s and %s\n" (Print.term_to_string typ) - (Print.term_to_string (goal_type goal))) ;! + if_verbose (fun () -> BU.print2 "__exact_now: unifying %s and %s\n" (show typ) + (show (goal_type goal))) ;! let! b = do_unify true (goal_env goal) typ (goal_type goal) in if b then ( // do unify succeeded with a trivial guard; so the goal is solved and we don't have to check it again @@ -856,7 +857,7 @@ let __exact_now set_expected_typ (t:term) : tac unit = (tts (goal_env goal) (goal_witness goal)) let t_exact try_refine set_expected_typ tm : tac unit = wrap_err "exact" <| ( - if_verbose (fun () -> BU.print1 "t_exact: tm = %s\n" (Print.term_to_string tm)) ;! + if_verbose (fun () -> BU.print1 "t_exact: tm = %s\n" (show tm)) ;! match! catch (__exact_now set_expected_typ tm) with | Inr r -> ret r | Inl e when not (try_refine) -> traise e @@ -896,7 +897,7 @@ let try_unify_by_application (should_check:option should_check_uvar) | Some (b, c) -> if not (U.is_total_comp c) then fail "Codomain is effectful" else let! uvt, uv = new_uvar "apply arg" e b.binder_bv.sort should_check typedness_deps rng in - if_verbose (fun () -> BU.print1 "t_apply: generated uvar %s\n" (Print.ctx_uvar_to_string uv)) ;! + if_verbose (fun () -> BU.print1 "t_apply: generated uvar %s\n" (show uv)) ;! let typ = U.comp_result c in let typ' = SS.subst [S.NT (b.binder_bv, uvt)] typ in aux ((uvt, U.aqual_of_binder b, uv)::acc) (uv::typedness_deps) typ' @@ -949,10 +950,10 @@ let t_apply (uopt:bool) (only_match:bool) (tc_resolved_uvars:bool) (tm:term) : t let tc_resolved_uvars = true in if_verbose (fun () -> BU.print4 "t_apply: uopt %s, only_match %s, tc_resolved_uvars %s, tm = %s\n" - (string_of_bool uopt) - (string_of_bool only_match) - (string_of_bool tc_resolved_uvars) - (Print.term_to_string tm)) ;! + (show uopt) + (show only_match) + (show tc_resolved_uvars) + (show tm)) ;! let! ps = get in let! goal = cur_goal in let e = goal_env goal in @@ -961,17 +962,17 @@ let t_apply (uopt:bool) (only_match:bool) (tc_resolved_uvars:bool) (tm:term) : t let! tm, typ, guard = __tc e tm in if_verbose (fun () -> BU.print5 "t_apply: tm = %s\nt_apply: goal = %s\nenv.gamma=%s\ntyp=%s\nguard=%s\n" - (Print.term_to_string tm) + (show tm) (goal_to_string_verbose goal) (Env.print_gamma e.gamma) - (Print.term_to_string typ) + (show typ) (Rel.guard_to_string e guard)) ;! // Focus helps keep the goal order let typ = bnorm e typ in let! uvs = try_unify_by_application (Some should_check) only_match e typ (goal_type goal) (rangeof goal) in if_verbose (fun () -> BU.print1 "t_apply: found args = %s\n" - (FStar.Common.string_of_list (fun (t, _, _) -> Print.term_to_string t) uvs)) ;! + (FStar.Common.string_of_list (fun (t, _, _) -> show t) uvs)) ;! let w = List.fold_right (fun (uvt, q, _) w -> U.mk_app w [(uvt, q)]) uvs tm in let uvset = List.fold_right @@ -1027,7 +1028,7 @@ let rec fold_left (f : ('a -> 'b -> tac 'b)) (e : 'b) (xs : list 'a) : tac 'b = let t_apply_lemma (noinst:bool) (noinst_lhs:bool) (tm:term) : tac unit = wrap_err "apply_lemma" <| focus ( let! ps = get in - if_verbose (fun () -> BU.print1 "apply_lemma: tm = %s\n" (Print.term_to_string tm)) ;! + if_verbose (fun () -> BU.print1 "apply_lemma: tm = %s\n" (show tm)) ;! let is_unit_t t = match (SS.compress t).n with | Tm_fvar fv when S.fv_eq_lid fv PC.unit_lid -> true @@ -1061,8 +1062,8 @@ let t_apply_lemma (noinst:bool) (noinst_lhs:bool) if Env.debug env <| Options.Other "2635" then BU.print2 "Apply lemma created a new uvar %s while applying %s\n" - (Print.ctx_uvar_to_string u) - (Print.term_to_string tm); + (show u) + (show tm); ret ((t, aq)::uvs, u::deps, (t, u)::imps, S.NT(b, t)::subst)) ([], [], [], []) bs @@ -1177,7 +1178,7 @@ let subst_goal (b1 : bv) (b2 : bv) (g:goal) : tac (option (bv * goal)) = let rewrite (h:binder) : tac unit = wrap_err "rewrite" <| ( let! goal = cur_goal in let bv = h.binder_bv in - if_verbose (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (Print.bv_to_string bv) (Print.term_to_string bv.sort)) ;! + if_verbose (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (show bv) (show bv.sort)) ;! match split_env bv (goal_env goal) with | None -> fail "binder not found in environment" | Some (e0, bv, bvs) -> @@ -1295,8 +1296,8 @@ let clear (b : binder) : tac unit = let bv = b.binder_bv in let! goal = cur_goal in if_verbose (fun () -> BU.print2 "Clear of (%s), env has %s binders\n" - (Print.binder_to_string b) - (Env.all_binders (goal_env goal) |> List.length |> string_of_int)) ;! + (show b) + (Env.all_binders (goal_env goal) |> List.length |> show)) ;! match split_env bv (goal_env goal) with | None -> fail "Cannot clear; binder not in environment" | Some (e', bv, bvs) -> @@ -1306,7 +1307,7 @@ let clear (b : binder) : tac unit = | bv'::bvs -> if free_in bv bv'.sort then fail (BU.format1 "Cannot clear; binder present in the type of %s" - (Print.bv_to_string bv')) + (show bv')) else check bvs in if free_in bv (goal_type goal) then @@ -1599,12 +1600,12 @@ let lax_on () : tac bool = ret (Options.lax () || (goal_env g).lax) let unquote (ty : term) (tm : term) : tac term = wrap_err "unquote" <| ( - if_verbose (fun () -> BU.print1 "unquote: tm = %s\n" (Print.term_to_string tm)) ;! + if_verbose (fun () -> BU.print1 "unquote: tm = %s\n" (show tm)) ;! let! goal = cur_goal in let env = Env.set_expected_typ (goal_env goal) ty in let! tm, typ, guard = __tc_ghost env tm in - if_verbose (fun () -> BU.print1 "unquote: tm' = %s\n" (Print.term_to_string tm)) ;! - if_verbose (fun () -> BU.print1 "unquote: typ = %s\n" (Print.term_to_string typ)) ;! + if_verbose (fun () -> BU.print1 "unquote: tm' = %s\n" (show tm)) ;! + if_verbose (fun () -> BU.print1 "unquote: typ = %s\n" (show typ)) ;! proc_guard "unquote" env guard (Some (should_check_goal_uvar goal)) (rangeof goal) ;! ret tm ) @@ -1728,7 +1729,7 @@ let fresh_bv_named (nm : string) : tac bv = idtac ;! ret (gen_bv nm None S.tun) let change (ty : typ) : tac unit = wrap_err "change" <| ( - if_verbose (fun () -> BU.print1 "change: ty = %s\n" (Print.term_to_string ty)) ;! + if_verbose (fun () -> BU.print1 "change: ty = %s\n" (show ty)) ;! let! g = cur_goal in let! ty, _, guard = __tc (goal_env g) ty in proc_guard "change" (goal_env g) guard (Some (should_check_goal_uvar g)) (rangeof g) ;! @@ -1809,8 +1810,8 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( | Some se -> match se.sigel with | Sig_datacon {us=c_us; t=c_ty; num_ty_params=nparam; mutuals=mut} -> - (* BU.print2 "ty of %s = %s\n" (Ident.string_of_lid c_lid) *) - (* (Print.term_to_string c_ty); *) + (* BU.print2 "ty of %s = %s\n" (show c_lid) *) + (* (show c_ty); *) let fv = S.lid_as_fv c_lid (Some Data_ctor) in @@ -1822,8 +1823,8 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( * fresh univ_uvars for its universes. *) let c_us, c_ty = Env.inst_tscheme (c_us, c_ty) in - (* BU.print2 "ty(2) of %s = %s\n" (Ident.string_of_lid c_lid) *) - (* (Print.term_to_string c_ty); *) + (* BU.print2 "ty(2) of %s = %s\n" (show c_lid) *) + (* (show c_ty); *) (* Deconstruct its type, separating the parameters from the * actual arguments (indices do not matter here). *) @@ -1833,7 +1834,7 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( let bs, comp = let rename_bv bv = let ppname = bv.ppname in - let ppname = mk_ident ("a" ^ string_of_id ppname, range_of_id ppname) in + let ppname = mk_ident ("a" ^ show ppname, range_of_id ppname) in // freshen just to be extra safe.. probably not needed freshen_bv ({ bv with ppname = ppname }) in @@ -2050,7 +2051,7 @@ let rec inspect (t:term) : tac term_view = wrap_err "inspect" ( ret <| Tv_Unknown | _ -> - Err.log_issue t.pos (Err.Warning_CantInspect, BU.format2 "inspect: outside of expected syntax (%s, %s)\n" (Print.tag_of_term t) (Print.term_to_string t)); + Err.log_issue t.pos (Err.Warning_CantInspect, BU.format2 "inspect: outside of expected syntax (%s, %s)\n" (Print.tag_of_term t) (show t)); ret <| Tv_Unsupp ) @@ -2190,18 +2191,18 @@ let t_commute_applied_match () : tac unit = wrap_err "t_commute_applied_match" < let string_to_term (e: Env.env) (s: string): tac term = let open FStar.Parser.ParseIt in - let frag_of_text s = { frag_fname= "" + let frag_of_text s = { frag_fname= "" ; frag_line = 1 ; frag_col = 0 ; frag_text = s } in match parse (Fragment (frag_of_text s)) with | Term t -> let dsenv = FStar.Syntax.DsEnv.set_current_module e.dsenv (current_module e) in begin try ret (FStar.ToSyntax.ToSyntax.desugar_term dsenv t) with - | FStar.Errors.Error (_, e, _, _) -> fail ("string_of_term: " ^ Errors.rendermsg e) - | _ -> fail ("string_of_term: Unknown error") + | FStar.Errors.Error (_, e, _, _) -> fail ("string_to_term: " ^ Errors.rendermsg e) + | _ -> fail ("string_to_term: Unknown error") end - | ASTFragment _ -> fail ("string_of_term: expected a Term as a result, got an ASTFragment") - | ParseError (_, err, _) -> fail ("string_of_term: got error " ^ Errors.rendermsg err) // FIXME + | ASTFragment _ -> fail ("string_to_term: expected a Term as a result, got an ASTFragment") + | ParseError (_, err, _) -> fail ("string_to_term: got error " ^ Errors.rendermsg err) // FIXME let push_bv_dsenv (e: Env.env) (i: string): tac (env * bv) = let ident = Ident.mk_ident (i, FStar.Compiler.Range.dummyRange) in @@ -2209,7 +2210,7 @@ let push_bv_dsenv (e: Env.env) (i: string): tac (env * bv) ret ({ e with dsenv }, bv) let term_to_string (t:term) : tac string - = let s = Print.term_to_string t in + = let s = show t in ret s let comp_to_string (c:comp) : tac string @@ -2217,7 +2218,7 @@ let comp_to_string (c:comp) : tac string ret s let range_to_string (r:FStar.Compiler.Range.range) : tac string - = ret (Range.string_of_range r) + = ret (show r) let term_eq_old (t1:term) (t2:term) : tac bool = idtac ;! diff --git a/src/tactics/FStar.Tactics.V1.InterpFuns.fst b/src/tactics/FStar.Tactics.V1.InterpFuns.fst index 0df6b8bfb41..ee60f8b60c0 100644 --- a/src/tactics/FStar.Tactics.V1.InterpFuns.fst +++ b/src/tactics/FStar.Tactics.V1.InterpFuns.fst @@ -51,16 +51,16 @@ let rec drop n l = let timing_int (l:Ident.lid) f = fun psc cb args -> - (* BU.print1 "Entering primitive %s {\n" (Ident.string_of_lid l); *) + (* BU.print1 "Entering primitive %s {\n" (show l); *) let r = f psc cb args in - (* BU.print1 "%s }\n" (Ident.string_of_lid l); *) + (* BU.print1 "%s }\n" (show l); *) r let timing_nbe (l:Ident.lid) f = fun nbe_cbs args -> - (* BU.print1 "Entering NBE primitive %s {\n" (Ident.string_of_lid l); *) + (* BU.print1 "Entering NBE primitive %s {\n" (show l); *) let r = f nbe_cbs args in - (* BU.print1 "%s }\n" (Ident.string_of_lid l); *) + (* BU.print1 "%s }\n" (show l); *) r let mk nm arity nunivs interp nbe_interp : PO.primitive_step = diff --git a/src/tactics/FStar.Tactics.V1.Interpreter.fst b/src/tactics/FStar.Tactics.V1.Interpreter.fst index d042d900e51..288f96ba216 100644 --- a/src/tactics/FStar.Tactics.V1.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V1.Interpreter.fst @@ -35,6 +35,7 @@ open FStar.Tactics.CtrlRewrite open FStar.Tactics.V1.InterpFuns open FStar.Tactics.Native open FStar.Tactics.Common +open FStar.Class.Show module BU = FStar.Compiler.Util module Cfg = FStar.TypeChecker.Cfg @@ -144,10 +145,10 @@ let unembed_tactic_0 (eb:embedding 'b) (embedded_tac_b:term) (ncb:norm_cb) : tac else N.normalize_with_primitive_steps in (* if proof_state.tac_verb_dbg then *) - (* BU.print1 "Starting normalizer with %s\n" (Print.term_to_string tm); *) + (* BU.print1 "Starting normalizer with %s\n" (show tm); *) let result = norm_f (primitive_steps ()) steps proof_state.main_context tm in (* if proof_state.tac_verb_dbg then *) - (* BU.print1 "Reduced tactic: got %s\n" (Print.term_to_string result); *) + (* BU.print1 "Reduced tactic: got %s\n" (show result); *) let res = unembed (E.e_result eb) result ncb in @@ -178,7 +179,7 @@ let unembed_tactic_0 (eb:embedding 'b) (embedded_tac_b:term) (ncb:norm_cb) : tac in Err.raise_error (Err.Fatal_TacticGotStuck, (BU.format2 "Tactic got stuck!\n\ - Reduction stopped at: %s%s" (Print.term_to_string h_result) maybe_admit_tip)) proof_state.main_context.range + Reduction stopped at: %s%s" (show h_result) maybe_admit_tip)) proof_state.main_context.range ) let unembed_tactic_nbe_0 (eb:NBET.embedding 'b) (cb:NBET.nbe_cbs) (embedded_tac_b:NBET.t) : tac 'b = diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index 6446aa7511d..f5a656bf63b 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -90,7 +90,7 @@ let core_check env sol t must_tot | Inr err -> debug (fun _ -> BU.print5 "(%s) Core checking failed (%s) on term %s and type %s\n%s\n" - (Range.string_of_range (Env.get_range env)) + (show (Env.get_range env)) (Core.print_error_short err) (show sol) (show t) @@ -249,33 +249,33 @@ let proc_guard_formula // should somehow taint the state instead of just printing a warning Err.log_issue e.range (Errors.Warning_TacAdmit, BU.format1 "Tactics admitted guard <%s>\n\n" - (Print.term_to_string f)); + (show f)); ret () | Goal -> - mlog (fun () -> BU.print2 "Making guard (%s:%s) into a goal\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Making guard (%s:%s) into a goal\n" reason (show f)) (fun () -> let! g = goal_of_guard reason e f sc_opt rng in push_goals [g]) | SMT -> - mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Pushing guard (%s:%s) as SMT goal\n" reason (show f)) (fun () -> let! g = goal_of_guard reason e f sc_opt rng in push_smt_goals [g]) | SMTSync -> - mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason (show f)) (fun () -> let g = { Env.trivial_guard with guard_f = NonTrivial f } in Rel.force_trivial_guard e g; ret ()) | Force -> - mlog (fun () -> BU.print2 "Forcing guard (%s:%s)\n" reason (Print.term_to_string f)) (fun () -> + mlog (fun () -> BU.print2 "Forcing guard (%s:%s)\n" reason (show f)) (fun () -> let g = { Env.trivial_guard with guard_f = NonTrivial f } in try if not (Env.is_trivial <| Rel.discharge_guard_no_smt e g) then fail1 "Forcing the guard failed (%s)" reason else ret () with - | _ -> mlog (fun () -> BU.print1 "guard = %s\n" (Print.term_to_string f)) (fun () -> + | _ -> mlog (fun () -> BU.print1 "guard = %s\n" (show f)) (fun () -> fail1 "Forcing the guard failed (%s)" reason)) let proc_guard' (simplify:bool) (reason:string) (e : env) (g : guard_t) (sc_opt:option should_check_uvar) (rng:Range.range) : tac unit = @@ -337,7 +337,7 @@ let tc_unifier_solved_implicits env (must_tot:bool) (allow_guards:bool) (uvs:lis && NonTrivial? guard.guard_f then ( fail3 "Could not typecheck unifier solved implicit %s to %s since it produced a guard and guards were not allowed;guard is\n%s" - (Print.uvar_to_string u.ctx_uvar_head) + (show u.ctx_uvar_head) (show sol) (show g) ) @@ -349,7 +349,7 @@ let tc_unifier_solved_implicits env (must_tot:bool) (allow_guards:bool) (uvs:lis | Inr failed -> fail3 "Could not typecheck unifier solved implicit %s to %s because %s" - (Print.uvar_to_string u.ctx_uvar_head) + (show u.ctx_uvar_head) (show sol) (Core.print_error failed) in @@ -418,7 +418,7 @@ let __do_unify_wflags end | Errors.Error (_, msg, r, _) -> begin mlog (fun () -> BU.print2 ">> do_unify error, (%s) at (%s)\n" - (Errors.rendermsg msg) (Range.string_of_range r)) (fun _ -> + (Errors.rendermsg msg) (show r)) (fun _ -> ret None) end ) @@ -705,14 +705,14 @@ let bv_to_binding (bv : bv) : RD.binding = { uniq = Z.of_int_fs bv.index; sort = bv.sort; - ppname = string_of_id bv.ppname; + ppname = show bv.ppname; } let binder_to_binding (b:binder) : RD.binding = bv_to_binding b.binder_bv let binding_to_string (b : RD.binding) : string = - b.ppname ^ "#" ^ string_of_int (Z.to_int_fs b.uniq) + b.ppname ^ "#" ^ show (Z.to_int_fs b.uniq) let binding_to_bv (b : RD.binding) : bv = @@ -767,7 +767,7 @@ let intro () : tac RD.binding = wrap_err "intro" <| ( // (show sol); //BU.print1 "[intro]: old goal is %s" (goal_to_string goal); //BU.print1 "[intro]: new goal is %s" - // (Print.ctx_uvar_to_string ctx_uvar); + // (show ctx_uvar); //ignore (FStar.Options.set_options "--debug_level Rel"); (* Suppose if instead of simply assigning `?u` to the lambda term on the RHS, we tried to unify `?u` with the `(fun (x:t) -> ?v @ [NM(x, 0)])`. @@ -933,7 +933,7 @@ let try_unify_by_application (should_check:option should_check_uvar) | Some (b, c) -> if not (U.is_total_comp c) then fail "Codomain is effectful" else let! uvt, uv = new_uvar "apply arg" e b.binder_bv.sort should_check typedness_deps rng in - if_verbose (fun () -> BU.print1 "t_apply: generated uvar %s\n" (Print.ctx_uvar_to_string uv)) ;! + if_verbose (fun () -> BU.print1 "t_apply: generated uvar %s\n" (show uv)) ;! let typ = U.comp_result c in let typ' = SS.subst [S.NT (b.binder_bv, uvt)] typ in aux ((uvt, U.aqual_of_binder b, uv)::acc) (uv::typedness_deps) typ' @@ -986,9 +986,9 @@ let t_apply (uopt:bool) (only_match:bool) (tc_resolved_uvars:bool) (tm:term) : t let tc_resolved_uvars = true in if_verbose (fun () -> BU.print4 "t_apply: uopt %s, only_match %s, tc_resolved_uvars %s, tm = %s\n" - (string_of_bool uopt) - (string_of_bool only_match) - (string_of_bool tc_resolved_uvars) + (show uopt) + (show only_match) + (show tc_resolved_uvars) (show tm)) ;! let! ps = get in let! goal = cur_goal in @@ -1098,7 +1098,7 @@ let t_apply_lemma (noinst:bool) (noinst_lhs:bool) if Env.debug env <| Options.Other "2635" then BU.print2 "Apply lemma created a new uvar %s while applying %s\n" - (Print.ctx_uvar_to_string u) + (show u) (show tm); ret ((t, aq)::uvs, u::deps, (t, u)::imps, S.NT(b, t)::subst)) ([], [], [], []) @@ -1215,7 +1215,7 @@ let rewrite (hh:RD.binding) : tac unit = wrap_err "rewrite" <| ( let! goal = cur_goal in let h = binding_to_binder hh in let bv = h.binder_bv in - if_verbose (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (Print.bv_to_string bv) (show bv.sort)) ;! + if_verbose (fun _ -> BU.print2 "+++Rewrite %s : %s\n" (show bv) (show bv.sort)) ;! match split_env bv (goal_env goal) with | None -> fail "binder not found in environment" | Some (e0, bv, bvs) -> @@ -1334,7 +1334,7 @@ let clear (b : RD.binding) : tac unit = let! goal = cur_goal in if_verbose (fun () -> BU.print2 "Clear of (%s), env has %s binders\n" (binding_to_string b) - (Env.all_binders (goal_env goal) |> List.length |> string_of_int)) ;! + (Env.all_binders (goal_env goal) |> List.length |> show)) ;! match split_env bv (goal_env goal) with | None -> fail "Cannot clear; binder not in environment" | Some (e', bv, bvs) -> @@ -1344,7 +1344,7 @@ let clear (b : RD.binding) : tac unit = | bv'::bvs -> if free_in bv bv'.sort then fail (BU.format1 "Cannot clear; binder present in the type of %s" - (Print.bv_to_string bv')) + (show bv')) else check bvs in if free_in bv (goal_type goal) then @@ -1855,7 +1855,7 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( | Some se -> match se.sigel with | Sig_datacon {us=c_us; t=c_ty; num_ty_params=nparam; mutuals=mut} -> - (* BU.print2 "ty of %s = %s\n" (Ident.string_of_lid c_lid) *) + (* BU.print2 "ty of %s = %s\n" (show c_lid) *) (* (show c_ty); *) let fv = S.lid_as_fv c_lid (Some Data_ctor) in @@ -1868,7 +1868,7 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( * fresh univ_uvars for its universes. *) let c_us, c_ty = Env.inst_tscheme (c_us, c_ty) in - (* BU.print2 "ty(2) of %s = %s\n" (Ident.string_of_lid c_lid) *) + (* BU.print2 "ty(2) of %s = %s\n" (show c_lid) *) (* (show c_ty); *) (* Deconstruct its type, separating the parameters from the @@ -1879,7 +1879,7 @@ let t_destruct (s_tm : term) : tac (list (fv * Z.t)) = wrap_err "destruct" <| ( let bs, comp = let rename_bv bv = let ppname = bv.ppname in - let ppname = mk_ident ("a" ^ string_of_id ppname, range_of_id ppname) in + let ppname = mk_ident ("a" ^ show ppname, range_of_id ppname) in // freshen just to be extra safe.. probably not needed freshen_bv ({ bv with ppname = ppname }) in @@ -2028,11 +2028,11 @@ let string_to_term (e: Env.env) (s: string): tac term let dsenv = FStar.Syntax.DsEnv.set_current_module e.dsenv (current_module e) in begin try ret (FStar.ToSyntax.ToSyntax.desugar_term dsenv t) with | FStar.Errors.Error (_, e, _, _) -> - fail ("string_of_term: " ^ Errors.rendermsg e) - | _ -> fail ("string_of_term: Unknown error") + fail ("string_to_term: " ^ Errors.rendermsg e) + | _ -> fail ("string_to_term: Unknown error") end - | ASTFragment _ -> fail ("string_of_term: expected a Term as a result, got an ASTFragment") - | ParseError (_, err, _) -> fail ("string_of_term: got error " ^ Errors.rendermsg err) // FIXME + | ASTFragment _ -> fail ("string_to_term: expected a Term as a result, got an ASTFragment") + | ParseError (_, err, _) -> fail ("string_to_term: got error " ^ Errors.rendermsg err) // FIXME let push_bv_dsenv (e: Env.env) (i: string): tac (env * RD.binding) = let ident = Ident.mk_ident (i, FStar.Compiler.Range.dummyRange) in @@ -2060,7 +2060,7 @@ let comp_to_doc (c:comp) : tac Pprint.document ret s let range_to_string (r:FStar.Compiler.Range.range) : tac string - = ret (Range.string_of_range r) + = ret (show r) let term_eq_old (t1:term) (t2:term) : tac bool = idtac ;! @@ -2260,10 +2260,10 @@ let refl_is_non_informative (g:env) (t:typ) : tac (option unit & issues) = let g = Env.set_range g t.pos in dbg_refl g (fun _ -> BU.format1 "refl_is_non_informative: %s\n" - (Print.term_to_string t)); + (show t)); let b = Core.is_non_informative g t in dbg_refl g (fun _ -> BU.format1 "refl_is_non_informative: returned %s" - (string_of_bool b)); + (show b)); if b then ((), []) else Errors.raise_error (Errors.Fatal_UnexpectedTerm, "is_non_informative returned false ") @@ -2386,7 +2386,7 @@ let refl_core_check_term_at_type (g:env) (e:term) (t:typ) let g = Env.set_range g e.pos in dbg_refl g (fun _ -> BU.format2 "refl_core_check_term_at_type: term: %s, type: %s\n" - (Print.term_to_string e) (Print.term_to_string t)); + (show e) (show t)); match Core.check_term_at_type g e t with | Inl (eff, None) -> dbg_refl g (fun _ -> @@ -2410,7 +2410,7 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ then refl_typing_builtin_wrapper "refl_tc_term" (fun _ -> let g = Env.set_range g e.pos in dbg_refl g (fun _ -> - BU.format2 "refl_tc_term@%s: %s\n" (Range.string_of_range e.pos) (show e)); + BU.format2 "refl_tc_term@%s: %s\n" (show e.pos) (show e)); dbg_refl g (fun _ -> "refl_tc_term: starting tc {\n"); // // we don't instantiate implicits at the end of e @@ -2439,7 +2439,7 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ if not (no_uvars_in_term e) then ( Errors.raise_error (Errors.Error_UnexpectedUnresolvedUvar, - BU.format1 "Elaborated term has unresolved implicits: %s" (Print.term_to_string e)) + BU.format1 "Elaborated term has unresolved implicits: %s" (show e)) e.pos ) else ( @@ -2449,15 +2449,15 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ // TODO: may be should we check here that e has no unresolved implicits? dbg_refl g (fun _ -> BU.format1 "} finished tc with e = %s\n" - (Print.term_to_string e)); + (show e)); let guards : ref (list (env & typ)) = BU.mk_ref [] in let gh = fun g guard -> (* collect guards and return them *) dbg_refl g (fun _ -> BU.format3 "Got guard in Env@%s |- %s@%s\n" - (Env.get_range g |> Range.string_of_range) - (Print.term_to_string guard) - (Range.string_of_range guard.pos) + (Env.get_range g |> show) + (show guard) + (show guard.pos) ); guards := (g, guard) :: !guards; true @@ -2467,9 +2467,9 @@ let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ let t = refl_norm_type g t in dbg_refl g (fun _ -> BU.format3 "refl_tc_term@%s for %s computed type %s\n" - (Range.string_of_range e.pos) - (Print.term_to_string e) - (Print.term_to_string t)); + (show e.pos) + (show e) + (show t)); ((e, (eff, t)), !guards) | Inr err -> dbg_refl g (fun _ -> BU.format1 "refl_tc_term failed: %s\n" (Core.print_error err)); @@ -2603,11 +2603,11 @@ let refl_instantiate_implicits (g:env) (e:term) if not (no_univ_uvars_in_term e) then Errors.raise_error (Errors.Error_UnexpectedUnresolvedUvar, - BU.format1 "Elaborated term has unresolved univ uvars: %s" (Print.term_to_string e)) + BU.format1 "Elaborated term has unresolved univ uvars: %s" (show e)) e.pos else if not (no_univ_uvars_in_term t) then Errors.raise_error (Errors.Error_UnexpectedUnresolvedUvar, - BU.format1 "Inferred type has unresolved univ uvars: %s" (Print.term_to_string t)) + BU.format1 "Inferred type has unresolved univ uvars: %s" (show t)) e.pos else let g = Env.push_bvs g (List.map (fun (bv, t) -> {bv with sort=t}) bvs_and_ts) in @@ -2620,8 +2620,8 @@ let refl_instantiate_implicits (g:env) (e:term) dbg_refl g (fun _ -> BU.format2 "} finished tc with e = %s and t = %s\n" - (Print.term_to_string e) - (Print.term_to_string t)); + (show e) + (show t)); ((bvs_and_ts, e, t), []) ) else ret (None, [unexpected_uvars_issue (Env.get_range g)]) @@ -2662,7 +2662,7 @@ let refl_maybe_unfold_head (g:env) (e:term) : tac (option term & issues) = then Errors.raise_error (Errors.Fatal_UnexpectedTerm, BU.format1 "Could not unfold head: %s\n" - (Print.term_to_string e)) e.pos + (show e)) e.pos else (eopt |> must, [])) else ret (None, [unexpected_uvars_issue (Env.get_range g)]) diff --git a/src/tactics/FStar.Tactics.V2.InterpFuns.fst b/src/tactics/FStar.Tactics.V2.InterpFuns.fst index 5889606c37a..0f5d2d9f64c 100644 --- a/src/tactics/FStar.Tactics.V2.InterpFuns.fst +++ b/src/tactics/FStar.Tactics.V2.InterpFuns.fst @@ -52,16 +52,16 @@ let rec drop n l = let timing_int (l:Ident.lid) f = fun psc cb args -> - (* BU.print1 "Entering primitive %s {\n" (Ident.string_of_lid l); *) + (* BU.print1 "Entering primitive %s {\n" (show l); *) let r = f psc cb args in - (* BU.print1 "%s }\n" (Ident.string_of_lid l); *) + (* BU.print1 "%s }\n" (show l); *) r let timing_nbe (l:Ident.lid) f = fun nbe_cbs args -> - (* BU.print1 "Entering NBE primitive %s {\n" (Ident.string_of_lid l); *) + (* BU.print1 "Entering NBE primitive %s {\n" (show l); *) let r = f nbe_cbs args in - (* BU.print1 "%s }\n" (Ident.string_of_lid l); *) + (* BU.print1 "%s }\n" (show l); *) r let mk nm arity nunivs interp nbe_interp : PO.primitive_step = diff --git a/src/tactics/FStar.Tactics.V2.Interpreter.fst b/src/tactics/FStar.Tactics.V2.Interpreter.fst index a7ffe3ee4fc..7b296570d50 100644 --- a/src/tactics/FStar.Tactics.V2.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V2.Interpreter.fst @@ -38,6 +38,7 @@ open FStar.Tactics.CtrlRewrite open FStar.Tactics.V2.InterpFuns open FStar.Tactics.Native open FStar.Tactics.Common +open FStar.Class.Show module BU = FStar.Compiler.Util module Cfg = FStar.TypeChecker.Cfg @@ -154,10 +155,10 @@ let unembed_tactic_0 (eb:embedding 'b) (embedded_tac_b:term) (ncb:norm_cb) : tac else N.normalize_with_primitive_steps in (* if proof_state.tac_verb_dbg then *) - (* BU.print1 "Starting normalizer with %s\n" (Print.term_to_string tm); *) + (* BU.print1 "Starting normalizer with %s\n" (show tm); *) let result = norm_f (primitive_steps ()) steps proof_state.main_context tm in (* if proof_state.tac_verb_dbg then *) - (* BU.print1 "Reduced tactic: got %s\n" (Print.term_to_string result); *) + (* BU.print1 "Reduced tactic: got %s\n" (show result); *) let res = unembed (E.e_result eb) result ncb in @@ -732,17 +733,17 @@ let report_implicits rng (is : TcRel.tagged_implicits) : unit = Errors.log_issue rng (Err.Error_UninstantiatedUnificationVarInTactic, BU.format3 ("Tactic left uninstantiated unification variable %s of type %s (reason = \"%s\")") - (Print.uvar_to_string imp.imp_uvar.ctx_uvar_head) - (Print.term_to_string (U.ctx_uvar_typ imp.imp_uvar)) + (show imp.imp_uvar.ctx_uvar_head) + (show (U.ctx_uvar_typ imp.imp_uvar)) imp.imp_reason) | TcRel.Implicit_has_typing_guard (tm, ty) -> Errors.log_issue rng (Err.Error_UninstantiatedUnificationVarInTactic, BU.format4 ("Tactic solved goal %s of type %s to %s : %s, but it has a non-trivial typing guard. Use gather_or_solve_explicit_guards_for_resolved_goals to inspect and prove these goals") - (Print.uvar_to_string imp.imp_uvar.ctx_uvar_head) - (Print.term_to_string (U.ctx_uvar_typ imp.imp_uvar)) - (Print.term_to_string tm) - (Print.term_to_string ty))); + (show imp.imp_uvar.ctx_uvar_head) + (show (U.ctx_uvar_typ imp.imp_uvar)) + (show tm) + (show ty))); Err.stop_if_err () let run_tactic_on_ps' @@ -763,8 +764,8 @@ let run_tactic_on_ps' let env = ps.main_context in if !tacdbg then BU.print2 "Typechecking tactic: (%s) (already_typed: %s) {\n" - (Print.term_to_string tactic) - (string_of_bool tactic_already_typed); + (show tactic) + (show tactic_already_typed); (* Do NOT use the returned tactic, the typechecker is not idempotent and * will mess up the monadic lifts. We're just making sure it's well-typed @@ -783,7 +784,7 @@ let run_tactic_on_ps' let tau = unembed_tactic_1 e_arg e_res tactic FStar.Syntax.Embeddings.id_norm_cb in (* if !tacdbg then *) - (* BU.print1 "Running tactic with goal = (%s) {\n" (Print.term_to_string typ); *) + (* BU.print1 "Running tactic with goal = (%s) {\n" (show typ); *) let res = Profiling.profile (fun () -> run_safe (tau arg) ps) @@ -796,42 +797,38 @@ let run_tactic_on_ps' match res with | Success (ret, ps) -> (* if !tacdbg || Options.tactics_info () then *) - (* BU.print1 "Tactic generated proofterm %s\n" (Print.term_to_string w); *) + (* BU.print1 "Tactic generated proofterm %s\n" (show w); *) let remaining_smt_goals = ps.goals@ps.smt_goals in List.iter (fun g -> FStar.Tactics.V2.Basic.mark_goal_implicit_already_checked g;//all of these will be fed to SMT anyway if is_irrelevant g then ( - if !tacdbg then BU.print1 "Assigning irrelevant goal %s\n" (Print.term_to_string (goal_witness g)); + if !tacdbg then BU.print1 "Assigning irrelevant goal %s\n" (show (goal_witness g)); if TcRel.teq_nosmt_force (goal_env g) (goal_witness g) U.exp_unit then () else failwith (BU.format1 "Irrelevant tactic witness does not unify with (): %s" - (Print.term_to_string (goal_witness g))) + (show (goal_witness g))) )) remaining_smt_goals; // Check that all implicits were instantiated if !tacdbg then BU.print1 "About to check tactic implicits: %s\n" (FStar.Common.string_of_list - (fun imp -> Print.ctx_uvar_to_string imp.imp_uvar) + (fun imp -> show imp.imp_uvar) ps.all_implicits); let g = {Env.trivial_guard with TcComm.implicits=ps.all_implicits} in let g = TcRel.solve_deferred_constraints env g in if !tacdbg then BU.print2 "Checked %s implicits (1): %s\n" - (string_of_int (List.length ps.all_implicits)) - (FStar.Common.string_of_list - (fun imp -> Print.ctx_uvar_to_string imp.imp_uvar) - ps.all_implicits); + (show (List.length ps.all_implicits)) + (show ps.all_implicits); let tagged_implicits = TcRel.resolve_implicits_tac env g in if !tacdbg then BU.print2 "Checked %s implicits (2): %s\n" - (string_of_int (List.length ps.all_implicits)) - (FStar.Common.string_of_list - (fun imp -> Print.ctx_uvar_to_string imp.imp_uvar) - ps.all_implicits); + (show (List.length ps.all_implicits)) + (show ps.all_implicits); report_implicits rng_goal tagged_implicits; // /implicits @@ -857,7 +854,7 @@ let run_tactic_on_ps' | TacticFailure s -> "\"" ^ s ^ "\"" | EExn t -> - "Uncaught exception: " ^ (Print.term_to_string t) + "Uncaught exception: " ^ (show t) | e -> raise e in diff --git a/src/typechecker/FStar.TypeChecker.Common.fst b/src/typechecker/FStar.TypeChecker.Common.fst index c7b9f7875aa..0a4fe72630b 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fst +++ b/src/typechecker/FStar.TypeChecker.Common.fst @@ -198,6 +198,10 @@ let check_uvar_ctx_invariant (reason:string) (r:range) (should_check:bool) (g:ga end | _ -> fail() +instance show_implicit : showable implicit = { + show = (fun i -> show i.imp_uvar.ctx_uvar_head); +} + let implicits_to_string imps = let imp_to_string i = Print.uvar_to_string i.imp_uvar.ctx_uvar_head diff --git a/src/typechecker/FStar.TypeChecker.Common.fsti b/src/typechecker/FStar.TypeChecker.Common.fsti index c3340343988..9a5f0978986 100644 --- a/src/typechecker/FStar.TypeChecker.Common.fsti +++ b/src/typechecker/FStar.TypeChecker.Common.fsti @@ -18,11 +18,17 @@ open Prims open FStar.Pervasives open FStar.Compiler.Effect -open FStar open FStar.Compiler +open FStar +open FStar.Compiler open FStar.Compiler.Util open FStar.Syntax open FStar.Syntax.Syntax open FStar.Ident +open FStar.Class.Show + +(* Bring instances in scope :-) *) +let () = let open FStar.Syntax.Print in () + module S = FStar.Syntax.Syntax module BU = FStar.Compiler.Util @@ -138,6 +144,9 @@ type implicit = { imp_tm : term; // The term, made up of the ctx_uvar imp_range : Range.range; // Position where it was introduced } + +instance val show_implicit : showable implicit + type implicits = list implicit val implicits_to_string : implicits -> string From 8ca2d3aece2491c15c9f58f1e93fae7a22828211 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 27 Nov 2023 21:53:01 -0800 Subject: [PATCH 2/2] snap --- .../generated/FStar_Compiler_Range_Ops.ml | 4 +- ocaml/fstar-lib/generated/FStar_Ident.ml | 6 +- .../fstar-lib/generated/FStar_Syntax_Print.ml | 10 +- .../generated/FStar_Tactics_CtrlRewrite.ml | 18 +- .../generated/FStar_Tactics_Embedding.ml | 10 +- .../generated/FStar_Tactics_Hooks.ml | 90 ++++++--- .../generated/FStar_Tactics_Monad.ml | 28 ++- .../generated/FStar_Tactics_Printing.ml | 36 ++-- .../generated/FStar_Tactics_V1_Basic.ml | 184 ++++++++++++------ .../generated/FStar_Tactics_V1_Interpreter.ml | 4 +- .../generated/FStar_Tactics_V2_Basic.ml | 149 +++++++++----- .../generated/FStar_Tactics_V2_Interpreter.ml | 68 ++++--- .../generated/FStar_TypeChecker_Common.ml | 7 + 13 files changed, 423 insertions(+), 191 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml b/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml index 8aaddcc84ef..a0c0ef1c24a 100644 --- a/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml +++ b/ocaml/fstar-lib/generated/FStar_Compiler_Range_Ops.ml @@ -254,4 +254,6 @@ let (json_of_def_range : FStar_Compiler_Range_Type.range -> FStar_Json.json) fun r -> let uu___ = file_of_range r in let uu___1 = start_of_range r in - let uu___2 = end_of_range r in json_of_range_fields uu___ uu___1 uu___2 \ No newline at end of file + let uu___2 = end_of_range r in json_of_range_fields uu___ uu___1 uu___2 +let (show_range : FStar_Compiler_Range_Type.range FStar_Class_Show.showable) + = { FStar_Class_Show.show = string_of_range } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Ident.ml b/ocaml/fstar-lib/generated/FStar_Ident.ml index 86f4119be37..664c003e056 100644 --- a/ocaml/fstar-lib/generated/FStar_Ident.ml +++ b/ocaml/fstar-lib/generated/FStar_Ident.ml @@ -127,4 +127,8 @@ let (qual_id : lident -> ident -> lident) = let uu___ = lid_of_ids (FStar_Compiler_List.op_At lid1.ns [lid1.ident; id]) in let uu___1 = range_of_id id in set_lid_range uu___ uu___1 -let (nsstr : lident -> Prims.string) = fun l -> l.nsstr \ No newline at end of file +let (nsstr : lident -> Prims.string) = fun l -> l.nsstr +let (showable_ident : ident FStar_Class_Show.showable) = + { FStar_Class_Show.show = string_of_id } +let (showable_lident : lident FStar_Class_Show.showable) = + { FStar_Class_Show.show = string_of_lid } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml index 81063503ef3..6ad6055fc83 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml @@ -2043,4 +2043,12 @@ let (pretty_term : FStar_Syntax_Syntax.term FStar_Class_PP.pretty) = let (showable_sigelt : FStar_Syntax_Syntax.sigelt FStar_Class_Show.showable) = { FStar_Class_Show.show = sigelt_to_string } let (showable_term : FStar_Syntax_Syntax.term FStar_Class_Show.showable) = - { FStar_Class_Show.show = term_to_string } \ No newline at end of file + { FStar_Class_Show.show = term_to_string } +let (showable_bv : FStar_Syntax_Syntax.bv FStar_Class_Show.showable) = + { FStar_Class_Show.show = bv_to_string } +let (showable_binder : FStar_Syntax_Syntax.binder FStar_Class_Show.showable) + = { FStar_Class_Show.show = binder_to_string } +let (showable_uvar : FStar_Syntax_Syntax.uvar FStar_Class_Show.showable) = + { FStar_Class_Show.show = uvar_to_string } +let (showable_ctxu : FStar_Syntax_Syntax.ctx_uvar FStar_Class_Show.showable) + = { FStar_Class_Show.show = ctx_uvar_to_string } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml index ae1a6825fcc..0df1e51fce7 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_CtrlRewrite.ml @@ -199,9 +199,11 @@ let (__do_rewrite : FStar_Tactics_Monad.if_verbose (fun uu___7 -> let uu___8 = - FStar_Syntax_Print.term_to_string tm in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm in let uu___9 = - FStar_Syntax_Print.term_to_string ut in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term ut in FStar_Compiler_Util.print2 "do_rewrite: making equality\n\t%s ==\n\t%s\n" uu___8 uu___9) in @@ -232,10 +234,12 @@ let (__do_rewrite : FStar_Tactics_Monad.if_verbose (fun uu___13 -> let uu___14 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm in let uu___15 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term ut1 in FStar_Compiler_Util.print2 "rewrite_rec: succeeded rewriting\n\t%s to\n\t%s\n" @@ -939,7 +943,8 @@ let (ctrl_rewrite : FStar_Tactics_Monad.if_verbose (fun uu___4 -> let uu___5 = - FStar_Syntax_Print.term_to_string gt in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term gt in FStar_Compiler_Util.print1 "ctrl_rewrite starting with %s\n" uu___5) in FStar_Tactics_Monad.op_let_Bang uu___3 @@ -954,7 +959,8 @@ let (ctrl_rewrite : FStar_Tactics_Monad.if_verbose (fun uu___7 -> let uu___8 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term gt' in FStar_Compiler_Util.print1 "ctrl_rewrite seems to have succeded with %s\n" diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml index a556be2fb37..18e47b80d8f 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml @@ -204,7 +204,7 @@ let (fv_as_emb_typ : FStar_Syntax_Syntax.fv -> FStar_Syntax_Syntax.emb_typ) = fun fv -> let uu___ = let uu___1 = - FStar_Ident.string_of_lid + FStar_Class_Show.show FStar_Ident.showable_lident (fv.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in (uu___1, []) in FStar_Syntax_Syntax.ET_app uu___ @@ -366,8 +366,8 @@ let (e_exn : Prims.exn FStar_Syntax_Embeddings_Base.embedding) = let uu___ = let uu___1 = let uu___2 = - FStar_Compiler_Effect.op_Bar_Greater FStar_Parser_Const.exn_lid - FStar_Ident.string_of_lid in + FStar_Class_Show.show FStar_Ident.showable_lident + FStar_Parser_Const.exn_lid in (uu___2, []) in FStar_Syntax_Syntax.ET_app uu___1 in FStar_Syntax_Embeddings_Base.mk_emb_full embed_exn unembed_exn @@ -489,8 +489,8 @@ let e_result : let uu___1 = let uu___2 = let uu___3 = - FStar_Compiler_Effect.op_Bar_Greater fstar_tactics_result.lid - FStar_Ident.string_of_lid in + FStar_Class_Show.show FStar_Ident.showable_lident + fstar_tactics_result.lid in let uu___4 = let uu___5 = FStar_Syntax_Embeddings_Base.emb_typ_of ea in [uu___5] in (uu___3, uu___4) in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml index 8e91a3b076d..cbb671dea49 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Hooks.ml @@ -570,7 +570,8 @@ let (preprocess : let uu___5 = FStar_TypeChecker_Env.all_binders env in FStar_Compiler_Effect.op_Bar_Greater uu___5 (FStar_Syntax_Print.binders_to_string ",") in - let uu___5 = FStar_Syntax_Print.term_to_string goal in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term goal in FStar_Compiler_Util.print2 "About to preprocess %s |= %s\n" uu___4 uu___5 else ()); @@ -593,7 +594,9 @@ let (preprocess : let uu___7 = FStar_TypeChecker_Env.all_binders env in FStar_Compiler_Effect.op_Bar_Greater uu___7 (FStar_Syntax_Print.binders_to_string ", ") in - let uu___7 = FStar_Syntax_Print.term_to_string t' in + let uu___7 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t' in FStar_Compiler_Util.print2 "Main goal simplified to: %s |- %s\n" uu___6 uu___7 else ()); @@ -618,7 +621,8 @@ let (preprocess : let uu___9 = let uu___10 = FStar_Tactics_Types.goal_type g in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___10 in FStar_Compiler_Util.format1 "Tactic returned proof-relevant goal: %s" @@ -634,11 +638,15 @@ let (preprocess : if uu___7 then let uu___8 = - FStar_Compiler_Util.string_of_int n in + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) + n in let uu___9 = let uu___10 = FStar_Tactics_Types.goal_type g in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___10 in FStar_Compiler_Util.print2 "Got goal #%s: %s\n" uu___8 uu___9 @@ -646,7 +654,10 @@ let (preprocess : (let label = let uu___7 = let uu___8 = - FStar_Compiler_Util.string_of_int n in + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) + n in let uu___9 = let uu___10 = let uu___11 = @@ -784,7 +795,9 @@ let rec (traverse_for_spinoff : | StrictlyPositive -> (if debug then - (let uu___1 = FStar_Syntax_Print.term_to_string t2 in + (let uu___1 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print1 "Spinning off %s\n" uu___1) else (); (let uu___1 = @@ -1053,7 +1066,8 @@ let rec (traverse_for_spinoff : (let uu___3 = FStar_TypeChecker_Env.get_range env in let uu___4 = let uu___5 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in FStar_Compiler_Util.format2 "Failed to split match term because %s (%s)" msg uu___5 in @@ -1066,9 +1080,11 @@ let rec (traverse_for_spinoff : (let uu___3 = FStar_TypeChecker_Env.get_range env in let uu___4 = let uu___5 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in let uu___6 = - FStar_Syntax_Print.term_to_string res1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term res1 in FStar_Compiler_Util.format2 "Rewrote match term\n%s\ninto %s\n" uu___5 uu___6 in @@ -1382,7 +1398,8 @@ let (spinoff_strictly_positive_goals : FStar_TypeChecker_Env.debug env (FStar_Options.Other "SpinoffAll") in if debug then - (let uu___1 = FStar_Syntax_Print.term_to_string goal in + (let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term goal in FStar_Compiler_Util.print1 "spinoff_all called with %s\n" uu___1) else (); FStar_Errors.with_ctx "While spinning off all goals" @@ -1417,7 +1434,9 @@ let (spinoff_strictly_positive_goals : FStar_TypeChecker_Env.all_binders env in FStar_Compiler_Effect.op_Bar_Greater uu___5 (FStar_Syntax_Print.binders_to_string ", ") in - let uu___5 = FStar_Syntax_Print.term_to_string t1 in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in FStar_Compiler_Util.format2 "Main goal simplified to: %s |- %s\n" uu___4 uu___5 in @@ -1468,7 +1487,8 @@ let (spinoff_strictly_positive_goals : (if debug then (let uu___8 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print1 "Got goal: %s\n" uu___8) @@ -1478,7 +1498,9 @@ let (spinoff_strictly_positive_goals : ((let uu___6 = FStar_TypeChecker_Env.get_range env in let uu___7 = let uu___8 = - FStar_Compiler_Util.string_of_int + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) (FStar_Compiler_List.length gs3) in FStar_Compiler_Util.format1 "Split query into %s sub-goals" uu___8 in @@ -1530,7 +1552,8 @@ let (synthesize : if uu___7 then let uu___8 = - FStar_Syntax_Print.term_to_string vc in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term vc in FStar_Compiler_Util.print1 "Synthesis left a goal: %s\n" uu___8 else ()); @@ -1582,7 +1605,9 @@ let (solve_implicits : if uu___4 then let uu___5 = - FStar_Compiler_Util.string_of_int + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) (FStar_Compiler_List.length gs) in FStar_Compiler_Util.print1 "solve_implicits produced %s goals\n" uu___5 @@ -1607,7 +1632,9 @@ let (solve_implicits : if uu___9 then let uu___10 = - FStar_Syntax_Print.term_to_string vc in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + vc in FStar_Compiler_Util.print1 "Synthesis left a goal: %s\n" uu___10 @@ -1734,7 +1761,8 @@ let (handle_smt_goal : if uu___8 then let uu___9 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term vc in FStar_Compiler_Util.print1 "handle_smt_goals left a goal: %s\n" @@ -2115,7 +2143,8 @@ let (splice : if uu___12 then let uu___13 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term vc in FStar_Compiler_Util.print1 "Splice left a goal: %s\n" @@ -2163,15 +2192,14 @@ let (splice : let uu___10 = let uu___11 = let uu___12 = - FStar_Ident.string_of_lid lid in + FStar_Class_Show.show + FStar_Ident.showable_lident + lid in let uu___13 = - let uu___14 = - FStar_Compiler_List.map - FStar_Ident.string_of_lid - lids' in - FStar_Compiler_Effect.op_Less_Bar - (FStar_Compiler_String.concat - ", ") uu___14 in + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Ident.showable_lident) + lids' in FStar_Compiler_Util.format2 "Splice declared the name %s but it was not defined.\nThose defined were: %s" uu___12 uu___13 in @@ -2186,8 +2214,9 @@ let (splice : if uu___10 then let uu___11 = - (FStar_Common.string_of_list ()) - FStar_Syntax_Print.sigelt_to_string + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_Syntax_Print.showable_sigelt) sigelts1 in FStar_Compiler_Util.print1 "splice: got decls = {\n\n%s\n\n}\n" @@ -2363,7 +2392,8 @@ let (postprocess : if uu___9 then let uu___10 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term vc in FStar_Compiler_Util.print1 "Postprocessing left a goal: %s\n" diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml index 3a00bb9c7d2..57a0083c23b 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml @@ -156,7 +156,10 @@ let (register_goal : FStar_Tactics_Types.goal -> unit) = (FStar_Options.Other "CoreEq") in if uu___6 then - let uu___7 = FStar_Compiler_Util.string_of_int i in + let uu___7 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) i in FStar_Compiler_Util.print1 "(%s) Registering goal\n" uu___7 else ()); (let should_register = is_goal_safe_as_well_typed g in @@ -172,7 +175,10 @@ let (register_goal : FStar_Tactics_Types.goal -> unit) = (FStar_Options.Other "RegisterGoal")) in (if uu___7 then - let uu___8 = FStar_Compiler_Util.string_of_int i in + let uu___8 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) i in FStar_Compiler_Util.print1 "(%s) Not registering goal since it has unresolved uvar deps\n" uu___8 @@ -188,8 +194,13 @@ let (register_goal : FStar_Tactics_Types.goal -> unit) = (FStar_Options.Other "RegisterGoal")) in if uu___8 then - let uu___9 = FStar_Compiler_Util.string_of_int i in - let uu___10 = FStar_Syntax_Print.ctx_uvar_to_string uv in + let uu___9 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) i in + let uu___10 = + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu + uv in FStar_Compiler_Util.print2 "(%s) Registering goal for %s\n" uu___9 uu___10 else ()); @@ -203,7 +214,8 @@ let (register_goal : FStar_Tactics_Types.goal -> unit) = let msg = let uu___9 = let uu___10 = FStar_Syntax_Util.ctx_uvar_typ uv in - FStar_Syntax_Print.term_to_string uu___10 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___10 in let uu___10 = FStar_TypeChecker_Core.print_error_short err in FStar_Compiler_Util.format2 @@ -426,7 +438,8 @@ let (check_valid_goal : FStar_Tactics_Types.goal -> unit) = let uu___7 = let uu___8 = let uu___9 = - FStar_Syntax_Print.bv_to_string bv in + FStar_Class_Show.show + FStar_Syntax_Print.showable_bv bv in Prims.op_Hat "bv: " uu___9 in Bad uu___8 in FStar_Compiler_Effect.raise uu___7 @@ -535,7 +548,8 @@ let (cur_goal : FStar_Tactics_Types.goal tac) = | FStar_Pervasives_Native.Some t -> ((let uu___3 = FStar_Tactics_Printing.goal_to_string_verbose hd in - let uu___4 = FStar_Syntax_Print.term_to_string t in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print2 "!!!!!!!!!!!! GOAL IS ALREADY SOLVED! %s\nsol is %s\n" uu___3 uu___4); diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Printing.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Printing.ml index 6da95721ff7..b11b3e1cf20 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Printing.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Printing.ml @@ -7,7 +7,7 @@ let (term_to_string : let (goal_to_string_verbose : FStar_Tactics_Types.goal -> Prims.string) = fun g -> let uu___ = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu g.FStar_Tactics_Types.goal_ctx_uvar in let uu___1 = let uu___2 = FStar_Tactics_Types.check_goal_solved' g in @@ -26,17 +26,19 @@ let (unshadow : = fun bs -> fun t -> - let s b = FStar_Ident.string_of_id b.FStar_Syntax_Syntax.ppname in - let sset bv s1 = + let sset bv s = let uu___ = let uu___1 = FStar_Ident.range_of_id bv.FStar_Syntax_Syntax.ppname in FStar_Pervasives_Native.Some uu___1 in - FStar_Syntax_Syntax.gen_bv s1 uu___ bv.FStar_Syntax_Syntax.sort in + FStar_Syntax_Syntax.gen_bv s uu___ bv.FStar_Syntax_Syntax.sort in let fresh_until b f = let rec aux i = let t1 = let uu___ = - let uu___1 = FStar_Compiler_Util.string_of_int i in + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) i in Prims.op_Hat "'" uu___1 in Prims.op_Hat b uu___ in let uu___ = f t1 in if uu___ then t1 else aux (i + Prims.int_one) in @@ -58,10 +60,12 @@ let (unshadow : (match uu___ with | (bv0, q) -> let nbs = - let uu___1 = s bv0 in + let uu___1 = + FStar_Class_Show.show FStar_Ident.showable_ident + bv0.FStar_Syntax_Syntax.ppname in fresh_until uu___1 - (fun s1 -> - Prims.op_Negation (FStar_Compiler_List.mem s1 seen)) in + (fun s -> + Prims.op_Negation (FStar_Compiler_List.mem s seen)) in let bv = sset bv0 nbs in let b2 = FStar_Syntax_Syntax.mk_binder_with_attrs bv q @@ -107,8 +111,14 @@ let (goal_to_string : match maybe_num with | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some (i, n) -> - let uu___ = FStar_Compiler_Util.string_of_int i in - let uu___1 = FStar_Compiler_Util.string_of_int n in + let uu___ = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) i in + let uu___1 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) n in FStar_Compiler_Util.format2 " %s/%s" uu___ uu___1 in let maybe_label = match g.FStar_Tactics_Types.label with @@ -188,7 +198,7 @@ let (ps_to_string : match uu___ with | (msg, ps) -> let p_imp imp = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_uvar (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in let n_active = FStar_Compiler_List.length ps.FStar_Tactics_Types.goals in @@ -199,7 +209,9 @@ let (ps_to_string : let uu___2 = let uu___3 = let uu___4 = - FStar_Compiler_Util.string_of_int + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_int) ps.FStar_Tactics_Types.depth in FStar_Compiler_Util.format2 "State dump @ depth %s (%s):\n" uu___4 msg in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index 01f7fc36746..8e4bc30853c 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -14,7 +14,7 @@ let (is_irrelevant : FStar_Tactics_Types.goal -> Prims.bool) = let (core_check : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> - FStar_Syntax_Syntax.term -> + FStar_Syntax_Syntax.typ -> Prims.bool -> (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option, FStar_TypeChecker_Core.error) FStar_Pervasives.either) @@ -47,11 +47,16 @@ let (core_check : (fun uu___4 -> let uu___5 = let uu___6 = FStar_TypeChecker_Env.get_range env in - FStar_Compiler_Range_Ops.string_of_range uu___6 in + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range uu___6 in let uu___6 = FStar_TypeChecker_Core.print_error_short err in - let uu___7 = FStar_Syntax_Print.term_to_string sol in - let uu___8 = FStar_Syntax_Print.term_to_string t in + let uu___7 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term sol in + let uu___8 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in let uu___9 = FStar_TypeChecker_Core.print_error err in FStar_Compiler_Util.print5 "(%s) Core checking failed (%s) on term %s and type %s\n%s\n" @@ -505,7 +510,8 @@ let (proc_guard' : FStar_Tactics_Monad.mlog (fun uu___4 -> let uu___5 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Pushing guard (%s:%s) as SMT goal\n" @@ -523,7 +529,8 @@ let (proc_guard' : FStar_Tactics_Monad.mlog (fun uu___4 -> let uu___5 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Sending guard (%s:%s) to SMT Synchronously\n" @@ -768,11 +775,15 @@ let (tc_unifier_solved_implicits : if uu___3 then let uu___4 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar u.FStar_Syntax_Syntax.ctx_uvar_head in let uu___5 = - FStar_Syntax_Print.term_to_string sol in - let uu___6 = FStar_Syntax_Print.term_to_string g in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term sol in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term g in fail3 "Could not typecheck unifier solved implicit %s to %s since it produced a guard and guards were not allowed;guard is\n%s" uu___4 uu___5 uu___6 @@ -787,9 +798,12 @@ let (tc_unifier_solved_implicits : FStar_Tactics_Monad.ret ())) | FStar_Pervasives.Inr failed -> let uu___3 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar u.FStar_Syntax_Syntax.ctx_uvar_head in - let uu___4 = FStar_Syntax_Print.term_to_string sol in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term sol in let uu___5 = FStar_TypeChecker_Core.print_error failed in fail3 @@ -839,8 +853,12 @@ let (__do_unify_wflags : fun t2 -> if dbg then - (let uu___1 = FStar_Syntax_Print.term_to_string t1 in - let uu___2 = FStar_Syntax_Print.term_to_string t2 in + (let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t1 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t2 in FStar_Compiler_Util.print2 "%%%%%%%%do_unify %s =? %s\n" uu___1 uu___2) else (); @@ -882,9 +900,13 @@ let (__do_unify_wflags : (FStar_TypeChecker_Rel.guard_to_string env1) res in let uu___7 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + t1 in let uu___8 = - FStar_Syntax_Print.term_to_string t2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + t2 in FStar_Compiler_Util.print3 "%%%%%%%%do_unify (RESULT %s) %s =? %s\n" uu___6 uu___7 uu___8) @@ -926,8 +948,8 @@ let (__do_unify_wflags : let uu___8 = FStar_Errors_Msg.rendermsg msg in let uu___9 = - FStar_Compiler_Range_Ops.string_of_range - r in + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range r in FStar_Compiler_Util.print2 ">> do_unify error, (%s) at (%s)\n" uu___8 uu___9) @@ -1143,8 +1165,9 @@ let (solve : (fun uu___ -> let uu___1 = let uu___2 = FStar_Tactics_Types.goal_witness goal in - FStar_Syntax_Print.term_to_string uu___2 in - let uu___2 = FStar_Syntax_Print.term_to_string solution in + FStar_Class_Show.show FStar_Syntax_Print.showable_term uu___2 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term solution in FStar_Compiler_Util.print2 "solve %s := %s\n" uu___1 uu___2) (fun uu___ -> let uu___1 = trysolve goal solution in @@ -1282,7 +1305,8 @@ let (__tc : (fun ps -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string t in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print1 "Tac> __tc(%s)\n" uu___1) (fun uu___ -> let e1 = @@ -1429,7 +1453,8 @@ let (__tc_ghost : (fun ps -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string t in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print1 "Tac> __tc_ghost(%s)\n" uu___1) (fun uu___ -> let e1 = @@ -1686,7 +1711,8 @@ let (__tc_lax : (fun ps -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string t in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in let uu___2 = let uu___3 = FStar_TypeChecker_Env.all_binders e in FStar_Compiler_Effect.op_Bar_Greater uu___3 @@ -2455,7 +2481,8 @@ let (norm : (fun uu___1 -> let uu___2 = let uu___3 = FStar_Tactics_Types.goal_witness goal in - FStar_Syntax_Print.term_to_string uu___3 in + FStar_Class_Show.show FStar_Syntax_Print.showable_term + uu___3 in FStar_Compiler_Util.print1 "norm: witness = %s\n" uu___2) in FStar_Tactics_Monad.op_let_Bang uu___ (fun uu___1 -> @@ -2485,7 +2512,9 @@ let (norm_term_env : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.term_to_string t in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print1 "norm_term_env: t = %s\n" uu___3) in FStar_Tactics_Monad.op_let_Bang uu___1 @@ -2508,7 +2537,8 @@ let (norm_term_env : FStar_Tactics_Monad.if_verbose (fun uu___8 -> let uu___9 = - FStar_Syntax_Print.term_to_string t2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print1 "norm_term_env: t' = %s\n" uu___9) in FStar_Tactics_Monad.op_let_Bang uu___7 @@ -2592,7 +2622,9 @@ let (__exact_now : let uu___2 = FStar_Tactics_Monad.if_verbose (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string typ in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term typ in let uu___5 = let uu___6 = FStar_Tactics_Types.goal_env goal in FStar_TypeChecker_Rel.guard_to_string uu___6 @@ -2615,11 +2647,13 @@ let (__exact_now : FStar_Tactics_Monad.if_verbose (fun uu___7 -> let uu___8 = - FStar_Syntax_Print.term_to_string typ in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term typ in let uu___9 = let uu___10 = FStar_Tactics_Types.goal_type goal in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___10 in FStar_Compiler_Util.print2 "__exact_now: unifying %s and %s\n" @@ -2680,7 +2714,8 @@ let (t_exact : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.term_to_string tm in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term tm in FStar_Compiler_Util.print1 "t_exact: tm = %s\n" uu___3) in FStar_Tactics_Monad.op_let_Bang uu___1 (fun uu___2 -> @@ -2789,7 +2824,8 @@ let (try_unify_by_application : FStar_Tactics_Monad.if_verbose (fun uu___8 -> let uu___9 = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu uv in FStar_Compiler_Util.print1 "t_apply: generated uvar %s\n" @@ -2873,11 +2909,22 @@ let (t_apply : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Compiler_Util.string_of_bool uopt in - let uu___4 = FStar_Compiler_Util.string_of_bool only_match in + let uu___3 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) uopt in + let uu___4 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) only_match in let uu___5 = - FStar_Compiler_Util.string_of_bool tc_resolved_uvars1 in - let uu___6 = FStar_Syntax_Print.term_to_string tm in + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) + tc_resolved_uvars1 in + let uu___6 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + tm in FStar_Compiler_Util.print4 "t_apply: uopt %s, only_match %s, tc_resolved_uvars %s, tm = %s\n" uu___3 uu___4 uu___5 uu___6) in @@ -2900,7 +2947,8 @@ let (t_apply : FStar_Tactics_Monad.if_verbose (fun uu___7 -> let uu___8 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm1 in let uu___9 = FStar_Tactics_Printing.goal_to_string_verbose @@ -2909,7 +2957,8 @@ let (t_apply : FStar_TypeChecker_Env.print_gamma e.FStar_TypeChecker_Env.gamma in let uu___11 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term typ in let uu___12 = FStar_TypeChecker_Rel.guard_to_string @@ -2943,7 +2992,8 @@ let (t_apply : with | (t, uu___13, uu___14) -> - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t) uvs in FStar_Compiler_Util.print1 "t_apply: found args = %s\n" @@ -3122,7 +3172,9 @@ let (t_apply_lemma : let uu___2 = FStar_Tactics_Monad.if_verbose (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string tm in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm in FStar_Compiler_Util.print1 "apply_lemma: tm = %s\n" uu___4) in FStar_Tactics_Monad.op_let_Bang uu___2 @@ -3255,11 +3307,13 @@ let (t_apply_lemma : then let uu___20 = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu u in let uu___21 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm1 in FStar_Compiler_Util.print2 "Apply lemma created a new uvar %s while applying %s\n" @@ -3664,9 +3718,10 @@ let (rewrite : FStar_Syntax_Syntax.binder -> unit FStar_Tactics_Monad.tac) = let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.bv_to_string bv in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_bv bv in let uu___4 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_term bv.FStar_Syntax_Syntax.sort in FStar_Compiler_Util.print2 "+++Rewrite %s : %s\n" uu___3 uu___4) in @@ -4018,7 +4073,8 @@ let (clear : FStar_Syntax_Syntax.binder -> unit FStar_Tactics_Monad.tac) = let uu___ = FStar_Tactics_Monad.if_verbose (fun uu___1 -> - let uu___2 = FStar_Syntax_Print.binder_to_string b in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_binder b in let uu___3 = let uu___4 = let uu___5 = @@ -4027,7 +4083,9 @@ let (clear : FStar_Syntax_Syntax.binder -> unit FStar_Tactics_Monad.tac) = FStar_Compiler_Effect.op_Bar_Greater uu___5 FStar_Compiler_List.length in FStar_Compiler_Effect.op_Bar_Greater uu___4 - FStar_Compiler_Util.string_of_int in + (FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat)) in FStar_Compiler_Util.print2 "Clear of (%s), env has %s binders\n" uu___2 uu___3) in FStar_Tactics_Monad.op_let_Bang uu___ @@ -4048,7 +4106,9 @@ let (clear : FStar_Syntax_Syntax.binder -> unit FStar_Tactics_Monad.tac) = if uu___3 then let uu___4 = - let uu___5 = FStar_Syntax_Print.bv_to_string bv' in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_bv bv' in FStar_Compiler_Util.format1 "Cannot clear; binder present in the type of %s" uu___5 in @@ -4854,7 +4914,8 @@ let (unquote : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.term_to_string tm in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term tm in FStar_Compiler_Util.print1 "unquote: tm = %s\n" uu___3) in FStar_Tactics_Monad.op_let_Bang uu___1 (fun uu___2 -> @@ -4872,7 +4933,8 @@ let (unquote : FStar_Tactics_Monad.if_verbose (fun uu___6 -> let uu___7 = - FStar_Syntax_Print.term_to_string tm1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm1 in FStar_Compiler_Util.print1 "unquote: tm' = %s\n" uu___7) in FStar_Tactics_Monad.op_let_Bang uu___5 @@ -4881,7 +4943,8 @@ let (unquote : FStar_Tactics_Monad.if_verbose (fun uu___8 -> let uu___9 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term typ in FStar_Compiler_Util.print1 "unquote: typ = %s\n" uu___9) in @@ -5362,7 +5425,8 @@ let (change : FStar_Syntax_Syntax.typ -> unit FStar_Tactics_Monad.tac) = let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.term_to_string ty in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term ty in FStar_Compiler_Util.print1 "change: ty = %s\n" uu___3) in FStar_Tactics_Monad.op_let_Bang uu___1 (fun uu___2 -> @@ -5658,7 +5722,8 @@ let (t_destruct : = let uu___27 = - FStar_Ident.string_of_id + FStar_Class_Show.show + FStar_Ident.showable_ident ppname in Prims.op_Hat "a" @@ -6558,7 +6623,9 @@ let rec (inspect : ((let uu___4 = let uu___5 = let uu___6 = FStar_Syntax_Print.tag_of_term t2 in - let uu___7 = FStar_Syntax_Print.term_to_string t2 in + let uu___7 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t2 in FStar_Compiler_Util.format2 "inspect: outside of expected syntax (%s, %s)\n" uu___6 uu___7 in @@ -6980,7 +7047,7 @@ let (string_to_term : fun s -> let frag_of_text s1 = { - FStar_Parser_ParseIt.frag_fname = ""; + FStar_Parser_ParseIt.frag_fname = ""; FStar_Parser_ParseIt.frag_text = s1; FStar_Parser_ParseIt.frag_line = Prims.int_one; FStar_Parser_ParseIt.frag_col = Prims.int_zero @@ -7004,17 +7071,17 @@ let (string_to_term : | FStar_Errors.Error (uu___2, e1, uu___3, uu___4) -> let uu___5 = let uu___6 = FStar_Errors_Msg.rendermsg e1 in - Prims.op_Hat "string_of_term: " uu___6 in + Prims.op_Hat "string_to_term: " uu___6 in FStar_Tactics_Monad.fail uu___5 | uu___2 -> - FStar_Tactics_Monad.fail "string_of_term: Unknown error") + FStar_Tactics_Monad.fail "string_to_term: Unknown error") | FStar_Parser_ParseIt.ASTFragment uu___1 -> FStar_Tactics_Monad.fail - "string_of_term: expected a Term as a result, got an ASTFragment" + "string_to_term: expected a Term as a result, got an ASTFragment" | FStar_Parser_ParseIt.ParseError (uu___1, err, uu___2) -> let uu___3 = let uu___4 = FStar_Errors_Msg.rendermsg err in - Prims.op_Hat "string_of_term: got error " uu___4 in + Prims.op_Hat "string_to_term: got error " uu___4 in FStar_Tactics_Monad.fail uu___3 let (push_bv_dsenv : env -> @@ -7132,7 +7199,8 @@ let (push_bv_dsenv : let (term_to_string : FStar_Syntax_Syntax.term -> Prims.string FStar_Tactics_Monad.tac) = fun t -> - let s = FStar_Syntax_Print.term_to_string t in FStar_Tactics_Monad.ret s + let s = FStar_Class_Show.show FStar_Syntax_Print.showable_term t in + FStar_Tactics_Monad.ret s let (comp_to_string : FStar_Syntax_Syntax.comp -> Prims.string FStar_Tactics_Monad.tac) = fun c -> @@ -7140,7 +7208,7 @@ let (comp_to_string : let (range_to_string : FStar_Compiler_Range_Type.range -> Prims.string FStar_Tactics_Monad.tac) = fun r -> - let uu___ = FStar_Compiler_Range_Ops.string_of_range r in + let uu___ = FStar_Class_Show.show FStar_Compiler_Range_Ops.show_range r in FStar_Tactics_Monad.ret uu___ let (term_eq_old : FStar_Syntax_Syntax.term -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml index a123bb6d7d6..789a72cf4cd 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Interpreter.ml @@ -308,7 +308,9 @@ let unembed_tactic_0 : else "" in let uu___ = let uu___1 = - let uu___2 = FStar_Syntax_Print.term_to_string h_result in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + h_result in FStar_Compiler_Util.format2 "Tactic got stuck!\nReduction stopped at: %s%s" uu___2 maybe_admit_tip in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index 813deb45a67..1fd976c1060 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -56,7 +56,8 @@ let (core_check : (fun uu___4 -> let uu___5 = let uu___6 = FStar_TypeChecker_Env.get_range env in - FStar_Compiler_Range_Ops.string_of_range uu___6 in + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range uu___6 in let uu___6 = FStar_TypeChecker_Core.print_error_short err in let uu___7 = @@ -447,7 +448,9 @@ let (proc_guard_formula : | FStar_Tactics_Types.Drop -> ((let uu___1 = let uu___2 = - let uu___3 = FStar_Syntax_Print.term_to_string f in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.format1 "Tactics admitted guard <%s>\n\n" uu___3 in (FStar_Errors_Codes.Warning_TacAdmit, uu___2) in @@ -457,7 +460,9 @@ let (proc_guard_formula : | FStar_Tactics_Types.Goal -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string f in + let uu___1 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Making guard (%s:%s) into a goal\n" reason uu___1) @@ -470,7 +475,9 @@ let (proc_guard_formula : | FStar_Tactics_Types.SMT -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string f in + let uu___1 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Pushing guard (%s:%s) as SMT goal\n" reason uu___1) @@ -483,7 +490,9 @@ let (proc_guard_formula : | FStar_Tactics_Types.SMTSync -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string f in + let uu___1 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Sending guard (%s:%s) to SMT Synchronously\n" reason uu___1) @@ -506,7 +515,9 @@ let (proc_guard_formula : | FStar_Tactics_Types.Force -> FStar_Tactics_Monad.mlog (fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string f in + let uu___1 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print2 "Forcing guard (%s:%s)\n" reason uu___1) (fun uu___ -> @@ -546,7 +557,8 @@ let (proc_guard_formula : FStar_Tactics_Monad.mlog (fun uu___2 -> let uu___3 = - FStar_Syntax_Print.term_to_string f in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print1 "guard = %s\n" uu___3) (fun uu___2 -> @@ -782,7 +794,8 @@ let (tc_unifier_solved_implicits : if uu___3 then let uu___4 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar u.FStar_Syntax_Syntax.ctx_uvar_head in let uu___5 = FStar_Class_Show.show @@ -804,7 +817,8 @@ let (tc_unifier_solved_implicits : FStar_Tactics_Monad.ret ())) | FStar_Pervasives.Inr failed -> let uu___3 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar u.FStar_Syntax_Syntax.ctx_uvar_head in let uu___4 = FStar_Class_Show.show @@ -953,8 +967,8 @@ let (__do_unify_wflags : let uu___8 = FStar_Errors_Msg.rendermsg msg in let uu___9 = - FStar_Compiler_Range_Ops.string_of_range - r in + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range r in FStar_Compiler_Util.print2 ">> do_unify error, (%s) at (%s)\n" uu___8 uu___9) @@ -2310,7 +2324,9 @@ let (bv_to_binding : FStar_Syntax_Syntax.bv -> FStar_Reflection_V2_Data.binding) = fun bv -> let uu___ = FStar_BigInt.of_int_fs bv.FStar_Syntax_Syntax.index in - let uu___1 = FStar_Ident.string_of_id bv.FStar_Syntax_Syntax.ppname in + let uu___1 = + FStar_Class_Show.show FStar_Ident.showable_ident + bv.FStar_Syntax_Syntax.ppname in { FStar_Reflection_V2_Data.uniq1 = uu___; FStar_Reflection_V2_Data.sort3 = (bv.FStar_Syntax_Syntax.sort); @@ -2324,7 +2340,9 @@ let (binding_to_string : FStar_Reflection_V2_Data.binding -> Prims.string) = let uu___ = let uu___1 = let uu___2 = FStar_BigInt.to_int_fs b.FStar_Reflection_V2_Data.uniq1 in - FStar_Compiler_Util.string_of_int uu___2 in + FStar_Class_Show.show + (FStar_Class_Show.printableshow FStar_Class_Printable.printable_int) + uu___2 in Prims.op_Hat "#" uu___1 in Prims.op_Hat b.FStar_Reflection_V2_Data.ppname3 uu___ let (binding_to_bv : @@ -2874,7 +2892,8 @@ let (try_unify_by_application : FStar_Tactics_Monad.if_verbose (fun uu___8 -> let uu___9 = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu uv in FStar_Compiler_Util.print1 "t_apply: generated uvar %s\n" @@ -2958,10 +2977,19 @@ let (t_apply : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Compiler_Util.string_of_bool uopt in - let uu___4 = FStar_Compiler_Util.string_of_bool only_match in + let uu___3 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) uopt in + let uu___4 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) only_match in let uu___5 = - FStar_Compiler_Util.string_of_bool tc_resolved_uvars1 in + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) + tc_resolved_uvars1 in let uu___6 = FStar_Class_Show.show FStar_Syntax_Print.showable_term tm in @@ -3347,7 +3375,8 @@ let (t_apply_lemma : then let uu___20 = - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu u in let uu___21 = @@ -3759,7 +3788,8 @@ let (rewrite : let uu___1 = FStar_Tactics_Monad.if_verbose (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.bv_to_string bv in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_bv bv in let uu___4 = FStar_Class_Show.show FStar_Syntax_Print.showable_term bv.FStar_Syntax_Syntax.sort in @@ -4123,7 +4153,9 @@ let (clear : FStar_Compiler_Effect.op_Bar_Greater uu___5 FStar_Compiler_List.length in FStar_Compiler_Effect.op_Bar_Greater uu___4 - FStar_Compiler_Util.string_of_int in + (FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat)) in FStar_Compiler_Util.print2 "Clear of (%s), env has %s binders\n" uu___2 uu___3) in FStar_Tactics_Monad.op_let_Bang uu___ @@ -4144,7 +4176,9 @@ let (clear : if uu___3 then let uu___4 = - let uu___5 = FStar_Syntax_Print.bv_to_string bv' in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_bv bv' in FStar_Compiler_Util.format1 "Cannot clear; binder present in the type of %s" uu___5 in @@ -5755,7 +5789,8 @@ let (t_destruct : = let uu___27 = - FStar_Ident.string_of_id + FStar_Class_Show.show + FStar_Ident.showable_ident ppname in Prims.op_Hat "a" @@ -6636,17 +6671,17 @@ let (string_to_term : | FStar_Errors.Error (uu___2, e1, uu___3, uu___4) -> let uu___5 = let uu___6 = FStar_Errors_Msg.rendermsg e1 in - Prims.op_Hat "string_of_term: " uu___6 in + Prims.op_Hat "string_to_term: " uu___6 in FStar_Tactics_Monad.fail uu___5 | uu___2 -> - FStar_Tactics_Monad.fail "string_of_term: Unknown error") + FStar_Tactics_Monad.fail "string_to_term: Unknown error") | FStar_Parser_ParseIt.ASTFragment uu___1 -> FStar_Tactics_Monad.fail - "string_of_term: expected a Term as a result, got an ASTFragment" + "string_to_term: expected a Term as a result, got an ASTFragment" | FStar_Parser_ParseIt.ParseError (uu___1, err, uu___2) -> let uu___3 = let uu___4 = FStar_Errors_Msg.rendermsg err in - Prims.op_Hat "string_of_term: got error " uu___4 in + Prims.op_Hat "string_to_term: got error " uu___4 in FStar_Tactics_Monad.fail uu___3 let (push_bv_dsenv : env -> @@ -6805,7 +6840,7 @@ let (comp_to_doc : let (range_to_string : FStar_Compiler_Range_Type.range -> Prims.string FStar_Tactics_Monad.tac) = fun r -> - let uu___ = FStar_Compiler_Range_Ops.string_of_range r in + let uu___ = FStar_Class_Show.show FStar_Compiler_Range_Ops.show_range r in FStar_Tactics_Monad.ret uu___ let (term_eq_old : FStar_Syntax_Syntax.term -> @@ -7145,13 +7180,17 @@ let (refl_is_non_informative : FStar_TypeChecker_Env.set_range g t.FStar_Syntax_Syntax.pos in dbg_refl g1 (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string t in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.format1 "refl_is_non_informative: %s\n" uu___4); (let b = FStar_TypeChecker_Core.is_non_informative g1 t in dbg_refl g1 (fun uu___4 -> - let uu___5 = FStar_Compiler_Util.string_of_bool b in + let uu___5 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) b in FStar_Compiler_Util.format1 "refl_is_non_informative: returned %s" uu___5); if b @@ -7437,8 +7476,12 @@ let (refl_core_check_term_at_type : FStar_TypeChecker_Env.set_range g e.FStar_Syntax_Syntax.pos in dbg_refl g1 (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - let uu___5 = FStar_Syntax_Print.term_to_string t in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + e in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t in FStar_Compiler_Util.format2 "refl_core_check_term_at_type: term: %s, type: %s\n" uu___4 uu___5); @@ -7501,7 +7544,7 @@ let (refl_tc_term : dbg_refl g1 (fun uu___3 -> let uu___4 = - FStar_Compiler_Range_Ops.string_of_range + FStar_Class_Show.show FStar_Compiler_Range_Ops.show_range e.FStar_Syntax_Syntax.pos in let uu___5 = FStar_Class_Show.show FStar_Syntax_Print.showable_term e in @@ -7738,7 +7781,8 @@ let (refl_tc_term : let uu___6 = let uu___7 = let uu___8 = - FStar_Syntax_Print.term_to_string e1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e1 in FStar_Compiler_Util.format1 "Elaborated term has unresolved implicits: %s" uu___8 in @@ -7755,7 +7799,8 @@ let (refl_tc_term : dbg_refl g2 (fun uu___8 -> let uu___9 = - FStar_Syntax_Print.term_to_string e2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e2 in FStar_Compiler_Util.format1 "} finished tc with e = %s\n" uu___9); (let guards = FStar_Compiler_Util.mk_ref [] in @@ -7767,11 +7812,14 @@ let (refl_tc_term : FStar_TypeChecker_Env.get_range g3 in FStar_Compiler_Effect.op_Bar_Greater uu___11 - FStar_Compiler_Range_Ops.string_of_range in + (FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range) in let uu___11 = - FStar_Syntax_Print.term_to_string guard in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term guard in let uu___12 = - FStar_Compiler_Range_Ops.string_of_range + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range guard.FStar_Syntax_Syntax.pos in FStar_Compiler_Util.format3 "Got guard in Env@%s |- %s@%s\n" uu___10 @@ -7792,12 +7840,15 @@ let (refl_tc_term : (dbg_refl g2 (fun uu___10 -> let uu___11 = - FStar_Compiler_Range_Ops.string_of_range + FStar_Class_Show.show + FStar_Compiler_Range_Ops.show_range e2.FStar_Syntax_Syntax.pos in let uu___12 = - FStar_Syntax_Print.term_to_string e2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e2 in let uu___13 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in FStar_Compiler_Util.format3 "refl_tc_term@%s for %s computed type %s\n" uu___11 uu___12 uu___13); @@ -8261,7 +8312,9 @@ let (refl_instantiate_implicits : then let uu___6 = let uu___7 = - let uu___8 = FStar_Syntax_Print.term_to_string e1 in + let uu___8 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e1 in FStar_Compiler_Util.format1 "Elaborated term has unresolved univ uvars: %s" uu___8 in @@ -8277,7 +8330,9 @@ let (refl_instantiate_implicits : then let uu___8 = let uu___9 = - let uu___10 = FStar_Syntax_Print.term_to_string t in + let uu___10 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.format1 "Inferred type has unresolved univ uvars: %s" uu___10 in @@ -8325,9 +8380,11 @@ let (refl_instantiate_implicits : dbg_refl g3 (fun uu___10 -> let uu___11 = - FStar_Syntax_Print.term_to_string e2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e2 in let uu___12 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in FStar_Compiler_Util.format2 "} finished tc with e = %s and t = %s\n" uu___11 uu___12); @@ -8424,7 +8481,9 @@ let (refl_maybe_unfold_head : then (let uu___4 = let uu___5 = - let uu___6 = FStar_Syntax_Print.term_to_string e in + let uu___6 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + e in FStar_Compiler_Util.format1 "Could not unfold head: %s\n" uu___6 in (FStar_Errors_Codes.Fatal_UnexpectedTerm, uu___5) in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml index d2a329dc3a5..8666dbb5b71 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml @@ -2945,13 +2945,15 @@ let (report_implicits : let uu___2 = let uu___3 = let uu___4 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in let uu___5 = let uu___6 = FStar_Syntax_Util.ctx_uvar_typ imp.FStar_TypeChecker_Common.imp_uvar in - FStar_Syntax_Print.term_to_string uu___6 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___6 in FStar_Compiler_Util.format3 "Tactic left uninstantiated unification variable %s of type %s (reason = \"%s\")" uu___4 uu___5 @@ -2964,13 +2966,15 @@ let (report_implicits : let uu___2 = let uu___3 = let uu___4 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in let uu___5 = let uu___6 = FStar_Syntax_Util.ctx_uvar_typ imp.FStar_TypeChecker_Common.imp_uvar in - FStar_Syntax_Print.term_to_string uu___6 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___6 in FStar_Compiler_Util.format3 "Tactic left uninstantiated unification variable %s of type %s (reason = \"%s\")" uu___4 uu___5 @@ -2983,15 +2987,21 @@ let (report_implicits : let uu___2 = let uu___3 = let uu___4 = - FStar_Syntax_Print.uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_uvar (imp.FStar_TypeChecker_Common.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head in let uu___5 = let uu___6 = FStar_Syntax_Util.ctx_uvar_typ imp.FStar_TypeChecker_Common.imp_uvar in - FStar_Syntax_Print.term_to_string uu___6 in - let uu___6 = FStar_Syntax_Print.term_to_string tm in - let uu___7 = FStar_Syntax_Print.term_to_string ty in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___6 in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm in + let uu___7 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term ty in FStar_Compiler_Util.format4 "Tactic solved goal %s of type %s to %s : %s, but it has a non-trivial typing guard. Use gather_or_solve_explicit_guards_for_resolved_goals to inspect and prove these goals" uu___4 uu___5 uu___6 uu___7 in @@ -3295,9 +3305,13 @@ let run_tactic_on_ps' : (let uu___1 = FStar_Compiler_Effect.op_Bang tacdbg in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string tactic in + let uu___2 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tactic in let uu___3 = - FStar_Compiler_Util.string_of_bool + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) tactic_already_typed in FStar_Compiler_Util.print2 "Typechecking tactic: (%s) (already_typed: %s) {\n" @@ -3363,7 +3377,8 @@ let run_tactic_on_ps' : let uu___11 = FStar_Tactics_Types.goal_witness g1 in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___11 in FStar_Compiler_Util.print1 "Assigning irrelevant goal %s\n" @@ -3385,7 +3400,8 @@ let run_tactic_on_ps' : let uu___13 = FStar_Tactics_Types.goal_witness g1 in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___13 in FStar_Compiler_Util.format1 "Irrelevant tactic witness does not unify with (): %s" @@ -3399,7 +3415,8 @@ let run_tactic_on_ps' : let uu___8 = (FStar_Common.string_of_list ()) (fun imp -> - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_ctxu imp.FStar_TypeChecker_Common.imp_uvar) ps3.FStar_Tactics_Types.all_implicits in FStar_Compiler_Util.print1 @@ -3427,14 +3444,15 @@ let run_tactic_on_ps' : if uu___8 then let uu___9 = - FStar_Compiler_Util.string_of_int + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) (FStar_Compiler_List.length ps3.FStar_Tactics_Types.all_implicits) in let uu___10 = - (FStar_Common.string_of_list ()) - (fun imp -> - FStar_Syntax_Print.ctx_uvar_to_string - imp.FStar_TypeChecker_Common.imp_uvar) + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_TypeChecker_Common.show_implicit) ps3.FStar_Tactics_Types.all_implicits in FStar_Compiler_Util.print2 "Checked %s implicits (1): %s\n" uu___9 @@ -3448,14 +3466,15 @@ let run_tactic_on_ps' : if uu___9 then let uu___10 = - FStar_Compiler_Util.string_of_int + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_nat) (FStar_Compiler_List.length ps3.FStar_Tactics_Types.all_implicits) in let uu___11 = - (FStar_Common.string_of_list ()) - (fun imp -> - FStar_Syntax_Print.ctx_uvar_to_string - imp.FStar_TypeChecker_Common.imp_uvar) + FStar_Class_Show.show + (FStar_Class_Show.show_list + FStar_TypeChecker_Common.show_implicit) ps3.FStar_Tactics_Types.all_implicits in FStar_Compiler_Util.print2 "Checked %s implicits (2): %s\n" uu___10 @@ -3495,7 +3514,8 @@ let run_tactic_on_ps' : Prims.op_Hat "\"" (Prims.op_Hat s "\"") | FStar_Tactics_Common.EExn t -> let uu___6 = - FStar_Syntax_Print.term_to_string t in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in Prims.op_Hat "Uncaught exception: " uu___6 | e2 -> FStar_Compiler_Effect.raise e2 in let rng = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml index 9432d0164cc..5a3d27c0cb8 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Common.ml @@ -550,6 +550,13 @@ let (__proj__Mkimplicit__item__imp_range : fun projectee -> match projectee with | { imp_reason; imp_uvar; imp_tm; imp_range;_} -> imp_range +let (show_implicit : implicit FStar_Class_Show.showable) = + { + FStar_Class_Show.show = + (fun i -> + FStar_Class_Show.show FStar_Syntax_Print.showable_uvar + (i.imp_uvar).FStar_Syntax_Syntax.ctx_uvar_head) + } type implicits = implicit Prims.list let (implicits_to_string : implicits -> Prims.string) = fun imps ->