type checked_l1_pattern = CL1P of NotationPt.term * int
+type binding =
+ | NoBinding
+ | Binding of string * Env.value_type
+ | Env of (string * Env.value_type) list
+
type db = {
grammars:
(int -> NotationPt.term,
(Ast.term Ast.capture_variable list *
Ast.term Ast.capture_variable * Ast.term * int) list,
Ast.term list * Ast.term option) grammars;
- items: (checked_l1_pattern * int * Gramext.g_assoc * NotationPt.term) list
+ keywords: string list;
+ items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list
}
let int_of_string s =
| Ast.Level precedence ->
Gramext.Snterml
(Grammar.Entry.obj
- (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e),
+ (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
level_of precedence)
;;
| `Keyword s -> gram_keyword s
| `Number s -> gram_number s
-type binding =
- | NoBinding
- | Binding of string * Env.value_type
- | Env of (string * Env.value_type) list
-
let make_action action bindings =
let rec aux (vl : NotationEnv.t) =
function
CL1P (cp,level)
;;
-let extend status (CL1P (level1_pattern,precedence)) action =
- assert false
-(*
- CicNotationParser.new_parser ();
- let create_cb_old (l1, precedence, associativity, l2) =
- ignore(
- CicNotationParser.extend l1
- (fun env loc ->
- NotationPt.AttributedTerm
- (`Loc loc,TermContentPres.instantiate_level2 env l2)))
- in
- RefCounter.iter create_cb_old !parser_ref_counter;
-*)
-(*
- let p_bindings, p_atoms =
- List.split (extract_term_production status level1_pattern)
- in
- let level = level_of precedence in
- let () =
- Grammar.extend
- [ Grammar.Entry.obj
- (status#notation_parser_db.grammars.term: 'a Grammar.Entry.e),
- Some (Gramext.Level level),
- [ None,
- Some (*Gramext.NonA*) Gramext.NonA,
- [ p_atoms,
- (make_action
- (fun (env: NotationEnv.t) (loc: Ast.location) ->
- (action env loc))
- p_bindings) ]]]
- in
- let keywords = NotationUtil.keywords_of_term level1_pattern in
- let rule_id = p_atoms in
- List.iter CicNotationLexer.add_level2_ast_keyword keywords;
- rule_id
-*)
-
(** {2 Grammar} *)
let fold_cluster binder terms ty body =
grammars
;;
-let initial_grammars =
- let lexers = CicNotationLexer.mk_lexers [] in
+let initial_grammars keywords =
+ let lexers = CicNotationLexer.mk_lexers keywords in
let level1_pattern_grammar =
Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in
let level2_ast_grammar =
method notation_parser_db: db
end
-class status =
- object(self)
- val db = { grammars = initial_grammars ; items = [] }
+class status ~keywords:kwds =
+ object
+ val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
method notation_parser_db = db
method set_notation_parser_db v = {< db = v >}
method set_notation_parser_status
= fun o -> {< db = o#notation_parser_db >}
end
+let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
+ (* move inside constructor XXX *)
+ let add1item status (level, level1_pattern, action) =
+ let p_bindings, p_atoms =
+ List.split (extract_term_production status level1_pattern) in
+ Grammar.extend
+ [ Grammar.Entry.obj
+ (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e),
+ Some (Gramext.Level level),
+ [ None,
+ Some (*Gramext.NonA*) Gramext.NonA,
+ [ p_atoms,
+ (make_action
+ (fun (env: NotationEnv.t) (loc: Ast.location) ->
+ (action env loc))
+ p_bindings) ]]];
+ status
+ in
+ let current_item =
+ let level = level_of precedence in
+ level, level1_pattern, action in
+ let keywords = NotationUtil.keywords_of_term level1_pattern @
+ status#notation_parser_db.keywords in
+ let items = current_item :: status#notation_parser_db.items in
+ let status = status#set_notation_parser_status (new status ~keywords) in
+ let status = status#set_notation_parser_db
+ {status#notation_parser_db with items = items} in
+ List.fold_left add1item status items
+;;
+
+
let parse_level1_pattern status =
parse_level1_pattern status#notation_parser_db.grammars
let parse_level2_ast status =
method notation_parser_db: db
end
-class status:
+class status: keywords:string list ->
object('self)
inherit g_status
method set_notation_parser_db: db -> 'self
let status =
Interpretations.add_interpretation status
dsc (symbol, args) cic_appl_pattern in
- let mode = assert false in (* VEDI SOTTO *)
+ let mode = GrafiteAst.WithPreferences (*assert false*) in (* VEDI SOTTO *)
let diff =
[DisambiguateTypes.Symbol (symbol, 0),
GrafiteAst.Symbol_alias (symbol,0,dsc)] in
let status = LexiconEngine.set_proof_aliases status mode diff in
- assert false (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO
+ status, []
+ (*assert false*) (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO
IL MODE WithPreference/WithOutPreferences*)
| GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
let l1 =
in
let status =
if dir <> Some `RightToLeft then
- CicNotationParser.extend status l1
+ GrafiteParser.extend status l1
(fun env loc ->
NotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2))
else
status
in
- assert false (* MANCA SALVATAGGIO SU DISCO *)
- status
+(* assert false (* MANCA SALVATAGGIO SU DISCO *) *)
+ status, [] (* capire [] XX *)
| GrafiteAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
dependenciesParser.cmi:
grafiteParser.cmi:
-cicNotation2.cmi:
grafiteDisambiguate.cmi:
print_grammar.cmi: grafiteParser.cmi
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
-cicNotation2.cmo: cicNotation2.cmi
-cicNotation2.cmx: cicNotation2.cmi
grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
print_grammar.cmo: print_grammar.cmi
dependenciesParser.cmi:
grafiteParser.cmi:
-cicNotation2.cmi:
-nEstatus.cmi:
-grafiteDisambiguate.cmi: nEstatus.cmi
-print_grammar.cmi:
+grafiteDisambiguate.cmi:
+print_grammar.cmi: grafiteParser.cmi
dependenciesParser.cmo: dependenciesParser.cmi
dependenciesParser.cmx: dependenciesParser.cmi
grafiteParser.cmo: grafiteParser.cmi
grafiteParser.cmx: grafiteParser.cmi
-cicNotation2.cmo: grafiteParser.cmi cicNotation2.cmi
-cicNotation2.cmx: grafiteParser.cmx cicNotation2.cmi
-nEstatus.cmo: nEstatus.cmi
-nEstatus.cmx: nEstatus.cmi
grafiteDisambiguate.cmo: grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: grafiteDisambiguate.cmi
print_grammar.cmo: print_grammar.cmi
INTERFACE_FILES = \
dependenciesParser.mli \
grafiteParser.mli \
- cicNotation2.mli \
grafiteDisambiguate.mli \
print_grammar.mli \
$(NULL)
+++ /dev/null
-(* 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$ *)
-
-let load_notation status ~include_paths fname =
- assert false
-(*
- let ic = open_in fname in
- let lexbuf = Ulexing.from_utf8_channel ic in
- let status = ref status in
- try
- while true do
- status := fst (GrafiteParser.parse_statement lexbuf !status)
- done;
- assert false
- with End_of_file -> close_in ic; !status
-*)
+++ /dev/null
-(* 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/
- *)
-
-(** @param fname file from which load notation *)
-val load_notation:
- #LexiconTypes.status as 'status -> include_paths:string list -> string ->
- 'status
m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
G.NCopy (loc,s,NUri.uri_of_string u,
List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
+ | lc = lexicon_command -> lc
]];
lexicon_command: [ [
LSome (G.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
LSome (G.Executable (loc,G.NCommand (loc,G.Include (iloc,mode,fname))))
- | scom = lexicon_command ; SYMBOL "." ->
- assert false
-(*
- let status = LE.eval_command status scom in
- status, LNone loc
-*)
| EOI -> raise End_of_file
]
];
end
class status =
- let lstatus = assert false in
- let grammar = CicNotationParser.level2_ast_grammar lstatus in
- object
- inherit LexiconTypes.status
- val db =
- mk_parser (Grammar.Entry.create grammar "statement") lstatus
- method parser_db = db
- method set_parser_db v = {< db = v >}
+ object(self)
+ inherit LexiconTypes.status as super
+ val mutable db = None
+ method parser_db = match db with None -> assert false | Some x -> x
+ method set_parser_db v = {< db = Some v >}
method set_parser_status
: 'status. #g_status as 'status -> 'self
- = fun o -> {< db = o#parser_db >}#set_lexicon_engine_status o
+ = fun o -> {< db = Some o#parser_db >}#set_lexicon_engine_status o
+ initializer
+ let grammar = CicNotationParser.level2_ast_grammar self in
+ db <- Some (mk_parser (Grammar.Entry.create grammar "statement") self)
end
+let extend status l1 action =
+ let status = CicNotationParser.extend status l1 action in
+ let grammar = CicNotationParser.level2_ast_grammar status in
+ status#set_parser_db
+ (mk_parser (Grammar.Entry.create grammar "statement") status)
+;;
+
+
let parse_statement status =
parse_statement status#parser_db
method set_parser_status : 'status. #g_status as 'status -> 'self
end
+val extend : #status as 'status ->
+ CicNotationParser.checked_l1_pattern ->
+ (NotationEnv.t -> NotationPt.location -> NotationPt.term) -> 'status
+
+
(* never_include: do not call LexiconEngine to do includes,
* always raise NoInclusionPerformed *)
(** @raise End_of_file *)
object(self)
inherit Interpretations.status
inherit TermContentPres.status
- inherit CicNotationParser.status
+ inherit CicNotationParser.status ~keywords:[]
val lstatus = initial_status
method lstatus = lstatus
method set_lstatus v = {< lstatus = v >}
+++ /dev/null
-(* exists *******************************************************************)
-
-notation "hvbox(∃ _ break . p)"
- with precedence 20
-for @{'exists $p }.
-
-notation < "hvbox(\exists ident i : ty break . p)"
- right associative with precedence 20
-for @{'exists (\lambda ${ident i} : $ty. $p) }.
-
-notation < "hvbox(\exists ident i break . p)"
- with precedence 20
-for @{'exists (\lambda ${ident i}. $p) }.
-
-(*
-notation < "hvbox(\exists ident i opt (: ty) break . p)"
- right associative with precedence 20
-for @{ 'exists ${default
- @{\lambda ${ident i} : $ty. $p}
- @{\lambda ${ident i} . $p}}}.
-*)
-
-notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
- with precedence 20
- for ${ default
- @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
- @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
- }.
-
-(* sigma ********************************************************************)
-
-notation < "hvbox(\Sigma ident i : ty break . p)"
- left associative with precedence 20
-for @{'sigma (\lambda ${ident i} : $ty. $p) }.
-
-notation < "hvbox(\Sigma ident i break . p)"
- with precedence 20
-for @{'sigma (\lambda ${ident i}. $p) }.
-
-(*
-notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
- right associative with precedence 20
-for @{ 'sigma ${default
- @{\lambda ${ident i} : $ty. $p}
- @{\lambda ${ident i} . $p}}}.
-*)
-
-notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
- with precedence 20
- for ${ default
- @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
- @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
- }.
-
-(* equality, conguence ******************************************************)
-
-notation > "hvbox(a break = b)"
- non associative with precedence 45
-for @{ 'eq ? $a $b }.
-
-notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
- non associative with precedence 45
-for @{ 'eq $t $a $b }.
-
-notation > "hvbox(n break (≅ \sub term 90 p) m)"
- non associative with precedence 45
-for @{ 'congruent $n $m $p }.
-
-notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
- non associative with precedence 45
-for @{ 'congruent $n $m $p }.
-
-(* other notations **********************************************************)
-
-notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
-with precedence 90 for @{ 'pair $a $b}.
-
-notation "hvbox(x break \times y)" with precedence 70
-for @{ 'product $x $y}.
-
-notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
-notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
-
-notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
-notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
-
-notation > "\fst" with precedence 90 for @{'pi1}.
-notation > "\snd" with precedence 90 for @{'pi2}.
-
-notation "hvbox(a break \to b)"
- right associative with precedence 20
-for @{ \forall $_:$a.$b }.
-
-notation < "hvbox(a break \to b)"
- right associative with precedence 20
-for @{ \Pi $_:$a.$b }.
-
-notation "hvbox(a break \leq b)"
- non associative with precedence 45
-for @{ 'leq $a $b }.
-
-notation "hvbox(a break \geq b)"
- non associative with precedence 45
-for @{ 'geq $a $b }.
-
-notation "hvbox(a break \lt b)"
- non associative with precedence 45
-for @{ 'lt $a $b }.
-
-notation "hvbox(a break \gt b)"
- non associative with precedence 45
-for @{ 'gt $a $b }.
-
-notation > "hvbox(a break \neq b)"
- non associative with precedence 45
-for @{ 'neq ? $a $b }.
-
-notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
- non associative with precedence 45
-for @{ 'neq $t $a $b }.
-
-notation "hvbox(a break \nleq b)"
- non associative with precedence 45
-for @{ 'nleq $a $b }.
-
-notation "hvbox(a break \ngeq b)"
- non associative with precedence 45
-for @{ 'ngeq $a $b }.
-
-notation "hvbox(a break \nless b)"
- non associative with precedence 45
-for @{ 'nless $a $b }.
-
-notation "hvbox(a break \ngtr b)"
- non associative with precedence 45
-for @{ 'ngtr $a $b }.
-
-notation "hvbox(a break \divides b)"
- non associative with precedence 45
-for @{ 'divides $a $b }.
-
-notation "hvbox(a break \ndivides b)"
- non associative with precedence 45
-for @{ 'ndivides $a $b }.
-
-notation "hvbox(a break + b)"
- left associative with precedence 50
-for @{ 'plus $a $b }.
-
-notation "hvbox(a break - b)"
- left associative with precedence 50
-for @{ 'minus $a $b }.
-
-notation "hvbox(a break * b)"
- left associative with precedence 55
-for @{ 'times $a $b }.
-
-notation "hvbox(a break \middot b)"
- left associative with precedence 55
- for @{ 'middot $a $b }.
-
-notation "hvbox(a break \mod b)"
- left associative with precedence 55
-for @{ 'module $a $b }.
-
-notation < "a \frac b"
- non associative with precedence 90
-for @{ 'divide $a $b }.
-
-notation "a \over b"
- left associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "hvbox(a break / b)"
- left associative with precedence 55
-for @{ 'divide $a $b }.
-
-notation "- term 60 a" with precedence 60
-for @{ 'uminus $a }.
-
-notation "a !"
- non associative with precedence 80
-for @{ 'fact $a }.
-
-notation "\sqrt a"
- non associative with precedence 60
-for @{ 'sqrt $a }.
-
-notation "hvbox(a break \lor b)"
- left associative with precedence 30
-for @{ 'or $a $b }.
-
-notation "hvbox(a break \land b)"
- left associative with precedence 35
-for @{ 'and $a $b }.
-
-notation "hvbox(\lnot a)"
- non associative with precedence 40
-for @{ 'not $a }.
-
-notation > "hvbox(a break \liff b)"
- left associative with precedence 25
-for @{ 'iff $a $b }.
-
-notation "hvbox(a break \leftrightarrow b)"
- left associative with precedence 25
-for @{ 'iff $a $b }.
-
-
-notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
-for @{ 'powerset $A }.
-notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
-for @{ 'powerset $A }.
-
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
-
-notation "hvbox(a break ∈ b)" non associative with precedence 45
-for @{ 'mem $a $b }.
-
-notation "hvbox(a break ≬ b)" non associative with precedence 45
-for @{ 'overlaps $a $b }. (* \between *)
-
-notation "hvbox(a break ⊆ b)" non associative with precedence 45
-for @{ 'subseteq $a $b }. (* \subseteq *)
-
-notation "hvbox(a break ∩ b)" left associative with precedence 55
-for @{ 'intersects $a $b }. (* \cap *)
-
-notation "hvbox(a break ∪ b)" left associative with precedence 50
-for @{ 'union $a $b }. (* \cup *)
-
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
-notation "hvbox(a break \approx b)" non associative with precedence 45
- for @{ 'napart $a $b}.
-
-notation "hvbox(a break # b)" non associative with precedence 45
- for @{ 'apart $a $b}.
-
-notation "hvbox(a break \circ b)"
- left associative with precedence 55
-for @{ 'compose $a $b }.
-
-notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
-notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
-
-notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
-
-notation "↑a" with precedence 55 for @{ 'uparrow $a }.
-
-notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
-
-notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
-notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
-notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
-notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
-notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
-notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
-
-notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
-
-notation "\naturals" non associative with precedence 90 for @{'N}.
-notation "\rationals" non associative with precedence 90 for @{'Q}.
-notation "\reals" non associative with precedence 90 for @{'R}.
-notation "\integers" non associative with precedence 90 for @{'Z}.
-notation "\complexes" non associative with precedence 90 for @{'C}.
-
-notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
-
-notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
-notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation > "⊩ " with precedence 60 for @{'Vdash ?}.
-notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
-
-notation < "maction (mstyle color #ff0000 (…)) (t)"
-non associative with precedence 90 for @{'hide $t}.
-
(* CSC: there is a known bug in invalidation; temporary fix here *)
NCicEnvironment.invalidate ()
| None -> ());
- let lexicon_status =
- CicNotation2.load_notation ~include_paths:[] empty_lstatus
- BuildTimeConf.core_notation_script
- in
+ let lexicon_status = empty_lstatus in
let grafite_status = (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
grafite_status
in
Librarian.baseuri_of_script ~include_paths fname in
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
- let lexicon_status =
- CicNotation2.load_notation ~include_paths:[] (new LexiconTypes.status)
- BuildTimeConf.core_notation_script
- in
+ let lexicon_status = new LexiconTypes.status in
atstart (); (* FG: do not invoke before loading the core notation script *)
let grafite_status =
(new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in
--- /dev/null
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'exists ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+ }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'sigma ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+ }.
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)"
+ non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
+ non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+notation "hvbox(a break \leq b)"
+ non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)"
+ non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)"
+ non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)"
+ non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)"
+ non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
+ non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)"
+ non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)"
+ non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)"
+ non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)"
+ non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+ non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+ non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)"
+ left associative with precedence 50
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)"
+ left associative with precedence 50
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)"
+ left associative with precedence 55
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)"
+ left associative with precedence 55
+ for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)"
+ left associative with precedence 55
+for @{ 'module $a $b }.
+
+notation < "a \frac b"
+ non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "- term 60 a" with precedence 60
+for @{ 'uminus $a }.
+
+notation "a !"
+ non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a"
+ non associative with precedence 60
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)"
+ left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)"
+ left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)"
+ non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45
+ for @{ 'napart $a $b}.
+
+notation "hvbox(a break # b)" non associative with precedence 45
+ for @{ 'apart $a $b}.
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 55 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+
+notation < "maction (mstyle color #ff0000 (…)) (t)"
+non associative with precedence 90 for @{'hide $t}.
projects / helm.git / commitdiff