helm/ocaml/cic_disambiguation/ast.mli

   1
   2   (* when an 'ident option is None, the default is to apply the tactic
   3   to the current goal *)
   4
   5 type reduction_kind = [ `Reduce | `Simpl | `Whd ]
   6
   7 type 'term pattern =
   8   | Pattern of 'term
   9
  10 type location = int * int
  11
  12 type ('term, 'ident) tactic =
  13   | LocatedTactic of location * ('term, 'ident) tactic
  14
  15   | Absurd
  16   | Apply of 'term
  17   | Assumption
  18   | Change of 'term * 'term * 'ident option (* what, with what, where *)
  19   | Change_pattern of 'term pattern * 'term * 'ident option
  20       (* what, with what, where *)
  21   | Contradiction
  22   | Cut of 'term
  23   | Decompose of 'ident * 'ident list (* which hypothesis, which principles *)
  24   | Discriminate of 'ident
  25   | Elim of 'term * 'term option (* what to elim, which principle to use *)
  26   | ElimType of 'term
  27   | Exact of 'term
  28   | Exists
  29   | Fold of reduction_kind * 'term
  30   | Fourier
  31   | Injection of 'ident
  32   | Intros of int option
  33   | Left
  34   | LetIn of 'term * 'ident
  35   | Named_intros of 'ident list
  36   | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *)
  37   | Reflexivity
  38   | Replace of 'term * 'term (* what, with what *)
  39   | Replace_pattern of 'term pattern * 'term
  40   | RewriteLeft of 'term * 'ident option
  41   | RewriteRight of 'term * 'ident option
  42   | Right
  43   | Ring
  44   | Split
  45   | Symmetry
  46   | Transitivity of 'term
  47
  48 type 'tactic tactical =
  49   | LocatedTactical of location * 'tactic tactical
  50
  51   | Fail
  52   | For of int * 'tactic tactical
  53   | IdTac
  54   | Repeat of 'tactic tactical
  55   | Seq of 'tactic tactical list (* sequential composition *)
  56   | Tactic of 'tactic
  57   | Then of 'tactic tactical * 'tactic tactical list
  58   | Tries of 'tactic tactical list
  59       (* try a sequence of tacticals until one succeeds, fail otherwise *)
  60   | Try of 'tactic tactical (* try a tactical and mask failures *)
  61
  62 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
  63 type induction_kind = [ `Inductive | `CoInductive ]
  64 type sort_kind = [ `Prop | `Set | `Type | `CProp ]
  65
  66 type case_pattern = string list
  67
  68 type term =
  69   | LocatedTerm of location * term
  70
  71   | Appl of term list
  72   | Appl_symbol of string * int * term list (* literal, args, instance *)
  73   | Binder of binder_kind * Cic.name * term option * term
  74       (* kind, name, type, body *)
  75   | Case of term * string * term option * (case_pattern * term) list
  76     (* what to match, inductive type, out type, <pattern,action> list *)
  77   | LetIn of string * term * term  (* name, body, where *)
  78   | LetRec of induction_kind * (string * term * term option * int) list * term
  79       (* (name, body, type, decreasing argument) list, where *)
  80   | Ident of string * subst list  (* literal, substitutions *)
  81   | Meta of int * meta_subst list
  82   | Num of string * int (* literal, instance *)
  83   | Sort of sort_kind
  84
  85 and meta_subst = term option
  86 and subst = string * term
  87
  88 (*
  89 type cexpr =
  90   | Symbol of string option * string * (subst option) * string option
  91                                      (* h:xref, name, subst, definitionURL *)
  92   | LocalVar of string option * string        (* h:xref, name *)
  93   | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
  94   | Num of string option * string             (* h:xref, value *)
  95   | Appl of string option * cexpr list        (* h:xref, args *)
  96   | Binder of string option *string * decl * cexpr
  97                                        (* h:xref, name, decl, body *)
  98   | Letin of string option * def * cexpr          (* h:xref, def, body *)
  99   | Letrec of string option * def list * cexpr    (* h:xref, def list, body *)
 100   | Case of string option * cexpr * ((string * cexpr) list)
 101                                (* h:xref, case_expr, named-pattern list *)
 102 and
 103   decl = string * cexpr               (* name, type *)
 104 and
 105   def = string * cexpr               (* name, body *)
 106 and
 107   subst = (UriManager.uri * cexpr) list
 108 and
 109   meta_subst = cexpr option list
 110 *)
 111