;;
(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
+(* It takes in input a hash table mapping ids to annotations, an annotated
+term, and gives back a Xml.token Stream.t representing the .ann file *)
let print_term i2a =
let rec aux =
let module C = Cic in
function
C.ARel (id,_,_) -> print_ann i2a id
| C.AVar (id,_) -> print_ann i2a id
- | C.AMeta (id,_) -> print_ann i2a id
+ | C.AMeta (id,_,_) -> print_ann i2a id
| C.ASort (id,_) -> print_ann i2a id
| C.AImplicit _ -> raise NotImplemented
| C.AProd (id,_,s,t) -> [< print_ann i2a id ; aux s ; aux t >]
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.ACurrentProof (xid, _, conjs, bo, ty) ->
[< print_ann i2a xid ;
List.fold_right
- (fun (_,t) i -> [< print_term i2a t ; i >])
- conjs [<>] ;
+ (fun (cid, _, context, t) i ->
+ [< print_ann i2a cid ;
+ List.fold_right
+ (fun (hid,context_entry) i ->
+ [<print_ann i2a hid ;
+ (match context_entry with
+ Some (_,C.ADecl at) -> print_term i2a at
+ | Some (_,C.ADef at) -> print_term i2a at
+ | None -> [< >]
+ ) ; i
+ >]
+ ) context [< >];
+ print_term i2a t ; i
+ >]
+ ) conjs [<>] ;
print_term i2a bo ;
print_term i2a ty
>]
end
>]
;;
+
+
+