- | `Statement -> pp t ((Some (b,Cic.Decl s))::context)
- | `Type -> "(function " ^ ppname b ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")")
- | C.LetIn (b,s,t) ->
- let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
- "(let " ^ ppname b ^ " = " ^ pp s context ^ " in " ^ pp t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
- | C.Appl (C.MutConstruct _ as he::tl) ->
- let hes = pp he context in
- let stl = String.concat "," (clean_args context tl) in
+ | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
+ | `Optimize -> prerr_endline "XXX lambda";assert false
+ | `Type ->
+ "(function " ^ ppname b ^ " -> " ^
+ pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
+ | C.LetIn (b,s,ty,t) ->
+ (match analyze_term context s with
+ | `Type
+ | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context)
+ | `Optimize
+ | `Term ->
+ "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*)
+ " = " ^ pp ~in_type:false s context ^ " in " ^
+ pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")")
+ | C.Appl (he::tl) when in_type ->
+ let hes = pp ~in_type he context in
+ let stl = String.concat "," (clean_args_for_ty context tl) in
+ (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
+ | C.Appl (C.MutInd _ as he::tl) ->
+ let hes = pp ~in_type he context in
+ let stl = String.concat "," (clean_args_for_ty context tl) in
+ (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
+ | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
+ let nparams =
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (_,_,nparams,_) -> nparams
+ | _ -> assert false in
+ let hes = pp ~in_type he context in
+ let stl = String.concat "," (clean_args_for_constr nparams context tl) in