vernac_types.py

# Python classes corresponding to OCaml datatypes
# They are used to generate the CFG of the S-expressions, see gallina.py
from collections import OrderedDict
import re


class Type:
    'Abstract class for Ocaml types'
    cache = {}

    def __new__(cls, *args):
        if len(args) == 0:
            nonterminal = cls.__name__.lower()
        else:
            nonterminal = (cls.__name__ + '___' + '____'.join([p.nonterminal for p in args])).lower()
        if hasattr(cls, 'inline') and cls.inline == True:
            nonterminal = '_' + nonterminal

        if nonterminal in Type.cache:
            t = Type.cache[nonterminal]
            t.initialized = True
            return t
        else:
            t = super().__new__(cls)
            t.initialized = False
            t.nonterminal = nonterminal
            Type.cache[nonterminal] = t
            return t

    def parsing_rules(self):
        'return a list of strings (production rules) and a list of symbols (dependencies)'
        raise NotImplementedError

    def to_ebnf(self, recursive=False, skip_symbols=None):
        if skip_symbols is None:
            skip_symbols = set()
        rules, dependencies = self.parsing_rules()
        ebnf = self.nonterminal + ' : ' + ('\n ' + ' ' * len(self.nonterminal) + '| ').join(rules)
        skip_symbols.add('constr__constr')
        if recursive:
            for t in dependencies:
                if not t.nonterminal in skip_symbols:
                    skip_symbols.add(t.nonterminal)
                    ebnf += '\n\n' + t.to_ebnf(True, skip_symbols)       
        return ebnf

    def is_alias_for(self, cls):
        return isinstance(self, cls)
        

class AliasType(Type):

    def __init__(self):
        self.nonterminal = self.alias.nonterminal

    def is_alias_for(self, cls):
        if isinstance(self, cls):
            return True
        else:
            return self.alias.is_alias_for(cls)

    def parsing_rules(self):
        return self.alias.parsing_rules()


class UnimplementedType(Type):

    def parsing_rules(self):
        raise ValueError(self.__class__.__name__ + " unimplemented")


# built-in types

class Int(Type):
    def parsing_rules(self):
        return ['SIGNED_INT'], []


class String(Type):
    def parsing_rules(self):
        return ['ESCAPED_STRING', 'STRING_INNER*'], []


class Bool(Type):
    def parsing_rules(self):
        return ['"true"', '"false"'], []


class Tuple(Type):
    inline = True

    def __init__(self, *args):
        self.types = args

    def parsing_rules(self):
        return ['"(" %s ")"' % ' '.join([e.nonterminal for e in self.types])], self.types


class List(Type):
    inline = True

    def __init__(self, t):
        assert isinstance(t, Type)
        self.t = t

    def parsing_rules(self):
        return ['"(" %s* ")"' % self.t.nonterminal], [self.t]


class Array(Type):
    inline = True

    def __init__(self, t):
        assert isinstance(t, Type)
        self.t = t

    def parsing_rules(self):
        return ['"(" %s* ")"' % self.t.nonterminal], [self.t]


class NonEmptyList(Type):
    def __init__(self, t):
        assert isinstance(t, Type)
        self.t = t

    def parsing_rules(self):
        return ['"(" %s+ ")"' % self.t.nonterminal], [self.t]


class Record(Type):

    def parsing_rules(self):
        return ['"(" %s ")"' % ' '.join(['"(" /%s/ %s ")"' % (k, v.nonterminal) 
                                            for k, v in self.fields.items()])], \
                [v for v in self.fields.values()]


class Variant(Type):

    def parsing_rules(self):
        rules = []
        dependencies = []
        for name, arg_type in self.constructors.items():
            if arg_type is None:
                rules.append('"%s"    -> constructor_%s' % (name, name.lower()))
                continue
            elif isinstance(arg_type, Tuple):
                args = ' '.join([t.nonterminal for t in arg_type.types])
                dependencies.extend(arg_type.types)
            else:
                args = arg_type.nonterminal
                dependencies.append(arg_type)
            rules.append('"(" "%s" %s ")"    -> constructor_%s' % (name, args, name.lower()))
        return rules, dependencies


class Option(Type):
    inline = True

    def __init__(self, t):
        assert isinstance(t, Type)
        self.t = t

    def parsing_rules(self):
        return ['"(" %s? ")"' % self.t.nonterminal], [self.t]


# Coq types

class Univ__Universe__t(AliasType):
    '''
    type t = Level.t * int
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_univ.ml: type _t = (Level.t * int) list'
        self.alias = List(Tuple(Univ__Level__t(), Int()))


class Sorts__t(Variant):
    '''
    type t =
    | Prop
    | Set
    | Type of Univ.Universe.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Prop': None,
            'Set': None,
            'Type': Univ__Universe__t(),
        })
    

class Univ__Level__t(Variant):
    '''
    type t = { 
        hash : int;
        data : RawLevel.t }
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_univ.ml: type _level = ULevel of int'
        self.constructors = OrderedDict({
            'ULevel': Int(),
        })


class Univ__Instance__t(Variant):
    '''
    type t = Level.t array
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_univ.ml: type _instance = Instance of Level.t array'
        self.constructors = OrderedDict({
            'Instance': Array(Univ__Level__t()),
        })


class Names__KerPair__t(Variant):
    '''
    type t =
    | Same of KerName.t (** user = canonical *)
    | Dual of KerName.t * KerName.t (** user then canonical *)
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Same': Names__KerName__t(),
            'Dual': Tuple(Names__KerName__t(), Names__KerName__t()),
        })


class Names__Constant__t(Variant):
    '''
    module Constant = KerPair
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_names.ml: type _constant = Constant of ModPath.t * DirPath.t * Label.t'
        self.constructors = OrderedDict({
            'Constant': Tuple(Names__ModPath__t(), Names__DirPath__t(), Names__Label__t()),
        })


class Names__MutInd__t(Variant):
    '''
    module MutInd = KerPair
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_names.ml: type _mutind = Mutind of ModPath.t * DirPath.t * Label.t'
        self.constructors = OrderedDict({
            'Mutind': Tuple(Names__ModPath__t(), Names__DirPath__t(), Names__Label__t()),
        })


class Names__inductive(AliasType):
    '''
    (** Designation of a (particular) inductive type. *)
    type inductive = MutInd.t      (* the name of the inductive type *)
                    * int           (* the position of this inductive type
                                        within the block of mutually-recursive inductive types.
                                        BEWARE: indexing starts from 0. *)
    '''
    def __init__(self):
        self.alias = Tuple(Names__MutInd__t(), Int())


class Names__constructor(AliasType):
    '''
    (** Designation of a (particular) constructor of a (particular) inductive type. *)
    type constructor = inductive   (* designates the inductive type *)
                        * int         (* the index of the constructor
                                        BEWARE: indexing starts from 1. *)
    '''
    def __init__(self):
        self.alias = Tuple(Names__inductive(), Int())


class Constr__case_style(Variant):
    '''
    type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'LetStyle': None,
            'IfStyle': None,
            'LetPatternStyle': None,
            'MatchStyle': None,
            'RegularStyle': None,
        })


class Constr__case_printing(Record):
    '''    
    type case_printing =
    { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *)
        cstr_tags : bool list array; (* whether each pattern var of each constructor is a let-in (true) or not (false) *)
        style     : case_style }
    '''
    def __init__(self):
        self.fields = OrderedDict({
            'ind_tags': List(Bool()),
            'cstr_tags': Array(List(Bool())),
            'style': Constr__case_style(),
        })


