add_xml_attrs (RenderingAttrs.builtin_symbol_attributes `MathML)
(builtin_symbol s)
-let string_of_sort_kind = function
- | `Prop -> "Prop"
- | `Set -> "Set"
- | `CProp _ -> "CProp"
- | `Type _ -> "Type"
- | `NType s -> "Type[" ^ s ^ "]"
+let xml_of_sort x =
+ let to_string x = Ast.Ident (x, None) in
+ let identify x =
+ add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
+ in
+ let lvl t = Ast.AttributedTerm (`Level 90,t) in
+ match x with
+ | `Prop -> identify "Prop"
+ | `Set -> identify "Set"
+ | `CProp _ -> identify "CProp"
+ | `Type _ -> identify "Type"
+ | `NType s -> lvl(Ast.Layout (Ast.Sub (identify "Type",to_string s)))
+ | `NCProp s -> lvl(Ast.Layout (Ast.Sub (identify "CProp",to_string s)))
+;;
+
let map_space f l =
HExtlib.list_concat
(fun (params, name, ty, body, rec_param) ->
[ break;
hvbox false true ([
- keyword "and";
+ keyword "and"; space;
name] @
params @
[space; keyword "on" ; space; rec_param ;space ] @
((hvbox false false
(fst_row :: List.flatten tl_rows
@ [ break; keyword "in"; break; k where ])))
- | Ast.Implicit -> builtin_symbol "?"
+ | Ast.Implicit `JustOne -> builtin_symbol "?"
+ | Ast.Implicit `Vector -> builtin_symbol "…"
| Ast.Meta (n, l) ->
let local_context l =
List.map (function None -> None | Some t -> Some (k t)) l
| Ast.Literal _
| Ast.UserInput as leaf -> leaf
| t -> CicNotationUtil.visit_ast ~special_k k t
- and aux_sort sort_kind =
- add_xml_attrs (RenderingAttrs.keyword_attributes `MathML)
- (Ast.Ident (string_of_sort_kind sort_kind, None))
+ and aux_sort sort_kind = xml_of_sort sort_kind
and aux_ty = function
| None -> builtin_symbol "?"
| Some ty -> k ty
aux ((name, (ty, v)) :: acc) tl
| Env.TermType _, Env.TermValue _ ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType _, Env.OptValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl
| Env.TermType _, Env.TermValue _ ->
aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType _, Env.OptValue _ ->
+ aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
| binding :: tl -> aux (binding :: acc) tl
| [] -> acc
Ast.Ident (name, Some (aux_substs env substs))
| Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
- | Ast.Implicit
+ | Ast.Implicit _
| Ast.Ident _
| Ast.Num _
| Ast.Sort _