X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=c4ec503c797a2418b66ea0dcfc8c39359f747b80;hb=489639a3c319d0349a9c864fd0eeaf659daa3d3f;hp=9ea33c2de294acd90212ef37c0fb830000f1324e;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 9ea33c2de..c4ec503c7 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -29,49 +29,39 @@ type direction = [ `LeftToRight | `RightToLeft ] type loc = Stdpp.location -type ('term, 'lazy_term, 'ident) pattern = - 'lazy_term option * ('ident * 'term) list * 'term option +type nterm = NotationPt.term type npattern = - CicNotationPt.term option * (string * CicNotationPt.term) list * CicNotationPt.term option + nterm option * (string * nterm) list * nterm option -type 'lazy_term reduction = - [ `Normalize - | `Simpl - | `Unfold of 'lazy_term option - | `Whd ] +type auto_params = nterm list option * (string*string) list -type 'ident intros_spec = int option * 'ident option list - -type 'term auto_params = 'term list option * (string*string) list - -type 'term just = - [ `Term of 'term - | `Auto of 'term auto_params ] +type just = [`Term of nterm | `Auto of auto_params] type ntactic = - | NApply of loc * CicNotationPt.term - | NSmartApply of loc * CicNotationPt.term - | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list - | NCases of loc * CicNotationPt.term * npattern + | NApply of loc * nterm + | NSmartApply of loc * nterm + | NAssert of loc * ((string * [`Decl of nterm | `Def of nterm * nterm]) list * nterm) list + | NCases of loc * nterm * npattern | NCase1 of loc * string - | NChange of loc * npattern * CicNotationPt.term - | NConstructor of loc * int option * CicNotationPt.term list - | NCut of loc * CicNotationPt.term -(* | NDiscriminate of loc * CicNotationPt.term - | NSubst of loc * CicNotationPt.term *) + | NChange of loc * npattern * nterm + | NClear of loc * string list + | NConstructor of loc * int option * nterm list + | NCut of loc * nterm +(* | NDiscriminate of loc * nterm + | NSubst of loc * nterm *) | NDestruct of loc * string list option * string list - | NElim of loc * CicNotationPt.term * npattern + | NElim of loc * nterm * npattern | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string | NIntros of loc * string list - | NInversion of loc * CicNotationPt.term * npattern - | NLApply of loc * CicNotationPt.term - | NLetIn of loc * npattern * CicNotationPt.term * string + | NInversion of loc * nterm * npattern + | NLApply of loc * nterm + | NLetIn of loc * npattern * nterm * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern - | NRewrite of loc * direction * CicNotationPt.term * npattern - | NAuto of loc * CicNotationPt.term auto_params + | NRewrite of loc * direction * nterm * npattern + | NAuto of loc * auto_params | NDot of loc | NSemicolon of loc | NBranch of loc @@ -87,186 +77,95 @@ type ntactic = | NAssumption of loc | NRepeat of loc * ntactic | NBlock of loc * ntactic list - -type ('term, 'lazy_term, 'reduction, 'ident) tactic = - (* Higher order tactics (i.e. tacticals) *) - | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic - | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - (* sequential composition *) - | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic * - ('term, 'lazy_term, 'reduction, 'ident) tactic list - | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - (* try a sequence of loc * tactic until one succeeds, fail otherwise *) - | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - (* try a tactic and mask failures *) - | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list - | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - (* Real tactics *) - | Absurd of loc * 'term - | Apply of loc * 'term - | ApplyRule of loc * 'term - | ApplyP of loc * 'term (* apply for procedural reconstruction *) - | ApplyS of loc * 'term * 'term auto_params - | Assumption of loc - | AutoBatch of loc * 'term auto_params - | Cases of loc * 'term * ('term, 'lazy_term, 'ident) pattern * - 'ident intros_spec - | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term - | Clear of loc * 'ident list - | ClearBody of loc * 'ident - | Compose of loc * 'term * 'term option * int * 'ident intros_spec - | Constructor of loc * int - | Contradiction of loc - | Cut of loc * 'ident option * 'term - | Decompose of loc * 'ident option list - | Demodulate of loc * 'term auto_params - | Destruct of loc * 'term list option - | Elim of loc * 'term * 'term option * ('term, 'lazy_term, 'ident) pattern * - 'ident intros_spec - | ElimType of loc * 'term * 'term option * 'ident intros_spec - | Exact of loc * 'term - | Exists of loc - | Fail of loc - | Fold of loc * 'reduction * 'lazy_term * ('term, 'lazy_term, 'ident) pattern - | Fourier of loc - | FwdSimpl of loc * string * 'ident option list - | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option - | IdTac of loc - | Intros of loc * 'ident intros_spec - | Inversion of loc * 'term - | LApply of loc * bool * int option * 'term list * 'term * 'ident option - | Left of loc - | LetIn of loc * 'term * 'ident - | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern - | Reflexivity of loc - | Replace of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term - | Rewrite of loc * direction * 'term * - ('term, 'lazy_term, 'ident) pattern * 'ident option list - | Right of loc - | Ring of loc - | Split of loc - | Symmetry of loc - | Transitivity of loc * 'term - (* Declarative language *) - | Assume of loc * 'ident * 'term - | Suppose of loc * 'term *'ident * 'term option - | By_just_we_proved of loc * 'term just * - 'term * 'ident option * 'term option - | We_need_to_prove of loc * 'term * 'ident option * 'term option - | Bydone of loc * 'term just - | We_proceed_by_induction_on of loc * 'term * 'term - | We_proceed_by_cases_on of loc * 'term * 'term - | Byinduction of loc * 'term * 'ident - | Thesisbecomes of loc * 'term - | Case of loc * string * (string * 'term) list - | ExistsElim of loc * 'term just * 'ident * 'term * 'ident * 'lazy_term - | AndElim of loc * 'term just * 'ident * 'term * 'ident * 'term - | RewritingStep of - loc * (string option * 'term) option * 'term * - [ `Term of 'term | `Auto of 'term auto_params - | `Proof | `SolveWith of 'term ] * - bool (* last step*) - -type search_kind = [ `Locate | `Hint | `Match | `Elim ] - -type print_kind = [ `Env | `Coer ] - -type inline_param = IPPrefix of string (* undocumented *) - | IPAs of Cic.object_flavour (* preferred flavour *) - | IPCoercions (* show coercions *) - | IPDebug of int (* set debug level *) - | IPProcedural (* procedural rendering *) - | IPNoDefaults (* no default-based tactics *) - | IPLevel of int (* granularity level *) - | IPDepth of int (* undocumented *) - | IPComments (* show statistics *) - | IPCR (* detect convertible rewriting *) - -type ('term,'lazy_term) macro = - (* Whelp's stuff *) - | WHint of loc * 'term - | WMatch of loc * 'term - | WInstance of loc * 'term - | WLocate of loc * string - | WElim of loc * 'term - (* real macros *) - | Eval of loc * 'lazy_term reduction * 'term - | Check of loc * 'term - | Hint of loc * bool - | AutoInteractive of loc * 'term auto_params - | Inline of loc * string * inline_param list - (* URI or base-uri, parameters *) + (* Declarative langauge *) + (* Not the best idea to use a string directly, an abstract type for identifiers would be better *) + | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *) + | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *) + | By_just_we_proved of loc * just * nterm * string option * nterm option (* loc, + justification, conclusion, identifier, eqconcl *) + | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion, + identifier, equivnewcon *) + | Bydone of loc * just + | ExistsElim of loc * just * string * nterm * nterm * string + | AndElim of loc * just * nterm * string * nterm * string + (* + | RewritingStep of + loc * (string option * nterm) option * nterm * + [ `Term of nterm | `Auto of auto_params + | `Proof | `SolveWith of nterm ] * + bool (* last step*) + *) + | RewritingStep of + loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*) + | Obtain of + loc * string * nterm + | Conclude of + loc * nterm + | Thesisbecomes of loc * nterm * nterm option + | We_proceed_by_induction_on of loc * nterm * nterm + | We_proceed_by_cases_on of loc * nterm * nterm + | Byinduction of loc * nterm * string + | Case of loc * string * (string * nterm) list + (* This is a debug tactic to print the stack to stdout, can be safely removed *) + | PrintStack of loc type nmacro = - | NCheck of loc * CicNotationPt.term + | NCheck of loc * nterm | Screenshot of loc * string - | NAutoInteractive of loc * CicNotationPt.term auto_params + | NAutoInteractive of loc * auto_params | NIntroGuess of loc (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 34 - -type ('term,'obj) command = - | Index of loc * 'term option (* key *) * UriManager.uri (* value *) - | Select of loc * UriManager.uri - | Pump of loc * int - | Coercion of loc * 'term * bool (* add_obj *) * - int (* arity *) * int (* saturations *) - | PreferCoercion of loc * 'term - | Inverter of loc * string * 'term * bool list - | Default of loc * string * UriManager.uri list - | Drop of loc - | Include of loc * bool (* normal? *) * [`New | `OldAndNew] * string - | Obj of loc * 'obj - | Relation of - loc * string * 'term * 'term * 'term option * 'term option * 'term option - | Set of loc * string * string - | Print of loc * string - | Qed of loc +let magic = 37 -type ncommand = - | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) - | NObj of loc * CicNotationPt.term CicNotationPt.obj - | NDiscriminator of loc * CicNotationPt.term - | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option - | NUnivConstraint of loc * NUri.uri * NUri.uri - | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list - | NCoercion of loc * string * - CicNotationPt.term * CicNotationPt.term * - (string * CicNotationPt.term) * CicNotationPt.term - | NQed of loc +(* composed magic: term + command magics. No need to change this value *) +let magic = magic + 10000 * NotationPt.magic -type punctuation_tactical = - | Dot of loc - | Semicolon of loc - | Branch of loc - | Shift of loc - | Pos of loc * int list - | Wildcard of loc - | Merge of loc +type alias_spec = + | Ident_alias of string * string (* identifier, uri *) + | Symbol_alias of string * int * string (* name, instance no, description *) + | Number_alias of int * string (* instance no, description *) -type non_punctuation_tactical = - | Focus of loc * int list - | Unfocus of loc - | Skip of loc +type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *) -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = - | Command of loc * ('term, 'obj) command - | NCommand of loc * ncommand - | Macro of loc * ('term,'lazy_term) macro +type command = + | Include of loc * inclusion_mode * string (* _,buri,_,path *) + | UnificationHint of loc * nterm * int (* term, precedence *) + | NObj of loc * nterm NotationPt.obj * bool + | NDiscriminator of loc * nterm + | NInverter of loc * string * nterm * bool list option * nterm option + | NUnivConstraint of loc * bool * NUri.uri * NUri.uri + | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list + | NCoercion of loc * string * bool * + (nterm * nterm * (string * nterm) * nterm) option + | NQed of loc * bool + (* ex lexicon commands *) + | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Notation of loc * direction option * nterm * Gramext.g_assoc * + int * nterm + (* direction, l1 pattern, associativity, precedence, l2 pattern *) + | Interpretation of loc * + string * (string * NotationPt.argument_pattern list) * + NotationPt.cic_appl_pattern + (* description (i.e. id), symbol, arg pattern, appl pattern *) + +type code = + | NCommand of loc * command | NMacro of loc * nmacro | NTactic of loc * ntactic list - | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option - * punctuation_tactical - | NonPunctuationTactical of loc * non_punctuation_tactical - * punctuation_tactical -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = +type comment = | Note of loc * string - | Code of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code + | Code of loc * code -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) statement = - | Executable of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) code - | Comment of loc * ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment +type statement = + | Executable of loc * code + | Comment of loc * comment + +let description_of_alias = + function + Ident_alias (_,desc) + | Symbol_alias (_,_,desc) + | Number_alias (_,desc) -> desc