+let ppty current_module_uri =
+ (* nparams is the number of left arguments
+ left arguments should either become parameters or be skipped altogether *)
+ let rec args nparams context =
+ function
+ Cic.Prod (n,s,t) ->
+ let n =
+ match n with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name n -> Cic.Name (String.uncapitalize n)
+ in
+ (match analyze_type context s with
+ | `Optimize
+ | `Statement
+ | `Sort Cic.Prop ->
+ args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+ | `Type when nparams > 0 ->
+ args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+ | `Type ->
+ let abstr,args =
+ args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
+ abstr,pp ~in_type:true current_module_uri s context::args
+ | `Sort _ when nparams <= 0 ->
+ let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in
+ args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+ | `Sort _ ->
+ let n =
+ match n with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name name -> Cic.Name ("'" ^ name) in
+ let abstr,args =
+ args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+ in
+ (match n with
+ Cic.Anonymous -> abstr
+ | Cic.Name name -> name::abstr),
+ args)
+ | _ -> [],[]
+ in
+ args
+;;
+
+exception DoNotExtract;;
+
+let pp_abstracted_ty current_module_uri =
+ let rec args context =
+ function
+ Cic.Lambda (n,s,t) ->
+ let n =
+ match n with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name n -> Cic.Name (String.uncapitalize n)
+ in
+ (match analyze_type context s with
+ | `Optimize
+ | `Statement
+ | `Type
+ | `Sort Cic.Prop ->
+ args ((Some (n,Cic.Decl s))::context) t
+ | `Sort _ ->
+ let n =
+ match n with
+ Cic.Anonymous -> Cic.Anonymous
+ | Cic.Name name -> Cic.Name ("'" ^ name) in
+ let abstr,res =
+ args ((Some (n,Cic.Decl s))::context) t
+ in
+ (match n with
+ Cic.Anonymous -> abstr
+ | Cic.Name name -> name::abstr),
+ res)
+ | ty ->
+ match analyze_type context ty with
+ | `Optimize ->
+ prerr_endline "XXX abstracted l2 ty"; assert false
+ | `Sort _
+ | `Statement -> raise DoNotExtract
+ | `Type ->
+ (* BUG HERE: this can be a real System F type *)
+ let head = pp ~in_type:true current_module_uri ty context in
+ [],head
+ in
+ args
+;;
+
+