- [] -> Box.Text([],constr)
- | vars ->
- let bvars =
- List.fold_right
- (fun var acc ->
- let bv =
- match var with
- (* ignoring the type *)
- (Cic.Anonymous, _) -> Box.Text([],"_")
- | (Cic.Name s, _) -> Box.Text([],s) in
- Box.Text([]," ")::bv::acc) vars [Box.Text([],")")] in
- Box.H([],Box.Text([],"(")::Box.Text([],constr)::bvars)
-
-
-and make_def let_txt var def end_txt =
- let name =
- (match var with
- (* ignoring the type *)
- (Cic.Anonymous, _) -> Box.Text([],"_")
- | (Cic.Name s, _) -> Box.Text([],s)) in
- pretty_append
- [Box.Text([],let_txt);
- Box.smallskip;
- name;
- Box.smallskip;
- Box.Text([],"=")
- ]
- def
- [Box.smallskip;Box.Text([],end_txt)]
-
-and make_subst start_txt varname body end_txt =
- pretty_append
- [Box.Text([],start_txt);
- Box.Text([],varname);
- Box.smallskip;
- Box.Text([],":=")
- ]
- body
- [Box.Text([],end_txt)]
-
-and pretty_append l ast tail =
- if is_big ast then
- [Box.H([],l);
- Box.H([],Box.skip::(bigast2box ast)::tail)]
- else
- [Box.H([],l@(Box.smallskip::(ast2box ast)::tail))]
+ | A.AttributedTerm (`Loc _, ast) -> aux ?xref ast
+ | A.AttributedTerm (`IdRef xref, ast) -> aux ~xref ast
+ | A.Symbol (name,_) ->
+ let attr = make_std_attributes xref in
+ P.Mi (attr,name)
+ | A.Ident (name,subst)
+ | A.Uri (name,subst) ->
+ let attr = make_std_attributes xref in
+ let rec make_subst =
+ (function
+ [] -> []
+ | (n,a)::tl ->
+ (aux a)::
+ P.Mtext([],"/")::
+ P.Mi([],n)::
+ P.Mtext([],"; ")::
+ P.smallskip::
+ (make_subst tl)) in
+ let subst =
+ match subst with
+ | None -> []
+ | Some subst -> make_subst subst
+ in
+ (match subst with
+ | [] -> P.Mi (attr, name)
+ | _ ->
+ P.Mrow ([],
+ P.Mi (attr,name)::
+ P.Mtext([],"[")::
+ subst @
+ [(P.Mtext([],"]"))]))
+ | A.Meta (no,l) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ let l' =
+ List.map
+ (function
+ None -> P.Mo([],"_")
+ | Some t -> aux t
+ ) l
+ in
+ P.Mrow ([],P.Mi (attr,"?" ^ string_of_int no) :: P.Mo ([],"[") ::
+ l' @ [P.Mo ([],"]")])
+ | A.Num (value, _) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ P.Mn (attr,value)
+ | A.Sort `Prop -> P.Mtext ([], "Prop")
+ | A.Sort `Set -> P.Mtext ([], "Set")
+ | 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 aattr = make_attributes [Some "helm","xref"] [xref] in
+ (match find_symbol None hd with
+ | `Symbol (name, sxref) ->
+ 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)
+ with Not_found ->
+ P.Mrow(aattr,
+ m_open_fence :: P.Mi(sattr,name)::(make_args tl) @
+ [m_close_fence]))
+ | `None ->
+ P.Mrow(aattr, m_open_fence :: (aux hd) :: (make_args tl) @
+ [m_close_fence]))
+ | A.Binder (`Pi, (Cic.Anonymous, Some ty), body)
+ | A.Binder (`Forall, (Cic.Anonymous, Some ty), body) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ P.Mrow (attr, [
+ aux ty;
+ P.Mtext ([], map_tex true "to");
+ aux body])
+ | A.Binder (kind,var,body) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ let binder = resolve_binder true kind in
+ let var = make_capture_variable var in
+ P.Mrow (attr,
+ P.Mtext([None,"mathcolor","blue"],binder) :: var @
+ [P.Mo([],"."); aux body])
+ | A.LetIn (var,s,body) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ P.Mrow (attr,
+ P.Mtext([],("let ")) ::
+ (make_capture_variable var @
+ P.Mtext([],("="))::
+ (aux s)::
+ P.Mtext([]," in ")::
+ [aux body]))
+ | A.LetRec (_, defs, body) ->
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ let rec make_defs =
+ (function
+ [] -> assert false
+ | [(var,body,_)] ->
+ make_capture_variable var @ [P.Mtext([],"=");(aux body)]
+ | (var,body,_)::tl ->
+ make_capture_variable var @
+ (P.Mtext([],"=")::
+ (aux body)::P.Mtext([]," and")::(make_defs tl))) in
+ P.Mrow (attr,
+ P.Mtext([],("let rec "))::
+ (make_defs defs)@
+ (P.Mtext([]," in ")::
+ [aux body]))
+ | A.Case (arg,_,outtype,patterns) ->
+ (* TODO print outtype *)
+ let attr = make_attributes [Some "helm","xref"] [xref] in
+ let rec make_patterns =
+ (function
+ [] -> []
+ | [(constr, vars),rhs] -> make_pattern constr vars rhs
+ | ((constr,vars), rhs)::tl ->
+ (make_pattern constr vars rhs)@(P.smallskip::
+ P.Mtext([],"|")::P.smallskip::(make_patterns tl)))
+ and make_pattern constr vars rhs =
+ let lhs =
+ P.Mtext([], constr) ::
+ (List.concat
+ (List.map
+ (fun var -> P.smallskip :: make_capture_variable var)
+ vars))
+ in
+ lhs @
+ [P.smallskip; P.Mtext([],map_tex true "to"); P.smallskip; aux rhs]
+ in
+ P.Mrow (attr,
+ P.Mtext([],"match")::P.smallskip::
+ (aux arg)::P.smallskip::
+ P.Mtext([],"with")::P.smallskip::
+ P.Mtext([],"[")::P.smallskip::
+ (make_patterns patterns)@(P.smallskip::[P.Mtext([],("]"))]))
+
+ and make_capture_variable (name, ty) =
+ let name =
+ match name with
+ | Cic.Anonymous -> [P.Mtext([], "_")]
+ | Cic.Name s -> [P.Mtext([], s)]
+ in
+ let ty =
+ match ty with
+ | None -> []
+ | Some ty -> [P.Mtext([],":"); aux ty]
+ in
+ name @ ty