From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- printing/ppconstr.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d92d832759..2c2f32209c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -319,7 +319,7 @@ let tag_var = tag Tag.variable let begin_of_binder = function LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalPattern(loc,_,_) -> fst (Loc.unloc loc) + | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -368,7 +368,7 @@ let tag_var = tag Tag.variable | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) - | LocalPattern (loc,p,tyo) -> + | LocalRawPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -384,7 +384,7 @@ let tag_var = tag Tag.variable match bl with | [LocalRawAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalPattern _) :: _ as bdl -> + | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false @@ -402,7 +402,7 @@ let tag_var = tag Tag.variable CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in - LocalPattern (loc,p,None) :: bl, c + LocalRawPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in LocalRawAssum (nal,bk,t) :: bl, c @@ -418,7 +418,7 @@ let tag_var = tag Tag.variable CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - LocalPattern (loc,p,None) :: bl, c + LocalRawPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in LocalRawAssum (nal,bk,t) :: bl, c @@ -469,7 +469,7 @@ let tag_var = tag Tag.variable let names_of_binder = function | LocalRawAssum (nal,_,_) -> nal | LocalRawDef (_,_) -> [] - | LocalPattern _ -> assert false + | LocalRawPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- printing/ppconstr.ml | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2c2f32209c..d895693cc9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,9 +317,9 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc) + CLocalDef((loc,_),_) -> fst (Loc.unloc loc) + | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -360,15 +360,15 @@ let tag_var = tag Tag.variable hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,k,t) -> + | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> + | CLocalDef (na,c) -> let c,topt = match c with | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) - | LocalRawPattern (loc,p,tyo) -> + | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -382,9 +382,9 @@ let tag_var = tag Tag.variable let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with - | [LocalRawAssum (nal,k,t)] -> + | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false @@ -395,33 +395,33 @@ let tag_var = tag Tag.variable let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c | CProdN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in - LocalRawPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let rec extract_lam_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c | CLambdaN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - LocalRawPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let split_lambda = function @@ -450,7 +450,7 @@ let tag_var = tag Tag.variable let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in let (bl,typ,def) = split_fix (n-1) typ def in - (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def) + (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = @@ -467,9 +467,9 @@ let tag_var = tag Tag.variable match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - | LocalRawPattern _ -> assert false + | CLocalAssum (nal,_,_) -> nal + | CLocalDef (_,_) -> [] + | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" -- cgit v1.2.3 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- printing/ppconstr.ml | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d895693cc9..0013d49a1b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,7 +317,7 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - CLocalDef((loc,_),_) -> fst (Loc.unloc loc) + | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc) | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false @@ -362,12 +362,9 @@ let tag_var = tag Tag.variable let pr_binder_among_many pr_c = function | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | CLocalDef (na,c) -> - let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in - surround (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c) + | CLocalDef (na,c,topt) -> + surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++ + pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt) | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with @@ -468,7 +465,7 @@ let tag_var = tag Tag.variable | CStructRec -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal - | CLocalDef (_,_) -> [] + | CLocalDef (_,_,_) -> [] | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then @@ -588,7 +585,7 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -598,11 +595,12 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CLetIn (_,x,a,b) -> + | CLetIn (_,x,a,t,b) -> return ( hv 0 ( hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" ++ pr spc ltop a ++ spc () + ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t ++ keyword "in") ++ pr spc ltop b), lletin -- cgit v1.2.3 From eec5145a5c6575d04b5ab442597fb52913daed29 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 4 Feb 2017 14:56:04 +0100 Subject: Applying same convention as in Definition for printing type in a let in. Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *) --- printing/ppconstr.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 0013d49a1b..f36c8c1530 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -363,8 +363,9 @@ let tag_var = tag Tag.variable | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) | CLocalDef (na,c,topt) -> - surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++ - pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt) + surround (pr_lname na ++ + pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ + str" :=" ++ spc() ++ pr_c c) | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with @@ -598,9 +599,9 @@ let tag_var = tag Tag.variable | CLetIn (_,x,a,t,b) -> return ( hv 0 ( - hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" - ++ pr spc ltop a ++ spc () - ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t + hov 2 (keyword "let" ++ spc () ++ pr_lname x + ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr mt ltop t) t + ++ str " :=" ++ pr spc ltop a ++ spc () ++ keyword "in") ++ pr spc ltop b), lletin -- cgit v1.2.3 From 3fe764dd8d6578adddb01b02bafc7f31d9cb776c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 2 Apr 2017 11:20:21 +0200 Subject: Fix higher-order pattern variables not being printed as "@?" (bug #5431). --- printing/ppconstr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d92d832759..7f5adbfe49 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -703,7 +703,7 @@ let tag_var = tag Tag.variable | CEvar (_,n,l) -> return (pr_evar (pr mt) n l, latom) | CPatVar (_,p) -> - return (str "?" ++ pr_patvar p, latom) + return (str "@?" ++ pr_patvar p, latom) | CSort (_,s) -> return (pr_glob_sort s, latom) | CCast (_,a,b) -> -- cgit v1.2.3