diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-04 13:27:29 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-04 13:50:56 +0200 |
commit | 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 (patch) | |
tree | 1244ce89baaff25f461b4aaa6785cf54989f5c0a /interp | |
parent | 6ffbe4308229feb63525506e6a1fa77a61d2895b (diff) |
Quick fix to #4595 (making notations containing "ltac:" unused for printing).
Also getting rid of a global side-effect.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/constrintern.ml | 4 | ||||
-rw-r--r-- | interp/constrintern.mli | 2 | ||||
-rw-r--r-- | interp/notation_ops.ml | 24 | ||||
-rw-r--r-- | interp/notation_ops.mli | 2 |
4 files changed, 18 insertions, 14 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f98873aa6..194f5f1c2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2013,14 +2013,14 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a = tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = notation_constr_of_glob_constr nenv c in + let a, reversible = notation_constr_of_glob_constr nenv c in (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> (!isonlybinding, out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) - vars, a + vars, a, reversible (* Interpret binders and contexts *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index eea76aa31..61e7c6f5c 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -186,7 +186,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr val interp_notation_constr : ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr + notation_constr * reversibility_flag (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index cc81a0091..7b520c1c1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -323,6 +323,7 @@ let compare_recursive_parts found f f' (iterator,subc) = 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 +369,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 +379,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 +405,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 +425,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 +441,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 +458,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 diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 4ebd3ddd8..c8fcbf741 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -29,7 +29,7 @@ val ldots_var : Id.t bound by the notation; also interpret recursive patterns *) val notation_constr_of_glob_constr : notation_interp_env -> - glob_constr -> notation_constr + glob_constr -> notation_constr * reversibility_flag (** Re-interpret a notation as a [glob_constr], taking care of binders *) |