let size1 = countvar c var in
countterm size1 s) current_size l in
countterm size1 t
- | A.Ident(s,None) -> current_size + (String.length s)
- | A.Ident(s,Some l) ->
+ | A.Ident (s,None)
+ | A.Uri (s, None) -> current_size + (String.length s)
+ | A.Ident (s,Some l)
+ | A.Uri (s,Some l) ->
List.fold_left
(fun c (v,t) -> countterm (c + (String.length v)) t)
(current_size + (String.length s)) l
| [] -> box
| _ -> Box.H ([], box :: (List.map (fun t -> Box.Text ([], t)) tail))
+let rec find_symbol idref = function
+ | A.AttributedTerm (`Loc _, t) -> find_symbol None t
+ | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
+ | A.Symbol (name, _) -> `Symbol (name, idref)
+ | _ -> `None
+
let ast2astBox ?(unicode = true) ?(priority = 0) ?(assoc = false) ?(tail = [])
(t, ids_to_uris)
=
| A.AttributedTerm (`IdRef xref, t) -> bigast2box ~xref ~tail t
| A.Appl [] -> assert false
| A.Appl ((hd::tl) as l) ->
- let rec find_symbol idref = function
- | A.AttributedTerm (`Loc _, t) -> find_symbol None t
- | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
- | A.Symbol (name, _) ->
- (match idref with
- | None -> assert false
- | Some idref -> `Symbol (name, idref))
- | _ -> `None
- in
let aattr = make_attributes [Some "helm","xref"] [xref] in
(match find_symbol None hd with
| `Symbol (name, sxref) ->
- let sattr = make_std_attributes (Some sxref) in
+ let sattr = make_std_attributes sxref in
(try
(let f = Hashtbl.find symbol_table_charcount name in
f tl ~unicode ~priority ~assoc ~tail ~ids_to_uris aattr sattr)
Box.smallskip;
Box.Text([],map_tex unicode "Rightarrow");
Box.smallskip;
- Box.Object([],rhs)]) in
- let plbox = match pl with
- [] -> Box.Text([],"[]")
+ append_tail ~tail (Box.Object([],rhs))]) in
+ let plbox =
+ match pl with
+ [] -> append_tail ~tail (Box.Text([],"[]"))
| r::tl ->
Box.V([],
(make_rule ~tail:[] "[" r) ::
(make_args
- (fun ~tail pat -> make_rule ~tail:[] "|" pat)
+ (fun ~tail pat -> make_rule ~tail "|" pat)
~tail:("]" :: tail)
tl))
in
match ty with
| Some ty ->
[ Box.H([],[Box.Text([],"[");
- ast2box ~tail ty;
+ ast2box ~tail:[] ty;
Box.Text([],"]")]) ]
| None -> []
in
Box.V(make_attributes [Some "helm","xref"] [xref],
ty_box @
[Box.Text([],"match");
- Box.indent (Box.H([],[Box.skip; bigast2box ~tail arg]));
+ Box.indent (Box.H([],[Box.skip; bigast2box ~tail:[] arg]));
Box.Text([],"with");
Box.indent plbox])
else
[Box.H(make_attributes [Some "helm","xref"] [xref],
[Box.Text([],"match");
Box.smallskip;
- ast2box ~tail arg;
+ ast2box ~tail:[] arg;
Box.smallskip;
Box.Text([],"with")]);
Box.indent plbox])
let definitions =
let rec make_defs let_txt = function
[] -> []
- | [(var,s,_)] ->
- make_def let_txt var s "in"
+ | [(var,s,_)] -> make_def let_txt var s "in"
| (var,s,_)::tl ->
(make_def let_txt var s "")@(make_defs "and" tl) in
make_defs "let rec" vars in
Box.V(make_attributes [Some "helm","xref"] [xref],
definitions@[ast2box ~tail body])
- | A.Ident (s, subst) ->
+ | A.Ident (s, subst)
+ | A.Uri (s, subst) ->
let subst =
let rec make_substs start_txt =
function
| A.Symbol (name,_) ->
let attr = make_std_attributes xref in
P.Mi (attr,name)
- | A.Ident (name,subst) ->
+ | A.Ident (name,subst)
+ | A.Uri (name,subst) ->
let attr = make_std_attributes xref in
let rec make_subst =
(function
| A.UserInput -> P.Mtext([], "")
| A.Appl [] -> assert false
| A.Appl ((hd::tl) as l) ->
- let rec find_symbol idref = function
- | A.AttributedTerm (`Loc _, t) -> find_symbol None t
- | A.AttributedTerm (`IdRef id, t) -> find_symbol (Some id) t
- | A.Symbol (name, _) ->
- (match idref with
- | None -> assert false
- | Some idref -> `Symbol (name, idref))
- | term ->
- `None
- in
let aattr = make_attributes [Some "helm","xref"] [xref] in
(match find_symbol None hd with
| `Symbol (name, sxref) ->
- let sattr = make_std_attributes (Some sxref) in
+ let sattr = make_std_attributes sxref in
(try
(let f = Hashtbl.find symbol_table name in
f tl ~priority ~assoc ~ids_to_uris aattr sattr)
let lhs =
P.Mtext([], constr) ::
(List.concat
- (List.map (fun var -> P.smallskip :: make_capture_variable var)
+ (List.map
+ (fun var -> P.smallskip :: make_capture_variable var)
vars))
in
lhs @
add_binary_op "times" 70 (`Ascii "*");
add_binary_op "minus" 60 (`Ascii "-");
add_binary_op "div" 60 (`Ascii "/");
+ add_binary_op "cast" 80 (`Ascii ":");