From: Andrea Asperti Date: Fri, 8 Oct 2010 09:23:01 +0000 (+0000) Subject: cicNotation* ==> notation* X-Git-Tag: make_still_working~2792 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git cicNotation* ==> notation* --- 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/cicNotationEnv.ml b/matita/components/content/cicNotationEnv.ml deleted file mode 100644 index 5b4190eb8..000000000 --- a/matita/components/content/cicNotationEnv.ml +++ /dev/null @@ -1,153 +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/ - *) - -(* $Id$ *) - -module Ast = CicNotationPt - -type value = - | TermValue of Ast.term - | StringValue of string - | NumValue of string - | OptValue of value option - | ListValue of value list - -type value_type = - | TermType of int - | StringType - | NumType - | OptType of value_type - | ListType of value_type - -exception Value_not_found of string -exception Type_mismatch of string * value_type - -type declaration = string * value_type -type binding = string * (value_type * value) -type t = binding list - -let lookup env name = - try - List.assoc name env - with Not_found -> raise (Value_not_found name) - -let lookup_value env name = - try - snd (List.assoc name env) - with Not_found -> raise (Value_not_found name) - -let remove_name env name = List.remove_assoc name env - -let remove_names env names = - List.filter (fun name, _ -> not (List.mem name names)) env - -let lookup_term env name = - match lookup env name with - | _, TermValue x -> x - | ty, _ -> raise (Type_mismatch (name, ty)) - -let lookup_num env name = - match lookup env name with - | _, NumValue x -> x - | ty, _ -> raise (Type_mismatch (name, ty)) - -let lookup_string env name = - match lookup env name with - | _, StringValue x -> x - | ty, _ -> raise (Type_mismatch (name, ty)) - -let lookup_opt env name = - match lookup env name with - | _, OptValue x -> x - | ty, _ -> raise (Type_mismatch (name, ty)) - -let lookup_list env name = - match lookup env name with - | _, ListValue x -> x - | ty, _ -> raise (Type_mismatch (name, ty)) - -let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) -let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) -let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None)) -let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) -let opt_declaration (n, ty) = (n, OptType ty) -let list_declaration (n, ty) = (n, ListType ty) - -let declaration_of_var = function - | Ast.NumVar s -> s, NumType - | Ast.IdentVar s -> s, StringType - | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l - | _ -> assert false - -let value_of_term = function - | Ast.Num (s, _) -> NumValue s - | Ast.Ident (s, None) -> StringValue s - | t -> TermValue t - -let term_of_value = function - | NumValue s -> Ast.Num (s, 0) - | StringValue s -> Ast.Ident (s, None) - | TermValue t -> t - | _ -> assert false (* TO BE UNDERSTOOD *) - -let rec well_typed ty value = - match ty, value with - | TermType _, TermValue _ - | StringType, StringValue _ - | OptType _, OptValue None - | NumType, NumValue _ -> true - | OptType ty', OptValue (Some value') -> well_typed ty' value' - | ListType ty', ListValue vl -> - List.for_all (fun value' -> well_typed ty' value') vl - | _ -> false - -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) - -let rec combine decls values = - match decls, values with - | [], [] -> [] - | (name, ty) :: decls, v :: values -> - (name, (ty, v)) :: (combine decls values) - | _ -> assert false - -let coalesce_env declarations env_list = - let env0 = List.map list_binding_of_name declarations in - let grow_env_entry env n v = - List.map - (function - | (n', (ty, ListValue vl)) as entry -> - if n' = n then n', (ty, ListValue (v :: vl)) else entry - | _ -> assert false) - env - in - let grow_env env_i env = - List.fold_left - (fun env (n, (_, v)) -> grow_env_entry env n v) - env env_i - in - List.fold_right grow_env env_list env0 - diff --git a/matita/components/content/cicNotationEnv.mli b/matita/components/content/cicNotationEnv.mli deleted file mode 100644 index aa937d00c..000000000 --- a/matita/components/content/cicNotationEnv.mli +++ /dev/null @@ -1,92 +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/ - *) - -(** {2 Types} *) - -type value = - | TermValue of CicNotationPt.term - | StringValue of string - | NumValue of string - | OptValue of value option - | ListValue of value list - -type value_type = - | TermType of int (* the level of the expected term *) - | StringType - | NumType - | OptType of value_type - | ListType of value_type - - (** looked up value not found in environment *) -exception Value_not_found of string - - (** looked up value has the wrong type - * parameters are value name and value type in environment *) -exception Type_mismatch of string * value_type - -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 well_typed: value_type -> value -> bool - -val declarations_of_env: t -> declaration list -val declarations_of_term: CicNotationPt.term -> declaration list -val combine: declaration list -> value list -> t (** @raise Invalid_argument *) - -(** {2 Environment lookup} *) - -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_string: t -> string -> string -val lookup_num: t -> string -> string -val lookup_opt: t -> string -> value option -val lookup_list: t -> string -> value list - -val remove_name: t -> string -> t -val remove_names: t -> string list -> t - -(** {2 Bindings mangling} *) - -val opt_binding_some: binding -> binding (* v -> Some v *) -val opt_binding_none: binding -> binding (* v -> None *) - -val opt_binding_of_name: declaration -> binding (* None binding *) -val list_binding_of_name: declaration -> binding (* [] binding *) - -val opt_declaration: declaration -> declaration (* t -> OptType t *) -val list_declaration: declaration -> declaration (* t -> ListType t *) - -(** given a list of environments bindings a set of names n_1, ..., n_k, returns - * a single environment where n_i is bound to the list of values bound in the - * starting environments *) -val coalesce_env: declaration list -> t list -> t - diff --git a/matita/components/content/cicNotationPp.ml b/matita/components/content/cicNotationPp.ml deleted file mode 100644 index f94891375..000000000 --- a/matita/components/content/cicNotationPp.ml +++ /dev/null @@ -1,371 +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/ - *) - -(* $Id$ *) - -open Printf - -module Ast = CicNotationPt -module Env = CicNotationEnv - - (* when set to true debugging information, not in sync with input syntax, will - * be added to the output of pp_term. - * set to false if you need, for example, cut and paste from matitac output to - * matitatop *) -let debug_printing = false - -let pp_binder = function - | `Lambda -> "lambda" - | `Pi -> "Pi" - | `Exists -> "exists" - | `Forall -> "forall" - -let pp_literal = - if debug_printing then - (function (* debugging version *) - | `Symbol s -> sprintf "symbol(%s)" s - | `Keyword s -> sprintf "keyword(%s)" s - | `Number s -> sprintf "number(%s)" s) - else - (function - | `Symbol s - | `Keyword s - | `Number s -> s) - -let pp_pos = - function -(* `None -> "`None" *) - | `Left -> "`Left" - | `Right -> "`Right" - | `Inner -> "`Inner" - -let pp_attribute = - function - | `IdRef id -> sprintf "x(%s)" id - | `XmlAttrs attrs -> - sprintf "X(%s)" - (String.concat ";" - (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) - | `Level (prec) -> sprintf "L(%d)" prec - | `Raw _ -> "R" - | `Loc _ -> "@" - | `ChildPos p -> sprintf "P(%s)" (pp_pos p) - -let pp_capture_variable pp_term = - function - | term, None -> pp_term (* ~pp_parens:false *) term - | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")" - -let rec pp_term ?(pp_parens = true) t = - let t_pp = - match t with - | Ast.AttributedTerm (attr, term) when debug_printing -> - sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term) - | Ast.AttributedTerm (`Raw text, _) -> text - | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term - | Ast.Appl terms -> - sprintf "%s" (String.concat " " (List.map pp_term terms)) - | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body) - | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) -> - sprintf "%s \\to %s" - (match typ with None -> "?" | Some typ -> pp_term typ) - (pp_term ~pp_parens:true body) - | Ast.Binder (kind, var, body) -> - sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var) - (pp_term ~pp_parens:true body) - | Ast.Case (term, indtype, typ, patterns) -> - sprintf "match %s%s%s with %s" - (pp_term term) - (match indtype with - | None -> "" - | Some (ty, href_opt) -> - sprintf " in %s%s" ty - (match debug_printing, href_opt with - | true, Some uri -> - sprintf "(i.e.%s)" (UriManager.string_of_uri uri) - | _ -> "")) - (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) - (pp_patterns patterns) - | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) - | Ast.LetIn ((var,t2), t1, t3) -> -(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) - sprintf "let %s \\def %s in %s" (pp_term var) -(* (pp_term ~pp_parens:true t2) *) - (pp_term ~pp_parens:true t1) - (pp_term ~pp_parens:true t3) - | Ast.LetRec (kind, definitions, term) -> - let rec get_guard i = function - | [] -> (*assert false*) Ast.Implicit `JustOne - | [term, _] when i = 1 -> term - | _ :: tl -> get_guard (pred i) tl - in - let map (params, (id,typ), body, i) = - let typ = - match typ with - None -> Ast.Implicit `JustOne - | Some typ -> typ - in - sprintf "%s %s on %s: %s \\def %s" - (pp_term ~pp_parens:false term) - (String.concat " " (List.map (pp_capture_variable pp_term) params)) - (pp_term ~pp_parens:false (get_guard i params)) - (pp_term typ) (pp_term body) - in - sprintf "let %s %s in %s" - (match kind with `Inductive -> "rec" | `CoInductive -> "corec") - (String.concat " and " (List.map map definitions)) - (pp_term term) - | Ast.Ident (name, Some []) | Ast.Ident (name, None) - | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name - | Ast.NRef nref -> NReference.string_of_reference nref - | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic - | Ast.Ident (name, Some substs) - | Ast.Uri (name, Some substs) -> - sprintf "%s \\subst [%s]" name (pp_substs substs) - | Ast.Implicit `Vector -> "…" - | Ast.Implicit `JustOne -> "?" - | Ast.Implicit (`Tagged name) -> "?"^name - | Ast.Meta (index, substs) -> - sprintf "%d[%s]" index - (String.concat "; " - (List.map (function None -> "?" | Some t -> pp_term t) substs)) - | Ast.Num (num, _) -> num - | Ast.Sort `Set -> "Set" - | Ast.Sort `Prop -> "Prop" - | Ast.Sort (`Type _) -> "Type" - | Ast.Sort (`CProp _)-> "CProp" - | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" - | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" - | Ast.Symbol (name, _) -> "'" ^ name - - | Ast.UserInput -> "%" - - | Ast.Literal l -> pp_literal l - | Ast.Layout l -> pp_layout l - | Ast.Magic m -> pp_magic m - | Ast.Variable v -> pp_variable v - in - match pp_parens, t with - | false, _ - | true, Ast.Implicit _ - | true, Ast.UserInput - | true, Ast.Sort _ - | true, Ast.Ident (_, Some []) - | true, Ast.Ident (_, None) -> t_pp - | _ -> sprintf "(%s)" t_pp - -and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) -and pp_substs substs = String.concat "; " (List.map pp_subst substs) - -and pp_pattern = - function - Ast.Pattern (head, href, vars), term -> - let head_pp = - head ^ - (match debug_printing, href with - | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) - | _ -> "") - in - sprintf "%s \\Rightarrow %s" - (match vars with - | [] -> head_pp - | _ -> - sprintf "(%s %s)" head_pp - (String.concat " " (List.map (pp_capture_variable pp_term) vars))) - (pp_term term) - | Ast.Wildcard, term -> - sprintf "_ \\Rightarrow %s" (pp_term term) - -and pp_patterns patterns = - sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) - -and pp_box_spec (kind, spacing, indent) = - let int_of_bool b = if b then 1 else 0 in - let kind_string = - match kind with - Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV" - in - sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent) - -and pp_layout = function - | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2) - | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2) - | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2) - | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2) - | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2) - | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2) - | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2) - | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) - (pp_term t2) (pp_term t3) - | Ast.Maction l -> sprintf "\\MACTION (%s)" - (String.concat "," (List.map pp_term l)) - | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t) - | Ast.Root (arg, index) -> - sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) - | Ast.Break -> "\\BREAK" -(* | Space -> "\\SPACE" *) - | Ast.Box (box_spec, terms) -> - sprintf "\\%s [%s]" (pp_box_spec box_spec) - (String.concat " " (List.map pp_term terms)) - | Ast.Group terms -> - sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) - | Ast.Mstyle (l,terms) -> - sprintf "\\MSTYLE %s [%s]" - (String.concat " " (List.map (fun (k,v) -> k^"="^v) l)) - (String.concat " " (List.map pp_term terms)) - | Ast.Mpadded (l,terms) -> - sprintf "\\MSTYLE %s [%s]" - (String.concat " " (List.map (fun (k,v) -> k^"="^v) l)) - (String.concat " " (List.map pp_term terms)) - -and pp_magic = function - | Ast.List0 (t, sep_opt) -> - sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | Ast.List1 (t, sep_opt) -> - sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt) - | Ast.Opt t -> sprintf "opt %s" (pp_term t) - | Ast.Fold (kind, p_base, names, p_rec) -> - let acc = match names with acc :: _ -> acc | _ -> assert false in - sprintf "fold %s %s rec %s %s" - (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec) - | Ast.Default (p_some, p_none) -> - sprintf "default %s %s" (pp_term p_some) (pp_term p_none) - | Ast.If (p_test, p_true, p_false) -> - sprintf "if %s then %s else %s" - (pp_term p_test) (pp_term p_true) (pp_term p_false) - | Ast.Fail -> "fail" - -and pp_fold_kind = function - | `Left -> "left" - | `Right -> "right" - -and pp_sep_opt = function - | None -> "" - | Some sep -> sprintf " sep %s" (pp_literal sep) - -and pp_variable = function - | Ast.NumVar s -> "number " ^ s - | Ast.IdentVar s -> "ident " ^ s - | Ast.TermVar (s,Ast.Self _) -> s - | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l - | Ast.Ascription (t, n) -> assert false - | Ast.FreshVar n -> "fresh " ^ n - -let _pp_term = ref (pp_term ~pp_parens:false) -let pp_term t = !_pp_term t -let set_pp_term f = _pp_term := f - -let pp_params pp_term = function - | [] -> "" - | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) - -let pp_flavour = function - | `Definition -> "definition" - | `MutualDefinition -> assert false - | `Fact -> "fact" - | `Goal -> "goal" - | `Lemma -> "lemma" - | `Remark -> "remark" - | `Theorem -> "theorem" - | `Variant -> "variant" - | `Axiom -> "axiom" - -let pp_fields pp_term fields = - (if fields <> [] then "\n" else "") ^ - String.concat ";\n" - (List.map - (fun (name,ty,coercion,arity) -> - " " ^ name ^ - (if coercion then - (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") - else ": ") ^ - pp_term ty) - fields) - -let pp_obj pp_term = function - | Ast.Inductive (params, types) -> - let pp_constructors constructors = - String.concat "\n" - (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) - constructors) - in - let pp_type (name, _, typ, constructors) = - sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) - (pp_constructors constructors) - in - (match types with - | [] -> assert false - | (name, inductive, typ, constructors) :: tl -> - let fst_typ_pp = - sprintf "%sinductive %s%s: %s \\def\n%s" - (if inductive then "" else "co") name (pp_params pp_term params) - (pp_term typ) (pp_constructors constructors) - in - fst_typ_pp ^ String.concat "" (List.map pp_type tl)) - | Ast.Theorem (`MutualDefinition, name, typ, body,_) -> - sprintf "<>" - | Ast.Theorem (flavour, name, typ, body,_) -> - sprintf "%s %s:\n %s\n%s" - (pp_flavour flavour) - name - (pp_term typ) - (match body with - | None -> "" - | Some body -> "\\def\n " ^ pp_term body) - | Ast.Record (params,name,ty,fields) -> - "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ - " \\def {" ^ pp_fields pp_term fields ^ "\n}" - -let rec pp_value = function - | Env.TermValue t -> sprintf "$%s$" (pp_term t) - | Env.StringValue s -> sprintf "\"%s\"" s - | Env.NumValue n -> n - | Env.OptValue (Some v) -> "Some " ^ pp_value v - | Env.OptValue None -> "None" - | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l)) - -let rec pp_value_type = - function - | Env.TermType l -> "Term "^string_of_int l - | Env.StringType -> "String" - | Env.NumType -> "Number" - | Env.OptType t -> "Maybe " ^ pp_value_type t - | Env.ListType l -> "List " ^ pp_value_type l - -let pp_env env = - String.concat "; " - (List.map - (fun (name, (ty, value)) -> - sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value)) - env) - -let rec pp_cic_appl_pattern = function - | Ast.UriPattern uri -> UriManager.string_of_uri uri - | Ast.NRefPattern nref -> NReference.string_of_reference nref - | Ast.VarPattern name -> name - | Ast.ImplicitPattern -> "?" - | Ast.ApplPattern aps -> - sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps)) - diff --git a/matita/components/content/cicNotationPp.mli b/matita/components/content/cicNotationPp.mli deleted file mode 100644 index d883ddfc6..000000000 --- a/matita/components/content/cicNotationPp.mli +++ /dev/null @@ -1,55 +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/ - *) - -(** ZACK - * This module does not print terms and object properly, it has been created - * mainly for debugging reason. There is no guarantee that printed strings are - * re-parsable. Moreover, actually there is no way at all to proper print - * objects in a way that is re-parsable. - * - * 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 - * and parametrize it over a function with the following type - * pp_term: CicNotationPt.term -> CicNotationPres.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_env: CicNotationEnv.t -> string -val pp_value: CicNotationEnv.value -> string -val pp_value_type: CicNotationEnv.value_type -> string - -val pp_pos: CicNotationPt.child_pos -> string -val pp_attribute: CicNotationPt.term_attribute -> string - -val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string - - (** non re-entrant change of pp_term function above *) -val set_pp_term: (CicNotationPt.term -> string) -> unit - diff --git a/matita/components/content/cicNotationPt.ml b/matita/components/content/cicNotationPt.ml deleted file mode 100644 index 731a2ba74..000000000 --- a/matita/components/content/cicNotationPt.ml +++ /dev/null @@ -1,199 +0,0 @@ -(* Copyright (C) 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/ - *) - -(* $Id$ *) - -(** CIC Notation Parse Tree *) - -type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] -type induction_kind = [ `Inductive | `CoInductive ] -type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of -CicUniv.universe | `NType of string |`NCProp of string] -type fold_kind = [ `Left | `Right ] - -type location = Stdpp.location -let fail floc msg = - let (x, y) = HExtlib.loc_of_floc floc in - failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) - -type href = UriManager.uri - -type child_pos = [ `Left | `Right | `Inner ] - -type term_attribute = - [ `Loc of location (* source file location *) - | `IdRef of string (* ACic pointer *) - | `Level of int - | `XmlAttrs of (string option * string * string) list - (* list of XML attributes: namespace, name, value *) - | `Raw of string (* unparsed version *) - ] - -type literal = - [ `Symbol of string - | `Keyword of string - | `Number of string - ] - -type case_indtype = string * href option - -type 'term capture_variable = 'term * 'term option - -(** To be increased each time the term type below changes, used for "safe" - * marshalling *) -let magic = 6 - -type term = - (* CIC AST *) - - | AttributedTerm of term_attribute * term - - | Appl of term list - | Binder of binder_kind * term capture_variable * term (* kind, name, body *) - | Case of term * case_indtype option * term option * - (case_pattern * term) list - (* what to match, inductive type, out type, list *) - | Cast of term * term - | LetIn of term capture_variable * term * term (* name, body, where *) - | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term - (* (params, name, body, decreasing arg) list, where *) - | Ident of string * subst list option - (* literal, substitutions. - * Some [] -> user has given an empty explicit substitution list - * None -> user has given no explicit substitution list *) - | Implicit of [`Vector | `JustOne | `Tagged of string] - | Meta of int * meta_subst list - | Num of string * int (* literal, instance *) - | Sort of sort_kind - | Symbol of string * int (* canonical name, instance *) - - | UserInput (* place holder for user input, used by MatitaConsole, not to be - used elsewhere *) - | Uri of string * subst list option (* as Ident, for long names *) - | NRef of NReference.reference - - | NCic of NCic.term - - (* Syntax pattern extensions *) - - | Literal of literal - | Layout of layout_pattern - - | Magic of magic_term - | Variable of pattern_variable - - (* name, type. First component must be Ident or Variable (FreshVar _) *) - -and meta_subst = term option -and subst = string * term -and case_pattern = - Pattern of string * href option * term capture_variable list - | Wildcard - -and box_kind = H | V | HV | HOV -and box_spec = box_kind * bool * bool (* kind, spacing, indent *) - -and layout_pattern = - | Sub of term * term - | Sup of term * term - | Below of term * term - | Above of term * term - | Frac of term * term - | Over of term * term - | Atop of term * term - | InfRule of term * term * term -(* | array of term * literal option * literal option - |+ column separator, row separator +| *) - | Maction of term list - | Sqrt of term - | Root of term * term (* argument, index *) - | Break - | Box of box_spec * term list - | Group of term list - | Mstyle of (string * string) list * term list - | Mpadded of (string * string) list * term list - -and magic_term = - (* level 1 magics *) - | List0 of term * literal option (* pattern, separator *) - | List1 of term * literal option (* pattern, separator *) - | Opt of term - - (* level 2 magics *) - | Fold of fold_kind * term * string list * term - (* base case pattern, recursive case bound names, recursive case pattern *) - | Default of term * term (* "some" case pattern, "none" case pattern *) - | Fail - | If of term * term * term (* test, pattern if true, pattern if false *) - -and term_level = Self of int | Level of int - -and pattern_variable = - (* level 1 and 2 variables *) - | NumVar of string - | IdentVar of string - | TermVar of string * term_level - - (* level 1 variables *) - | Ascription of term * string - - (* level 2 variables *) - | FreshVar of string - -type argument_pattern = - | IdentArg of int * string (* eta-depth, name *) - -type cic_appl_pattern = - | UriPattern of UriManager.uri - | NRefPattern of NReference.reference - | VarPattern of string - | ImplicitPattern - | ApplPattern of cic_appl_pattern list - - (** - * true means inductive, false coinductive *) -type 'term inductive_type = string * bool * 'term * (string * 'term) list - -type 'term obj = - | Inductive of 'term capture_variable list * 'term inductive_type list - (** parameters, list of loc * mutual inductive types *) - | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma - (** flavour, name, type, body - * - name is absent when an unnamed theorem is being proved, tipically in - * interactive usage - * - body is present when its given along with the command, otherwise it - * will be given in proof editing mode using the tactical language, - * unless the flavour is an Axiom - *) - | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list - (** left parameters, name, type, fields *) - -(** {2 Standard precedences} *) - -let let_in_prec = 10 -let binder_prec = 20 -let apply_prec = 70 -let simple_prec = 90 - diff --git a/matita/components/content/cicNotationUtil.ml b/matita/components/content/cicNotationUtil.ml deleted file mode 100644 index 7eccd7901..000000000 --- a/matita/components/content/cicNotationUtil.ml +++ /dev/null @@ -1,420 +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/ - *) - -(* $Id$ *) - -module Ast = CicNotationPt - -let visit_ast ?(special_k = fun _ -> assert false) - ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x) - ?(map_case_outtype= - fun k x -> match x with None -> None | Some x -> Some (k x)) - k -= - let rec aux = function - | Ast.Appl terms -> Ast.Appl (List.map k terms) - | Ast.Binder (kind, var, body) -> - Ast.Binder (kind, aux_capture_variable var, k body) - | Ast.Case (term, indtype, typ, patterns) -> - Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ, - aux_patterns map_xref_option patterns) - | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2) - | Ast.LetIn (var, t1, t3) -> - Ast.LetIn (aux_capture_variable var, k t1, k t3) - | Ast.LetRec (kind, definitions, term) -> - let definitions = - List.map - (fun (params, var, ty, decrno) -> - List.map aux_capture_variable params, aux_capture_variable var, - k ty, decrno) - definitions - in - Ast.LetRec (kind, definitions, k term) - | Ast.Ident (name, Some substs) -> - Ast.Ident (name, Some (aux_substs substs)) - | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs)) - | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs) - | (Ast.AttributedTerm _ - | Ast.Layout _ - | Ast.Literal _ - | Ast.Magic _ - | Ast.Variable _) as t -> special_k t - | (Ast.Ident _ - | Ast.NRef _ - | Ast.NCic _ - | Ast.Implicit _ - | Ast.Num _ - | Ast.Sort _ - | Ast.Symbol _ - | Ast.Uri _ - | Ast.UserInput) as t -> t - and aux_opt = function - | None -> None - | Some term -> Some (k term) - and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt - and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns - and aux_pattern k_xref = - function - Ast.Pattern (head, hrefs, vars), term -> - Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term - | Ast.Wildcard, term -> Ast.Wildcard, k term - and aux_subst (name, term) = (name, k term) - and aux_substs substs = List.map aux_subst substs - in - aux - -let visit_layout k = function - | Ast.Sub (t1, t2) -> Ast.Sub (k t1, k t2) - | Ast.Sup (t1, t2) -> Ast.Sup (k t1, k t2) - | Ast.Below (t1, t2) -> Ast.Below (k t1, k t2) - | Ast.Above (t1, t2) -> Ast.Above (k t1, k t2) - | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2) - | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2) - | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2) - | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3) - | Ast.Sqrt t -> Ast.Sqrt (k t) - | Ast.Root (arg, index) -> Ast.Root (k arg, k index) - | Ast.Break -> Ast.Break - | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms) - | Ast.Group terms -> Ast.Group (List.map k terms) - | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term) - | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term) - | Ast.Maction terms -> Ast.Maction (List.map k terms) - -let visit_magic k = function - | Ast.List0 (t, l) -> Ast.List0 (k t, l) - | Ast.List1 (t, l) -> Ast.List1 (k t, l) - | Ast.Opt t -> Ast.Opt (k t) - | Ast.Fold (kind, t1, names, t2) -> Ast.Fold (kind, k t1, names, k t2) - | Ast.Default (t1, t2) -> Ast.Default (k t1, k t2) - | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3) - | Ast.Fail -> Ast.Fail - -let visit_variable k = function - | Ast.NumVar _ - | Ast.IdentVar _ - | Ast.TermVar _ - | Ast.FreshVar _ as t -> t - | Ast.Ascription (t, s) -> Ast.Ascription (k t, s) - -let variables_of_term t = - let rec vars = ref [] in - let add_variable v = - if List.mem v !vars then () - else vars := v :: !vars - in - let rec aux = function - | Ast.Magic m -> Ast.Magic (visit_magic aux m) - | Ast.Layout l -> Ast.Layout (visit_layout aux l) - | Ast.Variable v -> Ast.Variable (aux_variable v) - | Ast.Literal _ as t -> t - | Ast.AttributedTerm (_, t) -> aux t - | t -> visit_ast aux t - and aux_variable = function - | (Ast.NumVar _ - | Ast.IdentVar _ - | Ast.TermVar _) as t -> - add_variable t ; - t - | Ast.FreshVar _ as t -> t - | Ast.Ascription _ -> assert false - in - ignore (aux t) ; - !vars - -let names_of_term t = - let aux = function - | Ast.NumVar s - | Ast.IdentVar s - | Ast.TermVar (s,_) -> s - | _ -> assert false - in - List.map aux (variables_of_term t) - -let keywords_of_term t = - let rec keywords = ref [] in - let add_keyword k = keywords := k :: !keywords in - let rec aux = function - | Ast.AttributedTerm (_, t) -> aux t - | Ast.Layout l -> Ast.Layout (visit_layout aux l) - | Ast.Literal (`Keyword k) as t -> - add_keyword k; - t - | Ast.Literal _ as t -> t - | Ast.Magic m -> Ast.Magic (visit_magic aux m) - | Ast.Variable _ as v -> v - | t -> visit_ast aux t - in - ignore (aux t) ; - !keywords - -let rec strip_attributes t = - let special_k = function - | Ast.AttributedTerm (_, term) -> strip_attributes term - | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m) - | Ast.Variable _ as t -> t - | t -> assert false - in - visit_ast ~special_k strip_attributes t - -let rec get_idrefs = - function - | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t - | Ast.AttributedTerm (_, t) -> get_idrefs t - | _ -> [] - -let meta_names_of_term term = - let rec names = ref [] in - let add_name n = - if List.mem n !names then () - else names := n :: !names - in - let rec aux = function - | Ast.AttributedTerm (_, term) -> aux term - | Ast.Appl terms -> List.iter aux terms - | Ast.Binder (_, _, body) -> aux body - | Ast.Case (term, indty, outty_opt, patterns) -> - aux term ; - aux_opt outty_opt ; - List.iter aux_branch patterns - | Ast.LetIn (_, t1, t3) -> - aux t1 ; - aux t3 - | Ast.LetRec (_, definitions, body) -> - List.iter aux_definition definitions ; - aux body - | Ast.Uri (_, Some substs) -> aux_substs substs - | Ast.Ident (_, Some substs) -> aux_substs substs - | Ast.Meta (_, substs) -> aux_meta_substs substs - - | Ast.Implicit _ - | Ast.Ident _ - | Ast.Num _ - | Ast.Sort _ - | Ast.Symbol _ - | Ast.Uri _ - | Ast.UserInput -> () - - | Ast.Magic magic -> aux_magic magic - | Ast.Variable var -> aux_variable var - - | _ -> assert false - and aux_opt = function - | Some term -> aux term - | None -> () - and aux_capture_var (_, ty_opt) = aux_opt ty_opt - and aux_branch (pattern, term) = - aux_pattern pattern ; - aux term - and aux_pattern = - function - Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars - | Ast.Wildcard -> () - and aux_definition (params, var, term, decrno) = - List.iter aux_capture_var params ; - aux_capture_var var ; - aux term - and aux_substs substs = List.iter (fun (_, term) -> aux term) substs - and aux_meta_substs meta_substs = List.iter aux_opt meta_substs - and aux_variable = function - | Ast.NumVar name -> add_name name - | Ast.IdentVar name -> add_name name - | Ast.TermVar (name,_) -> add_name name - | Ast.FreshVar _ -> () - | Ast.Ascription _ -> assert false - and aux_magic = function - | Ast.Default (t1, t2) - | Ast.Fold (_, t1, _, t2) -> - aux t1 ; - aux t2 - | Ast.If (t1, t2, t3) -> - aux t1 ; - aux t2 ; - aux t3 - | Ast.Fail -> () - | _ -> assert false - in - aux term ; - !names - -let rectangular matrix = - let columns = Array.length matrix.(0) in - try - Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix; - true - with Exit -> false - -let ncombine ll = - let matrix = Array.of_list (List.map Array.of_list ll) in - assert (rectangular matrix); - let rows = Array.length matrix in - let columns = Array.length matrix.(0) in - let lists = ref [] in - for j = 0 to columns - 1 do - let l = ref [] in - for i = 0 to rows - 1 do - l := matrix.(i).(j) :: !l - done; - lists := List.rev !l :: !lists - done; - List.rev !lists - -let string_of_literal = function - | `Symbol s - | `Keyword s - | `Number s -> s - -let boxify = function - | [ a ] -> a - | l -> Ast.Layout (Ast.Box ((Ast.H, false, false), l)) - -let unboxify = function - | Ast.Layout (Ast.Box ((Ast.H, false, false), [ a ])) -> a - | l -> l - -let group = function - | [ a ] -> a - | l -> Ast.Layout (Ast.Group l) - -let ungroup = - let rec aux acc = - function - [] -> List.rev acc - | Ast.Layout (Ast.Group terms) :: terms' -> aux acc (terms @ terms') - | term :: terms -> aux (term :: acc) terms - in - aux [] - -let dress ~sep:sauce = - let rec aux = - function - | [] -> [] - | [hd] -> [hd] - | hd :: tl -> hd :: sauce :: aux tl - in - aux - -let dressn ~sep:sauces = - let rec aux = - function - | [] -> [] - | [hd] -> [hd] - | hd :: tl -> hd :: sauces @ aux tl - in - aux - -let find_appl_pattern_uris ap = - let rec aux acc = - function - | Ast.UriPattern uri -> `Uri uri :: acc - | Ast.NRefPattern nref -> `NRef nref :: acc - | Ast.ImplicitPattern - | Ast.VarPattern _ -> acc - | Ast.ApplPattern apl -> List.fold_left aux acc apl - in - let uris = aux [] ap in - let cmp u1 u2 = - match u1,u2 with - `Uri u1, `Uri u2 -> UriManager.compare u1 u2 - | `NRef r1, `NRef r2 -> NReference.compare r1 r2 - | `Uri _,`NRef _ -> -1 - | `NRef _, `Uri _ -> 1 - in - HExtlib.list_uniq (List.fast_sort cmp uris) - -let rec find_branch = - function - Ast.Magic (Ast.If (_, Ast.Magic Ast.Fail, t)) -> find_branch t - | Ast.Magic (Ast.If (_, t, _)) -> find_branch t - | t -> t - -let cic_name_of_name = function - | Ast.Ident ("_", None) -> Cic.Anonymous - | Ast.Ident (name, None) -> Cic.Name name - | _ -> assert false - -let name_of_cic_name = -(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *) - (* ZACK why we used to generate dummy xrefs? *) - let add_dummy_xref t = t in - function - | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None)) - | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None)) - -let fresh_index = ref ~-1 - -type notation_id = int - -let fresh_id () = - incr fresh_index; - !fresh_index - - (* TODO ensure that names generated by fresh_var do not clash with user's *) - (* FG: "η" is not an identifier (it is rendered, but not be parsed) *) -let fresh_name () = "eta" ^ string_of_int (fresh_id ()) - -let rec freshen_term ?(index = ref 0) term = - let freshen_term = freshen_term ~index in - let fresh_instance () = incr index; !index in - let special_k = function - | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, freshen_term t) - | Ast.Layout l -> Ast.Layout (visit_layout freshen_term l) - | Ast.Magic m -> Ast.Magic (visit_magic freshen_term m) - | Ast.Variable v -> Ast.Variable (visit_variable freshen_term v) - | Ast.Literal _ as t -> t - | _ -> assert false - in - match term with - | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ()) - | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ()) - | t -> visit_ast ~special_k freshen_term t - -let freshen_obj obj = - let index = ref 0 in - let freshen_term = freshen_term ~index in - let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in - let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in - let freshen_capture_variables = - List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t)) - in - match obj with - | CicNotationPt.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) -> - 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, - freshen_term ty, freshen_name_ty_b fields) - -let freshen_term = freshen_term ?index:None - 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/notationEnv.ml b/matita/components/content/notationEnv.ml new file mode 100644 index 000000000..e95b3ab51 --- /dev/null +++ b/matita/components/content/notationEnv.ml @@ -0,0 +1,153 @@ +(* 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/ + *) + +(* $Id$ *) + +module Ast = NotationPt + +type value = + | TermValue of Ast.term + | StringValue of string + | NumValue of string + | OptValue of value option + | ListValue of value list + +type value_type = + | TermType of int + | StringType + | NumType + | OptType of value_type + | ListType of value_type + +exception Value_not_found of string +exception Type_mismatch of string * value_type + +type declaration = string * value_type +type binding = string * (value_type * value) +type t = binding list + +let lookup env name = + try + List.assoc name env + with Not_found -> raise (Value_not_found name) + +let lookup_value env name = + try + snd (List.assoc name env) + with Not_found -> raise (Value_not_found name) + +let remove_name env name = List.remove_assoc name env + +let remove_names env names = + List.filter (fun name, _ -> not (List.mem name names)) env + +let lookup_term env name = + match lookup env name with + | _, TermValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let lookup_num env name = + match lookup env name with + | _, NumValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let lookup_string env name = + match lookup env name with + | _, StringValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let lookup_opt env name = + match lookup env name with + | _, OptValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let lookup_list env name = + match lookup env name with + | _, ListValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) +let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) +let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None)) +let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) +let opt_declaration (n, ty) = (n, OptType ty) +let list_declaration (n, ty) = (n, ListType ty) + +let declaration_of_var = function + | Ast.NumVar s -> s, NumType + | Ast.IdentVar s -> s, StringType + | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l + | _ -> assert false + +let value_of_term = function + | Ast.Num (s, _) -> NumValue s + | Ast.Ident (s, None) -> StringValue s + | t -> TermValue t + +let term_of_value = function + | NumValue s -> Ast.Num (s, 0) + | StringValue s -> Ast.Ident (s, None) + | TermValue t -> t + | _ -> assert false (* TO BE UNDERSTOOD *) + +let rec well_typed ty value = + match ty, value with + | TermType _, TermValue _ + | StringType, StringValue _ + | OptType _, OptValue None + | NumType, NumValue _ -> true + | OptType ty', OptValue (Some value') -> well_typed ty' value' + | ListType ty', ListValue vl -> + List.for_all (fun value' -> well_typed ty' value') vl + | _ -> false + +let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty)) +let declarations_of_term p = + List.map declaration_of_var (NotationUtil.variables_of_term p) + +let rec combine decls values = + match decls, values with + | [], [] -> [] + | (name, ty) :: decls, v :: values -> + (name, (ty, v)) :: (combine decls values) + | _ -> assert false + +let coalesce_env declarations env_list = + let env0 = List.map list_binding_of_name declarations in + let grow_env_entry env n v = + List.map + (function + | (n', (ty, ListValue vl)) as entry -> + if n' = n then n', (ty, ListValue (v :: vl)) else entry + | _ -> assert false) + env + in + let grow_env env_i env = + List.fold_left + (fun env (n, (_, v)) -> grow_env_entry env n v) + env env_i + in + List.fold_right grow_env env_list env0 + diff --git a/matita/components/content/notationEnv.mli b/matita/components/content/notationEnv.mli new file mode 100644 index 000000000..858af233c --- /dev/null +++ b/matita/components/content/notationEnv.mli @@ -0,0 +1,92 @@ +(* 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/ + *) + +(** {2 Types} *) + +type value = + | TermValue of NotationPt.term + | StringValue of string + | NumValue of string + | OptValue of value option + | ListValue of value list + +type value_type = + | TermType of int (* the level of the expected term *) + | StringType + | NumType + | OptType of value_type + | ListType of value_type + + (** looked up value not found in environment *) +exception Value_not_found of string + + (** looked up value has the wrong type + * parameters are value name and value type in environment *) +exception Type_mismatch of string * value_type + +type declaration = string * value_type +type binding = string * (value_type * value) +type t = binding list + +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: NotationPt.term -> declaration list +val combine: declaration list -> value list -> t (** @raise Invalid_argument *) + +(** {2 Environment lookup} *) + +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 -> NotationPt.term +val lookup_string: t -> string -> string +val lookup_num: t -> string -> string +val lookup_opt: t -> string -> value option +val lookup_list: t -> string -> value list + +val remove_name: t -> string -> t +val remove_names: t -> string list -> t + +(** {2 Bindings mangling} *) + +val opt_binding_some: binding -> binding (* v -> Some v *) +val opt_binding_none: binding -> binding (* v -> None *) + +val opt_binding_of_name: declaration -> binding (* None binding *) +val list_binding_of_name: declaration -> binding (* [] binding *) + +val opt_declaration: declaration -> declaration (* t -> OptType t *) +val list_declaration: declaration -> declaration (* t -> ListType t *) + +(** given a list of environments bindings a set of names n_1, ..., n_k, returns + * a single environment where n_i is bound to the list of values bound in the + * starting environments *) +val coalesce_env: declaration list -> t list -> t + diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml new file mode 100644 index 000000000..a101747df --- /dev/null +++ b/matita/components/content/notationPp.ml @@ -0,0 +1,371 @@ +(* 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/ + *) + +(* $Id$ *) + +open Printf + +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. + * set to false if you need, for example, cut and paste from matitac output to + * matitatop *) +let debug_printing = false + +let pp_binder = function + | `Lambda -> "lambda" + | `Pi -> "Pi" + | `Exists -> "exists" + | `Forall -> "forall" + +let pp_literal = + if debug_printing then + (function (* debugging version *) + | `Symbol s -> sprintf "symbol(%s)" s + | `Keyword s -> sprintf "keyword(%s)" s + | `Number s -> sprintf "number(%s)" s) + else + (function + | `Symbol s + | `Keyword s + | `Number s -> s) + +let pp_pos = + function +(* `None -> "`None" *) + | `Left -> "`Left" + | `Right -> "`Right" + | `Inner -> "`Inner" + +let pp_attribute = + function + | `IdRef id -> sprintf "x(%s)" id + | `XmlAttrs attrs -> + sprintf "X(%s)" + (String.concat ";" + (List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs)) + | `Level (prec) -> sprintf "L(%d)" prec + | `Raw _ -> "R" + | `Loc _ -> "@" + | `ChildPos p -> sprintf "P(%s)" (pp_pos p) + +let pp_capture_variable pp_term = + function + | term, None -> pp_term (* ~pp_parens:false *) term + | term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")" + +let rec pp_term ?(pp_parens = true) t = + let t_pp = + match t with + | Ast.AttributedTerm (attr, term) when debug_printing -> + sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term) + | Ast.AttributedTerm (`Raw text, _) -> text + | Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term + | Ast.Appl terms -> + sprintf "%s" (String.concat " " (List.map pp_term terms)) + | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) -> + sprintf "%s \\to %s" + (match typ with None -> "?" | Some typ -> pp_term typ) + (pp_term ~pp_parens:true body) + | Ast.Binder (kind, var, body) -> + sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var) + (pp_term ~pp_parens:true body) + | Ast.Case (term, indtype, typ, patterns) -> + sprintf "match %s%s%s with %s" + (pp_term term) + (match indtype with + | None -> "" + | Some (ty, href_opt) -> + sprintf " in %s%s" ty + (match debug_printing, href_opt with + | true, Some uri -> + sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "")) + (match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t)) + (pp_patterns patterns) + | Ast.Cast (t1, t2) -> sprintf "(%s: %s)" (pp_term ~pp_parens:true t1) (pp_term ~pp_parens:true t2) + | Ast.LetIn ((var,t2), t1, t3) -> +(* let t2 = match t2 with None -> Ast.Implicit | Some t -> t in *) + sprintf "let %s \\def %s in %s" (pp_term var) +(* (pp_term ~pp_parens:true t2) *) + (pp_term ~pp_parens:true t1) + (pp_term ~pp_parens:true t3) + | Ast.LetRec (kind, definitions, term) -> + let rec get_guard i = function + | [] -> (*assert false*) Ast.Implicit `JustOne + | [term, _] when i = 1 -> term + | _ :: tl -> get_guard (pred i) tl + in + let map (params, (id,typ), body, i) = + let typ = + match typ with + None -> Ast.Implicit `JustOne + | Some typ -> typ + in + sprintf "%s %s on %s: %s \\def %s" + (pp_term ~pp_parens:false term) + (String.concat " " (List.map (pp_capture_variable pp_term) params)) + (pp_term ~pp_parens:false (get_guard i params)) + (pp_term typ) (pp_term body) + in + sprintf "let %s %s in %s" + (match kind with `Inductive -> "rec" | `CoInductive -> "corec") + (String.concat " and " (List.map map definitions)) + (pp_term term) + | Ast.Ident (name, Some []) | Ast.Ident (name, None) + | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name + | Ast.NRef nref -> NReference.string_of_reference nref + | Ast.NCic cic -> NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[] cic + | Ast.Ident (name, Some substs) + | Ast.Uri (name, Some substs) -> + sprintf "%s \\subst [%s]" name (pp_substs substs) + | Ast.Implicit `Vector -> "…" + | Ast.Implicit `JustOne -> "?" + | Ast.Implicit (`Tagged name) -> "?"^name + | Ast.Meta (index, substs) -> + sprintf "%d[%s]" index + (String.concat "; " + (List.map (function None -> "?" | Some t -> pp_term t) substs)) + | Ast.Num (num, _) -> num + | Ast.Sort `Set -> "Set" + | Ast.Sort `Prop -> "Prop" + | Ast.Sort (`Type _) -> "Type" + | Ast.Sort (`CProp _)-> "CProp" + | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]" + | Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]" + | Ast.Symbol (name, _) -> "'" ^ name + + | Ast.UserInput -> "%" + + | Ast.Literal l -> pp_literal l + | Ast.Layout l -> pp_layout l + | Ast.Magic m -> pp_magic m + | Ast.Variable v -> pp_variable v + in + match pp_parens, t with + | false, _ + | true, Ast.Implicit _ + | true, Ast.UserInput + | true, Ast.Sort _ + | true, Ast.Ident (_, Some []) + | true, Ast.Ident (_, None) -> t_pp + | _ -> sprintf "(%s)" t_pp + +and pp_subst (name, term) = sprintf "%s \\Assign %s" name (pp_term term) +and pp_substs substs = String.concat "; " (List.map pp_subst substs) + +and pp_pattern = + function + Ast.Pattern (head, href, vars), term -> + let head_pp = + head ^ + (match debug_printing, href with + | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri) + | _ -> "") + in + sprintf "%s \\Rightarrow %s" + (match vars with + | [] -> head_pp + | _ -> + sprintf "(%s %s)" head_pp + (String.concat " " (List.map (pp_capture_variable pp_term) vars))) + (pp_term term) + | Ast.Wildcard, term -> + sprintf "_ \\Rightarrow %s" (pp_term term) + +and pp_patterns patterns = + sprintf "[%s]" (String.concat " | " (List.map pp_pattern patterns)) + +and pp_box_spec (kind, spacing, indent) = + let int_of_bool b = if b then 1 else 0 in + let kind_string = + match kind with + Ast.H -> "H" | Ast.V -> "V" | Ast.HV -> "HV" | Ast.HOV -> "HOV" + in + sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent) + +and pp_layout = function + | Ast.Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2) + | Ast.Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2) + | Ast.Below (t1, t2) -> sprintf "%s \\BELOW %s" (pp_term t1) (pp_term t2) + | Ast.Above (t1, t2) -> sprintf "%s \\ABOVE %s" (pp_term t1) (pp_term t2) + | Ast.Over (t1, t2) -> sprintf "[%s \\OVER %s]" (pp_term t1) (pp_term t2) + | Ast.Atop (t1, t2) -> sprintf "[%s \\ATOP %s]" (pp_term t1) (pp_term t2) + | Ast.Frac (t1, t2) -> sprintf "\\FRAC %s %s" (pp_term t1) (pp_term t2) + | Ast.InfRule (t1, t2, t3) -> sprintf "\\INFRULE %s %s %s" (pp_term t1) + (pp_term t2) (pp_term t3) + | Ast.Maction l -> sprintf "\\MACTION (%s)" + (String.concat "," (List.map pp_term l)) + | Ast.Sqrt t -> sprintf "\\SQRT %s" (pp_term t) + | Ast.Root (arg, index) -> + sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) + | Ast.Break -> "\\BREAK" +(* | Space -> "\\SPACE" *) + | Ast.Box (box_spec, terms) -> + sprintf "\\%s [%s]" (pp_box_spec box_spec) + (String.concat " " (List.map pp_term terms)) + | Ast.Group terms -> + sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms)) + | Ast.Mstyle (l,terms) -> + sprintf "\\MSTYLE %s [%s]" + (String.concat " " (List.map (fun (k,v) -> k^"="^v) l)) + (String.concat " " (List.map pp_term terms)) + | Ast.Mpadded (l,terms) -> + sprintf "\\MSTYLE %s [%s]" + (String.concat " " (List.map (fun (k,v) -> k^"="^v) l)) + (String.concat " " (List.map pp_term terms)) + +and pp_magic = function + | Ast.List0 (t, sep_opt) -> + sprintf "list0 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Ast.List1 (t, sep_opt) -> + sprintf "list1 %s%s" (pp_term t) (pp_sep_opt sep_opt) + | Ast.Opt t -> sprintf "opt %s" (pp_term t) + | Ast.Fold (kind, p_base, names, p_rec) -> + let acc = match names with acc :: _ -> acc | _ -> assert false in + sprintf "fold %s %s rec %s %s" + (pp_fold_kind kind) (pp_term p_base) acc (pp_term p_rec) + | Ast.Default (p_some, p_none) -> + sprintf "default %s %s" (pp_term p_some) (pp_term p_none) + | Ast.If (p_test, p_true, p_false) -> + sprintf "if %s then %s else %s" + (pp_term p_test) (pp_term p_true) (pp_term p_false) + | Ast.Fail -> "fail" + +and pp_fold_kind = function + | `Left -> "left" + | `Right -> "right" + +and pp_sep_opt = function + | None -> "" + | Some sep -> sprintf " sep %s" (pp_literal sep) + +and pp_variable = function + | Ast.NumVar s -> "number " ^ s + | Ast.IdentVar s -> "ident " ^ s + | Ast.TermVar (s,Ast.Self _) -> s + | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l + | Ast.Ascription (t, n) -> assert false + | Ast.FreshVar n -> "fresh " ^ n + +let _pp_term = ref (pp_term ~pp_parens:false) +let pp_term t = !_pp_term t +let set_pp_term f = _pp_term := f + +let pp_params pp_term = function + | [] -> "" + | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params) + +let pp_flavour = function + | `Definition -> "definition" + | `MutualDefinition -> assert false + | `Fact -> "fact" + | `Goal -> "goal" + | `Lemma -> "lemma" + | `Remark -> "remark" + | `Theorem -> "theorem" + | `Variant -> "variant" + | `Axiom -> "axiom" + +let pp_fields pp_term fields = + (if fields <> [] then "\n" else "") ^ + String.concat ";\n" + (List.map + (fun (name,ty,coercion,arity) -> + " " ^ name ^ + (if coercion then + (":" ^ (if arity > 0 then string_of_int arity else "") ^ "> ") + else ": ") ^ + pp_term ty) + fields) + +let pp_obj pp_term = function + | Ast.Inductive (params, types) -> + let pp_constructors constructors = + String.concat "\n" + (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ)) + constructors) + in + let pp_type (name, _, typ, constructors) = + sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ) + (pp_constructors constructors) + in + (match types with + | [] -> assert false + | (name, inductive, typ, constructors) :: tl -> + let fst_typ_pp = + sprintf "%sinductive %s%s: %s \\def\n%s" + (if inductive then "" else "co") name (pp_params pp_term params) + (pp_term typ) (pp_constructors constructors) + in + fst_typ_pp ^ String.concat "" (List.map pp_type tl)) + | Ast.Theorem (`MutualDefinition, name, typ, body,_) -> + sprintf "<>" + | Ast.Theorem (flavour, name, typ, body,_) -> + sprintf "%s %s:\n %s\n%s" + (pp_flavour flavour) + name + (pp_term typ) + (match body with + | None -> "" + | Some body -> "\\def\n " ^ pp_term body) + | Ast.Record (params,name,ty,fields) -> + "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ + " \\def {" ^ pp_fields pp_term fields ^ "\n}" + +let rec pp_value = function + | Env.TermValue t -> sprintf "$%s$" (pp_term t) + | Env.StringValue s -> sprintf "\"%s\"" s + | Env.NumValue n -> n + | Env.OptValue (Some v) -> "Some " ^ pp_value v + | Env.OptValue None -> "None" + | Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map pp_value l)) + +let rec pp_value_type = + function + | Env.TermType l -> "Term "^string_of_int l + | Env.StringType -> "String" + | Env.NumType -> "Number" + | Env.OptType t -> "Maybe " ^ pp_value_type t + | Env.ListType l -> "List " ^ pp_value_type l + +let pp_env env = + String.concat "; " + (List.map + (fun (name, (ty, value)) -> + sprintf "%s : %s = %s" name (pp_value_type ty) (pp_value value)) + env) + +let rec pp_cic_appl_pattern = function + | Ast.UriPattern uri -> UriManager.string_of_uri uri + | Ast.NRefPattern nref -> NReference.string_of_reference nref + | Ast.VarPattern name -> name + | Ast.ImplicitPattern -> "?" + | Ast.ApplPattern aps -> + sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps)) + diff --git a/matita/components/content/notationPp.mli b/matita/components/content/notationPp.mli new file mode 100644 index 000000000..51a284e2e --- /dev/null +++ b/matita/components/content/notationPp.mli @@ -0,0 +1,55 @@ +(* 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/ + *) + +(** ZACK + * This module does not print terms and object properly, it has been created + * mainly for debugging reason. There is no guarantee that printed strings are + * re-parsable. Moreover, actually there is no way at all to proper print + * objects in a way that is re-parsable. + * + * TODO the proper implementation of a pp_obj function like the one below should + * be as follows. Change its type to + * pp_obj: NotationPt.obj -> NotationPres.markup + * and parametrize it over a function with the following type + * 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: NotationPt.term -> string +val pp_obj: ('term -> string) -> 'term NotationPt.obj -> string + +val pp_env: NotationEnv.t -> string +val pp_value: NotationEnv.value -> string +val pp_value_type: NotationEnv.value_type -> string + +val pp_pos: NotationPt.child_pos -> string +val pp_attribute: NotationPt.term_attribute -> string + +val pp_cic_appl_pattern: NotationPt.cic_appl_pattern -> string + + (** non re-entrant change of pp_term function above *) +val set_pp_term: (NotationPt.term -> string) -> unit + diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml new file mode 100644 index 000000000..731a2ba74 --- /dev/null +++ b/matita/components/content/notationPt.ml @@ -0,0 +1,199 @@ +(* Copyright (C) 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/ + *) + +(* $Id$ *) + +(** CIC Notation Parse Tree *) + +type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ] +type induction_kind = [ `Inductive | `CoInductive ] +type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of +CicUniv.universe | `NType of string |`NCProp of string] +type fold_kind = [ `Left | `Right ] + +type location = Stdpp.location +let fail floc msg = + let (x, y) = HExtlib.loc_of_floc floc in + failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg) + +type href = UriManager.uri + +type child_pos = [ `Left | `Right | `Inner ] + +type term_attribute = + [ `Loc of location (* source file location *) + | `IdRef of string (* ACic pointer *) + | `Level of int + | `XmlAttrs of (string option * string * string) list + (* list of XML attributes: namespace, name, value *) + | `Raw of string (* unparsed version *) + ] + +type literal = + [ `Symbol of string + | `Keyword of string + | `Number of string + ] + +type case_indtype = string * href option + +type 'term capture_variable = 'term * 'term option + +(** To be increased each time the term type below changes, used for "safe" + * marshalling *) +let magic = 6 + +type term = + (* CIC AST *) + + | AttributedTerm of term_attribute * term + + | Appl of term list + | Binder of binder_kind * term capture_variable * term (* kind, name, body *) + | Case of term * case_indtype option * term option * + (case_pattern * term) list + (* what to match, inductive type, out type, list *) + | Cast of term * term + | LetIn of term capture_variable * term * term (* name, body, where *) + | LetRec of induction_kind * (term capture_variable list * term capture_variable * term * int) list * term + (* (params, name, body, decreasing arg) list, where *) + | Ident of string * subst list option + (* literal, substitutions. + * Some [] -> user has given an empty explicit substitution list + * None -> user has given no explicit substitution list *) + | Implicit of [`Vector | `JustOne | `Tagged of string] + | Meta of int * meta_subst list + | Num of string * int (* literal, instance *) + | Sort of sort_kind + | Symbol of string * int (* canonical name, instance *) + + | UserInput (* place holder for user input, used by MatitaConsole, not to be + used elsewhere *) + | Uri of string * subst list option (* as Ident, for long names *) + | NRef of NReference.reference + + | NCic of NCic.term + + (* Syntax pattern extensions *) + + | Literal of literal + | Layout of layout_pattern + + | Magic of magic_term + | Variable of pattern_variable + + (* name, type. First component must be Ident or Variable (FreshVar _) *) + +and meta_subst = term option +and subst = string * term +and case_pattern = + Pattern of string * href option * term capture_variable list + | Wildcard + +and box_kind = H | V | HV | HOV +and box_spec = box_kind * bool * bool (* kind, spacing, indent *) + +and layout_pattern = + | Sub of term * term + | Sup of term * term + | Below of term * term + | Above of term * term + | Frac of term * term + | Over of term * term + | Atop of term * term + | InfRule of term * term * term +(* | array of term * literal option * literal option + |+ column separator, row separator +| *) + | Maction of term list + | Sqrt of term + | Root of term * term (* argument, index *) + | Break + | Box of box_spec * term list + | Group of term list + | Mstyle of (string * string) list * term list + | Mpadded of (string * string) list * term list + +and magic_term = + (* level 1 magics *) + | List0 of term * literal option (* pattern, separator *) + | List1 of term * literal option (* pattern, separator *) + | Opt of term + + (* level 2 magics *) + | Fold of fold_kind * term * string list * term + (* base case pattern, recursive case bound names, recursive case pattern *) + | Default of term * term (* "some" case pattern, "none" case pattern *) + | Fail + | If of term * term * term (* test, pattern if true, pattern if false *) + +and term_level = Self of int | Level of int + +and pattern_variable = + (* level 1 and 2 variables *) + | NumVar of string + | IdentVar of string + | TermVar of string * term_level + + (* level 1 variables *) + | Ascription of term * string + + (* level 2 variables *) + | FreshVar of string + +type argument_pattern = + | IdentArg of int * string (* eta-depth, name *) + +type cic_appl_pattern = + | UriPattern of UriManager.uri + | NRefPattern of NReference.reference + | VarPattern of string + | ImplicitPattern + | ApplPattern of cic_appl_pattern list + + (** + * true means inductive, false coinductive *) +type 'term inductive_type = string * bool * 'term * (string * 'term) list + +type 'term obj = + | Inductive of 'term capture_variable list * 'term inductive_type list + (** parameters, list of loc * mutual inductive types *) + | Theorem of Cic.object_flavour * string * 'term * 'term option * NCic.def_pragma + (** flavour, name, type, body + * - name is absent when an unnamed theorem is being proved, tipically in + * interactive usage + * - body is present when its given along with the command, otherwise it + * will be given in proof editing mode using the tactical language, + * unless the flavour is an Axiom + *) + | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list + (** left parameters, name, type, fields *) + +(** {2 Standard precedences} *) + +let let_in_prec = 10 +let binder_prec = 20 +let apply_prec = 70 +let simple_prec = 90 + diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml new file mode 100644 index 000000000..9b663dfc6 --- /dev/null +++ b/matita/components/content/notationUtil.ml @@ -0,0 +1,420 @@ +(* 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/ + *) + +(* $Id$ *) + +module Ast = NotationPt + +let visit_ast ?(special_k = fun _ -> assert false) + ?(map_xref_option= fun x -> x) ?(map_case_indty= fun x -> x) + ?(map_case_outtype= + fun k x -> match x with None -> None | Some x -> Some (k x)) + k += + let rec aux = function + | Ast.Appl terms -> Ast.Appl (List.map k terms) + | Ast.Binder (kind, var, body) -> + Ast.Binder (kind, aux_capture_variable var, k body) + | Ast.Case (term, indtype, typ, patterns) -> + Ast.Case (k term, map_case_indty indtype, map_case_outtype k typ, + aux_patterns map_xref_option patterns) + | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2) + | Ast.LetIn (var, t1, t3) -> + Ast.LetIn (aux_capture_variable var, k t1, k t3) + | Ast.LetRec (kind, definitions, term) -> + let definitions = + List.map + (fun (params, var, ty, decrno) -> + List.map aux_capture_variable params, aux_capture_variable var, + k ty, decrno) + definitions + in + Ast.LetRec (kind, definitions, k term) + | Ast.Ident (name, Some substs) -> + Ast.Ident (name, Some (aux_substs substs)) + | Ast.Uri (name, Some substs) -> Ast.Uri (name, Some (aux_substs substs)) + | Ast.Meta (index, substs) -> Ast.Meta (index, List.map aux_opt substs) + | (Ast.AttributedTerm _ + | Ast.Layout _ + | Ast.Literal _ + | Ast.Magic _ + | Ast.Variable _) as t -> special_k t + | (Ast.Ident _ + | Ast.NRef _ + | Ast.NCic _ + | Ast.Implicit _ + | Ast.Num _ + | Ast.Sort _ + | Ast.Symbol _ + | Ast.Uri _ + | Ast.UserInput) as t -> t + and aux_opt = function + | None -> None + | Some term -> Some (k term) + and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt + and aux_patterns k_xref patterns = List.map (aux_pattern k_xref) patterns + and aux_pattern k_xref = + function + Ast.Pattern (head, hrefs, vars), term -> + Ast.Pattern (head, k_xref hrefs, List.map aux_capture_variable vars), k term + | Ast.Wildcard, term -> Ast.Wildcard, k term + and aux_subst (name, term) = (name, k term) + and aux_substs substs = List.map aux_subst substs + in + aux + +let visit_layout k = function + | Ast.Sub (t1, t2) -> Ast.Sub (k t1, k t2) + | Ast.Sup (t1, t2) -> Ast.Sup (k t1, k t2) + | Ast.Below (t1, t2) -> Ast.Below (k t1, k t2) + | Ast.Above (t1, t2) -> Ast.Above (k t1, k t2) + | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2) + | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2) + | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2) + | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3) + | Ast.Sqrt t -> Ast.Sqrt (k t) + | Ast.Root (arg, index) -> Ast.Root (k arg, k index) + | Ast.Break -> Ast.Break + | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms) + | Ast.Group terms -> Ast.Group (List.map k terms) + | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term) + | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term) + | Ast.Maction terms -> Ast.Maction (List.map k terms) + +let visit_magic k = function + | Ast.List0 (t, l) -> Ast.List0 (k t, l) + | Ast.List1 (t, l) -> Ast.List1 (k t, l) + | Ast.Opt t -> Ast.Opt (k t) + | Ast.Fold (kind, t1, names, t2) -> Ast.Fold (kind, k t1, names, k t2) + | Ast.Default (t1, t2) -> Ast.Default (k t1, k t2) + | Ast.If (t1, t2, t3) -> Ast.If (k t1, k t2, k t3) + | Ast.Fail -> Ast.Fail + +let visit_variable k = function + | Ast.NumVar _ + | Ast.IdentVar _ + | Ast.TermVar _ + | Ast.FreshVar _ as t -> t + | Ast.Ascription (t, s) -> Ast.Ascription (k t, s) + +let variables_of_term t = + let rec vars = ref [] in + let add_variable v = + if List.mem v !vars then () + else vars := v :: !vars + in + let rec aux = function + | Ast.Magic m -> Ast.Magic (visit_magic aux m) + | Ast.Layout l -> Ast.Layout (visit_layout aux l) + | Ast.Variable v -> Ast.Variable (aux_variable v) + | Ast.Literal _ as t -> t + | Ast.AttributedTerm (_, t) -> aux t + | t -> visit_ast aux t + and aux_variable = function + | (Ast.NumVar _ + | Ast.IdentVar _ + | Ast.TermVar _) as t -> + add_variable t ; + t + | Ast.FreshVar _ as t -> t + | Ast.Ascription _ -> assert false + in + ignore (aux t) ; + !vars + +let names_of_term t = + let aux = function + | Ast.NumVar s + | Ast.IdentVar s + | Ast.TermVar (s,_) -> s + | _ -> assert false + in + List.map aux (variables_of_term t) + +let keywords_of_term t = + let rec keywords = ref [] in + let add_keyword k = keywords := k :: !keywords in + let rec aux = function + | Ast.AttributedTerm (_, t) -> aux t + | Ast.Layout l -> Ast.Layout (visit_layout aux l) + | Ast.Literal (`Keyword k) as t -> + add_keyword k; + t + | Ast.Literal _ as t -> t + | Ast.Magic m -> Ast.Magic (visit_magic aux m) + | Ast.Variable _ as v -> v + | t -> visit_ast aux t + in + ignore (aux t) ; + !keywords + +let rec strip_attributes t = + let special_k = function + | Ast.AttributedTerm (_, term) -> strip_attributes term + | Ast.Magic m -> Ast.Magic (visit_magic strip_attributes m) + | Ast.Variable _ as t -> t + | t -> assert false + in + visit_ast ~special_k strip_attributes t + +let rec get_idrefs = + function + | Ast.AttributedTerm (`IdRef id, t) -> id :: get_idrefs t + | Ast.AttributedTerm (_, t) -> get_idrefs t + | _ -> [] + +let meta_names_of_term term = + let rec names = ref [] in + let add_name n = + if List.mem n !names then () + else names := n :: !names + in + let rec aux = function + | Ast.AttributedTerm (_, term) -> aux term + | Ast.Appl terms -> List.iter aux terms + | Ast.Binder (_, _, body) -> aux body + | Ast.Case (term, indty, outty_opt, patterns) -> + aux term ; + aux_opt outty_opt ; + List.iter aux_branch patterns + | Ast.LetIn (_, t1, t3) -> + aux t1 ; + aux t3 + | Ast.LetRec (_, definitions, body) -> + List.iter aux_definition definitions ; + aux body + | Ast.Uri (_, Some substs) -> aux_substs substs + | Ast.Ident (_, Some substs) -> aux_substs substs + | Ast.Meta (_, substs) -> aux_meta_substs substs + + | Ast.Implicit _ + | Ast.Ident _ + | Ast.Num _ + | Ast.Sort _ + | Ast.Symbol _ + | Ast.Uri _ + | Ast.UserInput -> () + + | Ast.Magic magic -> aux_magic magic + | Ast.Variable var -> aux_variable var + + | _ -> assert false + and aux_opt = function + | Some term -> aux term + | None -> () + and aux_capture_var (_, ty_opt) = aux_opt ty_opt + and aux_branch (pattern, term) = + aux_pattern pattern ; + aux term + and aux_pattern = + function + Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars + | Ast.Wildcard -> () + and aux_definition (params, var, term, decrno) = + List.iter aux_capture_var params ; + aux_capture_var var ; + aux term + and aux_substs substs = List.iter (fun (_, term) -> aux term) substs + and aux_meta_substs meta_substs = List.iter aux_opt meta_substs + and aux_variable = function + | Ast.NumVar name -> add_name name + | Ast.IdentVar name -> add_name name + | Ast.TermVar (name,_) -> add_name name + | Ast.FreshVar _ -> () + | Ast.Ascription _ -> assert false + and aux_magic = function + | Ast.Default (t1, t2) + | Ast.Fold (_, t1, _, t2) -> + aux t1 ; + aux t2 + | Ast.If (t1, t2, t3) -> + aux t1 ; + aux t2 ; + aux t3 + | Ast.Fail -> () + | _ -> assert false + in + aux term ; + !names + +let rectangular matrix = + let columns = Array.length matrix.(0) in + try + Array.iter (fun a -> if Array.length a <> columns then raise Exit) matrix; + true + with Exit -> false + +let ncombine ll = + let matrix = Array.of_list (List.map Array.of_list ll) in + assert (rectangular matrix); + let rows = Array.length matrix in + let columns = Array.length matrix.(0) in + let lists = ref [] in + for j = 0 to columns - 1 do + let l = ref [] in + for i = 0 to rows - 1 do + l := matrix.(i).(j) :: !l + done; + lists := List.rev !l :: !lists + done; + List.rev !lists + +let string_of_literal = function + | `Symbol s + | `Keyword s + | `Number s -> s + +let boxify = function + | [ a ] -> a + | l -> Ast.Layout (Ast.Box ((Ast.H, false, false), l)) + +let unboxify = function + | Ast.Layout (Ast.Box ((Ast.H, false, false), [ a ])) -> a + | l -> l + +let group = function + | [ a ] -> a + | l -> Ast.Layout (Ast.Group l) + +let ungroup = + let rec aux acc = + function + [] -> List.rev acc + | Ast.Layout (Ast.Group terms) :: terms' -> aux acc (terms @ terms') + | term :: terms -> aux (term :: acc) terms + in + aux [] + +let dress ~sep:sauce = + let rec aux = + function + | [] -> [] + | [hd] -> [hd] + | hd :: tl -> hd :: sauce :: aux tl + in + aux + +let dressn ~sep:sauces = + let rec aux = + function + | [] -> [] + | [hd] -> [hd] + | hd :: tl -> hd :: sauces @ aux tl + in + aux + +let find_appl_pattern_uris ap = + let rec aux acc = + function + | Ast.UriPattern uri -> `Uri uri :: acc + | Ast.NRefPattern nref -> `NRef nref :: acc + | Ast.ImplicitPattern + | Ast.VarPattern _ -> acc + | Ast.ApplPattern apl -> List.fold_left aux acc apl + in + let uris = aux [] ap in + let cmp u1 u2 = + match u1,u2 with + `Uri u1, `Uri u2 -> UriManager.compare u1 u2 + | `NRef r1, `NRef r2 -> NReference.compare r1 r2 + | `Uri _,`NRef _ -> -1 + | `NRef _, `Uri _ -> 1 + in + HExtlib.list_uniq (List.fast_sort cmp uris) + +let rec find_branch = + function + Ast.Magic (Ast.If (_, Ast.Magic Ast.Fail, t)) -> find_branch t + | Ast.Magic (Ast.If (_, t, _)) -> find_branch t + | t -> t + +let cic_name_of_name = function + | Ast.Ident ("_", None) -> Cic.Anonymous + | Ast.Ident (name, None) -> Cic.Name name + | _ -> assert false + +let name_of_cic_name = +(* let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *) + (* ZACK why we used to generate dummy xrefs? *) + let add_dummy_xref t = t in + function + | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None)) + | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None)) + +let fresh_index = ref ~-1 + +type notation_id = int + +let fresh_id () = + incr fresh_index; + !fresh_index + + (* TODO ensure that names generated by fresh_var do not clash with user's *) + (* FG: "η" is not an identifier (it is rendered, but not be parsed) *) +let fresh_name () = "eta" ^ string_of_int (fresh_id ()) + +let rec freshen_term ?(index = ref 0) term = + let freshen_term = freshen_term ~index in + let fresh_instance () = incr index; !index in + let special_k = function + | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, freshen_term t) + | Ast.Layout l -> Ast.Layout (visit_layout freshen_term l) + | Ast.Magic m -> Ast.Magic (visit_magic freshen_term m) + | Ast.Variable v -> Ast.Variable (visit_variable freshen_term v) + | Ast.Literal _ as t -> t + | _ -> assert false + in + match term with + | Ast.Symbol (s, instance) -> Ast.Symbol (s, fresh_instance ()) + | Ast.Num (s, instance) -> Ast.Num (s, fresh_instance ()) + | t -> visit_ast ~special_k freshen_term t + +let freshen_obj obj = + let index = ref 0 in + let freshen_term = freshen_term ~index in + let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in + let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in + let freshen_capture_variables = + List.map (fun (n,t) -> (freshen_term n, HExtlib.map_option freshen_term t)) + in + match obj with + | NotationPt.Inductive (params, indtypes) -> + let indtypes = + List.map + (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors)) + indtypes + in + 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 + 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