diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 300 |
1 files changed, 11 insertions, 289 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index c64d3aa266..ecfb766ff4 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,294 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i*) -open Pp -open CErrors -open Util -open Names -open Nameops -open Libnames -open Misctypes -open Constrexpr open Constrexpr_ops -(*i*) - -let asymmetric_patterns = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "no parameters in constructors"; - Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !asymmetric_patterns); - Goptions.optwrite = (fun a -> asymmetric_patterns:=a); -} - -(**********************************************************************) -(* Miscellaneous *) - -let error_invalid_pattern_notation ?loc () = - user_err ?loc (str "Invalid notation for pattern.") - -(* Legacy functions *) -let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y - -(**********************************************************************) -(* Functions on constr_expr *) - -let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false - -let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with - | CPatRecord l -> - List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (pat,id) -> f id a - | CPatOr (patl) -> - List.fold_left (cases_pattern_fold_names f) a patl - | CPatCstr (_,patl1,patl2) -> - List.fold_left (cases_pattern_fold_names f) - (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,(patl,patll),patl') -> - List.fold_left (cases_pattern_fold_names f) - (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' - | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a - | CPatPrim _ | CPatAtom _ -> a - | CPatCast ({CAst.loc},_) -> - CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" - (Pp.strbrk "Casts are not supported here.") - -let ids_of_pattern = - cases_pattern_fold_names Id.Set.add Id.Set.empty - -let ids_of_pattern_list = - List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) - Id.Set.empty - -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - -let ids_of_cases_tomatch tms = - List.fold_right - (fun (_, ona, indnal) l -> - Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) - indnal - (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) - tms Id.Set.empty - -let rec fold_constr_expr_binders g f n acc b = function - | (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_constr_expr_binders g f n' acc b l) t - | [] -> - f n acc b - -let rec fold_local_binders g f n acc b = function - | CLocalAssum (nal,bk,t)::l -> - let nal = snd (List.split nal) in - let n' = List.fold_right (Name.fold_right g) nal n in - f n (fold_local_binders g f n' acc b l) t - | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t - | CLocalPattern (_,(pat,t))::l -> - let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in - Option.fold_left (f n) acc t - | [] -> - f n acc b - -let fold_constr_expr_with_binders g f n acc = CAst.with_val (function - | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l - | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) - | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (na,a,t,b) -> - f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b - | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a - | CNotation (_,(l,ll,bll)) -> - (* The following is an approximation: we don't know exactly if - an ident is binding nor to which subterms bindings apply *) - let acc = List.fold_left (f n) acc (l@List.flatten ll) in - List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll - | CGeneralization (_,_,c) -> f n acc c - | CDelimiters (_,a) -> f n acc a - | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> - acc - | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l - | CCases (sty,rtnpo,al,bl) -> - let ids = ids_of_cases_tomatch al in - let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in - let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in - List.fold_right (fun (loc,(patl,rhs)) acc -> - let ids = ids_of_pattern_list patl in - f (Id.Set.fold g ids n) acc rhs) bl acc - | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (Name.fold_right g)) nal n in - f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c - | CIf (c,(ona,po),b1,b2) -> - let acc = f n (f n (f n acc b1) b2) c in - Option.fold_left - (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po - | CFix (_,l) -> - let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in - List.fold_right (fun (_,(_,o),lb,t,c) acc -> - fold_local_binders g f n' - (fold_local_binders g f n acc t lb) c lb) l acc - | CCoFix (_,_) -> - Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc - ) - -let free_vars_of_constr_expr c = - let rec aux bdvars l = function - | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l - | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c - in aux [] Id.Set.empty c - -let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) - -(* Interpret the index of a recursion order annotation *) - -let split_at_annot bl na = - let names = List.map snd (names_of_local_assums bl) in - match na with - | None -> - begin match names with - | [] -> user_err (Pp.str "A fixpoint needs at least one parameter.") - | _ -> ([], bl) - end - | Some (loc, id) -> - let rec aux acc = function - | CLocalAssum (bls, k, t) as x :: rest -> - let test (_, na) = match na with - | Name id' -> Id.equal id id' - | Anonymous -> false - in - let l, r = List.split_when test bls in - begin match r with - | [] -> aux (x :: acc) rest - | _ -> - let ans = match l with - | [] -> acc - | _ -> CLocalAssum (l, k, t) :: acc - in - (List.rev ans, CLocalAssum (r, k, t) :: rest) - end - | CLocalDef ((_,na),_,_) as x :: rest -> - if Name.equal (Name id) na then - user_err ?loc - (Id.print id ++ str" must be a proper parameter and not a local definition.") - else - aux (x :: acc) rest - | CLocalPattern (_,_) :: rest -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") - | [] -> - user_err ?loc - (str "No parameter named " ++ Id.print id ++ str".") - in aux [] bl - -(* Used in correctness and interface *) - -let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e - -let map_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_local_binders f g e bl = - (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) - let h (e,bl) = function - CLocalAssum(nal,k,ty) -> - (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) - | CLocalDef((loc,na),c,ty) -> - (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) - | CLocalPattern (loc,(pat,t)) -> - let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in - let (e,rbl) = List.fold_left h (e,[]) bl in - (e, List.rev rbl) - -let map_constr_expr_with_binders g f e = CAst.map (function - | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l) - | CApp ((p,a),l) -> - CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l) - | CProdN (bl,b) -> - let (e,bl) = map_binders f g e bl in CProdN (bl,f e b) - | CLambdaN (bl,b) -> - let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) - | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) - | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) - | CNotation (n,(l,ll,bll)) -> - (* This is an approximation because we don't know what binds what *) - CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, - List.map (fun bl -> snd (map_local_binders f g e bl)) bll)) - | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c) - | CDelimiters (s,a) -> CDelimiters (s,f e a) - | CHole _ | CEvar _ | CPatVar _ | CSort _ - | CPrim _ | CRef _ as x -> x - | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l) - | CCases (sty,rtnpo,a,bl) -> - let bl = List.map (fun (loc,(patl,rhs)) -> - let ids = ids_of_pattern_list patl in - (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in - let ids = ids_of_cases_tomatch a in - let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in - CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) - | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (Name.fold_right g)) nal e in - let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) - | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in - CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) - | CFix (id,dl) -> - CFix (id,List.map (fun (id,n,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - (* Note: fix names should be inserted before the arguments... *) - let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,n,bl',t',d')) dl) - | CCoFix (id,dl) -> - CCoFix (id,List.map (fun (id,bl,t,d) -> - let (e',bl') = map_local_binders f g e bl in - let t' = f e' t in - let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in - let d' = f e'' d in - (id,bl',t',d')) dl) - ) - -(* Used in constrintern *) -let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x -> - (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x) - | c -> map_constr_expr_with_binders Id.Map.remove - replace_vars_constr_expr l c - -(* Returns the ranges of locs of the notation that are not occupied by args *) -(* and which are then occupied by proper symbols of the notation (or spaces) *) - -let locs_of_notation ?loc locs ntn = - let unloc loc = Option.cata Loc.unloc (0,0) loc in - let (bl, el) = unloc loc in - let locs = List.map unloc locs in - let rec aux pos = function - | [] -> if Int.equal pos el then [] else [(pos,el)] - | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l - in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs) - -let ntn_loc ?loc (args,argslist,binderslist) = - locs_of_notation ?loc - (List.map constr_loc (args@List.flatten argslist)@ - List.map local_binders_loc binderslist) - -let patntn_loc ?loc (args,argslist) = - locs_of_notation ?loc - (List.map cases_pattern_expr_loc (args@List.flatten argslist)) +let asymmetric_patterns = asymmetric_patterns +let error_invalid_pattern_notation = error_invalid_pattern_notation +let split_at_annot = split_at_annot +let ntn_loc = ntn_loc +let patntn_loc = patntn_loc +let map_constr_expr_with_binders = map_constr_expr_with_binders +let fold_constr_expr_with_binders = fold_constr_expr_with_binders +let ids_of_cases_indtype = ids_of_cases_indtype +let occur_var_constr_expr = occur_var_constr_expr +let free_vars_of_constr_expr = free_vars_of_constr_expr +let replace_vars_constr_expr = replace_vars_constr_expr |