module FStar.Tactics.PatternMatching

fsdoc: no-summary-found

fsdoc: no-comment-found

let ((mustfail #a (t:Unidentified product: [unit] (Tac a)) (message:string)):(Tac unit)):match trytac t with (Some _)  -> fail message | None  -> ()

Ensure that tactic t fails. *

let ((exact_hyp (a:Type0) (h:binder)):(Tac unit)):let  hd = quote ((FStar.Squash.return_squash #a)) in exact (mk_app hd (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 (pack ((Tv_Var (bv_of_binder h)))) Q_Explicit)) (Prims.Nil )))

Use a hypothesis at type a to satisfy a goal at type squash a

let ((exact_hyp' (h:binder)):(Tac unit)):exact (pack ((Tv_Var (bv_of_binder h))))

Use a hypothesis h (of type a) to satisfy a goal at type a

let ((interp_pattern_aux (pat:pattern) (cur_bindings:bindings) (tm:term)):(Tac (match_res bindings))):admit (); let  (interp_any () cur_bindings tm) = return (Prims.Nil ) in let  (interp_var (v:varname) cur_bindings tm) = match List.Tot.assoc v cur_bindings with (Some tm')  -> if term_eq tm tm' then return cur_bindings else raise ((NonLinearMismatch ((FStar.Pervasives.Native.Mktuple3 v tm tm')))) | None  -> return ((Prims.Cons ((FStar.Pervasives.Native.Mktuple2 v tm)) cur_bindings)) in let  (interp_qn (qn:qn) cur_bindings tm) = match inspect tm with (Tv_FVar fv)  -> if =(fv_to_string fv, qn) then return cur_bindings else raise ((NameMismatch ((FStar.Pervasives.Native.Mktuple2 qn (fv_to_string fv))))) | _  -> raise ((SimpleMismatch ((FStar.Pervasives.Native.Mktuple2 pat tm)))) in let  (interp_type cur_bindings tm) = match inspect tm with (Tv_Type ())  -> return cur_bindings | _  -> raise ((SimpleMismatch ((FStar.Pervasives.Native.Mktuple2 pat tm)))) in let  (interp_app (p_hd:(p:pattern:{<<(p, pat)})) (p_arg:(p:pattern:{<<(p, pat)})) cur_bindings tm) = match inspect tm with (Tv_App hd (arg, _))  -> with_hd <- interp_pattern_aux p_hd cur_bindings hd; with_arg <- interp_pattern_aux p_arg with_hd arg; return with_arg | _  -> raise ((SimpleMismatch ((FStar.Pervasives.Native.Mktuple2 pat tm)))) in match pat with PAny  -> interp_any () cur_bindings tm | (PVar var)  -> interp_var var cur_bindings tm | (PQn qn)  -> interp_qn qn cur_bindings tm | PType  -> interp_type cur_bindings tm | (PApp p_hd p_arg)  -> interp_app p_hd p_arg cur_bindings tm | _  -> fail "?"

Match a pattern against a term. cur_bindings is a list of bindings collected while matching previous parts of the pattern. Returns a result in the exception monad. *

let ((interp_pattern (pat:pattern)):Unidentified product: [term] (Tac (match_res bindings))):(fun (tm:term) -> rev_bindings <- interp_pattern_aux pat (Prims.Nil ) tm; return (List.Tot.rev rev_bindings))

Match a pattern pat against a term. Returns a result in the exception monad. *

let ((match_term pat (tm:term)):(Tac bindings)):match interp_pattern pat (norm_term (Prims.Nil ) tm) with (Success bb)  -> bb | (Failure ex)  -> Tactics.fail (string_of_match_exception ex)

Match a term tm against a pattern pat. Raises an exception if the match fails. This is mostly useful for debugging: use mgw to capture matches. *

let ((assoc_varname_fail (#b:Type) (key:varname) (ls:list (*(varname, b)))):(Tac b)):match List.Tot.assoc key ls with None  -> fail (^("Not found: ", key)) | (Some x)  -> x

Find a varname in an association list; fail if it can't be found. *

let ((solve_mp_for_single_hyp #a (name:varname) (pat:pattern) (hypotheses:list hypothesis) (body:Unidentified product: [matching_solution] (Tac a)) (part_sol:matching_solution)):(Tac a)):match hypotheses with []  -> fail #a "No matching hypothesis" | (Prims.Cons h hs)  -> or_else ((fun () -> match interp_pattern_aux pat part_sol.ms_vars (type_of_binder h) with (Failure ex)  -> fail (^("Failed to match hyp: ", (string_of_match_exception ex))) | (Success bindings)  -> let  ms_hyps = (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 name h)) part_sol.ms_hyps) in body ({part_sol with ms_vars=bindings ms_hyps=ms_hyps}))) ((fun () -> solve_mp_for_single_hyp name pat hs body part_sol))

Scan hypotheses for a match for pat that lets body succeed.

name is used to refer to the hypothesis matched in the final solution. part_sol includes bindings gathered while matching previous solutions. *

let ((solve_mp_for_hyps #a (mp_hyps:list (*(varname, pattern))) (hypotheses:list hypothesis) (body:Unidentified product: [matching_solution] (Tac a)) (partial_solution:matching_solution)):(Tac a)):match mp_hyps with []  -> body partial_solution | (Prims.Cons (name, pat) pats)  -> solve_mp_for_single_hyp name pat hypotheses (solve_mp_for_hyps pats hypotheses body) partial_solution

Scan hypotheses for matches for mp_hyps that lets body succeed. *

let ((solve_mp #a (problem:matching_problem) (hypotheses:binders) (goal:term) (body:Unidentified product: [matching_solution] (Tac a))):(Tac a)):let  goal_ps = match problem.mp_goal with None  -> {ms_vars=(Prims.Nil ) ms_hyps=(Prims.Nil )} | (Some pat)  -> match interp_pattern pat goal with (Failure ex)  -> fail (^("Failed to match goal: ", (string_of_match_exception ex))) | (Success bindings)  -> {ms_vars=bindings ms_hyps=(Prims.Nil )} in solve_mp_for_hyps #a problem.mp_hyps hypotheses body goal_ps

Solve a matching problem.

The solution returned is constructed to ensure that the continuation body succeeds: this implements the usual backtracking-match semantics. *

let ((pattern_of_term_ex tm):(Tac (match_res pattern))):match inspect tm with (Tv_Var bv)  -> return ((PVar (name_of_bv bv))) | (Tv_FVar fv)  -> let  qn = fv_to_string fv in return (if =(qn, any_qn) then PAny else (PQn qn)) | (Tv_Type ())  -> return PType | (Tv_App f (x, _))  -> let  is_any = match inspect f with (Tv_FVar fv)  -> =(fv_to_string fv, any_qn) | _  -> false in if is_any then return PAny else (fpat <- pattern_of_term_ex f; xpat <- pattern_of_term_ex x; return ((PApp fpat xpat))) | _  -> raise ((UnsupportedTermInPattern tm))

Compile a term tm into a pattern. *

let ((beta_reduce (tm:term)):(Tac term)):norm_term (Prims.Nil ) tm

β-reduce a term tm. This is useful to remove needles function applications introduced by F, like (fun a b c -> a) 1 2 3. 

let ((pattern_of_term tm):(Tac pattern)):match pattern_of_term_ex tm with (Success bb)  -> bb | (Failure ex)  -> Tactics.fail (string_of_match_exception ex)

Compile a term tm into a pattern. *

let ((binders_and_body_of_abs tm):(Tac (*(binders, term)))):match inspect tm with (Tv_Abs binder tm)  -> let  (binders, body) = binders_and_body_of_abs tm in (FStar.Pervasives.Native.Mktuple2 (Prims.Cons binder binders) body) | _  -> (FStar.Pervasives.Native.Mktuple2 (Prims.Nil ) tm)

Split an abstraction tm into a list of binders and a body. *

let ((matching_problem_of_abs (tm:term)):(Tac (*(matching_problem, abspat_continuation)))):let  (binders, body) = binders_and_body_of_abs (cleanup_abspat tm) in debug (^("Got binders: ", (String.concat ", " (map ((fun b -> (name_of_binder b : (Tac string)))) binders)))); let  classified_binders = map ((fun binder -> let  bv_name = name_of_binder binder in debug (^("Got binder: ", ^(bv_name, ^("; type is ", term_to_string (type_of_binder binder))))); let  (binder_kind, typ) = classify_abspat_binder binder in ((FStar.Pervasives.Native.Mktuple4 binder bv_name binder_kind typ)))) binders in let  problem = fold_left ((fun problem (binder, bv_name, binder_kind, typ) -> debug (^("Compiling binder ", ^(name_of_binder binder, ^(", classified as ", ^(string_of_abspat_binder_kind binder_kind, ^(", with type ", term_to_string typ)))))); match binder_kind with (ABKVar _)  -> {problem with mp_vars=(Prims.Cons bv_name problem.mp_vars)} | ABKHyp  -> {problem with mp_hyps=(Prims.Cons ((FStar.Pervasives.Native.Mktuple2 bv_name (pattern_of_term typ))) problem.mp_hyps)} | ABKGoal  -> {problem with mp_goal=(Some (pattern_of_term typ))})) ({mp_vars=(Prims.Nil ) mp_hyps=(Prims.Nil ) mp_goal=None}) classified_binders in let  continuation = let  ((abspat_argspec_of_binder xx):(Tac abspat_argspec)) = match xx with (binder, xx, binder_kind, yy)  -> {asa_name=binder asa_kind=binder_kind} in ((FStar.Pervasives.Native.Mktuple2 map abspat_argspec_of_binder classified_binders tm)) in let  mp = {mp_vars=List.rev #varname problem.mp_vars mp_hyps=List.rev #(*(varname, pattern)) problem.mp_hyps mp_goal=problem.mp_goal} in debug (^("Got matching problem: ", (string_of_matching_problem mp))); (FStar.Pervasives.Native.Mktuple2 mp continuation)

Parse a notation into a matching problem and a continuation.

Pattern-matching notations are of the form (fun binders… -> continuation), where binders are of one of the forms var …, hyp …, or goal …. var binders are typed holes to be used in other binders; hyp binders indicate a pattern to be matched against hypotheses; and goal binders match the goal.

A reduction phase is run to ensure that the pattern looks reasonable; it is needed because F* tends to infer arguments in β-expanded form.

The continuation returned can't directly be applied to a pattern-matching solution; see interp_abspat_continuation below for that. *

let ((arg_type_of_binder_kind binder_kind):(Tac term)):match binder_kind with (ABKVar typ)  -> typ | ABKHyp  -> (`(binder)) | ABKGoal  -> (`(unit))

Get the (quoted) type expected by a specific kind of abspat binder. *

let (locate_fn_of_binder_kind binder_kind):match binder_kind with (ABKVar _)  -> (`(ms_locate_var)) | ABKHyp  -> (`(ms_locate_hyp)) | ABKGoal  -> (`(ms_locate_unit))

Retrieve the function used to locate a value for a given abspat binder. *

let ((abspat_arg_of_abspat_argspec solution_term (argspec:abspat_argspec)):(Tac term)):let  loc_fn = locate_fn_of_binder_kind argspec.asa_kind in let  name_tm = pack ((Tv_Const ((C_String (name_of_binder argspec.asa_name))))) in let  locate_args = (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 arg_type_of_binder_kind argspec.asa_kind Q_Explicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 solution_term Q_Explicit)) (Prims.Cons ((FStar.Pervasives.Native.Mktuple2 name_tm Q_Explicit)) (Prims.Nil )))) in mk_app loc_fn locate_args

Construct a term fetching the value of an abspat argument from a quoted matching solution solution_term. *

let ((specialize_abspat_continuation' (continuation:abspat_continuation) (solution_term:term)):(Tac term)):let  (mk_arg argspec) = ((FStar.Pervasives.Native.Mktuple2 abspat_arg_of_abspat_argspec solution_term argspec Q_Explicit)) in let  (argspecs, body) = continuation in mk_app body (map mk_arg argspecs)

Specialize a continuation of type abspat_continuation. This constructs a fully applied version of continuation, but it requires a quoted solution to be passed in. *

let ((specialize_abspat_continuation (continuation:abspat_continuation)):(Tac term)):let  solution_binder = fresh_binder ((`(matching_solution))) in let  solution_term = pack ((Tv_Var (bv_of_binder solution_binder))) in let  applied = specialize_abspat_continuation' continuation solution_term in let  thunked = pack ((Tv_Abs solution_binder applied)) in debug (^("Specialized into ", (term_to_string thunked))); let  normalized = beta_reduce thunked in debug (^("… which reduces to ", (term_to_string normalized))); thunked

Specialize a continuation of type abspat_continuation. This yields a quoted function taking a matching solution and running its body with appropriate bindings. *

let ((interp_abspat_continuation (a:Type0) (continuation:abspat_continuation)):(Tac (Unidentified product: [matching_solution] (Tac a)))):let  applied = specialize_abspat_continuation continuation in unquote #(Unidentified product: [matching_solution] (Tac a)) applied

Interpret a continuation of type abspat_continuation. This yields a function taking a matching solution and running the body of the continuation with appropriate bindings. *

let ((interp_abspat #a (abspat:a)):(Tac (*(matching_problem, abspat_continuation)))):matching_problem_of_abs (quote (abspat))

Construct a matching problem from an abspat. *

let ((match_abspat #b #a (abspat:a) (k:Unidentified product: [abspat_continuation] (Tac (Unidentified product: [matching_solution] (Tac b))))):(Tac b)):let  goal = cur_goal () in let  hypotheses = binders_of_env (cur_env ()) in let  (problem, continuation) = interp_abspat abspat in admit (); solve_mp #matching_solution problem hypotheses goal (k continuation)

Construct an solve a matching problem. This higher-order function isn't very usable on its own — it's mostly a convenience function to avoid duplicating the problem-parsing code. *

let ((inspect_abspat_problem #a (abspat:a)):(Tac matching_problem)):fst (interp_abspat #a abspat)

Inspect the matching problem produced by parsing an abspat. *

let ((inspect_abspat_solution #a (abspat:a)):(Tac matching_solution)):match_abspat abspat ((fun _ -> (((fun solution -> solution)) : (Tac _))))

Inspect the matching solution produced by parsing and solving an abspat. *

let ((gpm #b #a (abspat:a) ()):(Tac b)):let  (continuation, solution) = match_abspat abspat tpair in interp_abspat_continuation b continuation solution

Solve a greedy pattern-matching problem and run its continuation. This if for pattern-matching problems in the Tac effect. *

let ((pm #b #a (abspat:a)):(Tac b)):match_abspat abspat (interp_abspat_continuation b)

Solve a greedy pattern-matching problem and run its continuation. This if for pattern-matching problems in the Tac effect. *