From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Jan 2017 01:27:40 +0100 Subject: [location] Use Loc.located for constr_expr. This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location. --- printing/ppconstr.ml | 117 ++++++++++++++++++++++++++------------------------- 1 file changed, 60 insertions(+), 57 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 966ba6734..a99c0951f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -213,11 +213,11 @@ let tag_var = tag Tag.variable str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () + | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> mt () | t -> cut () ++ str ":" ++ pr t let pr_opt_type_spc pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () + | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident (loc,id) = @@ -352,7 +352,7 @@ let tag_var = tag Tag.variable end | Default b -> match t with - | CHole (_,_,Misctypes.IntroAnonymous,_) -> + | _loc, CHole (_,Misctypes.IntroAnonymous,_) -> let s = prlist_with_sep spc pr_lname nal in hov 1 (surround_implicit b s) | _ -> @@ -394,39 +394,40 @@ let tag_var = tag Tag.variable (* | 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*) - | CProdN (loc,[],c) -> + | _loc, CProdN ([],c) -> extract_prod_binders c - | CProdN (loc,[[_,Name id],bk,t], - CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))])) + | loc, CProdN ([[_,Name id],bk,t], + (_loc', CCases (LetPatternStyle,None, [(_loc'', 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 - CLocalPattern (loc,p,None) :: bl, c - | CProdN (loc,(nal,bk,t)::bl,c) -> - let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in + CLocalPattern (loc, p,None) :: bl, c + | loc, CProdN ((nal,bk,t)::bl,c) -> + let bl,c = extract_prod_binders (loc, CProdN(bl,c)) in CLocalAssum (nal,bk,t) :: bl, c | c -> [], c - let rec extract_lam_binders = function + let rec extract_lam_binders (loc, ce) = match ce 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 (loc,[],c) -> + | CLambdaN ([],c) -> extract_lam_binders c - | CLambdaN (loc,[[_,Name id],bk,t], - CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))])) + | CLambdaN ([[_,Name id],bk,t], + (_loc, CCases (LetPatternStyle,None, [(_loc', 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 CLocalPattern (loc,p,None) :: bl, c - | CLambdaN (loc,(nal,bk,t)::bl,c) -> - let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in + | CLambdaN ((nal,bk,t)::bl,c) -> + let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in CLocalAssum (nal,bk,t) :: bl, c - | c -> [], c + | c -> [], Loc.tag ~loc c - let split_lambda = function - | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c) - | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) - | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c)) + let split_lambda = Loc.with_loc (fun ~loc -> function + | CLambdaN ([[na],bk,t],c) -> (na,t,c) + | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN(bl,c)) + | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN((nal,bk,t)::bl,c)) | _ -> anomaly (Pp.str "ill-formed fixpoint body") + ) let rename na na' t c = match (na,na') with @@ -435,12 +436,13 @@ let tag_var = tag Tag.variable | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) - let split_product na' = function - | CProdN (loc,[[na],bk,t],c) -> rename na na' t c - | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) - | CProdN (loc,(na::nal,bk,t)::bl,c) -> - rename na na' t (CProdN(loc,(nal,bk,t)::bl,c)) + let split_product na' = Loc.with_loc (fun ~loc -> function + | CProdN ([[na],bk,t],c) -> rename na na' t c + | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ~loc @@ CProdN(bl,c)) + | CProdN ((na::nal,bk,t)::bl,c) -> + rename na na' t (Loc.tag ~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) @@ -506,7 +508,7 @@ let tag_var = tag Tag.variable let pr_case_type pr po = match po with - | None | Some (CHole (_,_,Misctypes.IntroAnonymous,_)) -> mt() + | None | Some (_, CHole (_,Misctypes.IntroAnonymous,_)) -> mt() | Some p -> spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p) @@ -543,25 +545,25 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a with - | (CFix (_,_,[_])|CCoFix(_,_,[_])) -> + match snd a with + | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> pr sep inherited a let pr pr sep inherited a = let return (cmds, prec) = (tag_constr_expr a cmds, prec) in - let (strm, prec) = match a with + let (strm, prec) = match snd @@ Loc.to_pair a with | CRef (r, us) -> return (pr_cref r us, latom) - | CFix (_,id,fix) -> + | CFix (id,fix) -> return ( hov 0 (keyword "fix" ++ spc () ++ pr_recursive (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), lfix ) - | CCoFix (_,id,cofix) -> + | CCoFix (id,cofix) -> return ( hov 0 (keyword "cofix" ++ spc () ++ pr_recursive @@ -586,7 +588,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b) + | CLetIn ((_,Name x), ((_loc, CFix((_,x'),[_])) + | (_loc, CCoFix((_,x'),[_])) as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -596,7 +599,7 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CLetIn (_,x,a,t,b) -> + | CLetIn (x,a,t,b) -> return ( hv 0 ( hov 2 (keyword "let" ++ spc () ++ pr_lname x @@ -606,7 +609,7 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CAppExpl (_,(Some i,f,us),l) -> + | CAppExpl ((Some i,f,us),l) -> let l1,l2 = List.chop i l in let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in @@ -614,16 +617,16 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl (_,(None,Ident (_,var),us),[t]) - | CApp (_,(_,CRef(Ident(_,var),us)),[t,None]) + | CAppExpl ((None,Ident (_,var),us),[t]) + | CApp ((_,(_, CRef(Ident(_,var),us))),[t,None]) when Id.equal var Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg ) - | CAppExpl (_,(None,f,us),l) -> + | CAppExpl ((None,f,us),l) -> return (pr_appexpl (pr mt) (f,us) l, lapp) - | CApp (_,(Some i,f),l) -> + | CApp ((Some i,f),l) -> let l1,l2 = List.chop i l in let c,l1 = List.sep_last l1 in assert (Option.is_empty (snd c)); @@ -635,14 +638,14 @@ let tag_var = tag Tag.variable ) else return (p, lproj) - | CApp (_,(None,a),l) -> + | CApp ((None,a),l) -> return (pr_app (pr mt) a l, lapp) - | CRecord (_,l) -> + | CRecord l -> return ( hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ @@ -653,7 +656,7 @@ let tag_var = tag Tag.variable spc () ++ keyword "in" ++ pr spc ltop b)), lletpattern ) - | CCases(_,_,rtntypopt,c,eqns) -> + | CCases(_,rtntypopt,c,eqns) -> return ( v 0 (hv 0 (keyword "match" ++ brk (1,2) ++ @@ -666,7 +669,7 @@ let tag_var = tag Tag.variable ++ keyword "end"), latom ) - | CLetTuple (_,nal,(na,po),c,b) -> + | CLetTuple (nal,(na,po),c,b) -> return ( hv 0 ( hov 2 (keyword "let" ++ spc () ++ @@ -679,7 +682,7 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CIf (_,c,(na,po),b1,b2) -> + | CIf (c,(na,po),b1,b2) -> (* On force les parenthèses autour d'un "if" sous-terme (même si le parsing est lui plus tolérant) *) return ( @@ -693,19 +696,19 @@ let tag_var = tag Tag.variable lif ) - | CHole (_,_,Misctypes.IntroIdentifier id,_) -> + | CHole (_,Misctypes.IntroIdentifier id,_) -> return (str "?[" ++ pr_id id ++ str "]", latom) - | CHole (_,_,Misctypes.IntroFresh id,_) -> + | CHole (_,Misctypes.IntroFresh id,_) -> return (str "?[?" ++ pr_id id ++ str "]", latom) - | CHole (_,_,_,_) -> + | CHole (_,_,_) -> return (str "_", latom) - | CEvar (_,n,l) -> + | CEvar (n,l) -> return (pr_evar (pr mt) n l, latom) - | CPatVar (_,p) -> + | CPatVar p -> return (str "@?" ++ pr_patvar p, latom) - | CSort (_,s) -> + | CSort s -> return (pr_glob_sort s, latom) - | CCast (_,a,b) -> + | CCast (a,b) -> return ( hv 0 (pr mt (lcast,L) a ++ spc () ++ match b with @@ -715,15 +718,15 @@ 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) -> + | CNotation (s,env) -> pr_notation (pr mt) (pr_binders_gen (pr mt ltop)) s env - | CGeneralization (_,bk,ak,c) -> + | CGeneralization (bk,ak,c) -> return (pr_generalization bk ak (pr mt ltop c), latom) - | CPrim (_,p) -> + | CPrim p -> return (pr_prim_token p, prec_of_prim_token p) - | CDelimiters (_,sc,a) -> + | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) in let loc = constr_loc a in @@ -751,7 +754,7 @@ let tag_var = tag Tag.variable let pr prec c = pr prec (transf (Global.env()) c) let pr_simpleconstr = function - | CAppExpl (_,(None,f,us),[]) -> str "@" ++ pr_cref f us + | _lock, CAppExpl ((None,f,us),[]) -> str "@" ++ pr_cref f us | c -> pr lsimpleconstr c let default_term_pr = { -- cgit v1.2.3