| Unit -> 1
| Top -> 1
| TConst c -> 1
- | Arrow (l, r) -> 1 + size_of_type l + size_of_type r
+ | Arrow _ -> 2
| Skip t -> size_of_type t
- | Forall (name, kind, typ) -> 1 + size_of_type typ
- | TAppl l -> List.fold_right (+) (List.map size_of_type l) 0
+ | Forall _ -> 2
+ | TAppl l -> 1
;;
type term =
| TermDeclaration of term_former_decl
| TermDefinition of term_former_def
| LetRec of obj_kind list
- | Algebraic of (string * typ_context * (string * typ) list) list
+ (* name, left, right, constructors *)
+ | Algebraic of (string * typ_context * typ_context * (string * typ) list) list
type obj = NUri.uri * obj_kind
| `Kind ->
let arity = kind_of status ~metasenv [] arity in
let ctx,_ = split_kind_prods [] arity in
+ let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
let ref =
NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
let status =
name,ty
) cl
in
- status,i+1,(name,ctx,cl)::res
+ status,i+1,(name,left,right,cl)::res
) (status,0,[]) il
in
match rev_tyl with
let name = if name = "" then "a" else name in
name @::: l
else if List.mem name l then (name ^ "'") @::: l
- else name,l
+ else if name="" then "[erased]",l else name,l
;;
let (@::) x l = let x,l = x @::: l in x::l;;
let rec pp_obj status (uri,obj_kind) =
let pretty_print_context ctx =
- String.concat " " (List.rev
+ String.concat " " (List.rev (snd
(List.fold_right
- (fun (x,kind) l ->
+ (fun (x,kind) (l,res) ->
let x,l = x @:::l in
if size_of_kind kind > 1 then
- ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l
+ x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
else
- x::l)
- (HExtlib.filter_map (fun x -> x) ctx) []))
+ x::l,x::res)
+ (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
in
let namectx_of_ctx ctx =
List.fold_right (@::)
| Algebraic il ->
String.concat "\n"
(List.map
- (fun _name,ctx,cl ->
+ (fun _name,left,right,cl ->
(*CSC: BUG always uses the name of the URI *)
- "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " where\n " ^
+ "data " ^ name_of_uri `TypeName uri ^ " " ^
+ pretty_print_context (right@left) ^ " where\n " ^
String.concat "\n " (List.map
(fun name,tys ->
- let namectx = namectx_of_ctx ctx in
+ let namectx = namectx_of_ctx left in
capitalize `Constructor name ^ " :: " ^
pretty_print_type status namectx tys
) cl