From 8a660ee06d72cfee52c707bb1d8d8be3bab0d682 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Oct 2010 09:23:01 +0000 Subject: [PATCH] cicNotation* ==> notation* --- .../components/binaries/transcript/grafite.ml | 2 +- matita/components/content/.depend | 30 +++-- matita/components/content/.depend.opt | 30 +++-- matita/components/content/Makefile | 8 +- matita/components/content/cicNotationUtil.mli | 98 --------------- matita/components/content/interpretations.ml | 19 +-- matita/components/content/interpretations.mli | 14 +-- .../{cicNotationEnv.ml => notationEnv.ml} | 4 +- .../{cicNotationEnv.mli => notationEnv.mli} | 12 +- .../{cicNotationPp.ml => notationPp.ml} | 4 +- .../{cicNotationPp.mli => notationPp.mli} | 22 ++-- .../{cicNotationPt.ml => notationPt.ml} | 0 .../{cicNotationUtil.ml => notationUtil.ml} | 14 +-- matita/components/content/notationUtil.mli | 98 +++++++++++++++ .../content_pres/cicNotationParser.ml | 34 +++--- .../content_pres/cicNotationParser.mli | 20 +-- .../content_pres/cicNotationPres.ml | 20 +-- .../content_pres/cicNotationPres.mli | 4 +- .../components/content_pres/content2pres.ml | 4 +- .../components/content_pres/content2pres.mli | 2 +- .../content_pres/content2presMatcher.ml | 14 +-- .../content_pres/content2presMatcher.mli | 6 +- .../components/content_pres/sequent2pres.mli | 2 +- .../content_pres/termContentPres.ml | 88 +++++++------- .../content_pres/termContentPres.mli | 8 +- .../components/disambiguation/disambiguate.ml | 2 +- .../disambiguation/disambiguate.mli | 4 +- matita/components/grafite/grafiteAst.ml | 48 ++++---- matita/components/grafite/grafiteAstPp.ml | 32 ++--- .../grafite_engine/grafiteEngine.ml | 2 +- .../grafite_engine/nCicCoercDeclaration.mli | 8 +- .../grafite_parser/grafiteDisambiguate.ml | 14 +-- .../grafite_parser/grafiteDisambiguate.mli | 12 +- .../grafite_parser/grafiteParser.ml | 6 +- .../grafite_parser/grafiteParser.mli | 6 +- .../components/grafite_parser/test_parser.ml | 10 +- matita/components/lexicon/cicNotation.ml | 2 +- matita/components/lexicon/lexiconAst.ml | 10 +- matita/components/lexicon/lexiconAstPp.ml | 8 +- matita/components/lexicon/lexiconEngine.ml | 12 +- matita/components/lexicon/lexiconMarshal.ml | 16 +-- .../ng_cic_content/nTermCicContent.ml | 10 +- .../ng_cic_content/nTermCicContent.mli | 20 +-- .../ng_cic_content/ncic2astMatcher.ml | 6 +- .../ng_cic_content/ncic2astMatcher.mli | 2 +- .../ng_disambiguation/disambiguateChoices.ml | 2 +- .../ng_disambiguation/disambiguateChoices.mli | 4 +- .../ng_disambiguation/nCicDisambiguate.ml | 114 +++++++++--------- .../ng_disambiguation/nCicDisambiguate.mli | 6 +- matita/components/ng_tactics/nCicElim.ml | 68 +++++------ matita/components/ng_tactics/nCicElim.mli | 4 +- matita/components/ng_tactics/nDestructTac.ml | 114 +++++++++--------- matita/components/ng_tactics/nInversion.ml | 28 ++--- matita/components/ng_tactics/nTacStatus.ml | 2 +- matita/components/ng_tactics/nTacStatus.mli | 2 +- matita/components/ng_tactics/nTactics.ml | 2 +- matita/components/ng_tactics/nnAuto.ml | 16 +-- matita/components/ng_tactics/nnAuto.mli | 2 +- matita/matita/matitaEngine.mli | 8 +- matita/matita/matitaMathView.ml | 2 +- matita/matita/matitaScript.ml | 6 +- matita/matita/matitacLib.ml | 12 +- 62 files changed, 580 insertions(+), 599 deletions(-) delete mode 100644 matita/components/content/cicNotationUtil.mli rename matita/components/content/{cicNotationEnv.ml => notationEnv.ml} (97%) rename matita/components/content/{cicNotationEnv.mli => notationEnv.mli} (90%) rename matita/components/content/{cicNotationPp.ml => notationPp.ml} (99%) rename matita/components/content/{cicNotationPp.mli => notationPp.mli} (73%) rename matita/components/content/{cicNotationPt.ml => notationPt.ml} (100%) rename matita/components/content/{cicNotationUtil.ml => notationUtil.ml} (97%) create mode 100644 matita/components/content/notationUtil.mli diff --git a/matita/components/binaries/transcript/grafite.ml b/matita/components/binaries/transcript/grafite.ml index d44a17c58..719b4854a 100644 --- a/matita/components/binaries/transcript/grafite.ml +++ b/matita/components/binaries/transcript/grafite.ml @@ -27,7 +27,7 @@ module T = Types module O = Options module UM = UriManager -module NP = CicNotationPp +module NP = NotationPp module GP = GrafiteAstPp module G = GrafiteAst module H = HExtlib diff --git a/matita/components/content/.depend b/matita/components/content/.depend index 50d486b4f..a4aeebd43 100644 --- a/matita/components/content/.depend +++ b/matita/components/content/.depend @@ -1,19 +1,17 @@ content.cmi: -cicNotationUtil.cmi: cicNotationPt.cmo -cicNotationEnv.cmi: cicNotationPt.cmo -cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi -interpretations.cmi: cicNotationPt.cmo -cicNotationPt.cmo: -cicNotationPt.cmx: +notationUtil.cmi: +notationEnv.cmi: +notationPp.cmi: +interpretations.cmi: notationPt.cmo +notationPt.cmo: +notationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi -cicNotationUtil.cmo: cicNotationPt.cmo cicNotationUtil.cmi -cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi -cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi -cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi -cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi -cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmo \ - interpretations.cmi -interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ - interpretations.cmi +notationUtil.cmo: notationPt.cmo notationUtil.cmi +notationUtil.cmx: notationPt.cmx notationUtil.cmi +notationEnv.cmo: notationUtil.cmi notationPt.cmo notationEnv.cmi +notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo: notationPt.cmo notationEnv.cmi notationPp.cmi +notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi +interpretations.cmo: notationUtil.cmi notationPt.cmo interpretations.cmi +interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 9af10948d..a964a1fca 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,19 +1,17 @@ content.cmi: -cicNotationUtil.cmi: cicNotationPt.cmx -cicNotationEnv.cmi: cicNotationPt.cmx -cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi -interpretations.cmi: cicNotationPt.cmx -cicNotationPt.cmo: -cicNotationPt.cmx: +notationUtil.cmi: +notationEnv.cmi: +notationPp.cmi: +interpretations.cmi: notationPt.cmx +notationPt.cmo: +notationPt.cmx: content.cmo: content.cmi content.cmx: content.cmi -cicNotationUtil.cmo: cicNotationPt.cmx cicNotationUtil.cmi -cicNotationUtil.cmx: cicNotationPt.cmx cicNotationUtil.cmi -cicNotationEnv.cmo: cicNotationUtil.cmi cicNotationPt.cmx cicNotationEnv.cmi -cicNotationEnv.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmi -cicNotationPp.cmo: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmi -cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi -interpretations.cmo: cicNotationUtil.cmi cicNotationPt.cmx \ - interpretations.cmi -interpretations.cmx: cicNotationUtil.cmx cicNotationPt.cmx \ - interpretations.cmi +notationUtil.cmo: notationPt.cmx notationUtil.cmi +notationUtil.cmx: notationPt.cmx notationUtil.cmi +notationEnv.cmo: notationUtil.cmi notationPt.cmx notationEnv.cmi +notationEnv.cmx: notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo: notationPt.cmx notationEnv.cmi notationPp.cmi +notationPp.cmx: notationPt.cmx notationEnv.cmx notationPp.cmi +interpretations.cmo: notationUtil.cmi notationPt.cmx interpretations.cmi +interpretations.cmx: notationUtil.cmx notationPt.cmx interpretations.cmi diff --git a/matita/components/content/Makefile b/matita/components/content/Makefile index 2f1a3896a..5ea3ee796 100644 --- a/matita/components/content/Makefile +++ b/matita/components/content/Makefile @@ -3,13 +3,13 @@ PREDICATES = INTERFACE_FILES = \ content.mli \ - cicNotationUtil.mli \ - cicNotationEnv.mli \ - cicNotationPp.mli \ + notationUtil.mli \ + notationEnv.mli \ + notationPp.mli \ interpretations.mli \ $(NULL) IMPLEMENTATION_FILES = \ - cicNotationPt.ml \ + notationPt.ml \ $(INTERFACE_FILES:%.mli=%.ml) include ../../Makefile.defs diff --git a/matita/components/content/cicNotationUtil.mli b/matita/components/content/cicNotationUtil.mli deleted file mode 100644 index 77350a2ac..000000000 --- a/matita/components/content/cicNotationUtil.mli +++ /dev/null @@ -1,98 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -val fresh_name: unit -> string - -val variables_of_term: CicNotationPt.term -> CicNotationPt.pattern_variable list -val names_of_term: CicNotationPt.term -> string list - - (** extract all keywords (i.e. string literals) from a level 1 pattern *) -val keywords_of_term: CicNotationPt.term -> string list - -val visit_ast: - ?special_k:(CicNotationPt.term -> CicNotationPt.term) -> - ?map_xref_option:(CicNotationPt.href option -> CicNotationPt.href option) -> - ?map_case_indty:(CicNotationPt.case_indtype option -> - CicNotationPt.case_indtype option) -> - ?map_case_outtype:((CicNotationPt.term -> CicNotationPt.term) -> - CicNotationPt.term option -> CicNotationPt.term - option) -> - (CicNotationPt.term -> CicNotationPt.term) -> - CicNotationPt.term -> - CicNotationPt.term - -val visit_layout: - (CicNotationPt.term -> CicNotationPt.term) -> - CicNotationPt.layout_pattern -> - CicNotationPt.layout_pattern - -val visit_magic: - (CicNotationPt.term -> CicNotationPt.term) -> - CicNotationPt.magic_term -> - CicNotationPt.magic_term - -val visit_variable: - (CicNotationPt.term -> CicNotationPt.term) -> - CicNotationPt.pattern_variable -> - CicNotationPt.pattern_variable - -val strip_attributes: CicNotationPt.term -> CicNotationPt.term - - (** @return the list of proper (i.e. non recursive) IdRef of a term *) -val get_idrefs: CicNotationPt.term -> string list - - (** generalization of List.combine to n lists *) -val ncombine: 'a list list -> 'a list list - -val string_of_literal: CicNotationPt.literal -> string - -val dress: sep:'a -> 'a list -> 'a list -val dressn: sep:'a list -> 'a list -> 'a list - -val boxify: CicNotationPt.term list -> CicNotationPt.term -val group: CicNotationPt.term list -> CicNotationPt.term -val ungroup: CicNotationPt.term list -> CicNotationPt.term list - -val find_appl_pattern_uris: - CicNotationPt.cic_appl_pattern -> - [`Uri of UriManager.uri | `NRef of NReference.reference] list - -val find_branch: - CicNotationPt.term -> CicNotationPt.term - -val cic_name_of_name: CicNotationPt.term -> Cic.name -val name_of_cic_name: Cic.name -> CicNotationPt.term - - (** Symbol/Numbers instances *) - -val freshen_term: CicNotationPt.term -> CicNotationPt.term -val freshen_obj: CicNotationPt.term CicNotationPt.obj -> CicNotationPt.term CicNotationPt.obj - - (** Notation id handling *) - -type notation_id - -val fresh_id: unit -> notation_id - diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index 599a0704e..c7bfa5768 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -27,7 +27,7 @@ open Printf -module Ast = CicNotationPt +module Ast = NotationPt module Obj = LibraryObjects let debug = false @@ -42,21 +42,6 @@ type term_info = uri: (Cic.id, UriManager.uri) Hashtbl.t; } -let destroy_nat annterm = - let is_zero = function - | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true - | _ -> false - in - let is_succ = function - | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true - | _ -> false - in - let rec aux acc = function - | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl - | t when is_zero t -> Some acc - | _ -> None in - aux 0 annterm - (* persistent state *) let initial_level2_patterns32 () = Hashtbl.create 211 @@ -108,7 +93,7 @@ let instantiate32 term_info idrefs env symbol args = in let rec add_lambda t n = if n > 0 then - let name = CicNotationUtil.fresh_name () in + let name = NotationUtil.fresh_name () in Ast.Binder (`Lambda, (Ast.Ident (name, None), None), Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) else diff --git a/matita/components/content/interpretations.mli b/matita/components/content/interpretations.mli index 259a7b1ac..222a340f4 100644 --- a/matita/components/content/interpretations.mli +++ b/matita/components/content/interpretations.mli @@ -30,15 +30,15 @@ type interpretation_id val add_interpretation: string -> (* id / description *) - string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *) - CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) + NotationPt.cic_appl_pattern -> (* level 3 pattern *) interpretation_id (** @raise Interpretation_not_found *) val lookup_interpretations: ?sorted:bool -> string -> (* symbol *) - (string * CicNotationPt.argument_pattern list * - CicNotationPt.cic_appl_pattern) list + (string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) list exception Interpretation_not_found @@ -60,7 +60,7 @@ val instantiate_appl_pattern: mk_implicit:(bool -> 'term) -> term_of_uri : (UriManager.uri -> 'term) -> term_of_nref : (NReference.reference -> 'term) -> - (string * 'term) list -> CicNotationPt.cic_appl_pattern -> + (string * 'term) list -> NotationPt.cic_appl_pattern -> 'term val push: unit -> unit @@ -70,8 +70,8 @@ val pop: unit -> unit val find_level2_patterns32: int -> string * string * - CicNotationPt.argument_pattern list * CicNotationPt.cic_appl_pattern + NotationPt.argument_pattern list * NotationPt.cic_appl_pattern val add_load_patterns32: - ((bool * CicNotationPt.cic_appl_pattern * int) list -> unit) -> unit + ((bool * NotationPt.cic_appl_pattern * int) list -> unit) -> unit val init: unit -> unit diff --git a/matita/components/content/cicNotationEnv.ml b/matita/components/content/notationEnv.ml similarity index 97% rename from matita/components/content/cicNotationEnv.ml rename to matita/components/content/notationEnv.ml index 5b4190eb8..e95b3ab51 100644 --- a/matita/components/content/cicNotationEnv.ml +++ b/matita/components/content/notationEnv.ml @@ -25,7 +25,7 @@ (* $Id$ *) -module Ast = CicNotationPt +module Ast = NotationPt type value = | TermValue of Ast.term @@ -125,7 +125,7 @@ let rec well_typed ty value = let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty)) let declarations_of_term p = - List.map declaration_of_var (CicNotationUtil.variables_of_term p) + List.map declaration_of_var (NotationUtil.variables_of_term p) let rec combine decls values = match decls, values with diff --git a/matita/components/content/cicNotationEnv.mli b/matita/components/content/notationEnv.mli similarity index 90% rename from matita/components/content/cicNotationEnv.mli rename to matita/components/content/notationEnv.mli index aa937d00c..858af233c 100644 --- a/matita/components/content/cicNotationEnv.mli +++ b/matita/components/content/notationEnv.mli @@ -26,7 +26,7 @@ (** {2 Types} *) type value = - | TermValue of CicNotationPt.term + | TermValue of NotationPt.term | StringValue of string | NumValue of string | OptValue of value option @@ -50,13 +50,13 @@ type declaration = string * value_type type binding = string * (value_type * value) type t = binding list -val declaration_of_var: CicNotationPt.pattern_variable -> declaration -val value_of_term: CicNotationPt.term -> value -val term_of_value: value -> CicNotationPt.term +val declaration_of_var: NotationPt.pattern_variable -> declaration +val value_of_term: NotationPt.term -> value +val term_of_value: value -> NotationPt.term val well_typed: value_type -> value -> bool val declarations_of_env: t -> declaration list -val declarations_of_term: CicNotationPt.term -> declaration list +val declarations_of_term: NotationPt.term -> declaration list val combine: declaration list -> value list -> t (** @raise Invalid_argument *) (** {2 Environment lookup} *) @@ -65,7 +65,7 @@ val lookup_value: t -> string -> value (** @raise Value_not_found *) (** lookup_* functions below may raise Value_not_found and Type_mismatch *) -val lookup_term: t -> string -> CicNotationPt.term +val lookup_term: t -> string -> NotationPt.term val lookup_string: t -> string -> string val lookup_num: t -> string -> string val lookup_opt: t -> string -> value option diff --git a/matita/components/content/cicNotationPp.ml b/matita/components/content/notationPp.ml similarity index 99% rename from matita/components/content/cicNotationPp.ml rename to matita/components/content/notationPp.ml index f94891375..a101747df 100644 --- a/matita/components/content/cicNotationPp.ml +++ b/matita/components/content/notationPp.ml @@ -27,8 +27,8 @@ open Printf -module Ast = CicNotationPt -module Env = CicNotationEnv +module Ast = NotationPt +module Env = NotationEnv (* when set to true debugging information, not in sync with input syntax, will * be added to the output of pp_term. diff --git a/matita/components/content/cicNotationPp.mli b/matita/components/content/notationPp.mli similarity index 73% rename from matita/components/content/cicNotationPp.mli rename to matita/components/content/notationPp.mli index d883ddfc6..51a284e2e 100644 --- a/matita/components/content/cicNotationPp.mli +++ b/matita/components/content/notationPp.mli @@ -31,25 +31,25 @@ * * TODO the proper implementation of a pp_obj function like the one below should * be as follows. Change its type to - * pp_obj: CicNotationPt.obj -> CicNotationPres.markup + * pp_obj: NotationPt.obj -> NotationPres.markup * and parametrize it over a function with the following type - * pp_term: CicNotationPt.term -> CicNotationPres.markup + * pp_term: NotationPt.term -> NotationPres.markup * The obtained markup can then be printed using CicNotationPres.print_xml or * BoxPp.render_to_string(s) *) -val pp_term: CicNotationPt.term -> string -val pp_obj: ('term -> string) -> 'term CicNotationPt.obj -> string +val pp_term: NotationPt.term -> string +val pp_obj: ('term -> string) -> 'term NotationPt.obj -> string -val pp_env: CicNotationEnv.t -> string -val pp_value: CicNotationEnv.value -> string -val pp_value_type: CicNotationEnv.value_type -> string +val pp_env: NotationEnv.t -> string +val pp_value: NotationEnv.value -> string +val pp_value_type: NotationEnv.value_type -> string -val pp_pos: CicNotationPt.child_pos -> string -val pp_attribute: CicNotationPt.term_attribute -> string +val pp_pos: NotationPt.child_pos -> string +val pp_attribute: NotationPt.term_attribute -> string -val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string +val pp_cic_appl_pattern: NotationPt.cic_appl_pattern -> string (** non re-entrant change of pp_term function above *) -val set_pp_term: (CicNotationPt.term -> string) -> unit +val set_pp_term: (NotationPt.term -> string) -> unit diff --git a/matita/components/content/cicNotationPt.ml b/matita/components/content/notationPt.ml similarity index 100% rename from matita/components/content/cicNotationPt.ml rename to matita/components/content/notationPt.ml diff --git a/matita/components/content/cicNotationUtil.ml b/matita/components/content/notationUtil.ml similarity index 97% rename from matita/components/content/cicNotationUtil.ml rename to matita/components/content/notationUtil.ml index 7eccd7901..9b663dfc6 100644 --- a/matita/components/content/cicNotationUtil.ml +++ b/matita/components/content/notationUtil.ml @@ -25,7 +25,7 @@ (* $Id$ *) -module Ast = CicNotationPt +module Ast = NotationPt let visit_ast ?(special_k = fun _ -> assert false) ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x) @@ -400,20 +400,20 @@ let freshen_obj obj = List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t)) in match obj with - | CicNotationPt.Inductive (params, indtypes) -> + | NotationPt.Inductive (params, indtypes) -> let indtypes = List.map (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors)) indtypes in - CicNotationPt.Inductive (freshen_capture_variables params, indtypes) - | CicNotationPt.Theorem (flav, n, t, ty_opt,p) -> + NotationPt.Inductive (freshen_capture_variables params, indtypes) + | NotationPt.Theorem (flav, n, t, ty_opt,p) -> let ty_opt = match ty_opt with None -> None | Some ty -> Some (freshen_term ty) in - CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt,p) - | CicNotationPt.Record (params, n, ty, fields) -> - CicNotationPt.Record (freshen_capture_variables params, n, + NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p) + | NotationPt.Record (params, n, ty, fields) -> + NotationPt.Record (freshen_capture_variables params, n, freshen_term ty, freshen_name_ty_b fields) let freshen_term = freshen_term ?index:None diff --git a/matita/components/content/notationUtil.mli b/matita/components/content/notationUtil.mli new file mode 100644 index 000000000..6194fc855 --- /dev/null +++ b/matita/components/content/notationUtil.mli @@ -0,0 +1,98 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val fresh_name: unit -> string + +val variables_of_term: NotationPt.term -> NotationPt.pattern_variable list +val names_of_term: NotationPt.term -> string list + + (** extract all keywords (i.e. string literals) from a level 1 pattern *) +val keywords_of_term: NotationPt.term -> string list + +val visit_ast: + ?special_k:(NotationPt.term -> NotationPt.term) -> + ?map_xref_option:(NotationPt.href option -> NotationPt.href option) -> + ?map_case_indty:(NotationPt.case_indtype option -> + NotationPt.case_indtype option) -> + ?map_case_outtype:((NotationPt.term -> NotationPt.term) -> + NotationPt.term option -> NotationPt.term + option) -> + (NotationPt.term -> NotationPt.term) -> + NotationPt.term -> + NotationPt.term + +val visit_layout: + (NotationPt.term -> NotationPt.term) -> + NotationPt.layout_pattern -> + NotationPt.layout_pattern + +val visit_magic: + (NotationPt.term -> NotationPt.term) -> + NotationPt.magic_term -> + NotationPt.magic_term + +val visit_variable: + (NotationPt.term -> NotationPt.term) -> + NotationPt.pattern_variable -> + NotationPt.pattern_variable + +val strip_attributes: NotationPt.term -> NotationPt.term + + (** @return the list of proper (i.e. non recursive) IdRef of a term *) +val get_idrefs: NotationPt.term -> string list + + (** generalization of List.combine to n lists *) +val ncombine: 'a list list -> 'a list list + +val string_of_literal: NotationPt.literal -> string + +val dress: sep:'a -> 'a list -> 'a list +val dressn: sep:'a list -> 'a list -> 'a list + +val boxify: NotationPt.term list -> NotationPt.term +val group: NotationPt.term list -> NotationPt.term +val ungroup: NotationPt.term list -> NotationPt.term list + +val find_appl_pattern_uris: + NotationPt.cic_appl_pattern -> + [`Uri of UriManager.uri | `NRef of NReference.reference] list + +val find_branch: + NotationPt.term -> NotationPt.term + +val cic_name_of_name: NotationPt.term -> Cic.name +val name_of_cic_name: Cic.name -> NotationPt.term + + (** Symbol/Numbers instances *) + +val freshen_term: NotationPt.term -> NotationPt.term +val freshen_obj: NotationPt.term NotationPt.obj -> NotationPt.term NotationPt.obj + + (** Notation id handling *) + +type notation_id + +val fresh_id: unit -> notation_id + diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 829e78b6d..18c52b7cf 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -27,8 +27,8 @@ open Printf -module Ast = CicNotationPt -module Env = CicNotationEnv +module Ast = NotationPt +module Env = NotationEnv exception Parse_error of string exception Level_not_found of int @@ -110,7 +110,7 @@ type binding = | Env of (string * Env.value_type) list let make_action action bindings = - let rec aux (vl : CicNotationEnv.t) = + let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) @@ -136,7 +136,7 @@ let make_action action bindings = (fun (v:'a list) -> aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl) | Env _ :: tl -> - Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) + Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl) (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -160,7 +160,7 @@ let extract_term_production pattern = | Ast.Magic m -> aux_magic m | Ast.Variable v -> aux_variable v | t -> - prerr_endline (CicNotationPp.pp_term t); + prerr_endline (NotationPp.pp_term t); assert false and aux_literal = function @@ -192,7 +192,7 @@ let extract_term_production pattern = match magic with | Ast.Opt p -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) = + let action (env_opt : NotationEnv.t option) (loc : Ast.location) = match env_opt with | Some env -> List.map Env.opt_binding_some env | None -> List.map Env.opt_binding_of_name p_names @@ -204,8 +204,8 @@ let extract_term_production pattern = | Ast.List0 (p, _) | Ast.List1 (p, _) -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_list : CicNotationEnv.t list) (loc : Ast.location) = - CicNotationEnv.coalesce_env p_names env_list + let action (env_list : NotationEnv.t list) (loc : Ast.location) = + NotationEnv.coalesce_env p_names env_list in let gram_of_list s = match magic with @@ -232,7 +232,7 @@ let extract_term_production pattern = let p_bindings, p_atoms = List.split (aux p) in let p_names = flatten_opt p_bindings in let action = - make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env) + make_action (fun (env : NotationEnv.t) (loc : Ast.location) -> env) p_bindings in p_bindings, p_atoms, p_names, action @@ -256,7 +256,7 @@ let compare_rule_id x y = let initial_owned_keywords () = Hashtbl.create 23 let owned_keywords = ref (initial_owned_keywords ()) -type checked_l1_pattern = CL1P of CicNotationPt.term * int +type checked_l1_pattern = CL1P of NotationPt.term * int let check_l1_pattern level1_pattern pponly level associativity = let variables = ref 0 in @@ -328,7 +328,7 @@ let check_l1_pattern level1_pattern pponly level associativity = raise (Parse_error ("You can not specify an associative notation " ^ "at level "^string_of_int min_precedence ^ "; increase it")); let cp = aux level1_pattern in -(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *) +(* prerr_endline ("checked_pattern: " ^ NotationPp.pp_term cp); *) if !variables <> 2 && associativity <> Gramext.NonA then raise (Parse_error ("Exactly 2 variables must be specified in an "^ "associative notation")); @@ -348,11 +348,11 @@ let extend (CL1P (level1_pattern,precedence)) action = Some (*Gramext.NonA*) Gramext.NonA, [ p_atoms, (make_action - (fun (env: CicNotationEnv.t) (loc: Ast.location) -> + (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings) ]]] in - let keywords = CicNotationUtil.keywords_of_term level1_pattern in + let keywords = NotationUtil.keywords_of_term level1_pattern in let rule_id = p_atoms in List.iter CicNotationLexer.add_level2_ast_keyword keywords; Hashtbl.add !owned_keywords rule_id keywords; (* keywords may be [] *) @@ -424,7 +424,7 @@ EXTEND GLOBAL: level1_pattern; level1_pattern: [ - [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ] + [ p = l1_pattern; EOI -> fun l -> NotationUtil.boxify (p l) ] ]; l1_pattern: [ [ p = LIST1 l1_simple_pattern -> @@ -513,9 +513,9 @@ EXTEND | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Maction (List.map (fun x -> - CicNotationUtil.group (x l)) m))) + NotationUtil.group (x l)) m))) | LPAREN; p = l1_pattern; RPAREN -> - return_term_of_level loc (fun l -> CicNotationUtil.group (p l)) + return_term_of_level loc (fun l -> NotationUtil.group (p l)) ] | "simple" NONA [ i = IDENT -> @@ -670,7 +670,7 @@ EXTEND let rec find_arg name n = function | [] -> Ast.fail loc (sprintf "Argument %s not found" - (CicNotationPp.pp_term name)) + (NotationPp.pp_term name)) | (l,_) :: tl -> (match position_of name 0 l with | None, len -> find_arg name (n + len) tl diff --git a/matita/components/content_pres/cicNotationParser.mli b/matita/components/content_pres/cicNotationParser.mli index ba9003e90..c25ba1864 100644 --- a/matita/components/content_pres/cicNotationParser.mli +++ b/matita/components/content_pres/cicNotationParser.mli @@ -26,17 +26,17 @@ exception Parse_error of string exception Level_not_found of int -type checked_l1_pattern = private CL1P of CicNotationPt.term * int +type checked_l1_pattern = private CL1P of NotationPt.term * int (** {2 Parsing functions} *) (** concrete syntax pattern: notation level 1, the * integer is the precedence *) -val parse_level1_pattern: int -> Ulexing.lexbuf -> CicNotationPt.term +val parse_level1_pattern: int -> Ulexing.lexbuf -> NotationPt.term (** AST pattern: notation level 2 *) -val parse_level2_ast: Ulexing.lexbuf -> CicNotationPt.term -val parse_level2_meta: Ulexing.lexbuf -> CicNotationPt.term +val parse_level2_ast: Ulexing.lexbuf -> NotationPt.term +val parse_level2_meta: Ulexing.lexbuf -> NotationPt.term (** {2 Grammar extension} *) @@ -45,11 +45,11 @@ type rule_id val compare_rule_id : rule_id -> rule_id -> int val check_l1_pattern: (* level1_pattern, pponly, precedence, assoc *) - CicNotationPt.term -> bool -> int -> Gramext.g_assoc -> checked_l1_pattern + NotationPt.term -> bool -> int -> Gramext.g_assoc -> checked_l1_pattern val extend: checked_l1_pattern -> - (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) -> + (NotationEnv.t -> NotationPt.location -> NotationPt.term) -> rule_id val delete: rule_id -> unit @@ -59,16 +59,16 @@ val delete: rule_id -> unit val level2_ast_grammar: unit -> Grammar.g -val term : unit -> CicNotationPt.term Grammar.Entry.e +val term : unit -> NotationPt.term Grammar.Entry.e val let_defs : unit -> - (CicNotationPt.term CicNotationPt.capture_variable list * CicNotationPt.term CicNotationPt.capture_variable * CicNotationPt.term * int) list + (NotationPt.term NotationPt.capture_variable list * NotationPt.term NotationPt.capture_variable * NotationPt.term * int) list Grammar.Entry.e val protected_binder_vars : unit -> - (CicNotationPt.term list * CicNotationPt.term option) Grammar.Entry.e + (NotationPt.term list * NotationPt.term option) Grammar.Entry.e -val parse_term: Ulexing.lexbuf -> CicNotationPt.term +val parse_term: Ulexing.lexbuf -> NotationPt.term (** {2 Debugging} *) diff --git a/matita/components/content_pres/cicNotationPres.ml b/matita/components/content_pres/cicNotationPres.ml index 82a326c48..26370ff22 100644 --- a/matita/components/content_pres/cicNotationPres.ml +++ b/matita/components/content_pres/cicNotationPres.ml @@ -27,7 +27,7 @@ open Printf -module Ast = CicNotationPt +module Ast = NotationPt module Mpres = Mpresentation type mathml_markup = boxml_markup Mpres.mpres @@ -102,7 +102,7 @@ let box_of mathonly spec attrs children = let kind, spacing, indent = spec in let dress children = if spacing then - CicNotationUtil.dress small_skip children + NotationUtil.dress small_skip children else children in @@ -283,7 +283,7 @@ let render ~lookup_uri ?(prec=(-1)) = let substs' = box_of mathonly (A.H, false, false) [] (open_brace - :: (CicNotationUtil.dress semicolon + :: (NotationUtil.dress semicolon (List.map (fun (name, t) -> box_of mathonly (A.H, false, false) [] [ @@ -299,7 +299,7 @@ let render ~lookup_uri ?(prec=(-1)) = let local_context l = box_of mathonly (A.H, false, false) [] ([ Mpres.Mtext ([], "[") ] @ - (CicNotationUtil.dress (Mpres.Mtext ([], ";")) + (NotationUtil.dress (Mpres.Mtext ([], ";")) (List.map (function | None -> Mpres.Mtext ([], "_") @@ -316,7 +316,7 @@ let render ~lookup_uri ?(prec=(-1)) = | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) | t -> - prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t); + prerr_endline ("unexpected ast: " ^ NotationPp.pp_term t); assert false and aux_attributes xmlattrs mathonly xref prec t = let reset = ref false in @@ -357,7 +357,7 @@ let render ~lookup_uri ?(prec=(-1)) = then ((*prerr_endline "reset";*)t') else add_parens child_prec prec t') in -(* prerr_endline (CicNotationPp.pp_term t); *) +(* prerr_endline (NotationPp.pp_term t); *) aux_attribute t and aux_literal xmlattrs xref prec l = let attrs = make_href xmlattrs xref in @@ -400,7 +400,7 @@ let render ~lookup_uri ?(prec=(-1)) = | A.Box ((_, spacing, _) as kind, terms) -> let children = aux_children mathonly spacing xref prec - (CicNotationUtil.ungroup terms) + (NotationUtil.ungroup terms) in box_of mathonly kind attrs children | A.Mstyle (l,terms) -> @@ -408,19 +408,19 @@ let render ~lookup_uri ?(prec=(-1)) = (List.map (fun (k,v) -> None,k,v) l, box_of mathonly (A.H, false, false) attrs (aux_children mathonly false xref prec - (CicNotationUtil.ungroup terms))) + (NotationUtil.ungroup terms))) | A.Mpadded (l,terms) -> Mpres.Mpadded (List.map (fun (k,v) -> None,k,v) l, box_of mathonly (A.H, false, false) attrs (aux_children mathonly false xref prec - (CicNotationUtil.ungroup terms))) + (NotationUtil.ungroup terms))) | A.Maction alternatives -> toggle_action (List.map invoke_reinit alternatives) | A.Group terms -> let children = aux_children mathonly false xref prec - (CicNotationUtil.ungroup terms) + (NotationUtil.ungroup terms) in box_of mathonly (A.H, false, false) attrs children | A.Break -> assert false (* TODO? *) diff --git a/matita/components/content_pres/cicNotationPres.mli b/matita/components/content_pres/cicNotationPres.mli index 6a25e5672..3c9f0ce15 100644 --- a/matita/components/content_pres/cicNotationPres.mli +++ b/matita/components/content_pres/cicNotationPres.mli @@ -41,7 +41,7 @@ val lookup_uri: (Cic.id,UriManager.uri) Hashtbl.t -> Cic.id -> string option * @param ids_to_uris mapping id -> uri for hyperlinking * @param prec precedence level *) val render: - lookup_uri:(Cic.id -> string option) -> ?prec:int -> CicNotationPt.term -> + lookup_uri:(Cic.id -> string option) -> ?prec:int -> NotationPt.term -> markup (** level 0 -> xml stream *) @@ -50,7 +50,7 @@ val print_xml: markup -> Xml.token Stream.t (* |+* level 1 -> xml stream * @param ids_to_uris +| val render_to_boxml: - (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t *) + (Cic.id, string) Hashtbl.t -> NotationPt.term -> Xml.token Stream.t *) val print_box: boxml_markup -> Xml.token Stream.t val print_mpres: mathml_markup -> Xml.token Stream.t diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml index 617c9ddca..cd2e62c21 100644 --- a/matita/components/content_pres/content2pres.ml +++ b/matita/components/content_pres/content2pres.ml @@ -916,7 +916,7 @@ let definition2pres ?recno term2pres d = let name = match d.Content.def_name with Some x -> x|_->assert false in let rno = match recno with None -> -1 (* cofix *) | Some x -> x in let ty = d.Content.def_type in - let module P = CicNotationPt in + let module P = NotationPt in let rec split_pi i t = if i <= 1 then match t with @@ -994,7 +994,7 @@ let njoint_def2pres term2pres joint_kind defs = let ncontent2pres0 ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres - (id,params,metasenv,obj : CicNotationPt.term Content.cobj) + (id,params,metasenv,obj : NotationPt.term Content.cobj) = match obj with | `Def (Content.Const, thesis, `Proof p) -> diff --git a/matita/components/content_pres/content2pres.mli b/matita/components/content_pres/content2pres.mli index 57e75a978..4b9fc4498 100644 --- a/matita/components/content_pres/content2pres.mli +++ b/matita/components/content_pres/content2pres.mli @@ -35,6 +35,6 @@ val ncontent2pres: ?skip_initial_lambdas:int -> ?skip_thm_and_qed:bool -> ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> - CicNotationPt.term Content.cobj -> + NotationPt.term Content.cobj -> CicNotationPres.boxml_markup diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml index 23f620924..2a432d332 100644 --- a/matita/components/content_pres/content2presMatcher.ml +++ b/matita/components/content_pres/content2presMatcher.ml @@ -27,10 +27,10 @@ open Printf -module Ast = CicNotationPt -module Env = CicNotationEnv -module Pp = CicNotationPp -module Util = CicNotationUtil +module Ast = NotationPt +module Env = NotationEnv +module Pp = NotationPp +module Util = NotationUtil let get_tag term0 = let subterms = ref [] in @@ -39,7 +39,7 @@ let get_tag term0 = Ast.Implicit `JustOne in let rec aux t = - CicNotationUtil.visit_ast + NotationUtil.visit_ast ~map_xref_option:(fun _ -> None) ~map_case_indty:(fun _ -> None) ~map_case_outtype:(fun _ _ -> None) @@ -67,8 +67,8 @@ struct | _ -> PatternMatcher.Constructor let tag_of_pattern = get_tag let tag_of_term t = get_tag t - let string_of_term = CicNotationPp.pp_term - let string_of_pattern = CicNotationPp.pp_term + let string_of_term = NotationPp.pp_term + let string_of_pattern = NotationPp.pp_term end module M = PatternMatcher.Matcher (Pattern21) diff --git a/matita/components/content_pres/content2presMatcher.mli b/matita/components/content_pres/content2presMatcher.mli index 86b97b6d8..4ddfb7129 100644 --- a/matita/components/content_pres/content2presMatcher.mli +++ b/matita/components/content_pres/content2presMatcher.mli @@ -27,8 +27,8 @@ module Matcher21: sig (** @param l2_patterns level 2 (AST) patterns *) val compiler : - (CicNotationPt.term * int) list -> - (CicNotationPt.term -> - (CicNotationEnv.t * CicNotationPt.term list * int) option) + (NotationPt.term * int) list -> + (NotationPt.term -> + (NotationEnv.t * NotationPt.term list * int) option) end diff --git a/matita/components/content_pres/sequent2pres.mli b/matita/components/content_pres/sequent2pres.mli index 38570ba64..bf2a30f55 100644 --- a/matita/components/content_pres/sequent2pres.mli +++ b/matita/components/content_pres/sequent2pres.mli @@ -34,5 +34,5 @@ val nsequent2pres : ids_to_nrefs:(NTermCicContent.id, NReference.reference) Hashtbl.t -> - subst:NCic.substitution -> CicNotationPt.term Content.conjecture -> + subst:NCic.substitution -> NotationPt.term Content.conjecture -> CicNotationPres.boxml_markup diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml index 68cc4ccbb..28bcbe314 100644 --- a/matita/components/content_pres/termContentPres.ml +++ b/matita/components/content_pres/termContentPres.ml @@ -27,8 +27,8 @@ open Printf -module Ast = CicNotationPt -module Env = CicNotationEnv +module Ast = NotationPt +module Env = NotationEnv let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -122,7 +122,7 @@ let pp_ast0 t k = (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl in add_level_info Ast.apply_prec - (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts))) + (hovbox true true (NotationUtil.dress break (aux_args 70 ts))) | Ast.Binder (binder_kind, (id, ty), body) -> add_level_info Ast.binder_prec (hvbox false true @@ -275,7 +275,7 @@ let pp_ast0 t k = | Ast.Uri (_, None) | Ast.Uri (_, Some []) | Ast.Literal _ | Ast.UserInput as leaf -> leaf - | t -> CicNotationUtil.visit_ast ~special_k k t + | t -> NotationUtil.visit_ast ~special_k k t and aux_sort sort_kind = xml_of_sort sort_kind and aux_ty = function | None -> builtin_symbol "?" @@ -289,7 +289,7 @@ let pp_ast0 t k = and special_k = function | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) | t -> - prerr_endline ("unexpected special: " ^ CicNotationPp.pp_term t); + prerr_endline ("unexpected special: " ^ NotationPp.pp_term t); assert false in aux t @@ -338,13 +338,13 @@ let instantiate21 idrefs env l1 = function Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, subst_singleton pos env t) - | t -> CicNotationUtil.group (subst pos env t) + | t -> NotationUtil.group (subst pos env t) and subst pos env = function | Ast.AttributedTerm (attr, t) -> -(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *) +(* prerr_endline ("loosing attribute " ^ NotationPp.pp_attribute attr); *) subst pos env t | Ast.Variable var -> - let name, expected_ty = CicNotationEnv.declaration_of_var var in + let name, expected_ty = NotationEnv.declaration_of_var var in let ty, value = try List.assoc name env @@ -352,15 +352,15 @@ let instantiate21 idrefs env l1 = prerr_endline ("name " ^ name ^ " not found in environment"); assert false in - assert (CicNotationEnv.well_typed ty value); (* INVARIANT *) + assert (NotationEnv.well_typed ty value); (* INVARIANT *) (* following assertion should be a conditional that makes this * instantiation fail *) - if not (CicNotationEnv.well_typed expected_ty value) then + if not (NotationEnv.well_typed expected_ty value) then begin prerr_endline ("The variable " ^ name ^ " is used with the wrong type in the notation declaration"); assert false end; - let value = CicNotationEnv.term_of_value value in + let value = NotationEnv.term_of_value value in let value = match expected_ty with | Env.TermType l -> Ast.AttributedTerm (`Level l,value) @@ -374,15 +374,15 @@ let instantiate21 idrefs env l1 = | `Keyword k -> [ add_keyword_attrs t ] | _ -> [ t ]) | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ] - | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ] + | t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ] and subst_magic pos env = function | Ast.List0 (p, sep_opt) | Ast.List1 (p, sep_opt) -> - let rec_decls = CicNotationEnv.declarations_of_term p in + let rec_decls = NotationEnv.declarations_of_term p in let rec_values = - List.map (fun (n, _) -> CicNotationEnv.lookup_list env n) rec_decls + List.map (fun (n, _) -> NotationEnv.lookup_list env n) rec_decls in - let values = CicNotationUtil.ncombine rec_values in + let values = NotationUtil.ncombine rec_values in let sep = match sep_opt with | None -> [] @@ -391,24 +391,24 @@ let instantiate21 idrefs env l1 = let rec instantiate_list acc = function | [] -> List.rev acc | value_set :: [] -> - let env = CicNotationEnv.combine rec_decls value_set in - instantiate_list (CicNotationUtil.group (subst pos env p) :: acc) + let env = NotationEnv.combine rec_decls value_set in + instantiate_list (NotationUtil.group (subst pos env p) :: acc) [] | value_set :: tl -> - let env = CicNotationEnv.combine rec_decls value_set in + let env = NotationEnv.combine rec_decls value_set in let terms = subst pos env p in - instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl + instantiate_list (NotationUtil.group (terms @ sep) :: acc) tl in if values = [] then [] else [hovbox false false (instantiate_list [] values)] | Ast.Opt p -> - let opt_decls = CicNotationEnv.declarations_of_term p in + let opt_decls = NotationEnv.declarations_of_term p in let env = let rec build_env = function | [] -> [] | (name, ty) :: tl -> (* assumption: if one of the value is None then all are *) - (match CicNotationEnv.lookup_opt env name with + (match NotationEnv.lookup_opt env name with | None -> raise Exit | Some v -> (name, (ty, v)) :: build_env tl) in @@ -424,7 +424,7 @@ let instantiate21 idrefs env l1 = | Ast.Box (kind, tl) -> let tl' = subst_children pos env tl in Ast.Box (kind, List.concat tl') - | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l + | l -> NotationUtil.visit_layout (subst_singleton pos env) l and subst_children pos env = function | [] -> [] @@ -451,20 +451,20 @@ let instantiate21 idrefs env l1 = let rec pp_ast1 term = let rec pp_value = function - | CicNotationEnv.NumValue _ as v -> v - | CicNotationEnv.StringValue _ as v -> v -(* | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *) - | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t) - | CicNotationEnv.OptValue None as v -> v - | CicNotationEnv.OptValue (Some v) -> - CicNotationEnv.OptValue (Some (pp_value v)) - | CicNotationEnv.ListValue vl -> - CicNotationEnv.ListValue (List.map pp_value vl) + | NotationEnv.NumValue _ as v -> v + | NotationEnv.StringValue _ as v -> v +(* | NotationEnv.TermValue t when t == term -> NotationEnv.TermValue (pp_ast0 t pp_ast1) *) + | NotationEnv.TermValue t -> NotationEnv.TermValue (pp_ast1 t) + | NotationEnv.OptValue None as v -> v + | NotationEnv.OptValue (Some v) -> + NotationEnv.OptValue (Some (pp_value v)) + | NotationEnv.ListValue vl -> + NotationEnv.ListValue (List.map pp_value vl) in let ast_env_of_env env = List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env in -(* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *) +(* prerr_endline ("pattern matching from 2 to 1 on term " ^ NotationPp.pp_term term); *) match term with | Ast.AttributedTerm (attrs, term') -> Ast.AttributedTerm (attrs, pp_ast1 term') @@ -473,7 +473,7 @@ let rec pp_ast1 term = | None -> pp_ast0 term pp_ast1 | Some (env, ctors, pid) -> let idrefs = - List.flatten (List.map CicNotationUtil.get_idrefs ctors) + List.flatten (List.map NotationUtil.get_idrefs ctors) in let l1 = try @@ -488,7 +488,7 @@ let load_patterns21 t = let pp_ast ast = debug_print (lazy "pp_ast <-"); let ast' = pp_ast1 ast in - debug_print (lazy ("pp_ast -> " ^ CicNotationPp.pp_term ast')); + debug_print (lazy ("pp_ast -> " ^ NotationPp.pp_term ast')); ast' exception Pretty_printer_not_found @@ -514,7 +514,7 @@ let fresh_id = let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) = let id = fresh_id () in let l1' = add_level_info precedence (fill_pos_info l1) in - let l2' = CicNotationUtil.strip_attributes l2 in + let l2' = NotationUtil.strip_attributes l2 in Hashtbl.add !level1_patterns21 id l1'; pattern21_matrix := (l2', id) :: !pattern21_matrix; load_patterns21 !pattern21_matrix; @@ -575,18 +575,18 @@ let tail_names names env = aux [] env let instantiate_level2 env term = -(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *) +(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = try List.assoc n !fresh_env with Not_found -> - let new_name = CicNotationUtil.fresh_name () in + let new_name = NotationUtil.fresh_name () in fresh_env := (n, new_name) :: !fresh_env; new_name in let rec aux env term = -(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *) +(* prerr_endline ("ENV " ^ NotationPp.pp_env env); *) match term with | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) @@ -645,8 +645,8 @@ let instantiate_level2 env term = | Ast.Ascription (term, name) -> assert false and aux_magic env = function | Ast.Default (some_pattern, none_pattern) -> - let some_pattern_names = CicNotationUtil.names_of_term some_pattern in - let none_pattern_names = CicNotationUtil.names_of_term none_pattern in + let some_pattern_names = NotationUtil.names_of_term some_pattern in + let none_pattern_names = NotationUtil.names_of_term none_pattern in let opt_names = List.filter (fun name -> not (List.mem name none_pattern_names)) @@ -665,13 +665,13 @@ let instantiate_level2 env term = | _ -> prerr_endline (sprintf "lookup of %s in env %s did not return an optional value" - name (CicNotationPp.pp_env env)); + name (NotationPp.pp_env env)); assert false)) | Ast.Fold (`Left, base_pattern, names, rec_pattern) -> let acc_name = List.hd names in (* names can't be empty, cfr. parser *) let meta_names = List.filter ((<>) acc_name) - (CicNotationUtil.names_of_term rec_pattern) + (NotationUtil.names_of_term rec_pattern) in (match meta_names with | [] -> assert false (* as above *) @@ -693,7 +693,7 @@ let instantiate_level2 env term = let acc_name = List.hd names in (* names can't be empty, cfr. parser *) let meta_names = List.filter ((<>) acc_name) - (CicNotationUtil.names_of_term rec_pattern) + (NotationUtil.names_of_term rec_pattern) in (match meta_names with | [] -> assert false (* as above *) @@ -711,7 +711,7 @@ let instantiate_level2 env term = in instantiate_fold_right env) | Ast.If (_, p_true, p_false) as t -> - aux env (CicNotationUtil.find_branch (Ast.Magic t)) + aux env (NotationUtil.find_branch (Ast.Magic t)) | Ast.Fail -> assert false | _ -> assert false in diff --git a/matita/components/content_pres/termContentPres.mli b/matita/components/content_pres/termContentPres.mli index 40e8fc021..a9bcd850c 100644 --- a/matita/components/content_pres/termContentPres.mli +++ b/matita/components/content_pres/termContentPres.mli @@ -28,7 +28,7 @@ type pretty_printer_id val add_pretty_printer: - CicNotationPt.term -> (* level 2 pattern *) + NotationPt.term -> (* level 2 pattern *) CicNotationParser.checked_l1_pattern -> pretty_printer_id @@ -39,14 +39,14 @@ val remove_pretty_printer: pretty_printer_id -> unit (** {2 content -> pres} *) -val pp_ast: CicNotationPt.term -> CicNotationPt.term +val pp_ast: NotationPt.term -> NotationPt.term (** {2 pres -> content} *) (** fills a term pattern instantiating variable magics *) val instantiate_level2: - CicNotationEnv.t -> CicNotationPt.term -> - CicNotationPt.term + NotationEnv.t -> NotationPt.term -> + NotationPt.term val push: unit -> unit val pop: unit -> unit diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml index 5b5b53f52..0e4636d57 100644 --- a/matita/components/disambiguation/disambiguate.ml +++ b/matita/components/disambiguation/disambiguate.ml @@ -30,7 +30,7 @@ open Printf open DisambiguateTypes open UriManager -module Ast = CicNotationPt +module Ast = NotationPt (* the integer is an offset to be added to each location *) exception Ambiguous_input diff --git a/matita/components/disambiguation/disambiguate.mli b/matita/components/disambiguation/disambiguate.mli index cffb1df0a..167de714b 100644 --- a/matita/components/disambiguation/disambiguate.mli +++ b/matita/components/disambiguation/disambiguate.mli @@ -82,9 +82,9 @@ val resolve : val find_in_context: string -> string option list -> int val domain_of_term: context: - string option list -> CicNotationPt.term -> domain + string option list -> NotationPt.term -> domain val domain_of_obj: - context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain + context:string option list -> NotationPt.term NotationPt.obj -> domain val disambiguate_thing: context:'context -> diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 5adc2e91b..9d68213b7 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -33,7 +33,7 @@ type ('term, 'lazy_term, 'ident) pattern = 'lazy_term option * ('ident * 'term) list * 'term option type npattern = - CicNotationPt.term option * (string * CicNotationPt.term) list * CicNotationPt.term option + NotationPt.term option * (string * NotationPt.term) list * NotationPt.term option type 'lazy_term reduction = [ `Normalize @@ -50,28 +50,28 @@ type 'term just = | `Auto of 'term 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 * NotationPt.term + | NSmartApply of loc * NotationPt.term + | NAssert of loc * ((string * [`Decl of NotationPt.term | `Def of NotationPt.term * NotationPt.term]) list * NotationPt.term) list + | NCases of loc * NotationPt.term * 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 * NotationPt.term + | NConstructor of loc * int option * NotationPt.term list + | NCut of loc * NotationPt.term +(* | NDiscriminate of loc * NotationPt.term + | NSubst of loc * NotationPt.term *) | NDestruct of loc * string list option * string list - | NElim of loc * CicNotationPt.term * npattern + | NElim of loc * NotationPt.term * 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 * NotationPt.term * npattern + | NLApply of loc * NotationPt.term + | NLetIn of loc * npattern * NotationPt.term * 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 * NotationPt.term * npattern + | NAuto of loc * NotationPt.term auto_params | NDot of loc | NSemicolon of loc | NBranch of loc @@ -193,9 +193,9 @@ type ('term,'lazy_term) macro = (* URI or base-uri, parameters *) type nmacro = - | NCheck of loc * CicNotationPt.term + | NCheck of loc * NotationPt.term | Screenshot of loc * string - | NAutoInteractive of loc * CicNotationPt.term auto_params + | NAutoInteractive of loc * NotationPt.term auto_params | NIntroGuess of loc (** To be increased each time the command type below changes, used for "safe" @@ -221,15 +221,15 @@ type ('term,'obj) command = | Qed of loc 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 + | UnificationHint of loc * NotationPt.term * int (* term, precedence *) + | NObj of loc * NotationPt.term NotationPt.obj + | NDiscriminator of loc * NotationPt.term + | NInverter of loc * string * NotationPt.term * bool list option * NotationPt.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 + NotationPt.term * NotationPt.term * + (string * NotationPt.term) * NotationPt.term | NQed of loc type punctuation_tactical = diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 5ba1b649d..e506742c4 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -90,43 +90,43 @@ let pp_just ~term_pp = ;; let rec pp_ntactic ~map_unicode_to_tex = - let term_pp = CicNotationPp.pp_term in + let term_pp = NotationPp.pp_term in let lazy_term_pp = fun _ -> assert false in let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in function - | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t + | NApply (_,t) -> "napply " ^ NotationPp.pp_term t | NSmartApply (_,t) -> "fixme" | NAuto (_,(None,flgs)) -> "nautobatch" ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) | NAuto (_,(Some l,flgs)) -> "nautobatch" ^ " by " ^ - (String.concat "," (List.map CicNotationPp.pp_term l)) ^ + (String.concat "," (List.map NotationPp.pp_term l)) ^ String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) - | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ + | NCases (_,what,where) -> "ncases " ^ NotationPp.pp_term what ^ assert false ^ " " ^ assert false | NConstructor (_,None,l) -> "@ " ^ - String.concat " " (List.map CicNotationPp.pp_term l) + String.concat " " (List.map NotationPp.pp_term l) | NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^ - String.concat " " (List.map CicNotationPp.pp_term l) + String.concat " " (List.map NotationPp.pp_term l) | NCase1 (_,n) -> "*" ^ n ^ ":" | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ - " with " ^ CicNotationPp.pp_term wwhat - | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t -(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t - | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *) + " with " ^ NotationPp.pp_term wwhat + | NCut (_,t) -> "ncut " ^ NotationPp.pp_term t +(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term t + | NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term t *) | NDestruct (_,dom,skip) -> "ndestruct ..." - | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ + | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term what ^ assert false ^ " " ^ assert false | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n - | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^ + | NInversion (_,what,where) -> "ninversion " ^ NotationPp.pp_term what ^ assert false ^ " " ^ assert false - | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t + | NLApply (_,t) -> "lapply " ^ NotationPp.pp_term t | NRewrite (_,dir,n,where) -> "nrewrite " ^ (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^ - " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where + " " ^ NotationPp.pp_term n ^ " " ^ pp_tactic_pattern where | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED" | NDot _ -> "##." | NSemicolon _ -> "##;" @@ -311,7 +311,7 @@ let pp_arg ~term_pp arg = "(" ^ s ^ ")" let pp_nmacro = function - | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term) + | NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term term) | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name ;; @@ -373,7 +373,7 @@ let pp_coercion ~term_pp t do_composites arity saturations= let pp_ncommand ~obj_pp = function | UnificationHint (_,t, n) -> - "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t + "unification hint " ^ string_of_int n ^ " " ^ NotationPp.pp_term t | NDiscriminator (_,_) | NInverter (_,_,_,_,_) | NUnivConstraint (_) -> "not supported" diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index a12a246aa..e87795900 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -543,7 +543,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = try let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm None status [] [] [] - ("",0,CicNotationPt.Ident (name,None)) in + ("",0,NotationPt.Ident (name,None)) in assert (metasenv = [] && subst = []); let status, nuris = NCicCoercDeclaration. diff --git a/matita/components/grafite_engine/nCicCoercDeclaration.mli b/matita/components/grafite_engine/nCicCoercDeclaration.mli index aee0e9fc3..1c9062fd6 100644 --- a/matita/components/grafite_engine/nCicCoercDeclaration.mli +++ b/matita/components/grafite_engine/nCicCoercDeclaration.mli @@ -14,10 +14,10 @@ val eval_ncoercion: #GrafiteTypes.status as 'status -> string -> - CicNotationPt.term -> - CicNotationPt.term -> - string * CicNotationPt.term -> - CicNotationPt.term -> 'status * [> `New of NUri.uri list ] + NotationPt.term -> + NotationPt.term -> + string * NotationPt.term -> + NotationPt.term -> 'status * [> `New of NUri.uri list ] (* for records, the term is the projection, already refined, while the * first integer is the number of left params and the second integer is diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index af8c86204..c23e5acff 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -28,8 +28,8 @@ exception BaseUriNotSetYet type tactic = - (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, string) + (NotationPt.term, NotationPt.term, + NotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic type lazy_tactic = @@ -138,7 +138,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing type pattern = - CicNotationPt.term Disambiguate.disambiguator_input option * + NotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) = @@ -193,10 +193,10 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = in let name = match obj with - | CicNotationPt.Inductive (_,(name,_,_,_)::_) - | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind" - | CicNotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" - | CicNotationPt.Inductive _ -> assert false + | NotationPt.Inductive (_,(name,_,_,_)::_) + | NotationPt.Record (_,name,_,_) -> name ^ ".ind" + | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con" + | NotationPt.Inductive _ -> assert false in NUri.uri_of_string (baseuri ^ "/" ^ name) in diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli index 439a817d3..7590699f9 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.mli +++ b/matita/components/grafite_parser/grafiteDisambiguate.mli @@ -26,8 +26,8 @@ exception BaseUriNotSetYet type tactic = - (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, string) + (NotationPt.term, NotationPt.term, + NotationPt.term GrafiteAst.reduction, string) GrafiteAst.tactic type lazy_tactic = @@ -37,24 +37,24 @@ type lazy_tactic = val disambiguate_command: LexiconEngine.status as 'status -> ?baseuri:string -> - ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> + ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> 'status * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_nterm : NCic.term option -> (#NEstatus.status as 'status) -> NCic.context -> NCic.metasenv -> NCic.substitution -> - CicNotationPt.term Disambiguate.disambiguator_input -> + NotationPt.term Disambiguate.disambiguator_input -> NCic.metasenv * NCic.substitution * 'status * NCic.term val disambiguate_nobj : #NEstatus.status as 'status -> ?baseuri:string -> - (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input -> + (NotationPt.term NotationPt.obj) Disambiguate.disambiguator_input -> 'status * NCic.obj type pattern = - CicNotationPt.term Disambiguate.disambiguator_input option * + NotationPt.term Disambiguate.disambiguator_input option * (string * NCic.term) list * NCic.term option val disambiguate_npattern: diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index 89a09fc50..e7e3234c9 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -25,7 +25,7 @@ (* $Id$ *) -module N = CicNotationPt +module N = NotationPt module G = GrafiteAst module L = LexiconAst module LE = LexiconEngine @@ -222,7 +222,7 @@ EXTEND | N.Implicit _ -> false | N.UserInput -> true | _ -> raise (Invalid_argument "malformed target parameter list 1")) l - | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ] + | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ] ]; direction: [ [ SYMBOL ">" -> `LeftToRight @@ -868,7 +868,7 @@ EXTEND | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; SYMBOL <:unicode> ; u2 = tactic_term -> let urify = function - | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) -> + | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) -> NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ") | _ -> raise (Failure "only a Type[…] sort can be constrained") in diff --git a/matita/components/grafite_parser/grafiteParser.mli b/matita/components/grafite_parser/grafiteParser.mli index d657e4975..2dc833194 100644 --- a/matita/components/grafite_parser/grafiteParser.mli +++ b/matita/components/grafite_parser/grafiteParser.mli @@ -28,9 +28,9 @@ type 'a localized_option = | LNone of GrafiteAst.loc type ast_statement = - (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, - CicNotationPt.term CicNotationPt.obj, string) + (NotationPt.term, NotationPt.term, + NotationPt.term GrafiteAst.reduction, + NotationPt.term NotationPt.obj, string) GrafiteAst.statement exception NoInclusionPerformed of string (* full path *) diff --git a/matita/components/grafite_parser/test_parser.ml b/matita/components/grafite_parser/test_parser.ml index 9f42238e9..72d6e981d 100644 --- a/matita/components/grafite_parser/test_parser.ml +++ b/matita/components/grafite_parser/test_parser.ml @@ -63,7 +63,7 @@ let pp_precedence = string_of_int let process_stream istream = let char_count = ref 0 in - let module P = CicNotationPt in + let module P = NotationPt in let module G = GrafiteAst in let status = ref @@ -90,12 +90,12 @@ let process_stream istream = | None -> () | Some id -> prerr_endline "removing last notation rule ..."; - CicNotationParser.delete id) *) + NotationParser.delete id) *) | G.Executable (_, G.Macro (_, G.Check (_, t))) -> - prerr_endline (sprintf "ast: %s" (CicNotationPp.pp_term t)); + prerr_endline (sprintf "ast: %s" (NotationPp.pp_term t)); let t' = TermContentPres.pp_ast t in prerr_endline (sprintf "rendered ast: %s" - (CicNotationPp.pp_term t')); + (NotationPp.pp_term t')); let tbl = Hashtbl.create 0 in dump_xml t' tbl "out.xml" | statement -> @@ -104,7 +104,7 @@ let process_stream istream = GrafiteAstPp.pp_statement ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~term_pp:CicNotationPp.pp_term + ~term_pp:NotationPp.pp_term ~lazy_term_pp:(fun _ -> "_lazy_term_here_") ~obj_pp:(fun _ -> "_obj_here_") statement) diff --git a/matita/components/lexicon/cicNotation.ml b/matita/components/lexicon/cicNotation.ml index 7351596fa..28cab9458 100644 --- a/matita/components/lexicon/cicNotation.ml +++ b/matita/components/lexicon/cicNotation.ml @@ -60,7 +60,7 @@ let process_notation st = let id = CicNotationParser.extend l1 (fun env loc -> - CicNotationPt.AttributedTerm + NotationPt.AttributedTerm (`Loc loc,TermContentPres.instantiate_level2 env l2)) in rule_id := [ RuleId id ]; Hashtbl.add !rule_ids_to_items id item diff --git a/matita/components/lexicon/lexiconAst.ml b/matita/components/lexicon/lexiconAst.ml index 0c588d189..b0b9399b5 100644 --- a/matita/components/lexicon/lexiconAst.ml +++ b/matita/components/lexicon/lexiconAst.ml @@ -44,16 +44,16 @@ type command = | Include of loc * string * inclusion_mode * string (* _,buri,_,path *) | Alias of loc * alias_spec (** parameters, name, type, fields *) - | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * - int * CicNotationPt.term + | 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 * CicNotationPt.argument_pattern list) * - CicNotationPt.cic_appl_pattern + string * (string * NotationPt.argument_pattern list) * + NotationPt.cic_appl_pattern (* description (i.e. id), symbol, arg pattern, appl pattern *) (* composed magic: term + command magics. No need to change this value *) -let magic = magic + 10000 * CicNotationPt.magic +let magic = magic + 10000 * NotationPt.magic let description_of_alias = function diff --git a/matita/components/lexicon/lexiconAstPp.ml b/matita/components/lexicon/lexiconAstPp.ml index c11e4f094..cf8ea3d03 100644 --- a/matita/components/lexicon/lexiconAstPp.ml +++ b/matita/components/lexicon/lexiconAstPp.ml @@ -29,8 +29,8 @@ open Printf open LexiconAst -let pp_l1_pattern = CicNotationPp.pp_term -let pp_l2_pattern = CicNotationPp.pp_term +let pp_l1_pattern = NotationPp.pp_term +let pp_l2_pattern = NotationPp.pp_term let pp_alias = function | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri @@ -50,7 +50,7 @@ let pp_associativity = function let pp_precedence i = sprintf "with precedence %d" i let pp_argument_pattern = function - | CicNotationPt.IdentArg (eta_depth, name) -> + | NotationPt.IdentArg (eta_depth, name) -> let eta_buf = Buffer.create 5 in for i = 1 to eta_depth do Buffer.add_string eta_buf "\\eta." @@ -61,7 +61,7 @@ let pp_interpretation dsc symbol arg_patterns cic_appl_pattern = sprintf "interpretation \"%s\" '%s %s = %s." dsc symbol (String.concat " " (List.map pp_argument_pattern arg_patterns)) - (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern) + (NotationPp.pp_cic_appl_pattern cic_appl_pattern) let pp_dir_opt = function | None -> "" diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index 39d95a7f2..8a5b50354 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -124,23 +124,23 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd = | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) -> let rec disambiguate = function - CicNotationPt.ApplPattern l -> - CicNotationPt.ApplPattern (List.map disambiguate l) - | CicNotationPt.VarPattern id + NotationPt.ApplPattern l -> + NotationPt.ApplPattern (List.map disambiguate l) + | NotationPt.VarPattern id when not (List.exists - (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args) + (function (NotationPt.IdentArg (_,id')) -> id'=id) args) -> let item = DisambiguateTypes.Id id in begin try match DisambiguateTypes.Environment.find item status.aliases with L.Ident_alias (_, uri) -> (try - CicNotationPt.NRefPattern + NotationPt.NRefPattern (NReference.reference_of_string uri) with NReference.IllFormedReference _ -> - CicNotationPt.UriPattern (UriManager.uri_of_string uri)) + NotationPt.UriPattern (UriManager.uri_of_string uri)) | _ -> assert false with Not_found -> prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ diff --git a/matita/components/lexicon/lexiconMarshal.ml b/matita/components/lexicon/lexiconMarshal.ml index 5d69fafc0..6693de214 100644 --- a/matita/components/lexicon/lexiconMarshal.ml +++ b/matita/components/lexicon/lexiconMarshal.ml @@ -43,15 +43,15 @@ let rehash_cmd_uris = | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) -> let rec aux = function - | CicNotationPt.UriPattern uri -> - CicNotationPt.UriPattern (rehash_uri uri) - | CicNotationPt.NRefPattern (NReference.Ref (uri,spec)) -> + | NotationPt.UriPattern uri -> + NotationPt.UriPattern (rehash_uri uri) + | NotationPt.NRefPattern (NReference.Ref (uri,spec)) -> let uri = NCicLibrary.refresh_uri uri in - CicNotationPt.NRefPattern (NReference.reference_of_spec uri spec) - | CicNotationPt.ApplPattern args -> - CicNotationPt.ApplPattern (List.map aux args) - | CicNotationPt.VarPattern _ - | CicNotationPt.ImplicitPattern as pat -> pat + NotationPt.NRefPattern (NReference.reference_of_spec uri spec) + | NotationPt.ApplPattern args -> + NotationPt.ApplPattern (List.map aux args) + | NotationPt.VarPattern _ + | NotationPt.ImplicitPattern as pat -> pat in let appl_pattern = aux cic_appl_pattern in LexiconAst.Interpretation (loc, dsc, args, appl_pattern) diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml index b8d474cc2..18685f35b 100644 --- a/matita/components/ng_cic_content/nTermCicContent.ml +++ b/matita/components/ng_cic_content/nTermCicContent.ml @@ -27,7 +27,7 @@ open Printf -module Ast = CicNotationPt +module Ast = NotationPt let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -89,7 +89,7 @@ let destroy_nat = (* CODICE c&p da NCicPp *) let nast_of_cic0 status ~(idref: - ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term) + ?reference:NReference.reference -> NotationPt.term -> NotationPt.term) ~output_type ~metasenv ~subst k ~context = function | NCic.Rel n -> @@ -277,7 +277,7 @@ let instantiate32 idrefs env symbol args = in let rec add_lambda t n = if n > 0 then - let name = CicNotationUtil.fresh_name () in + let name = NotationUtil.fresh_name () in Ast.Binder (`Lambda, (Ast.Ident (name, None), None), Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)]) else @@ -305,7 +305,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term = idref ~reference: (match term with NCic.Const nref -> nref | _ -> assert false) - (CicNotationPt.Ident ("dummy",None)) + (NotationPt.Ident ("dummy",None)) in match attrterm with Ast.AttributedTerm (`IdRef id, _) -> id @@ -345,7 +345,7 @@ let ast_of_acic ~output_type id_to_sort annterm = ^ CicPp.ppterm (Deannotate.deannotate_term annterm))); let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in let ast = ast_of_acic1 ~output_type term_info annterm in - debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast)); + debug_print (lazy ("ast_of_acic -> " ^ NotationPp.pp_term ast)); ast, term_info.uri let fresh_id = diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli index 38c0ebf3c..d691acdec 100644 --- a/matita/components/ng_cic_content/nTermCicContent.mli +++ b/matita/components/ng_cic_content/nTermCicContent.mli @@ -31,15 +31,15 @@ type interpretation_id val add_interpretation: string -> (* id / description *) - string * CicNotationPt.argument_pattern list -> (* symbol, level 2 pattern *) - CicNotationPt.cic_appl_pattern -> (* level 3 pattern *) + string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) + NotationPt.cic_appl_pattern -> (* level 3 pattern *) interpretation_id (** @raise Interpretation_not_found *) val lookup_interpretations: string -> (* symbol *) - (string * CicNotationPt.argument_pattern list * - CicNotationPt.cic_appl_pattern) list + (string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern) list exception Interpretation_not_found @@ -56,9 +56,9 @@ val set_active_interpretations: interpretation_id list -> unit val ast_of_acic: output_type:[`Pattern|`Term] -> - (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) + (Cic.id, NotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) Cic.annterm -> (* acic *) - CicNotationPt.term (* ast *) + NotationPt.term (* ast *) * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *) (** {2 content -> acic} *) @@ -69,7 +69,7 @@ val instantiate_appl_pattern: mk_appl:('term list -> 'term) -> mk_implicit:(bool -> 'term) -> term_of_uri : (UriManager.uri -> 'term) -> - (string * 'term) list -> CicNotationPt.cic_appl_pattern -> + (string * 'term) list -> NotationPt.cic_appl_pattern -> 'term val push: unit -> unit @@ -80,7 +80,7 @@ val pop: unit -> unit val nast_of_cic : output_type:[`Pattern | `Term ] -> subst:NCic.substitution -> context:NCic.context -> NCic.term -> - CicNotationPt.term + NotationPt.term *) type id = string @@ -90,10 +90,10 @@ val hide_coercions: bool ref val nmap_sequent: #NCicCoercion.status -> metasenv:NCic.metasenv -> subst:NCic.substitution -> int * NCic.conjecture -> - CicNotationPt.term Content.conjecture * + NotationPt.term Content.conjecture * (id, NReference.reference) Hashtbl.t (* id -> reference *) val nmap_obj: #NCicCoercion.status -> NCic.obj -> - CicNotationPt.term Content.cobj * + NotationPt.term Content.cobj * (id, NReference.reference) Hashtbl.t (* id -> reference *) diff --git a/matita/components/ng_cic_content/ncic2astMatcher.ml b/matita/components/ng_cic_content/ncic2astMatcher.ml index 2245e3429..2ae782bdb 100644 --- a/matita/components/ng_cic_content/ncic2astMatcher.ml +++ b/matita/components/ng_cic_content/ncic2astMatcher.ml @@ -25,8 +25,8 @@ (* $Id: acic2astMatcher.ml 9271 2008-11-28 18:28:58Z fguidi $ *) -module Ast = CicNotationPt -module Util = CicNotationUtil +module Ast = NotationPt +module Util = NotationUtil let reference_of_oxuri = ref (fun _ -> assert false);; let set_reference_of_oxuri f = reference_of_oxuri := f;; @@ -65,7 +65,7 @@ struct type pattern_t = Ast.cic_appl_pattern type term_t = NCic.term - let string_of_pattern = CicNotationPp.pp_cic_appl_pattern + let string_of_pattern = NotationPp.pp_cic_appl_pattern let string_of_term t = (*CSC: ??? *) NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t diff --git a/matita/components/ng_cic_content/ncic2astMatcher.mli b/matita/components/ng_cic_content/ncic2astMatcher.mli index 6205f8522..1feae63b0 100644 --- a/matita/components/ng_cic_content/ncic2astMatcher.mli +++ b/matita/components/ng_cic_content/ncic2astMatcher.mli @@ -29,7 +29,7 @@ module Matcher32: sig (** @param l3_patterns level 3 (CIC) patterns (AKA cic_appl_pattern) *) val compiler : - (CicNotationPt.cic_appl_pattern * int) list -> + (NotationPt.cic_appl_pattern * int) list -> (NCic.term -> ((string * NCic.term) list * NCic.term list * int) option) end diff --git a/matita/components/ng_disambiguation/disambiguateChoices.ml b/matita/components/ng_disambiguation/disambiguateChoices.ml index 3da5f9baa..6c335ab64 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.ml +++ b/matita/components/ng_disambiguation/disambiguateChoices.ml @@ -57,7 +57,7 @@ let mk_choice ~mk_appl ~mk_implicit ~term_of_uri ~term_of_nref (dsc, args, appl (fun cic_args -> let env',rest = let names = - List.map (function CicNotationPt.IdentArg (_, name) -> name) args + List.map (function NotationPt.IdentArg (_, name) -> name) args in let rec combine_with_rest l1 l2 = match l1,l2 with diff --git a/matita/components/ng_disambiguation/disambiguateChoices.mli b/matita/components/ng_disambiguation/disambiguateChoices.mli index 4d1ed5329..4e9807932 100644 --- a/matita/components/ng_disambiguation/disambiguateChoices.mli +++ b/matita/components/ng_disambiguation/disambiguateChoices.mli @@ -65,7 +65,7 @@ val mk_choice: mk_implicit: (bool -> 'term) -> term_of_uri: (UriManager.uri -> 'term) -> term_of_nref: (NReference.reference -> 'term) -> - string * CicNotationPt.argument_pattern list * - CicNotationPt.cic_appl_pattern -> + string * NotationPt.argument_pattern list * + NotationPt.cic_appl_pattern -> 'term codomain_item diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 487bceb87..2c5b06394 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -16,7 +16,7 @@ open Printf open DisambiguateTypes open UriManager -module Ast = CicNotationPt +module Ast = NotationPt module NRef = NReference let debug_print s = prerr_endline (Lazy.force s);; @@ -115,24 +115,24 @@ let interpretate_term_and_interpretate_term_option assert (uri = None); let rec aux ~localize loc context = function - | CicNotationPt.AttributedTerm (`Loc loc, term) -> + | NotationPt.AttributedTerm (`Loc loc, term) -> let res = aux ~localize loc context term in if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; res - | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term - | CicNotationPt.Appl (CicNotationPt.Appl inner :: args) -> - aux ~localize loc context (CicNotationPt.Appl (inner @ args)) - | CicNotationPt.Appl - (CicNotationPt.AttributedTerm (att,(CicNotationPt.Appl inner))::args)-> + | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term + | NotationPt.Appl (NotationPt.Appl inner :: args) -> + aux ~localize loc context (NotationPt.Appl (inner @ args)) + | NotationPt.Appl + (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)-> aux ~localize loc context - (CicNotationPt.AttributedTerm (att,CicNotationPt.Appl (inner @ args))) - | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> + (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args))) + | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args) - | CicNotationPt.Appl terms -> + | NotationPt.Appl terms -> NCic.Appl (List.map (aux ~localize loc context) terms) - | CicNotationPt.Binder (binder_kind, (var, typ), body) -> + | NotationPt.Binder (binder_kind, (var, typ), body) -> let cic_type = aux_option ~localize loc context `Type typ in let cic_name = cic_name_of_name var in let cic_body = aux ~localize loc (cic_name :: context) body in @@ -143,7 +143,7 @@ let interpretate_term_and_interpretate_term_option | `Exists -> Disambiguate.resolve ~env ~mk_choice (Symbol ("exists", 0)) (`Args [ cic_type; NCic.Lambda (cic_name, cic_type, cic_body) ])) - | CicNotationPt.Case (term, indty_ident, outtype, branches) -> + | NotationPt.Case (term, indty_ident, outtype, branches) -> let cic_term = aux ~localize loc context term in let cic_outtype = aux_option ~localize loc context `Term outtype in let do_branch ((_, _, args), term) = @@ -289,8 +289,8 @@ let interpretate_term_and_interpretate_term_option function 0 -> term | n -> - CicNotationPt.Binder - (`Lambda, (CicNotationPt.Ident ("_", None), None), + NotationPt.Binder + (`Lambda, (NotationPt.Ident ("_", None), None), mk_lambdas (n - 1)) in (("wildcard",None,[]), @@ -299,11 +299,11 @@ let interpretate_term_and_interpretate_term_option let branches = sort branches cl in NCic.Match (indtype_ref, cic_outtype, cic_term, (List.map do_branch branches)) - | CicNotationPt.Cast (t1, t2) -> + | NotationPt.Cast (t1, t2) -> let cic_t1 = aux ~localize loc context t1 in let cic_t2 = aux ~localize loc context t2 in NCic.LetIn ("_",cic_t2,cic_t1, NCic.Rel 1) - | CicNotationPt.LetIn ((name, typ), def, body) -> + | NotationPt.LetIn ((name, typ), def, body) -> let cic_def = aux ~localize loc context def in let cic_name = cic_name_of_name name in let cic_typ = @@ -313,11 +313,11 @@ let interpretate_term_and_interpretate_term_option in let cic_body = aux ~localize loc (cic_name :: context) body in NCic.LetIn (cic_name, cic_typ, cic_def, cic_body) - | CicNotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term - | CicNotationPt.Ident _ - | CicNotationPt.Uri _ - | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed - | CicNotationPt.Ident (name, subst) -> + | NotationPt.LetRec (_kind, _defs, _body) -> NCic.Implicit `Term + | NotationPt.Ident _ + | NotationPt.Uri _ + | NotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed + | NotationPt.Ident (name, subst) -> assert (subst = None); (try NCic.Rel (find_in_context name context) @@ -325,59 +325,59 @@ let interpretate_term_and_interpretate_term_option try NCic.Const (List.assoc name obj_context) with Not_found -> Disambiguate.resolve ~env ~mk_choice (Id name) (`Args [])) - | CicNotationPt.Uri (uri, subst) -> + | NotationPt.Uri (uri, subst) -> assert (subst = None); (try NCic.Const (!reference_of_oxuri(UriManager.uri_of_string uri)) with NRef.IllFormedReference _ -> - CicNotationPt.fail loc "Ill formed reference") - | CicNotationPt.NRef nref -> NCic.Const nref - | CicNotationPt.NCic t -> + NotationPt.fail loc "Ill formed reference") + | NotationPt.NRef nref -> NCic.Const nref + | NotationPt.NCic t -> let context = (* to make metas_of_term happy *) List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in assert(NCicUntrusted.metas_of_term [] context t = []); t - | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector - | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term - | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) - | CicNotationPt.UserInput -> NCic.Implicit `Hole - | CicNotationPt.Num (num, i) -> + | NotationPt.Implicit `Vector -> NCic.Implicit `Vector + | NotationPt.Implicit `JustOne -> NCic.Implicit `Term + | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s) + | NotationPt.UserInput -> NCic.Implicit `Hole + | NotationPt.Num (num, i) -> Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num) - | CicNotationPt.Meta (index, subst) -> + | NotationPt.Meta (index, subst) -> let cic_subst = List.map (function None -> assert false| Some t -> aux ~localize loc context t) subst in NCic.Meta (index, (0, NCic.Ctx cic_subst)) - | CicNotationPt.Sort `Prop -> NCic.Sort NCic.Prop - | CicNotationPt.Sort `Set -> NCic.Sort (NCic.Type + | NotationPt.Sort `Prop -> NCic.Sort NCic.Prop + | NotationPt.Sort `Set -> NCic.Sort (NCic.Type [`Type,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) - | CicNotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type + | NotationPt.Sort (`Type _u) -> NCic.Sort (NCic.Type [`Type,NUri.uri_of_string "cic:/matita/pts/Type0.univ"]) - | CicNotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type + | NotationPt.Sort (`NType s) -> NCic.Sort (NCic.Type [`Type,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) - | CicNotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type + | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")]) - | CicNotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type + | NotationPt.Sort (`CProp _u) -> NCic.Sort (NCic.Type [`CProp,NUri.uri_of_string "cic:/matita/pts/Type.univ"]) - | CicNotationPt.Symbol (symbol, instance) -> + | NotationPt.Symbol (symbol, instance) -> Disambiguate.resolve ~env ~mk_choice (Symbol (symbol, instance)) (`Args []) - | CicNotationPt.Variable _ - | CicNotationPt.Magic _ - | CicNotationPt.Layout _ - | CicNotationPt.Literal _ -> assert false (* god bless Bologna *) + | NotationPt.Variable _ + | NotationPt.Magic _ + | NotationPt.Layout _ + | NotationPt.Literal _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation - | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) -> + | Some (NotationPt.AttributedTerm (`Loc loc, term)) -> let res = aux_option ~localize loc context annotation (Some term) in if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; res - | Some (CicNotationPt.AttributedTerm (_, term)) -> + | Some (NotationPt.AttributedTerm (_, term)) -> aux_option ~localize loc context annotation (Some term) - | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation - | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector + | Some NotationPt.Implicit `JustOne -> NCic.Implicit annotation + | Some NotationPt.Implicit `Vector -> NCic.Implicit `Vector | Some term -> aux ~localize loc context term in (fun ~context -> aux ~localize:true HExtlib.dummy_floc context), @@ -442,7 +442,7 @@ let interpretate_obj interpretate_term_option ~mk_choice ~localization_tbl ~obj_context in let uri = match uri with | None -> assert false | Some u -> u in match obj with - | CicNotationPt.Theorem (flavour, name, ty, bo, pragma) -> + | NotationPt.Theorem (flavour, name, ty, bo, pragma) -> let ty' = interpretate_term ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty @@ -459,7 +459,7 @@ let interpretate_obj NCic.Constant ([],name,Some (NCic.Implicit `Term),ty',attrs) | Some bo,_ -> (match bo with - | CicNotationPt.LetRec (kind, defs, _) -> + | NotationPt.LetRec (kind, defs, _) -> let inductive = kind = `Inductive in let _,obj_context = List.fold_left @@ -476,7 +476,7 @@ let interpretate_obj let add_binders kind t = List.fold_right (fun var t -> - CicNotationPt.Binder (kind, var, t)) params t + NotationPt.Binder (kind, var, t)) params t in let cic_body = interpretate_term @@ -501,14 +501,14 @@ let interpretate_obj in let attrs = `Provided, new_flavour_of_flavour flavour, pragma in NCic.Constant ([],name,Some bo,ty',attrs))) - | CicNotationPt.Inductive (params,tyl) -> + | NotationPt.Inductive (params,tyl) -> let context,params = let context,res = List.fold_left (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit `JustOne + None -> NotationPt.Implicit `JustOne | Some t -> t in let name = cic_name_of_name name in let t = @@ -557,14 +557,14 @@ let interpretate_obj let attrs = `Provided, `Regular in uri, height, [], [], NCic.Inductive (inductive,leftno,tyl,attrs) - | CicNotationPt.Record (params,name,ty,fields) -> + | NotationPt.Record (params,name,ty,fields) -> let context,params = let context,res = List.fold_left (fun (context,res) (name,t) -> let t = match t with - None -> CicNotationPt.Implicit `JustOne + None -> NotationPt.Implicit `JustOne | Some t -> t in let name = cic_name_of_name name in let t = @@ -621,11 +621,11 @@ let disambiguate_term ~context ~metasenv ~subst ~expty let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let res,b = MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:CicNotationUtil.freshen_term + ~freshen_thing:NotationUtil.freshen_term ~context ~metasenv ~initial_ugraph:() ~aliases ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) - ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term + ~universe ~uri:None ~pp_thing:NotationPp.pp_term ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term ~interpretate_thing:(interpretate_term ~obj_context:[] ~mk_choice (?create_dummy_ids:None)) @@ -643,13 +643,13 @@ let disambiguate_obj let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in let res,b = MultiPassDisambiguator.disambiguate_thing - ~freshen_thing:CicNotationUtil.freshen_obj + ~freshen_thing:NotationUtil.freshen_obj ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases ~mk_implicit ~description_of_alias ~fix_instance ~string_context_of_context:(List.map (fun (x,_) -> Some x)) ~universe ~uri:(Some uri) - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~pp_thing:(NotationPp.pp_obj NotationPp.pp_term) ~passes:(MultiPassDisambiguator.passes ()) ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj ~interpretate_thing:(interpretate_obj ~mk_choice) diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.mli b/matita/components/ng_disambiguation/nCicDisambiguate.mli index d28708e3a..25ac95ff4 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.mli +++ b/matita/components/ng_disambiguation/nCicDisambiguate.mli @@ -30,7 +30,7 @@ val disambiguate_term : DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> 'alias list) -> - CicNotationPt.term Disambiguate.disambiguator_input -> + NotationPt.term Disambiguate.disambiguator_input -> ((DisambiguateTypes.domain_item * 'alias) list * NCic.metasenv * NCic.substitution * @@ -51,10 +51,10 @@ val disambiguate_obj : DisambiguateTypes.Environment.key -> 'alias list) -> uri:NUri.uri -> - string * int * CicNotationPt.term CicNotationPt.obj -> + string * int * NotationPt.term NotationPt.obj -> ((DisambiguateTypes.Environment.key * 'alias) list * NCic.metasenv * NCic.substitution * NCic.obj) list * bool -val disambiguate_path: CicNotationPt.term -> NCic.term +val disambiguate_path: NotationPt.term -> NCic.term diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index b493edb6a..8d41e88e1 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -20,7 +20,7 @@ let fresh_name = let mk_id id = let id = if id = "_" then fresh_name () else id in - CicNotationPt.Ident (id,None) + NotationPt.Ident (id,None) ;; (*CSC: cut&paste from nCicReduction.split_prods, but does not check that @@ -38,8 +38,8 @@ let mk_appl = function [] -> assert false | [x] -> x - | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2) - | l -> CicNotationPt.Appl l + | NotationPt.Appl l1 :: l2 -> NotationPt.Appl (l1 @ l2) + | l -> NotationPt.Appl l ;; let mk_elim uri leftno it (outsort,suffix) pragma = @@ -55,11 +55,11 @@ let mk_elim uri leftno it (outsort,suffix) pragma = let rec_arg = mk_id (fresh_name ()) in let p_ty = List.fold_right - (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args - (CicNotationPt.Binder + (fun name res -> NotationPt.Binder (`Forall,(name,None),res)) args + (NotationPt.Binder (`Forall, (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), - CicNotationPt.Sort outsort)) in + NotationPt.Sort outsort)) in let args = args @ [rec_arg] in let k_names = List.map (function _,name,_ -> name_of_k name) cl in let final_params = @@ -92,29 +92,29 @@ let mk_elim uri leftno it (outsort,suffix) pragma = name, Some ( List.fold_right (fun id res -> - CicNotationPt.Binder (`Lambda,(id,None),res)) + NotationPt.Binder (`Lambda,(id,None),res)) abs - (CicNotationPt.Appl + (NotationPt.Appl (rec_name :: params @ [p_name] @ k_names @ - List.map (fun _ -> CicNotationPt.Implicit `JustOne) + List.map (fun _ -> NotationPt.Implicit `JustOne) (List.tl args) @ [mk_appl (name::abs)]))) | _ -> mk_id name,None ) cargs in let cargs,recursive_args = List.split cargs_and_recursive_args in let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in - CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), + NotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), mk_appl (name_of_k name :: cargs @ recursive_args) ) cl in - let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in + let bo = NotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in let recno = List.length final_params in let where = recno - 1 in let res = - CicNotationPt.LetRec (`Inductive, + NotationPt.LetRec (`Inductive, [final_params, (rec_name,ty), bo, where], rec_name) in (* @@ -122,7 +122,7 @@ let mk_elim uri leftno it (outsort,suffix) pragma = (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) - 80 (CicNotationPres.render (fun _ -> None) + 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res))); prerr_endline "#####"; let cobj = ("xxx", [], None, `Joint { @@ -136,7 +136,7 @@ let mk_elim uri leftno it (outsort,suffix) pragma = def_term = bo; def_type = List.fold_right - (fun x t -> CicNotationPt.Binder(`Forall,x,t)) + (fun x t -> NotationPt.Binder(`Forall,x,t)) final_params cty } ]; @@ -147,11 +147,11 @@ let mk_elim uri leftno it (outsort,suffix) pragma = prerr_endline ( (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) 80 - (CicNotationPres.mpres_of_box boxml))); + (NotationPres.mpres_of_box boxml))); *) - CicNotationPt.Theorem + NotationPt.Theorem (`Definition,srec_name, - CicNotationPt.Implicit `JustOne,Some res,pragma) + NotationPt.Implicit `JustOne,Some res,pragma) ;; let ast_of_sort s = @@ -190,7 +190,7 @@ let mk_lambda = function [] -> assert false | [t] -> t - | l -> CicNotationPt.Appl l + | l -> NotationPt.Appl l ;; let rec count_prods = function NCic.Prod (_,_,t) -> 1 + count_prods t | _ -> 0;; @@ -208,21 +208,21 @@ let rec pp rels = function NCic.Rel i -> List.nth rels (i - 1) | NCic.Const _ as t -> - CicNotationPt.Ident + NotationPt.Ident (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t,None) - | NCic.Sort s -> CicNotationPt.Sort (fst (ast_of_sort s)) + | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s)) | NCic.Meta _ | NCic.Implicit _ -> assert false - | NCic.Appl l -> CicNotationPt.Appl (List.map (pp rels) l) + | NCic.Appl l -> NotationPt.Appl (List.map (pp rels) l) | NCic.Prod (n,s,t) -> let n = mk_id n in - CicNotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t) + NotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t) | NCic.Lambda (n,s,t) -> let n = mk_id n in - CicNotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) + NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) | NCic.LetIn (n,s,ty,t) -> let n = mk_id n in - CicNotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) + NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> let name = NUri.name_of_uri uri in let case_indty = Some (name, None) in @@ -245,11 +245,11 @@ let rec pp rels = List.map2 (fun (_, name, ty) pat -> let capture_variables,rhs = eat_branch leftno rels ty pat in - CicNotationPt.Pattern (name, None, capture_variables), rhs + NotationPt.Pattern (name, None, capture_variables), rhs ) constructors patterns with Invalid_argument _ -> assert false in - CicNotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns) + NotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns) ;; let mk_projection leftno tyname consname consty (projname,_,_) i = @@ -260,19 +260,19 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = let arg = mk_id "xxx" in let arg_ty = mk_appl (mk_id tyname :: List.rev names) in let bvar = mk_id "yyy" in - let underscore = CicNotationPt.Ident ("_",None),None in + let underscore = NotationPt.Ident ("_",None),None in let bvars = HExtlib.mk_list underscore i @ [bvar,None] @ HExtlib.mk_list underscore (argsno - i -1) in - let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in + let branch = NotationPt.Pattern (consname,None,bvars), bvar in let projs,outtype = nth_prod [] i ty in let rels = List.map (fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs @ names in let outtype = pp rels outtype in - let outtype= CicNotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in - [arg, Some arg_ty], CicNotationPt.Case (arg,None,Some outtype,[branch]) + let outtype= NotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in + [arg, Some arg_ty], NotationPt.Case (arg,None,Some outtype,[branch]) | _,NCic.Prod (name,_,t) -> let name = mk_id name in let params,body = aux (name::names) t (leftno - 1) in @@ -282,16 +282,16 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = let params,bo = aux [] consty leftno in let pprojname = mk_id projname in let res = - CicNotationPt.LetRec (`Inductive, + NotationPt.LetRec (`Inductive, [params, (pprojname,None), bo, leftno], pprojname) in (* prerr_endline (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) - 80 (CicNotationPres.render (fun _ -> None) + 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) - CicNotationPt.Theorem - (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection) + NotationPt.Theorem + (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection) ;; let mk_projections (_,_,_,_,obj) = diff --git a/matita/components/ng_tactics/nCicElim.mli b/matita/components/ng_tactics/nCicElim.mli index bbb96facb..470a800a1 100644 --- a/matita/components/ng_tactics/nCicElim.mli +++ b/matita/components/ng_tactics/nCicElim.mli @@ -11,7 +11,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list -val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list +val mk_elims: NCic.obj -> NotationPt.term NotationPt.obj list +val mk_projections: NCic.obj -> NotationPt.term NotationPt.obj list val ast_of_sort : NCic.sort -> [> `NCProp of string | `NType of string | `Prop ] * string diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml index 7814aacfd..25d297be2 100644 --- a/matita/components/ng_tactics/nDestructTac.ml +++ b/matita/components/ng_tactics/nDestructTac.ml @@ -41,20 +41,20 @@ let fresh_name = let mk_id id = let id = if id = "_" then fresh_name () else id in - CicNotationPt.Ident (id,None) + NotationPt.Ident (id,None) ;; let rec mk_prods l t = match l with [] -> t - | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) + | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; let mk_appl = function [] -> assert false | [x] -> x - | l -> CicNotationPt.Appl l + | l -> NotationPt.Appl l ;; let rec iter f n acc = @@ -124,7 +124,7 @@ let nargs it nleft consno = let _,_,t_k = List.nth cl consno in List.length (arg_list nleft t_k) ;; -let default_pattern = "",0,(None,[],Some CicNotationPt.UserInput);; +let default_pattern = "",0,(None,[],Some NotationPt.UserInput);; (* returns the discrimination = injection+contradiction principle *) @@ -135,8 +135,8 @@ let mk_discriminator it ~use_jmeq nleft xyty status = let mk_eq tys ts us es n = if use_jmeq then mk_appl [mk_id "jmeq"; - CicNotationPt.Implicit `JustOne; List.nth ts n; - CicNotationPt.Implicit `JustOne; List.nth us n] + NotationPt.Implicit `JustOne; List.nth ts n; + NotationPt.Implicit `JustOne; List.nth us n] else (* eqty = Tn u0 e0...un-1 en-1 *) let eqty = mk_appl @@ -170,54 +170,54 @@ let mk_discriminator it ~use_jmeq nleft xyty status = let tys = List.map (fun x -> iter (fun i acc -> - CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), - CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), + NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), + NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), acc))) (x-1) - (CicNotationPt.Implicit (`Tagged ("T" ^ (string_of_int x))))) + (NotationPt.Implicit (`Tagged ("T" ^ (string_of_int x))))) (HExtlib.list_seq 0 nargs) in let tys = tys @ [iter (fun i acc -> - CicNotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), - CicNotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), + NotationPt.Binder (`Lambda, (mk_id ("x" ^ string_of_int i), None), + NotationPt.Binder (`Lambda, (mk_id ("p" ^ string_of_int i), None), acc))) (nargs-1) - (mk_appl [mk_id "eq"; CicNotationPt.Implicit `JustOne; + (mk_appl [mk_id "eq"; NotationPt.Implicit `JustOne; mk_appl (mk_id (kname it i):: List.map (fun x -> mk_id ("x" ^string_of_int x)) (HExtlib.list_seq 0 (List.length ts))); mk_appl (mk_id (kname it j)::us)])] in - (** CicNotationPt.Binder (`Lambda, (mk_id "e", + (** NotationPt.Binder (`Lambda, (mk_id "e", Some (mk_appl [mk_id "eq"; - CicNotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; mk_appl (mk_id (kname it i)::ts); mk_appl (mk_id (kname it j)::us)])), let ts = ts @ [mk_id "e"] in let refl2 = mk_appl [mk_id "refl"; - CicNotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; mk_appl (mk_id (kname it j)::us)] in let us = us @ [refl2] in *) - CicNotationPt.Binder (`Forall, (mk_id "P", Some (CicNotationPt.Sort (`NType "1") )), + NotationPt.Binder (`Forall, (mk_id "P", Some (NotationPt.Sort (`NType "1") )), if i = j then - CicNotationPt.Binder (`Forall, (mk_id "_", + NotationPt.Binder (`Forall, (mk_id "_", Some (iter (fun i acc -> - CicNotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc)) + NotationPt.Binder (`Forall, (List.nth es i, Some (mk_eq tys ts us es i)), acc)) (nargs-1) - (** (CicNotationPt.Binder (`Forall, (mk_id "_", + (** (NotationPt.Binder (`Forall, (mk_id "_", Some (mk_eq tys ts us es nargs)),*) (mk_id "P"))), mk_id "P") else mk_id "P") in - let inner i ts = CicNotationPt.Case + let inner i ts = NotationPt.Case (mk_id "y",None, - (*Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None), - CicNotationPt.Binder (`Forall, (mk_id "_", Some - (mk_appl [mk_id "eq";CicNotationPt.Implicit - `JustOne;(*CicNotationPt.Implicit `JustOne*) + (*Some (NotationPt.Binder (`Lambda, (mk_id "y",None), + NotationPt.Binder (`Forall, (mk_id "_", Some + (mk_appl [mk_id "eq";NotationPt.Implicit + `JustOne;(*NotationPt.Implicit `JustOne*) mk_appl (mk_id (kname it i)::ts);mk_id "y"])), - CicNotationPt.Implicit `JustOne )))*) + NotationPt.Implicit `JustOne )))*) None, List.map (fun j -> @@ -226,13 +226,13 @@ let mk_discriminator it ~use_jmeq nleft xyty status = (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - CicNotationPt.Pattern (kname it j, + NotationPt.Pattern (kname it j, None, List.combine us nones), branch i j ts us) (HExtlib.list_seq 0 (List.length cl))) in - let outer = CicNotationPt.Case + let outer = NotationPt.Case (mk_id "x",None, None , List.map @@ -242,15 +242,15 @@ let mk_discriminator it ~use_jmeq nleft xyty status = (nargs_kty - 1) [] in let nones = iter (fun _ acc -> None::acc) (nargs_kty - 1) [] in - CicNotationPt.Pattern (kname it i, + NotationPt.Pattern (kname it i, None, List.combine ts nones), inner i ts) (HExtlib.list_seq 0 (List.length cl))) in - let principle = CicNotationPt.Binder (`Lambda, (mk_id "x", Some xyty), - CicNotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer)) + let principle = NotationPt.Binder (`Lambda, (mk_id "x", Some xyty), + NotationPt.Binder (`Lambda, (mk_id "y", Some xyty), outer)) in - pp (lazy ("discriminator = " ^ (CicNotationPp.pp_term principle))); + pp (lazy ("discriminator = " ^ (NotationPp.pp_term principle))); status, principle ;; @@ -332,13 +332,13 @@ let discriminate_tac ~context cur_eq status = NTactics.block_tac ( [(fun status -> let status, discr = mk_discriminator it ~use_jmeq leftno xyty status in - let cut_term = mk_prods params (CicNotationPt.Binder (`Forall, (mk_id "x", + let cut_term = mk_prods params (NotationPt.Binder (`Forall, (mk_id "x", Some xyty), - CicNotationPt.Binder (`Forall, (mk_id "y", Some xyty), - CicNotationPt.Binder (`Forall, (mk_id "e", - Some (mk_appl [mk_id "eq";CicNotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), + NotationPt.Binder (`Forall, (mk_id "y", Some xyty), + NotationPt.Binder (`Forall, (mk_id "e", + Some (mk_appl [mk_id "eq";NotationPt.Implicit `JustOne; mk_id "x"; mk_id "y"])), mk_appl [discr; mk_id "x"; mk_id "y"(*;mk_id "e"*)])))) in - let status = print_tac (lazy ("cut_term = "^ CicNotationPp.pp_term cut_term)) status in + let status = print_tac (lazy ("cut_term = "^ NotationPp.pp_term cut_term)) status in NTactics.cut_tac ("",0, cut_term) status); NTactics.branch_tac; @@ -356,7 +356,7 @@ let discriminate_tac ~context cur_eq status = print_tac (lazy "ci sono 3"); NTactics.intro_tac "#discriminate"; NTactics.apply_tac ("",0,mk_appl ([mk_id "#discriminate"]@ - HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length params + 2) @ + HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length params + 2) @ [mk_id eq_name ])); NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern; NTactics.clear_tac ["#discriminate"]; @@ -403,7 +403,7 @@ let subst_tac ~context ~dir skip cur_eq = else let gen_tac x = NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in + ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in NTactics.block_tac ((List.map gen_tac names_to_gen)@ [NTactics.clear_tac names_to_gen; NTactics.rewrite_tac ~dir @@ -434,14 +434,14 @@ let clearid_tac ~context skip cur_eq = let names_to_gen = names_to_gen @ [eq_name] in let gen_tac x = NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in + ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in NTactics.block_tac ((List.map gen_tac names_to_gen)@ [NTactics.clear_tac names_to_gen; NTactics.apply_tac ("",0, mk_appl [streicher_id; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne]); + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]); NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern] @ (let names_to_intro = @@ -462,14 +462,14 @@ let clearid_tac ~context skip cur_eq = let names_to_gen = names_to_gen @ [eq_name] in let gen_tac x = NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in + ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in NTactics.block_tac ((List.map gen_tac names_to_gen)@ [NTactics.clear_tac names_to_gen; NTactics.apply_tac ("",0, mk_appl [streicher_id; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne]); + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]); NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern] @ (let names_to_intro = @@ -486,21 +486,21 @@ let clearid_tac ~context skip cur_eq = let names_to_gen = names_to_gen (* @ [eq_name]*) in let gen_tac x = NTactics.generalize_tac - ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in + ~where:("",0,(Some (mk_id x),[], Some NotationPt.UserInput)) in let gen_eq = NTactics.generalize_tac ~where:("",0,(Some (mk_appl [mk_id "jmeq_to_eq"; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - mk_id eq_name]),[], Some CicNotationPt.UserInput)) in + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + mk_id eq_name]),[], Some NotationPt.UserInput)) in NTactics.block_tac ((List.map gen_tac names_to_gen)@gen_eq:: [NTactics.clear_tac names_to_gen; NTactics.try_tac (NTactics.clear_tac [eq_name]); NTactics.apply_tac ("",0, mk_appl [streicher_id; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne; - CicNotationPt.Implicit `JustOne]); + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne; + NotationPt.Implicit `JustOne]); NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern] @ (let names_to_intro = List.rev names_to_gen in diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index aebda4bce..904a221ff 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -23,7 +23,7 @@ let fresh_name = let mk_id id = let id = if id = "_" then fresh_name () else id in - CicNotationPt.Ident (id,None) + NotationPt.Ident (id,None) ;; let rec split_arity ~subst context te = @@ -37,13 +37,13 @@ let mk_appl = function [] -> assert false | [x] -> x - | l -> CicNotationPt.Appl l + | l -> NotationPt.Appl l ;; let rec mk_prods l t = match l with [] -> t - | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) + | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; let rec mk_arrows ?(pattern=false) xs ys selection target = @@ -51,7 +51,7 @@ let rec mk_arrows ?(pattern=false) xs ys selection target = [],[],[] -> target | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target | true :: l,x::xs,y::ys -> - CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then CicNotationPt.Implicit `JustOne else mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), + NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])), mk_arrows ~pattern xs ys l target) | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; @@ -118,15 +118,15 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = let outsort, suffix = NCicElim.ast_of_sort outsort in let theorem = mk_prods xs - (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))), - mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs))))) + (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (NotationPt.Sort outsort))), + mk_prods hyplist (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs))))) in let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def",0, - CicNotationPt.Theorem + NotationPt.Theorem (`Theorem,name,theorem, - Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) + Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in @@ -138,18 +138,18 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = let rs = List.map (fun x -> mk_id x) rs in mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in - let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), + let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), -CicNotationPt.Implicit (`Tagged "end")); - CicNotationPt.Implicit (`Tagged "cut")] in +NotationPt.Implicit (`Tagged "end")); + NotationPt.Implicit (`Tagged "cut")] in let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in let where = "",0,(None,[], Some ( mk_arrows ~pattern:true - (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys)) - (HExtlib.mk_list CicNotationPt.UserInput (List.length ys)) - selection CicNotationPt.UserInput)) in + (HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length ys)) + (HExtlib.mk_list NotationPt.UserInput (List.length ys)) + selection NotationPt.UserInput)) in let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in let status = NTactics.block_tac diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml index 1aaeb50f6..9f653abd5 100644 --- a/matita/components/ng_tactics/nTacStatus.ml +++ b/matita/components/ng_tactics/nTacStatus.ml @@ -48,7 +48,7 @@ class pstatus = = fun o -> (self#set_estatus o)#set_obj o#obj end -type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input +type tactic_term = NotationPt.term Disambiguate.disambiguator_input type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input let pp_tac_status status = diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli index 561679457..a51435e24 100644 --- a/matita/components/ng_tactics/nTacStatus.mli +++ b/matita/components/ng_tactics/nTacStatus.mli @@ -29,7 +29,7 @@ class pstatus : method set_pstatus: #g_pstatus -> 'self end -type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input +type tactic_term = NotationPt.term Disambiguate.disambiguator_input type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input type cic_term diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index c45e825a4..09427a315 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -18,7 +18,7 @@ let debug_print s = if debug then prerr_endline (Lazy.force s) else () open Continuationals.Stack open NTacStatus -module Ast = CicNotationPt +module Ast = NotationPt let id_tac status = status ;; let print_tac print_status message status = diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml index 96ccf0e0d..5080e34bf 100644 --- a/matita/components/ng_tactics/nnAuto.ml +++ b/matita/components/ng_tactics/nnAuto.ml @@ -18,7 +18,7 @@ let debug_print = noprint open Continuationals.Stack open NTacStatus -module Ast = CicNotationPt +module Ast = NotationPt (* ======================= statistics ========================= *) @@ -73,7 +73,7 @@ let print_stat tbl = Pervasives.compare (relevance v1) (relevance v2) in let l = List.sort vcompare l in let vstring (a,v)= - CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^ + NotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^ (string_of_float (relevance v)) ^ "; uses = " ^ (string_of_int !(v.uses)) ^ "; nom = " ^ (string_of_int !(v.nominations)) in @@ -140,7 +140,7 @@ let is_a_fact_obj s uri = let is_a_fact_ast status subst metasenv ctx cand = debug_print ~depth:0 - (lazy ("------- checking " ^ CicNotationPp.pp_term cand)); + (lazy ("------- checking " ^ NotationPp.pp_term cand)); let status, t = disambiguate status ctx ("",0,cand) None in let status,t = term_of_cic_term status t ctx in let ty = NCicTypeChecker.typeof subst metasenv ctx t in @@ -815,14 +815,14 @@ type cache = let add_to_trace ~depth cache t = match t with | Ast.NRef _ -> - debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t)); + debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term t)); {cache with trace = t::cache.trace} | Ast.NCic _ (* local candidate *) | _ -> (*not an application *) cache let pptrace tr = (lazy ("Proof Trace: " ^ (String.concat ";" - (List.map CicNotationPp.pp_term tr)))) + (List.map NotationPp.pp_term tr)))) (* not used let remove_from_trace cache t = match t with @@ -896,7 +896,7 @@ let sort_candidates status ctx candidates = List.sort (fun (a,_) (b,_) -> a - b) candidates in let candidates = List.map snd candidates in debug_print (lazy ("candidates =\n" ^ (String.concat "\n" - (List.map CicNotationPp.pp_term candidates)))); + (List.map NotationPp.pp_term candidates)))); candidates let sort_new_elems l = @@ -904,7 +904,7 @@ let sort_new_elems l = let try_candidate ?(smart=0) flags depth status eq_cache ctx t = try - debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t)); + debug_print ~depth (lazy ("try " ^ NotationPp.pp_term t)); let status = if smart= 0 then NTactics.apply_tac ("",0,t) status else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status @@ -1626,7 +1626,7 @@ auto_main flags signature cache depth status: unit = (lazy ("(re)considering goal " ^ (string_of_int g) ^" : "^ppterm status gty)); debug_print (~depth:depth) - (lazy ("Case: " ^ CicNotationPp.pp_term t)); + (lazy ("Case: " ^ NotationPp.pp_term t)); let depth,cache = if t=Ast.Ident("__whd",None) || t=Ast.Ident("__intros",None) diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli index 2376a773a..87b2e8e4b 100644 --- a/matita/components/ng_tactics/nnAuto.mli +++ b/matita/components/ng_tactics/nnAuto.mli @@ -29,7 +29,7 @@ val smart_apply_tac: val auto_tac: params:(NTacStatus.tactic_term list option * (string * string) list) -> - ?trace_ref:CicNotationPt.term list ref -> + ?trace_ref:NotationPt.term list ref -> 's NTacStatus.tactic val keys_of_type: diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 92b2d8e1c..070a7a48f 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -27,8 +27,8 @@ val eval_ast : ?do_heavy_checks:bool -> GrafiteTypes.status -> string * int * - ((CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) + ((NotationPt.term, NotationPt.term, + NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string) GrafiteAst.statement) -> (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list @@ -50,8 +50,8 @@ val eval_from_stream : GrafiteTypes.status -> Ulexing.lexbuf -> (GrafiteTypes.status -> - (CicNotationPt.term, CicNotationPt.term, - CicNotationPt.term GrafiteAst.reduction, CicNotationPt.term CicNotationPt.obj, string) + (NotationPt.term, NotationPt.term, + NotationPt.term GrafiteAst.reduction, NotationPt.term NotationPt.obj, string) GrafiteAst.statement -> unit) -> (GrafiteTypes.status * (DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b9fa4646..8a7b8fdcb 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -884,7 +884,7 @@ let blank_uri = BuildTimeConf.blank_uri let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = - [ `Ast of CicNotationPt.term + [ `Ast of NotationPt.term | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `String of string ] diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 62305ec00..1de645619 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -125,7 +125,7 @@ let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statem ;; let pp_eager_statement_ast = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = @@ -151,7 +151,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let m, s, status, t = GrafiteDisambiguate.disambiguate_nterm None status ctx menv subst (parsed_text,parsed_text_length, - CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne)) + NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s)); @@ -181,7 +181,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us | thms -> String.concat ", " (HExtlib.filter_map (function - | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) + | NotationPt.NRef r -> Some (NCicPp.r2s true r) | _ -> None) thms) in diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 114ed5937..d9ce848d5 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -36,9 +36,9 @@ let slash_n_RE = Pcre.regexp "\\n" ;; let pp_ast_statement grafite_status stm = let stm = GrafiteAstPp.pp_statement ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj - CicNotationPp.pp_term) stm + ~term_pp:NotationPp.pp_term + ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj + NotationPp.pp_term) stm in let stm = Pcre.replace ~rex:slash_n_RE stm in let stm = @@ -59,11 +59,11 @@ let dump f = let floc = H.dummy_floc in let nl_ast = G.Comment (floc, G.Note (floc, "")) in let pp_statement stm = - GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term + GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~lazy_term_pp:CicNotationPp.pp_term - ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm + ~lazy_term_pp:NotationPp.pp_term + ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm in let pp_lexicon = LexiconAstPp.pp_command in let och = open_out f in -- 2.39.2