class Constr__case_info(Record):
    '''
    type case_info =
    { ci_ind        : inductive;      (* inductive type to which belongs the value that is being matched *)
        ci_npar       : int;            (* number of parameters of the above inductive type *)
        ci_cstr_ndecls : int array;     (* For each constructor, the corresponding integer determines
                                        the number of values that can be bound in a match-construct.
                                        NOTE: parameters of the inductive type are therefore excluded from the count *)
        ci_cstr_nargs : int array;      (* for each constructor, the corresponding integers determines
                                        the number of values that can be applied to the constructor,
                                        in addition to the parameters of the related inductive type
                                        NOTE: "lets" are therefore excluded from the count
                                        NOTE: parameters of the inductive type are also excluded from the count *)
        ci_pp_info    : case_printing   (* not interpreted by the kernel *)
    }
    '''
    def __init__(self):
        self.fields = OrderedDict({
            'ci_ind': Names__inductive(),
            'ci_npar': Int(),
            'ci_cstr_ndecls': Array(Int()),
            'ci_cstr_nargs': Array(Int()),
            'ci_pp_info': Constr__case_printing(),
        })


class Evar__t(Variant):
    '''
    type t = int
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_evar.ml: type _evar = Ser_Evar of int [@@deriving sexp]'
        self.constructors = OrderedDict({
            'Ser_Evar': Int(),
        })


class Constr__existential_key(AliasType):
    '''
    type existential_key = Evar.t
    '''
    def __init__(self):
        self.alias = Evar__t()


class Constr__pexistential(AliasType):
    '''
    type 'constr pexistential = existential_key * 'constr array
    '''
    def __init__(self, constr):
        self.constr = constr
        self.alias = Tuple(Constr__existential_key(), Array(self.constr))
        

class Constr__prec_declaration(AliasType):
    '''
    type ('constr, 'types) prec_declaration =
        Name.t array * 'types array * 'constr array
    '''
    def __init__(self, constr, types):
        self.constr = constr
        self.types = types
        self.alias = Tuple(Array(Names__Name__t()), Array(self.types), Array(self.constr))


class Constr__pfixpoint(AliasType):
    '''
    type ('constr, 'types) pfixpoint =
        (int array * int) * ('constr, 'types) prec_declaration
    '''
    def __init__(self, constr, types):
        self.constr = constr
        self.types = types
        self.alias = Tuple(Tuple(Array(Int()), Int()), Constr__prec_declaration(self.constr, self.types))


class Constr__pcofixpoint(AliasType):
    '''
    type ('constr, 'types) pcofixpoint =
        int * ('constr, 'types) prec_declaration 
    '''
    def __init__(self, constr, types):
        self.constr = constr
        self.types = types
        self.alias = Tuple(Int(), Constr__prec_declaration(self.constr, self.types))


class Names__Projection__t(Variant):
    '''
    type t =
      { proj_ind : inductive;
        proj_npars : int;
        proj_arg : int;
        proj_name : Label.t; }
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_names.ml: type _projection = Projection of Constant.t * bool'
        self.constructors = OrderedDict({
            'Projection': Tuple(Names__Constant__t(), Bool()),
        })


class Constr__cast_kind(Variant):
    '''
    type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'VMcast': None,
            'NATIVEcast': None,
            'DEFAULTcast': None,
            'REVERTcast': None,
        })


class Constr__metavariable(AliasType):
    '''
    type metavariable = int
    '''
    def __init__(self):
        self.alias = Int()


class Constr__kind_of_term(Variant):
    '''
    type ('constr, 'types, 'sort, 'univs) kind_of_term =
    | Rel       of int
    | Var       of Id.t
    | Meta      of metavariable
    | Evar      of 'constr pexistential
    | Sort      of 'sort
    | Cast      of 'constr * cast_kind * 'types
    | Prod      of Name.t * 'types * 'types
    | Lambda    of Name.t * 'types * 'constr
    | LetIn     of Name.t * 'constr * 'types * 'constr
    | App       of 'constr * 'constr array
    | Const     of (Constant.t * 'univs)
    | Ind       of (inductive * 'univs)
    | Construct of (constructor * 'univs)
    | Case      of case_info * 'constr * 'constr * 'constr array
    | Fix       of ('constr, 'types) pfixpoint
    | CoFix     of ('constr, 'types) pcofixpoint
    | Proj      of Projection.t * 'constr
    '''
    def __init__(self, constr, types, sort, univs):
        self.constr = constr
        self.types = types
        self.sort = sort
        self.univs = univs
        self.constructors = OrderedDict({
            'Rel': Int(),
            'Var': Names__Id__t(),
            'Meta': Constr__metavariable(),
            'Evar': Constr__pexistential(self.constr),
            'Sort': self.sort,
            'Cast': Tuple(self.constr, Constr__cast_kind(), self.types),
            'Prod': Tuple(Names__Name__t(), self.types, self.types),
            'Lambda': Tuple(Names__Name__t(), self.types, self.constr),
            'LetIn': Tuple(Names__Name__t(), self.constr, self.types, self.constr),
            'App': Tuple(self.constr, Array(self.constr)),
            'Const': Tuple(Tuple(Names__Constant__t(), self.univs)),
            'Ind': Tuple(Tuple(Names__inductive(), self.univs)),
            'Construct': Tuple(Tuple(Names__constructor(), self.univs)),
            'Case': Tuple(Constr__case_info(), self.constr, self.constr, Array(self.constr)),
            'Fix': Constr__pfixpoint(self.constr, self.types),
            'CoFix': Constr__pcofixpoint(self.constr, self.types),
            'Proj': Tuple(Names__Projection__t(), self.constr),
        })
        

class Constr__constr(AliasType):
    '''
    type t = (t, t, Sorts.t, Instance.t) kind_of_term
    type constr = t
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = Constr__kind_of_term(Constr__constr(), Constr__constr(), Sorts__t(), Univ__Instance__t())


class Loc__source(Variant):
    constructors = OrderedDict({
        'InFile': String(),
        'ToplevelInput': None,
    })


class Loc__t(Record):
    '''
    type t = {
        fname : source; (** filename or toplevel input *)
        line_nb : int; (** start line number *)
        bol_pos : int; (** position of the beginning of start line *)
        line_nb_last : int; (** end line number *)
        bol_pos_last : int; (** position of the beginning of end line *)
        bp : int; (** start position *)
        ep : int; (** end position *)
    }
    '''
    def __init__(self):
        self.fields = OrderedDict({
            'bp': Int(),
            'ep': Int(),
        })


class Vernacexpr__vernac_flag(Variant):
    def __init__(self):
        self.constructors = OrderedDict({
            'VernacProgram': None,
            'VernacPolymorphic': Bool(),
            'VernacLocal': Bool(),
        })


class Genarg__rlevel(UnimplementedType):
    '''
    type rlevel = [ `rlevel ]
    '''
    pass


class Genarg__glevel(UnimplementedType):
    '''
    type glevel = [ `glevel ]
    '''
    pass


class Genarg__tlevel(UnimplementedType):
    '''
    type tlevel = [ `tlevel ]
    '''
    pass


class Genarg__ArgT__tag(Type):
    '''
    type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
    '''
    tags = ['auto_using',
            'bindings',
            'by_arg_tac',
            'casted_constr',
            'clause_dft_concl',
            'constr',
            'constr_with_bindings',
            'destruction_arg',
            'firstorder_using',
            'fun_ind_using',
            'glob_constr_with_bindings',
            'hintbases',
            'ident',
            'in_clause',
            'int_or_var',
            'intropattern',
            'ltac_info',
            'ltac_selector',
            'ltac_use_default',
            'natural',
            'orient',
            'preident',
            'quant_hyp',
            'rename',
            'rewstrategy',
            'ssrapplyarg',
            'ssrarg',
            'ssrcasearg',
            'ssrclauses',
            'ssrcongrarg',
            'ssrdoarg',
            'ssrexactarg',
            'ssrfwdid',
            'ssrhavefwdwbinders',
            'ssrhintarg',
            'ssrintrosarg',
            'ssrmovearg',
            'ssrposefwd',
            'ssrrpat',
            'ssrrwargs',
            'ssrseqarg',
            'ssrseqdir',
            'ssrsetfwd',
            'ssrsufffwd',
            'ssrtclarg',
            'ssrunlockargs',
            'tactic',
            'uconstr',
            'var',
            'with_names']
            
    def parsing_rules(self):
        'coq-serapi/serlib/ser_genarg.ml'
        return ['"%s"' % tag for tag in Genarg__ArgT__tag.tags], []


class Genarg__genarg_type(Variant):
    '''
    type (_, _, _) genarg_type =
    | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
    | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
    | OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
    | PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
        ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'ExtraArg': Genarg__ArgT__tag(),
            'ListArg': self,
            'OptArg': self,
            'PairArg': Tuple(self, self)
        })


class Locus__occurrences_gen(Variant):
    '''
    type 'a occurrences_gen =
    | AllOccurrences
    | AllOccurrencesBut of 'a list (** non-empty *)
    | NoOccurrences
    | OnlyOccurrences of 'a list (** non-empty *)
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'AllOccurrences': None,
            'AllOccurrencesBut': List(a),
            'NoOccurrences': None,
            'OnlyOccurrences': List(a),
        })



class Locus__occurrences_expr(AliasType):
    '''
    type occurrences_expr = (int or_var) occurrences_gen
    '''
    def __init__(self):
        self.alias = Locus__occurrences_gen(Misctypes__or_var(Int()))


class Locus__with_occurrences(AliasType):
    '''
    type 'a with_occurrences = occurrences_expr * 'a
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = Tuple(Locus__occurrences_expr(), a)


class Util__union(Variant):
    '''
    type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
    '''
    def __init__(self, a, b):
        assert isinstance(a, Type) and isinstance(b, Type)
        self.a = a
        self.b = b
        self.constructors = OrderedDict({
            'Inl': a,
            'Inr': b,
        })

class Genredexpr__glob_red_flag(Record):
    '''
    type 'a glob_red_flag = {
        rBeta : bool;
        rMatch : bool;
        rFix : bool;
        rCofix : bool;
        rZeta : bool;
        rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
        rConst : 'a list
    }
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.fields = OrderedDict({
            'rBeta' : Bool(),
            'rMatch' : Bool(),
            'rFix' : Bool(),
            'rCofix' : Bool(),
            'rZeta' : Bool(),
            'rDelta' : Bool(),
            'rConst' : List(a),
        })


