From 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Oct 2020 13:18:09 +0200 Subject: A step towards supporting pattern cast deeplier. We at least support a cast at the top of patterns in notations. --- printing/ppconstr.ml | 64 +++++++++++++++++++++++-------------------------- printing/proof_diffs.ml | 3 ++- 2 files changed, 32 insertions(+), 35 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f726626ac4..8942bc7805 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -273,28 +273,29 @@ let tag_var = tag Tag.variable let las = lapp let lpator = 0 let lpatrec = 0 + let lpatcast = LevelLe 100 let lpattop = LevelLe 200 - let rec pr_patt sep inh p = + let rec pr_patt sep pr inh p = let (strm,prec) = match CAst.(p.v) with | CPatRecord l -> - pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec + pr_record_body "{|" "|}" (pr_patt spc pr lpattop) l, lpatrec | CPatAlias (p, na) -> - pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las + pr_patt mt pr (LevelLe las) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom | CPatCstr (c, None, args) -> - pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp + pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp | CPatCstr (c, Some args, []) -> - str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp + str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) args, lapp | CPatCstr (c, Some expl_args, extra_args) -> - surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args) - ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp + surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc pr (LevelLt lapp)) expl_args) + ++ prlist (pr_patt spc pr (LevelLt lapp)) extra_args, lapp | CPatAtom (None) -> str "_", latom @@ -303,25 +304,25 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - let pp p = hov 0 (pr_patt mt lpattop p) in + let pp p = hov 0 (pr_patt mt pr lpattop p) in surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation (_,(_,"( _ )"),([p],[]),[]) -> - pr_patt (fun()->str"(") lpattop p ++ str")", latom + pr_patt (fun()->str"(") pr lpattop p ++ str")", latom | CPatNotation (which,s,(l,ll),args) -> - let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in + let strm_not, l_not = pr_notation (pr_patt mt pr) (fun _ _ _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not) - ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not + ++ prlist (pr_patt spc pr (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not | CPatPrim p -> pr_prim_token p, latom | CPatDelimiters (k,p) -> - pr_delimiters k (pr_patt mt lsimplepatt p), 1 + pr_delimiters k (pr_patt mt pr lsimplepatt p), 1 - | CPatCast _ -> - assert false + | CPatCast (p,t) -> + (pr_patt mt pr lpatcast p ++ spc () ++ str ":" ++ ws 1 ++ pr t), 1 in let loc = p.CAst.loc in pr_with_comments ?loc @@ -329,21 +330,21 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt - let pr_patt_binder prec style bk c = + let pr_patt_binder pr prec style bk c = match bk with - | MaxImplicit -> str "{" ++ pr_patt lpattop c ++ str "}" - | NonMaxImplicit -> str "[" ++ pr_patt lpattop c ++ str "]" + | MaxImplicit -> str "{" ++ pr_patt pr lpattop c ++ str "}" + | NonMaxImplicit -> str "[" ++ pr_patt pr lpattop c ++ str "]" | Explicit -> match style, c with - | NotQuotedPattern, _ | _, {v=CPatAtom _} -> pr_patt prec c - | QuotedPattern, _ -> str "'" ++ pr_patt prec c + | NotQuotedPattern, _ | _, {v=CPatAtom _} -> pr_patt pr prec c + | QuotedPattern, _ -> str "'" ++ pr_patt pr prec c let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ hov 0 (prlist_with_sep pr_spcbar - (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt ltop) p)) pl + (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt (pr ltop) ltop) p)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) @@ -400,13 +401,8 @@ let tag_var = tag Tag.variable surround (pr_lname na ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ str" :=" ++ spc() ++ pr_c c) - | CLocalPattern {CAst.loc; v = p,tyo} -> - let p = pr_patt lsimplepatt p in - match tyo with - | None -> - str "'" ++ p - | Some ty -> - str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty) + | CLocalPattern p -> + str "'" ++ pr_patt pr_c lsimplepatt p let pr_undelimited_binders sep pr_c = prlist_with_sep sep (pr_binder_among_many pr_c) @@ -468,16 +464,16 @@ let tag_var = tag Tag.variable (pr_decl "with" true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id - let pr_asin pr na indnalopt = + let pr_as_in pr na indnalopt = (match na with (* Decision of printing "_" or not moved to constrextern.ml *) | Some na -> spc () ++ keyword "as" ++ spc () ++ pr_lname na | None -> mt ()) ++ (match indnalopt with | None -> mt () - | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t) + | Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt pr lsimplepatt t) let pr_case_item pr (tm,as_clause, in_clause) = - hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause) + hov 0 (pr (LevelLe lcast) tm ++ pr_as_in (pr ltop) as_clause in_clause) let pr_case_type pr po = match po with @@ -610,8 +606,8 @@ let tag_var = tag Tag.variable return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ - hov 0 (pr_patt ltop p ++ - pr_asin (pr_dangling_with_for mt pr) as_clause in_clause ++ + hov 0 (pr_patt (pr mt ltop) ltop p ++ + pr_as_in (pr mt ltop) as_clause in_clause ++ str " :=" ++ pr spc ltop c ++ pr_case_type (pr_dangling_with_for mt pr) rtntypopt ++ spc () ++ keyword "in" ++ pr spc ltop b)), @@ -682,7 +678,7 @@ let tag_var = tag Tag.variable | CNotation (_,(_,"( _ )"),([t],[],[],[])) -> return (pr (fun()->str"(") ltop t ++ str")", latom) | CNotation (which,s,env) -> - pr_notation (pr mt) pr_patt_binder (pr_binders_gen (pr mt ltop)) which s env + pr_notation (pr mt) (pr_patt_binder (pr mt ltop)) (pr_binders_gen (pr mt ltop)) which s env | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) | CPrim p -> @@ -746,7 +742,7 @@ let tag_var = tag Tag.variable let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c - let pr_cases_pattern_expr = pr_patt ltop + let pr_cases_pattern_expr = pr_patt (pr ltop) ltop let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop) diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index b2ebc61b4e..9bf765717f 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -433,7 +433,8 @@ let match_goals ot nt = constr_expr ogname c c2; constr_expr_opt ogname t t2 | CLocalPattern p, CLocalPattern p2 -> - let (p,ty), (p2,ty2) = p.v,p2.v in + let ty = match p.v with CPatCast (_,ty) -> Some ty | _ -> None in + let ty2 = match p2.v with CPatCast (_,ty) -> Some ty | _ -> None in constr_expr_opt ogname ty ty2 | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)") in -- cgit v1.2.3