diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 418 |
1 files changed, 301 insertions, 117 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 57028469..401ef7fe 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -6,7 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: prettyp.ml 9314 2006-10-29 20:11:08Z herbelin $ *) +(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu> + * on May-June 2006 for implementation of abstraction of pretty-printing of objects. + *) + +(* $Id: prettyp.ml 10971 2008-05-22 17:12:11Z barras $ *) open Pp open Util @@ -29,6 +33,24 @@ open Libnames open Nametab open Recordops +type object_pr = { + print_inductive : mutual_inductive -> std_ppcmds; + print_constant_with_infos : constant -> std_ppcmds; + print_section_variable : variable -> std_ppcmds; + print_syntactic_def : kernel_name -> std_ppcmds; + print_module : bool -> Names.module_path -> std_ppcmds; + print_modtype : module_path -> std_ppcmds; + print_named_decl : identifier * constr option * types -> std_ppcmds; + print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; + print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; + print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; + print_typed_value_in_env : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds; +} + +let gallina_print_module = print_module +let gallina_print_modtype = print_modtype + (*********************) (** Basic printing *) @@ -36,29 +58,29 @@ let print_basename sp = pr_global (ConstRef sp) let print_closed_sections = ref false +let with_line_skip p = if ismt p then mt() else (fnl () ++ p) + (********************************) (** Printing implicit arguments *) -let print_impl_args_by_pos = function - | [] -> mt () - | [i] -> str"Position [" ++ int i ++ str"] is implicit" ++ fnl() - | l -> - str"Positions [" ++ - prlist_with_sep (fun () -> str "; ") int l ++ - str"] are implicit" ++ fnl() +let conjugate_to_be = function [_] -> "is" | _ -> "are" -let print_impl_args_by_name = function +let pr_implicit imp = pr_id (name_of_implicit imp) + +let print_impl_args_by_name max = function | [] -> mt () - | [i] -> str"Argument " ++ pr_id (name_of_implicit i) ++ str" is implicit" ++ - fnl() - | l -> - str"Arguments " ++ - prlist_with_sep (fun () -> str ", ") - (fun imp -> pr_id (name_of_implicit imp)) l ++ - str" are implicit" ++ fnl() + | impls -> + hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ + prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ + str (conjugate_to_be impls) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt())) ++ fnl() let print_impl_args l = - print_impl_args_by_name (List.filter is_status_implicit l) + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = list_subtract imps maximps in + print_impl_args_by_name false nonmaximps ++ + print_impl_args_by_name true maximps (*********************) (** Printing Scopes *) @@ -90,16 +112,17 @@ let need_expansion impl ref = type opacity = | FullyOpaque - | TransparentMaybeOpacified of bool + | TransparentMaybeOpacified of Conv_oracle.level let opacity env = function | VarRef v when pi2 (Environ.lookup_named v env) <> None -> - Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_var v)) + Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(VarKey v))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in if cb.const_body = None then None else if cb.const_opaque then Some FullyOpaque - else Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_cst cst)) + else Some + (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst))) | _ -> None let print_opacity ref = @@ -108,8 +131,14 @@ let print_opacity ref = | Some s -> pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" - | TransparentMaybeOpacified true -> "basically transparent but considered opaque for reduction" - | TransparentMaybeOpacified false -> "transparent") ++ fnl() + | TransparentMaybeOpacified Conv_oracle.Opaque -> + "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified lev when lev = Conv_oracle.transparent -> + "transparent" + | TransparentMaybeOpacified (Conv_oracle.Level n) -> + "transparent (with expansion weight "^string_of_int n^")" + | TransparentMaybeOpacified Conv_oracle.Expand -> + "transparent (with minimal expansion weight)") ++ fnl() let print_name_infos ref = let impl = implicits_of_global ref in @@ -120,12 +149,7 @@ let print_name_infos ref = str "Expanded type for implicit arguments" ++ fnl () ++ print_ref true ref ++ fnl() else mt() in - (if (List.filter is_status_implicit impl<>[]) - or not (List.for_all ((=) None) scopes) - then fnl() - else mt()) - ++ type_for_implicit - ++ print_impl_args impl ++ print_argument_scopes scopes + type_for_implicit ++ print_impl_args impl ++ print_argument_scopes scopes let print_id_args_data test pr id l = if List.exists test l then @@ -158,7 +182,7 @@ type logical_name = | Term of global_reference | Dir of global_dir_reference | Syntactic of kernel_name - | ModuleType of qualid * kernel_name + | ModuleType of qualid * module_path | Undefined of qualid let locate_any_name ref = @@ -223,21 +247,12 @@ let print_located_qualid ref = (******************************************) (**** Printing declarations and judgments *) +(**** Gallina layer *****) -let print_typed_value_in_env env (trm,typ) = +let gallina_print_typed_value_in_env env (trm,typ) = (pr_lconstr_env env trm ++ fnl () ++ str " : " ++ pr_ltype_env env typ ++ fnl ()) -let print_typed_value x = print_typed_value_in_env (Global.env ()) x - -let print_judgment env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, typ) - -let print_safe_judgment env j = - let trm = Safe_typing.j_val j in - let typ = Safe_typing.j_type j in - print_typed_value_in_env env (trm, typ) - (* To be improved; the type should be used to provide the types in the abstractions. This should be done recursively inside pr_lconstr, so that the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) @@ -250,12 +265,12 @@ let print_named_def name body typ = (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ - str "]" ++ fnl ()) + str "]") let print_named_assum name typ = - (str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" ++ fnl ()) + str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" -let print_named_decl (id,c,typ) = +let gallina_print_named_decl (id,c,typ) = let s = string_of_id id in match c with | Some body -> print_named_def s body typ @@ -307,28 +322,64 @@ let pr_mutual_inductive finite indl = hov 0 ( str (if finite then "Inductive " else "CoInductive ") ++ prlist_with_sep (fun () -> fnl () ++ str" with ") - print_one_inductive indl) ++ - fnl () + print_one_inductive indl) + +let get_fields = + let rec prodec_rec l subst c = + match kind_of_term c with + | Prod (na,t,c) -> + let id = match na with Name id -> id | Anonymous -> id_of_string "_" in + prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c + | LetIn (na,b,_,c) -> + let id = match na with Name id -> id | Anonymous -> id_of_string "_" in + prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c + | _ -> List.rev l + in + prodec_rec [] [] -let print_mutual sp = +let pr_record (sp,tyi) = + let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in + let env = Global.env () in + let envpar = push_rel_context params env in + let fields = get_fields cstrtypes.(0) in + hov 0 ( + hov 0 ( + str "Record " ++ pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ + print_params env params ++ + str ": " ++ pr_lconstr_env envpar arity ++ brk(1,2) ++ + str ":= " ++ pr_id cstrnames.(0)) ++ + brk(1,2) ++ + hv 2 (str "{ " ++ + prlist_with_sep (fun () -> str "; " ++ brk(1,0)) + (fun (id,b,c) -> + pr_id id ++ str (if b then " : " else " := ") ++ + pr_lconstr_env envpar c) fields) ++ str" }") + +let gallina_print_inductive sp = let (mib,mip) = Global.lookup_inductive (sp,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in - pr_mutual_inductive mib.mind_finite names ++ - print_inductive_implicit_args sp mipv ++ - print_inductive_argument_scopes sp mipv + (if mib.mind_record & not !Flags.raw_print then + pr_record (List.hd names) + else + pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ + with_line_skip + (print_inductive_implicit_args sp mipv ++ + print_inductive_argument_scopes sp mipv) + +let print_named_decl id = + gallina_print_named_decl (Global.lookup_named id) ++ fnl () -let print_section_variable sp = - let d = get_variable sp in - print_named_decl d ++ - print_name_infos (VarRef sp) +let gallina_print_section_variable id = + print_named_decl id ++ + with_line_skip (print_name_infos (VarRef id)) let print_body = function | Some lc -> pr_lconstr (Declarations.force lc) | None -> (str"<no body>") let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) + (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ) let ungeneralized_type_of_constant_type = function | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) @@ -343,84 +394,190 @@ let print_constant with_values sep sp = | None -> str"*** [ " ++ print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ - str" ]" ++ fnl () + str" ]" | _ -> print_basename sp ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else pr_ltype typ) ++ - fnl ()) - -let print_constant_with_infos sp = - print_constant true " = " sp ++ print_name_infos (ConstRef sp) - -let print_inductive sp = (print_mutual sp) - -let print_syntactic_def sep kn = - let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in - let c = Syntax_def.search_syntactic_definition dummy_loc kn in - str "Notation " ++ pr_qualid qid ++ str sep ++ + (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)) + ++ fnl () + +let gallina_print_constant_with_infos sp = + print_constant true " = " sp ++ + with_line_skip (print_name_infos (ConstRef sp)) + +let gallina_print_syntactic_def kn = + let sep = " := " + and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn + and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in + let c = Topconstr.rawconstr_of_aconstr dummy_loc a in + str "Notation " ++ pr_qualid qid ++ + prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++ Constrextern.without_symbols pr_lrawconstr c ++ fnl () -let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = - let tag = object_tag lobj in - match (oname,tag) with - | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes - constraints *) - (try Some(print_section_variable (basename sp)) with Not_found -> None) - | (_,"CONSTANT") -> - Some (print_constant with_values sep (constant_of_kn kn)) - | (_,"INDUCTIVE") -> - Some (print_inductive kn) - | (_,"MODULE") -> - let (mp,_,l) = repr_kn kn in - Some (print_module with_values (MPdot (mp,l))) - | (_,"MODULE TYPE") -> - Some (print_modtype kn) - | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None - (* To deal with forgotten cases... *) - | (_,s) -> None -(* - | (_,s) -> - (str(string_of_path sp) ++ str" : " ++ - str"Unrecognized object " ++ str s ++ fnl ()) -*) - -let rec print_library_entry with_values ent = - let sep = if with_values then " = " else " : " in +let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = + let sep = if with_values then " = " else " : " + and tag = object_tag lobj in + match (oname,tag) with + | (_,"VARIABLE") -> + (* Outside sections, VARIABLES still exist but only with universes + constraints *) + (try Some(print_named_decl (basename sp)) with Not_found -> None) + | (_,"CONSTANT") -> + Some (print_constant with_values sep (constant_of_kn kn)) + | (_,"INDUCTIVE") -> + Some (gallina_print_inductive kn) + | (_,"MODULE") -> + let (mp,_,l) = repr_kn kn in + Some (print_module with_values (MPdot (mp,l))) + | (_,"MODULE TYPE") -> + let (mp,_,l) = repr_kn kn in + Some (print_modtype (MPdot (mp,l))) + | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + (* To deal with forgotten cases... *) + | (_,s) -> None + +let gallina_print_library_entry with_values ent = let pr_name (sp,_) = pr_id (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - print_leaf_entry with_values sep (oname,lobj) + gallina_print_leaf_entry with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection) -> + | (oname,Lib.ClosedSection _) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> Some (str " >>>>>>> Library " ++ pr_dirpath dir) | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) + | (oname,Lib.ClosedModule _) -> + Some (str " >>>>>>> Closed Module " ++ pr_name oname) | (oname,Lib.OpenedModtype _) -> Some (str " >>>>>>> Module Type " ++ pr_name oname) + | (oname,Lib.ClosedModtype _) -> + Some (str " >>>>>>> Closed Module Type " ++ pr_name oname) | (_,Lib.FrozenState _) -> None - -let print_context with_values = + +let gallina_print_leaf_entry with_values c = + match gallina_print_leaf_entry with_values c with + | None -> mt () + | Some pp -> pp ++ fnl() + +let gallina_print_context with_values = let rec prec n = function - | h::rest when n = None or out_some n > 0 -> - (match print_library_entry with_values h with + | h::rest when n = None or Option.get n > 0 -> + (match gallina_print_library_entry with_values h with | None -> prec n rest - | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ()) + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec +let gallina_print_eval red_fun env evmap _ {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env evmap trm in + (str " = " ++ gallina_print_typed_value_in_env env (ntrm,typ)) + +(******************************************) +(**** Printing abstraction layer *) + +let default_object_pr = { + print_inductive = gallina_print_inductive; + print_constant_with_infos = gallina_print_constant_with_infos; + print_section_variable = gallina_print_section_variable; + print_syntactic_def = gallina_print_syntactic_def; + print_module = gallina_print_module; + print_modtype = gallina_print_modtype; + print_named_decl = gallina_print_named_decl; + print_leaf_entry = gallina_print_leaf_entry; + print_library_entry = gallina_print_library_entry; + print_context = gallina_print_context; + print_typed_value_in_env = gallina_print_typed_value_in_env; + print_eval = gallina_print_eval; +} + +let object_pr = ref default_object_pr +let set_object_pr = (:=) object_pr + +let print_inductive x = !object_pr.print_inductive x +let print_constant_with_infos c = !object_pr.print_constant_with_infos c +let print_section_variable c = !object_pr.print_section_variable c +let print_syntactic_def x = !object_pr.print_syntactic_def x +let print_module x = !object_pr.print_module x +let print_modtype x = !object_pr.print_modtype x +let print_named_decl x = !object_pr.print_named_decl x +let print_leaf_entry x = !object_pr.print_leaf_entry x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x +let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x +let print_eval x = !object_pr.print_eval x + +(******************************************) +(**** Printing declarations and judgments *) +(**** Abstract layer *****) + +let print_typed_value x = print_typed_value_in_env (Global.env ()) x + +let print_judgment env {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env (trm, typ) + +let print_safe_judgment env j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + print_typed_value_in_env env (trm, typ) + +(*********************) +(* *) + let print_full_context () = print_context true None (Lib.contents_after None) let print_full_context_typ () = print_context false None (Lib.contents_after None) +let print_full_pure_context () = + let rec prec = function + | ((_,kn),Lib.Leaf lobj)::rest -> + let pp = match object_tag lobj with + | "CONSTANT" -> + let con = constant_of_kn kn in + let cb = Global.lookup_constant con in + let val_0 = cb.const_body in + let typ = ungeneralized_type_of_constant_type cb.const_type in + hov 0 ( + match val_0 with + | None -> + str (if cb.const_opaque then "Axiom " else "Parameter ") ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype typ + | Some v -> + if cb.const_opaque then + str "Theorem " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ + str "Proof " ++ print_body val_0 + else + str "Definition " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ + print_body val_0) ++ str "." ++ fnl () ++ fnl () + | "INDUCTIVE" -> + let (mib,mip) = Global.lookup_inductive (kn,0) in + let mipv = mib.mind_packets in + let names = list_tabulate (fun x -> (kn,x)) (Array.length mipv) in + pr_mutual_inductive mib.mind_finite names ++ str "." ++ + fnl () ++ fnl () + | "MODULE" -> + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | "MODULE TYPE" -> + (* TODO: make it reparsable *) + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | _ -> mt () in + prec rest ++ pp + | _::rest -> prec rest + | _ -> mt () in + prec (Lib.contents_after None) + (* For printing an inductive definition with its constructors and elimination, assume that the declaration of constructors and eliminations @@ -446,8 +603,9 @@ let read_sec_context r = let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection)::rest -> + | (_,Lib.ClosedSection _)::rest -> error "Cannot print the contents of a closed section" + (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -460,17 +618,13 @@ let print_sec_context sec = let print_sec_context_typ sec = print_context false None (read_sec_context sec) -let print_eval red_fun env {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env Evd.empty trm in - (str " = " ++ print_judgment env {uj_val = ntrm; uj_type = typ}) - let print_name ref = match locate_any_name ref with | Term (ConstRef sp) -> print_constant_with_infos sp | Term (IndRef (sp,_)) -> print_inductive sp | Term (ConstructRef ((sp,_),_)) -> print_inductive sp | Term (VarRef sp) -> print_section_variable sp - | Syntactic kn -> print_syntactic_def " := " kn + | Syntactic kn -> print_syntactic_def kn | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () | ModuleType (_,kn) -> print_modtype kn @@ -491,9 +645,7 @@ let print_name ref = | Lib.Leaf obj -> (oname,obj) | _ -> raise Not_found in - match print_leaf_entry true " = " (oname,lobj) with - | None -> mt () - | Some pp -> pp ++ fnl() + print_leaf_entry true (oname,lobj) with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object") @@ -508,7 +660,7 @@ let print_opaque_name qid = else error "not a defined constant" | IndRef (sp,_) -> - print_mutual sp + print_inductive sp | ConstructRef cstr -> let ty = Inductiveops.type_of_constructor env cstr in print_typed_value (mkConstruct cstr, ty) @@ -519,10 +671,11 @@ let print_opaque_name qid = let print_about ref = let k = locate_any_name ref in begin match k with - | Term ref -> - print_ref false ref ++ print_name_infos ref ++ print_opacity ref + | Term ref -> + print_ref false ref ++ fnl () ++ print_name_infos ref ++ + print_opacity ref | Syntactic kn -> - print_syntactic_def " := " kn + print_syntactic_def kn | Dir _ | ModuleType _ | Undefined _ -> mt () end ++ @@ -597,9 +750,40 @@ let print_path_between cls clt = in print_path ((i,j),p) +let pr_cs_pattern = function + Const_cs c -> pr_global c + | Prod_cs -> str "_ -> _" + | Default_cs -> str "_" + | Sort_cs s -> pr_sort_family s + let print_canonical_projections () = - prlist_with_sep pr_fnl (fun ((r1,r2),o) -> - pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") + prlist_with_sep pr_fnl + (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + str " <- " ++ + pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) + +(*************************************************************************) +(* Pretty-printing functions for type classes *) + +open Typeclasses + +let pr_typeclass env t = + print_ref false t.cl_impl + +let print_typeclasses () = + let env = Global.env () in + prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) + +let pr_instance env i = + (* gallina_print_constant_with_infos i.is_impl *) + (* lighter *) + print_ref false (ConstRef (instance_impl i)) + +let print_instances r = + let env = Global.env () in + let inst = instances r in + prlist_with_sep fnl (pr_instance env) inst + |