| ListValue of value list
type value_type =
- | TermType of (int * Gramext.g_assoc) option
+ | TermType of int option
| StringType
| NumType
| OptType of value_type
| ListValue of value list
type value_type =
- | TermType of (int * Gramext.g_assoc) option
+ | TermType of int option
| StringType
| NumType
| OptType of value_type
| `Keyword s
| `Number s -> s)
-let pp_assoc =
- function
- | Gramext.NonA -> "N"
- | Gramext.LeftA -> "L"
- | Gramext.RightA -> "R"
-
let pp_pos =
function
(* `None -> "`None" *)
sprintf "X(%s)"
(String.concat ";"
(List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
- | `Level (prec, assoc) -> sprintf "L(%d%s)" prec (pp_assoc assoc)
+ | `Level (prec) -> sprintf "L(%d)" prec
| `Raw _ -> "R"
| `Loc _ -> "@"
| `ChildPos p -> sprintf "P(%s)" (pp_pos p)
| Ast.NumVar s -> "number " ^ s
| Ast.IdentVar s -> "ident " ^ s
| Ast.TermVar (s,None) -> s
- | Ast.TermVar (s,Some (l,a)) -> "term " ^string_of_int l ^ " " ^ pp_assoc a ^ " " ^ s
+ | Ast.TermVar (s,Some l) -> "term " ^string_of_int l
| Ast.Ascription (t, n) -> assert false
| Ast.FreshVar n -> "fresh " ^ n
let rec pp_value_type =
function
| Env.TermType None -> "Term"
- | Env.TermType (Some (l,a)) -> "Term "^string_of_int l ^ " " ^ pp_assoc a
+ | Env.TermType (Some l) -> "Term "^string_of_int l
| Env.StringType -> "String"
| Env.NumType -> "Number"
| Env.OptType t -> "Maybe " ^ pp_value_type t
type term_attribute =
[ `Loc of location (* source file location *)
| `IdRef of string (* ACic pointer *)
- | `Level of int * Gramext.g_assoc (* precedence, associativity *)
- | `ChildPos of child_pos (* position of l1 pattern variables *)
+ | `Level of int
| `XmlAttrs of (string option * string * string) list
(* list of XML attributes: namespace, name, value *)
| `Raw of string (* unparsed version *)
(* level 1 and 2 variables *)
| NumVar of string
| IdentVar of string
- | TermVar of string * (int * Gramext.g_assoc) option
+ | TermVar of string * int option
(* level 1 variables *)
| Ascription of term * string
let apply_prec = 70
let simple_prec = 90
-let let_in_assoc = Gramext.NonA
-let binder_assoc = Gramext.RightA
-let apply_assoc = Gramext.LeftA
-let simple_assoc = Gramext.NonA
-
(** {2 Grammar extension} *)
-let level_of precedence associativity =
+let level_of precedence =
if precedence < min_precedence || precedence > max_precedence then
raise (Level_not_found precedence);
- let assoc_string =
- match associativity with
- | Gramext.NonA -> "N"
- | Gramext.LeftA -> "L"
- | Gramext.RightA -> "R"
- in
- string_of_int precedence ^ assoc_string
+ string_of_int precedence ^ "N"
let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
let gram_ident s = Gramext.Stoken ("IDENT", s)
let gram_keyword s = Gramext.Stoken ("", s)
let gram_term = function
| None -> Gramext.Sself
- | Some (precedence, associativity) ->
- Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence associativity)
+ | Some (precedence) ->
+ Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence)
;;
let gram_of_literal =
| Ast.List0 (p, _)
| Ast.List1 (p, _) ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-(* let env0 = List.map list_binding_of_name p_names 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 *)
let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
CicNotationEnv.coalesce_env p_names env_list
in
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
let owned_keywords = Hashtbl.create 23
-let extend level1_pattern ~precedence ~associativity action =
+type checked_l1_pattern = CL1P of CicNotationPt.term * int
+
+let check_l1_pattern level1_pattern level associativity =
+ let variables = ref 0 in
+ let symbols = ref 0 in
+ let rec aux = function
+ | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t)
+ | Ast.Literal _ as l -> incr symbols; l
+ | Ast.Layout l -> Ast.Layout (aux_layout l)
+ | Ast.Magic m -> Ast.Magic (aux_magic m)
+ | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | t -> assert false
+ and aux_layout = function
+ | Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
+ | Ast.Sup (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (p1, p2)
+ | Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
+ | Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
+ | Ast.Frac (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+ | Ast.Atop (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
+ | Ast.Over (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
+ | Ast.Root (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
+ | Ast.Sqrt p -> Ast.Sqrt (aux p)
+ | Ast.Break as t -> t
+ | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
+ | Ast.Group pl -> Ast.Group (List.map aux pl)
+ and aux_magic magic =
+ match magic with
+ | Ast.Opt p -> Ast.Opt (aux p)
+ | Ast.List0 (p, x) -> Ast.List0 (aux p, x)
+ | Ast.List1 (p, x) -> Ast.List1 (aux p, x)
+ | _ -> assert false
+ and aux_variable =
+ function
+ | Ast.NumVar _ as t -> t
+ | Ast.TermVar (s,None) when associativity <> Gramext.NonA ->
+ incr variables;
+ if !variables > 2 then
+ raise (Parse_error ("Exactly 2 variables must be specified in an "^
+ "associative notation"));
+ (match !variables, associativity with
+ | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some
+ (level-1)) *)
+ | 1,Gramext.RightA -> Ast.TermVar (s, None)
+ | 2,Gramext.LeftA ->Ast.TermVar (s, None)
+ | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1))
+ | _ -> assert false)
+ | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA ->
+ raise (Parse_error ("Variables can not be declared with a " ^
+ "precedence in an associative notation"))
+ (* avoid camlp5 divergence due to non-Sself recursion at the same level *)
+ | Ast.TermVar (s,Some l) when l=level ->
+ incr variables;
+ Ast.TermVar (s,None)
+ (* avoid camlp5 divergence due to non-Sself left recursion *)
+ | Ast.TermVar (s,Some _) when !symbols = 0 && !variables = 0 ->
+ raise (Parse_error "Left recursive rule with precedence not allowed")
+ | Ast.TermVar _ as t -> incr variables; t
+ | Ast.IdentVar _ as t -> t
+ | Ast.Ascription _ -> assert false (* TODO *)
+ | Ast.FreshVar _ -> assert false
+ in
+ if associativity <> Gramext.NonA && level = min_precedence then
+ raise (Parse_error ("You can not specify an associative notation " ^
+ "at level "^string_of_int min_precedence ^ "; increase it"));
+ let cp = CL1P (aux level1_pattern, level) in
+ if !variables <> 2 && associativity <> Gramext.NonA then
+ raise (Parse_error ("Exactly 2 variables must be specified in an "^
+ "associative notation"));
+ cp
+;;
+
+let extend (CL1P (level1_pattern,precedence)) action =
let p_bindings, p_atoms =
List.split (extract_term_production level1_pattern)
in
- let level = level_of precedence associativity in
-(* let p_names = flatten_opt p_bindings in *)
+ let level = level_of precedence in
let _ =
Grammar.extend
[ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
Some (Gramext.Level level),
[ None,
- Some associativity,
+ Some (*Gramext.NonA*) Gramext.LeftA,
[ p_atoms,
(make_action
(fun (env: CicNotationEnv.t) (loc: Ast.location) ->
| i when i < first -> acc
| i ->
aux
- ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod)
- :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod)
- :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod)
+ ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.LeftA, dummy_prod)
:: acc)
(i - 1)
in
| "opt"; p = l1_simple_pattern -> Ast.Opt p
]
];
- l1_associativity : [
- [ IDENT "L" -> Gramext.LeftA
- | IDENT "N" -> Gramext.NonA
- | IDENT "R" -> Gramext.RightA
- ]
- ];
l1_pattern_variable: [
- [ "term"; precedence = NUMBER; assoc = l1_associativity ; id = IDENT ->
- Ast.TermVar (id, Some (int_of_string precedence,assoc))
+ [ "term"; precedence = NUMBER; id = IDENT ->
+ Ast.TermVar (id, Some (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
(* {{{ Grammar for ast magics, notation level 2 *)
EXTEND
GLOBAL: level2_meta;
- l2_associativity : [
- [ IDENT "L" -> Gramext.LeftA
- | IDENT "N" -> Gramext.NonA
- | IDENT "R" -> Gramext.RightA
- ]
- ];
l2_variable: [
- [ "term"; precedence = NUMBER; assoc = l2_associativity; id = IDENT ->
- Ast.TermVar (id,Some (int_of_string precedence, assoc))
+ [ "term"; precedence = NUMBER; id = IDENT ->
+ Ast.TermVar (id,Some (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
| "fresh"; id = IDENT -> Ast.FreshVar id
| vars = protected_binder_vars -> vars
]
];
- term: LEVEL "10N" [ (* let in *)
+ term: LEVEL "10N"
+ [
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
- term: LEVEL "20R" (* binder *)
+ term: LEVEL "20N"
[
- [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
+ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" ->
return_term loc (fold_cluster b vars typ body)
| SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
+ (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"->
return_term loc (fold_exists vars typ body)
]
];
- term: LEVEL "70L" (* apply *)
+ term: LEVEL "70N"
[
[ p1 = term; p2 = term ->
let rec aux = function
return_term loc (Ast.Appl (aux p1 @ [p2]))
]
];
- term: LEVEL "90N" (* simple *)
+ term: LEVEL "90N"
[
[ id = IDENT -> return_term loc (Ast.Ident (id, None))
| id = IDENT; s = explicit_subst ->
exception Parse_error of string
exception Level_not_found of int
+type checked_l1_pattern = private CL1P of CicNotationPt.term * int
+
(** {2 Parsing functions} *)
(** concrete syntax pattern: notation level 1 *)
type rule_id
+val check_l1_pattern: (* level1_pattern *)
+ CicNotationPt.term -> int -> Gramext.g_assoc -> checked_l1_pattern
+
val extend:
- CicNotationPt.term -> (* level 1 pattern *)
- precedence:int ->
- associativity:Gramext.g_assoc ->
+ checked_l1_pattern ->
(CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) ->
rule_id
in
aux_mpres t
-let add_parens child_prec child_assoc child_pos curr_prec t =
+let add_parens child_prec curr_prec t =
(* eprintf
("add_parens: " ^^
"child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!")
child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
curr_prec; *)
if is_atomic t then t
- else if child_prec >= 0
- && (child_prec < curr_prec
- || (child_prec = curr_prec &&
- child_assoc = Gramext.LeftA &&
- child_pos <> `Left)
- || (child_prec = curr_prec &&
- child_assoc = Gramext.RightA &&
- child_pos <> `Right))
- then begin (* parens should be added *)
+ else if child_prec >= 0 && child_prec < curr_prec then
+ begin (* parens should be added *)
(* prerr_endline "adding parens!"; *)
match t with
| Mpresentation.Mobject (_, box) ->
in
(* when mathonly is true no boxes should be generated, only mrows *)
(* "xref" is *)
- let rec aux xmlattrs mathonly xref pos prec t =
+ let rec aux xmlattrs mathonly xref prec t =
match t with
| A.AttributedTerm _ ->
- aux_attributes xmlattrs mathonly xref pos prec t
+ aux_attributes xmlattrs mathonly xref prec t
| A.Num (literal, _) ->
let attrs =
(RenderingAttrs.number_attributes `MathML)
box_of mathonly (A.H, false, false) [] [
Mpres.Mi ([], name);
Mpres.Mo ([], to_unicode "\\def");
- aux [] mathonly xref pos prec t ])
+ aux [] mathonly xref prec t ])
substs))
@ [ closed_brace ])
in
(List.map
(function
| None -> Mpres.Mtext ([], "_")
- | Some t -> aux xmlattrs mathonly xref pos prec t) l)) @
+ | Some t -> aux xmlattrs mathonly xref prec t) l)) @
[ Mpres.Mtext ([], "]")])
in
let lctxt_maction = toggle_action [ hidden_lctxt; local_context l ] in
@ (if l <> [] then [lctxt_maction] else []))
| A.Literal l -> aux_literal xmlattrs xref prec l
| A.UserInput -> Mpres.Mtext ([], "%")
- | A.Layout l -> aux_layout mathonly xref pos prec l
+ | A.Layout l -> aux_layout mathonly xref prec l
| A.Magic _
| A.Variable _ -> assert false (* should have been instantiated *)
| t ->
prerr_endline ("unexpected ast: " ^ CicNotationPp.pp_term t);
assert false
- and aux_attributes xmlattrs mathonly xref pos prec t =
+ and aux_attributes xmlattrs mathonly xref prec t =
let reset = ref false in
let inferred_level = ref None in
let expected_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
- let new_pos = ref pos in
(* let reinit = ref false in *)
let rec aux_attribute =
function
(match attr with
| `Loc _
| `Raw _ -> ()
- | `Level (-1, _) -> reset := true
- | `Level (child_prec, child_assoc) ->
+ | `Level (-1) -> reset := true
+ | `Level child_prec ->
assert (!expected_level = None);
expected_level := !inferred_level;
- inferred_level := Some (child_prec, child_assoc)
+ inferred_level := Some child_prec
| `IdRef xref -> new_xref := xref :: !new_xref
- | `ChildPos pos -> new_pos := pos
| `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
aux_attribute t
| t ->
let prec =
match !expected_level with
| None -> prec
- | Some (prec, _) -> prec
+ | Some prec -> prec
in
(match !inferred_level with
- | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
- | Some (child_prec, child_assoc) ->
+ | None -> aux !new_xmlattrs mathonly new_xref prec t
+ | Some child_prec ->
let t' =
- aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
+ aux !new_xmlattrs mathonly new_xref child_prec t in
if !reset
then t'
- else add_parens child_prec child_assoc !new_pos prec t')
+ else add_parens child_prec prec t')
in
aux_attribute t
and aux_literal xmlattrs xref prec l =
| `Symbol s -> Mpres.Mo (attrs, to_unicode s)
| `Keyword s -> Mpres.Mtext (attrs, to_unicode s)
| `Number s -> Mpres.Mn (attrs, to_unicode s))
- and aux_layout mathonly xref pos prec l =
+ and aux_layout mathonly xref prec l =
let attrs = make_xref xref in
- let invoke' t = aux [] true (ref []) pos prec t in
+ let invoke' t = aux [] true (ref []) prec t in
(* use the one below to reset precedence and associativity *)
- let invoke_reinit t = aux [] mathonly xref `Inner ~-1 t in
+ let invoke_reinit t = aux [] mathonly xref ~-1 t in
match l with
| A.Sub (t1, t2) -> Mpres.Msub (attrs, invoke' t1, invoke_reinit t2)
| A.Sup (t1, t2) -> Mpres.Msup (attrs, invoke' t1, invoke_reinit t2)
Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)
| A.Box ((_, spacing, _) as kind, terms) ->
let children =
- aux_children mathonly spacing xref pos prec
+ aux_children mathonly spacing xref prec
(CicNotationUtil.ungroup terms)
in
box_of mathonly kind attrs children
| A.Group terms ->
let children =
- aux_children mathonly false xref pos prec
+ aux_children mathonly false xref prec
(CicNotationUtil.ungroup terms)
in
box_of mathonly (A.H, false, false) attrs children
| A.Break -> assert false (* TODO? *)
- and aux_children mathonly spacing xref pos prec terms =
+ and aux_children mathonly spacing xref prec terms =
let find_clusters =
let rec aux_list first clusters acc =
function
| (A.Layout A.Break) :: tl ->
aux_list first (List.rev acc :: clusters) [] tl
| [hd] ->
-(* let pos' =
- if first then
- pos
- else
- match pos with
- `None -> `Right
- | `Inner -> `Inner
- | `Right -> `Right
- | `Left -> `Inner
- in *)
aux_list false clusters
- (aux [] mathonly xref pos prec hd :: acc) []
+ (aux [] mathonly xref prec hd :: acc) []
| hd :: tl ->
-(* let pos' =
- match pos, first with
- `None, true -> `Left
- | `None, false -> `Inner
- | `Left, true -> `Left
- | `Left, false -> `Inner
- | `Right, _ -> `Inner
- | `Inner, _ -> `Inner
- in *)
aux_list false clusters
- (aux [] mathonly xref pos prec hd :: acc) tl
+ (aux [] mathonly xref prec hd :: acc) tl
in
aux_list true [] []
in
in
List.map boxify_pres (find_clusters terms)
in
- aux [] false (ref []) `Inner prec
+ aux [] false (ref []) prec
let rec print_box (t: boxml_markup) =
Box.box2xml print_mpres t
| `Forall -> "\\forall"
| `Exists -> "\\exists"
-let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t)
-let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t)
-let left_pos = add_pos_info `Left
-let right_pos = add_pos_info `Right
-let inner_pos = add_pos_info `Inner
-
-let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t)
-(* function
- | Ast.AttributedTerm (`Level _, t) ->
- add_level_info ~-1 Gramext.NonA (inner_pos t)
- | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t)
- | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *)
+let add_level_info prec t = Ast.AttributedTerm (`Level prec, t)
+
+let rec top_pos t = add_level_info ~-1 t
let rec remove_level_info =
function
| [] -> []
| [ last ] ->
let last = k last in
- if pos = `Left then [ left_pos last ] else [ right_pos last ]
+ [ last ]
| hd :: tl ->
- (add_pos_info pos (k hd)) :: aux_args `Inner tl
+ (k hd) :: aux_args `Inner tl
in
- add_level_info Ast.apply_prec Ast.apply_assoc
+ add_level_info Ast.apply_prec
(hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
| Ast.Binder (binder_kind, (id, ty), body) ->
- add_level_info Ast.binder_prec Ast.binder_assoc
+ add_level_info Ast.binder_prec
(hvbox false true
[ binder_symbol (resolve_binder binder_kind);
k id; builtin_symbol ":"; aux_ty ty; break;
- builtin_symbol "."; right_pos (k body) ])
+ builtin_symbol "."; k body ])
| Ast.Case (what, indty_opt, outty_opt, patterns) ->
let outty_box =
match outty_opt with
hbox false false [ builtin_symbol "["; hd ]
:: aux_patterns tl
in
- add_level_info Ast.simple_prec Ast.simple_assoc
+ add_level_info Ast.simple_prec
(hvbox false false [
hvbox false false ([match_box]); break;
hbox false false [ hvbox false false patterns'' ] ])
| Ast.Cast (bo, ty) ->
- add_level_info Ast.simple_prec Ast.simple_assoc
+ add_level_info Ast.simple_prec
(hvbox false true [
builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":";
top_pos (k ty); builtin_symbol ")"])
| Ast.LetIn (var, s, t) ->
- add_level_info Ast.let_in_prec Ast.let_in_assoc
+ add_level_info Ast.let_in_prec
(hvbox false true [
hvbox false true [
keyword "let"; space;
[ builtin_symbol "\\def"; break; body ])])
tl_funs
in
- add_level_info Ast.let_in_prec Ast.let_in_assoc
+ add_level_info Ast.let_in_prec
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
Ast.AttributedTerm (`Level l,value)
| _ -> value
in
- [ add_pos_info pos value ]
+ [ value ]
| Ast.Magic m -> subst_magic pos env m
| Ast.Literal l as t ->
let t = add_idrefs idrefs t in
incr counter;
!counter
-let add_pretty_printer ~precedence ~associativity l2 l1 =
+let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) =
let id = fresh_id () in
- let l1' = add_level_info precedence associativity (fill_pos_info l1) in
+ let l1' = add_level_info precedence (fill_pos_info l1) in
let l2' = CicNotationUtil.strip_attributes l2 in
Hashtbl.add level1_patterns21 id l1';
pattern21_matrix := (l2', id) :: !pattern21_matrix;
type pretty_printer_id
val add_pretty_printer:
- precedence:int ->
- associativity:Gramext.g_assoc ->
CicNotationPt.term -> (* level 2 pattern *)
- CicNotationPt.term -> (* level 1 pattern *)
+ CicNotationParser.checked_l1_pattern ->
pretty_printer_id
exception Pretty_printer_not_found
| Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
| Stdpp.Exc_located (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
+ | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+ raise
+ (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
| Stdpp.Exc_located (floc, exn) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
let process_notation st =
match st with
| Notation (loc, dir, l1, associativity, precedence, l2) ->
+ let l1 =
+ CicNotationParser.check_l1_pattern l1 precedence associativity
+ in
let item = (l1, precedence, associativity, l2) in
let rule_id = ref [] in
let _ =
if dir <> Some `RightToLeft then
let create_cb (l1, precedence, associativity, l2) =
let id =
- CicNotationParser.extend l1 ?precedence ?associativity
+ CicNotationParser.extend l1
(fun env loc ->
CicNotationPt.AttributedTerm
(`Loc loc,TermContentPres.instantiate_level2 env l2)) in
let pp_id =
if dir <> Some `LeftToRight then
[ PrettyPrinterId
- (TermContentPres.add_pretty_printer ?precedence ?associativity
+ (TermContentPres.add_pretty_printer
l2 l1) ]
else
[]
left associative with precedence 55
for @{ 'divide $a $b }.
-notation > "- a"
- right associative with precedence 60
-for @{ 'uminus $a }.
-
-notation < "- a"
- right associative with precedence 75
+notation "- term 59 a" with precedence 60
for @{ 'uminus $a }.
notation "a !"
(cic:/matita/algebra/finite_groups/repr.con S
(cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
-notation "hvbox(ι e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 60
for @{ 'index_of_finite_enumerable_semigroup $e }.
interpretation "Index_of_finite_enumerable representation"
f_morph: ∀x,y:G.image(x·y) = image x · image y
}.
-notation "hvbox(f˜ x)" with precedence 79
+notation "hvbox(f\tilde x)" with precedence 79
for @{ 'morimage $f $x }.
interpretation "Morphism image" 'morimage f x =
definition member_of_subgroup ≝
λG.λH:subgroup G.λx:G.∃y.x=y \sub H.
-notation "hvbox(x break ∈ H)" with precedence 79
+notation "hvbox(x break \in H)" with precedence 79
for @{ 'member_of $x $H }.
-notation "hvbox(x break ∉ H)" with precedence 79
+notation "hvbox(x break \notin H)" with precedence 79
for @{ 'not_member_of $x $H }.
interpretation "Member of subgroup" 'member_of x H =
λG.λC,C':left_coset G.
∀x.¬(((element ? C)·x \sub (subgrp ? C)) ∈ C').
-notation "hvbox(a break ∥ b)"
+notation "hvbox(a break \par b)"
non associative with precedence 45
for @{ 'disjoint $a $b }.
(cic:/matita/demo/power_derivative/derivative.con f).
*)
-notation "hvbox(\frac 'd' ('d' 'x') break p)"
- right associative with precedence 90
+notation "hvbox(\frac 'd' ('d' 'x') break p)" with precedence 90
for @{ 'derivative $p}.
interpretation "Rderivative" 'derivative f =
match s return λs.P (pi1 ? ? s) with
[ sigma_intro _ p ⇒ p].
-notation "hvbox(Σ ident i opt (: ty) break . p)"
+notation "hvbox(\Sigma ident i opt (: ty) break . p)"
right associative with precedence 20
for @{ 'sigma ${default
@{\lambda ${ident i} : $ty. $p}
| cons: A -> list A -> list A.
notation "hvbox(hd break :: tl)"
- right associative with precedence 46
+ right associative with precedence 47
for @{'cons $hd $tl}.
notation "[ list0 x sep ; ]"
(* theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. *)
theorem nil_cons:
- \forall A:Type.\forall l:list A.\forall a:A.
- a::l <> [].
+ \forall A:Type.\forall l:list A.\forall a:A. a::l ≠ [].
intros;
unfold Not;
intros;
[ true \Rightarrow i
| false \Rightarrow n]].
-notation < "(❲i↹j❳)n"
- right associative with precedence 71
+notation < "(❲i↹j❳)n" with precedence 71
for @{ 'transposition $i $j $n}.
-notation < "(❲i \atop j❳)n"
- right associative with precedence 71
+notation < "(❲i \atop j❳)n" with precedence 71
for @{ 'transposition $i $j $n}.
interpretation "natural transposition" 'transposition i j n =
projects / helm.git / commitdiff