class Genredexpr__red_expr_gen(Variant):
    '''
    type ('a,'b,'c) red_expr_gen =
    | Red of bool
    | Hnf
    | Simpl of 'b glob_red_flag * ('b,'c) Util.union Locus.with_occurrences option
    | Cbv of 'b glob_red_flag
    | Cbn of 'b glob_red_flag
    | Lazy of 'b glob_red_flag
    | Unfold of 'b Locus.with_occurrences list
    | Fold of 'a list
    | Pattern of 'a Locus.with_occurrences list
    | ExtraRedExpr of string
    | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
    | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
    '''
    def __init__(self, a, b, c):
        assert isinstance(a, Type) and isinstance(b, Type) and isinstance(c, Type)
        self.a = a
        self.b = b
        self.c = c
        self.constructors = OrderedDict({
            'Simpl': Tuple(Genredexpr__glob_red_flag(b), 
                           Option(Locus__with_occurrences(Util__union(b, c)))),
            'Unfold': List(Locus__with_occurrences(b)),
        })


class Locus__hyp_location_flag(Variant):
    '''
    type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'InHyp': None,
            'InHypTypeOnly': None,
            'InHypValueOnly': None,
        })


class Locus__hyp_location_expr(AliasType):
    '''
    type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = Tuple(Locus__with_occurrences(a), Locus__hyp_location_flag())


class Locus__clause_expr(Record):
    '''
    type 'id clause_expr =
        { onhyps : 'id hyp_location_expr list option;
            concl_occs : occurrences_expr }
    '''
    def __init__(self, id):
        assert isinstance(id, Type)
        self.id = id
        self.fields = OrderedDict({
            'onhyps': Option(List(Locus__hyp_location_expr(id))),
            'concl_occs': Locus__occurrences_expr(),
        })


# (** Possible arguments of a tactic definition *)

class Tacexpr__gen_tactic_arg(Variant):
    '''
    type 'a gen_tactic_arg =
    | TacGeneric     of 'lev generic_argument
    | ConstrMayEval  of ('trm,'cst,'pat) may_eval
    | Reference      of 'ref
    | TacCall    of ('ref * 'a gen_tactic_arg list) Loc.located
    | TacFreshId of string or_var list
    | Tacexp of 'tacexpr
    | TacPretype of 'trm
    | TacNumgoals

    constraint 'a = <
        term:'trm;
        dterm: 'dtrm;
        pattern:'pat;
        constant:'cst;
        reference:'ref;
        name:'nam;
        tacexpr:'tacexpr;
        level:'lev
    >
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'TacGeneric': Genarg__generic_argument(a.members['level']),
            'TacCall': Loc__located(Tuple(a.members['reference'], List(self))),
        })



class Tacexpr__advanced_flag(AliasType):
    '''
    type advanced_flag = bool  (* true = advanced         false = basic *)
    '''
    def __init__(self):
        self.alias = Bool()


class Tacexpr__evars_flag(AliasType):
    '''
    type evars_flag = bool     (* true = pose evars       false = fail on evars *)
    '''
    def __init__(self):
        self.alias = Bool()


class Tacexpr__clear_flag(AliasType):
    '''
    type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
    '''
    def __init__(self):
        self.alias = Option(Bool())


class Tacexpr__with_bindings_arg(AliasType):
    '''
    type 'a with_bindings_arg = clear_flag * 'a with_bindings
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = Tuple(Tacexpr__clear_flag(), Tactypes__with_bindings(a))


