diff options
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rw-r--r-- | interp/constrintern.ml | 1 | ||||
| -rw-r--r-- | interp/interp.mllib | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 20 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 806 | ||||
| -rw-r--r-- | interp/notation_ops.mli | 63 | ||||
| -rw-r--r-- | interp/reserve.ml | 6 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.ml | 783 | ||||
| -rw-r--r-- | interp/topconstr.mli | 45 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/grammar.mllib | 1 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
17 files changed, 896 insertions, 850 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 299ea8d79..c8a43c866 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -23,6 +23,7 @@ open Libnames open Impargs open Constrexpr open Notation_term +open Notation_ops open Topconstr open Glob_term open Glob_ops @@ -470,7 +471,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function | (keyrule,pat,n as _rule)::rules -> try apply_notation_to_pattern dummy_loc - (match_aconstr_ind_pattern ind args pat) allscopes vars keyrule + (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with No_match -> extern_symbol_ind_pattern allscopes vars ind args rules @@ -763,7 +764,7 @@ let rec extern inctx scopes vars r = (sub_extern false scopes vars tm, (na',Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> PatVar (dummy_loc, x)) nal in - let fullargs = Topconstr.add_patterns_for_params ind args in + let fullargs = Notation_ops.add_patterns_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x))) tml in let eqns = List.map (extern_eqn inctx scopes vars) eqns in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5a1dea89e..7b5a8ebbb 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -23,6 +23,7 @@ open Pretyping open Cases open Constrexpr open Notation_term +open Notation_ops open Topconstr open Nametab open Notation diff --git a/interp/interp.mllib b/interp/interp.mllib index 546f277e4..ff2549a03 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,5 +1,6 @@ Tok Lexer +Notation_ops Topconstr Ppextend Notation diff --git a/interp/notation.ml b/interp/notation.ml index 16fdef469..f2dec3bc1 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -351,7 +351,7 @@ let find_prim_token g loc p sc = (* Try for a user-defined numerical notation *) try let (_,c),df = find_notation (notation_of_prim_token p) sc in - g (Topconstr.glob_constr_of_notation_constr loc c),df + g (Notation_ops.glob_constr_of_notation_constr loc c),df with Not_found -> (* Try for a primitive numerical notation *) let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in @@ -403,34 +403,34 @@ let uninterp_prim_token c = let (sc,numpr,_) = Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in match numpr c with - | None -> raise Topconstr.No_match + | None -> raise Notation_ops.No_match | Some n -> (sc,n) - with Not_found -> raise Topconstr.No_match + with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_ind_pattern ind args = let ref = IndRef ind in try let (sc,numpr,b) = Hashtbl.find prim_token_key_table (RefKey (canonical_gr ref)) in - if not b then raise No_match; + if not b then raise Notation_ops.No_match; let args' = List.map (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in let ref = GRef (dummy_loc,ref) in match numpr (GApp (dummy_loc,ref,args')) with - | None -> raise No_match + | None -> raise Notation_ops.No_match | Some n -> (sc,n) - with Not_found -> raise No_match + with Not_found -> raise Notation_ops.No_match let uninterp_prim_token_cases_pattern c = try let k = cases_pattern_key c in let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in - if not b then raise Topconstr.No_match; + if not b then raise Notation_ops.No_match; let na,c = glob_constr_of_closed_cases_pattern c in match numpr c with - | None -> raise Topconstr.No_match + | None -> raise Notation_ops.No_match | Some n -> (na,sc,n) - with Not_found -> raise Topconstr.No_match + with Not_found -> raise Notation_ops.No_match let availability_of_prim_token n printer_scope local_scopes = let f scope = @@ -653,7 +653,7 @@ let pr_scope_classes sc = let pr_notation_info prglob ntn c = str "\"" ++ str ntn ++ str "\" := " ++ - prglob (Topconstr.glob_constr_of_notation_constr dummy_loc c) + prglob (Notation_ops.glob_constr_of_notation_constr dummy_loc c) let pr_named_scope prglob scope sc = (if scope = default_scope then diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml new file mode 100644 index 000000000..f0a20d648 --- /dev/null +++ b/interp/notation_ops.ml @@ -0,0 +1,806 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Errors +open Util +open Names +open Nameops +open Libnames +open Misctypes +open Glob_term +open Glob_ops +open Term +open Mod_subst +open Constrexpr +open Notation_term +open Decl_kinds + +(**********************************************************************) +(* Re-interpret a notation as a glob_constr, taking care of binders *) + +let name_to_ident = function + | Anonymous -> Errors.error "This expression should be a simple identifier." + | Name id -> id + +let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na + +let rec cases_pattern_fold_map loc g e = function + | PatVar (_,na) -> + let e',na' = g e na in e', PatVar (loc,na') + | PatCstr (_,cstr,patl,na) -> + let e',na' = g e na in + let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in + e', PatCstr (loc,cstr,patl',na') + +let rec subst_glob_vars l = function + | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | GProd (loc,Name id,bk,t,c) -> + let id = + try match List.assoc id l with GVar(_,id') -> id' | _ -> id + with Not_found -> id in + GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | GLambda (loc,Name id,bk,t,c) -> + let id = + try match List.assoc id l with GVar(_,id') -> id' | _ -> id + with Not_found -> id in + GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) + | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) + +let ldots_var = id_of_string ".." + +let glob_constr_of_notation_constr_with_binders loc g f e = function + | NVar id -> GVar (loc,id) + | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) + | NList (x,y,iter,tail,swap) -> + let t = f e tail in let it = f e iter in + let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in + let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in + subst_glob_vars outerl it + | NBinderList (x,y,iter,tail) -> + let t = f e tail in let it = f e iter in + let innerl = [(ldots_var,t);(x,GVar(loc,y))] in + let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in + let outerl = [(ldots_var,inner)] in + subst_glob_vars outerl it + | NLambda (na,ty,c) -> + let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) + | NProd (na,ty,c) -> + let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) + | NLetIn (na,b,c) -> + let e',na = g e na in GLetIn (loc,na,f e b,f e' c) + | NCases (sty,rtntypopt,tml,eqnl) -> + let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> + let e',t' = match t with + | None -> e',None + | Some (ind,nal) -> + let e',nal' = List.fold_right (fun na (e',nal) -> + let e',na' = g e' na in e',na'::nal) nal (e',[]) in + e',Some (loc,ind,nal') in + let e',na' = g e' na in + (e',(f e tm,(na',t'))::tml')) tml (e,[]) in + let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in + let eqnl' = List.map (fun (patl,rhs) -> + let ((idl,e),patl) = + list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in + (loc,idl,patl,f e rhs)) eqnl in + GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') + | NLetTuple (nal,(na,po),b,c) -> + let e',nal = list_fold_map g e nal in + let e'',na = g e na in + GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) + | NIf (c,(na,po),b1,b2) -> + let e',na = g e na in + GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) + | NRec (fk,idl,dll,tl,bl) -> + let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> + let e,na = g e na in + (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in + let e',idl = array_fold_map (to_id g) e idl in + GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) + | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k) + | NSort x -> GSort (loc,x) + | NHole x -> GHole (loc,x) + | NPatVar n -> GPatVar (loc,(false,n)) + | NRef x -> GRef (loc,x) + +let rec glob_constr_of_notation_constr loc x = + let rec aux () x = + glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x + in aux () x + +(****************************************************************************) +(* Translating a glob_constr into a notation, interpreting recursive patterns *) + +let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) +let add_name r = function Anonymous -> () | Name id -> add_id r id + +let split_at_recursive_part c = + let sub = ref None in + let rec aux = function + | GApp (loc0,GVar(loc,v),c::l) when v = ldots_var -> + if !sub <> None then + (* Not narrowed enough to find only one recursive part *) + raise Not_found + else + (sub := Some c; + if l = [] then GVar (loc,ldots_var) + else GApp (loc0,GVar (loc,ldots_var),l)) + | c -> map_glob_constr aux c in + let outer_iterator = aux c in + match !sub with + | None -> (* No recursive pattern found *) raise Not_found + | Some c -> + match outer_iterator with + | GVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found + | _ -> outer_iterator, c + +let on_true_do b f c = if b then (f c; b) else b + +let compare_glob_constr f add t1 t2 = match t1,t2 with + | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 + | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) + | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 + | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 + | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> + on_true_do (f ty1 ty2 & f c1 c2) add na1 + | GHole _, GHole _ -> true + | GSort (_,s1), GSort (_,s2) -> s1 = s2 + | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 -> + on_true_do (f b1 b2 & f c1 c2) add na1 + | (GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ + | _,(GCases _ | GRec _ + | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) + -> error "Unsupported construction in recursive notations." + | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ + | GHole _ | GSort _ | GLetIn _), _ + -> false + +let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 + +let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) + +let check_is_hole id = function GHole _ -> () | t -> + user_err_loc (loc_of_glob_constr t,"", + strbrk "In recursive notation with binders, " ++ pr_id id ++ + strbrk " is expected to come without type.") + +let compare_recursive_parts found f (iterator,subc) = + let diff = ref None in + let terminator = ref None in + let rec aux c1 c2 = match c1,c2 with + | GVar(_,v), term when v = ldots_var -> + (* We found the pattern *) + assert (!terminator = None); terminator := Some term; + true + | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var -> + (* We found the pattern, but there are extra arguments *) + (* (this allows e.g. alternative (recursive) notation of application) *) + assert (!terminator = None); terminator := Some term; + list_for_all2eq aux l1 l2 + | GVar (_,x), GVar (_,y) when x<>y -> + (* We found the position where it differs *) + let lassoc = (!terminator <> None) in + let x,y = if lassoc then y,x else x,y in + !diff = None && (diff := Some (x,y,Some lassoc); true) + | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) + | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> + (* We found a binding position where it differs *) + check_is_hole x t_x; + check_is_hole y t_y; + !diff = None && (diff := Some (x,y,None); aux c term) + | _ -> + compare_glob_constr aux (add_name found) c1 c2 in + if aux iterator subc then + match !diff with + | None -> + let loc1 = loc_of_glob_constr iterator in + let loc2 = loc_of_glob_constr (Option.get !terminator) in + (* Here, we would need a loc made of several parts ... *) + user_err_loc (subtract_loc loc1 loc2,"", + str "Both ends of the recursive pattern are the same.") + | Some (x,y,Some lassoc) -> + let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in + let iterator = + f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator + else iterator) in + (* found have been collected by compare_constr *) + found := newfound; + NList (x,y,iterator,f (Option.get !terminator),lassoc) + | Some (x,y,None) -> + let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in + let iterator = f iterator in + (* found have been collected by compare_constr *) + found := newfound; + NBinderList (x,y,iterator,f (Option.get !terminator)) + else + raise Not_found + +let notation_constr_and_vars_of_glob_constr a = + let found = ref ([],[],[]) in + let rec aux c = + let keepfound = !found in + (* n^2 complexity but small and done only once per notation *) + try compare_recursive_parts found aux' (split_at_recursive_part c) + with Not_found -> + found := keepfound; + match c with + | GApp (_,GVar (loc,f),[c]) when f = ldots_var -> + (* Fall on the second part of the recursive pattern w/o having + found the first part *) + user_err_loc (loc,"", + str "Cannot find where the recursive pattern starts.") + | c -> + aux' c + and aux' = function + | GVar (_,id) -> add_id found id; NVar id + | GApp (_,g,args) -> NApp (aux g, List.map aux args) + | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) + | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) + | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) + | GCases (_,sty,rtntypopt,tml,eqnl) -> + let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in + NCases (sty,Option.map aux rtntypopt, + List.map (fun (tm,(na,x)) -> + add_name found na; + Option.iter + (fun (_,_,nl) -> List.iter (add_name found) nl) x; + (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml, + List.map f eqnl) + | GLetTuple (loc,nal,(na,po),b,c) -> + add_name found na; + List.iter (add_name found) nal; + NLetTuple (nal,(na,Option.map aux po),aux b,aux c) + | GIf (loc,c,(na,po),b1,b2) -> + add_name found na; + NIf (aux c,(na,Option.map aux po),aux b1,aux b2) + | GRec (_,fk,idl,dll,tl,bl) -> + Array.iter (add_id found) idl; + let dll = Array.map (List.map (fun (na,bk,oc,b) -> + if bk <> Explicit then + error "Binders marked as implicit not allowed in notations."; + add_name found na; (na,Option.map aux oc,aux b))) dll in + NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) + | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) + | GSort (_,s) -> NSort s + | GHole (_,w) -> NHole w + | GRef (_,r) -> NRef r + | GPatVar (_,(_,n)) -> NPatVar n + | GEvar _ -> + error "Existential variables not allowed in notations." + + in + let t = aux a in + (* Side effect *) + t, !found + +let rec list_rev_mem_assoc x = function + | [] -> false + | (_,x')::l -> x = x' || list_rev_mem_assoc x l + +let check_variables vars recvars (found,foundrec,foundrecbinding) = + let useless_vars = List.map snd recvars in + let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in + let check_recvar x = + if List.mem x found then + errorlabstrm "" (pr_id x ++ + strbrk " should only be used in the recursive part of a pattern.") in + List.iter (fun (x,y) -> check_recvar x; check_recvar y) + (foundrec@foundrecbinding); + let check_bound x = + if not (List.mem x found) then + if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding + or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding + then + error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.") + else + error ((string_of_id x)^" is unbound in the right-hand side.") in + let check_pair s x y where = + if not (List.mem (x,y) where) then + errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ + str " position as part of a recursive pattern.") in + let check_type (x,typ) = + match typ with + | NtnInternTypeConstr -> + begin + try check_pair "term" x (List.assoc x recvars) foundrec + with Not_found -> check_bound x + end + | NtnInternTypeBinder -> + begin + try check_pair "binding" x (List.assoc x recvars) foundrecbinding + with Not_found -> check_bound x + end + | NtnInternTypeIdent -> check_bound x in + List.iter check_type vars + +let notation_constr_of_glob_constr vars recvars a = + let a,found = notation_constr_and_vars_of_glob_constr a in + check_variables vars recvars found; + a + +(* Substitution of kernel names, avoiding a list of bound identifiers *) + +let notation_constr_of_constr avoiding t = + notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) + +let rec subst_pat subst pat = + match pat with + | PatVar _ -> pat + | PatCstr (loc,((kn,i),j),cpl,n) -> + let kn' = subst_ind subst kn + and cpl' = list_smartmap (subst_pat subst) cpl in + if kn' == kn && cpl' == cpl then pat else + PatCstr (loc,((kn',i),j),cpl',n) + +let rec subst_notation_constr subst bound raw = + match raw with + | NRef ref -> + let ref',t = subst_global subst ref in + if ref' == ref then raw else + notation_constr_of_constr bound t + + | NVar _ -> raw + + | NApp (r,rl) -> + let r' = subst_notation_constr subst bound r + and rl' = list_smartmap (subst_notation_constr subst bound) rl in + if r' == r && rl' == rl then raw else + NApp(r',rl') + + | NList (id1,id2,r1,r2,b) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + NList (id1,id2,r1',r2',b) + + | NLambda (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + NLambda (n,r1',r2') + + | NProd (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + NProd (n,r1',r2') + + | NBinderList (id1,id2,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + NBinderList (id1,id2,r1',r2') + + | NLetIn (n,r1,r2) -> + let r1' = subst_notation_constr subst bound r1 + and r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && r2' == r2 then raw else + NLetIn (n,r1',r2') + + | NCases (sty,rtntypopt,rl,branches) -> + let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt + and rl' = list_smartmap + (fun (a,(n,signopt) as x) -> + let a' = subst_notation_constr subst bound a in + let signopt' = Option.map (fun ((indkn,i),nal as z) -> + let indkn' = subst_ind subst indkn in + if indkn == indkn' then z else ((indkn',i),nal)) signopt in + if a' == a && signopt' == signopt then x else (a',(n,signopt'))) + rl + and branches' = list_smartmap + (fun (cpl,r as branch) -> + let cpl' = list_smartmap (subst_pat subst) cpl + and r' = subst_notation_constr subst bound r in + if cpl' == cpl && r' == r then branch else + (cpl',r')) + branches + in + if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & + rl' == rl && branches' == branches then raw else + NCases (sty,rtntypopt',rl',branches') + + | NLetTuple (nal,(na,po),b,c) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b' = subst_notation_constr subst bound b + and c' = subst_notation_constr subst bound c in + if po' == po && b' == b && c' == c then raw else + NLetTuple (nal,(na,po'),b',c') + + | NIf (c,(na,po),b1,b2) -> + let po' = Option.smartmap (subst_notation_constr subst bound) po + and b1' = subst_notation_constr subst bound b1 + and b2' = subst_notation_constr subst bound b2 + and c' = subst_notation_constr subst bound c in + if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else + NIf (c',(na,po'),b1',b2') + + | NRec (fk,idl,dll,tl,bl) -> + let dll' = + array_smartmap (list_smartmap (fun (na,oc,b as x) -> + let oc' = Option.smartmap (subst_notation_constr subst bound) oc in + let b' = subst_notation_constr subst bound b in + if oc' == oc && b' == b then x else (na,oc',b'))) dll in + let tl' = array_smartmap (subst_notation_constr subst bound) tl in + let bl' = array_smartmap (subst_notation_constr subst bound) bl in + if dll' == dll && tl' == tl && bl' == bl then raw else + NRec (fk,idl,dll',tl',bl') + + | NPatVar _ | NSort _ -> raw + + | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> + let ref',t = subst_global subst ref in + if ref' == ref then raw else + NHole (Evar_kinds.InternalHole) + | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ + |Evar_kinds.CasesType |Evar_kinds.InternalHole + |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar + |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw + + | NCast (r1,k) -> + let r1' = subst_notation_constr subst bound r1 in + let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in + if r1' == r1 && k' == k then raw else NCast(r1',k') + +let subst_interpretation subst (metas,pat) = + let bound = List.map fst metas in + (metas,subst_notation_constr subst bound pat) + +(* Pattern-matching glob_constr and notation_constr *) + +let abstract_return_type_context pi mklam tml rtno = + Option.map (fun rtn -> + let nal = + List.flatten (List.map (fun (_,(na,t)) -> + match t with Some x -> (pi x)@[na] | None -> [na]) tml) in + List.fold_right mklam nal rtn) + rtno + +let abstract_return_type_context_glob_constr = + abstract_return_type_context (fun (_,_,nal) -> nal) + (fun na c -> + GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) + +let abstract_return_type_context_notation_constr = + abstract_return_type_context snd + (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) + +exception No_match + +let rec alpha_var id1 id2 = function + | (i1,i2)::_ when i1=id1 -> i2 = id2 + | (i1,i2)::_ when i2=id2 -> i1 = id1 + | _::idl -> alpha_var id1 id2 idl + | [] -> id1 = id2 + +let alpha_eq_val (x,y) = x = y + +let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = + try + let vvar = List.assoc var sigma in + if alpha_eq_val (v,vvar) then fullsigma + else raise No_match + with Not_found -> + (* Check that no capture of binding variables occur *) + if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; + (* TODO: handle the case of multiple occs in different scopes *) + ((var,v)::sigma,sigmalist,sigmabinders) + +let bind_binder (sigma,sigmalist,sigmabinders) x bl = + (sigma,sigmalist,(x,List.rev bl)::sigmabinders) + +let match_fix_kind fk1 fk2 = + match (fk1,fk2) with + | GCoFix n1, GCoFix n2 -> n1 = n2 + | GFix (nl1,n1), GFix (nl2,n2) -> + n1 = n2 && + array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 + | _ -> false + +let match_opt f sigma t1 t2 = match (t1,t2) with + | None, None -> sigma + | Some t1, Some t2 -> f sigma t1 t2 + | _ -> raise No_match + +let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with + | (_,Name id2) when List.mem id2 (fst metas) -> + let rhs = match na1 with + | Name id1 -> GVar (dummy_loc,id1) + | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in + alp, bind_env alp sigma id2 rhs + | (Name id1,Name id2) -> (id1,id2)::alp,sigma + | (Anonymous,Anonymous) -> alp,sigma + | _ -> raise No_match + +let rec match_cases_pattern_binders metas acc pat1 pat2 = + match (pat1,pat2) with + | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2 + | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2) + when c1 = c2 & List.length patl1 = List.length patl2 -> + List.fold_left2 (match_cases_pattern_binders metas) + (match_names metas acc na1 na2) patl1 patl2 + | _ -> raise No_match + +let glue_letin_with_decls = true + +let rec match_iterated_binders islambda decls = function + | GLambda (_,na,bk,t,b) when islambda -> + match_iterated_binders islambda ((na,bk,None,t)::decls) b + | GProd (_,(Name _ as na),bk,t,b) when not islambda -> + match_iterated_binders islambda ((na,bk,None,t)::decls) b + | GLetIn (loc,na,c,b) when glue_letin_with_decls -> + match_iterated_binders islambda + ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b + | b -> (decls,b) + +let remove_sigma x (sigmavar,sigmalist,sigmabinders) = + (List.remove_assoc x sigmavar,sigmalist,sigmabinders) + +let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin = + let rec aux sigma acc rest = + try + let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in + let rest = List.assoc ldots_var (pi1 sigma) in + let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in + let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + aux sigma (b::acc) rest + with No_match when acc <> [] -> + acc, match_fun metas sigma rest termin in + let bl,sigma = aux sigma [] rest in + bind_binder sigma x bl + +let match_alist match_fun metas sigma rest x iter termin lassoc = + let rec aux sigma acc rest = + try + let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in + let rest = List.assoc ldots_var (pi1 sigma) in + let t = List.assoc x (pi1 sigma) in + let sigma = remove_sigma x (remove_sigma ldots_var sigma) in + aux sigma (t::acc) rest + with No_match when acc <> [] -> + acc, match_fun metas sigma rest termin in + let l,sigma = aux sigma [] rest in + (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) + +let does_not_come_from_already_eta_expanded_var = + (* This is hack to avoid looping on a rule with rhs of the form *) + (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) + (* "F (fun x => H x)" and "H x" is recursively matched against the same *) + (* rule, giving "H (fun x' => x x')" and so on. *) + (* Ideally, we would need the type of the expression to know which of *) + (* the arguments applied to it can be eta-expanded without looping. *) + (* The following test is then an approximation of what can be done *) + (* optimally (whether other looping situations can occur remains to be *) + (* checked). *) + function GVar _ -> false | _ -> true + +let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = + match (a1,a2) with + + (* Matching notation variable *) + | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 + + (* Matching recursive notations for terms *) + | r1, NList (x,_,iter,termin,lassoc) -> + match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc + + (* Matching recursive notations for binders: ad hoc cases supporting let-in *) + | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> + let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in + (* TODO: address the possibility that termin is a Lambda itself *) + match_in u alp metas (bind_binder sigma x decls) b termin + | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) + when na1 <> Anonymous -> + let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in + (* TODO: address the possibility that termin is a Prod itself *) + match_in u alp metas (bind_binder sigma x decls) b termin + (* Matching recursive notations for binders: general case *) + | r, NBinderList (x,_,iter,termin) -> + match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin + + (* Matching individual binders as part of a recursive pattern *) + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> + match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) + when List.mem id blmetas & na <> Anonymous -> + match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + + (* Matching compositionally *) + | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma + | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma + | GPatVar (_,(_,n1)), NPatVar n2 when n1=n2 -> sigma + | GApp (loc,f1,l1), NApp (f2,l2) -> + let n1 = List.length l1 and n2 = List.length l2 in + let f1,l1,f2,l2 = + if n1 < n2 then + let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 + else if n1 > n2 then + let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 + else f1,l1, f2, l2 in + let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in + List.fold_left2 (match_ may_use_eta u alp metas) + (match_in u alp metas sigma f1 f2) l1 l2 + | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) + when sty1 = sty2 + & List.length tml1 = List.length tml2 + & List.length eqnl1 = List.length eqnl2 -> + let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in + let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in + let sigma = + try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' + with Option.Heterogeneous -> raise No_match + in + let sigma = List.fold_left2 + (fun s (tm1,_) (tm2,_) -> + match_in u alp metas s tm1 tm2) sigma tml1 tml2 in + List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 + | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) + when List.length nal1 = List.length nal2 -> + let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in + let sigma = match_in u alp metas sigma b1 b2 in + let (alp,sigma) = + List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in + match_in u alp metas sigma c1 c2 + | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) -> + let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in + List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] + | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2) + when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & + array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 + -> + let alp,sigma = array_fold_left2 + (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) -> + let sigma = + match_in u alp metas + (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2 + in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in + let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in + let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> + match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in + array_fold_left2 (match_in u alp metas) sigma bl1 bl2 + | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) + | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> + match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 + | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> + match_in u alp metas sigma c1 c2 + | GSort (_,GType _), NSort (GType None) when not u -> sigma + | GSort (_,s1), NSort s2 when s1 = s2 -> sigma + | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match + | a, NHole _ -> sigma + + (* On the fly eta-expansion so as to use notations of the form + "exists x, P x" for "ex P"; expects type not given because don't know + otherwise how to ensure it corresponds to a well-typed eta-expansion; + ensure at least one constructor is consumed to avoid looping *) + | b1, NLambda (Name id,NHole _,b2) when inner -> + let id' = Namegen.next_ident_away id (free_glob_vars b1) in + match_in u alp metas (bind_binder sigma id + [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) + (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2 + + | (GRec _ | GEvar _), _ + | _,_ -> raise No_match + +and match_in u = match_ true u + +and match_hd u = match_ false u + +and match_binders u alp metas na1 na2 sigma b1 b2 = + let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in + match_in u alp metas sigma b1 b2 + +and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = + (* patl1 and patl2 have the same length because they respectively + correspond to some tml1 and tml2 that have the same length *) + let (alp,sigma) = + List.fold_left2 (match_cases_pattern_binders metas) + (alp,sigma) patl1 patl2 in + match_in u alp metas sigma rhs1 rhs2 + +let match_notation_constr u c (metas,pat) = + let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in + let vars = (List.map fst (fst vars), List.map fst (snd vars)) in + let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in + (* Reorder canonically the substitution *) + let find x = + try List.assoc x terms + with Not_found -> + (* Happens for binders bound to Anonymous *) + (* Find a better way to propagate Anonymous... *) + GVar (dummy_loc,x) in + List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> + match typ with + | NtnTypeConstr -> + ((find x, scl)::terms',termlists',binders') + | NtnTypeConstrList -> + (terms',(List.assoc x termlists,scl)::termlists',binders') + | NtnTypeBinderList -> + (terms',termlists',(List.assoc x binders,scl)::binders')) + metas ([],[],[]) + +(* Matching cases pattern *) +let add_patterns_for_params ind l = + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l + +let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = + try + let vvar = List.assoc var sigma in + if v=vvar then fullsigma else raise No_match + with Not_found -> + (* TODO: handle the case of multiple occs in different scopes *) + (var,v)::sigma,sigmalist,x + +let rec match_cases_pattern metas sigma a1 a2 = + match (a1,a2) with + | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] + | PatVar (_,Anonymous), NHole _ -> sigma,[] + | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 -> + sigma,largs + | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) + when r1 = r2 -> + let l1 = add_patterns_for_params (fst r1) args1 in + let le2 = List.length l2 in + if le2 > List.length l1 + then + raise No_match + else + let l1',more_args = Util.list_chop le2 l1 in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args + | r1, NList (x,_,iter,termin,lassoc) -> + (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) + (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[] + | _ -> raise No_match + +and match_cases_pattern_no_more_args metas sigma a1 a2 = + match match_cases_pattern metas sigma a1 a2 with + |out,[] -> out + |_ -> raise No_match + +let match_ind_pattern metas sigma ind pats a2 = + match a2 with + | NRef (IndRef r2) when ind = r2 -> + sigma,pats + | NApp (NRef (IndRef r2),l2) + when ind = r2 -> + let le2 = List.length l2 in + if le2 > List.length pats + then + raise No_match + else + let l1',more_args = Util.list_chop le2 pats in + (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args + |_ -> raise No_match + +let reorder_canonically_substitution terms termlists metas = + List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> + match typ with + | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists') + | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists') + | NtnTypeBinderList -> assert false) + metas ([],[]) + +let match_notation_constr_cases_pattern c (metas,pat) = + let vars = List.map fst metas in + let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in + reorder_canonically_substitution terms termlists metas,more_args + +let match_notation_constr_ind_pattern ind args (metas,pat) = + let vars = List.map fst metas in + let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in + reorder_canonically_substitution terms termlists metas,more_args diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli new file mode 100644 index 000000000..9dfc656a0 --- /dev/null +++ b/interp/notation_ops.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Names +open Notation_term +open Misctypes +open Glob_term + +(** Utilities about [notation_constr] *) + +(** Translate a [glob_constr] into a notation given the list of variables + bound by the notation; also interpret recursive patterns *) + +val notation_constr_of_glob_constr : + (identifier * notation_var_internalization_type) list -> + (identifier * identifier) list -> glob_constr -> notation_constr + +(** Name of the special identifier used to encode recursive notations *) +val ldots_var : identifier + +(** Equality of [glob_constr] (warning: only partially implemented) *) +val eq_glob_constr : glob_constr -> glob_constr -> bool + +(** Re-interpret a notation as a [glob_constr], taking care of binders *) + +val glob_constr_of_notation_constr_with_binders : Pp.loc -> + ('a -> name -> 'a * name) -> + ('a -> notation_constr -> glob_constr) -> + 'a -> notation_constr -> glob_constr + +val glob_constr_of_notation_constr : Pp.loc -> notation_constr -> glob_constr + +(** [match_notation_constr] matches a [glob_constr] against a notation + interpretation; raise [No_match] if the matching fails *) + +exception No_match + +val match_notation_constr : bool -> glob_constr -> interpretation -> + (glob_constr * subscopes) list * (glob_constr list * subscopes) list * + (glob_decl list * subscopes) list + +val match_notation_constr_cases_pattern : + cases_pattern -> interpretation -> + ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * + (cases_pattern list) + +val match_notation_constr_ind_pattern : + inductive -> cases_pattern list -> interpretation -> + ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * + (cases_pattern list) + +(** Substitution of kernel names in interpretation data *) + +val subst_interpretation : + Mod_subst.substitution -> interpretation -> interpretation + +val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list diff --git a/interp/reserve.ml b/interp/reserve.ml index 2cfd6f5ea..296fb2811 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -80,8 +80,8 @@ let revert_reserved_type t = let t = Detyping.detype false [] [] t in list_try_find (fun (pat,id) -> - try let _ = Topconstr.match_notation_constr false t ([],pat) in Name id - with Topconstr.No_match -> failwith "") l + try let _ = Notation_ops.match_notation_constr false t ([],pat) in Name id + with Notation_ops.No_match -> failwith "") l with Not_found | Failure _ -> Anonymous let _ = Namegen.set_reserved_typed_name revert_reserved_type @@ -92,7 +92,7 @@ let anonymize_if_reserved na t = match na with | Name id as na -> (try if not !Flags.raw_print & - (try Topconstr.notation_constr_of_glob_constr [] [] t + (try Notation_ops.notation_constr_of_glob_constr [] [] t = find_reserved_type id with UserError _ -> false) then GHole (dummy_loc,Evar_kinds.BinderType na) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index f20d9727d..7415931f0 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -58,7 +58,7 @@ let cache_syntax_constant d = open_syntax_constant 1 d let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,Topconstr.subst_interpretation subst pat,onlyparse) + (local,Notation_ops.subst_interpretation subst pat,onlyparse) let classify_syntax_constant (local,_,_ as o) = if local then Dispose else Substitute o diff --git a/interp/topconstr.ml b/interp/topconstr.ml index ab603c37d..f3bec1d0b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -23,789 +23,6 @@ open Constrexpr open Notation_term (*i*) -(**********************************************************************) -(* Re-interpret a notation as a glob_constr, taking care of binders *) - -let name_to_ident = function - | Anonymous -> error "This expression should be a simple identifier." - | Name id -> id - -let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na - -let rec cases_pattern_fold_map loc g e = function - | PatVar (_,na) -> - let e',na' = g e na in e', PatVar (loc,na') - | PatCstr (_,cstr,patl,na) -> - let e',na' = g e na in - let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in - e', PatCstr (loc,cstr,patl',na') - -let rec subst_glob_vars l = function - | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) - | GProd (loc,Name id,bk,t,c) -> - let id = - try match List.assoc id l with GVar(_,id') -> id' | _ -> id - with Not_found -> id in - GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) - | GLambda (loc,Name id,bk,t,c) -> - let id = - try match List.assoc id l with GVar(_,id') -> id' | _ -> id - with Not_found -> id in - GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) - | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) - -let ldots_var = id_of_string ".." - -let glob_constr_of_notation_constr_with_binders loc g f e = function - | NVar id -> GVar (loc,id) - | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args) - | NList (x,y,iter,tail,swap) -> - let t = f e tail in let it = f e iter in - let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in - let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in - let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in - subst_glob_vars outerl it - | NBinderList (x,y,iter,tail) -> - let t = f e tail in let it = f e iter in - let innerl = [(ldots_var,t);(x,GVar(loc,y))] in - let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in - let outerl = [(ldots_var,inner)] in - subst_glob_vars outerl it - | NLambda (na,ty,c) -> - let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) - | NProd (na,ty,c) -> - let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | NLetIn (na,b,c) -> - let e',na = g e na in GLetIn (loc,na,f e b,f e' c) - | NCases (sty,rtntypopt,tml,eqnl) -> - let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> - let e',t' = match t with - | None -> e',None - | Some (ind,nal) -> - let e',nal' = List.fold_right (fun na (e',nal) -> - let e',na' = g e' na in e',na'::nal) nal (e',[]) in - e',Some (loc,ind,nal') in - let e',na' = g e' na in - (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in - let eqnl' = List.map (fun (patl,rhs) -> - let ((idl,e),patl) = - list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in - (loc,idl,patl,f e rhs)) eqnl in - GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') - | NLetTuple (nal,(na,po),b,c) -> - let e',nal = list_fold_map g e nal in - let e'',na = g e na in - GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) - | NIf (c,(na,po),b1,b2) -> - let e',na = g e na in - GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) - | NRec (fk,idl,dll,tl,bl) -> - let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> - let e,na = g e na in - (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in - let e',idl = array_fold_map (to_id g) e idl in - GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) - | NCast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k) - | NSort x -> GSort (loc,x) - | NHole x -> GHole (loc,x) - | NPatVar n -> GPatVar (loc,(false,n)) - | NRef x -> GRef (loc,x) - -let rec glob_constr_of_notation_constr loc x = - let rec aux () x = - glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x - in aux () x - -(****************************************************************************) -(* Translating a glob_constr into a notation, interpreting recursive patterns *) - -let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r) -let add_name r = function Anonymous -> () | Name id -> add_id r id - -let split_at_recursive_part c = - let sub = ref None in - let rec aux = function - | GApp (loc0,GVar(loc,v),c::l) when v = ldots_var -> - if !sub <> None then - (* Not narrowed enough to find only one recursive part *) - raise Not_found - else - (sub := Some c; - if l = [] then GVar (loc,ldots_var) - else GApp (loc0,GVar (loc,ldots_var),l)) - | c -> map_glob_constr aux c in - let outer_iterator = aux c in - match !sub with - | None -> (* No recursive pattern found *) raise Not_found - | Some c -> - match outer_iterator with - | GVar (_,v) when v = ldots_var -> (* Not enough context *) raise Not_found - | _ -> outer_iterator, c - -let on_true_do b f c = if b then (f c; b) else b - -let compare_glob_constr f add t1 t2 = match t1,t2 with - | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2 - | GVar (_,v1), GVar (_,v2) -> on_true_do (v1 = v2) add (Name v1) - | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 & list_for_all2eq f l1 l2 - | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> on_true_do (f ty1 ty2 & f c1 c2) add na1 - | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2) when na1 = na2 && bk1 = bk2 -> - on_true_do (f ty1 ty2 & f c1 c2) add na1 - | GHole _, GHole _ -> true - | GSort (_,s1), GSort (_,s2) -> s1 = s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 -> - on_true_do (f b1 b2 & f c1 c2) add na1 - | (GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ - | _,(GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> error "Unsupported construction in recursive notations." - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ - | GHole _ | GSort _ | GLetIn _), _ - -> false - -let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 - -let subtract_loc loc1 loc2 = make_loc (fst (unloc loc1),fst (unloc loc2)-1) - -let check_is_hole id = function GHole _ -> () | t -> - user_err_loc (loc_of_glob_constr t,"", - strbrk "In recursive notation with binders, " ++ pr_id id ++ - strbrk " is expected to come without type.") - -let compare_recursive_parts found f (iterator,subc) = - let diff = ref None in - let terminator = ref None in - let rec aux c1 c2 = match c1,c2 with - | GVar(_,v), term when v = ldots_var -> - (* We found the pattern *) - assert (!terminator = None); terminator := Some term; - true - | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var -> - (* We found the pattern, but there are extra arguments *) - (* (this allows e.g. alternative (recursive) notation of application) *) - assert (!terminator = None); terminator := Some term; - list_for_all2eq aux l1 l2 - | GVar (_,x), GVar (_,y) when x<>y -> - (* We found the position where it differs *) - let lassoc = (!terminator <> None) in - let x,y = if lassoc then y,x else x,y in - !diff = None && (diff := Some (x,y,Some lassoc); true) - | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term) - | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) -> - (* We found a binding position where it differs *) - check_is_hole x t_x; - check_is_hole y t_y; - !diff = None && (diff := Some (x,y,None); aux c term) - | _ -> - compare_glob_constr aux (add_name found) c1 c2 in - if aux iterator subc then - match !diff with - | None -> - let loc1 = loc_of_glob_constr iterator in - let loc2 = loc_of_glob_constr (Option.get !terminator) in - (* Here, we would need a loc made of several parts ... *) - user_err_loc (subtract_loc loc1 loc2,"", - str "Both ends of the recursive pattern are the same.") - | Some (x,y,Some lassoc) -> - let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in - let iterator = - f (if lassoc then subst_glob_vars [y,GVar(dummy_loc,x)] iterator - else iterator) in - (* found have been collected by compare_constr *) - found := newfound; - NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,None) -> - let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in - let iterator = f iterator in - (* found have been collected by compare_constr *) - found := newfound; - NBinderList (x,y,iterator,f (Option.get !terminator)) - else - raise Not_found - -let notation_constr_and_vars_of_glob_constr a = - let found = ref ([],[],[]) in - let rec aux c = - let keepfound = !found in - (* n^2 complexity but small and done only once per notation *) - try compare_recursive_parts found aux' (split_at_recursive_part c) - with Not_found -> - found := keepfound; - match c with - | GApp (_,GVar (loc,f),[c]) when f = ldots_var -> - (* Fall on the second part of the recursive pattern w/o having - found the first part *) - user_err_loc (loc,"", - str "Cannot find where the recursive pattern starts.") - | c -> - aux' c - and aux' = function - | GVar (_,id) -> add_id found id; NVar id - | GApp (_,g,args) -> NApp (aux g, List.map aux args) - | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) - | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) - | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) - | GCases (_,sty,rtntypopt,tml,eqnl) -> - let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in - NCases (sty,Option.map aux rtntypopt, - List.map (fun (tm,(na,x)) -> - add_name found na; - Option.iter - (fun (_,_,nl) -> List.iter (add_name found) nl) x; - (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml, - List.map f eqnl) - | GLetTuple (loc,nal,(na,po),b,c) -> - add_name found na; - List.iter (add_name found) nal; - NLetTuple (nal,(na,Option.map aux po),aux b,aux c) - | GIf (loc,c,(na,po),b1,b2) -> - add_name found na; - NIf (aux c,(na,Option.map aux po),aux b1,aux b2) - | GRec (_,fk,idl,dll,tl,bl) -> - Array.iter (add_id found) idl; - let dll = Array.map (List.map (fun (na,bk,oc,b) -> - if bk <> Explicit then - error "Binders marked as implicit not allowed in notations."; - add_name found na; (na,Option.map aux oc,aux b))) dll in - NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl) - | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k) - | GSort (_,s) -> NSort s - | GHole (_,w) -> NHole w - | GRef (_,r) -> NRef r - | GPatVar (_,(_,n)) -> NPatVar n - | GEvar _ -> - error "Existential variables not allowed in notations." - - in - let t = aux a in - (* Side effect *) - t, !found - -let rec list_rev_mem_assoc x = function - | [] -> false - | (_,x')::l -> x = x' || list_rev_mem_assoc x l - -let check_variables vars recvars (found,foundrec,foundrecbinding) = - let useless_vars = List.map snd recvars in - let vars = List.filter (fun (y,_) -> not (List.mem y useless_vars)) vars in - let check_recvar x = - if List.mem x found then - errorlabstrm "" (pr_id x ++ - strbrk " should only be used in the recursive part of a pattern.") in - List.iter (fun (x,y) -> check_recvar x; check_recvar y) - (foundrec@foundrecbinding); - let check_bound x = - if not (List.mem x found) then - if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding - or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding - then - error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.") - else - error ((string_of_id x)^" is unbound in the right-hand side.") in - let check_pair s x y where = - if not (List.mem (x,y) where) then - errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ - str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ - str " position as part of a recursive pattern.") in - let check_type (x,typ) = - match typ with - | NtnInternTypeConstr -> - begin - try check_pair "term" x (List.assoc x recvars) foundrec - with Not_found -> check_bound x - end - | NtnInternTypeBinder -> - begin - try check_pair "binding" x (List.assoc x recvars) foundrecbinding - with Not_found -> check_bound x - end - | NtnInternTypeIdent -> check_bound x in - List.iter check_type vars - -let notation_constr_of_glob_constr vars recvars a = - let a,found = notation_constr_and_vars_of_glob_constr a in - check_variables vars recvars found; - a - -(* Substitution of kernel names, avoiding a list of bound identifiers *) - -let notation_constr_of_constr avoiding t = - notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t) - -let rec subst_pat subst pat = - match pat with - | PatVar _ -> pat - | PatCstr (loc,((kn,i),j),cpl,n) -> - let kn' = subst_ind subst kn - and cpl' = list_smartmap (subst_pat subst) cpl in - if kn' == kn && cpl' == cpl then pat else - PatCstr (loc,((kn',i),j),cpl',n) - -let rec subst_notation_constr subst bound raw = - match raw with - | NRef ref -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - notation_constr_of_constr bound t - - | NVar _ -> raw - - | NApp (r,rl) -> - let r' = subst_notation_constr subst bound r - and rl' = list_smartmap (subst_notation_constr subst bound) rl in - if r' == r && rl' == rl then raw else - NApp(r',rl') - - | NList (id1,id2,r1,r2,b) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NList (id1,id2,r1',r2',b) - - | NLambda (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NLambda (n,r1',r2') - - | NProd (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NProd (n,r1',r2') - - | NBinderList (id1,id2,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NBinderList (id1,id2,r1',r2') - - | NLetIn (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NLetIn (n,r1',r2') - - | NCases (sty,rtntypopt,rl,branches) -> - let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = list_smartmap - (fun (a,(n,signopt) as x) -> - let a' = subst_notation_constr subst bound a in - let signopt' = Option.map (fun ((indkn,i),nal as z) -> - let indkn' = subst_ind subst indkn in - if indkn == indkn' then z else ((indkn',i),nal)) signopt in - if a' == a && signopt' == signopt then x else (a',(n,signopt'))) - rl - and branches' = list_smartmap - (fun (cpl,r as branch) -> - let cpl' = list_smartmap (subst_pat subst) cpl - and r' = subst_notation_constr subst bound r in - if cpl' == cpl && r' == r then branch else - (cpl',r')) - branches - in - if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' & - rl' == rl && branches' == branches then raw else - NCases (sty,rtntypopt',rl',branches') - - | NLetTuple (nal,(na,po),b,c) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po - and b' = subst_notation_constr subst bound b - and c' = subst_notation_constr subst bound c in - if po' == po && b' == b && c' == c then raw else - NLetTuple (nal,(na,po'),b',c') - - | NIf (c,(na,po),b1,b2) -> - let po' = Option.smartmap (subst_notation_constr subst bound) po - and b1' = subst_notation_constr subst bound b1 - and b2' = subst_notation_constr subst bound b2 - and c' = subst_notation_constr subst bound c in - if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else - NIf (c',(na,po'),b1',b2') - - | NRec (fk,idl,dll,tl,bl) -> - let dll' = - array_smartmap (list_smartmap (fun (na,oc,b as x) -> - let oc' = Option.smartmap (subst_notation_constr subst bound) oc in - let b' = subst_notation_constr subst bound b in - if oc' == oc && b' == b then x else (na,oc',b'))) dll in - let tl' = array_smartmap (subst_notation_constr subst bound) tl in - let bl' = array_smartmap (subst_notation_constr subst bound) bl in - if dll' == dll && tl' == tl && bl' == bl then raw else - NRec (fk,idl,dll',tl',bl') - - | NPatVar _ | NSort _ -> raw - - | NHole (Evar_kinds.ImplicitArg (ref,i,b)) -> - let ref',t = subst_global subst ref in - if ref' == ref then raw else - NHole (Evar_kinds.InternalHole) - | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _ - |Evar_kinds.CasesType |Evar_kinds.InternalHole - |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar - |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw - - | NCast (r1,k) -> - let r1' = subst_notation_constr subst bound r1 in - let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in - if r1' == r1 && k' == k then raw else NCast(r1',k') - -let subst_interpretation subst (metas,pat) = - let bound = List.map fst metas in - (metas,subst_notation_constr subst bound pat) - -(* Pattern-matching glob_constr and notation_constr *) - -let abstract_return_type_context pi mklam tml rtno = - Option.map (fun rtn -> - let nal = - List.flatten (List.map (fun (_,(na,t)) -> - match t with Some x -> (pi x)@[na] | None -> [na]) tml) in - List.fold_right mklam nal rtn) - rtno - -let abstract_return_type_context_glob_constr = - abstract_return_type_context (fun (_,_,nal) -> nal) - (fun na c -> - GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c)) - -let abstract_return_type_context_notation_constr = - abstract_return_type_context snd - (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c)) - -exception No_match - -let rec alpha_var id1 id2 = function - | (i1,i2)::_ when i1=id1 -> i2 = id2 - | (i1,i2)::_ when i2=id2 -> i1 = id1 - | _::idl -> alpha_var id1 id2 idl - | [] -> id1 = id2 - -let alpha_eq_val (x,y) = x = y - -let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = - try - let vvar = List.assoc var sigma in - if alpha_eq_val (v,vvar) then fullsigma - else raise No_match - with Not_found -> - (* Check that no capture of binding variables occur *) - if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; - (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::sigma,sigmalist,sigmabinders) - -let bind_binder (sigma,sigmalist,sigmabinders) x bl = - (sigma,sigmalist,(x,List.rev bl)::sigmabinders) - -let match_fix_kind fk1 fk2 = - match (fk1,fk2) with - | GCoFix n1, GCoFix n2 -> n1 = n2 - | GFix (nl1,n1), GFix (nl2,n2) -> - n1 = n2 && - array_for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2 - | _ -> false - -let match_opt f sigma t1 t2 = match (t1,t2) with - | None, None -> sigma - | Some t1, Some t2 -> f sigma t1 t2 - | _ -> raise No_match - -let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (_,Name id2) when List.mem id2 (fst metas) -> - let rhs = match na1 with - | Name id1 -> GVar (dummy_loc,id1) - | Anonymous -> GHole (dummy_loc,Evar_kinds.InternalHole) in - alp, bind_env alp sigma id2 rhs - | (Name id1,Name id2) -> (id1,id2)::alp,sigma - | (Anonymous,Anonymous) -> alp,sigma - | _ -> raise No_match - -let rec match_cases_pattern_binders metas acc pat1 pat2 = - match (pat1,pat2) with - | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2 - | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2) - when c1 = c2 & List.length patl1 = List.length patl2 -> - List.fold_left2 (match_cases_pattern_binders metas) - (match_names metas acc na1 na2) patl1 patl2 - | _ -> raise No_match - -let glue_letin_with_decls = true - -let rec match_iterated_binders islambda decls = function - | GLambda (_,na,bk,t,b) when islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b - | GProd (_,(Name _ as na),bk,t,b) when not islambda -> - match_iterated_binders islambda ((na,bk,None,t)::decls) b - | GLetIn (loc,na,c,b) when glue_letin_with_decls -> - match_iterated_binders islambda - ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na))::decls) b - | b -> (decls,b) - -let remove_sigma x (sigmavar,sigmalist,sigmabinders) = - (List.remove_assoc x sigmavar,sigmalist,sigmabinders) - -let rec match_abinderlist_with_app match_fun metas sigma rest x iter termin = - let rec aux sigma acc rest = - try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = List.assoc ldots_var (pi1 sigma) in - let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in - aux sigma (b::acc) rest - with No_match when acc <> [] -> - acc, match_fun metas sigma rest termin in - let bl,sigma = aux sigma [] rest in - bind_binder sigma x bl - -let match_alist match_fun metas sigma rest x iter termin lassoc = - let rec aux sigma acc rest = - try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = List.assoc ldots_var (pi1 sigma) in - let t = List.assoc x (pi1 sigma) in - let sigma = remove_sigma x (remove_sigma ldots_var sigma) in - aux sigma (t::acc) rest - with No_match when acc <> [] -> - acc, match_fun metas sigma rest termin in - let l,sigma = aux sigma [] rest in - (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) - -let does_not_come_from_already_eta_expanded_var = - (* This is hack to avoid looping on a rule with rhs of the form *) - (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *) - (* "F (fun x => H x)" and "H x" is recursively matched against the same *) - (* rule, giving "H (fun x' => x x')" and so on. *) - (* Ideally, we would need the type of the expression to know which of *) - (* the arguments applied to it can be eta-expanded without looping. *) - (* The following test is then an approximation of what can be done *) - (* optimally (whether other looping situations can occur remains to be *) - (* checked). *) - function GVar _ -> false | _ -> true - -let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = - match (a1,a2) with - - (* Matching notation variable *) - | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 - - (* Matching recursive notations for terms *) - | r1, NList (x,_,iter,termin,lassoc) -> - match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc - - (* Matching recursive notations for binders: ad hoc cases supporting let-in *) - | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> - let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in - (* TODO: address the possibility that termin is a Lambda itself *) - match_in u alp metas (bind_binder sigma x decls) b termin - | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) - when na1 <> Anonymous -> - let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in - (* TODO: address the possibility that termin is a Prod itself *) - match_in u alp metas (bind_binder sigma x decls) b termin - (* Matching recursive notations for binders: general case *) - | r, NBinderList (x,_,iter,termin) -> - match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin - - (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) - when List.mem id blmetas & na <> Anonymous -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 - - (* Matching compositionally *) - | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma - | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma - | GPatVar (_,(_,n1)), NPatVar n2 when n1=n2 -> sigma - | GApp (loc,f1,l1), NApp (f2,l2) -> - let n1 = List.length l1 and n2 = List.length l2 in - let f1,l1,f2,l2 = - if n1 < n2 then - let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22 - else if n1 > n2 then - let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2 - else f1,l1, f2, l2 in - let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in - List.fold_left2 (match_ may_use_eta u alp metas) - (match_in u alp metas sigma f1 f2) l1 l2 - | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) - when sty1 = sty2 - & List.length tml1 = List.length tml2 - & List.length eqnl1 = List.length eqnl2 -> - let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in - let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in - let sigma = - try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2' - with Option.Heterogeneous -> raise No_match - in - let sigma = List.fold_left2 - (fun s (tm1,_) (tm2,_) -> - match_in u alp metas s tm1 tm2) sigma tml1 tml2 in - List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2 - | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2) - when List.length nal1 = List.length nal2 -> - let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in - let sigma = match_in u alp metas sigma b1 b2 in - let (alp,sigma) = - List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in - match_in u alp metas sigma c1 c2 - | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) -> - let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in - List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2] - | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2) - when match_fix_kind fk1 fk2 & Array.length idl1 = Array.length idl2 & - array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2 - -> - let alp,sigma = array_fold_left2 - (List.fold_left2 (fun (alp,sigma) (na1,_,oc1,b1) (na2,oc2,b2) -> - let sigma = - match_in u alp metas - (match_opt (match_in u alp metas) sigma oc1 oc2) b1 b2 - in match_names metas (alp,sigma) na1 na2)) (alp,sigma) dll1 dll2 in - let sigma = array_fold_left2 (match_in u alp metas) sigma tl1 tl2 in - let alp,sigma = array_fold_right2 (fun id1 id2 alsig -> - match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in - array_fold_left2 (match_in u alp metas) sigma bl1 bl2 - | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2) - | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) -> - match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2 - | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) -> - match_in u alp metas sigma c1 c2 - | GSort (_,GType _), NSort (GType None) when not u -> sigma - | GSort (_,s1), NSort s2 when s1 = s2 -> sigma - | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match - | a, NHole _ -> sigma - - (* On the fly eta-expansion so as to use notations of the form - "exists x, P x" for "ex P"; expects type not given because don't know - otherwise how to ensure it corresponds to a well-typed eta-expansion; - ensure at least one constructor is consumed to avoid looping *) - | b1, NLambda (Name id,NHole _,b2) when inner -> - let id' = Namegen.next_ident_away id (free_glob_vars b1) in - match_in u alp metas (bind_binder sigma id - [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))]) - (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2 - - | (GRec _ | GEvar _), _ - | _,_ -> raise No_match - -and match_in u = match_ true u - -and match_hd u = match_ false u - -and match_binders u alp metas na1 na2 sigma b1 b2 = - let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in - match_in u alp metas sigma b1 b2 - -and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = - (* patl1 and patl2 have the same length because they respectively - correspond to some tml1 and tml2 that have the same length *) - let (alp,sigma) = - List.fold_left2 (match_cases_pattern_binders metas) - (alp,sigma) patl1 patl2 in - match_in u alp metas sigma rhs1 rhs2 - -let match_notation_constr u c (metas,pat) = - let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in - let vars = (List.map fst (fst vars), List.map fst (snd vars)) in - let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in - (* Reorder canonically the substitution *) - let find x = - try List.assoc x terms - with Not_found -> - (* Happens for binders bound to Anonymous *) - (* Find a better way to propagate Anonymous... *) - GVar (dummy_loc,x) in - List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> - match typ with - | NtnTypeConstr -> - ((find x, scl)::terms',termlists',binders') - | NtnTypeConstrList -> - (terms',(List.assoc x termlists,scl)::termlists',binders') - | NtnTypeBinderList -> - (terms',termlists',(List.assoc x binders,scl)::binders')) - metas ([],[],[]) - -(* Matching cases pattern *) -let add_patterns_for_params ind l = - let mib,_ = Global.lookup_inductive ind in - let nparams = mib.Declarations.mind_nparams in - Util.list_addn nparams (PatVar (dummy_loc,Anonymous)) l - -let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = - try - let vvar = List.assoc var sigma in - if v=vvar then fullsigma else raise No_match - with Not_found -> - (* TODO: handle the case of multiple occs in different scopes *) - (var,v)::sigma,sigmalist,x - -let rec match_cases_pattern metas sigma a1 a2 = - match (a1,a2) with - | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[] - | PatVar (_,Anonymous), NHole _ -> sigma,[] - | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 -> - sigma,largs - | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2) - when r1 = r2 -> - let l1 = add_patterns_for_params (fst r1) args1 in - let le2 = List.length l2 in - if le2 > List.length l1 - then - raise No_match - else - let l1',more_args = Util.list_chop le2 l1 in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args - | r1, NList (x,_,iter,termin,lassoc) -> - (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) - (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[] - | _ -> raise No_match -and match_cases_pattern_no_more_args metas sigma a1 a2 = - match match_cases_pattern metas sigma a1 a2 with - |out,[] -> out - |_ -> raise No_match - -let match_ind_pattern metas sigma ind pats a2 = - match a2 with - | ARef (IndRef r2) when ind = r2 -> - sigma,pats - | AApp (ARef (IndRef r2),l2) - when ind = r2 -> - let le2 = List.length l2 in - if le2 > List.length pats - then - raise No_match - else - let l1',more_args = Util.list_chop le2 pats in - (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args - |_ -> raise No_match - -let reorder_canonically_substitution terms termlists metas = - List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> - match typ with - | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists') - | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists') - | NtnTypeBinderList -> assert false) - metas ([],[]) - -let match_notation_constr_cases_pattern c (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in - reorder_canonically_substitution terms termlists metas,more_args - -let match_aconstr_ind_pattern ind args (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in - reorder_canonically_substitution terms termlists metas,more_args - let oldfashion_patterns = ref (true) let write_oldfashion_patterns = Goptions.declare_bool_option { diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 760ee14a5..7556f1385 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -20,49 +20,6 @@ open Notation_term (** Topconstr *) -(** Translate a glob_constr into a notation given the list of variables - bound by the notation; also interpret recursive patterns *) - -val notation_constr_of_glob_constr : - (identifier * notation_var_internalization_type) list -> - (identifier * identifier) list -> glob_constr -> notation_constr - -(** Name of the special identifier used to encode recursive notations *) -val ldots_var : identifier - -(** Equality of glob_constr (warning: only partially implemented) *) -val eq_glob_constr : glob_constr -> glob_constr -> bool - -(** Re-interpret a notation as a glob_constr, taking care of binders *) - -val glob_constr_of_notation_constr_with_binders : loc -> - ('a -> name -> 'a * name) -> - ('a -> notation_constr -> glob_constr) -> - 'a -> notation_constr -> glob_constr - -val glob_constr_of_notation_constr : loc -> notation_constr -> glob_constr - -(** [match_notation_constr] matches a glob_constr against a notation interpretation; - raise [No_match] if the matching fails *) - -exception No_match - -val match_notation_constr : bool -> glob_constr -> interpretation -> - (glob_constr * subscopes) list * (glob_constr list * subscopes) list * - (glob_decl list * subscopes) list - -val match_notation_constr_cases_pattern : - cases_pattern -> interpretation -> - ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * - (cases_pattern list) - -val match_aconstr_ind_pattern : inductive -> cases_pattern list -> interpretation -> - ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list) - -(** Substitution of kernel names in interpretation data *) - -val subst_interpretation : substitution -> interpretation -> interpretation - val oldfashion_patterns : bool ref (** Utilities on constr_expr *) @@ -133,5 +90,3 @@ val patntn_loc : (** For cases pattern parsing errors *) val error_invalid_pattern_notation : Pp.loc -> 'a - -val add_patterns_for_params : inductive -> cases_pattern list -> cases_pattern list diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1bc46f83f..3e1af6fed 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -183,7 +183,7 @@ GEXTEND Gram CApp(loc,(None,CPatVar(locid,(true,id))),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> - CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ] + CAppExpl (loc,(None,Ident (loc,Notation_ops.ldots_var)),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> @@ -395,7 +395,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(loc,Name Topconstr.ldots_var);id2], + [LocalRawAssum ([id1;(loc,Name Notation_ops.ldots_var);id2], Default Explicit,CHole (loc,None))] | bl = closed_binder; bl' = binders -> bl@bl' diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index 1a9c03f72..182234f7c 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -65,6 +65,7 @@ Inductiveops Miscops Glob_ops Detyping +Notation_ops Topconstr Genarg Ppextend diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index d7e968ad4..1fc721769 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -467,7 +467,7 @@ let pr pr sep inherited a = p, lproj | CAppExpl (_,(None,Ident (_,var)),[t]) | CApp (_,(_,CRef(Ident(_,var))),[t,None]) - when var = Topconstr.ldots_var -> + when var = Notation_ops.ldots_var -> hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp | CApp (_,(Some i,f),l) -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d90e655b1..f1f6db64d 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -435,7 +435,7 @@ let gallina_print_constant_with_infos sp = let gallina_print_syntactic_def kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Topconstr.glob_constr_of_notation_constr dummy_loc a in + let c = Notation_ops.glob_constr_of_notation_constr dummy_loc a in hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 95c6a6d99..9fe77bf9d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1243,7 +1243,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b if array_for_all (fun l -> let (n',nt',is_defined') = List.nth l i in - n = n' && Topconstr.eq_glob_constr nt nt' && is_defined = is_defined') + n = n' && Notation_ops.eq_glob_constr nt nt' && is_defined = is_defined') rels_params then l := param::!l diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 5a305ccc9..6b64f9546 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -14,6 +14,7 @@ open Util open Names open Constrexpr open Notation_term +open Notation_ops open Topconstr open Ppextend open Extend diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 73c05de3f..4c2b2f9b2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -875,7 +875,7 @@ let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t = Constrintern.interp_type Evd.empty (Global.env()) c in let t = Detyping.detype false [] [] t in - let t = Topconstr.notation_constr_of_glob_constr [] [] t in + let t = Notation_ops.notation_constr_of_glob_constr [] [] t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |