val repeat' (#a: _) (f: (unit -> Tac a)) : Tac unit
let repeat' #a (f: unit -> Tac a) : Tac unit =
  let _ = repeat f in ()
val repeat' (#a: _) (f: (unit -> Tac a)) : Tac unit
let repeat' #a (f: (unit -> Tac a)) : Tac unit =
let _ = repeat f in
()
FStar.Tactics.PatternMatching.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Squash.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked
FStar.Tactics.PatternMatching.fst
Prims.unit Prims.list FStar.Tactics.V2.Derived.repeat
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
/// ==========================
///  Pattern-matching tactics
/// ==========================
///
/// :Author: Clément Pit-Claudel
/// :Contact: clement.pitclaudel@live.com
/// :Date: 2017-10-13

module FStar.Tactics.PatternMatching

open FStar.Tactics.V2

/// Contents
/// ========
///
///  1  Contents
///  2  Motivation
///  3  Some utility functions
///  4  Pattern types
///  5  Pattern matching exceptions
///    5.1  Types of exceptions
///    5.2  The exception monad
///    5.3  Liftings
///  6  Pattern interpretation
///  7  Pattern-matching problems
///    7.1  Definitions
///    7.2  Resolution
///  8  A DSL for pattern-matching
///    8.1  Pattern notations
///    8.2  Problem notations
///    8.3  Continuations
///  9  Putting it all together
/// 10  Examples
///   10.1  Simple examples
///   10.2  A real-life example
/// 11  Possible extensions
/// 12  Notes
///
/// Motivation
/// ==========
///
/// Suppose you have a goal of the form ``squash (a == b)``.  How do you capture
/// `a` and `b` for further inspection?
///
/// Here's a basic (but cumbersome!) implementation:

let fetch_eq_side () : Tac (term * term) =
  let g = cur_goal () in
  match inspect g with
  | Tv_App squash (g, _) ->
    (match inspect squash with
     | Tv_UInst squash _
     | Tv_FVar squash ->
       if fv_to_string squash = flatten_name squash_qn then
         (match inspect g with
          | Tv_App eq_type_x (y, _) ->
            (match inspect eq_type_x with
             | Tv_App eq_type (x, _) ->
               (match inspect eq_type with
                | Tv_App eq (typ, _) ->
                  (match inspect eq with
                   | Tv_UInst eq _
                   | Tv_FVar eq ->
                     if fv_to_string eq = flatten_name eq2_qn then
                       (x, y)
                     else fail "not an equality"
                   | _ -> fail "not an app2 of fvar: ")
                | _ -> fail "not an app3")
             | _ -> fail "not an app2")
          | _ -> fail "not an app under squash")
       else fail "not a squash"
     | _ -> fail "not an app of fvar at top level")
  | _ -> fail "not an app at top level"

/// …and here's how you could use it:

(* let _ = *)
(*   assert_by_tactic (1 + 1 == 2) *)
(*     (fun () -> let l, r = fetch_eq_side () in *)
(*                print (term_to_string l ^ " / " ^ term_to_string r)) *)

/// This file defines pattern-matching primitives that let you write the same
/// thing like this…
///
/// .. code:: fstar
///
///    let fetch_eq_side' #a () : Tac (term * term) =
///      gpm (fun (left right: a) (g: pm_goal (squash (left == right))) ->
///             (quote left, quote right) <: Tac (term * term))
///
///    let _ =
///      assert_by_tactic (1 + 1 == 2)
///        (fun () -> let l, r = fetch_eq_side' #int () in
///                   print (term_to_string l ^ " / " ^ term_to_string r))
///
/// …or, more succinctly, like this:
///
/// .. code:: fstar
///
///    let _ =
///      assert_by_tactic (1 + 1 == 2)
///        (gpm (fun (left right: int) (g: pm_goal (squash (left == right))) ->
///                let l, r = quote left, quote right in
///                print (term_to_string l ^ " / " ^ term_to_string r) <: Tac unit))


/// Some utility functions
/// ======================
///
/// (Skip over this part on a quick read — these are just convenience functions)


(** Ensure that tactic `t` fails. **)
let mustfail #a (t: unit -> Tac a) (message: string) : Tac unit =
    match trytac t with
    | Some _ -> fail message
    | None -> ()

/// The following two tactics are needed because of issues with the ``Tac``
/// effect.

let implies_intro' () : Tac unit =
  let _ = implies_intro () in ()
val repeat' (#a: _) (f: (unit -> Tac a)) : Tac unit
f: (_: Prims.unit -> FStar.Tactics.Effect.Tac a) -> FStar.Tactics.Effect.Tac Prims.unit