class Tacexpr__gen_atomic_tactic_expr(Variant):
    '''
    type 'a gen_atomic_tactic_expr =
    (* Basic tactics *)
    | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
    | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
        ('nam * 'dtrm intro_pattern_expr CAst.t option) option
    | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
    | TacCase of evars_flag * 'trm with_bindings_arg
    | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
    | TacMutualCofix of Id.t * (Id.t * 'trm) list
    | TacAssert of
        evars_flag * bool * 'tacexpr option option *
        'dtrm intro_pattern_expr CAst.t option * 'trm
    | TacGeneralize of ('trm with_occurrences * Name.t) list
    | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
        intro_pattern_naming_expr CAst.t option

    (* Derived basic tactics *)
    | TacInductionDestruct of
        rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list

    (* Conversion *)
    | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
    | TacChange of 'pat option * 'dtrm * 'nam clause_expr

    (* Equality and inversion *)
    | TacRewrite of evars_flag *
        (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
        (* spiwack: using ['dtrm] here is a small hack, may not be
            stable by a change in the representation of delayed
            terms. Because, in fact, it is the whole "with_bindings"
            which is delayed. But because the "t" level for ['dtrm] is
            uninterpreted, it works fine here too, and avoid more
            disruption of this file. *)
        'tacexpr option
    | TacInversion of ('trm,'dtrm,'nam) inversion_strength * quantified_hypothesis

    constraint 'a = <
        term:'trm;
        dterm: 'dtrm;
        pattern:'pat;
        constant:'cst;
        reference:'ref;
        name:'nam;
        tacexpr:'tacexpr;
        level:'lev
    >
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'TacIntroPattern': Tuple(Tacexpr__evars_flag(), List(CAst__t(Tactypes__intro_pattern_expr(a.members['dterm'])))),
            'TacApply': Tuple(Tacexpr__advanced_flag(), Tacexpr__evars_flag(), 
                              List(Tacexpr__with_bindings_arg(a.members['term'])), 
                              Option(Tuple(a.members['name'], Option(CAst__t(Tactypes__intro_pattern_expr(a.members['dterm'])))))),
            'TacCase': Tuple(Tacexpr__evars_flag(), Tacexpr__with_bindings_arg(a.members['term'])),
            'TacReduce': Tuple(Genredexpr__red_expr_gen(a.members['term'], a.members['constant'], a.members['pattern']), 
                               Locus__clause_expr(a.members['name'])),
        })
        

class Tacexpr__gen_tactic_expr(Variant):
    '''
    and 'a gen_tactic_expr =
    | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
    | TacThen of
        'a gen_tactic_expr *
        'a gen_tactic_expr
    | TacDispatch of
        'a gen_tactic_expr list
    | TacExtendTac of
        'a gen_tactic_expr array *
        'a gen_tactic_expr *
        'a gen_tactic_expr array
    | TacThens of
        'a gen_tactic_expr *
        'a gen_tactic_expr list
    | TacThens3parts of
        'a gen_tactic_expr *
        'a gen_tactic_expr array *
        'a gen_tactic_expr *
        'a gen_tactic_expr array
    | TacFirst of 'a gen_tactic_expr list
    | TacComplete of 'a gen_tactic_expr
    | TacSolve of 'a gen_tactic_expr list
    | TacTry of 'a gen_tactic_expr
    | TacOr of
        'a gen_tactic_expr *
        'a gen_tactic_expr
    | TacOnce of
        'a gen_tactic_expr
    | TacExactlyOnce of
        'a gen_tactic_expr
    | TacIfThenCatch of
        'a gen_tactic_expr *
        'a gen_tactic_expr *
        'a gen_tactic_expr
    | TacOrelse of
        'a gen_tactic_expr *
        'a gen_tactic_expr
    | TacDo of int or_var * 'a gen_tactic_expr
    | TacTimeout of int or_var * 'a gen_tactic_expr
    | TacTime of string option * 'a gen_tactic_expr
    | TacRepeat of 'a gen_tactic_expr
    | TacProgress of 'a gen_tactic_expr
    | TacShowHyps of 'a gen_tactic_expr
    | TacAbstract of
        'a gen_tactic_expr * Id.t option
    | TacId of 'n message_token list
    | TacFail of global_flag * int or_var * 'n message_token list
    | TacInfo of 'a gen_tactic_expr
    | TacLetIn of rec_flag *
        (lname * 'a gen_tactic_arg) list *
        'a gen_tactic_expr
    | TacMatch of lazy_flag *
        'a gen_tactic_expr *
        ('p,'a gen_tactic_expr) match_rule list
    | TacMatchGoal of lazy_flag * direction_flag *
        ('p,'a gen_tactic_expr) match_rule list
    | TacFun of 'a gen_tactic_fun_ast
    | TacArg of 'a gen_tactic_arg located
    | TacSelect of goal_selector * 'a gen_tactic_expr
    (* For ML extensions *)
    | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
    (* For syntax extensions *)
    | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located

    constraint 'a = <
        term:'t;
        dterm: 'dtrm;
        pattern:'p;
        constant:'c;
        reference:'r;
        name:'n;
        tacexpr:'tacexpr;
        level:'l
    >
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'TacAtom': Loc__located(Tacexpr__gen_atomic_tactic_expr(a)),
            'TacThen': Tuple(self, self),
            'TacTry': self,
            'TacAlias': Loc__located(Tuple(Names__KerName__t(), List(Tacexpr__gen_tactic_arg(a)))), 
            'TacArg': Loc__located(Tacexpr__gen_tactic_arg(a)),
        })

class Evar_kinds__t(Variant):
    '''
    type t =
    | ImplicitArg of global_reference * (int * Id.t option)
        * bool (** Force inference *)
    | BinderType of Name.t
    | NamedHole of Id.t (* coming from some ?[id] syntax *)
    | QuestionMark of obligation_definition_status * Name.t
    | CasesType of bool (* true = a subterm of the type *)
    | InternalHole
    | TomatchTypeParameter of inductive * int
    | GoalEvar
    | ImpossibleCase
    | MatchingVar of matching_var_kind
    | VarInstance of Id.t
    | SubEvar of Evar.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'BinderType': Names__Name__t(),
        })

class Decl_kinds__binding_kind(Variant):
    '''
    type binding_kind = Explicit | Implicit
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Explicit': None,
            'Implicit': None,
        })

class Constr__case_style(Variant):
    '''
    type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
    | RegularStyle (** infer printing form from number of constructor *)
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'LetStyle': None,
            'IfStyle': None,
            'LetPatternStyle': None,
            'MatchStyle': None,
            'RegularStyle': None,
        })

class Constrexpr__binder_kind(Variant):
    '''
    type binder_kind =
    | Default of binding_kind
    | Generalized of binding_kind * binding_kind * bool
        (** Inner binding, outer bindings, typeclass-specific flag
        for implicit generalization of superclasses *)
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Default': Decl_kinds__binding_kind(),
            'Generalized': Tuple(Decl_kinds__binding_kind(), Decl_kinds__binding_kind(), Bool()),
        })


class Constrexpr__proj_flag(AliasType):
    '''
    type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
    '''
    def __init__(self):
        self.alias = Option(Int())


class Constrexpr__instance_expr(AliasType):
    '''
    type instance_expr = Glob_term.glob_level list
    '''
    def __init__(self):
        self.alias = List(Glob_term__glob_level())


class Constrexpr__cases_pattern_expr_r(Variant):
    '''
    type cases_pattern_expr_r =
    | CPatAlias of cases_pattern_expr * lname
    | CPatCstr  of qualid
        * cases_pattern_expr list option * cases_pattern_expr list
    (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
    | CPatAtom of qualid option
    | CPatOr   of cases_pattern_expr list
    | CPatNotation of notation * cases_pattern_notation_substitution
        * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
                    (notation n applied with substitution l1)
                    applied to arguments l2 *)
    | CPatPrim   of prim_token
    | CPatRecord of (qualid * cases_pattern_expr) list
    | CPatDelimiters of string * cases_pattern_expr
    | CPatCast   of cases_pattern_expr * constr_expr
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'CPatAlias': Tuple(Constrexpr__cases_pattern_expr(), Names__lname()),
            'CPatCstr': Tuple(Libnames__qualid(), Option(List(Constrexpr__cases_pattern_expr())), List(Constrexpr__cases_pattern_expr())),
            'CPatAtom': Option(Libnames__qualid()),
            'CPatNotation': Tuple(Constrexpr__notation(), Constrexpr__cases_pattern_notation_substitution(), List(Constrexpr__cases_pattern_expr())),
            'CPatPrim': Constrexpr__prime_token(),
            'CPatRecord': List(Tuple(Libnames__qualid(), Constrexpr__cases_pattern_expr())),
            'CPatDelimiters': Tuple(String(), Constrexpr__cases_pattern_expr()),
        })


class Constrexpr__cases_pattern_expr(AliasType):
    '''
    and cases_pattern_expr = cases_pattern_expr_r CAst.t
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = CAst__t(Constrexpr__cases_pattern_expr_r())


class Constrexpr__cases_pattern_notation_substitution(AliasType):
    '''
    and cases_pattern_notation_substitution =
        cases_pattern_expr list *     (** for constr subterms *)
        cases_pattern_expr list list  (** for recursive notations *)
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = Tuple(List(Constrexpr__cases_pattern_expr()), List(List(Constrexpr__cases_pattern_expr())))


class Constrexpr__notation_key(AliasType):
    '''
    type notation_key = string
    '''
    inline = True

    def __init__(self):
        self.alias = String()

class Constrexpr__notation_entry_level(Variant):
    '''
    type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'InConstrEntrySomeLevel': None,
            'InCustomEntryLevel': Tuple(String(), Int()),
        })

class Constrexpr__notation(AliasType):
    '''
    type notation = notation_entry_level * notation_key
    '''
    def __init__(self):
        self.alias = Tuple(Constrexpr__notation_entry_level(), Constrexpr__notation_key())


class Constrexpr__explicitation(Variant):
    '''
    type explicitation =
    | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
    | ExplByName of Id.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'ExplByPos': Tuple(Int(), Option(Names__Id__t())),
            'ExplByName': Names__Id__t(),
        })


class Constrexpr__sign(AliasType):
    '''
    type sign = bool
    '''
    def __init__(self):
        self.alias = Bool()


class Constrexpr__raw_natural_number(AliasType):
    '''
    type raw_natural_number = string
    '''
    def __init__(self):
        self.alias = Int()


class Constrexpr__prime_token(Variant):
    '''
    type prim_token =
    | Numeral of raw_natural_number * sign
    | String of string
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Numeral': Tuple(Constrexpr__raw_natural_number(), Constrexpr__sign()),
            'String': String(),
        })


class Constrexpr__constr_expr_r(Variant):
    '''
    and constr_expr_r =
    | CRef     of qualid * instance_expr option
    | CFix     of lident * fix_expr list
    | CCoFix   of lident * cofix_expr list
    | CProdN   of local_binder_expr list * constr_expr
    | CLambdaN of local_binder_expr list * constr_expr
    | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
    | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
    | CApp     of (proj_flag * constr_expr) *
                    (constr_expr * explicitation CAst.t option) list
    | CRecord  of (qualid * constr_expr) list

    (* representation of the "let" and "match" constructs *)
    | CCases of Constr.case_style   (* determines whether this value represents "let" or "match" construct *)
                * constr_expr option  (* return-clause *)
                * case_expr list
                * branch_expr list    (* branches *)

    | CLetTuple of lname list * (lname option * constr_expr option) *
                    constr_expr * constr_expr
    | CIf of constr_expr * (lname option * constr_expr option)
            * constr_expr * constr_expr
    | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
    | CPatVar of Pattern.patvar
    | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
    | CSort   of Glob_term.glob_sort
    | CCast   of constr_expr * constr_expr Glob_term.cast_type
    | CNotation of notation * constr_notation_substitution
    | CGeneralization of binding_kind * abstraction_kind option * constr_expr
    | CPrim of prim_token
    | CDelimiters of string * constr_expr
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'CRef': Tuple(Libnames__qualid(), Option(Constrexpr__instance_expr())),
            'CFix': Tuple(Names__lident(), List(Constrexpr__fix_expr())),
            'CCoFix': Tuple(Names__lident(), List(Constrexpr__cofix_expr())), 
            'CProdN': Tuple(List(Constrexpr__local_binder_expr()), Constrexpr__constr_expr()),
            'CLambdaN': Tuple(List(Constrexpr__local_binder_expr()), Constrexpr__constr_expr()),
            'CLetIn': Tuple(Names__lname(), Constrexpr__constr_expr(), Option(Constrexpr__constr_expr()), Constrexpr__constr_expr()),
            'CAppExpl': Tuple(Tuple(Constrexpr__proj_flag(), Libnames__qualid(), Option(Constrexpr__instance_expr())), List(Constrexpr__constr_expr())),
            'CApp': Tuple(Tuple(Constrexpr__proj_flag(), Constrexpr__constr_expr()), List(Tuple(Constrexpr__constr_expr(), Option(CAst__t(Constrexpr__explicitation()))))),
            'CCases': Tuple(Constr__case_style(), Option(Constrexpr__constr_expr()), List(Constrexpr__case_expr()), List(Constrexpr__branch_expr())), 
            'CLetTuple': Tuple(List(Names__lname()), Tuple(Option(Names__lname()), Option(Constrexpr__constr_expr())), Constrexpr__constr_expr(), Constrexpr__constr_expr()),
            'CIf': Tuple(Constrexpr__constr_expr(), Tuple(Option(Names__lname()), Option(Constrexpr__constr_expr())), Constrexpr__constr_expr(), Constrexpr__constr_expr()),
            'CHole': Tuple(Option(Evar_kinds__t()), Namegen__intro_pattern_naming_expr(), Option(Genarg__raw_generic_argument())),
            'CEvar': Tuple(Glob_term__existential_name(), List(Tuple(Names__Id__t(), Constrexpr__constr_expr()))),
            'CSort': Glob_term__glob_sort(),
            'CCast': Tuple(Constrexpr__constr_expr(), Glob_term__cast_type(Constrexpr__constr_expr())),
            'CNotation': Tuple(Constrexpr__notation(), Constrexpr__constr_notation_substitution()),
            'CPrim': Constrexpr__prime_token(),
            'CDelimiters': Tuple(String(), Constrexpr__constr_expr()),
        })


class Constrexpr__constr_expr(AliasType):
    '''
    and constr_expr = constr_expr_r CAst.t
    '''
    inline = True

    def __init__(self):
        if self.initialized:
            return
        self.alias = CAst__t(Constrexpr__constr_expr_r())


class Constrexpr__case_expr(AliasType):
    '''
    and case_expr = constr_expr                 (* expression that is being matched *)
                    * lname option                (* as-clause *)
                    * cases_pattern_expr option   (* in-clause *)
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = Tuple(Constrexpr__constr_expr(), Option(Names__lname()), Option(Constrexpr__cases_pattern_expr()))


class Constrexpr__branch_expr(AliasType):
    '''
    and branch_expr =
        (cases_pattern_expr list list * constr_expr) CAst.t
    '''
    inline = True

    def __init__(self):
        if self.initialized:
            return
        self.alias = CAst__t(Tuple(List(List(Constrexpr__cases_pattern_expr())), Constrexpr__constr_expr()))

class Constrexpr__fix_expr(AliasType):
    '''
    and fix_expr =
        lident * (lident option * recursion_order_expr) *
        local_binder_expr list * constr_expr * constr_expr
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = Tuple(Names__lident(), Tuple(Option(Names__lident()), Constrexpr__recursion_order_expr()), List(Constrexpr__local_binder_expr()), Constrexpr__constr_expr(), Constrexpr__constr_expr())


class Constrexpr__cofix_expr(AliasType):
    '''
    and cofix_expr =
        lident * local_binder_expr list * constr_expr * constr_expr
    '''
    def __init__(self):
        if self.initialized:
            return
        self.alias = Tuple(Names__lident(), List(Constrexpr__local_binder_expr()), Constrexpr__constr_expr(), Constrexpr__constr_expr())


class Constrexpr__recursion_order_expr(Variant):
    '''
    and recursion_order_expr =
    | CStructRec
    | CWfRec of constr_expr
    | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'CStructRec': None,
            'CWfRec': Constrexpr__constr_expr(),
            'CMeasureRec': Tuple(Constrexpr__constr_expr(), Option(Constrexpr__constr_expr())),
        })


class Constrexpr__constr_pattern_expr(AliasType):
    '''
    type constr_pattern_expr = constr_expr
    '''
    def __init__(self):
        self.alias = Constrexpr__constr_expr()


class Constrexpr__local_binder_expr(Variant):
    '''
    and local_binder_expr =
    | CLocalAssum   of lname list * binder_kind * constr_expr
    | CLocalDef     of lname * constr_expr * constr_expr option
    | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
    '''
    def  __init__(self):
        self.constructors = OrderedDict({
            'CLocalAssum': Tuple(List(Names__lname()), Constrexpr__binder_kind(), Constrexpr__constr_expr()),
            'CLocalPattern': CAst__t(Tuple(Constrexpr__cases_pattern_expr(), Option(Constrexpr__constr_expr())))
        })

class Constrexpr__constr_notation_substitution(AliasType):
    '''
    and constr_notation_substitution =
        constr_expr list *      (** for constr subterms *)
        constr_expr list list * (** for recursive notations *)
        cases_pattern_expr list *   (** for binders *)
        local_binder_expr list list (** for binder lists (recursive notations) *)
    '''
    def __init__(self):
        self.alias = Tuple(List(Constrexpr__constr_expr()), 
                           List(List(Constrexpr__constr_expr())),
                           List(Constrexpr__cases_pattern_expr()),
                           List(List(Constrexpr__local_binder_expr())))


class Names__module_ident(AliasType):
    '''
    type module_ident = Id.t
    '''
    def __init__(self):
        self.alias = Names__Id__t()


class Names__DirPath__t(Variant):
    '''
    type t = module_ident list
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_names.ml: type _dirpath = DirPath of Id.t list'
        self.constructors = OrderedDict({
            'DirPath': List(Names__Id__t()),
        }) 
  

class Names__MBId__t(Variant):
    '''
    type t = int * Id.t * DirPath.t
    '''
    def __init__(self):
        'coq-serapi/serlib/ser_names.ml: type _mbid = Mbid of Id.t * DirPath.t'
        self.constructors = OrderedDict({
            'Mbid': Tuple(Names__Id__t(), Names__DirPath__t()),
        })


class Names__Label__t(AliasType):
    '''
    type t = Id.t
    '''
    def __init__(self):
        self.alias = Names__Id__t()


class Names__ModPath__t(Variant):
    '''
    type t =
    | MPfile of DirPath.t
    | MPbound of MBId.t
    | MPdot of t * Label.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'MPfile': Names__DirPath__t(),
            'MPbound': Names__MBId__t(),
            'MPdot': Tuple(self, Names__Label__t())
        })


class Names__KerName__t(Variant):
    '''
      type t = {
        canary : Canary.t;
        modpath : ModPath.t;
        dirpath : DirPath.t;
        knlabel : Label.t;
        mutable refhash : int;
        (** Lazily computed hash. If unset, it is set to negative values. *)
    }
    '''
    def __init__(self):
       'coq-serapi/serlib/ser_names.ml: type _kername = Kername of ModPath.t * DirPath.t * Label.t'
       self.constructors = OrderedDict({
           'Kername': Tuple(Names__ModPath__t(), 
                            Names__DirPath__t(),
                            Names__Label__t())
       })


class Libnames__full_path(Record):
    '''
    type full_path = {
        dirpath : DirPath.t ;
        basename : Id.t }
    '''
    def __init__(self):
        self.fields = OrderedDict({
            'dirpath': Names__DirPath__t(),
            'basename': Names__Id__t(),
        }) 


class Libnames__qualid_r(Variant):
    '''
    type qualid_r = full_path
    '''
    def __init__(self):
        '''
        coq-serapi/serlib/ser_libnames.ml: 
        type _qualid =
            Ser_Qualid of Names.DirPath.t * Names.Id.t
        [@@deriving sexp]
        '''
        self.constructors = OrderedDict({
            'Ser_Qualid': Tuple(Names__DirPath__t(), Names__Id__t()),
        })


class Libnames__qualid(AliasType):
    '''
    type qualid = qualid_r CAst.t
    '''
    inline = True

    def __init__(self):
        self.alias = CAst__t(Libnames__qualid_r())


class Libnames__reference_r(Variant):
    '''
    type reference_r =
    | Qualid of qualid
    | Ident of Id.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Qualid': Libnames__qualid(),
            'Ident': Names__Id__t(),
        })


class Libnames__reference(AliasType):
    '''
    type reference = reference_r CAst.t
    '''
    inline = True

    def __init__(self):
        self.alias = CAst__t(Libnames__reference_r())


class Tacexpr__r_trm(AliasType):
    '''
    type r_trm = constr_expr
    '''
    def __init__(self):
        self.alias = Constrexpr__constr_expr()


class Tacexpr__r_pat(AliasType):
    '''
    type r_pat = constr_pattern_expr
    '''
    def __init__(self):
        self.alias = Constrexpr__constr_pattern_expr()


class Tacexpr__r_cst(AliasType):
    '''
    type r_cst = reference or_by_notation
    '''
    def __init__(self):
        self.alias = Constrexpr__or_by_notation(Libnames__reference())


class Tacexpr__r_ref(AliasType):
    '''
    type r_ref = reference
    '''
    def __init__(self):
        self.alias = Libnames__reference()


class Tacexpr__r_nam(AliasType):
    '''
    type r_nam = lident
    '''
    def __init__(self):
        self.alias = Names__lident()


class Tacexpr__r_lev(AliasType):
    '''
    type r_lev = rlevel
    '''
    def __init__(self):
        self.alias = Genarg__rlevel()


class Tacexpr__r_dispatch(UnimplementedType):
    '''
    type r_dispatch =  <
        term:r_trm;
        dterm:r_trm;
        pattern:r_pat;
        constant:r_cst;
        reference:r_ref;
        name:r_nam;
        tacexpr:raw_tactic_expr;
        level:rlevel
    >
    '''
    def __init__(self):
        self.members = OrderedDict({
            'term': Tacexpr__r_trm(),
            'dterm': Tacexpr__r_trm(),
            'pattern': Tacexpr__r_pat(),
            'constant': Tacexpr__r_cst(),
            'reference': Tacexpr__r_ref(),
            'name': Tacexpr__r_nam(),
            'level': Tacexpr__r_lev(),
        })


class Tacexpr__raw_tactic_expr(AliasType):
    '''
    and raw_tactic_expr =
        r_dispatch gen_tactic_expr
    '''
    def __init__(self):
        self.alias = Tacexpr__gen_tactic_expr(Tacexpr__r_dispatch())


class Genarg__genarg_val(Type):
    '''
    type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
    '''
    def parsing_rules(self):
        raw_tacexpr = Tacexpr__raw_tactic_expr()
        ty = Genarg__genarg_type()
        list_val = NonEmptyList(self)
        opt_val = Option(self)
        pair_val = Tuple(self, self)
        return [
            list_val.nonterminal,
            opt_val.nonterminal,
            pair_val.nonterminal,
            '"(\\\"[XXX ser_gen]\\\" raw" %s ")"' % ty.nonterminal,  # default
            '"(\\\"[XXX ser_gen]\\\" glb" %s ")"' % ty.nonterminal,  # default
            '"(\\\"[XXX ser_gen]\\\" top" %s ")"' % ty.nonterminal,  # default
            Bool().nonterminal,
            Names__Id__t().nonterminal,
            raw_tacexpr.nonterminal,
        ], [list_val, opt_val, pair_val, raw_tacexpr, ty]


class Genarg__generic_argument(Variant):
    '''
    type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
    '''
    def __init__(self, l):
        assert isinstance(l, Type)
        self.l = l

    def parsing_rules(self):
        'coq-serapi/serlib/ser_genarg.ml'
        if self.l.is_alias_for(Genarg__rlevel):
            level = 'raw'
        elif self.l.is_alias_for(Genarg__glevel):
            level = 'glb'
        else:
            assert self.l.is_alias_for(Genarg__tlevel)
            level = 'top'
        ty = Genarg__genarg_type()
        t = Genarg__genarg_val()
        return ['"(GenArg" "%s" %s %s ")"' % (level, ty.nonterminal, t.nonterminal)], [ty, t]


class Genarg__raw_generic_argument(AliasType):
    '''
    type raw_generic_argument = rlevel generic_argument
    '''
    def __init__(self):
        self.alias = Genarg__generic_argument(Genarg__rlevel())


class Vernacexpr__section_subset_expr(Variant):
    '''
    type section_subset_expr =
    | SsEmpty
    | SsType
    | SsSingl of lident
    | SsCompl of section_subset_expr
    | SsUnion of section_subset_expr * section_subset_expr
    | SsSubstr of section_subset_expr * section_subset_expr
    | SsFwdClose of section_subset_expr
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'SsEmpty': None,
            'SsType': None,
            'SsSingl': Names__lident(),
            'SsCompl': self,
            'SsUnion': Tuple(self, self),
            'SsSubstr': Tuple(self, self),
            'SsFwdClose': self,
        })


class Vernacexpr__opacity_flag(Variant):
    '''
    type opacity_flag   = Opaque | Transparent
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Opaque': None,
            'Transparent': None,
        })
 

class Names__Id__t(Type):
    '''
    type t = string
    '''
    inline = True

    def parsing_rules(self):
        #'coq-serapi/serlib/ser_names.ml'
        #rules, dependencies = String().parsing_rules()
        #return ['"(Id" %s ")"' % r for r in rules], dependencies
        return ['"(Id" /[^\)]+/ ")"'], []


class Names__Name__t(Variant):
    '''
    type t = Anonymous     (** anonymous identifier *)
    | Name of Id.t  (** non-anonymous identifier *)
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Anonymous': None,
            'Name': Names__Id__t(),
        })


class Names__lident(AliasType):
    '''
    type lident = Id.t CAst.t
    '''
    inline = True

    def __init__(self):
        self.alias = CAst__t(Names__Id__t())


class Names__lname(AliasType):
    '''
    type lname = Name.t CAst.t
    '''
    inline = True

    def __init__(self):
        self.alias = CAst__t(Names__Name__t())


class Glob_term__existential_name(AliasType):
    '''
    type existential_name = Id.t
    '''
    def __init__(self):
        self.alias = Names__Id__t()


# (** Sorts *)

class Glob_term__glob_sort_gen(Variant):
    '''
    type 'a glob_sort_gen =
    | GProp (** representation of [Prop] literal *)
    | GSet  (** representation of [Set] literal *)
    | GType of 'a (** representation of [Type] literal *)
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'GProp': None,
            'GSet': None,
            'GType': a,
        })


class Glob_term__sort_info(AliasType):
    '''
    type sort_info = (Libnames.qualid * int) option list
    '''
    def __init__(self):
        self.alias = List(Option(Tuple(Libnames__qualid(), Int())))
        #super().__init__()


class Glob_term__glob_sort(AliasType):
    '''
    type glob_sort = sort_info glob_sort_gen
    '''
    def __init__(self):
        self.alias = Glob_term__glob_sort_gen(Glob_term__sort_info())


# (** Casts *)

class Glob_term__cast_type(Variant):
    '''
    type 'a cast_type =
    | CastConv of 'a
    | CastVM of 'a
    | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
    | CastNative of 'a
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'CastConv': a,
            'CastVM': a,
            'CastCoerce': None,
            'CastNative': a,
        })


class Glob_term__universe_kind(Variant):
    '''
    type 'a universe_kind =
    | UAnonymous
    | UUnknown
    | UNamed of 'a
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'UAnonymous': None,
            'UUnknown': None,
            'UNamed': a,
        })


class Glob_term__level_info(AliasType):
    '''
    type level_info = Libnames.qualid universe_kind
    '''
    def __init__(self):
        self.alias = Glob_term__universe_kind(Libnames__qualid())

class Glob_term__glob_level(AliasType):
    '''
    type glob_level = level_info glob_sort_gen
    '''
    def __init__(self):
        self.alias = Glob_term__glob_sort_gen(Glob_term__level_info())


# (** Bindings *) 

class Tactypes__quantified_hypothesis(Variant):
    '''
    type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'AnonHyp': Int(),
            'NamedHyp': Names__Id__t(),       
        })


class Tactypes__explicit_bindings(AliasType):
    '''
    type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = List(CAst__t(Tuple(Tactypes__quantified_hypothesis(), a)))


class Tactypes__bindings(Variant):
    '''
    type 'a bindings =
    | ImplicitBindings of 'a list
    | ExplicitBindings of 'a explicit_bindings
    | NoBindings
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'ImplicitBindings': List(a),
            'ExplicitBindings': Tactypes__explicit_bindings(a),
            'NoBindings': None,
        })


# (** Introduction patterns *)

class Tactypes__intro_pattern_expr(Variant):
    '''
    type 'constr intro_pattern_expr =
    | IntroForthcoming of bool
    | IntroNaming of intro_pattern_naming_expr
    | IntroAction of 'constr intro_pattern_action_expr
    '''
    def __init__(self, constr):
        if self.initialized:
            return
        assert isinstance(constr, Type)
        self.constr = constr
        self.constructors = OrderedDict({
            'IntroForthcoming': Bool(),
            'IntroNaming': Namegen__intro_pattern_naming_expr(),
            'IntroAction': Tactypes__intro_pattern_action_expr(constr),
        })


class Namegen__intro_pattern_naming_expr(Variant):
    '''
    and intro_pattern_naming_expr =
    | IntroIdentifier of Id.t
    | IntroFresh of Id.t
    | IntroAnonymous
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'IntroIdentifier': Names__Id__t(),
            'IntroFresh': Names__Id__t(),
            'IntroAnonymous': None,
        })

class Tactypes__intro_pattern_action_expr(Variant):
    '''
    and 'constr intro_pattern_action_expr =
    | IntroWildcard
    | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
    | IntroInjection of ('constr intro_pattern_expr) CAst.t list
    | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
    | IntroRewrite of bool
    '''
    def __init__(self, constr):
        assert isinstance(constr, Type)
        self.constr = constr
        self.constructors = OrderedDict({
            'IntroWildcard': None,
            'IntroOrAndPattern': Tactypes__or_and_intro_pattern_expr(constr),
            'IntroInjection': List(CAst__t(Tactypes__intro_pattern_expr(constr))),
            'IntroApplyOn': Tuple(CAst__t(constr), CAst__t(Tactypes__intro_pattern_expr(constr))),
            'IntroRewrite': Bool(),
        })


class Tactypes__or_and_intro_pattern_expr(Variant):
    '''
    and 'constr or_and_intro_pattern_expr =
    | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
    | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
    '''
    def __init__(self, constr):
        assert isinstance(constr, Type)
        self.constr = constr
        self.constructors = OrderedDict({
            'IntroOrPattern': List(List(CAst__t(Tactypes__intro_pattern_expr(constr))))  
        })


class Tactypes__with_bindings(AliasType):
    '''
    type 'a with_bindings = 'a * 'a bindings
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = Tuple(a, Tactypes__bindings(a))


class Constrexpr__or_by_notation_r(Variant):
    '''
    type 'a or_by_notation_r =
    | AN of 'a
    | ByNotation of (string * string option)
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'AN': a,
            'ByNotation': Tuple(String(), Option(String())),
        })


class Constrexpr__or_by_notation(AliasType):
    '''
    type 'a or_by_notation = 'a or_by_notation_r CAst.t
    '''
    inline = True

    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.alias = CAst__t(Constrexpr__or_by_notation_r(a))


class Misctypes__or_var(Variant):
    '''
    type 'a or_var =
    | ArgArg of 'a
    | ArgVar of lident
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.constructors = OrderedDict({
            'ArgArg': a,
            'ArgVar': Names__lident(),
        })

class Vernacexpr__proof_end(Variant):
    '''
    type proof_end =
    | Admitted
    (*                         name in `Save ident` when closing goal *)
    | Proved of opacity_flag * lident option
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Admitted': None,
            'Proved': Tuple(Vernacexpr__opacity_flag(), Option(Names__lident())),
        })


class Vernacexpr__bullet(Variant):
    '''
    type bullet =
    | Dash of int
    | Star of int
    | Plus of int
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'Dash': Int(), 
            'Star': Int(),
            'Plus': Int(),
        })


class Vernacexpr__extend_name(AliasType):
    '''
    type extend_name =
    (** Name of the vernac entry where the tactic is defined, typically found
        after the VERNAC EXTEND statement in the source. *)
    string *
    (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch
        is given an offset, starting from zero. *)
    int
    '''
    def __init__(self):
        self.alias = Tuple(String(), Int())


