From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Apr 2017 21:41:41 +0200 Subject: Creating a module Nameops.Name extending module Names.Name. This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name. --- engine/termops.ml | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) (limited to 'engine/termops.ml') diff --git a/engine/termops.ml b/engine/termops.ml index ca32c06a7..1af9bd1ff 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -31,10 +31,6 @@ let pr_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") -let pr_name = function - | Name id -> pr_id id - | Anonymous -> str "_" - let pr_con sp = str(string_of_con sp) let pr_fix pr_constr ((t,i),(lna,tl,bl)) = @@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ pr_constr c ++ str")") | Lambda (na,t,c) -> hov 1 - (str"fun " ++ pr_name na ++ str":" ++ + (str"fun " ++ Name.print na ++ str":" ++ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ + (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ pr_constr c) | App (c,l) -> hov 1 @@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ pr_constr ty ++ + Name.print na ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -308,8 +304,8 @@ let pr_evar_universe_context ctx = let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function - | RelDecl.LocalAssum (n,_) -> pr_name n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalAssum (n,_) -> Name.print n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in -- cgit v1.2.3