let ann = get_ann i2a id in
match ann with
None -> [<>]
- | Some ann -> (X.xml_nempty "Annotation" ["of", id] (X.xml_cdata ann))
+ | Some ann -> (X.xml_nempty "Annotation" [None,"of", id] (X.xml_cdata ann))
;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let module X = Xml in
let module U = UriManager in
function
- C.ARel (id,_,_) -> print_ann i2a id
- | C.AVar (id,_) -> print_ann i2a id
+ C.ARel (id,_,_,_) -> print_ann i2a id
| C.AMeta (id,_,_) -> print_ann i2a id
| C.ASort (id,_) -> print_ann i2a id
| C.AImplicit _ -> raise NotImplemented
[< print_ann i2a id ;
List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>]
>]
- | C.AConst (id,_,_) -> print_ann i2a id
- | C.AAbst (id,_) -> raise NotImplemented
- | C.AMutInd (id,_,_,_) -> print_ann i2a id
- | C.AMutConstruct (id,_,_,_,_) -> print_ann i2a id
- | C.AMutCase (id,_,_,_,ty,te,patterns) ->
+ | C.AVar (id,_,exp_named_subst)
+ | C.AConst (id,_,exp_named_subst)
+ | C.AMutInd (id,_,_,exp_named_subst)
+ | C.AMutConstruct (id,_,_,_,exp_named_subst) ->
+ [< print_ann i2a id ;
+ List.fold_right
+ (fun (_,x) i -> [< aux x ; i >])
+ exp_named_subst [<>]
+ >]
+ | C.AMutCase (id,_,_,ty,te,patterns) ->
[< print_ann i2a id ;
aux ty ;
aux te ;
| C.AFix (id,_,funs) ->
[< print_ann i2a id ;
List.fold_right
- (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
+ (fun (_,_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
>]
| C.ACoFix (id,no,funs) ->
[< print_ann i2a id ;
List.fold_right
- (fun (_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
+ (fun (_,_,ti,bi) i -> [< aux ti ; aux bi ; i >]) funs [<>]
>]
in
aux
;;
-let print_mutual_inductive_type i2a (_,_,arity,constructors) =
+let print_mutual_inductive_type i2a (_,_,_,arity,constructors) =
[< print_term i2a arity ;
List.fold_right
- (fun (name,ty,_) i -> [< print_term i2a ty ; i >]) constructors [<>]
+ (fun (name,ty) i -> [< print_term i2a ty ; i >]) constructors [<>]
>]
;;
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Annotations SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
X.xml_nempty "Annotations"
- ["of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
+ [None, "of", UriManager.string_of_uri (UriManager.cicuri_of_uri curi)]
begin
match obj with
- C.ADefinition (xid, _, te, ty, _) ->
- [< print_ann i2a xid ; print_term i2a te ; print_term i2a ty >]
- | C.AAxiom (xid, _, ty, _) -> [< print_ann i2a xid ; print_term i2a ty >]
- | C.AVariable (xid, _, bo, ty) ->
+ C.AConstant (xid, xidobj, _, te, ty, _, _) ->
+ [< print_ann i2a xid ;
+ (match xidobj,te with
+ Some xidobj, Some te ->
+ [< print_ann i2a xidobj ;
+ print_term i2a te
+ >]
+ | None, None -> [<>]
+ | _,_ -> assert false
+ ) ;
+ print_term i2a ty
+ >]
+ | C.AVariable (xid, _, bo, ty,_, _) ->
[< print_ann i2a xid ;
(match bo with
None -> [<>]
) ;
print_term i2a ty
>]
- | C.ACurrentProof (xid, _, conjs, bo, ty) ->
+ | C.ACurrentProof (xid, xidobj, _, conjs, bo, ty,_, _) ->
[< print_ann i2a xid ;
+ print_ann i2a xidobj ;
List.fold_right
(fun (cid, _, context, t) i ->
[< print_ann i2a cid ;
print_term i2a bo ;
print_term i2a ty
>]
- | C.AInductiveDefinition (xid, tys, params, paramsno) ->
+ | C.AInductiveDefinition (xid, tys, params, paramsno, _) ->
[< print_ann i2a xid ;
List.fold_right
(fun x i -> [< print_mutual_inductive_type i2a x ; i >])