aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml104
1 files changed, 55 insertions, 49 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7eda89f4e..d7345b701 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -15,6 +15,7 @@ open CAst
open Names
open Nameops
open Namegen
+open Constr
open Libnames
open Globnames
open Impargs
@@ -393,7 +394,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
env fvs in
let bl = List.map
CAst.(map (fun id ->
- (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -430,7 +431,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
| GLocalAssum (na,bk,t) -> (na,bk,None,t)
| GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
| GLocalDef (na,bk,c,None) ->
- let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+ let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in
(na,bk,Some c,t)
| GLocalPattern (_,_,_,_) ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
@@ -471,7 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
let tyc =
match ty with
| Some ty -> ty
- | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+ | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
in
let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
let bk = Default Explicit in
@@ -501,11 +502,11 @@ let intern_generalization intern env ntnvars loc bk ak c =
if pi then
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
- GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
else
(fun {loc=loc';v=id} acc ->
DAst.make ?loc:(Loc.merge_opt loc' loc) @@
- GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
in
List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
@@ -525,7 +526,7 @@ let rec expand_binders ?loc mk bl c =
let tm = DAst.make ?loc (GVar id) in
(* Distribute the disjunctive patterns over the shared right-hand side *)
let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in
- let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
+ let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
(**********************************************************************)
@@ -563,7 +564,7 @@ let term_of_name = function
| Name id -> DAst.make (GVar id)
| Anonymous ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
- DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+ DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None))
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
| Anonymous -> (renaming,env), None, Anonymous
@@ -605,7 +606,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id'
type binder_action =
-| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
+| AddLetIn of lname * constr_expr * constr_expr option
| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -625,7 +626,7 @@ let terms_of_binders bl =
| PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
| PatCstr (c,l,_) ->
let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in
- let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+ let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables l = match l with
@@ -819,11 +820,11 @@ let split_by_type ids subst =
| NtnTypeConstr ->
let terms,terms' = bind id scl terms terms' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
+ | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
@@ -980,25 +981,28 @@ let intern_reference ref =
in
Smartlocate.global_of_extended_global r
-let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
match info with
- | Misctypes.UAnonymous -> None
- | Misctypes.UUnknown -> None
- | Misctypes.UNamed id -> Some (id, 0)
+ | UAnonymous -> None
+ | UUnknown -> None
+ | UNamed id -> Some (id, 0)
-let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
- | Misctypes.GProp -> Misctypes.GProp
- | Misctypes.GSet -> Misctypes.GSet
- | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+ | GProp -> GProp
+ | GSet -> GSet
+ | GType info -> GType [sort_info_of_level_info info]
(* Is it a global reference or a syntactic definition? *)
-let intern_qualid qid intern env ntnvars us args =
+let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
let loc = qid.loc in
match intern_extended_global_of_qualid qid with
+ | TrueGlobal (VarRef _) when no_secvar ->
+ (* Rule out section vars since these should have been found by intern_var *)
+ raise Not_found
| TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
| SynDef sp ->
- let (ids,c) = Syntax_def.search_syntactic_definition sp in
+ let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments ?loc;
let args1,args2 = List.chop nids args in
@@ -1024,7 +1028,7 @@ let intern_qualid qid intern env ntnvars us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
- | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
| Some [_old_level], GSort _new_sort ->
(* TODO: add old_level and new_sort to the error message *)
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
@@ -1032,13 +1036,6 @@ let intern_qualid qid intern env ntnvars us args =
in
c, projapp, args2
-(* Rule out section vars since these should have been found by intern_var *)
-let intern_non_secvar_qualid qid intern env ntnvars us args =
- let c, _, _ as r = intern_qualid qid intern env ntnvars us args in
- match DAst.get c with
- | GRef (VarRef _, _) -> raise Not_found
- | _ -> r
-
let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
function
| {loc; v=Qualid qid} ->
@@ -1054,7 +1051,7 @@ function
with Not_found ->
let qid = make ?loc @@ qualid_of_ident id in
try
- let r, projapp, args2 = intern_non_secvar_qualid qid intern env ntnvars us args in
+ let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
with Not_found ->
@@ -1076,11 +1073,11 @@ let interp_reference vars r =
(** Private internalization patterns *)
type 'a raw_cases_pattern_expr_r =
- | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
- | RCPatCstr of Globnames.global_reference
+ | RCPatAlias of 'a raw_cases_pattern_expr * lname
+ | RCPatCstr of GlobRef.t
* 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
- | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+ | RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
@@ -1140,9 +1137,18 @@ let check_number_of_pattern loc n l =
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 (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then
- user_err ?loc (str
- "The components of this disjunctive pattern must bind the same variables.")
+ let eq_id {v=id} {v=id'} = Id.equal id id' in
+ (* Collect remaining patterns which do not have the same variables as the first pattern *)
+ let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in
+ match idsl with
+ | ids'::_ ->
+ (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *)
+ let ids'' = List.subtract eq_id ids ids' in
+ let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in
+ user_err ?loc
+ (strbrk "The components of this disjunctive pattern must bind the same variables (" ++
+ Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).")
+ | [] -> ()
(** Use only when params were NOT asked to the user.
@return if letin are included *)
@@ -1314,7 +1320,7 @@ let sort_fields ~complete loc fields completer =
| [] -> (idx, acc_first_idx, acc)
| (Some field_glob_id) :: projs ->
let field_glob_ref = ConstRef field_glob_id in
- let first_field = eq_gr field_glob_ref first_field_glob_ref in
+ let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
begin match proj_kinds with
| [] -> anomaly (Pp.str "Number of projections mismatch.")
| (_, regular) :: proj_kinds ->
@@ -1352,7 +1358,7 @@ let sort_fields ~complete loc fields completer =
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
- let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+ let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
try CList.extract_first the_proj remaining_projs
with Not_found ->
user_err ?loc
@@ -1379,7 +1385,7 @@ let sort_fields ~complete loc fields completer =
(** {6 Manage multiple aliases} *)
type alias = {
- alias_ids : Misctypes.lident list;
+ alias_ids : lident list;
alias_map : Id.t Id.Map.t;
}
@@ -1719,15 +1725,15 @@ let get_implicit_name n imps =
let set_hole_implicit i b c =
let loc = c.CAst.loc in
match DAst.get c with
- | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
| GApp (r, _) ->
let loc = r.CAst.loc in
begin match DAst.get r with
| GRef (r, _) ->
- Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
| _ -> anomaly (Pp.str "Only refs have implicits.")
end
- | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+ | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None)
| _ -> anomaly (Pp.str "Only refs have implicits.")
let exists_implicit_name id =
@@ -1913,13 +1919,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let fields =
sort_fields ~complete:true loc fs
(fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
- Misctypes.IntroAnonymous, None))
+ IntroAnonymous, None))
in
begin
match fields with
| None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
| Some (n, constrname, args) ->
- let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+ let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
intern env app
end
@@ -1959,13 +1965,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let main_sub_eqn = CAst.make @@
([],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env')
- (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
if List.for_all (irrefutable globalenv) thepats then [] else
[CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
- DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in
- Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+ DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))] (* "=> _" *) in
+ Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
DAst.make ?loc @@
@@ -1995,7 +2001,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| None ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
(match naming with
- | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+ | IntroIdentifier id -> Evar_kinds.NamedHole id
| _ -> Evar_kinds.QuestionMark (st,Anonymous))
| Some k -> k
in
@@ -2040,7 +2046,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GSort s
| CCast (c1, c2) ->
DAst.make ?loc @@
- GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
+ GCast (intern env c1, map_cast_type (intern_type env) c2)
| CProj (pr, c) ->
match intern_reference pr with
| ConstRef p ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 14:13:45 +0000