From d65eaaaa8cb311a0344a584df7a4b405034780b9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 15:56:51 +0100 Subject: Revert "Useless check when loading notations through import." This reverts commit 124734fd2c523909802d095abb37350519856864. --- interp/notation.ml | 8 ++++++++ interp/notation.mli | 4 ++++ 2 files changed, 12 insertions(+) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index aeec4b6153..6040c33a5e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -516,6 +516,14 @@ let availability_of_prim_token n printer_scope local_scopes = (* Miscellaneous *) +let exists_notation_in_scope scopt ntn r = + let scope = match scopt with Some s -> s | None -> default_scope in + try + let sc = String.Map.find scope !scope_map in + let (r',_) = String.Map.find ntn sc.notations in + Pervasives.(=) r' r (** FIXME *) + with Not_found -> false + let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) diff --git a/interp/notation.mli b/interp/notation.mli index c66115cbdd..854c52b2c7 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -140,6 +140,10 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *) val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) -> notation -> delimiters option -> global_reference +(** Checks for already existing notations *) +val exists_notation_in_scope : scope_name option -> notation -> + interpretation -> bool + (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> global_reference -> scope_name option list -> unit -- cgit v1.2.3 From 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 24 Mar 2015 16:01:03 +0100 Subject: Fixing equality of notation_constrs. Fixes bug #4136. --- interp/notation.ml | 20 +++++++++++++++- interp/notation_ops.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++++ interp/notation_ops.mli | 2 ++ 3 files changed, 84 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 6040c33a5e..f498761344 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -516,12 +516,30 @@ let availability_of_prim_token n printer_scope local_scopes = (* Miscellaneous *) +let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 + +let ntpe_eq t1 t2 = match t1, t2 with +| NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeConstrList, NtnTypeConstrList -> true +| NtnTypeBinderList, NtnTypeBinderList -> true +| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false + + +let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = + Id.equal id1 id2 && + pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + ntpe_eq tp1 tp2 + +let interpretation_eq (vars1, t1) (vars2, t2) = + List.equal vars_eq vars1 vars2 && + Notation_ops.eq_notation_constr t1 t2 + let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in try let sc = String.Map.find scope !scope_map in let (r',_) = String.Map.find ntn sc.notations in - Pervasives.(=) r' r (** FIXME *) + interpretation_eq r' r with Not_found -> false let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index c91c781591..2762dc0b8d 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -170,6 +170,69 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2 +let rec eq_notation_constr t1 t2 = match t1, t2 with +| NRef gr1, NRef gr2 -> eq_gr gr1 gr2 +| NVar id1, NVar id2 -> Id.equal id1 id2 +| NApp (t1, a1), NApp (t2, a2) -> + eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 +| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 && b1 == b2 +| NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NProd (na1, t1, u1), NProd (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> + Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) + let eqpat (p1, t1) (p2, t2) = + List.equal cases_pattern_eq p1 p2 && + eq_notation_constr t1 t2 + in + let eqf (t1, (na1, o1)) (t2, (na2, o2)) = + let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in + eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + in + Option.equal eq_notation_constr o1 o2 && + List.equal eqf r1 r2 && + List.equal eqpat p1 p2 +| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> + List.equal Name.equal nas1 nas2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 && + eq_notation_constr u1 u2 +| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> + eq_notation_constr t1 t2 && + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr u1 u2 && + eq_notation_constr r1 r2 +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) + let eq (na1, o1, t1) (na2, o2, t2) = + Name.equal na1 na2 && + Option.equal eq_notation_constr o1 o2 && + eq_notation_constr t1 t2 + in + Array.equal Id.equal ids1 ids2 && + Array.equal (List.equal eq) ts1 ts2 && + Array.equal eq_notation_constr us1 us2 && + Array.equal eq_notation_constr rs1 rs2 +| NSort s1, NSort s2 -> + Miscops.glob_sort_eq s1 s2 +| NPatVar p1, NPatVar p2 -> + Id.equal p1 p2 +| NCast (t1, c1), NCast (t2, c2) -> + eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 +| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ + | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ + | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false + + let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1) let check_is_hole id = function GHole _ -> () | t -> diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 7283ed6f12..c6770deea2 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -25,6 +25,8 @@ val ldots_var : Id.t (** FIXME: nothing to do here *) val eq_glob_constr : glob_constr -> glob_constr -> bool +val eq_notation_constr : notation_constr -> notation_constr -> bool + (** Re-interpret a notation as a [glob_constr], taking care of binders *) val glob_constr_of_notation_constr_with_binders : Loc.t -> -- cgit v1.2.3 From f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 27 Mar 2015 19:46:40 +0100 Subject: Normalize scope names before storing them in vo files. (Fix for bug #4162) Note that I do not understand why the delimiter map is incomplete on loading and thus was causing a failure. So, while the patch is the proper way to deal with notation scopes, there might be another bug lurking in this file. --- interp/notation.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index f498761344..80db2cb396 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -136,10 +136,6 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = if Int.equal i 1 then - let sc = match sc with - | Scope sc -> Scope (normalize_scope sc) - | _ -> sc - in scope_stack := if op then sc :: !scope_stack else List.except scope_eq sc !scope_stack @@ -166,7 +162,7 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope sc)) + Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) let empty_scope_stack = [] -- cgit v1.2.3 From b4f2e48b9e128a62d63668621844b571d3449cbf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Mar 2015 11:13:41 +0200 Subject: grammar: export hypident This is necessary to make ssr compile with both camlp4/5 --- interp/constrarg.ml | 3 +++ interp/constrarg.mli | 2 ++ 2 files changed, 5 insertions(+) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 3f232c3612..a7241399e0 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType let wit_bindings = unsafe_of_type BindingsArgType +let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = + Genarg.make0 None "hyp_location_flag" + let wit_red_expr = unsafe_of_type RedExprArgType let wit_clause_dft_concl = diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 74c6bd310c..fdeddd66a1 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -64,6 +64,8 @@ val wit_bindings : glob_constr_and_expr bindings, constr bindings Evd.sigma) genarg_type +val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type + val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, -- cgit v1.2.3