diff options
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 58 |
1 files changed, 31 insertions, 27 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index fcdc2aee..eef28fcf 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ppconstr.ml 13358 2010-07-29 23:10:17Z herbelin $ *) (*i*) open Util @@ -64,8 +64,8 @@ let prec_of_prim_token = function open Notation -let print_hunks n pr (env,envlist) unp = - let env = ref env and envlist = ref envlist in +let print_hunks n pr pr_binders (terms,termlists,binders) unp = + let env = ref terms and envlist = ref termlists and bll = ref binders in let pop r = let a = List.hd !r in r := List.tl !r; a in let rec aux = function | [] -> mt () @@ -76,6 +76,8 @@ let print_hunks n pr (env,envlist) unp = let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in let pp2 = aux l in pp1 ++ pp2 + | UnpBinderListMetaVar (_,isopen,sl) :: l -> + let cl = pop bll in pr_binders (fun () -> aux sl) isopen cl ++ aux l | UnpTerminal s :: l -> str s ++ aux l | UnpBox (b,sub) :: l -> (* Keep order: side-effects *) @@ -85,9 +87,9 @@ let print_hunks n pr (env,envlist) unp = | UnpCut cut :: l -> ppcmd_of_cut cut ++ aux l in aux unp -let pr_notation pr s env = +let pr_notation pr pr_binders s env = let unpl, level = find_notation_printing_rule s in - print_hunks level pr env unpl, level + print_hunks level pr pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -191,7 +193,8 @@ let rec pr_patt sep inh p = hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator | CPatNotation (_,"( _ )",([p],[])) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom - | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env + | CPatNotation (_,s,(l,ll)) -> + pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) | CPatPrim (_,p) -> pr_prim_token p, latom | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1 in @@ -254,18 +257,22 @@ let pr_binder_among_many pr_c = function hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) -let pr_undelimited_binders pr_c = - prlist_with_sep spc (pr_binder_among_many pr_c) +let pr_undelimited_binders sep pr_c = + prlist_with_sep sep (pr_binder_among_many pr_c) -let pr_delimited_binders kw pr_c bl = +let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with | [LocalRawAssum (nal,k,t)] -> pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t) | LocalRawAssum _ :: _ as bdl -> - pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl + pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false +let pr_binders_gen pr_c sep is_open = + if is_open then pr_delimited_binders mt sep pr_c + else pr_undelimited_binders sep pr_c + let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in @@ -399,7 +406,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in pr_id id ++ str" " ++ - hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++ + hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ pr_opt_type_spc pr t ++ str " :=" ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c @@ -446,7 +453,7 @@ let tm_clash = function let pr_asin pr (na,indnalopt) = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) - | Some na -> spc () ++ str "as " ++ pr_name na + | Some na -> spc () ++ str "as " ++ pr_lname na | None -> mt ()) ++ (match indnalopt with | None -> mt () @@ -465,7 +472,7 @@ let pr_return_type pr po = pr_case_type pr po let pr_simple_return_type pr na po = (match na with - | Some (Name id) -> + | Some (_,Name id) -> spc () ++ str "as " ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -483,15 +490,11 @@ let pr_app pr a l = pr (lapp,L) a ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l) -let pr_forall () = - if !Flags.unicode_syntax then str"Π" ++ spc () - else str"forall" ++ spc () +let pr_forall () = str"forall" ++ spc () -let pr_fun () = - if !Flags.unicode_syntax then str"λ" ++ spc () - else str"fun" ++ spc () +let pr_fun () = str"fun" ++ spc () -let pr_fun_sep = lazy (if !Flags.unicode_syntax then str "," else str " =>") +let pr_fun_sep = str " =>" let pr_dangling_with_for sep pr inherited a = @@ -519,16 +522,16 @@ let pr pr sep inherited a = | CProdN _ -> let (bl,a) = extract_prod_binders a in hov 0 ( - hov 2 (pr_delimited_binders pr_forall + hov 2 (pr_delimited_binders pr_forall spc (pr mt ltop) bl) ++ str "," ++ pr spc ltop a), lprod | CLambdaN _ -> let (bl,a) = extract_lam_binders a in hov 0 ( - hov 2 (pr_delimited_binders pr_fun + hov 2 (pr_delimited_binders pr_fun spc (pr mt ltop) bl) ++ - Lazy.force pr_fun_sep ++ pr spc ltop a), + pr_fun_sep ++ pr spc ltop a), llambda | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) when x=x' -> @@ -599,7 +602,7 @@ let pr pr sep inherited a = hv 0 ( str "let " ++ hov 0 (str "(" ++ - prlist_with_sep sep_v pr_name nal ++ + prlist_with_sep sep_v pr_lname nal ++ str ")" ++ pr_simple_return_type (pr mt) na po ++ str " :=" ++ pr spc ltop c ++ str " in") ++ @@ -626,9 +629,10 @@ let pr pr sep inherited a = | CCast (_,a,CastCoerce) -> hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"), lcast - | CNotation (_,"( _ )",([t],[])) -> + | CNotation (_,"( _ )",([t],[],[])) -> pr (fun()->str"(") (max_int,L) t ++ str")", latom - | CNotation (_,s,env) -> pr_notation (pr mt) s env + | CNotation (_,s,env) -> + pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1 @@ -700,7 +704,7 @@ let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c let pr_cases_pattern_expr = pr_patt ltop -let pr_binders = pr_undelimited_binders (pr ltop) +let pr_binders = pr_undelimited_binders spc (pr ltop) let pr_with_occurrences pr occs = match occs with |