From: Andrea Asperti Date: Fri, 8 Oct 2010 13:21:54 +0000 (+0000) Subject: Cic.term and Cic.obj unused! X-Git-Tag: make_still_working~2784 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=729e08f5fb86b3ffee460fda4577b024ab5888aa;p=helm.git Cic.term and Cic.obj unused! --- diff --git a/matita/components/binaries/transcript/grafite.ml b/matita/components/binaries/transcript/grafite.ml index 89f8d2d02..176c7f55e 100644 --- a/matita/components/binaries/transcript/grafite.ml +++ b/matita/components/binaries/transcript/grafite.ml @@ -71,30 +71,9 @@ let out_command och cmd = let command_of_obj obj = G.Executable (floc, G.Command (floc, obj)) -let command_of_macro macro = - G.Executable (floc, G.Macro (floc, macro)) - let require moo value = command_of_obj (G.Include (floc, moo, `OldAndNew, value ^ ".ma")) -let coercion value = - command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0)) - -let inline kind uri prefix flavour params = - let params = match prefix with - | "" -> params - | prefix -> G.IPPrefix prefix :: params - in - let params = match flavour with - | None -> params - | Some flavour -> G.IPAs flavour :: params - in - let params = match kind with - | T.Declarative -> params - | T.Procedural -> G.IPProcedural :: params - in - command_of_macro (G.Inline (floc, uri, params)) - let out_alias och name uri = Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri @@ -117,13 +96,6 @@ let commit kind och items = if !O.comments then out_unexported och "NOTATION" (snd specs) (**) | T.Inline (_, T.Var, src, _, _, _) -> if !O.comments then out_unexported och "UNEXPORTED" src -(* FG: we do not export variables because we cook the other objects - * let name = UriManager.name_of_uri (UriManager.uri_of_string src) in - * out_alias och name src - *) - | T.Inline (_, _, src, pre, fl, params) -> - if !O.getter then check och src; - out_command och (inline kind src pre fl params) | T.Section specs -> if !O.comments then out_unexported och "UNEXPORTED" (trd specs) | T.Comment comment -> diff --git a/matita/components/cic/.depend b/matita/components/cic/.depend index 2ba6ab8fd..e69de29bb 100644 --- a/matita/components/cic/.depend +++ b/matita/components/cic/.depend @@ -1,8 +0,0 @@ -cicUniv.cmi: -cicPp.cmi: cic.cmo -cic.cmo: cicUniv.cmi -cic.cmx: cicUniv.cmx -cicUniv.cmo: cicUniv.cmi -cicUniv.cmx: cicUniv.cmi -cicPp.cmo: cic.cmo cicPp.cmi -cicPp.cmx: cic.cmx cicPp.cmi diff --git a/matita/components/cic/cic.ml b/matita/components/cic/cic.ml index 012f52eea..8b1d379b7 100644 --- a/matita/components/cic/cic.ml +++ b/matita/components/cic/cic.ml @@ -37,17 +37,7 @@ (* $Id$ *) -(* STUFF TO MANAGE IDENTIFIERS *) type id = string (* the abstract type of the (annotated) node identifiers *) -type 'term explicit_named_substitution = (UriManager.uri * 'term) list - -type implicit_annotation = [ `Closed | `Type | `Hole ] - -(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *) - -type sort = - Prop - | Set type name = | Name of string @@ -63,175 +53,3 @@ type object_flavour = | `Variant | `Axiom ] - -type object_class = - [ `Elim of sort (** elimination principle; if sort is Type, the universe is - * not relevant *) - | `Record of (string * bool * int) list (** - inductive type that encodes a record; the arguments are - the record fields names and if they are coercions and - then the coercion arity *) - | `Projection (** record projection *) - | `InversionPrinciple (** inversion principle *) - ] - -type attribute = - [ `Class of object_class - | `Flavour of object_flavour - | `Generated - ] - -type term = - Rel of int (* DeBrujin index, 1 based*) - | Var of UriManager.uri * (* uri, *) - term explicit_named_substitution (* explicit named subst. *) - | Meta of int * (term option) list (* numeric id, *) - (* local context *) - | Sort of sort (* sort *) - | Implicit of implicit_annotation option (* *) - | Cast of term * term (* value, type *) - | Prod of name * term * term (* binder, source, target *) - | Lambda of name * term * term (* binder, source, target *) - | LetIn of name * term * term * term (* binder, term, type, target *) - | Appl of term list (* arguments *) - | Const of UriManager.uri * (* uri, *) - term explicit_named_substitution (* explicit named subst. *) - | MutInd of UriManager.uri * int * (* uri, typeno, *) - term explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - | MutConstruct of UriManager.uri * (* uri, *) - int * int * (* typeno, consno *) - term explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - (* consno is 1 based *) - | MutCase of UriManager.uri * (* ind. uri, *) - int * (* ind. typeno, *) - term * term * (* outtype, ind. term *) - term list (* patterns *) - | Fix of int * inductiveFun list (* funno (0 based), funs *) - | CoFix of int * coInductiveFun list (* funno (0 based), funs *) -and obj = - Constant of string * term option * term * (* id, body, type, *) - UriManager.uri list * attribute list (* parameters *) - | Variable of string * term option * term * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | CurrentProof of string * metasenv * term * (* name, conjectures, body, *) - term * UriManager.uri list * attribute list (* type, parameters *) - | InductiveDefinition of inductiveType list * (* inductive types, *) - UriManager.uri list * int * attribute list (* params, left params no *) -and inductiveType = - string * bool * term * (* typename, inductive, arity *) - constructor list (* constructors *) -and constructor = - string * term (* id, type *) -and inductiveFun = - string * int * term * term (* name, ind. index, type, body *) -and coInductiveFun = - string * term * term (* name, type, body *) - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and conjecture = int * context * term -and metasenv = conjecture list -and substitution = (int * (context * term * term)) list - - - -(* a metasenv is a list of declarations of metas in declarations *) -(* order (i.e. [oldest ; ... ; newest]). Older variables can not *) -(* depend on new ones. *) -and annconjecture = id * int * anncontext * annterm -and annmetasenv = annconjecture list - -and annterm = - ARel of id * id * int * (* idref, DeBrujin index, *) - string (* binder *) - | AVar of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMeta of id * int * (annterm option) list (* numeric id, *) - (* local context *) - | ASort of id * sort (* sort *) - | AImplicit of id * implicit_annotation option (* *) - | ACast of id * annterm * annterm (* value, type *) - | AProd of id * name * annterm * annterm (* binder, source, target *) - | ALambda of id * name * annterm * annterm (* binder, source, target *) - | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *) - | AAppl of id * annterm list (* arguments *) - | AConst of id * UriManager.uri * (* uri, *) - annterm explicit_named_substitution (* explicit named subst. *) - | AMutInd of id * UriManager.uri * int * (* uri, typeno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - | AMutConstruct of id * UriManager.uri * (* uri, *) - int * int * (* typeno, consno *) - annterm explicit_named_substitution (* explicit named subst. *) - (* typeno is 0 based *) - (* consno is 1 based *) - | AMutCase of id * UriManager.uri * (* ind. uri, *) - int * (* ind. typeno, *) - annterm * annterm * (* outtype, ind. term *) - annterm list (* patterns *) - | AFix of id * int * anninductiveFun list (* funno, functions *) - | ACoFix of id * int * anncoInductiveFun list (* funno, functions *) -and annobj = - AConstant of id * id option * string * (* name, *) - annterm option * annterm * (* body, type, *) - UriManager.uri list * attribute list (* parameters *) - | AVariable of id * - string * annterm option * annterm * (* name, body, type *) - UriManager.uri list * attribute list (* parameters *) - | ACurrentProof of id * id * - string * annmetasenv * (* name, conjectures, *) - annterm * annterm * UriManager.uri list * (* body,type,parameters *) - attribute list - | AInductiveDefinition of id * - anninductiveType list * (* inductive types , *) - UriManager.uri list * int * attribute list (* parameters,n ind. pars*) -and anninductiveType = - id * string * bool * annterm * (* typename, inductive, arity *) - annconstructor list (* constructors *) -and annconstructor = - string * annterm (* id, type *) -and anninductiveFun = - id * string * int * annterm * annterm (* name, ind. index, type, body *) -and anncoInductiveFun = - id * string * annterm * annterm (* name, type, body *) -and annotation = - string - -and context_entry = (* A declaration or definition *) - Decl of term - | Def of term * term (* body, type *) - -and hypothesis = - (name * context_entry) option (* None means no more accessible *) - -and context = hypothesis list - -and anncontext_entry = (* A declaration or definition *) - ADecl of annterm - | ADef of annterm * annterm - -and annhypothesis = - id * (name * anncontext_entry) option (* None means no more accessible *) - -and anncontext = annhypothesis list -;; - -type anntarget = - Object of annobj (* if annobj is a Constant, this is its type *) - | ConstantBody of annobj - | Term of annterm - | Conjecture of annconjecture - | Hypothesis of annhypothesis - -module CicHash = - Hashtbl.Make - (struct - type t = term - let equal = (==) - let hash = Hashtbl.hash_param 100 1000 - end) -;; - diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 9d68213b7..833f98d7c 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -183,15 +183,6 @@ type inline_param = IPPrefix of string (* undocumented *) | IPComments (* show statistics *) | IPCR (* detect convertible rewriting *) -type ('term,'lazy_term) macro = - (* 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 *) - type nmacro = | NCheck of loc * NotationPt.term | Screenshot of loc * string @@ -202,20 +193,9 @@ type nmacro = * 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 +type command = | 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 @@ -247,9 +227,8 @@ type non_punctuation_tactical = | Skip of loc type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = - | Command of loc * ('term, 'obj) command + | Command of loc * command | NCommand of loc * ncommand - | Macro of loc * ('term,'lazy_term) macro | NMacro of loc * nmacro | NTactic of loc * ntactic list | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index e506742c4..a4df0b24d 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -315,46 +315,6 @@ let pp_nmacro = function | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name ;; -let pp_macro ~term_pp ~lazy_term_pp = - let term_pp = pp_arg ~term_pp in - let flavour_pp = function - | `Definition -> "definition" - | `Fact -> "fact" - | `Lemma -> "lemma" - | `Remark -> "remark" - | `Theorem -> "theorem" - | `Variant -> "variant" - | `Axiom -> "axiom" - | `MutualDefinition -> assert false - in - let pp_inline_params l = - let pp_param = function - | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\"" - | IPAs flavour -> flavour_pp flavour - | IPCoercions -> "coercions" - | IPDebug debug -> "debug = " ^ string_of_int debug - | IPProcedural -> "procedural" - | IPNoDefaults -> "nodefaults" - | IPDepth depth -> "depth = " ^ string_of_int depth - | IPLevel level -> "level = " ^ string_of_int level - | IPComments -> "comments" - | IPCR -> "cr" - in - let s = String.concat " " (List.map pp_param l) in - if s = "" then s else " " ^ s - in - let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in - function - (* real macros *) - | Eval (_, kind, term) -> - Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term) - | Check (_, term) -> Printf.sprintf "check %s" (term_pp term) - | Hint (_, true) -> "hint rewrite" - | Hint (_, false) -> "hint" - | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params - | Inline (_, suri, params) -> - Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params) - let pp_associativity = function | Gramext.LeftA -> "left associative" | Gramext.RightA -> "right associative" @@ -388,36 +348,13 @@ let pp_ncommand ~obj_pp = function map) ;; -let pp_command ~term_pp ~obj_pp = function - | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri - | Coercion (_, t, do_composites, i, j) -> - pp_coercion ~term_pp t do_composites i j - | PreferCoercion (_,t) -> - "prefer coercion " ^ term_pp t - | Inverter (_,n,ty,params) -> - "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params - | Default (_,what,uris) -> pp_default what uris +let pp_command = function | Drop _ -> "drop" | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\"" | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\"" | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path - | Obj (_,obj) -> obj_pp obj - | Qed _ -> "qed" - | Relation (_,id,a,aeq,refl,sym,trans) -> - "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^ - (match refl with - Some r -> " reflexivity proved by " ^ term_pp r - | None -> "") ^ - (match sym with - Some r -> " symmetry proved by " ^ term_pp r - | None -> "") ^ - (match trans with - Some r -> " transitivity proved by " ^ term_pp r - | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value - | Pump (_) -> "not supported" let pp_punctuation_tactical = function @@ -439,7 +376,6 @@ let pp_non_punctuation_tactical = let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = function | NMacro (_, macro) -> pp_nmacro macro ^ "." - | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "." | Tactic (_, Some tac, punct) -> pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac ^ pp_punctuation_tactical punct @@ -450,7 +386,7 @@ let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp = | NonPunctuationTactical (_, tac, punct) -> pp_non_punctuation_tactical tac ^ pp_punctuation_tactical punct - | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." + | Command (_, cmd) -> pp_command cmd ^ "." | NCommand (_, cmd) -> let obj_pp = Obj.magic obj_pp in pp_ncommand ~obj_pp cmd ^ "." diff --git a/matita/components/grafite/grafiteAstPp.mli b/matita/components/grafite/grafiteAstPp.mli index 4ae11a59b..6594d2137 100644 --- a/matita/components/grafite/grafiteAstPp.mli +++ b/matita/components/grafite/grafiteAstPp.mli @@ -43,14 +43,7 @@ val pp_reduction_kind: 'a GrafiteAst.reduction -> string -val pp_command: - term_pp:('term -> string) -> - obj_pp:('obj -> string) -> - ('term,'obj) GrafiteAst.command -> string -val pp_macro: - term_pp:('term -> string) -> - lazy_term_pp:('lazy_term -> string) -> - ('term,'lazy_term) GrafiteAst.macro -> string +val pp_command: GrafiteAst.command -> string val pp_comment: map_unicode_to_tex:bool -> term_pp:('term -> string) -> diff --git a/matita/components/grafite/grafiteMarshal.ml b/matita/components/grafite/grafiteMarshal.ml index 15e4f5217..327f39809 100644 --- a/matita/components/grafite/grafiteMarshal.ml +++ b/matita/components/grafite/grafiteMarshal.ml @@ -25,7 +25,7 @@ (* $Id$ *) -type ast_command = (Cic.term,Cic.obj) GrafiteAst.command +type ast_command = GrafiteAst.command type moo = ast_command list let format_name = "grafite" @@ -41,15 +41,12 @@ let rehash_cmd_uris = let rehash_uri uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in function - | GrafiteAst.Default (loc, name, uris) -> - let uris = List.map rehash_uri uris in - GrafiteAst.Default (loc, name, uris) | GrafiteAst.Include _ as cmd -> cmd | cmd -> prerr_endline "Found a command not expected in a .moo:"; let term_pp _ = assert false in let obj_pp _ = assert false in - prerr_endline (GrafiteAstPp.pp_command ~term_pp ~obj_pp cmd); + prerr_endline (GrafiteAstPp.pp_command cmd); assert false let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo) diff --git a/matita/components/grafite/grafiteMarshal.mli b/matita/components/grafite/grafiteMarshal.mli index cad7b1187..aebaf1a7f 100644 --- a/matita/components/grafite/grafiteMarshal.mli +++ b/matita/components/grafite/grafiteMarshal.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -type ast_command = (Cic.term,Cic.obj) GrafiteAst.command +type ast_command = GrafiteAst.command type moo = ast_command list val save_moo: fname:string -> moo -> unit diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 6dd087d78..b4a20c202 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -28,9 +28,6 @@ exception Drop (* mo file name, ma file name *) exception IncludedFileNotCompiled of string * string -exception Macro of - GrafiteAst.loc * - (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -51,13 +48,8 @@ type eval_ast = disambiguate_command: (GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - - disambiguate_macro: - (GrafiteTypes.status -> - (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) -> + (GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * GrafiteAst.command) -> ?do_heavy_checks:bool -> GrafiteTypes.status -> @@ -69,18 +61,18 @@ type eval_ast = type 'a eval_command = {ec_go: 'term 'obj. disambiguate_command: - (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> + (GrafiteTypes.status -> GrafiteAst.command disambiguator_input -> + GrafiteTypes.status * GrafiteAst.command) -> options -> GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteAst.command disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } type 'a eval_comment = {ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident. disambiguate_command: - (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> + (GrafiteTypes.status -> GrafiteAst.command disambiguator_input -> + GrafiteTypes.status * GrafiteAst.command) -> options -> GrafiteTypes.status -> (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input -> GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] @@ -91,13 +83,8 @@ type 'a eval_executable = disambiguate_command: (GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> - - disambiguate_macro: - (GrafiteTypes.status -> - (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) -> + GrafiteAst.command disambiguator_input -> + GrafiteTypes.status * GrafiteAst.command) -> options -> GrafiteTypes.status -> @@ -678,13 +665,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,`New [] | GrafiteAst.Print (_,_) -> status,`New [] | GrafiteAst.Set (loc, name, value) -> status, `New [] -(* GrafiteTypes.set_option status name value,[] *) - | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false in status,uris } and eval_executable = {ee_go = fun ~disambiguate_command -~disambiguate_macro opts status (text,prefix_len,ex) -> + opts status (text,prefix_len,ex) -> match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then @@ -702,8 +687,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.NCommand (_, cmd) -> eval_ncommand opts status (text,prefix_len,cmd) - | GrafiteAst.Macro (loc, macro) -> - raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro))) | GrafiteAst.NMacro (loc, macro) -> raise (NMacro (loc,macro)) @@ -720,21 +703,20 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,lemmas = eval_ast.ea_go ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd) - ~disambiguate_macro:(fun _ _ -> assert false) status ast in assert (lemmas=`New []); status) status moo } and eval_ast = {ea_go = fun ~disambiguate_command -~disambiguate_macro ?(do_heavy_checks=false) status +?(do_heavy_checks=false) status (text,prefix_len,st) -> let opts = { do_heavy_checks = do_heavy_checks ; } in match st with | GrafiteAst.Executable (_,ex) -> eval_executable.ee_go ~disambiguate_command - ~disambiguate_macro opts status (text,prefix_len,ex) + opts status (text,prefix_len,ex) | GrafiteAst.Comment (_,c) -> eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) } and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index dd3216412..921718611 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -25,9 +25,6 @@ exception Drop exception IncludedFileNotCompiled of string * string -exception Macro of - GrafiteAst.loc * - (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a @@ -35,13 +32,8 @@ type 'a disambiguator_input = string * int * 'a val eval_ast : disambiguate_command: (GrafiteTypes.status -> - (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> - - disambiguate_macro: - (GrafiteTypes.status -> - (('term,'lazy_term) GrafiteAst.macro) disambiguator_input -> - Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) -> + (GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * GrafiteAst.command) -> ?do_heavy_checks:bool -> GrafiteTypes.status -> diff --git a/matita/components/grafite_engine/grafiteSync.ml b/matita/components/grafite_engine/grafiteSync.ml index 9302cbf89..16f731aab 100644 --- a/matita/components/grafite_engine/grafiteSync.ml +++ b/matita/components/grafite_engine/grafiteSync.ml @@ -27,34 +27,6 @@ open Printf -let is_a_variant obj = - match obj with - | Cic.Constant(_,_,_,_,attrs) -> - List.exists (fun x -> x = `Flavour `Variant) attrs - | _ -> false - -let uris_for_inductive_type uri obj = - match obj with - | Cic.InductiveDefinition(types,_,_,_) -> - let suri = UriManager.string_of_uri uri in - let uris,_ = - List.fold_left - (fun (acc,i) (_,_,_,constructors)-> - let is = string_of_int i in - let newacc,_ = - List.fold_left - (fun (acc,j) _ -> - let js = string_of_int j in - UriManager.uri_of_string - (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1) - (acc,1) constructors - in - newacc,i+1) - ([],1) types - in uris - | _ -> [uri] -;; - (** @return l2 \ l1 *) let uri_list_diff l2 l1 = let module S = UriManager.UriSet in diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 7f264d6fa..d68331fec 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -55,19 +55,7 @@ class status = fun (b : string) -> let add_moo_content cmds status = let content = status#moo_content_rev in - let content' = - List.fold_right - (fun cmd acc -> -(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *) - match cmd with - | GrafiteAst.Default _ - | GrafiteAst.Index _ - | GrafiteAst.Coercion _ -> - if List.mem cmd content then acc - else cmd :: acc - | _ -> cmd :: acc) - cmds content - in + let content' = cmds@content in (* prerr_endline ("new moo content: " ^ String.concat " " (List.map GrafiteAstPp.pp_command content')); *) status#set_moo_content_rev content' diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index bd633d5d2..07e502822 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -213,18 +213,8 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ;; let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)= match cmd with - | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Select (loc,uri) -> - estatus, GrafiteAst.Select(loc,uri) - | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Default _ | GrafiteAst.Drop _ | GrafiteAst.Include _ | GrafiteAst.Print _ - | GrafiteAst.Qed _ | GrafiteAst.Set _ as cmd -> estatus,cmd - | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false - | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 4392de870..e08908166 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -33,8 +33,8 @@ type tactic = val disambiguate_command: LexiconEngine.status as 'status -> ?baseuri:string -> - ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> - 'status * (Cic.term,Cic.obj) GrafiteAst.command + GrafiteAst.command Disambiguate.disambiguator_input -> + 'status * GrafiteAst.command val disambiguate_nterm : NCic.term option -> diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index e7e3234c9..fbd42cba0 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -101,10 +101,6 @@ let nmk_rec_corec ind_kind defs loc = let loc,t = mk_rec_corec ind_kind defs loc in G.NObj (loc,t) -let mk_rec_corec ind_kind defs loc = - let loc,t = mk_rec_corec ind_kind defs loc in - G.Obj (loc,t) - let npunct_of_punct = function | G.Branch loc -> G.NBranch loc | G.Shift loc -> G.NShift loc @@ -717,19 +713,6 @@ EXTEND (params,name,typ,fields) ] ]; - macro: [ - [ [ IDENT "check" ]; t = term -> - G.Check (loc, t) - | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term -> - G.Eval (loc, kind, t) - | IDENT "inline"; suri = QSTRING; params = inline_params -> - G.Inline (loc, suri, params) - | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") -> - if rew = None then G.Hint (loc, false) else G.Hint (loc,true) - | IDENT "auto"; params = auto_params -> - G.AutoInteractive (loc,params) - ] - ]; alias_spec: [ [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING -> let alpha = "[a-zA-Z]" in @@ -895,66 +878,6 @@ EXTEND G.Set (loc, n, v) | IDENT "drop" -> G.Drop loc | IDENT "print"; s = IDENT -> G.Print (loc,s) - | IDENT "qed" -> G.Qed loc - | IDENT "variant" ; name = IDENT; SYMBOL ":"; - typ = term; SYMBOL <:unicode> ; newname = IDENT -> - G.Obj (loc, - N.Theorem - (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular)) - | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term; - body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> - G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular)) - | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode> (* ≝ *); - body = term -> - G.Obj (loc, - N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular)) - | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term -> - G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular)) - | LETCOREC ; defs = let_defs -> - mk_rec_corec `CoInductive defs loc - | LETREC ; defs = let_defs -> - mk_rec_corec `Inductive defs loc - | IDENT "inductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - G.Obj (loc, N.Inductive (params, ind_types)) - | IDENT "coinductive"; spec = inductive_spec -> - let (params, ind_types) = spec in - let ind_types = (* set inductive flags to false (coinductive) *) - List.map (fun (name, _, term, ctors) -> (name, false, term, ctors)) - ind_types - in - G.Obj (loc, N.Inductive (params, ind_types)) - | IDENT "coercion" ; - t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ; - arity = OPT int ; saturations = OPT int; - composites = OPT (IDENT "nocomposites") -> - let arity = match arity with None -> 0 | Some x -> x in - let saturations = match saturations with None -> 0 | Some x -> x in - let composites = match composites with None -> true | Some _ -> false in - G.Coercion - (loc, t, composites, arity, saturations) - | IDENT "prefer" ; IDENT "coercion"; t = tactic_term -> - G.PreferCoercion (loc, t) - | IDENT "pump" ; steps = int -> - G.Pump(loc,steps) - | IDENT "inverter"; name = IDENT; IDENT "for"; - indty = tactic_term; paramspec = inverter_param_list -> - G.Inverter - (loc, name, indty, paramspec) - | IDENT "record" ; (params,name,ty,fields) = record_spec -> - G.Obj (loc, N.Record (params,name,ty,fields)) - | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> - let uris = List.map UriManager.uri_of_string uris in - G.Default (loc,what,uris) - | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ; - refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ; - refl = tactic_term -> refl ] ; - sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ; - sym = tactic_term -> sym ] ; - trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ; - trans = tactic_term -> trans ] ; - "as" ; id = IDENT -> - G.Relation (loc,id,a,aeq,refl,sym,trans) ]]; lexicon_command: [ [ IDENT "alias" ; spec = alias_spec -> @@ -988,7 +911,6 @@ EXTEND | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical -> G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct]) - | mac = macro; SYMBOL "." -> G.Macro (loc, mac) ] ]; comment: [ diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml index 72d6e981d..500c2420f 100644 --- a/matita/components/grafite_parser/test_parser.ml +++ b/matita/components/grafite_parser/test_parser.ml @@ -91,13 +91,6 @@ let process_stream istream = | Some id -> prerr_endline "removing last notation rule ..."; NotationParser.delete id) *) - | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline (sprintf "ast: %s" (NotationPp.pp_term t)); - let t' = TermContentPres.pp_ast t in - prerr_endline (sprintf "rendered ast: %s" - (NotationPp.pp_term t')); - let tbl = Hashtbl.create 0 in - dump_xml t' tbl "out.xml" | statement -> prerr_endline ("Unsupported statement: " ^ diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml index 325a8d837..33d21a93f 100644 --- a/matita/components/lexicon/lexiconSync.ml +++ b/matita/components/lexicon/lexiconSync.ml @@ -73,14 +73,6 @@ let add_alias_for_constant status uri = let new_env = build_aliases [(name,uri)] in LexiconEngine.set_proof_aliases status new_env -let add_aliases_for_object status uri = - function - Cic.InductiveDefinition (types,_,_,_) -> - add_aliases_for_inductive_def status types uri - | Cic.Constant _ -> add_alias_for_constant status uri - | Cic.Variable _ - | Cic.CurrentProof _ -> assert false - let add_aliases_for_objs status = function `Old _ -> assert false (* MATITA 1.0 *) diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index dfddae59b..071f1e00e 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -31,21 +31,12 @@ open DisambiguateTypes exception Choice_not_found of string Lazy.t -let num_choices = ref [] let nnum_choices = ref [] -let add_num_choice choice = num_choices := choice :: !num_choices let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices let has_description dsc = (fun x -> fst x = dsc) -let lookup_num_choices () = !num_choices - -let lookup_num_by_dsc dsc = - try - List.find (has_description dsc) !num_choices - with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc))) - let nlookup_num_by_dsc dsc = try List.find (has_description dsc) !nnum_choices diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli index f96d90459..cdb7004a6 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.mli +++ b/matita/components/ng_disambiguation/disambiguateChoices.mli @@ -30,20 +30,12 @@ open DisambiguateTypes (** raised by lookup_XXXX below *) exception Choice_not_found of string Lazy.t - (** register a new number choice *) -val add_num_choice: Cic.term codomain_item -> unit - (** register a new number choice *) val nadd_num_choice: NCic.term codomain_item -> unit (** {2 Choices lookup} * for user defined aliases *) -val lookup_num_choices: unit -> Cic.term codomain_item list - - (** @param dsc description (1st component of codomain_item) *) -val lookup_num_by_dsc: string -> Cic.term codomain_item - (** @param dsc description (1st component of codomain_item) *) val nlookup_num_by_dsc: string -> NCic.term codomain_item diff --git a/matita/components/ng_refiner/nCicCoercion.mli b/matita/components/ng_refiner/nCicCoercion.mli index 1094753cf..f2cd52682 100644 --- a/matita/components/ng_refiner/nCicCoercion.mli +++ b/matita/components/ng_refiner/nCicCoercion.mli @@ -13,9 +13,6 @@ type db -val set_convert_term: - (UriManager.uri -> Cic.term -> NCic.term * NCic.obj list) -> unit - class type g_status = object inherit NCicUnifHint.g_status diff --git a/matita/components/ng_tactics/continuationals.ml b/matita/components/ng_tactics/continuationals.ml index 714dad533..b10877130 100644 --- a/matita/components/ng_tactics/continuationals.ml +++ b/matita/components/ng_tactics/continuationals.ml @@ -114,10 +114,6 @@ struct | [ [], [], [], `NoTag ] -> true | _ -> false - let of_metasenv metasenv = - let goals = List.map (fun (g, _, _) -> g) metasenv in - [ zero_pos goals, [], [], `NoTag ] - let of_nmetasenv metasenv = let goals = List.map (fun (g, _) -> g) metasenv in [ zero_pos goals, [], [], `NoTag ] diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli index 293d056b3..1dcf4aa7d 100644 --- a/matita/components/ng_tactics/continuationals.mli +++ b/matita/components/ng_tactics/continuationals.mli @@ -41,7 +41,6 @@ sig val find_goal: t -> goal (** find "next" goal *) val is_empty: t -> bool (** a singleton empty level *) - val of_metasenv: Cic.metasenv -> t val of_nmetasenv: (goal * 'a) list -> t val head_switches: t -> switch list (** top level switches *) val head_goals: t -> goal list (** top level goals *) diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index dcc111a95..ab357e5c3 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -65,15 +65,8 @@ let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = let lexicon_status_ref = ref (status :> LexiconEngine.status) in let baseuri = status#baseuri in let new_status,new_objs = - match ast with - | G.Executable (_, G.Command (_, G.Coercion _)) when dump -> -(* FG: some commands can not be executed when mmas are parsed *************) -(* To be removed when mmas will be executed *) - status, `New [] - | ast -> GrafiteEngine.eval_ast ~disambiguate_command:(disambiguate_command lexicon_status_ref) - ~disambiguate_macro:((* MATITA 1.0*) fun _ -> assert false) ?do_heavy_checks status (text,prefix_len,ast) in let new_status = diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index fd5b6d4ac..480bf1210 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -193,9 +193,9 @@ object (self) self#misc#modify_font_by_name (sprintf "%s %d" BuildTimeConf.script_font !current_font_size) method set_href_callback = (function _ -> () : (string -> unit) option -> unit) - method private set_cic_info = (function _ -> () : (Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t * + method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t * (Cic.id, Cic.hypothesis) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option) option -> unit) + (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit) (* dal widget di Luca *) method load_root ~root = self#buffer#delete ~start:(self#buffer#get_iter `START) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index ae56969d3..9fc79ca92 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -190,40 +190,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length | TA.NAutoInteractive (_, (Some _,_)) -> assert false -let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = - (* no idea why ocaml wants this *) - let parsed_text_length = String.length parsed_text in - match mac with - (* REAL macro *) - | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false - | TA.Eval (_, kind, term) -> assert false (* MATITA 1.0 - let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in - let context = - match user_goal with - None -> [] - | Some n -> GrafiteTypes.get_proof_context grafite_status n in - let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in - let term = - match kind with - | `Normalize -> - CicReduction.normalize ~delta:true ~subst:[] context term - | `Simpl -> - ProofEngineReduction.simpl context term - | `Unfold None -> - ProofEngineReduction.unfold ?what:None context term - | `Unfold (Some lazy_term) -> - let what, _, _ = - lazy_term context metasenv CicUniv.empty_ugraph in - ProofEngineReduction.unfold ~what context term - | `Whd -> - CicReduction.whd ~delta:true ~subst:[] context term - in - let t_and_ty = Cic.Cast (term,ty) in - guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [(grafite_status#set_proof_status No_proof), parsed_text ],"", - parsed_text_length *) - -and eval_executable include_paths (buffer : GText.buffer) guistuff +let rec eval_executable include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text skipped_txt nonskipped_txt script ex loc = @@ -236,11 +203,6 @@ script ex loc (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 - | GrafiteEngine.Macro (_loc,lazy_macro) -> - let context = [] in - let grafite_status,macro = lazy_macro context in - eval_macro include_paths buffer guistuff grafite_status - user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro | GrafiteEngine.NMacro (_loc,macro) -> eval_nmacro include_paths buffer guistuff grafite_status user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 706981937..eb4ed6991 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -217,7 +217,6 @@ let compile atstart options fname = in let grafite_status = let rec aux_for_dump x grafite_status = - try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths grafite_status buf x @@ -226,21 +225,6 @@ let compile atstart options fname = | (g,None)::_ -> g | (g,Some _)::_ -> raise (AttemptToInsertAnAlias (g :> LexiconEngine.status)) - with MatitaEngine.EnrichedWithStatus - (GrafiteEngine.Macro (floc, f), grafite) as exn -> - match f (get_macro_context (Some grafite)) with - | _, GrafiteAst.Inline (_, _suri, _params) -> -(* - let str = - ApplyTransformation.txt_of_inline_macro style prefix suri - ?flavour - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - in - !out str; -*) - aux_for_dump x grafite - |_-> raise exn in aux_for_dump print_cb grafite_status in