diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 54 |
1 files changed, 33 insertions, 21 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd51fd6b..e117f1dc 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -11,7 +11,7 @@ *) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -35,7 +35,7 @@ type object_pr = { print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; print_modtype : module_path -> std_ppcmds; - print_named_decl : Id.t * constr option * types -> std_ppcmds; + print_named_decl : Context.Named.Declaration.t -> 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 -> Evd.evar_map -> Term.constr * Term.types -> Pp.std_ppcmds; @@ -132,7 +132,8 @@ let print_renames_list prefix l = let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in let ctx = prod_assum typ in - let nprods = List.length (List.filter (fun (_,b,_) -> Option.is_empty b) ctx) in + let open Context.Rel.Declaration in + let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && let _,lastimpl = List.chop nprods impl in List.exists is_status_implicit lastimpl @@ -168,8 +169,10 @@ type opacity = | FullyOpaque | TransparentMaybeOpacified of Conv_oracle.level -let opacity env = function - | VarRef v when not (Option.is_empty (pi2 (Environ.lookup_named v env))) -> +let opacity env = + let open Context.Named.Declaration in + function + | VarRef v when is_local_def (Environ.lookup_named v env) -> Some(TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) | ConstRef cst -> @@ -212,15 +215,21 @@ let print_polymorphism ref = else "not universe polymorphic") ] else [] +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite -> mt () - | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> @@ -232,7 +241,7 @@ let print_name_infos ref = let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = - try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in + try Arguments_renaming.arguments_names ref with Not_found -> [] in let type_info_for_implicit = if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) @@ -241,6 +250,7 @@ let print_name_infos ref = else [] in print_polymorphism ref @ + print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ print_renames_list (mt()) renames @ @@ -271,7 +281,7 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids (fun r -> - try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) + try Arguments_renaming.arguments_names r with Not_found -> []) ((!=) Anonymous) print_renames_list @@ -440,11 +450,13 @@ let print_named_def name body typ = let print_named_assum name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" -let gallina_print_named_decl (id,c,typ) = - let s = Id.to_string id in - match c with - | Some body -> print_named_def s body typ - | None -> print_named_assum s typ +let gallina_print_named_decl = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum (Id.to_string id) typ + | LocalDef (id, body, typ) -> + print_named_def (Id.to_string id) body typ let assumptions_for_print lna = List.fold_right (fun na env -> add_name na env) lna empty_names_context @@ -721,8 +733,8 @@ let print_any_name = function try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in if not (DirPath.is_empty dir) then raise Not_found; - let (_,c,typ) = Global.lookup_named str in - (print_named_decl (str,c,typ)) + let open Context.Named.Declaration in + str |> Global.lookup_named |> set_id str |> print_named_decl with Not_found -> errorlabstrm "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") @@ -750,8 +762,8 @@ let print_opaque_name qid = let ty = Universes.unsafe_type_of_global gr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> - let (_,c,ty) = lookup_named id env in - print_named_decl (id,c,ty) + let open Context.Named.Declaration in + lookup_named id env |> set_id id |> print_named_decl let print_about_any loc k = match k with @@ -860,7 +872,7 @@ let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) print_ref false (instance_impl i) ++ - begin match instance_priority i with + begin match hint_priority i with | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i end |