- | C.ALambda (id,C.Anonimous,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts id in
- X.xml_nempty "LAMBDA" ["id",id ; "sort",sort]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" [] (aux t)
- >]
- | C.ALambda (xid,C.Name id,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts xid in
- X.xml_nempty "LAMBDA" ["id",xid ; "sort",sort]
- [< X.xml_nempty "source" [] (aux s) ;
- X.xml_nempty "target" ["binder",id] (aux t)
- >]
- | C.ALetIn (xid,C.Anonimous,s,t) ->
- assert false (*CSC: significa che e' sbagliato il tipo di LetIn!!!*)
- | C.ALetIn (xid,C.Name id,s,t) ->
- let sort = Hashtbl.find ids_to_inner_sorts xid in
- X.xml_nempty "LETIN" ["id",xid ; "sort",sort]
- [< X.xml_nempty "term" [] (aux s) ;
- X.xml_nempty "letintarget" ["binder",id] (aux t)
- >]
+ | C.ALambda (last_id,_,_,_) as lambdas ->
+ let rec eat_lambdas =
+ function
+ C.ALambda (id,n,s,t) ->
+ let lambdas,t' = eat_lambdas t in
+ (id,n,s)::lambdas,t'
+ | t -> [],t
+ in
+ let lambdas,t = eat_lambdas lambdas in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LAMBDA" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("type",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "decl" attrs (aux s) >]
+ ) [< >] lambdas ;
+ X.xml_nempty "target" [] (aux t)
+ >]
+ | C.ALetIn (xid,C.Anonymous,s,t) ->
+ assert false
+ | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ let rec eat_letins =
+ function
+ C.ALetIn (id,n,s,t) ->
+ let letins,t' = eat_letins t in
+ (id,n,s)::letins,t'
+ | t -> [],t
+ in
+ let letins,t = eat_letins letins in
+ let sort = Hashtbl.find ids_to_inner_sorts last_id in
+ X.xml_nempty "LETIN" ["sort",sort]
+ [< List.fold_left
+ (fun i (id,binder,s) ->
+ let sort = Hashtbl.find ids_to_inner_sorts id in
+ let attrs =
+ ("id",id)::("sort",sort)::
+ match binder with
+ C.Anonymous -> []
+ | C.Name b -> ["binder",b]
+ in
+ [< i ; X.xml_nempty "def" attrs (aux s) >]
+ ) [< >] letins ;
+ X.xml_nempty "target" [] (aux t)
+ >]