From: Stefano Zacchiroli Date: Tue, 5 Jul 2005 16:03:13 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_7_1~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=3d63cb9ed38f05c679fc3284a5b3bb4d92e52296;p=helm.git snapshot - bugfixes here and there ... - precedence still need to be fixed --- diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 92d6560fc..e5350566d 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -17,8 +17,8 @@ INTERFACE_FILES = \ cicNotationPp.mli \ cicNotationMatcher.mli \ cicNotationFwd.mli \ - cicNotationRew.mli \ cicNotationParser.mli \ + cicNotationRew.mli \ cicNotationPres.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 46469e769..1c1532548 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -117,14 +117,12 @@ struct let variable_closure k = (fun matched_terms terms -> - prerr_endline "variable_closure"; match terms with | hd :: tl -> k (hd :: matched_terms) tl | _ -> assert false) let constructor_closure ks k = (fun matched_terms terms -> - prerr_endline "constructor_closure"; match terms with | t :: tl -> (try @@ -187,9 +185,7 @@ struct | Pt.Variable _ -> Variable | Pt.Magic _ | Pt.Layout _ - | Pt.Literal _ as t -> - prerr_endline (CicNotationPp.pp_term t); - assert false + | Pt.Literal _ as t -> assert false | _ -> Constructor let tag_of_pattern = CicNotationTag.get_tag let tag_of_term = CicNotationTag.get_tag @@ -260,7 +256,6 @@ struct candidates in let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); let candidates = List.map (fun (pl, pid) -> @@ -355,7 +350,6 @@ struct let compiler rows = let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); let pl, pid = try List.hd rows with Not_found -> assert false in (fun matched_terms -> let env = diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 681dfd5e5..ba12b49da 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -37,6 +37,16 @@ let min_precedence = 0 let max_precedence = 100 let default_precedence = 50 +let let_in_prec = 10 +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 + let level1_pattern = Grammar.Entry.create grammar "level1_pattern" let level2_pattern = Grammar.Entry.create grammar "level2_pattern" let level3_term = Grammar.Entry.create grammar "level3_term" @@ -320,14 +330,15 @@ EXTEND | SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF -> return_term loc (Layout (Root (arg, index))); | SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box (H, p))) + return_term loc (Layout (Box ((H, false, false), p))) | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box (V, p))) + return_term loc (Layout (Box ((V, false, false), p))) | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box (HV, p))) + return_term loc (Layout (Box ((HV, false, false), p))) | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" -> - return_term loc (Layout (Box (HOV, p))) + return_term loc (Layout (Box ((HOV, false, false), p))) (* | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *) +(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *) | DELIM "\\["; p = l1_pattern; DELIM "\\]" -> return_term loc (CicNotationUtil.boxify p) | p = SELF; SYMBOL "\\AS"; id = IDENT -> diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index 6192bf05b..22dffd4bf 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -53,6 +53,18 @@ val extend: val delete: rule_id -> unit +(** {2 Standard precedences} *) + +val let_in_prec: int +val binder_prec: int +val apply_prec: int +val simple_prec: int + +val let_in_assoc: Gramext.g_assoc +val binder_assoc: Gramext.g_assoc +val apply_assoc: Gramext.g_assoc +val simple_assoc: Gramext.g_assoc + (** {2 Debugging} *) (** print "level2_pattern" entry on stdout, flushing afterwards *) diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml index d81550637..a3e4f4621 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.ml +++ b/helm/ocaml/cic_notation/cicNotationPp.ml @@ -118,6 +118,13 @@ and pp_capture_variable = function | term, None -> pp_term term | term, Some typ -> "(" ^ pp_term term ^ ": " ^ pp_term typ ^ ")" +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 H -> "H" | V -> "V" | HV -> "HV" | HOV -> "HOV" + in + sprintf "%sBOX%d%d" kind_string (int_of_bool spacing) (int_of_bool indent) + and pp_layout = function | Sub (t1, t2) -> sprintf "%s \\SUB %s" (pp_term t1) (pp_term t2) | Sup (t1, t2) -> sprintf "%s \\SUP %s" (pp_term t1) (pp_term t2) @@ -130,14 +137,10 @@ and pp_layout = function | Root (arg, index) -> sprintf "\\ROOT %s \\OF %s" (pp_term index) (pp_term arg) (* | Break -> "\\BREAK" *) - | Box (H, terms) -> - sprintf "\\HBOX [%s]" (String.concat " " (List.map pp_term terms)) - | Box (V, terms) -> - sprintf "\\VBOX [%s]" (String.concat " " (List.map pp_term terms)) - | Box (HV, terms) -> - sprintf "\\HVBOX [%s]" (String.concat " " (List.map pp_term terms)) - | Box (HOV, terms) -> - sprintf "\\HOVBOX [%s]" (String.concat " " (List.map pp_term terms)) +(* | Space -> "\\SPACE" *) + | Box (box_spec, terms) -> + sprintf "\\%s [%s]" (pp_box_spec box_spec) + (String.concat " " (List.map pp_term terms)) and pp_magic = function | List0 (t, sep_opt) -> diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index ebe5bf6eb..b898f6d1f 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -36,20 +36,12 @@ let mpres_arrow = Mpresentation.Mo (binder_attributes, "->") (* TODO unicode symbol "to" *) let mpres_implicit = Mpresentation.Mtext ([], "?") -let map_tex use_unicode texcmd = - let default_map_tex = Printf.sprintf "\\%s " in - if use_unicode then - try - Utf8Macro.expand texcmd - with Utf8Macro.Macro_not_found _ -> default_map_tex texcmd - else - default_map_tex texcmd - -let resolve_binder use_unicode = function - | `Lambda -> map_tex use_unicode "lambda" - | `Pi -> map_tex use_unicode "Pi" - | `Forall -> map_tex use_unicode "forall" - | `Exists -> map_tex use_unicode "exists" +let to_unicode s = + try + if s.[0] = '\\' then + Utf8Macro.expand (String.sub s 1 (String.length s - 1)) + else s + with Utf8Macro.Macro_not_found _ -> s let rec make_attributes l1 = function | [] -> [] @@ -73,20 +65,34 @@ let genuine_math = | Mpresentation.Mobject _ -> false | _ -> true -let box_of mathonly kind attrs children = - if mathonly then Mpresentation.Mrow (attrs, children) - else - match kind with - | CicNotationPt.H when List.for_all genuine_math children -> - Mpresentation.Mrow (attrs, children) +let box_of mathonly spec attrs children = + match children with + | [t] -> t + | _ -> + let kind, spacing, indent = spec in + let rec dress = function + | [] -> [] + | [hd] -> [hd] + | hd :: tl -> hd :: Mpresentation.Mtext ([], " ") :: dress tl + in + if mathonly then Mpresentation.Mrow (attrs, dress children) + else + let attrs' = + if spacing then [None, "spacing", "0.5em"] else [] + @ if indent then [None, "indent", "0em 0.5em"] else [] + @ attrs + in + match kind with + | CicNotationPt.H when List.for_all genuine_math children -> + Mpresentation.Mrow (attrs', children) | CicNotationPt.H -> - mpres_of_box (Box.H (attrs, List.map box_of_mpres children)) + mpres_of_box (Box.H (attrs', List.map box_of_mpres children)) | CicNotationPt.V -> - mpres_of_box (Box.V (attrs, List.map box_of_mpres children)) + mpres_of_box (Box.V (attrs', List.map box_of_mpres children)) | CicNotationPt.HV -> - mpres_of_box (Box.HV (attrs, List.map box_of_mpres children)) + mpres_of_box (Box.HV (attrs', List.map box_of_mpres children)) | CicNotationPt.HOV -> - mpres_of_box (Box.HOV (attrs, List.map box_of_mpres children)) + mpres_of_box (Box.HOV (attrs', List.map box_of_mpres children)) let open_paren = Mpresentation.Mo ([], "(") let closed_paren = Mpresentation.Mo ([], ")") @@ -95,8 +101,50 @@ let closed_box_paren = Box.Text ([], ")") type child_pos = [ `Left | `Right | `Inner ] +let pp_assoc = + function + | Gramext.LeftA -> "LeftA" + | Gramext.RightA -> "RightA" + | Gramext.NonA -> "NonA" + +let pp_pos = + function + | `Left -> "`Left" + | `Right -> "`Right" + | `Inner -> "`Inner" + +let is_atomic t = + let module P = Mpresentation in + let rec aux_mpres = function + | P.Mi _ + | P.Mo _ + | P.Mn _ + | P.Ms _ + | P.Mtext _ + | P.Mspace _ -> true + | P.Mobject (_, box) -> aux_box box + | P.Maction (_, [mpres]) + | P.Mrow (_, [mpres]) -> aux_mpres mpres + | _ -> false + and aux_box = function + | Box.Space _ + | Box.Ink _ + | Box.Text _ -> true + | Box.Object (_, mpres) -> aux_mpres mpres + | Box.H (_, [box]) + | Box.V (_, [box]) + | Box.HV (_, [box]) + | Box.HOV (_, [box]) + | Box.Action (_, [box]) -> aux_box box + | _ -> false + in + aux_mpres t + let add_parens child_prec child_assoc child_pos curr_prec t = - if child_prec < curr_prec + prerr_endline (Printf.sprintf "add_parens %d %s %s %d" child_prec + (pp_assoc child_assoc) (pp_pos child_pos) (curr_prec)); + if is_atomic t then t + else if child_prec < curr_prec || (child_prec = curr_prec && child_assoc = Gramext.LeftA && child_pos <> `Left) @@ -146,10 +194,10 @@ let render ids_to_uris t = | A.AttributedTerm (`IdRef xref, t) -> return (invoke mathonly (Some xref) prec assoc t) - | A.Ident (literal, None) -> return (P.Mi (make_href xref, literal)) - | A.Num (literal, _) -> return (P.Mn (make_href xref, literal)) - | A.Symbol (literal, _) -> return (P.Mo (make_href xref, literal)) - | A.Uri (literal, None) -> return (P.Mi (make_href xref, literal)) + | A.Ident (literal, _) -> return (P.Mi (make_href xref, to_unicode literal)) + | A.Num (literal, _) -> return (P.Mn (make_href xref, to_unicode literal)) + | A.Symbol (literal, _) -> return (P.Mo (make_href xref,to_unicode literal)) + | A.Uri (literal, _) -> return (P.Mi (make_href xref, to_unicode literal)) (* default pretty printing shant' be implemented here *) (* | A.Appl terms -> @@ -170,15 +218,17 @@ let render ids_to_uris t = | A.Magic _ | A.Variable _ -> assert false (* should have been instantiated *) - | _ -> assert false + | t -> + prerr_endline (CicNotationPp.pp_term t); + assert false and aux_literal xref prec assoc l = let return t = t, (prec, assoc) in let attrs = make_href xref in match l with | `Symbol s - | `Keyword s -> return (P.Mo (attrs, s)) - | `Number s -> return (P.Mn (attrs, s)) + | `Keyword s -> return (P.Mo (attrs, to_unicode s)) + | `Number s -> return (P.Mn (attrs, to_unicode s)) and aux_layout mathonly xref prec assoc l = let return t = t, (prec, assoc) in let attrs = make_xref xref in @@ -203,11 +253,14 @@ let render ids_to_uris t = [] -> [] | [t] -> let t', (child_prec, child_assoc) = aux mathonly xref prec assoc t in + prerr_endline ("T " ^ CicNotationPp.pp_term t); [add_parens child_prec child_assoc `Right prec t'] | t :: tl -> let t', (child_prec, child_assoc) = aux mathonly xref prec assoc t in + prerr_endline ( "T " ^ CicNotationPp.pp_term t); let child_pos = if first then `Left else `Inner in - add_parens child_prec child_assoc child_pos prec t' :: aux_list false tl + let hd = add_parens child_prec child_assoc child_pos prec t' in + hd :: aux_list false tl in match terms with [t] -> [invoke mathonly xref prec assoc t] @@ -215,3 +268,12 @@ let render ids_to_uris t = in fst (aux false None 0 Gramext.NonA t) +let render_to_boxml id_to_uri t = + let rec print_box (t: CicNotationPres.boxml_markup) = + Box.box2xml print_mpres t + and print_mpres (t: CicNotationPres.mathml_markup) = + Mpresentation.print_mpres print_box t + in + let xml_stream = print_box (box_of_mpres (render id_to_uri t)) in + Ast2pres.add_xml_declaration xml_stream + diff --git a/helm/ocaml/cic_notation/cicNotationPres.mli b/helm/ocaml/cic_notation/cicNotationPres.mli index 3181ec0b8..d7fcb9ea3 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.mli +++ b/helm/ocaml/cic_notation/cicNotationPres.mli @@ -31,3 +31,9 @@ type markup = mathml_markup (** @param ids_to_uris mapping id -> uri for hyperlinking *) val render: (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> markup +val render_to_boxml: + (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> Xml.token Stream.t + +(* val render_to_mathml: + (Cic.id, string) Hashtbl.t -> CicNotationPt.term -> mathml_markup *) + diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 15b9a21ad..c702f5115 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -36,7 +36,6 @@ let loc_of_floc = function | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } -> (loc_begin, loc_end) - type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) @@ -90,6 +89,7 @@ and subst = string * term and case_pattern = string * capture_variable list and box_kind = H | V | HV | HOV +and box_spec = box_kind * bool * bool (* kind, spacing, indent *) and layout_pattern = | Sub of term * term @@ -104,7 +104,7 @@ and layout_pattern = | Sqrt of term | Root of term * term (* argument, index *) (* | Break *) - | Box of box_kind * term list + | Box of box_spec * term list and magic_term = (* level 1 magics *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index 151ec8a08..2f95a5635 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -62,6 +62,7 @@ let constructor_of_inductive_type uri i j = with Not_found -> assert false) module Ast = CicNotationPt +module Parser = CicNotationParser let string_of_name = function | Cic.Name s -> s @@ -71,11 +72,41 @@ let ident_of_name n = Ast.Ident (string_of_name n, None) let idref id t = Ast.AttributedTerm (`IdRef id, t) +let resolve_binder = function + | `Lambda -> "\\lambda" + | `Pi -> "\\Pi" + | `Forall -> "\\forall" + | `Exists -> "\\exists" + let pp_ast0 t k = - prerr_endline "pp_ast0"; - let rec aux t = CicNotationUtil.visit_ast ~special_k k t + let rec aux = function + | Ast.Appl ts -> + Ast.AttributedTerm (`Level (Parser.apply_prec, Parser.apply_assoc), + Ast.Layout (Ast.Box ((Ast.HOV, true, true), List.map k ts))) + | Ast.Binder (`Forall, (Ast.Ident ("_", _), ty), body) + | Ast.Binder (`Pi, (Ast.Ident ("_", _), ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + aux_ty ty; + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol "\\to"); k body]))]))) + | Ast.Binder (binder_kind, (id, ty), body) -> + Ast.AttributedTerm (`Level (Parser.binder_prec, Parser.binder_assoc), + Ast.Layout (Ast.Box ((Ast.HV, false, true), [ + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol (resolve_binder binder_kind)); + k id; + Ast.Literal (`Symbol ":"); + aux_ty ty ])); + Ast.Layout (Ast.Box ((Ast.H, false, false), [ + Ast.Literal (`Symbol "."); + k body ]))]))) + | t -> CicNotationUtil.visit_ast ~special_k k t + and aux_ty = function + | None -> Ast.Literal (`Symbol "?") + | Some ty -> k ty and special_k = function - | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, aux t) + | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, k t) | _ -> assert false in aux t @@ -222,7 +253,6 @@ let set_compiled21 f = compiled21 := Some f let set_compiled32 f = compiled32 := Some f let instantiate21 env precedence associativity l1 = - prerr_endline "instantiate21"; let rec subst_singleton env t = CicNotationUtil.boxify (subst env t) and subst env = function diff --git a/helm/ocaml/cic_notation/cicNotationTag.ml b/helm/ocaml/cic_notation/cicNotationTag.ml index 336f204b7..b454cf24d 100644 --- a/helm/ocaml/cic_notation/cicNotationTag.ml +++ b/helm/ocaml/cic_notation/cicNotationTag.ml @@ -29,7 +29,6 @@ type tag = int type pattern_t = CicNotationPt.term let get_tag term0 = - prerr_endline "get_tag"; let subterms = ref [] in let map_term t = subterms := t :: !subterms ; @@ -42,7 +41,6 @@ let get_tag term0 = in let term_mask = aux term0 in let tag = Hashtbl.hash term_mask in - Printf.printf "TAG = %d\n" tag ; flush stdout ; tag, !subterms let compatible t1 t2 = diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml index e701c5049..964c303ee 100644 --- a/helm/ocaml/cic_notation/cicNotationUtil.ml +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -309,5 +309,5 @@ let string_of_literal = function let boxify = function | [ a ] -> a - | l -> Layout (Box (H, l)) + | l -> Layout (Box ((H, false, false), l)) diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index 0ff7c558e..1585f43e2 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -41,8 +41,7 @@ let dump_xml t id_to_uri fname = print_endline (sprintf "dumping MathML to %s ..." fname); flush stdout; let oc = open_out fname in - let markup = CicNotationPres.render id_to_uri t in - Xml.pp_to_outchan (xml_stream_of_markup markup) oc; + Xml.pp_to_outchan (CicNotationPres.render_to_boxml id_to_uri t) oc; close_out oc let _ = @@ -116,7 +115,7 @@ let _ = let t' = CicNotationRew.pp_ast t in let time4 = Unix.gettimeofday () in printf "pretty printing took %f seconds\n" (time4 -. time3); - dump_xml t id_to_uri "out.xml"; + dump_xml t' id_to_uri "out.xml"; print_endline (CicNotationPp.pp_term t'); flush stdout ) (* CicNotationParser.print_l2_pattern ()) *)