From: Enrico Tassi Date: Thu, 19 Jun 2008 11:18:58 +0000 (+0000) Subject: notation on steroids: 'term 40 x' is a valid variable name in notation and X-Git-Tag: make_still_working~5014 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c4659819a1c1f2e450d9a588ecca37d95ae48e9;p=helm.git notation on steroids: 'term 40 x' is a valid variable name in notation and places 'x' at term level 40 even if the notation is placed elsewhere --- diff --git a/helm/software/components/acic_content/cicNotationEnv.ml b/helm/software/components/acic_content/cicNotationEnv.ml index 5a1c4c945..f0a14846f 100644 --- a/helm/software/components/acic_content/cicNotationEnv.ml +++ b/helm/software/components/acic_content/cicNotationEnv.ml @@ -35,7 +35,7 @@ type value = | ListValue of value list type value_type = - | TermType of (int * Gramext.g_assoc) option + | TermType of int option | StringType | NumType | OptType of value_type diff --git a/helm/software/components/acic_content/cicNotationEnv.mli b/helm/software/components/acic_content/cicNotationEnv.mli index 5d2bba6c7..c332bcfff 100644 --- a/helm/software/components/acic_content/cicNotationEnv.mli +++ b/helm/software/components/acic_content/cicNotationEnv.mli @@ -33,7 +33,7 @@ type value = | ListValue of value list type value_type = - | TermType of (int * Gramext.g_assoc) option + | TermType of int option | StringType | NumType | OptType of value_type diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 7fbc9f492..4f94fa742 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -54,12 +54,6 @@ let pp_literal = | `Keyword s | `Number s -> s) -let pp_assoc = - function - | Gramext.NonA -> "N" - | Gramext.LeftA -> "L" - | Gramext.RightA -> "R" - let pp_pos = function (* `None -> "`None" *) @@ -74,7 +68,7 @@ let pp_attribute = 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) @@ -257,7 +251,7 @@ and pp_variable = function | 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 @@ -335,7 +329,7 @@ let rec pp_value = function 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 diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 92d081fee..1ca514810 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -44,8 +44,7 @@ type child_pos = [ `Left | `Right | `Inner ] 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 *) @@ -145,7 +144,7 @@ and pattern_variable = (* 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 @@ -187,8 +186,3 @@ let binder_prec = 20 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 - diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 7690aeb9b..698539207 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -57,16 +57,10 @@ let int_of_string s = (** {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) @@ -74,8 +68,8 @@ let gram_number s = Gramext.Stoken ("NUMBER", 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 = @@ -180,20 +174,6 @@ 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 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 @@ -234,18 +214,88 @@ type rule_id = Grammar.token Gramext.g_symbol list (* 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) -> @@ -305,9 +355,7 @@ let _ = | 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 @@ -339,15 +387,9 @@ EXTEND | "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 ] @@ -399,15 +441,9 @@ EXTEND (* {{{ 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 @@ -568,7 +604,8 @@ EXTEND | vars = protected_binder_vars -> vars ] ]; - term: LEVEL "10N" [ (* let in *) + term: LEVEL "10N" + [ [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) @@ -580,16 +617,16 @@ EXTEND 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> (* ∃ *); - (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 @@ -601,7 +638,7 @@ EXTEND 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 -> diff --git a/helm/software/components/content_pres/cicNotationParser.mli b/helm/software/components/content_pres/cicNotationParser.mli index 134a42c3c..161c9167c 100644 --- a/helm/software/components/content_pres/cicNotationParser.mli +++ b/helm/software/components/content_pres/cicNotationParser.mli @@ -26,6 +26,8 @@ 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 *) @@ -39,10 +41,11 @@ val parse_level2_meta: Ulexing.lexbuf -> CicNotationPt.term 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 diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index a7bce6437..84eaaeb2a 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -181,22 +181,15 @@ let is_atomic t = 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) -> @@ -257,10 +250,10 @@ let render ids_to_uris ?(prec=(-1)) = 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) @@ -293,7 +286,7 @@ let render ids_to_uris ?(prec=(-1)) = 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 @@ -307,7 +300,7 @@ let render ids_to_uris ?(prec=(-1)) = (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 @@ -316,19 +309,18 @@ let render ids_to_uris ?(prec=(-1)) = @ (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 @@ -336,29 +328,28 @@ let render ids_to_uris ?(prec=(-1)) = (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 = @@ -367,11 +358,11 @@ let render ids_to_uris ?(prec=(-1)) = | `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) @@ -388,18 +379,18 @@ let render ids_to_uris ?(prec=(-1)) = 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 @@ -410,30 +401,11 @@ let render ids_to_uris ?(prec=(-1)) = | (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 @@ -444,7 +416,7 @@ let render ids_to_uris ?(prec=(-1)) = 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 diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 8f15664d0..89dba2987 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -42,18 +42,9 @@ let resolve_binder = function | `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 @@ -112,18 +103,18 @@ let pp_ast0 t k = | [] -> [] | [ 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 @@ -189,17 +180,17 @@ let pp_ast0 t k = 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; @@ -251,7 +242,7 @@ let pp_ast0 t k = [ 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 ]))) @@ -337,7 +328,7 @@ let instantiate21 idrefs env l1 = 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 @@ -486,9 +477,9 @@ let fresh_id = 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; diff --git a/helm/software/components/content_pres/termContentPres.mli b/helm/software/components/content_pres/termContentPres.mli index 77cda8a81..9b36a9345 100644 --- a/helm/software/components/content_pres/termContentPres.mli +++ b/helm/software/components/content_pres/termContentPres.mli @@ -28,10 +28,8 @@ 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 diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 101e55a54..6fcb9dba4 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -743,6 +743,9 @@ let exc_located_wrapper f = | 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))) diff --git a/helm/software/components/lexicon/cicNotation.ml b/helm/software/components/lexicon/cicNotation.ml index bea67a0b4..e10a89d5b 100644 --- a/helm/software/components/lexicon/cicNotation.ml +++ b/helm/software/components/lexicon/cicNotation.ml @@ -38,13 +38,16 @@ let rule_ids_to_items = Hashtbl.create 113 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 @@ -56,7 +59,7 @@ let process_notation st = let pp_id = if dir <> Some `LeftToRight then [ PrettyPrinterId - (TermContentPres.add_pretty_printer ?precedence ?associativity + (TermContentPres.add_pretty_printer l2 l1) ] else [] diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo index 17d5993b1..b991adac5 100644 --- a/helm/software/matita/core_notation.moo +++ b/helm/software/matita/core_notation.moo @@ -88,12 +88,7 @@ notation "hvbox(a break / b)" 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 !" diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma index 8b1beb702..d3f5cf272 100644 --- a/helm/software/matita/library/algebra/finite_groups.ma +++ b/helm/software/matita/library/algebra/finite_groups.ma @@ -46,7 +46,7 @@ interpretation "Finite_enumerable representation" 'repr S i = (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" diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma index c83b3d2d0..aeb0d779a 100644 --- a/helm/software/matita/library/algebra/groups.ma +++ b/helm/software/matita/library/algebra/groups.ma @@ -144,7 +144,7 @@ record morphism (G,G':Group) : Type ≝ 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 = @@ -193,10 +193,10 @@ interpretation "Subgroup image" 'subgroupimage H 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 = @@ -235,7 +235,7 @@ definition left_coset_disjoint ≝ λ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 }. diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 76fa66115..9e360caab 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -294,8 +294,7 @@ interpretation "Rderivative" 'derivative \eta.f = (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 = diff --git a/helm/software/matita/library/demo/realisability.ma b/helm/software/matita/library/demo/realisability.ma index 93b5e712f..d1b569c40 100644 --- a/helm/software/matita/library/demo/realisability.ma +++ b/helm/software/matita/library/demo/realisability.ma @@ -57,7 +57,7 @@ definition pi2 ≝ 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} diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma index f3738eca1..2e0df971e 100644 --- a/helm/software/matita/library/list/list.ma +++ b/helm/software/matita/library/list/list.ma @@ -23,7 +23,7 @@ inductive list (A:Type) : Type := | 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 ; ]" @@ -41,8 +41,7 @@ interpretation "cons" 'cons hd tl = (* 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; diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma index 884c18ddc..4654f33fc 100644 --- a/helm/software/matita/library/nat/permutation.ma +++ b/helm/software/matita/library/nat/permutation.ma @@ -72,12 +72,10 @@ match eqb n i with [ 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 =