class Vernacexpr__goal_selector(Variant):
    '''
    type goal_selector =
    | SelectNth of int
    | SelectList of (int * int) list
    | SelectId of Id.t
    | SelectAll
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'SelectNth': Int(),
            'SelectList': List(Tuple(Int(), Int())),
            'SelectId': Names__Id__t(),
            'SelectAll': None,
        })


class Vernacexpr__vernac_expr(Variant):
    '''
    type nonrec vernac_expr =

    | VernacLoad of verbose_flag * string
    (* Syntax *)
    | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
    | VernacOpenCloseScope of bool * scope_name
    | VernacDelimiters of scope_name * string option
    | VernacBindScope of scope_name * class_rawexpr list
    | VernacInfix of (lstring * syntax_modifier list) *
        constr_expr * scope_name option
    | VernacNotation of
        constr_expr * (lstring * syntax_modifier list) *
        scope_name option
    | VernacNotationAddFormat of string * string * string

    (* Gallina *)
    | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
    | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
    | VernacEndProof of proof_end
    | VernacExactProof of constr_expr
    | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
        inline * (ident_decl list * constr_expr) with_coercion list
    | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
    | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
    | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
    | VernacScheme of (lident option * scheme) list
    | VernacCombinedScheme of lident * lident list
    | VernacUniverse of lident list
    | VernacConstraint of glob_constraint list

    (* Gallina extensions *)
    | VernacBeginSection of lident
    | VernacEndSegment of lident
    | VernacRequire of
        reference option * export_flag option * reference list
    | VernacImport of export_flag * reference list
    | VernacCanonical of reference or_by_notation
    | VernacCoercion of reference or_by_notation *
        class_rawexpr * class_rawexpr
    | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr
    | VernacNameSectionHypSet of lident * section_subset_expr 

    (* Type classes *)
    | VernacInstance of
        bool * (* abstract instance *)
        local_binder_expr list * (* super *)
        typeclass_constraint * (* instance name, class name, params *)
        (bool * constr_expr) option * (* props *)
        hint_info_expr

    | VernacContext of local_binder_expr list

    | VernacDeclareInstances of
        (reference * hint_info_expr) list (* instances names, priorities and patterns *)

    | VernacDeclareClass of reference (* inductive or definition name *)

    (* Modules and Module Types *)
    | VernacDeclareModule of bool option * lident *
        module_binder list * module_ast_inl
    | VernacDefineModule of bool option * lident * module_binder list *
        module_ast_inl module_signature * module_ast_inl list
    | VernacDeclareModuleType of lident *
        module_binder list * module_ast_inl list * module_ast_inl list
    | VernacInclude of module_ast_inl list

    (* Solving *)

    | VernacSolveExistential of int * constr_expr

    (* Auxiliary file and library management *)
    | VernacAddLoadPath of rec_flag * string * DirPath.t option
    | VernacRemoveLoadPath of string
    | VernacAddMLPath of rec_flag * string
    | VernacDeclareMLModule of string list
    | VernacChdir of string option

    (* State management *)
    | VernacWriteState of string
    | VernacRestoreState of string

    (* Resetting *)
    | VernacResetName of lident
    | VernacResetInitial
    | VernacBack of int
    | VernacBackTo of int

    (* Commands *)
    | VernacCreateHintDb of string * bool
    | VernacRemoveHints of string list * reference list
    | VernacHints of string list * hints_expr
    | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
        onlyparsing_flag
    | VernacDeclareImplicits of reference or_by_notation *
        (explicitation * bool * bool) list list
    | VernacArguments of reference or_by_notation *
        vernac_argument_status list (* Main arguments status list *) *
            (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) *
        int option (* Number of args to trigger reduction *) *
            [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
            `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
            `DefaultImplicits ] list
    | VernacArgumentsScope of reference or_by_notation *
        scope_name option list
    | VernacReserve of simple_binder list
    | VernacGeneralizable of (lident list) option
    | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list)
    | VernacSetStrategy of
        (Conv_oracle.level * reference or_by_notation list) list
    | VernacUnsetOption of export_flag * Goptions.option_name
    | VernacSetOption of export_flag * Goptions.option_name * option_value
    | VernacAddOption of Goptions.option_name * option_ref_value list
    | VernacRemoveOption of Goptions.option_name * option_ref_value list
    | VernacMemOption of Goptions.option_name * option_ref_value list
    | VernacPrintOption of Goptions.option_name
    | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr
    | VernacGlobalCheck of constr_expr
    | VernacDeclareReduction of string * Genredexpr.raw_red_expr
    | VernacPrint of printable
    | VernacSearch of searchable * goal_selector option * search_restriction
    | VernacLocate of locatable
    | VernacRegister of lident * register_kind
    | VernacComments of comment list

    (* Proof management *)
    | VernacAbort of lident option
    | VernacAbortAll
    | VernacRestart
    | VernacUndo of int
    | VernacUndoTo of int
    | VernacBacktrack of int*int*int
    | VernacFocus of int option
    | VernacUnfocus
    | VernacUnfocused
    | VernacBullet of bullet
    | VernacSubproof of goal_selector option
    | VernacEndSubproof
    | VernacShow of showable
    | VernacCheckGuard
    | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
    | VernacProofMode of string
    (* Toplevel control *)
    | VernacToplevelControl of exn

    (* For extension *)
    | VernacExtend of extend_name * Genarg.raw_generic_argument list
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            #'VernacAddMLPath': Tuple(Bool(), String()),
            #'VernacChdir': Option(String()),
            'VernacEndProof': Vernacexpr__proof_end(),
            'VernacBullet': Vernacexpr__bullet(),
            'VernacFocus': Option(Int()),
            'VernacUnfocus': None,
            'VernacSubproof': Option(Vernacexpr__goal_selector()),
            'VernacEndSubproof': None,
            'VernacProof': Tuple(Option(Genarg__raw_generic_argument()), 
                                 Option(Vernacexpr__section_subset_expr())),
            'VernacExtend': Tuple(Vernacexpr__extend_name(), List(Genarg__raw_generic_argument())),
        })


class CAst__t(Record):
    '''
    type 'a t = {
        v   : 'a;
        loc : Loc.t option;
    }
    '''
    def __init__(self, a):
        assert isinstance(a, Type)
        self.a = a
        self.fields = OrderedDict({
            'v': a,
            'loc': Option(Loc__t()),
        })

    def parsing_rules(self):
        return ['"(" %s ")"' % self.fields['v'].nonterminal], [self.fields['v']]


class Vernacexpr__vernac_control(Variant):
    '''
    type vernac_control =
    | VernacExpr of vernac_flag list * vernac_expr
    (* boolean is true when the `-time` batch-mode command line flag was set.
        the flag is used to print differently in `-time` vs `Time foo` *)
    | VernacTime of bool * vernac_control CAst.t
    | VernacRedirect of string * vernac_control CAst.t
    | VernacTimeout of int * vernac_control
    | VernacFail of vernac_control
    '''
    def __init__(self):
        self.constructors = OrderedDict({
            'VernacExpr': Tuple(List(Vernacexpr__vernac_flag()), Vernacexpr__vernac_expr()),
            #'VernacTime': Tuple(Bool(), CAst__t(self)),
            #'VernacRedirect': Tuple(String(), CAst__t(self)),
            #'VernacTimeout': Tuple(Int(), self),
            #'VernacFail': self,
        })


class Loc__located(Type):
    '''
    type 'a located = t option * 'a
    '''
    def __init__(self, t):
        assert isinstance(t, Type)
        self.t = t

    def parsing_rules(self):
        return Tuple(Option(Loc__t()), self.t).parsing_rules()


class Serapi__CoqAst(Variant):
    def __init__(self):
        self.constructors = OrderedDict({
            'CoqAst': Loc__located(Vernacexpr__vernac_control()),
        })


if __name__ == '__main__':
    t1 = Serapi__CoqAst()
    print(t1.to_ebnf(recursive=True))
    #print(t2.parsing_rules())
    #print(t3.parsing_rules())