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
| A.Num (s, _) -> current_size + String.length s
| A.Sort _ -> current_size + 4 (* sort name *)
| A.Symbol (s,_) -> current_size + String.length s
+
+ | A.UserInput -> current_size
;;
let is_big t =
| [] -> 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
[] -> []
| [(s,t)] ->
- make_subst start_txt s t "]"
+ make_subst start_txt s t ""
| (s,t)::tl ->
- (make_subst start_txt s t ";")@(make_substs " " tl)
+ (make_subst start_txt s t ";")@(make_substs "" tl)
in
match subst with
- | Some subst -> make_substs ((map_tex unicode "subst") ^ "[") subst
- | None -> []
+ | Some subst ->
+ Box.H([],
+ [Box.Text(make_std_attributes xref,s);
+ Box.Action([],
+ [Box.Text([],"[...]");
+ Box.H([], [Box.Text([], map_tex unicode "subst" ^ "[");
+ Box.V([], make_substs "" subst);
+ Box.Text([], "]")])])])
+ | None -> Box.Text(make_std_attributes xref, s)
in
- Box.V([], (* attr here or on Vbox? *)
+ subst
+ (*
+ Box.H([], (* attr here or on Vbox? *)
[Box.Text(make_std_attributes xref,s);
- Box.indent(Box.V([],subst))])
+ Box.Action([], [Box.Text([], "[_]"); Box.V([],subst)])])
+ (* Box.indent(Box.V([],subst))]) *)
+ *)
| A.Implicit ->
Box.Text([],"_") (* big? *)
| A.Meta (n, l) ->
| A.Symbol (s, _) ->
Box.Text([],s)
+ | A.UserInput -> Box.Text([],"")
+
and aux_option ~tail = function
None -> Box.Text([],"_")
| Some ast -> ast2box ~tail ast
and make_subst start_txt varname body end_txt =
pretty_append ~tail:[end_txt]
- [Box.Text([],start_txt);
- Box.Text([],varname);
- Box.smallskip;
- Box.Text([],map_tex unicode "Assign")
- ]
+ ((if start_txt <> "" then [Box.Text([],start_txt)] else [])@
+ [Box.Text([],varname);
+ Box.smallskip;
+ Box.Text([],map_tex unicode "Assign")
+ ])
body
and pretty_append ~tail l ast =
| 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.Sort `Type -> P.Mtext ([], "Type")
| A.Sort `CProp -> P.Mtext ([], "CProp")
| A.Implicit -> P.Mtext([], "?")
+ | 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 ":");