From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Jan 2017 13:02:55 +0100 Subject: [location] Move Glob_term.cases_pattern to located. We continue the uniformization pass. No big news here, trying to be minimally invasive. --- pretyping/patternops.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b16d044956..8c570dffee 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = function [0,tags,pat_of_raw metas vars c]) | GCases (loc,sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind + | (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -408,15 +408,15 @@ let rec pat_of_raw metas vars = function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | PatVar(_,na) -> + | _, PatVar na -> name_iter (fun n -> metas := n::!metas) na; na - | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") + | loc, PatCstr(_,_,_) -> err ~loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) - | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs -> + | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) + | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> -- cgit v1.2.3 From be83b52cf50ed4c596e40cfd52da03258a7a4a18 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Jan 2017 13:22:42 +0100 Subject: [location] Move Glob_term.predicate_pattern to located. We continue the uniformization pass. No big news here, trying to be minimally invasive. --- pretyping/patternops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 8c570dffee..48ae93f3ef 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -380,13 +380,13 @@ let rec pat_of_raw metas vars = function | _ -> None in let ind_tags,ind = match indnames with - | Some (_,ind,nal) -> Some (List.length nal), Some ind + | Some (_,(ind,nal)) -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with - | Some p, Some (_,_,nal) -> + | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | (None | Some (GHole _)), _ -> PMeta None -- cgit v1.2.3 From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 14:23:53 +0100 Subject: [location] Switch glob_constr to Loc.located --- pretyping/patternops.ml | 45 +++++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 22 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 48ae93f3ef..6696e174bd 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -324,46 +324,46 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = function - | GVar (_,id) -> +let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function + | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (_,(false,n)) -> + | GPatVar (false,n) -> metas := n::!metas; PMeta (Some n) - | GRef (_,gr,_) -> + | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp (_, GPatVar (_,(true,n)), cl) -> + | GApp ((_, GPatVar (true,n)), cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | GApp (_,c,cl) -> + | GApp (c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) - | GLambda (_,na,bk,c1,c2) -> + | GLambda (na,bk,c1,c2) -> name_iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GProd (_,na,bk,c1,c2) -> + | GProd (na,bk,c1,c2) -> name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GLetIn (_,na,c1,t,c2) -> + | GLetIn (na,c1,t,c2) -> name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) - | GSort (_,s) -> + | GSort s -> PSort s | GHole _ -> PMeta None - | GCast (_,c,_) -> + | GCast (c,_) -> warn_cast_in_pattern (); pat_of_raw metas vars c - | GIf (_,c,(_,None),b1,b2) -> + | GIf (c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) - | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = - GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in + | GLetTuple (nal,(_,None),b,c) -> + let mkGLambda c na = Loc.tag ~loc @@ + GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; @@ -374,9 +374,9 @@ let rec pat_of_raw metas vars = function let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in PCase (cip, PMeta None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas vars c]) - | GCases (loc,sty,p,[c,(na,indnames)],brs) -> + | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind + | (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (GHole _)), _ -> PMeta None + | (None | Some (_, GHole _)), _ -> PMeta None | Some p, None -> user_err ~loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in @@ -404,7 +404,8 @@ let rec pat_of_raw metas vars = function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.") + | r -> err ~loc (Pp.str "Non supported pattern.") + ) and pats_of_glob_branches loc metas vars ind brs = let get_arg = function @@ -415,8 +416,8 @@ and pats_of_glob_branches loc metas vars ind brs = in let rec get_pat indexes = function | [] -> false, [] - | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) - | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs -> + | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *) + | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> @@ -431,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs = let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) - | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.") + | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs -- cgit v1.2.3 From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- pretyping/patternops.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 6696e174bd..84d846afd9 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -324,7 +324,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function +let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -362,7 +362,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = Loc.tag ~loc @@ + let mkGLambda c na = Loc.tag ?loc @@ GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = @@ -391,7 +391,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | (None | Some (_, GHole _)), _ -> PMeta None | Some p, None -> - user_err ~loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") + user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; @@ -404,7 +404,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err ~loc (Pp.str "Non supported pattern.") + | r -> err ?loc (Pp.str "Non supported pattern.") ) and pats_of_glob_branches loc metas vars ind brs = @@ -412,7 +412,7 @@ and pats_of_glob_branches loc metas vars ind brs = | _, PatVar na -> name_iter (fun n -> metas := n::!metas) na; na - | loc, PatCstr(_,_,_) -> err ~loc (Pp.str "Non supported pattern.") + | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] @@ -421,10 +421,10 @@ and pats_of_glob_branches loc metas vars ind brs = let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> - err ~loc (Pp.str "All constructors must be in the same inductive type.") + err ?loc (Pp.str "All constructors must be in the same inductive type.") in if Int.Set.mem (j-1) indexes then - err ~loc + err ?loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in @@ -432,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs = let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) - | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.") + | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs -- cgit v1.2.3 From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:35:20 +0200 Subject: [location] [ast] Port module AST to CAst --- pretyping/patternops.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'pretyping/patternops.ml') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 84d846afd9..1884b69279 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -324,7 +324,7 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function +let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -333,7 +333,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ((_, GPatVar (true,n)), cl) -> + | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) | GApp (c,cl) -> PApp (pat_of_raw metas vars c, @@ -362,8 +362,8 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda c na = Loc.tag ?loc @@ - GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda c na = CAst.make ?loc @@ + GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; @@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind + | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with @@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (_, GHole _)), _ -> PMeta None + | (None | Some { CAst.v = GHole _}), _ -> PMeta None | Some p, None -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in @@ -409,15 +409,15 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | _, PatVar na -> + | { CAst.v = PatVar na } -> name_iter (fun n -> metas := n::!metas) na; na - | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.") + | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *) - | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs -> + | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) + | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> -- cgit v1.2.3