diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 41 | ||||
| -rw-r--r-- | interp/constrextern.ml | 52 | ||||
| -rw-r--r-- | interp/constrintern.ml | 114 | ||||
| -rw-r--r-- | interp/modintern.ml | 11 | ||||
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/topconstr.ml | 24 |
6 files changed, 117 insertions, 133 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index a592b4cff8..3ba5d985f9 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -59,31 +59,31 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with let eq_located f (_, x) (_, y) = f x y -let rec cases_pattern_expr_eq p1 p2 = +let rec cases_pattern_expr_eq (l1, p1) (l2, p2) = if p1 == p2 then true else match p1, p2 with - | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) -> + | CPatAlias(a1,i1), CPatAlias(a2,i2) -> Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 - | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) -> + | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> eq_reference c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 - | CPatAtom(_,r1), CPatAtom(_,r2) -> + | CPatAtom(r1), CPatAtom(r2) -> Option.equal eq_reference r1 r2 - | CPatOr (_, a1), CPatOr (_, a2) -> + | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 - | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) -> + | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> String.equal n1 n2 && cases_pattern_notation_substitution_eq s1 s2 && List.equal cases_pattern_expr_eq l1 l2 - | CPatPrim(_,i1), CPatPrim(_,i2) -> + | CPatPrim i1, CPatPrim i2 -> prim_token_eq i1 i2 - | CPatRecord (_, l1), CPatRecord (_, l2) -> + | CPatRecord l1, CPatRecord l2 -> let equal (r1, e1) (r2, e2) = eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 in List.equal equal l1 l2 - | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) -> + | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> String.equal s1 s2 && cases_pattern_expr_eq e1 e2 | _ -> false @@ -183,7 +183,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal (eq_located Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 -and branch_expr_eq (_, p1, e1) (_, p2, e2) = +and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && constr_expr_eq e1 e2 @@ -252,22 +252,9 @@ let constr_loc = function | CPrim (loc,_) -> loc | CDelimiters (loc,_,_) -> loc -let cases_pattern_expr_loc = function - | CPatAlias (loc,_,_) -> loc - | CPatCstr (loc,_,_,_) -> loc - | CPatAtom (loc,_) -> loc - | CPatOr (loc,_) -> loc - | CPatNotation (loc,_,_,_) -> loc - | CPatRecord (loc, _) -> loc - | CPatPrim (loc,_) -> loc - | CPatDelimiters (loc,_,_) -> loc - | CPatCast(loc,_,_) -> loc - -let raw_cases_pattern_expr_loc = function - | RCPatAlias (loc,_,_) -> loc - | RCPatCstr (loc,_,_,_) -> loc - | RCPatAtom (loc,_) -> loc - | RCPatOr (loc,_) -> loc +let cases_pattern_expr_loc (l,_) = l + +let raw_cases_pattern_expr_loc (l, _) = l let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) @@ -330,7 +317,7 @@ let expand_binders mkC loc bl c = let c = CCases (loc, LetPatternStyle, None, [(e,None,None)], - [(loc1, [(loc1,[p])], c)]) + [(loc1, ([(loc1,[p])], c))]) in (ni :: env, mkC loc ([id],Default Explicit,ty) c) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 59b8b4e5b9..7a229856e0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -148,11 +148,11 @@ let insert_delimiters e = function let insert_pat_delimiters loc p = function | None -> p - | Some sc -> CPatDelimiters (loc,sc,p) + | Some sc -> Loc.tag ~loc @@ CPatDelimiters (sc,p) let insert_pat_alias loc p = function | Anonymous -> p - | Name id -> CPatAlias (loc,p,id) + | Name id -> Loc.tag ~loc @@ CPatAlias (p,id) (**********************************************************************) (* conversion of references *) @@ -178,7 +178,7 @@ let extern_reference loc vars l = !my_extern_reference loc vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else @@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args = let rec impls_fit l = function |[],t -> Some (List.rev_append l t) |_,[] -> None - |h::t,CPatAtom(_,None)::tt when is_status_implicit h -> impls_fit l (t,tt) + |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt) |h::_,_ when is_status_implicit h -> None |_::t,hh::tt -> impls_fit (hh::l) (t,tt) in let rec aux = function @@ -237,7 +237,7 @@ let expand_curly_brackets loc mknot ntn l = mknot (loc,!ntn',l) let destPrim = function CPrim(_,t) -> Some t | _ -> None -let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None +let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None let make_notation_gen loc ntn mknot mkprim destprim l = if has_curly_brackets ntn @@ -267,15 +267,15 @@ let make_notation loc ntn (terms,termlists,binders as subst) = destPrim terms let make_pat_notation loc ntn (terms,termlists as subst) args = - if not (List.is_empty termlists) then CPatNotation (loc,ntn,subst,args) else + if not (List.is_empty termlists) then (loc, CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),args)) - (fun (loc,p) -> CPatPrim (loc,p)) + (fun (loc,ntn,l) -> Loc.tag ~loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,p) -> Loc.tag ~loc @@ CPatPrim p) destPatPrim terms let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l) + if List.is_empty l then Loc.tag ~loc @@ CPatAtom (Some qid) else Loc.tag ~loc @@ CPatCstr (qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in @@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) + Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | None -> raise No_match | Some key -> let loc = cases_pattern_loc pat in - insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na + insert_pat_alias loc (insert_pat_delimiters loc (Loc.tag ~loc @@ CPatPrim p) key) na with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> match pat with - | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id))) - | PatVar (loc,Anonymous) -> CPatAtom (loc, None) + | PatVar (loc,Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None | PatCstr(loc,cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in let p = @@ -327,24 +327,24 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = | Some c :: q -> match args with | [] -> raise No_match - | CPatAtom(_, None) :: tail -> ip q tail acc + | (_loc, CPatAtom(None)) :: tail -> ip q tail acc (* we don't want to have 'x = _' in our patterns *) | head :: tail -> ip q tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in - CPatRecord(loc, List.rev (ip projs args [])) + Loc.tag ~loc @@ CPatRecord(List.rev (ip projs args [])) with Not_found | No_match | Exit -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, c, None, args) - else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) + then Loc.tag ~loc @@ CPatCstr (c, None, args) + else Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - |Some true_args -> CPatCstr (loc, c, None, true_args) - |None -> CPatCstr (loc, c, Some full_args, []) + | Some true_args -> Loc.tag ~loc @@ CPatCstr (c, None, true_args) + | None -> Loc.tag ~loc @@ CPatCstr (c, Some full_args, []) in insert_pat_alias loc p na and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -401,8 +401,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function let p = apply_notation_to_pattern loc (ConstructRef cstr) (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias loc p na - | PatVar (loc,Anonymous) -> CPatAtom (loc, None) - | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id))) + | PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None + | PatVar (loc,Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id))) with No_match -> extern_notation_pattern allscopes vars t rules @@ -422,7 +422,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), []) + Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -430,7 +430,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = match availability_of_prim_token p sc scopes with | None -> raise No_match | Some key -> - insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key + insert_pat_delimiters Loc.ghost (Loc.tag @@ CPatPrim p) key with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -440,8 +440,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args) - |None -> CPatCstr (Loc.ghost, c, Some args, []) + |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args) + |None -> Loc.tag @@ CPatCstr (c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -868,7 +868,7 @@ and extern_local_binder scopes vars = function (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = - (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], + Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf3..6bf6772c61 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | CPatNotation (_,"{ _ }",([a],[]),[]) :: l -> + | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> @@ -430,17 +430,16 @@ let intern_assumption intern lvar env nal bk ty = let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in env, b -let rec free_vars_of_pat il = - function - | CPatCstr (loc, c, l1, l2) -> +let rec free_vars_of_pat il (loc, pt) = match pt with + | CPatCstr (c, l1, l2) -> let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in List.fold_left free_vars_of_pat il l2 - | CPatAtom (loc, ro) -> + | CPatAtom ro -> begin match ro with | Some (Ident (loc, i)) -> (loc, i) :: il | Some _ | None -> il end - | CPatNotation (loc, n, l1, l2) -> + | CPatNotation (n, l1, l2) -> let il = List.fold_left free_vars_of_pat il (fst l1) in List.fold_left (List.fold_left free_vars_of_pat) il (snd l1) | _ -> anomaly (str "free_vars_of_pat") @@ -988,10 +987,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 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) + then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(None))::out) else fail (remaining_args (len_pl1+i) il) |imp::q,(hh::tt as l) -> if is_status_implicit imp - then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out) + then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out) else let (b,out) = aux (succ i) (q,tt) in (b,hh::out) in aux 0 (impl_list,pl2) @@ -1194,14 +1193,14 @@ let alias_of als = match als.alias_ids with *) -let rec subst_pat_iterator y t p = match p with - | RCPatAtom (_,id) -> - begin match id with Some x when Id.equal 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) - | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a) - | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl) +let rec subst_pat_iterator y t (loc, p) = match p with + | RCPatAtom id -> + begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end + | RCPatCstr (id,l1,l2) -> + Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1, + List.map (subst_pat_iterator y t) l2) + | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a) + | RCPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl) let drop_notations_pattern looked_for = (* At toplevel, Constructors and Inductives are accepted, in recursive calls @@ -1250,46 +1249,46 @@ let drop_notations_pattern looked_for = let (_,argscs) = find_remaining_scopes [] pats g in Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats) with Not_found -> None - and in_pat top scopes = function - | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id) - | CPatRecord (loc, l) -> + and in_pat top scopes (loc, pt) = match pt with + | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id) + | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in + sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in begin match sorted_fields with - | None -> RCPatAtom (loc, None) + | None -> Loc.tag ~loc @@ RCPatAtom None | Some (n, head, pl) -> let pl = if !asymmetric_patterns then pl else - let pars = List.make n (CPatAtom (loc, None)) in + let pars = List.make n (loc, CPatAtom None) in List.rev_append pars pl in match drop_syndef top scopes head pl with - |Some (a,b,c) -> RCPatCstr(loc, a, b, c) + |Some (a,b,c) -> (loc, RCPatCstr(a, b, c)) |None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, head, None, pl) -> + | CPatCstr (head, None, pl) -> begin match drop_syndef top scopes head pl with - | Some (a,b,c) -> RCPatCstr(loc, a, b, c) + | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, Some expl_pl, pl) -> + | CPatCstr (r, Some expl_pl, pl) -> let g = try locate (snd (qualid_of_reference r)) with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) - RCPatCstr (loc, g, List.map (in_pat false scopes) pl, []) + Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) else (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in - RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) - | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) + Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) + | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[]) when Bigint.is_strictly_pos p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes) - | CPatNotation (_,"( _ )",([a],[]),[]) -> + | CPatNotation ("( _ )",([a],[]),[]) -> in_pat top scopes a - | CPatNotation (loc, ntn, fullargs,extrargs) -> + | CPatNotation (ntn, fullargs,extrargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in let ((ids',c),df) = Notation.interp_notation loc ntn scopes in let (ids',idsl',_) = split_by_type ids' in @@ -1297,18 +1296,17 @@ let drop_notations_pattern looked_for = let substlist = make_subst idsl' argsl in let subst = make_subst ids' args in in_not top loc scopes (subst,substlist) extrargs c - | CPatDelimiters (loc, key, e) -> + | CPatDelimiters (key, e) -> in_pat top (None,find_delimiters_scope loc key::snd scopes) e - | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes) - | CPatAtom (loc, Some id) -> + | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes) + | CPatAtom Some id -> begin match drop_syndef top scopes id [] with - |Some (a,b,c) -> RCPatCstr (loc, a, b, c) - |None -> RCPatAtom (loc, Some (find_pattern_variable id)) + | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c) + | None -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id)) end - | CPatAtom (loc,None) -> RCPatAtom (loc,None) - | CPatOr (loc, pl) -> - RCPatOr (loc,List.map (in_pat top scopes) pl) + | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None + | CPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl) | CPatCast _ -> assert false and in_pat_sc scopes x = in_pat false (x,snd scopes) @@ -1322,17 +1320,17 @@ let drop_notations_pattern looked_for = let (a,(scopt,subscopes)) = Id.Map.find id subst in in_pat top (scopt,subscopes@snd scopes) a with Not_found -> - if Id.equal id ldots_var then RCPatAtom (loc,Some id) else + if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id) end | NRef g -> ensure_kind top loc g; let (_,argscs) = find_remaining_scopes [] args g in - RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args) + Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - RCPatCstr (loc, g, + Loc.tag ~loc @@ RCPatCstr (g, List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @ List.map (in_pat false scopes) args, []) | NList (x,y,iter,terminator,lassoc) -> @@ -1351,7 +1349,7 @@ let drop_notations_pattern looked_for = anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NHole _ -> let () = assert (List.is_empty args) in - RCPatAtom (loc, None) + Loc.tag ~loc @@ RCPatAtom None | t -> error_invalid_pattern_notation ~loc () in in_pat true @@ -1363,10 +1361,10 @@ let rec intern_pat genv aliases pat = (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in match pat with - | RCPatAlias (loc, p, id) -> + | loc, RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in intern_pat genv aliases' p - | RCPatCstr (loc, head, expl_pl, pl) -> + | loc, RCPatCstr (head, expl_pl, pl) -> if !asymmetric_patterns then 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 @@ -1378,13 +1376,13 @@ let rec intern_pat genv aliases pat = let with_letin, pl2 = add_implicits_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@pl2) - | RCPatAtom (loc, Some id) -> + | loc, RCPatAtom (Some id) -> let aliases = merge_aliases aliases id in (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)]) - | RCPatAtom (loc, None) -> + | loc, RCPatAtom (None) -> let { alias_ids = ids; alias_map = asubst; } = aliases in (ids, [asubst, PatVar (loc, alias_of aliases)]) - | RCPatOr (loc, pl) -> + | loc, RCPatOr pl -> assert (not (List.is_empty pl)); let pl' = List.map (intern_pat genv aliases) pl in let (idsl,pl') = List.split pl' in @@ -1402,21 +1400,21 @@ let rec intern_pat genv aliases pat = of lambdas in the encoding of match in constr. We put this check here and not in the parser because it would require to duplicate the levels of the [pattern] rule. *) -let rec check_no_patcast = function - | CPatCast (loc,_,_) -> +let rec check_no_patcast (loc, pt) = match pt with + | CPatCast (_,_) -> CErrors.user_err ~loc ~hdr:"check_no_patcast" (Pp.strbrk "Casts are not supported here.") - | CPatDelimiters(_,_,p) - | CPatAlias(_,p,_) -> check_no_patcast p - | CPatCstr(_,_,opl,pl) -> + | CPatDelimiters(_,p) + | CPatAlias(p,_) -> check_no_patcast p + | CPatCstr(_,opl,pl) -> Option.iter (List.iter check_no_patcast) opl; List.iter check_no_patcast pl - | CPatOr(_,pl) -> + | CPatOr pl -> List.iter check_no_patcast pl - | CPatNotation(_,_,subst,pl) -> + | CPatNotation(_,subst,pl) -> check_no_patcast_subst subst; List.iter check_no_patcast pl - | CPatRecord(_,prl) -> + | CPatRecord prl -> List.iter (fun (_,p) -> check_no_patcast p) prl | CPatAtom _ | CPatPrim _ -> () @@ -1441,7 +1439,7 @@ let intern_ind_pattern genv scopes pat = with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc in match no_not with - | RCPatCstr (loc, head, expl_pl, pl) -> + | loc, RCPatCstr (head, expl_pl, pl) -> let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in let with_letin, pl2 = add_implicits_check_ind_length genv loc c (List.length expl_pl) pl in @@ -1784,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (ids,List.flatten mpl') (* Expands a pattern-matching clause [lhs => rhs] *) - and intern_eqn n env (loc,lhs,rhs) = + and intern_eqn n env (loc,(lhs,rhs)) = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; diff --git a/interp/modintern.ml b/interp/modintern.ml index d4ade7058a..166711659f 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -65,17 +65,16 @@ let transl_with_decl env = function let ctx = Evd.evar_context_universe_context ectx in WithDef (fqid,(c,ctx)) -let loc_of_module = function - | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc +let loc_of_module (l, _) = l (* Invariant : the returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let rec interp_module_ast env kind = function +let rec interp_module_ast env kind (loc, m) = match m with | CMident qid -> - let (mp,kind) = lookup_module_or_modtype kind qid in + let (mp,kind) = lookup_module_or_modtype kind (loc,qid) in (MEident mp, kind) - | CMapply (_,me1,me2) -> + | CMapply (me1,me2) -> let me1',kind1 = interp_module_ast env kind me1 in let me2',kind2 = interp_module_ast env ModAny me2 in let mp2 = match me2' with @@ -85,7 +84,7 @@ let rec interp_module_ast env kind = function if kind2 == ModType then error_application_to_module_type (loc_of_module me2); (MEapply (me1',mp2), kind1) - | CMwith (loc,me,decl) -> + | CMwith (me,decl) -> let me,kind = interp_module_ast env kind me in if kind == Module then error_incorrect_with_in_module loc; let decl = transl_with_decl env decl in diff --git a/interp/notation.ml b/interp/notation.ml index 90ac7f7296..04711808b7 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -472,11 +472,11 @@ let interp_prim_token = (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob looked_for = function - | GVar (loc,id) -> RCPatAtom (loc,Some id) - | GHole (loc,_,_,_) -> RCPatAtom (loc,None) - | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[]) + | GVar (loc,id) -> Loc.tag ~loc @@ RCPatAtom (Some id) + | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None) + | GRef (loc,g,_) -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[]) | GApp (loc,GRef (_,g,_),l) -> - looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[]) + looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[]) | _ -> raise Not_found let interp_prim_token_cases_pattern_expr loc looked_for p = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index d3142e7f0c..172caa2caa 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -43,22 +43,22 @@ let is_constructor id = (Nametab.locate_extended (qualid_of_ident id))) with Not_found -> false -let rec cases_pattern_fold_names f a = function - | CPatRecord (_, l) -> +let rec cases_pattern_fold_names f a pt = match snd pt with + | CPatRecord l -> List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l - | CPatAlias (_,pat,id) -> f id a - | CPatOr (_,patl) -> + | CPatAlias (pat,id) -> f id a + | CPatOr (patl) -> List.fold_left (cases_pattern_fold_names f) a patl - | CPatCstr (_,_,patl1,patl2) -> + | CPatCstr (_,patl1,patl2) -> List.fold_left (cases_pattern_fold_names f) (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 - | CPatNotation (_,_,(patl,patll),patl') -> + | CPatNotation (_,(patl,patll),patl') -> List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' - | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a + | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat + | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a | CPatPrim _ | CPatAtom _ -> a - | CPatCast (loc,_,_) -> + | CPatCast ((loc,_),_) -> CErrors.user_err ~loc ~hdr:"cases_pattern_fold_names" (Pp.strbrk "Casts are not supported here.") @@ -125,7 +125,7 @@ let fold_constr_expr_with_binders g f n acc = function let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in - List.fold_right (fun (loc,patl,rhs) acc -> + List.fold_right (fun (loc,(patl,rhs)) acc -> let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (loc,nal,(ona,po),b,c) -> @@ -230,9 +230,9 @@ let map_constr_expr_with_binders g f e = function | CPrim _ | CRef _ as x -> x | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> - let bl = List.map (fun (loc,patl,rhs) -> + let bl = List.map (fun (loc,(patl,rhs)) -> let ids = ids_of_pattern_list patl in - (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in + (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in let ids = ids_of_cases_tomatch a in let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) |