diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index cc81a00919..0c5393cf41 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -248,6 +248,10 @@ let check_is_hole id = function GHole _ -> () | t -> let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' +type recursive_pattern_kind = +| RecursiveTerms of bool (* associativity *) +| RecursiveBinders of glob_constr * glob_constr + let compare_recursive_parts found f f' (iterator,subc) = let diff = ref None in let terminator = ref None in @@ -269,18 +273,16 @@ let compare_recursive_parts found f f' (iterator,subc) = let x,y = if lassoc then y,x else x,y in begin match !diff with | None -> - let () = diff := Some (x, y, Some lassoc) in + let () = diff := Some (x, y, RecursiveTerms lassoc) in true | Some _ -> false end | 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; begin match !diff with | None -> - let () = diff := Some (x, y, None) in + let () = diff := Some (x, y, RecursiveBinders (t_x,t_y)) in aux c term | Some _ -> false end @@ -294,7 +296,7 @@ let compare_recursive_parts found f f' (iterator,subc) = (* 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) -> + | Some (x,y,RecursiveTerms lassoc) -> let newfound,x,y,lassoc = if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) || List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found) @@ -312,17 +314,20 @@ let compare_recursive_parts found f f' (iterator,subc) = (* found have been collected by compare_constr *) found := newfound; NList (x,y,iterator,f (Option.get !terminator),lassoc) - | Some (x,y,None) -> + | Some (x,y,RecursiveBinders (t_x,t_y)) -> let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in (* found have been collected by compare_constr *) found := newfound; + check_is_hole x t_x; + check_is_hole y t_y; 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 has_ltac = ref false in let rec aux c = let keepfound = !found in (* n^2 complexity but small and done only once per notation *) @@ -368,7 +373,9 @@ let notation_constr_and_vars_of_glob_constr a = 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,naming,arg) -> NHole (w, naming, arg) + | GHole (_,w,naming,arg) -> + if arg != None then has_ltac := true; + NHole (w, naming, arg) | GRef (_,r,_) -> NRef r | GEvar _ | GPatVar _ -> error "Existential variables not allowed in notations." @@ -376,9 +383,10 @@ let notation_constr_and_vars_of_glob_constr a = in let t = aux a in (* Side effect *) - t, !found + t, !found, !has_ltac -let check_variables nenv (found,foundrec,foundrecbinding) = +let check_variables_and_reversibility nenv (found,foundrec,foundrecbinding) = + let injective = ref true in let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in let useless_vars = Id.Map.fold fold recvars Id.Set.empty in @@ -401,7 +409,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = error (Id.to_string x ^ " should not be bound in a recursive pattern of the right-hand side.") - else nenv.ninterp_only_parse <- true + else injective := false in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then @@ -421,12 +429,13 @@ let check_variables nenv (found,foundrec,foundrecbinding) = with Not_found -> check_bound x end | NtnInternTypeIdent -> check_bound x in - Id.Map.iter check_type vars + Id.Map.iter check_type vars; + !injective let notation_constr_of_glob_constr nenv a = - let a, found = notation_constr_and_vars_of_glob_constr a in - let () = check_variables nenv found in - a + let a, found, has_ltac = notation_constr_and_vars_of_glob_constr a in + let injective = check_variables_and_reversibility nenv found in + a, not has_ltac && injective (**********************************************************************) (* Substitution of kernel names, avoiding a list of bound identifiers *) @@ -436,7 +445,6 @@ let notation_constr_of_constr avoiding t = let nenv = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; - ninterp_only_parse = false; } in notation_constr_of_glob_constr nenv t @@ -454,7 +462,7 @@ let rec subst_notation_constr subst bound raw = | NRef ref -> let ref',t = subst_global subst ref in if ref' == ref then raw else - notation_constr_of_constr bound t + fst (notation_constr_of_constr bound t) | NVar _ -> raw |