X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=32a29c2158a98e8f1dda73f10191a6a6f6fe3d54;hb=3a5ad4a99fd7f312424200a9241ea1a4ce7fcd29;hp=833f98d7c8b5766cba5d30d419c9dbf193280757;hpb=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 833f98d7c..32a29c215 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -29,25 +29,10 @@ type direction = [ `LeftToRight | `RightToLeft ] type loc = Stdpp.location -type ('term, 'lazy_term, 'ident) pattern = - 'lazy_term option * ('ident * 'term) list * 'term option - type npattern = NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option -type 'lazy_term reduction = - [ `Normalize - | `Simpl - | `Unfold of 'lazy_term option - | `Whd ] - -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 auto_params = NotationPt.term list option * (string*string) list type ntactic = | NApply of loc * NotationPt.term @@ -56,6 +41,7 @@ type ntactic = | NCases of loc * NotationPt.term * npattern | NCase1 of loc * string | NChange of loc * npattern * NotationPt.term + | NClear of loc * string list | NConstructor of loc * int option * NotationPt.term list | NCut of loc * NotationPt.term (* | NDiscriminate of loc * NotationPt.term @@ -71,7 +57,7 @@ type ntactic = | NLetIn of loc * npattern * NotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern | NRewrite of loc * direction * NotationPt.term * npattern - | NAuto of loc * NotationPt.term auto_params + | NAuto of loc * auto_params | NDot of loc | NSemicolon of loc | NBranch of loc @@ -88,119 +74,28 @@ type ntactic = | 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 nmacro = | NCheck of loc * NotationPt.term | Screenshot of loc * string - | NAutoInteractive of loc * NotationPt.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 +let magic = 35 -type command = - | Drop of loc - | Include of loc * bool (* normal? *) * [`New | `OldAndNew] * string - | Set of loc * string * string - | Print of loc * string - | Qed of loc +(* composed magic: term + command magics. No need to change this value *) +let magic = magic + 10000 * NotationPt.magic + +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 ncommand = +type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *) + +type command = + | Include of loc * inclusion_mode * string (* _,buri,_,path *) | UnificationHint of loc * NotationPt.term * int (* term, precedence *) | NObj of loc * NotationPt.term NotationPt.obj | NDiscriminator of loc * NotationPt.term @@ -211,35 +106,32 @@ type ncommand = NotationPt.term * NotationPt.term * (string * NotationPt.term) * NotationPt.term | NQed of loc - -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 non_punctuation_tactical = - | Focus of loc * int list - | Unfocus of loc - | Skip of loc - -type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = - | Command of loc * command - | NCommand of loc * ncommand + (* ex lexicon commands *) + | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Notation of loc * direction option * NotationPt.term * Gramext.g_assoc * + int * NotationPt.term + (* 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