diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 146 |
1 files changed, 44 insertions, 102 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1146b42a01..3c7095505a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -10,6 +10,7 @@ open CErrors open Util open Pp +open CAst open Names open Nameops open Libnames @@ -86,8 +87,8 @@ let tag_var = tag Tag.variable open Notation - let print_hunks n pr pr_binders (terms, termlists, binders) unps = - let env = ref terms and envlist = ref termlists and bll = ref binders in + let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps = + let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in (* Warning: @@ -102,6 +103,11 @@ let tag_var = tag Tag.variable let pp2 = aux l in let pp1 = pr (n, prec) c in return unp pp1 pp2 + | UnpBinderMetaVar (_, prec) as unp :: l -> + let c = pop bl in + let pp2 = aux l in + let pp1 = pr_patt (n, prec) c in + return unp pp1 pp2 | UnpListMetaVar (_, prec, sl) as unp :: l -> let cl = pop envlist in let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in @@ -127,9 +133,9 @@ let tag_var = tag Tag.variable in aux unps - let pr_notation pr pr_binders s env = + let pr_notation pr pr_patt pr_binders s env = let unpl, level = find_notation_printing_rule s in - print_hunks level pr pr_binders env unpl, level + print_hunks level pr pr_patt pr_binders env unpl, level let pr_delimiters key strm = strm ++ str ("%"^key) @@ -146,7 +152,7 @@ let tag_var = tag Tag.variable if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() - let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp) + let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp) let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) @@ -215,28 +221,28 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a - | Some (_,ExplByPos (n,_id)) -> + | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") - | Some (_,ExplByName id) -> + | Some {v=ExplByName id} -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident (loc,id) = + let pr_lident {loc; v=id} = match loc with | None -> pr_id id | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id + pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,s) -> pr_lident (loc,s) + | ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -263,8 +269,8 @@ let tag_var = tag Tag.variable in str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec - | CPatAlias (p, id) -> - pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las + | CPatAlias (p, na) -> + pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las | CPatCstr (c, None, []) -> pr_reference c, latom @@ -292,7 +298,7 @@ let tag_var = tag Tag.variable pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom | CPatNotation (s,(l,ll),args) -> - let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in + let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) s (l,ll,[],[]) in (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not) ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not @@ -310,7 +316,7 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt - let pr_eqn pr (loc,(pl,rhs)) = + let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ @@ -318,12 +324,12 @@ let tag_var = tag Tag.variable ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder l_bi = + let begin_of_binder l_bi = let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in match l_bi with - | CLocalDef((loc,_),_,_) -> b_loc loc - | CLocalAssum((loc,_)::_,_,_) -> b_loc loc - | CLocalPattern(loc,(_,_)) -> b_loc loc + | CLocalDef({loc},_,_) -> b_loc loc + | CLocalAssum({loc}::_,_,_) -> b_loc loc + | CLocalPattern{loc} -> b_loc loc | _ -> assert false let begin_of_binders = function @@ -345,12 +351,12 @@ let tag_var = tag Tag.variable | Generalized (b, b', t') -> assert (match b with Implicit -> true | _ -> false); begin match nal with - |[loc,Anonymous] -> + |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' ((if t' then str "!" else mt ()) ++ pr t))) - |[loc,Name id] -> + |[{loc; v=Name id}] -> hov 1 (str "`" ++ (surround_impl b' - (pr_lident (loc,id) ++ str " : " ++ + (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end @@ -370,7 +376,7 @@ 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 (loc,(p,tyo)) -> + | CLocalPattern {CAst.loc; v = p,tyo} -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -394,68 +400,6 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let rec extract_prod_binders = let open CAst in function - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_prod_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | { v = CProdN ([],c) } -> - extract_prod_binders c - | { loc; v = CProdN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) } - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_prod_binders b in - CLocalPattern (loc, (p,None)) :: bl, c - | { loc; v = CProdN ((nal,bk,t)::bl,c) } -> - let bl,c = extract_prod_binders (CAst.make ?loc @@ CProdN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | c -> [], c - - let rec extract_lam_binders ce = let open CAst in match ce.v with - (* | CLetIn (loc,na,b,c) as x -> - let bl,c = extract_lam_binders c in - if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) - | CLambdaN ([],c) -> - extract_lam_binders c - | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) - when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> - let bl,c = extract_lam_binders b in - CLocalPattern (ce.loc,(p,None)) :: bl, c - | CLambdaN ((nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CAst.make ?loc:ce.loc @@ CLambdaN(bl,c)) in - CLocalAssum (nal,bk,t) :: bl, c - | _ -> [], ce - - let split_lambda = CAst.with_loc_val (fun ?loc -> function - | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t, CAst.make ?loc @@ CLambdaN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rename na na' t c = - match (na,na') with - | (_,Name id), (_,Name id') -> - (na',t,replace_vars_constr_expr (Id.Map.singleton id id') c) - | (_,Name id), (_,Anonymous) -> (na,t,c) - | _ -> (na',t,c) - - let split_product na' = CAst.with_loc_val (fun ?loc -> function - | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (CAst.make ?loc @@ CProdN(bl,c)) - | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (CAst.make ?loc @@ CProdN((nal,bk,t)::bl,c)) - | _ -> anomaly (Pp.str "ill-formed fixpoint body.") - ) - - let rec split_fix n typ def = - if Int.equal n 0 then ([],typ,def) - else - 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 - (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 = if dangling_with_for then pr_dangling else pr in @@ -467,7 +411,7 @@ let tag_var = tag Tag.variable let pr_guard_annot pr_aux bl (n,ro) = match n with | None -> mt () - | Some (loc, id) -> + | Some {loc; v = id} -> match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function @@ -484,11 +428,11 @@ let tag_var = tag Tag.variable spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = + let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function @@ -518,7 +462,7 @@ let tag_var = tag Tag.variable let pr_simple_return_type pr na po = (match na with - | Some (_,Name id) -> + | Some {v=Name id} -> spc () ++ keyword "as" ++ spc () ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -549,7 +493,7 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a.CAst.v with + match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> @@ -564,18 +508,17 @@ let tag_var = tag Tag.variable return ( hov 0 (keyword "fix" ++ spc () ++ pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( hov 0 (keyword "cofix" ++ spc () ++ pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) - | CProdN _ -> - let (bl,a) = extract_prod_binders a in + | CProdN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_forall spc @@ -583,8 +526,7 @@ let tag_var = tag Tag.variable str "," ++ pr spc ltop a), lprod ) - | CLambdaN _ -> - let (bl,a) = extract_lam_binders a in + | CLambdaN (bl,a) -> return ( hov 0 ( hov 2 (pr_delimited_binders pr_fun spc @@ -592,8 +534,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])} - | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b) + | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])} + | { v = CCoFix({v=x'},[_]) } as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -649,7 +591,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -722,10 +664,10 @@ let tag_var = tag Tag.variable | CastCoerce -> str ":>"), lcast ) - | CNotation ("( _ )",([t],[],[])) -> + | CNotation ("( _ )",([t],[],[],[])) -> return (pr (fun()->str"(") (max_int,L) t ++ str")", latom) | CNotation (s,env) -> - pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env + pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) s env | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) | CPrim p -> |