aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml128
-rw-r--r--interp/constrintern.ml157
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/dumpglob.ml15
-rw-r--r--interp/genarg.ml3
-rw-r--r--interp/implicit_quantifiers.ml53
-rw-r--r--interp/notation.ml101
-rw-r--r--interp/notation_ops.ml131
-rw-r--r--interp/reserve.ml9
-rw-r--r--interp/syntax_def.ml6
-rw-r--r--interp/topconstr.ml29
11 files changed, 372 insertions, 262 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6cfe74382..e7f276f55 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -159,38 +159,47 @@ let extern_reference loc vars r =
(************************************************************************)
(* Equality up to location (useful for translator v8) *)
+let prim_token_eq t1 t2 = match t1, t2 with
+| Numeral i1, Numeral i2 -> Bigint.equal i1 i2
+| String s1, String s2 -> String.equal s1 s2
+| _ -> false
+
+(** ppedrot: FIXME, EVERYTHING IS WRONG HERE! *)
+
let rec check_same_pattern p1 p2 =
match p1, p2 with
- | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when i1=i2 ->
+ | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when id_eq i1 i2 ->
check_same_pattern a1 a2
- | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when c1=c2 ->
+ | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when eq_reference c1 c2 ->
let () = List.iter2 check_same_pattern a1 a2 in
List.iter2 check_same_pattern b1 b2
- | CPatAtom(_,r1), CPatAtom(_,r2) when r1=r2 -> ()
- | CPatPrim(_,i1), CPatPrim(_,i2) when i1=i2 -> ()
- | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when s1=s2 ->
+ | CPatAtom(_,r1), CPatAtom(_,r2) when Option.Misc.compare eq_reference r1 r2 -> ()
+ | CPatPrim(_,i1), CPatPrim(_,i2) when prim_token_eq i1 i2 -> ()
+ | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when String.equal s1 s2 ->
check_same_pattern e1 e2
| _ -> failwith "not same pattern"
let check_same_ref r1 r2 =
- match r1,r2 with
- | Qualid(_,q1), Qualid(_,q2) when q1=q2 -> ()
- | Ident(_,i1), Ident(_,i2) when i1=i2 -> ()
- | _ -> failwith "not same ref"
+ if not (eq_reference r1 r2) then failwith "not same ref"
+
+let eq_located f (_, x) (_, y) = f x y
+
+let same_id (id1, c1) (id2, c2) =
+ Option.Misc.compare (eq_located id_eq) id1 id2 && Pervasives.(=) c1 c2
let rec check_same_type ty1 ty2 =
match ty1, ty2 with
| CRef r1, CRef r2 -> check_same_ref r1 r2
- | CFix(_,(_,id1),fl1), CFix(_,(_,id2),fl2) when id1=id2 ->
- List.iter2 (fun (id1,i1,bl1,a1,b1) (id2,i2,bl2,a2,b2) ->
- if id1<>id2 || i1<>i2 then failwith "not same fix";
+ | CFix(_,id1,fl1), CFix(_,id2,fl2) when eq_located id_eq id1 id2 ->
+ List.iter2 (fun ((_, id1),i1,bl1,a1,b1) ((_, id2),i2,bl2,a2,b2) ->
+ if not (id_eq id1 id2) || not (same_id i1 i2) then failwith "not same fix";
check_same_fix_binder bl1 bl2;
check_same_type a1 a2;
check_same_type b1 b2)
fl1 fl2
- | CCoFix(_,(_,id1),fl1), CCoFix(_,(_,id2),fl2) when id1=id2 ->
+ | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) when eq_located id_eq id1 id2 ->
List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) ->
- if id1<>id2 then failwith "not same fix";
+ if not (eq_located id_eq id1 id2) then failwith "not same fix";
check_same_fix_binder bl1 bl2;
check_same_type a1 a2;
check_same_type b1 b2)
@@ -201,16 +210,16 @@ let rec check_same_type ty1 ty2 =
| CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
List.iter2 check_same_binder bl1 bl2;
check_same_type a1 a2
- | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when na1=na2 ->
+ | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when name_eq na1 na2 ->
check_same_type a1 a2;
check_same_type b1 b2
- | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when proj1=proj2 ->
+ | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.Misc.compare Int.equal proj1 proj2 ->
check_same_ref r1 r2;
List.iter2 check_same_type al1 al2
| CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) ->
check_same_type e1 e2;
List.iter2 (fun (a1,e1) (a2,e2) ->
- if e1<>e2 then failwith "not same expl";
+ if Option.Misc.compare (eq_located Constrintern.explicitation_eq) e1 e2 then failwith "not same expl";
check_same_type a1 a2) al1 al2
| CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) ->
List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2;
@@ -218,26 +227,26 @@ let rec check_same_type ty1 ty2 =
List.iter2 (Loc.located_iter2 (List.iter2 check_same_pattern)) pl1 pl2;
check_same_type r1 r2) brl1 brl2
| CHole _, CHole _ -> ()
- | CPatVar(_,i1), CPatVar(_,i2) when i1=i2 -> ()
- | CSort(_,s1), CSort(_,s2) when s1=s2 -> ()
+ | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) when (b1 : bool) == b2 && id_eq i1 i2 -> ()
+ | CSort(_,s1), CSort(_,s2) when glob_sort_eq s1 s2 -> ()
| CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
check_same_type a1 a2;
check_same_type b1 b2
| CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
check_same_type a1 a2
- | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when n1=n2 ->
+ | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when String.equal n1 n2 ->
List.iter2 check_same_type e1 e2;
List.iter2 (List.iter2 check_same_type) el1 el2;
List.iter2 check_same_fix_binder bl1 bl2
- | CPrim(_,i1), CPrim(_,i2) when i1=i2 -> ()
- | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when s1=s2 ->
+ | CPrim(_,i1), CPrim(_,i2) when prim_token_eq i1 i2 -> ()
+ | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when String.equal s1 s2 ->
check_same_type e1 e2
- | _ when ty1=ty2 -> ()
+ | _ when Pervasives.(=) ty1 ty2 -> () (** FIXME *)
| _ -> failwith "not same type"
and check_same_binder (nal1,_,e1) (nal2,_,e2) =
List.iter2 (fun (_,na1) (_,na2) ->
- if na1<>na2 then failwith "not same name") nal1 nal2;
+ if name_eq na1 na2 then failwith "not same name") nal1 nal2;
check_same_type e1 e2
and check_same_fix_binder bl1 bl2 =
@@ -280,16 +289,16 @@ let drop_implicits_in_patt cst nb_expl args =
impls_fit [] (imps,args)
let has_curly_brackets ntn =
- String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
- String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
+ String.length ntn >= 6 && (String.equal (String.sub ntn 0 6) "{ _ } " ||
+ String.equal (String.sub ntn (String.length ntn - 6) 6) " { _ }" ||
String.string_contains ~where:ntn ~what:" { _ } ")
let rec wildcards ntn n =
- if n = String.length ntn then []
- else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
+ if Int.equal n (String.length ntn) then []
+ else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
and spaces ntn n =
- if n = String.length ntn then []
- else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
+ if Int.equal n (String.length ntn) then []
+ else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
let expand_curly_brackets loc mknot ntn l =
let ntn' = ref ntn in
@@ -299,7 +308,7 @@ let expand_curly_brackets loc mknot ntn l =
| a::l ->
let a' =
let p = List.nth (wildcards !ntn' 0) i - 2 in
- if p>=0 & p+5 <= String.length !ntn' & String.sub !ntn' p 5 = "{ _ }"
+ if p>=0 & p+5 <= String.length !ntn' && String.equal (String.sub !ntn' p 5) "{ _ }"
then begin
ntn' :=
String.sub !ntn' 0 p ^ "_" ^
@@ -333,14 +342,16 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
mknot (loc,ntn,l)
let make_notation loc ntn (terms,termlists,binders as subst) =
- if termlists <> [] or binders <> [] then CNotation (loc,ntn,subst) else
- make_notation_gen loc ntn
- (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
- (fun (loc,p) -> CPrim (loc,p))
- destPrim terms
+ if not (List.is_empty termlists) || not (List.is_empty binders) then
+ CNotation (loc,ntn,subst)
+ else
+ make_notation_gen loc ntn
+ (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
+ (fun (loc,p) -> CPrim (loc,p))
+ destPrim terms
let make_pat_notation loc ntn (terms,termlists as subst) args =
- if termlists <> [] then CPatNotation (loc,ntn,subst,args) else
+ if not (List.is_empty termlists) then CPatNotation (loc,ntn,subst,args) else
make_notation_gen loc ntn
(fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),args))
(fun (loc,p) -> CPatPrim (loc,p))
@@ -348,7 +359,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args =
let mkPat loc qid l =
(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
- if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
+ if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l)
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -440,7 +451,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
List.map (extern_cases_pattern_in_scope subscope vars) c)
substlist in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
- let l2' = if !Topconstr.oldfashion_patterns || ll <> [] then l2
+ let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2
else
match drop_implicits_in_patt gr nb_to_drop l2 with
|Some true_args -> true_args
@@ -462,7 +473,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
|Some true_args -> true_args
|None -> raise No_match
in
- assert (substlist = []);
+ assert (List.is_empty substlist);
mkPat loc qid (List.rev_append l1 l2')
and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
@@ -539,7 +550,7 @@ let is_significant_implicit a =
not (is_hole a)
let is_needed_for_correct_partial_application tail imp =
- tail = [] & not (maximal_insertion_of imp)
+ List.is_empty tail && not (maximal_insertion_of imp)
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
@@ -566,33 +577,33 @@ let explicitize loc inctx impl (cf,f) args =
| [], _ -> [] in
match is_projection (List.length args) cf with
| Some i as ip ->
- if impl <> [] & is_status_implicit (List.nth impl (i-1)) then
+ if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
let f' = match f with CRef f -> f | _ -> assert false in
CAppExpl (loc,(ip,f'),args)
else
let (args1,args2) = List.chop i args in
- let (impl1,impl2) = if impl=[] then [],[] else List.chop i impl in
+ let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
CApp (loc,(Some (List.length args1),f),args1@args2)
| None ->
let args = exprec 1 (args,impl) in
- if args = [] then f else CApp (loc, (None, f), args)
+ if List.is_empty args then f else CApp (loc, (None, f), args)
let extern_global loc impl f =
if not !Constrintern.parsing_explicit &&
- impl <> [] && List.for_all is_status_implicit impl
+ not (List.is_empty impl) && List.for_all is_status_implicit impl
then
CAppExpl (loc, (None, f), [])
else
CRef f
let extern_app loc inctx impl (cf,f) args =
- if args = [] then
+ if List.is_empty args then
(* If coming from a notation "Notation a := @b" *)
CAppExpl (loc, (None, f), [])
else if not !Constrintern.parsing_explicit &&
- ((!Flags.raw_print or
+ ((!Flags.raw_print ||
(!print_implicits & not !print_implicits_explicit_args)) &
List.exists is_status_implicit impl)
then
@@ -629,7 +640,7 @@ let rec remove_coercions inctx = function
been confused with ordinary application or would have need
a surrounding context and the coercion to funclass would
have been made explicit to match *)
- if l = [] then a' else GApp (loc,a',l)
+ if List.is_empty l then a' else GApp (loc,a',l)
| _ -> c
with Not_found -> c)
| c -> c
@@ -767,11 +778,16 @@ let rec extern inctx scopes vars r =
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
- Anonymous, GVar (_,id) when
- rtntypopt<>None & occur_glob_constr id (Option.get rtntypopt)
- -> Some (Loc.ghost,Anonymous)
+ | Anonymous, GVar (_, id) ->
+ begin match rtntypopt with
+ | None -> None
+ | Some ntn ->
+ if occur_glob_constr id ntn then
+ Some (Loc.ghost, Anonymous)
+ else None
+ end
| Anonymous, _ -> None
- | Name id, GVar (_,id') when id=id' -> None
+ | Name id, GVar (_,id') when id_eq id id' -> None
| Name _, _ -> Some (Loc.ghost,na) in
(sub_extern false scopes vars tm,
(na',Option.map (fun (loc,ind,nal) ->
@@ -843,7 +859,7 @@ and factorize_prod scopes vars na bk aty c =
let c = extern_typ scopes vars c in
match na, c with
| Name id, CProdN (loc,[nal,Default bk',ty],c)
- when bk = bk' && is_same_type aty ty
+ when binding_kind_eq bk bk' && is_same_type aty ty
& not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
nal,c
| _ ->
@@ -853,7 +869,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
let c = sub_extern inctx scopes vars c in
match c with
| CLambdaN (loc,[nal,Default bk',ty],c)
- when bk = bk' && is_same_type aty ty
+ when binding_kind_eq bk bk' && is_same_type aty ty
& not (occur_name na ty) (* avoid na in ty escapes scope *) ->
nal,c
| _ ->
@@ -951,8 +967,8 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
extern true (scopt,scl@scopes) vars c, None)
terms in
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in
- if l = [] then a else CApp (loc,(None,a),l) in
- if args = [] then e
+ if List.is_empty l then a else CApp (loc,(None,a),l) in
+ if List.is_empty args then e
else
let args = extern_args (extern true) scopes vars args argsscopes in
explicitize loc false argsimpls (None,e) args
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 57de9da33..2ee8ed02f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -191,17 +191,17 @@ let compute_internalization_env env ty =
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
- if n = String.length ntn then []
- else let l = spaces ntn (n+1) in if ntn.[n] = '_' then n::l else l
+ if Int.equal n (String.length ntn) then []
+ else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
and spaces ntn n =
- if n = String.length ntn then []
- else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
+ if Int.equal n (String.length ntn) then []
+ else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
let expand_notation_string ntn n =
let pos = List.nth (wildcards ntn 0) n in
let hd = if Int.equal pos 0 then "" else String.sub ntn 0 pos in
let tl =
- if pos = String.length ntn then ""
+ if Int.equal pos (String.length ntn) then ""
else String.sub ntn (pos+1) (String.length ntn - pos -1) in
hd ^ "{ _ }" ^ tl
@@ -243,10 +243,10 @@ type intern_env = {
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
-let make_current_scope = function
- | (Some tmp_scope,(sc::_ as scopes)) when sc = tmp_scope -> scopes
- | (Some tmp_scope,scopes) -> tmp_scope::scopes
- | None,scopes -> scopes
+let make_current_scope tmp scopes = match tmp, scopes with
+| Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes
+| Some tmp_scope, scopes -> tmp_scope :: scopes
+| None, scopes -> scopes
let pr_scope_stack = function
| [] -> str "the empty scope stack"
@@ -268,17 +268,16 @@ let error_expect_binder_notation_type loc id =
let set_var_scope loc id istermvar env ntnvars =
try
let idscopes,typ = List.assoc id ntnvars in
- if istermvar then
+ let () = if istermvar then
(* scopes have no effect on the interpretation of identifiers *)
- if !idscopes = None then
- idscopes := Some (env.tmp_scope,env.scopes)
- else
- if make_current_scope (Option.get !idscopes)
- <> make_current_scope (env.tmp_scope,env.scopes)
- then
- error_inconsistent_scope loc id
- (make_current_scope (Option.get !idscopes))
- (make_current_scope (env.tmp_scope,env.scopes));
+ begin match !idscopes with
+ | None -> idscopes := Some (env.tmp_scope, env.scopes)
+ | Some (tmp, scope) ->
+ let s1 = make_current_scope tmp scope in
+ let s2 = make_current_scope env.tmp_scope env.scopes in
+ if not (List.equal String.equal s1 s2) then error_inconsistent_scope loc id s1 s2
+ end
+ in
match typ with
| NtnInternTypeBinder ->
if istermvar then error_expect_binder_notation_type loc id
@@ -444,12 +443,15 @@ let intern_generalization intern env lvar loc bk ak c =
let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:env.ids c in
let env', c' =
let abs =
- let pi =
- match ak with
+ let pi = match ak with
| Some AbsPi -> true
- | None when env.tmp_scope = Some Notation.type_scope
- || List.mem Notation.type_scope env.scopes -> true
- | _ -> false
+ | Some _ -> false
+ | None ->
+ let is_type_scope = match env.tmp_scope with
+ | None -> false
+ | Some sc -> String.equal sc Notation.type_scope
+ in
+ is_type_scope || List.mem Notation.type_scope env.scopes
in
if pi then
(fun (id, loc') acc ->
@@ -467,7 +469,7 @@ let intern_generalization intern env lvar loc bk ak c =
(* Syntax extensions *)
let option_mem_assoc id = function
- | Some (id',c) -> id = id'
+ | Some (id',c) -> id_eq id id'
| None -> false
let find_fresh_name renaming (terms,termlists,binders) id =
@@ -491,7 +493,7 @@ let traverse_binder (terms,_,_ as subst)
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
let id' = find_fresh_name renaming subst id in
- let renaming' = if id=id' then renaming else (id,id')::renaming in
+ let renaming' = if id_eq id id' then renaming else (id,id')::renaming in
(renaming',env), Name id'
let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c))
@@ -508,7 +510,7 @@ let rec subordinate_letins letins = function
letins,[]
let rec subst_iterator y t = function
- | GVar (_,id) as x -> if id = y then t else x
+ | GVar (_,id) as x -> if id_eq id y then t else x
| x -> map_glob_constr (subst_iterator y t) x
let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
@@ -622,7 +624,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
then
(set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
(* Is [id] the special variable for recursive notations *)
- else if ntnvars <> [] && id = ldots_var
+ else if ntnvars != [] && id_eq id ldots_var
then
GVar (loc,id), [], [], []
else
@@ -650,7 +652,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let find_appl_head_data = function
| GRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
| GApp (_,GRef (_,ref),l) as x
- when l <> [] & Flags.version_strictly_greater Flags.V8_2 ->
+ when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
x,List.map (drop_first_implicits n) (implicits_of_global ref),
List.skipn_at_least n (find_arguments_scope ref),[]
@@ -660,11 +662,13 @@ let error_not_enough_arguments loc =
user_err_loc (loc,"",str "Abbreviation is not applied enough.")
let check_no_explicitation l =
- let l = List.filter (fun (a,b) -> b <> None) l in
- if l <> [] then
- let loc = fst (Option.get (snd (List.hd l))) in
- user_err_loc
- (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
+ let is_unset (a, b) = match b with None -> false | Some _ -> true in
+ let l = List.filter is_unset l in
+ match l with
+ | [] -> ()
+ | (_, None) :: _ -> assert false
+ | (_, Some (loc, _)) :: _ ->
+ user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
let dump_extended_global loc = function
| TrueGlobal ref -> Dumpglob.add_glob loc ref
@@ -735,7 +739,7 @@ let rec simple_adjust_scopes n scopes =
(* Note: they can be less scopes than arguments but also more scopes *)
(* than arguments because extra scopes are used in the presence of *)
(* coercions to funclass *)
- if n=0 then [] else match scopes with
+ if Int.equal n 0 then [] else match scopes with
| [] -> None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
@@ -785,7 +789,7 @@ let check_linearity lhs ids =
(* Match the number of pattern against the number of matched args *)
let check_number_of_pattern loc n l =
let p = List.length l in
- if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
+ if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
let check_or_pat_variables loc ids idsl =
if List.exists (fun ids' -> not (List.eq_set ids ids')) idsl then
@@ -797,8 +801,8 @@ let check_or_pat_variables loc ids idsl =
let check_constructor_length env loc cstr len_pl pl0 =
let nargs = Inductiveops.mis_constructor_nargs cstr in
let n = len_pl + List.length pl0 in
- if n = nargs then false else
- (n = (fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr) ||
+ if Int.equal n nargs then false else
+ (Int.equal n ((fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr)) ||
(error_wrong_numarg_constructor_loc loc env cstr
(nargs - (Inductiveops.inductive_nparams (fst cstr))))
@@ -809,8 +813,8 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
let rec aux i = function
|[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
- ((if args_len = nargs then false
- else args_len = nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
+ ((if Int.equal args_len nargs then false
+ else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
,l)
|imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out)
@@ -853,7 +857,7 @@ let find_constructor loc add_params ref =
|IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.")
|_ -> anomaly "unexpected global_reference in pattern") ref in
cstr, (function (ind,_ as c) -> match add_params with
- |Some nb_args -> let nb = if nb_args = Inductiveops.constructor_nrealhyps c
+ |Some nb_args -> let nb = if Int.equal nb_args (Inductiveops.constructor_nrealhyps c)
then fst (Inductiveops.inductive_nargs ind)
else Inductiveops.inductive_nparams ind in
Util.List.make nb ([],[([],PatVar(Loc.ghost,Anonymous))])
@@ -889,15 +893,16 @@ let sort_fields mode loc l completer =
| [] -> anomaly "Number of projections mismatch"
| (_, regular)::tm ->
let boolean = not regular in
- if ConstRef name = global_reference_of_reference refer
- then
+ begin match global_reference_of_reference refer with
+ | ConstRef name' when eq_constant name name' ->
if boolean && mode then
user_err_loc (loc, "", str"No local fields allowed in a record construction.")
else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
- else
+ | _ ->
build_patt b tm (if boolean&&mode then i else i + 1)
(if boolean && mode then acc
- else fst acc, (i, ConstRef name) :: snd acc))
+ else fst acc, (i, ConstRef name) :: snd acc)
+ end)
| None :: b-> (* we don't want anonymous fields *)
if mode then
user_err_loc (loc, "", str "This record contains anonymous fields.")
@@ -929,7 +934,7 @@ let sort_fields mode loc l completer =
(loc, "",
str "This record contains fields of different records.")
| (i, a) :: b->
- if glob_refer = a
+ if eq_gr glob_refer a
then (i,List.rev_append acc l)
else add_patt b ((i,a)::acc)
in
@@ -957,7 +962,12 @@ let sort_fields mode loc l completer =
(* [merge_aliases] returns the sets of all aliases encountered at this
point and a substitution mapping extra aliases to the first one *)
let merge_aliases (ids,asubst as _aliases) id =
- ids@[id], if ids=[] then asubst else (id, List.hd ids)::asubst
+ let ans = ids @ [id] in
+ let subst = match ids with
+ | [] -> asubst
+ | id' :: _ -> (id, id') :: asubst
+ in
+ (ans, subst)
let alias_of = function
| ([],_) -> Anonymous
@@ -977,7 +987,7 @@ let message_redundant_alias (id1,id2) =
let rec subst_pat_iterator y t p = match p with
| RCPatAtom (_,id) ->
- begin match id with Some x when x = y -> t |_ -> p end
+ begin match id with Some x when id_eq x y -> t | _ -> p end
| RCPatCstr (loc,id,l1,l2) ->
RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
List.map (subst_pat_iterator y t) l2)
@@ -994,12 +1004,12 @@ let drop_notations_pattern looked_for =
(match a with
| NRef g ->
looked_for g;
- let () = assert (vars = []) in
+ let () = assert (List.is_empty vars) in
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g, [], List.map2 (in_pat_sc env) argscs pats)
| NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *)
looked_for g;
- let () = assert (vars = []) in
+ let () = assert (List.is_empty vars) in
let (argscs,_) = find_remaining_scopes pats [] g in
Some (g, List.map2 (in_pat_sc env) argscs pats, [])
| NApp (NRef g,args) ->
@@ -1074,7 +1084,7 @@ let drop_notations_pattern looked_for =
and in_pat_sc env x = in_pat {env with tmp_scope = x}
and in_not loc env (subst,substlist as fullsubst) args = function
| NVar id ->
- assert (args = []);
+ let () = assert (List.is_empty args) in
begin
(* subst remembers the delimiters stack in the interpretation *)
(* of the notations *)
@@ -1083,7 +1093,7 @@ let drop_notations_pattern looked_for =
in_pat {env with scopes=subscopes@env.scopes;
tmp_scope = scopt} a
with Not_found ->
- if id = ldots_var then RCPatAtom (loc,Some id) else
+ if id_eq id ldots_var then RCPatAtom (loc,Some id) else
anomaly ("Unbound pattern notation variable: "^(string_of_id id))
end
| NRef g ->
@@ -1097,7 +1107,7 @@ let drop_notations_pattern looked_for =
List.map2 (fun x -> in_not loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
List.map2 (in_pat_sc env) argscs2 args)
| NList (x,_,iter,terminator,lassoc) ->
- let () = assert (args = []) in
+ let () = assert (List.is_empty args) in
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
let (l,(scopt,subscopes)) = List.assoc x substlist in
@@ -1108,7 +1118,9 @@ let drop_notations_pattern looked_for =
(if lassoc then List.rev l else l) termin
with Not_found ->
anomaly "Inconsistent substitution of recursive notation")
- | NHole _ -> let () = assert (args = []) in RCPatAtom (loc,None)
+ | NHole _ ->
+ let () = assert (List.is_empty args) in
+ RCPatAtom (loc, None)
| t -> error_invalid_pattern_notation loc
in in_pat
@@ -1125,7 +1137,8 @@ let rec intern_pat genv (ids,asubst as aliases) pat =
intern_pat genv aliases' p
| RCPatCstr (loc, head, expl_pl, pl) ->
if !oldfashion_patterns then
- let c,idslpl1 = find_constructor loc (if expl_pl = [] then Some (List.length pl) else None) head in
+ let len = if List.is_empty expl_pl then Some (List.length pl) else None in
+ let c,idslpl1 = find_constructor loc len head in
let with_letin =
check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl)
@@ -1140,7 +1153,7 @@ let rec intern_pat genv (ids,asubst as aliases) pat =
| RCPatAtom (loc, None) ->
(ids,[asubst, PatVar (loc,alias_of aliases)])
| RCPatOr (loc, pl) ->
- assert (pl <> []);
+ assert (not (List.is_empty pl));
let pl' = List.map (intern_pat genv aliases) pl in
let (idsl,pl') = List.split pl' in
let ids = List.hd idsl in
@@ -1183,10 +1196,14 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
| _ -> false
let merge_impargs l args =
+ let test x = function
+ | (_, Some (_, y)) -> explicitation_eq x y
+ | _ -> false
+ in
List.fold_right (fun a l ->
match a with
| (_,Some (_,(ExplByName id as x))) when
- List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l
+ List.exists (test x) args -> l
| _ -> a::l)
l args
@@ -1195,7 +1212,7 @@ let check_projection isproj nargs r =
| GRef (loc, ref), Some _ ->
(try
let n = Recordops.find_projection_nparams ref + 1 in
- if nargs <> n then
+ if not (Int.equal nargs n) then
user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
with Not_found ->
user_err_loc
@@ -1212,7 +1229,7 @@ let set_hole_implicit i b = function
| _ -> anomaly "Only refs have implicits"
let exists_implicit_name id =
- List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp)
+ List.exists (fun imp -> is_status_implicit imp && id_eq id (name_of_implicit imp))
let extract_explicit_arg imps args =
let rec aux = function
@@ -1361,7 +1378,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
| CApp (loc, (isproj,f), args) ->
let isproj,f,args = match f with
(* Compact notations like "t.(f args') args" *)
- | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args
+ | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> isproj,f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> isproj,f,args in
let (c,impargs,args_scopes,l),args =
@@ -1472,7 +1489,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
(* Expands a disjunction of multiple pattern *)
and intern_disjunctive_multiple_pattern env loc n mpl =
- assert (mpl <> []);
+ assert (not (List.is_empty mpl));
let mpl' = List.map (intern_multiple_pattern env n) mpl in
let (idsl,mpl') = List.split mpl' in
let ids = List.hd idsl in
@@ -1554,10 +1571,10 @@ let internalize sigma globalenv env allow_patvar lvar c =
let l = select_impargs_size (List.length args) l in
let eargs, rargs = extract_explicit_arg l args in
if !parsing_explicit then
- if eargs <> [] then
- error "Arguments given by name or position not supported in explicit mode."
- else
- intern_args env subscopes rargs
+ begin match eargs with
+ | [] -> intern_args env subscopes rargs
+ | _ -> error "Arguments given by name or position not supported in explicit mode."
+ end
else
let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
@@ -1569,7 +1586,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
let eargs' = List.remove_assoc id eargs in
intern enva a :: aux (n+1) impl' subscopes' eargs' rargs
with Not_found ->
- if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then
+ if List.is_empty rargs && List.is_empty eargs && not (maximal_insertion_of imp) then
(* Less regular arguments than expected: complete *)
(* with implicit arguments if maximal insertion is set *)
[]
@@ -1580,14 +1597,14 @@ let internalize sigma globalenv env allow_patvar lvar c =
| (imp::impl', a::rargs') ->
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
| (imp::impl', []) ->
- if eargs <> [] then
+ if not (List.is_empty eargs) then
(let (id,(loc,_)) = List.hd eargs in
user_err_loc (loc,"",str "Not enough non implicit \
arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
| ([], rargs) ->
- assert (eargs = []);
+ assert (List.is_empty eargs);
intern_args env subscopes rargs
in aux 1 l subscopes eargs rargs
@@ -1691,7 +1708,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
| None -> ref Evd.empty
| Some evdref -> evdref
in
- let istype = kind = IsType in
+ let istype = kind == IsType in
let c = intern_gen kind ~impls !evdref env c in
let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
understand_tcc_evars ~fail_evar evdref env kind c, imps
@@ -1777,7 +1794,7 @@ let interp_rawcontext_gen understand_type understand_judgment env bl =
let t = understand_type env t' in
let d = (na,None,t) in
let impls =
- if k = Implicit then
+ if k == Implicit then
let na = match na with Name n -> Some n | Anonymous -> None in
(ExplByPos (n, na), (true, true, true)) :: impls
else impls
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 531ca5bf4..607355873 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -67,7 +67,7 @@ let check_required_library d =
let dir = make_dirpath (List.rev d') in
let mp = (fst(Lib.current_prefix())) in
let current_dir = match mp with
- | MPfile dp -> (dir=dp)
+ | MPfile dp -> dir_path_eq dir dp
| _ -> false
in
if not (Library.library_is_loaded dir) then
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 101645dfc..f87130e57 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
(* Dump of globalization (to be used by coqdoc) *)
@@ -138,7 +139,7 @@ let add_glob_gen loc sp lib_dp ty =
dump_ref loc filepath modpath ident ty
let add_glob loc ref =
- if dump () && loc <> Loc.ghost then
+ if dump () && not (Loc.is_ghost loc) then
let sp = Nametab.path_of_global ref in
let lib_dp = Lib.library_part ref in
let ty = type_of_global_ref ref in
@@ -149,7 +150,7 @@ let mp_of_kn kn =
Names.MPdot (mp,l)
let add_glob_kn loc kn =
- if dump () && loc <> Loc.ghost then
+ if dump () && not (Loc.is_ghost loc) then
let sp = Nametab.path_of_syndef kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
add_glob_gen loc sp lib_dp "syndef"
@@ -174,7 +175,7 @@ let dump_constraint ((loc, n), _, _) sec ty =
let dump_modref loc mp ty =
if dump () then
let (dp, l) = Lib.split_modpath mp in
- let l = if l = [] then l else Util.List.drop_last l in
+ let l = if List.is_empty l then l else List.drop_last l in
let fp = Names.string_of_dirpath dp in
let mp = Names.string_of_dirpath (Names.make_dirpath l) in
let bl,el = interval loc in
@@ -207,19 +208,19 @@ let cook_notation df sc =
let l = String.length df - 1 in
let i = ref 0 in
while !i <= l do
- assert (df.[!i] <> ' ');
- if df.[!i] = '_' && (!i = l || df.[!i+1] = ' ') then
+ assert (df.[!i] != ' ');
+ if df.[!i] == '_' && (Int.equal !i l || df.[!i+1] == ' ') then
(* Next token is a non-terminal *)
(ntn.[!j] <- 'x'; incr j; incr i)
else begin
(* Next token is a terminal *)
ntn.[!j] <- '\''; incr j;
- while !i <= l && df.[!i] <> ' ' do
+ while !i <= l && df.[!i] != ' ' do
if df.[!i] < ' ' then
let c = char_of_int (int_of_char 'A' + int_of_char df.[!i] - 1) in
(String.blit ("'^" ^ String.make 1 c) 0 ntn !j 3; j := !j+3; incr i)
else begin
- if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
+ if df.[!i] == '\'' then (ntn.[!j] <- '\''; incr j);
ntn.[!j] <- df.[!i]; incr j; incr i
end
done;
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 1192423c2..382c38da3 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Util
open Glob_term
open Constrexpr
open Misctypes
@@ -173,7 +174,7 @@ let wit_opt t = OptArgType t
let wit_pair t1 t2 = PairArgType (t1,t2)
let in_gen t o = (t,Obj.repr o)
-let out_gen t (t',o) = if t = t' then Obj.magic o else failwith "out_gen"
+let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
let genarg_tag (s,_) = s
let fold_list0 f = function
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 64e890616..13c39f60d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -32,7 +32,7 @@ let _ =
Summary.init_function = (fun () -> generalizable_table := Idpred.empty) }
let declare_generalizable_ident table (loc,id) =
- if id <> root_of_id id then
+ if not (id_eq id (root_of_id id)) then
user_err_loc(loc,"declare_generalizable_ident",
(pr_id id ++ str
" is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
@@ -210,7 +210,11 @@ let combine_params avoid fn applied needed =
List.partition
(function
(t, Some (loc, ExplByName id)) ->
- if not (List.exists (fun (_, (id', _, _)) -> Name id = id') needed) then
+ let is_id (_, (na, _, _)) = match na with
+ | Name id' -> id_eq id id'
+ | Anonymous -> false
+ in
+ if not (List.exists is_id needed) then
user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id);
true
| _ -> false) applied
@@ -219,7 +223,11 @@ let combine_params avoid fn applied needed =
(fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
named
in
- let needed = List.filter (fun (_, (_, b, _)) -> b = None) needed in
+ let is_unset (_, (_, b, _)) = match b with
+ | None -> true
+ | Some _ -> false
+ in
+ let needed = List.filter is_unset needed in
let rec aux ids avoid app need =
match app, need with
[], [] -> List.rev ids, avoid
@@ -280,9 +288,13 @@ let implicit_application env ?(allow_partial=true) f ty =
let (ci, rd) = c.cl_context in
if not allow_partial then
begin
- let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
- let needlen = List.fold_left (fun acc x -> if x = None then succ acc else acc) 0 ci in
- if needlen <> applen then
+ let opt_succ x n = match x with
+ | None -> succ n
+ | Some _ -> n
+ in
+ let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+ if not (Int.equal needlen applen) then
Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
end;
let pars = List.rev (List.combine ci rd) in
@@ -291,15 +303,16 @@ let implicit_application env ?(allow_partial=true) f ty =
in c, avoid
let implicits_of_glob_constr ?(with_products=true) l =
- let add_impl i na bk l =
- if bk = Implicit then
- let name =
- match na with
- | Name id -> Some id
- | Anonymous -> None
- in
- (ExplByPos (i, name), (true, true, true)) :: l
- else l in
+ let add_impl i na bk l = match bk with
+ | Implicit ->
+ let name =
+ match na with
+ | Name id -> Some id
+ | Anonymous -> None
+ in
+ (ExplByPos (i, name), (true, true, true)) :: l
+ | _ -> l
+ in
let rec aux i c =
let abs na bk b =
add_impl i na bk (aux (succ i) b)
@@ -307,11 +320,13 @@ let implicits_of_glob_constr ?(with_products=true) l =
match c with
| GProd (loc, na, bk, t, b) ->
if with_products then abs na bk b
- else
- (if bk = Implicit then
+ else
+ let () = match bk with
+ | Implicit ->
msg_warning (strbrk "Ignoring implicit status of product binder " ++
- pr_name na ++ strbrk " and following binders");
- [])
+ pr_name na ++ strbrk " and following binders")
+ | _ -> ()
+ in []
| GLambda (loc, na, bk, t, b) -> abs na bk b
| GLetIn (loc, na, t, b) -> aux i b
| GRec (_, fix_kind, nas, args, tys, bds) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index a3a6708eb..50a536eab 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -130,7 +130,7 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
(* Exportation of scopes *)
let open_scope i (_,(local,op,sc)) =
- if i=1 then
+ if Int.equal i 1 then
let sc = match sc with
| Scope sc -> Scope (normalize_scope sc)
| _ -> sc
@@ -181,7 +181,7 @@ let declare_delimiters scope key =
let newsc = { sc with delimiters = Some key } in
begin match sc.delimiters with
| None -> scope_map := Gmap.add scope newsc !scope_map
- | Some oldkey when oldkey = key -> ()
+ | Some oldkey when String.equal oldkey key -> ()
| Some oldkey ->
Flags.if_warn msg_warning
(strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
@@ -189,7 +189,7 @@ let declare_delimiters scope key =
end;
try
let oldscope = Gmap.find key !delimiters_map in
- if oldscope = scope then ()
+ if String.equal oldscope scope then ()
else begin
Flags.if_warn msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope));
delimiters_map := Gmap.add key scope !delimiters_map
@@ -311,20 +311,24 @@ let find_with_delimiters = function
let rec find_without_delimiters find (ntn_scope,ntn) = function
| Scope scope :: scopes ->
(* Is the expected ntn/numpr attached to the most recently open scope? *)
- if Some scope = ntn_scope then
+ begin match ntn_scope with
+ | Some scope' when String.equal scope scope' ->
Some (None,None)
- else
+ | _ ->
(* If the most recently open scope has a notation/numeral printer
but not the expected one then we need delimiters *)
if find scope then
find_with_delimiters ntn_scope
else
find_without_delimiters find (ntn_scope,ntn) scopes
+ end
| SingleNotation ntn' :: scopes ->
- if ntn_scope = None & ntn = Some ntn' then
- Some (None,None)
- else
+ begin match ntn_scope, ntn with
+ | None, Some ntn when String.equal ntn ntn' ->
+ Some (None, None)
+ | _ ->
find_without_delimiters find (ntn_scope,ntn) scopes
+ end
| [] ->
(* Can we switch to [scope]? Yes if it has defined delimiters *)
find_with_delimiters ntn_scope
@@ -344,12 +348,20 @@ let level_of_notation ntn =
let declare_notation_interpretation ntn scopt pat df =
let scope = match scopt with Some s -> s | None -> default_scope in
let sc = find_scope scope in
- if Gmap.mem ntn sc.notations then
- Flags.if_warn msg_warning (strbrk ("Notation "^ntn^" was already used"^
- (if scopt = None then "" else " in scope "^scope)));
+ let () =
+ if Gmap.mem ntn sc.notations then
+ let which_scope = match scopt with
+ | None -> ""
+ | Some _ -> " in scope " ^ scope in
+ let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in
+ Flags.if_warn msg_warning (strbrk message)
+ in
let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
- scope_map := Gmap.add scope sc !scope_map;
- if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
+ let () = scope_map := Gmap.add scope sc !scope_map in
+ begin match scopt with
+ | None -> scope_stack := SingleNotation ntn :: !scope_stack
+ | Some _ -> ()
+ end
let declare_uninterpretation rule (metas,c as pat) =
let (key,n) = notation_constr_key c in
@@ -360,7 +372,7 @@ let rec find_interpretation ntn find = function
| Scope scope :: scopes ->
(try let (pat,df) = find scope in pat,(df,Some scope)
with Not_found -> find_interpretation ntn find scopes)
- | SingleNotation ntn'::scopes when ntn' = ntn ->
+ | SingleNotation ntn'::scopes when String.equal ntn' ntn ->
(try let (pat,df) = find default_scope in pat,(df,None)
with Not_found ->
(* e.g. because single notation only for constr, not cases_pattern *)
@@ -473,7 +485,7 @@ let exists_notation_in_scope scopt ntn r =
try
let sc = Gmap.find scope !scope_map in
let (r',_) = Gmap.find ntn sc.notations in
- r' = r
+ Pervasives.(=) r' r (** FIXME *)
with Not_found -> false
let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
@@ -575,11 +587,11 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
(ArgsScopeNoDischarge,r',scl'',cls')
let discharge_arguments_scope (_,(req,r,l,_)) =
- if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
+ if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
else Some (req,Lib.discharge_global r,l,[])
let classify_arguments_scope (req,_,_,_ as obj) =
- if req = ArgsScopeNoDischarge then Dispose else Substitute obj
+ if req == ArgsScopeNoDischarge then Dispose else Substitute obj
let rebuild_arguments_scope (req,r,l,_) =
match req with
@@ -679,7 +691,7 @@ let pr_delimiters_info = function
| Some key -> str "Delimiting key is " ++ str key
let classes_of_scope sc =
- Gmap.fold (fun cl sc' l -> if sc = sc' then cl::l else l) !scope_class_map []
+ Gmap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map []
let pr_scope_class = function
| ScopeSort -> str "Sort"
@@ -687,9 +699,11 @@ let pr_scope_class = function
let pr_scope_classes sc =
let l = classes_of_scope sc in
- if l = [] then mt()
- else
- hov 0 (str ("Bound to class"^(if List.tl l=[] then "" else "es")) ++
+ match l with
+ | [] -> mt ()
+ | _ :: l ->
+ let opt_s = match l with [] -> "" | _ -> "es" in
+ hov 0 (str ("Bound to class" ^ opt_s) ++
spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
let pr_notation_info prglob ntn c =
@@ -697,10 +711,10 @@ let pr_notation_info prglob ntn c =
prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
let pr_named_scope prglob scope sc =
- (if scope = default_scope then
+ (if String.equal scope default_scope then
match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with
| 0 -> str "No lonely notation"
- | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s")
+ | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
else
str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters)
++ fnl ()
@@ -720,7 +734,7 @@ let pr_scopes prglob =
let rec find_default ntn = function
| Scope scope::_ when Gmap.mem ntn (find_scope scope).notations ->
Some scope
- | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope
+ | SingleNotation ntn'::_ when String.equal ntn ntn' -> Some default_scope
| _::scopes -> find_default ntn scopes
| [] -> None
@@ -730,17 +744,21 @@ let factorize_entries = function
let (ntn,l_of_ntn,rest) =
List.fold_left
(fun (a',l,rest) (a,c) ->
- if a = a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
+ if String.equal a a' then (a',c::l,rest) else (a,[c],(a',l)::rest))
(ntn,[c],[]) l in
(ntn,l_of_ntn)::rest
let browse_notation strict ntn map =
- let find =
- if String.contains ntn ' ' then (=) ntn
- else fun ntn' ->
+ let find ntn' =
+ if String.contains ntn ' ' then String.equal ntn ntn'
+ else
let toks = decompose_notation_key ntn' in
let trms = List.filter (function Terminal _ -> true | _ -> false) toks in
- if strict then [Terminal ntn] = trms else List.mem (Terminal ntn) trms in
+ if strict then match trms with
+ | [Terminal ntn'] -> String.equal ntn ntn'
+ | _ -> false
+ else
+ List.mem (Terminal ntn) trms in
let l =
Gmap.fold
(fun scope_name sc ->
@@ -775,7 +793,12 @@ let interp_notation_as_global_reference loc test ntn sc =
| [_,_,ref] -> ref
| [] -> error_notation_not_reference loc ntn
| refs ->
- let f (ntn,sc,ref) = find_default ntn !scope_stack = Some sc in
+ let f (ntn,sc,ref) =
+ let def = find_default ntn !scope_stack in
+ match def with
+ | None -> false
+ | Some sc' -> String.equal sc sc'
+ in
match List.filter f refs with
| [_,_,ref] -> ref
| [] -> error_notation_not_reference loc ntn
@@ -784,9 +807,9 @@ let interp_notation_as_global_reference loc test ntn sc =
let locate_notation prglob ntn scope =
let ntns = factorize_entries (browse_notation false ntn !scope_map) in
let scopes = Option.fold_right push_scope scope !scope_stack in
- if ntns = [] then
- str "Unknown notation"
- else
+ match ntns with
+ | [] -> str "Unknown notation"
+ | _ ->
t (str "Notation " ++
tab () ++ str "Scope " ++ tab () ++ fnl () ++
prlist (fun (ntn,l) ->
@@ -795,14 +818,14 @@ let locate_notation prglob ntn scope =
(fun (sc,r,(_,df)) ->
hov 0 (
pr_notation_info prglob df r ++ tbrk (1,2) ++
- (if sc = default_scope then mt () else (str ": " ++ str sc)) ++
+ (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
tbrk (1,2) ++
- (if Some sc = scope then str "(default interpretation)" else mt ())
+ (if Option.Misc.compare String.equal (Some sc) scope then str "(default interpretation)" else mt ())
++ fnl ()))
l) ntns)
let collect_notation_in_scope scope sc known =
- assert (scope <> default_scope);
+ assert (not (String.equal scope default_scope));
Gmap.fold
(fun ntn ((_,r),(_,df)) (l,known as acc) ->
if List.mem ntn known then acc else ((df,r)::l,ntn::known))
@@ -823,7 +846,7 @@ let collect_notations stack =
let ((_,r),(_,df)) =
Gmap.find ntn (find_scope default_scope).notations in
let all' = match all with
- | (s,lonelyntn)::rest when s = default_scope ->
+ | (s,lonelyntn)::rest when String.equal s default_scope ->
(s,(df,r)::lonelyntn)::rest
| _ ->
(default_scope,[df,r])::all in
@@ -835,8 +858,8 @@ let pr_visible_in_scope prglob (scope,ntns) =
List.fold_right
(fun (df,r) strm -> pr_notation_info prglob df r ++ fnl () ++ strm)
ntns (mt ()) in
- (if scope = default_scope then
- str "Lonely notation" ++ (if List.length ntns <> 1 then str "s" else mt())
+ (if String.equal scope default_scope then
+ str "Lonely notation" ++ (match ntns with [_] -> mt () | _ -> str "s")
else
str "Visible in scope " ++ str scope)
++ fnl () ++ strm
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d3c55c1f5..c0289fbad 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -122,35 +122,42 @@ 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))
+ | GApp (loc0,GVar(loc,v),c::l) when id_eq v ldots_var ->
+ begin match !sub with
+ | None ->
+ let () = sub := Some c in
+ begin match l with
+ | [] -> GVar (loc, ldots_var)
+ | _ :: _ -> GApp (loc0, GVar (loc, ldots_var), l)
+ end
+ | Some _ ->
+ (* Not narrowed enough to find only one recursive part *)
+ raise Not_found
+ end
| 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
+ | GVar (_,v) when id_eq 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 ->
+ | GVar (_,v1), GVar (_,v2) -> on_true_do (id_eq 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 name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
+ on_true_do (f ty1 ty2 & f c1 c2) add na1
+ | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
+ when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq 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 ->
+ | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
+ | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when name_eq na1 na2 ->
on_true_do (f b1 b2 & f c1 c2) add na1
| (GCases _ | GRec _
| GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
@@ -174,26 +181,38 @@ 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 ->
+ | GVar(_,v), term when id_eq v ldots_var ->
(* We found the pattern *)
- assert (!terminator = None); terminator := Some term;
+ assert (match !terminator with None -> true | Some _ -> false);
+ terminator := Some term;
true
- | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when v = ldots_var ->
+ | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when id_eq 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;
+ assert (match !terminator with None -> true | Some _ -> false);
+ terminator := Some term;
List.for_all2eq aux l1 l2
- | GVar (_,x), GVar (_,y) when x<>y ->
+ | GVar (_,x), GVar (_,y) when not (id_eq x y) ->
(* We found the position where it differs *)
- let lassoc = (!terminator <> None) in
+ let lassoc = match !terminator with None -> false | Some _ -> true in
let x,y = if lassoc then y,x else x,y in
- !diff = None && (diff := Some (x,y,Some lassoc); true)
+ begin match !diff with
+ | None ->
+ let () = diff := Some (x, y, Some 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;
- !diff = None && (diff := Some (x,y,None); aux c term)
+ begin match !diff with
+ | None ->
+ let () = diff := Some (x, y, None) in
+ aux c term
+ | Some _ -> false
+ end
| _ ->
compare_glob_constr aux (add_name found) c1 c2 in
if aux iterator subc then
@@ -230,7 +249,7 @@ let notation_constr_and_vars_of_glob_constr a =
with Not_found ->
found := keepfound;
match c with
- | GApp (_,GVar (loc,f),[c]) when f = ldots_var ->
+ | GApp (_,GVar (loc,f),[c]) when id_eq f ldots_var ->
(* Fall on the second part of the recursive pattern w/o having
found the first part *)
user_err_loc (loc,"",
@@ -262,7 +281,7 @@ let notation_constr_and_vars_of_glob_constr a =
| 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
+ 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)
@@ -281,7 +300,7 @@ let notation_constr_and_vars_of_glob_constr a =
let rec list_rev_mem_assoc x = function
| [] -> false
- | (_,x')::l -> x = x' || list_rev_mem_assoc x l
+ | (_,x')::l -> id_eq x x' || list_rev_mem_assoc x l
let check_variables vars recvars (found,foundrec,foundrecbinding) =
let useless_vars = List.map snd recvars in
@@ -474,17 +493,15 @@ let abstract_return_type_context_notation_constr =
exception No_match
let rec alpha_var id1 id2 = function
- | (i1,i2)::_ when i1=id1 -> i2 = id2
- | (i1,i2)::_ when i2=id2 -> i1 = id1
+ | (i1,i2)::_ when id_eq i1 id1 -> id_eq i2 id2
+ | (i1,i2)::_ when id_eq i2 id2 -> id_eq i1 id1
| _::idl -> alpha_var id1 id2 idl
- | [] -> id1 = id2
-
-let alpha_eq_val (x,y) = x = y
+ | [] -> id_eq id1 id2
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
+ if Pervasives.(=) v vvar then fullsigma (** FIXME *)
else raise No_match
with Not_found ->
(* Check that no capture of binding variables occur *)
@@ -497,10 +514,15 @@ let bind_binder (sigma,sigmalist,sigmabinders) x bl =
let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
- | GCoFix n1, GCoFix n2 -> n1 = n2
+ | GCoFix n1, GCoFix n2 -> Int.equal n1 n2
| GFix (nl1,n1), GFix (nl2,n2) ->
- n1 = n2 &&
- Array.for_all2 (fun (n1,_) (n2,_) -> n2 = None || n1 = n2) nl1 nl2
+ let test (n1, _) (n2, _) = match n1, n2 with
+ | _, None -> true
+ | Some id1, Some id2 -> Int.equal id1 id2
+ | _ -> false
+ in
+ Int.equal n1 n2 &&
+ Array.for_all2 test nl1 nl2
| _ -> false
let match_opt f sigma t1 t2 = match (t1,t2) with
@@ -522,7 +544,7 @@ 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 ->
+ when eq_constructor c1 c2 && Int.equal (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
@@ -550,7 +572,7 @@ let match_abinderlist_with_app match_fun metas sigma rest x iter termin =
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 <> [] ->
+ with No_match when not (List.is_empty acc) ->
acc, match_fun metas sigma rest termin in
let bl,sigma = aux sigma [] rest in
bind_binder sigma x bl
@@ -563,7 +585,7 @@ let match_alist match_fun metas sigma rest x iter termin lassoc =
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 <> [] ->
+ with No_match when not (List.is_empty 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)
@@ -596,7 +618,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
(* 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 ->
+ 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
@@ -608,13 +630,13 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
| 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 ->
+ 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
+ | GPatVar (_,(_,n1)), NPatVar n2 when id_eq 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 =
@@ -633,9 +655,9 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
| 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 ->
+ when sty1 == sty2
+ && Int.equal (List.length tml1) (List.length tml2)
+ && Int.equal (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 =
@@ -647,7 +669,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
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 ->
+ when Int.equal (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) =
@@ -657,8 +679,8 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
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
+ when match_fix_kind fk1 fk2 && Int.equal (Array.length idl1) (Array.length idl2) &&
+ Array.for_all2 (fun l1 l2 -> Int.equal (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) ->
@@ -676,7 +698,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
| 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
+ | GSort (_,s1), NSort s2 when glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -710,7 +732,8 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
match_in u alp metas sigma rhs1 rhs2
let match_notation_constr u c (metas,pat) =
- let vars = List.partition (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
+ let test (_, (_, x)) = match x with NtnTypeBinderList -> false | _ -> true in
+ let vars = List.partition test 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 *)
@@ -739,7 +762,7 @@ let add_patterns_for_params ind 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
+ if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *)
with Not_found ->
(* TODO: handle the case of multiple occs in different scopes *)
(var,v)::sigma,sigmalist,x
@@ -748,10 +771,10 @@ 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),(0,[])
| PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
- | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 ->
+ | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
sigma,(0,largs)
| PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
- when r1 = r2 ->
+ when eq_constructor r1 r2 ->
let l1 = add_patterns_for_params (fst r1) args1 in
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
@@ -772,10 +795,10 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
let match_ind_pattern metas sigma ind pats a2 =
match a2 with
- | NRef (IndRef r2) when ind = r2 ->
+ | NRef (IndRef r2) when eq_ind ind r2 ->
sigma,(0,pats)
| NApp (NRef (IndRef r2),l2)
- when ind = r2 ->
+ when eq_ind ind r2 ->
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
then
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 23fce79c1..3a865cb7d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -53,7 +53,7 @@ let _ =
Summary.init_function = init_reserved }
let declare_reserved_type_binding (loc,id) t =
- if id <> root_of_id id then
+ if not (id_eq id (root_of_id id)) then
user_err_loc(loc,"declare_reserved_type",
(pr_id id ++ str
" is not reservable: it must have no trailing digits, quote, or _"));
@@ -94,9 +94,10 @@ open Glob_term
let anonymize_if_reserved na t = match na with
| Name id as na ->
(try
- if not !Flags.raw_print &
- (try Notation_ops.notation_constr_of_glob_constr [] [] t
- = find_reserved_type id
+ if not !Flags.raw_print &&
+ (try
+ let ntn = Notation_ops.notation_constr_of_glob_constr [] [] t in
+ Pervasives.(=) ntn (find_reserved_type id) (** FIXME *)
with UserError _ -> false)
then GHole (Loc.ghost,Evar_kinds.BinderType na)
else t
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 202a3d770..cabd207e2 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -42,17 +42,19 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
let is_alias_of_already_visible_name sp = function
| _,NRef ref ->
let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
- dir = empty_dirpath && id = basename sp
+ dir_path_eq dir empty_dirpath && id_eq id (basename sp)
| _ ->
false
let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
if not (is_alias_of_already_visible_name sp pat) then begin
Nametab.push_syndef (Nametab.Exactly i) sp kn;
- if onlyparse = None then
+ match onlyparse with
+ | None ->
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared inbetween *)
Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ | _ -> ()
end
let cache_syntax_constant d =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index dd656d479..046904cf5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -153,16 +153,27 @@ let split_at_annot bl na =
let names = List.map snd (names_of_local_assums bl) in
match na with
| None ->
- if names = [] then error "A fixpoint needs at least one parameter."
- else [], bl
+ begin match names with
+ | [] -> error "A fixpoint needs at least one parameter."
+ | _ -> ([], bl)
+ end
| Some (loc, id) ->
let rec aux acc = function
| LocalRawAssum (bls, k, t) as x :: rest ->
- let l, r = List.split_when (fun (loc, na) -> na = Name id) bls in
- if r = [] then aux (x :: acc) rest
- else
- (List.rev (if l = [] then acc else LocalRawAssum (l, k, t) :: acc),
- LocalRawAssum (r, k, t) :: rest)
+ let test (_, na) = match na with
+ | Name id' -> id_eq id id'
+ | Anonymous -> false
+ in
+ let l, r = List.split_when test bls in
+ begin match r with
+ | [] -> aux (x :: acc) rest
+ | _ ->
+ let ans = match l with
+ | [] -> acc
+ | _ -> LocalRawAssum (l, k, t) :: acc
+ in
+ (List.rev ans, LocalRawAssum (r, k, t) :: rest)
+ end
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
| [] ->
user_err_loc(loc,"",
@@ -251,8 +262,8 @@ let locs_of_notation loc locs ntn =
let (bl, el) = Loc.unloc loc in
let locs = List.map Loc.unloc locs in
let rec aux pos = function
- | [] -> if pos = el then [] else [(pos,el-1)]
- | (ba,ea)::l ->if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+ | [] -> if Int.equal pos el then [] else [(pos,el-1)]
+ | (ba,ea)::l ->if Int.equal pos ba then aux ea l else (pos,ba-1)::aux ea l
in aux bl (Sort.list (fun l1 l2 -> fst l1 < fst l2) locs)
let ntn_loc loc (args,argslist,binderslist) =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 01:21:34 +0000