From a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:08:44 +0000 Subject: Glob_term now mli-only, operations now in Glob_ops Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/cases.ml | 1 + pretyping/detyping.ml | 1 + pretyping/glob_ops.ml | 267 ++++++++++++++++++++++++++++++++ pretyping/glob_ops.mli | 50 ++++++ pretyping/glob_term.ml | 381 ---------------------------------------------- pretyping/glob_term.mli | 138 ----------------- pretyping/miscops.ml | 10 ++ pretyping/miscops.mli | 8 +- pretyping/pattern.ml | 1 + pretyping/pretyping.ml | 1 + pretyping/pretyping.mllib | 3 +- pretyping/redops.ml | 36 +++++ pretyping/redops.mli | 13 ++ 13 files changed, 389 insertions(+), 521 deletions(-) create mode 100644 pretyping/glob_ops.ml create mode 100644 pretyping/glob_ops.mli delete mode 100644 pretyping/glob_term.ml delete mode 100644 pretyping/glob_term.mli create mode 100644 pretyping/redops.ml create mode 100644 pretyping/redops.mli (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 7019495afb..4b7f9187fd 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -23,6 +23,7 @@ open Reductionops open Typeops open Type_errors open Glob_term +open Glob_ops open Retyping open Pretype_errors open Evarutil diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 832d32086d..c1e0d123db 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -18,6 +18,7 @@ open Inductiveops open Environ open Sign open Glob_term +open Glob_ops open Nameops open Termops open Namegen diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml new file mode 100644 index 0000000000..7a48ee9de2 --- /dev/null +++ b/pretyping/glob_ops.ml @@ -0,0 +1,267 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* loc + | PatCstr(loc,_,_,_) -> loc + +let cases_predicate_names tml = + List.flatten (List.map (function + | (tm,(na,None)) -> [na] + | (tm,(na,Some (_,_,nal))) -> na::nal) tml) + +let mkGApp loc p t = + match p with + | GApp (loc,f,l) -> GApp (loc,f,l@[t]) + | _ -> GApp (loc,p,[t]) + +let map_glob_decl_left_to_right f (na,k,obd,ty) = + let comp1 = Option.map f obd in + let comp2 = f ty in + (na,k,comp1,comp2) + +let map_glob_constr_left_to_right f = function + | GApp (loc,g,args) -> + let comp1 = f g in + let comp2 = Util.list_map_left f args in + GApp (loc,comp1,comp2) + | GLambda (loc,na,bk,ty,c) -> + let comp1 = f ty in + let comp2 = f c in + GLambda (loc,na,bk,comp1,comp2) + | GProd (loc,na,bk,ty,c) -> + let comp1 = f ty in + let comp2 = f c in + GProd (loc,na,bk,comp1,comp2) + | GLetIn (loc,na,b,c) -> + let comp1 = f b in + let comp2 = f c in + GLetIn (loc,na,comp1,comp2) + | GCases (loc,sty,rtntypopt,tml,pl) -> + let comp1 = Option.map f rtntypopt in + let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in + let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in + GCases (loc,sty,comp1,comp2,comp3) + | GLetTuple (loc,nal,(na,po),b,c) -> + let comp1 = Option.map f po in + let comp2 = f b in + let comp3 = f c in + GLetTuple (loc,nal,(na,comp1),comp2,comp3) + | GIf (loc,c,(na,po),b1,b2) -> + let comp1 = Option.map f po in + let comp2 = f b1 in + let comp3 = f b2 in + GIf (loc,f c,(na,comp1),comp2,comp3) + | GRec (loc,fk,idl,bl,tyl,bv) -> + let comp1 = Array.map (Util.list_map_left (map_glob_decl_left_to_right f)) bl in + let comp2 = Array.map f tyl in + let comp3 = Array.map f bv in + GRec (loc,fk,idl,comp1,comp2,comp3) + | GCast (loc,c,k) -> + let comp1 = f c in + let comp2 = Miscops.map_cast_type f k in + GCast (loc,comp1,comp2) + | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x + +let map_glob_constr = map_glob_constr_left_to_right + +let fold_glob_constr f acc = + let rec fold acc = function + | GVar _ -> acc + | GApp (_,c,args) -> List.fold_left fold (fold acc c) args + | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> + fold (fold acc b) c + | GCases (_,_,rtntypopt,tml,pl) -> + List.fold_left fold_pattern + (List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml)) + pl + | GLetTuple (_,_,rtntyp,b,c) -> + fold (fold (fold_return_type acc rtntyp) b) c + | GIf (_,c,rtntyp,b1,b2) -> + fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2 + | GRec (_,_,_,bl,tyl,bv) -> + let acc = Array.fold_left + (List.fold_left (fun acc (na,k,bbd,bty) -> + fold (Option.fold_left fold acc bbd) bty)) acc bl in + Array.fold_left fold (Array.fold_left fold acc tyl) bv + | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc + + and fold_pattern acc (_,idl,p,c) = fold acc c + + and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt + + in fold acc + +let iter_glob_constr f = fold_glob_constr (fun () -> f) () + +let occur_glob_constr id = + let rec occur = function + | GVar (loc,id') -> id = id' + | GApp (loc,f,args) -> (occur f) or (List.exists occur args) + | GLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | GProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) + | GLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) + | GCases (loc,sty,rtntypopt,tml,pl) -> + (occur_option rtntypopt) + or (List.exists (fun (tm,_) -> occur tm) tml) + or (List.exists occur_pattern pl) + | GLetTuple (loc,nal,rtntyp,b,c) -> + occur_return_type rtntyp id + or (occur b) or (not (List.mem (Name id) nal) & (occur c)) + | GIf (loc,c,rtntyp,b1,b2) -> + occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) + | GRec (loc,fk,idl,bl,tyl,bv) -> + not (array_for_all4 (fun fid bl ty bd -> + let rec occur_fix = function + [] -> not (occur ty) && (fid=id or not(occur bd)) + | (na,k,bbd,bty)::bl -> + not (occur bty) && + (match bbd with + Some bd -> not (occur bd) + | _ -> true) && + (na=Name id or not(occur_fix bl)) in + occur_fix bl) + idl bl tyl bv) + | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false) + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false + + and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) + + and occur_option = function None -> false | Some p -> occur p + + and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt + + in occur + + +let add_name_to_ids set na = + match na with + | Anonymous -> set + | Name id -> Idset.add id set + +let free_glob_vars = + let rec vars bounded vs = function + | GVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs + | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + let vs' = vars bounded vs ty in + let bounded' = add_name_to_ids bounded na in + vars bounded' vs' c + | GCases (loc,sty,rtntypopt,tml,pl) -> + let vs1 = vars_option bounded vs rtntypopt in + let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in + List.fold_left (vars_pattern bounded) vs2 pl + | GLetTuple (loc,nal,rtntyp,b,c) -> + let vs1 = vars_return_type bounded vs rtntyp in + let vs2 = vars bounded vs1 b in + let bounded' = List.fold_left add_name_to_ids bounded nal in + vars bounded' vs2 c + | GIf (loc,c,rtntyp,b1,b2) -> + let vs1 = vars_return_type bounded vs rtntyp in + let vs2 = vars bounded vs1 c in + let vs3 = vars bounded vs2 b1 in + vars bounded vs3 b2 + | GRec (loc,fk,idl,bl,tyl,bv) -> + let bounded' = Array.fold_right Idset.add idl bounded in + let vars_fix i vs fid = + let vs1,bounded1 = + List.fold_left + (fun (vs,bounded) (na,k,bbd,bty) -> + let vs' = vars_option bounded vs bbd in + let vs'' = vars bounded vs' bty in + let bounded' = add_name_to_ids bounded na in + (vs'',bounded') + ) + (vs,bounded') + bl.(i) + in + let vs2 = vars bounded1 vs1 tyl.(i) in + vars bounded1 vs2 bv.(i) + in + array_fold_left_i vars_fix vs idl + | GCast (loc,c,k) -> let v = vars bounded vs c in + (match k with CastConv t | CastVM t -> vars bounded v t | _ -> v) + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs + + and vars_pattern bounded vs (loc,idl,p,c) = + let bounded' = List.fold_right Idset.add idl bounded in + vars bounded' vs c + + and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p + + and vars_return_type bounded vs (na,tyopt) = + let bounded' = add_name_to_ids bounded na in + vars_option bounded' vs tyopt + in + fun rt -> + let vs = vars Idset.empty Idset.empty rt in + Idset.elements vs + + +let loc_of_glob_constr = function + | GRef (loc,_) -> loc + | GVar (loc,_) -> loc + | GEvar (loc,_,_) -> loc + | GPatVar (loc,_) -> loc + | GApp (loc,_,_) -> loc + | GLambda (loc,_,_,_,_) -> loc + | GProd (loc,_,_,_,_) -> loc + | GLetIn (loc,_,_,_) -> loc + | GCases (loc,_,_,_,_) -> loc + | GLetTuple (loc,_,_,_,_) -> loc + | GIf (loc,_,_,_,_) -> loc + | GRec (loc,_,_,_,_,_) -> loc + | GSort (loc,_) -> loc + | GHole (loc,_) -> loc + | GCast (loc,_,_) -> loc + +(**********************************************************************) +(* Conversion from glob_constr to cases pattern, if possible *) + +let rec cases_pattern_of_glob_constr na = function + | GVar (loc,id) when na<>Anonymous -> + (* Unable to manage the presence of both an alias and a variable *) + raise Not_found + | GVar (loc,id) -> PatVar (loc,Name id) + | GHole (loc,_) -> PatVar (loc,na) + | GRef (loc,ConstructRef cstr) -> + PatCstr (loc,cstr,[],na) + | GApp (loc,GRef (_,ConstructRef cstr),l) -> + PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | _ -> raise Not_found + +(* Turn a closed cases pattern into a glob_constr *) +let rec glob_constr_of_closed_cases_pattern_aux = function + | PatCstr (loc,cstr,[],Anonymous) -> + GRef (loc,ConstructRef cstr) + | PatCstr (loc,cstr,l,Anonymous) -> + let ref = GRef (loc,ConstructRef cstr) in + GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) + | _ -> raise Not_found + +let glob_constr_of_closed_cases_pattern = function + | PatCstr (loc,cstr,l,na) -> + na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) + | _ -> + raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli new file mode 100644 index 0000000000..19d003a92c --- /dev/null +++ b/pretyping/glob_ops.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* loc + +val cases_predicate_names : tomatch_tuples -> name list + +(** Apply one argument to a glob_constr *) +val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr + +val map_glob_constr : + (glob_constr -> glob_constr) -> glob_constr -> glob_constr + +(** Ensure traversal from left to right *) +val map_glob_constr_left_to_right : + (glob_constr -> glob_constr) -> glob_constr -> glob_constr + +val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit +val occur_glob_constr : identifier -> glob_constr -> bool +val free_glob_vars : glob_constr -> identifier list +val loc_of_glob_constr : glob_constr -> loc + +(** Conversion from glob_constr to cases pattern, if possible + + Take the current alias as parameter, + @raise Not_found if translation is impossible *) +val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern + +val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml deleted file mode 100644 index 466e73b8ea..0000000000 --- a/pretyping/glob_term.ml +++ /dev/null @@ -1,381 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* loc - | PatCstr(loc,_,_,_) -> loc - -type glob_constr = - | GRef of (loc * global_reference) - | GVar of (loc * identifier) - | GEvar of loc * existential_key * glob_constr list option - | GPatVar of loc * (bool * patvar) (* Used for patterns only *) - | GApp of loc * glob_constr * glob_constr list - | GLambda of loc * name * binding_kind * glob_constr * glob_constr - | GProd of loc * name * binding_kind * glob_constr * glob_constr - | GLetIn of loc * name * glob_constr * glob_constr - | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses - | GLetTuple of loc * name list * (name * glob_constr option) * - glob_constr * glob_constr - | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr - | GRec of loc * fix_kind * identifier array * glob_decl list array * - glob_constr array * glob_constr array - | GSort of loc * glob_sort - | GHole of (loc * Evar_kinds.t) - | GCast of loc * glob_constr * glob_constr cast_type - -and glob_decl = name * binding_kind * glob_constr option * glob_constr - -and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option - -and fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) - | GCoFix of int - -and predicate_pattern = - name * (loc * inductive * name list) option - -and tomatch_tuple = (glob_constr * predicate_pattern) - -and tomatch_tuples = tomatch_tuple list - -and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) - -and cases_clauses = cases_clause list - -let cases_predicate_names tml = - List.flatten (List.map (function - | (tm,(na,None)) -> [na] - | (tm,(na,Some (_,_,nal))) -> na::nal) tml) - -let mkGApp loc p t = - match p with - | GApp (loc,f,l) -> GApp (loc,f,l@[t]) - | _ -> GApp (loc,p,[t]) - -let map_glob_decl_left_to_right f (na,k,obd,ty) = - let comp1 = Option.map f obd in - let comp2 = f ty in - (na,k,comp1,comp2) - -let map_glob_constr_left_to_right f = function - | GApp (loc,g,args) -> - let comp1 = f g in - let comp2 = Util.list_map_left f args in - GApp (loc,comp1,comp2) - | GLambda (loc,na,bk,ty,c) -> - let comp1 = f ty in - let comp2 = f c in - GLambda (loc,na,bk,comp1,comp2) - | GProd (loc,na,bk,ty,c) -> - let comp1 = f ty in - let comp2 = f c in - GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,c) -> - let comp1 = f b in - let comp2 = f c in - GLetIn (loc,na,comp1,comp2) - | GCases (loc,sty,rtntypopt,tml,pl) -> - let comp1 = Option.map f rtntypopt in - let comp2 = Util.list_map_left (fun (tm,x) -> (f tm,x)) tml in - let comp3 = Util.list_map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in - GCases (loc,sty,comp1,comp2,comp3) - | GLetTuple (loc,nal,(na,po),b,c) -> - let comp1 = Option.map f po in - let comp2 = f b in - let comp3 = f c in - GLetTuple (loc,nal,(na,comp1),comp2,comp3) - | GIf (loc,c,(na,po),b1,b2) -> - let comp1 = Option.map f po in - let comp2 = f b1 in - let comp3 = f b2 in - GIf (loc,f c,(na,comp1),comp2,comp3) - | GRec (loc,fk,idl,bl,tyl,bv) -> - let comp1 = Array.map (Util.list_map_left (map_glob_decl_left_to_right f)) bl in - let comp2 = Array.map f tyl in - let comp3 = Array.map f bv in - GRec (loc,fk,idl,comp1,comp2,comp3) - | GCast (loc,c,k) -> - let comp1 = f c in - let comp2 = Miscops.map_cast_type f k in - GCast (loc,comp1,comp2) - | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x - -let map_glob_constr = map_glob_constr_left_to_right - -(* -let name_app f e = function - | Name id -> let (id, e) = f id e in (Name id, e) - | Anonymous -> Anonymous, e - -let fold_ident g idl e = - let (idl,e) = - Array.fold_right - (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e) - in (Array.of_list idl,e) - -let map_glob_constr_with_binders_loc loc g f e = function - | GVar (_,id) -> GVar (loc,id) - | GApp (_,a,args) -> GApp (loc,f e a, List.map (f e) args) - | GLambda (_,na,ty,c) -> - let na,e = name_app g e na in GLambda (loc,na,f e ty,f e c) - | GProd (_,na,ty,c) -> - let na,e = name_app g e na in GProd (loc,na,f e ty,f e c) - | GLetIn (_,na,b,c) -> - let na,e = name_app g e na in GLetIn (loc,na,f e b,f e c) - | GCases (_,tyopt,tml,pl) -> - (* We don't modify pattern variable since we don't traverse patterns *) - let g' id e = snd (g id e) in - let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in - GCases - (loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl) - | GRec (_,fk,idl,tyl,bv) -> - let idl',e' = fold_ident g idl e in - GRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv) - | GCast (_,c,t) -> GCast (loc,f e c,f e t) - | GSort (_,x) -> GSort (loc,x) - | GHole (_,x) -> GHole (loc,x) - | GRef (_,x) -> GRef (loc,x) - | GEvar (_,x,l) -> GEvar (loc,x,l) - | GPatVar (_,x) -> GPatVar (loc,x) -*) - -let fold_glob_constr f acc = - let rec fold acc = function - | GVar _ -> acc - | GApp (_,c,args) -> List.fold_left fold (fold acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> - fold (fold acc b) c - | GCases (_,_,rtntypopt,tml,pl) -> - List.fold_left fold_pattern - (List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml)) - pl - | GLetTuple (_,_,rtntyp,b,c) -> - fold (fold (fold_return_type acc rtntyp) b) c - | GIf (_,c,rtntyp,b1,b2) -> - fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2 - | GRec (_,_,_,bl,tyl,bv) -> - let acc = Array.fold_left - (List.fold_left (fun acc (na,k,bbd,bty) -> - fold (Option.fold_left fold acc bbd) bty)) acc bl in - Array.fold_left fold (Array.fold_left fold acc tyl) bv - | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc - - and fold_pattern acc (_,idl,p,c) = fold acc c - - and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt - - in fold acc - -let iter_glob_constr f = fold_glob_constr (fun () -> f) () - -let occur_glob_constr id = - let rec occur = function - | GVar (loc,id') -> id = id' - | GApp (loc,f,args) -> (occur f) or (List.exists occur args) - | GLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) - | GProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c)) - | GLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> - (occur_option rtntypopt) - or (List.exists (fun (tm,_) -> occur tm) tml) - or (List.exists occur_pattern pl) - | GLetTuple (loc,nal,rtntyp,b,c) -> - occur_return_type rtntyp id - or (occur b) or (not (List.mem (Name id) nal) & (occur c)) - | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> - not (array_for_all4 (fun fid bl ty bd -> - let rec occur_fix = function - [] -> not (occur ty) && (fid=id or not(occur bd)) - | (na,k,bbd,bty)::bl -> - not (occur bty) && - (match bbd with - Some bd -> not (occur bd) - | _ -> true) && - (na=Name id or not(occur_fix bl)) in - occur_fix bl) - idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - - and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c) - - and occur_option = function None -> false | Some p -> occur p - - and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt - - in occur - - -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Idset.add id set - -let free_glob_vars = - let rec vars bounded vs = function - | GVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs - | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> - let vs' = vars bounded vs ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bounded vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in - List.fold_left (vars_pattern bounded) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 b in - let bounded' = List.fold_left add_name_to_ids bounded nal in - vars bounded' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 c in - let vs3 = vars bounded vs2 b1 in - vars bounded vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bounded' = Array.fold_right Idset.add idl bounded in - let vars_fix i vs fid = - let vs1,bounded1 = - List.fold_left - (fun (vs,bounded) (na,k,bbd,bty) -> - let vs' = vars_option bounded vs bbd in - let vs'' = vars bounded vs' bty in - let bounded' = add_name_to_ids bounded na in - (vs'',bounded') - ) - (vs,bounded') - bl.(i) - in - let vs2 = vars bounded1 vs1 tyl.(i) in - vars bounded1 vs2 bv.(i) - in - array_fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bounded vs (loc,idl,p,c) = - let bounded' = List.fold_right Idset.add idl bounded in - vars bounded' vs c - - and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p - - and vars_return_type bounded vs (na,tyopt) = - let bounded' = add_name_to_ids bounded na in - vars_option bounded' vs tyopt - in - fun rt -> - let vs = vars Idset.empty Idset.empty rt in - Idset.elements vs - - -let loc_of_glob_constr = function - | GRef (loc,_) -> loc - | GVar (loc,_) -> loc - | GEvar (loc,_,_) -> loc - | GPatVar (loc,_) -> loc - | GApp (loc,_,_) -> loc - | GLambda (loc,_,_,_,_) -> loc - | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_) -> loc - | GCases (loc,_,_,_,_) -> loc - | GLetTuple (loc,_,_,_,_) -> loc - | GIf (loc,_,_,_,_) -> loc - | GRec (loc,_,_,_,_,_) -> loc - | GSort (loc,_) -> loc - | GHole (loc,_) -> loc - | GCast (loc,_,_) -> loc - -(**********************************************************************) -(* Conversion from glob_constr to cases pattern, if possible *) - -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) when na<>Anonymous -> - (* Unable to manage the presence of both an alias and a variable *) - raise Not_found - | GVar (loc,id) -> PatVar (loc,Name id) - | GHole (loc,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) - | _ -> raise Not_found - -(* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux = function - | PatCstr (loc,cstr,[],Anonymous) -> - GRef (loc,ConstructRef cstr) - | PatCstr (loc,cstr,l,Anonymous) -> - let ref = GRef (loc,ConstructRef cstr) in - GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) - | _ -> raise Not_found - -let glob_constr_of_closed_cases_pattern = function - | PatCstr (loc,cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) - | _ -> - raise Not_found - -(**********************************************************************) -(* Reduction expressions *) - -type 'a glob_red_flag = { - rBeta : bool; - rIota : bool; - rZeta : bool; - rDelta : bool; (* true = delta all but rConst; false = delta only on rConst*) - rConst : 'a list -} - -let all_flags = - {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} - -type ('a,'b,'c) red_expr_gen = - | Red of bool - | Hnf - | Simpl of 'c with_occurrences option - | Cbv of 'b glob_red_flag - | Lazy of 'b glob_red_flag - | Unfold of 'b with_occurrences list - | Fold of 'a list - | Pattern of 'a with_occurrences list - | ExtraRedExpr of string - | CbvVm of 'c with_occurrences option - -type ('a,'b,'c) may_eval = - | ConstrTerm of 'a - | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (loc * identifier) * 'a - | ConstrTypeOf of 'a diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli deleted file mode 100644 index f654925ef8..0000000000 --- a/pretyping/glob_term.mli +++ /dev/null @@ -1,138 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* loc - -type glob_constr = - | GRef of (loc * global_reference) - | GVar of (loc * identifier) - | GEvar of loc * existential_key * glob_constr list option - | GPatVar of loc * (bool * patvar) (** Used for patterns only *) - | GApp of loc * glob_constr * glob_constr list - | GLambda of loc * name * binding_kind * glob_constr * glob_constr - | GProd of loc * name * binding_kind * glob_constr * glob_constr - | GLetIn of loc * name * glob_constr * glob_constr - | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses - (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in - [MatchStyle]) *) - - | GLetTuple of loc * name list * (name * glob_constr option) * - glob_constr * glob_constr - | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr - | GRec of loc * fix_kind * identifier array * glob_decl list array * - glob_constr array * glob_constr array - | GSort of loc * glob_sort - | GHole of (loc * Evar_kinds.t) - | GCast of loc * glob_constr * glob_constr cast_type - -and glob_decl = name * binding_kind * glob_constr option * glob_constr - -and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option - -and fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) - | GCoFix of int - -and predicate_pattern = - name * (loc * inductive * name list) option - (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) - -and tomatch_tuple = (glob_constr * predicate_pattern) - -and tomatch_tuples = tomatch_tuple list - -and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) -(** [(p,il,cl,t)] = "|'cl' => 't'" where FV(t) \subset il *) - -and cases_clauses = cases_clause list - -val cases_predicate_names : tomatch_tuples -> name list - -(* Apply one argument to a glob_constr *) -val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr - -val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr - -(* Ensure traversal from left to right *) -val map_glob_constr_left_to_right : - (glob_constr -> glob_constr) -> glob_constr -> glob_constr - -(* -val map_glob_constr_with_binders_loc : loc -> - (identifier -> 'a -> identifier * 'a) -> - ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr -*) - -val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a -val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit -val occur_glob_constr : identifier -> glob_constr -> bool -val free_glob_vars : glob_constr -> identifier list -val loc_of_glob_constr : glob_constr -> loc - -(** Conversion from glob_constr to cases pattern, if possible - - Take the current alias as parameter, - @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern - -val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr - -(** {6 Reduction expressions} *) - -type 'a glob_red_flag = { - rBeta : bool; - rIota : bool; - rZeta : bool; - rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) - rConst : 'a list -} - -val all_flags : 'a glob_red_flag - -type ('a,'b,'c) red_expr_gen = - | Red of bool - | Hnf - | Simpl of 'c with_occurrences option - | Cbv of 'b glob_red_flag - | Lazy of 'b glob_red_flag - | Unfold of 'b with_occurrences list - | Fold of 'a list - | Pattern of 'a with_occurrences list - | ExtraRedExpr of string - | CbvVm of 'c with_occurrences option - -type ('a,'b,'c) may_eval = - | ConstrTerm of 'a - | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of (loc * identifier) * 'a - | ConstrTypeOf of 'a diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 2528d57f30..0f659f1b65 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -10,6 +10,8 @@ open Misctypes open Pp open Nameops +(** Mapping [cast_type] *) + let map_cast_type f = function | CastConv a -> CastConv (f a) | CastVM a -> CastVM (f a) @@ -41,3 +43,11 @@ and pr_or_and_intro_pattern = function str "[" ++ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll) ++ str "]" + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index b8f6f68606..123d307de9 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -8,11 +8,17 @@ open Misctypes -val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type +(** Mapping [cast_type] *) +val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Printing of [intro_pattern] *) val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds + +(** Printing of [move_location] *) + +val pr_move_location : + ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index ef81aa4d32..08e5ac75c9 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -13,6 +13,7 @@ open Libnames open Nameops open Term open Glob_term +open Glob_ops open Environ open Nametab open Pp diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 82f030ae09..b241336e77 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -42,6 +42,7 @@ open Recordops open Evarutil open Pretype_errors open Glob_term +open Glob_ops open Evarconv open Pattern open Misctypes diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index e520602db2..fca2d714f8 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -15,7 +15,8 @@ Evarconv Arguments_renaming Typing Miscops -Glob_term +Glob_ops +Redops Pattern Matching Tacred diff --git a/pretyping/redops.ml b/pretyping/redops.ml new file mode 100644 index 0000000000..53ac6e6c87 --- /dev/null +++ b/pretyping/redops.ml @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FIota :: lf -> add_flag { red with rIota = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + Errors.error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag { red with rConst = Util.list_union red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] & not red.rDelta then + Errors.error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag + { red with rConst = Util.list_union red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + l + + +let all_flags = + {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} diff --git a/pretyping/redops.mli b/pretyping/redops.mli new file mode 100644 index 0000000000..b555970984 --- /dev/null +++ b/pretyping/redops.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a glob_red_flag + +val all_flags : 'a glob_red_flag -- cgit v1.2.3