- bugfixes here and there ...
- precedence still need to be fixed
cicNotationPp.mli \
cicNotationMatcher.mli \
cicNotationFwd.mli \
- cicNotationRew.mli \
cicNotationParser.mli \
+ cicNotationRew.mli \
cicNotationPres.mli \
$(NULL)
IMPLEMENTATION_FILES = \
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
| 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
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) ->
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 =
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"
| 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 ->
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 *)
| 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)
| 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) ->
(* 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
| [] -> []
| 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 ([], ")")
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)
| 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 ->
| 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
[] -> []
| [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]
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
+
(** @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 *)
+
| { 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 *)
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
| 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 *)
with Not_found -> assert false)
module Ast = CicNotationPt
+module Parser = CicNotationParser
let string_of_name = function
| Cic.Name s -> s
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
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
type pattern_t = CicNotationPt.term
let get_tag term0 =
- prerr_endline "get_tag";
let subterms = ref [] in
let map_term t =
subterms := t :: !subterms ;
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 =
let boxify = function
| [ a ] -> a
- | l -> Layout (Box (H, l))
+ | l -> Layout (Box ((H, false, false), l))
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 _ =
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 ()) *)
projects / helm.git / commitdiff