From a9a6c796d25130293584c7425b52f91b84c0f6ca Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 25 Nov 2012 17:39:00 +0000 Subject: Monomorphization (interp) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15999 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.ml | 128 ++++++++++++++++++--------------- interp/constrintern.ml | 157 +++++++++++++++++++++++------------------ interp/coqlib.ml | 2 +- interp/dumpglob.ml | 15 ++-- interp/genarg.ml | 3 +- interp/implicit_quantifiers.ml | 53 +++++++++----- interp/notation.ml | 101 ++++++++++++++++---------- interp/notation_ops.ml | 131 ++++++++++++++++++++-------------- interp/reserve.ml | 9 +-- interp/syntax_def.ml | 6 +- interp/topconstr.ml | 29 +++++--- 11 files changed, 372 insertions(+), 262 deletions(-) (limited to 'interp') 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) = -- cgit v1.2.3