X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=12b7774cd32938f9141e9e332f6e315d155d2f13;hb=cb7af66937e8c72ae6ea6694350a0c86f3e6ccf9;hp=d4e94b28bea16ce511ca4341b6489378becedde4;hpb=e937a197c1123e9adc6b2036ae47c7952ebbf138;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index d4e94b28b..12b7774cd 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -24,56 +24,46 @@ *) type direction = [ `Left | `Right ] -type reduction_kind = [ `Reduce | `Simpl | `Whd ] -(* type 'term pattern = Pattern of 'term *) - - (* everywhere includes goal and hypotheses *) -type 'term pattern = [ `Goal | `Everywhere ] - - (* when an 'ident option is None, the default is to apply the tactic - to the current goal *) +type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ] type loc = CicAst.location +type ('term, 'ident) pattern = + ('ident * 'term) list * 'term option + type ('term, 'ident) tactic = | Absurd of loc * 'term | Apply of loc * 'term - | Auto of loc + | Auto of loc * int option | Assumption of loc | Change of loc * 'term * 'term * 'ident option (* what, with what, where *) - | Change_pattern of loc * 'term pattern * 'term * 'ident option - (* what, with what, where *) | Contradiction of loc | Cut of loc * 'term | Decompose of loc * 'ident * 'ident list (* where, which principles *) - | Discriminate of loc * 'ident + | Discriminate of loc * 'term | Elim of loc * 'term * 'term option (* what to elim, which principle to use *) | ElimType of loc * 'term | Exact of loc * 'term | Exists of loc | Fold of loc * reduction_kind * 'term | Fourier of loc + | Generalize of loc * 'term * ('term, 'ident) pattern | Goal of loc * int (* change current goal, argument is goal number 1-based *) | Injection of loc * 'ident | Intros of loc * int option * 'ident list | Left of loc | LetIn of loc * 'term * 'ident -(* | Named_intros of loc * 'ident list (* joined with Intros above *) *) -(* | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *) - | Reduce of loc * reduction_kind * ('term list * 'term pattern) option - (* kind, (what, where) - * if second argument is None, reduction is applied to the current goal, - * otherwise to each occurrence of loc * terms given in list occuring in term - * pattern *) + | Reduce of loc * reduction_kind * ('term, 'ident) pattern | Reflexivity of loc | Replace of loc * 'term * 'term (* what, with what *) - | Replace_pattern of loc * 'term pattern * 'term - | Rewrite of loc * direction * 'term * 'ident option + | Rewrite of loc * direction * 'term * ('term, 'ident) pattern | Right of loc | Ring of loc | Split of loc | Symmetry of loc | Transitivity of loc * 'term + | FwdSimpl of loc * 'ident + | LApply of loc * 'term * ('ident * 'term) list type thm_flavour = [ `Definition @@ -92,14 +82,20 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] type 'term macro = - | Abort of loc + (* 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 *) +(* | Abort of loc *) | Print of loc * string | Check of loc * 'term | Hint of loc - | Match of loc * 'term | Quit of loc - | Redo of loc * int option - | Undo of loc * int option +(* | Redo of loc * int option + | Undo of loc * int option *) (* | Print of loc * print_kind *) | Search_pat of loc * search_kind * string (* searches with string pattern *) | Search_term of loc * search_kind * 'term (* searches with term pattern *) @@ -109,23 +105,30 @@ type alias_spec = | Symbol_alias of string * int * string (* name, instance no, description *) | Number_alias of int * string (* instance no, description *) -type 'term command = - | Set of loc * string * string - | Qed of loc - (** name. - * Name is needed when theorem was started without providing a name - *) - | Inductive of loc * (string * 'term) list * 'term inductive_type list +type obj = + | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list (** parameters, list of loc * mutual inductive types *) - | Theorem of loc * thm_flavour * string option * 'term * 'term option + | Theorem of thm_flavour * string * CicAst.term * CicAst.term option (** flavour, name, type, body * - name is absent when an unnamed theorem is being proved, tipically in * interactive usage * - body is present when its given along with the command, otherwise it * will be given in proof editing mode using the tactical language *) + | Record of + (string * CicAst.term) list * string * CicAst.term * + (string * CicAst.term) list + +type ('term,'obj) command = + | Set of loc * string * string + | Qed of loc + (** name. + * Name is needed when theorem was started without providing a name + *) | Coercion of loc * 'term | Alias of loc * alias_spec + (** parameters, name, type, fields *) + | Obj of loc * 'obj type ('term, 'ident) tactical = | Tactic of loc * ('term, 'ident) tactic @@ -139,11 +142,20 @@ type ('term, 'ident) tactical = (* try a sequence of loc * tacticals until one succeeds, fail otherwise *) | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *) -type ('term, 'ident) statement = - | Command of loc * 'term command + +type ('term, 'obj, 'ident) code = + | Command of loc * ('term,'obj) command | Macro of loc * 'term macro (* Macro are substantially queries, but since we are not the kind of * peolpe that like to push "start" to turn off the computer * we added this command *) | Tactical of loc * ('term, 'ident) tactical + +type ('term, 'obj, 'ident) comment = + | Note of loc * string + | Code of loc * ('term, 'obj, 'ident) code + +type ('term, 'obj, 'ident) statement = + | Executable of loc * ('term, 'obj, 'ident) code + | Comment of loc * ('term, 'obj, 'ident) comment