diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /interp/notation.ml | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 32 |
1 files changed, 27 insertions, 5 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index aeec4b61..80db2cb3 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 = [] @@ -516,6 +512,32 @@ 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 + interpretation_eq r' r + with Not_found -> false + let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) |