aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml162
1 files changed, 80 insertions, 82 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c2afa097bb..bb66658a37 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,7 +67,10 @@ let print_no_symbol = ref false
(**********************************************************************)
(* Turning notations and scopes on and off for printing *)
-module IRuleSet = InterpRuleSet
+module IRuleSet = Set.Make(struct
+ type t = interp_rule
+ let compare x y = Pervasives.compare x y
+ end)
let inactive_notations_table =
Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty)
@@ -107,13 +110,13 @@ let deactivate_notation nr =
(* shouldn't we check wether it is well defined? *)
inactive_notations_table := IRuleSet.add nr !inactive_notations_table
| NotationRule (scopt, ntn) ->
- if not (exists_notation_interpretation_in_scope scopt ntn) then
- user_err ~hdr:"Notation"
+ match availability_of_notation (scopt, ntn) (scopt, []) with
+ | None -> user_err ~hdr:"Notation"
(pr_notation ntn ++ spc () ++ str "does not exist"
++ (match scopt with
| None -> spc () ++ str "in the empty scope."
| Some _ -> show_scope scopt ++ str "."))
- else
+ | Some _ ->
if IRuleSet.mem nr !inactive_notations_table then
Feedback.msg_warning
(str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
@@ -212,7 +215,7 @@ let encode_record r =
module PrintingRecordRecord =
PrintingInductiveMake (struct
- let encode = encode_record
+ let encode _env = encode_record
let field = "Record"
let title = "Types leading to pretty-printing using record notation: "
let member_message s b =
@@ -224,7 +227,7 @@ module PrintingRecordRecord =
module PrintingRecordConstructor =
PrintingInductiveMake (struct
- let encode = encode_record
+ let encode _env = encode_record
let field = "Constructor"
let title = "Types leading to pretty-printing using constructor form: "
let member_message s b =
@@ -260,11 +263,6 @@ let rec insert_pat_coercion ?loc l c = match l with
| [] -> c
| ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
-let add_lonely keyrule seen =
- match keyrule with
- | NotationRule (None,ntn) -> ntn::seen
- | SynDefRule _ | NotationRule (Some _,_) -> seen
-
(**********************************************************************)
(* conversion of references *)
@@ -289,11 +287,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l
let add_patt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l
let add_cpatt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -318,29 +316,28 @@ let drop_implicits_in_patt cst nb_expl args =
let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
-let is_number s =
- let rec aux i =
- Int.equal (String.length s) i ||
- match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
- in aux 0
-
let is_zero s =
let rec aux i =
Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
in aux 0
+let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
let make_notation_gen loc ntn mknot mkprim destprim l bl =
match snd ntn,List.map destprim l with
(* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
- | "- _", [Some (Numeral (p,true))] when not (is_zero p) ->
+ | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) ->
assert (bl=[]);
mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
- | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
- mkprim (loc, Numeral (x,false))
- | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
- mkprim (loc, Numeral (x,true))
+ | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+ begin match NumTok.of_string x with
+ | Some n -> mkprim (loc, Numeral (SMinus,n))
+ | None -> mknot (loc,ntn,l,bl) end
+ | (InConstrEntrySomeLevel,[Terminal x]), [] ->
+ begin match NumTok.of_string x with
+ | Some n -> mkprim (loc, Numeral (SPlus,n))
+ | None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
@@ -365,7 +362,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
- let nb_params = Inductiveops.inductive_nparams ind in
+ let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
List.exists (fun (_,impls) ->
(List.length impls >= nb_params) &&
let params,args = Util.List.chop nb_params impls in
@@ -389,8 +386,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
with No_match ->
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_pattern allscopes [] vars pat
- (uninterp_cases_pattern_notations scopes pat)
+ extern_notation_pattern allscopes vars pat
+ (uninterp_cases_pattern_notations pat)
with No_match ->
let loc = pat.CAst.loc in
match DAst.get pat with
@@ -443,15 +440,18 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
insert_pat_coercion coercion pat
and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
- (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars =
+ (custom, (tmp_scope, scopes) as allscopes) vars =
function
- | NotationRule (sc,ntn),key,need_delim ->
+ | NotationRule (sc,ntn) ->
begin
match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- let key = if need_delim || List.mem ntn lonely_seen then key else None in
- let scopt = match key with Some _ -> sc | _ -> None in
+ match availability_of_notation (sc,ntn) (tmp_scope,scopes) with
+ (* Uninterpretation is not allowed in current context *)
+ | None -> raise No_match
+ (* Uninterpretation is allowed in current context *)
+ | Some (scopt,key) ->
let scopes' = Option.List.cons scopt scopes in
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -473,8 +473,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(insert_pat_delimiters ?loc
(make_pat_notation ?loc ntn (l,ll) l2') key)
end
- | SynDefRule kn,key,need_delim ->
- assert (key = None && need_delim = false);
+ | SynDefRule kn ->
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
@@ -492,9 +491,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
in
assert (List.is_empty substlist);
insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
-and extern_notation_pattern allscopes lonely_seen vars t = function
+and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
- | (keyrule,pat,n as _rule,key,need_delim)::rules ->
+ | (keyrule,pat,n as _rule)::rules ->
try
if is_inactive_rule keyrule then raise No_match;
let loc = t.loc in
@@ -502,40 +501,35 @@ and extern_notation_pattern allscopes lonely_seen vars t = function
| PatCstr (cstr,args,na) ->
let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
- (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars
- (keyrule,key,need_delim) in
+ (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
insert_pat_alias ?loc p na
| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
| PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
with
- No_match ->
- let lonely_seen = add_lonely keyrule lonely_seen in
- extern_notation_pattern allscopes lonely_seen vars t rules
+ No_match -> extern_notation_pattern allscopes vars t rules
-let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function
+let rec extern_notation_ind_pattern allscopes vars ind args = function
| [] -> raise No_match
- | (keyrule,pat,n as _rule,key,need_delim)::rules ->
+ | (keyrule,pat,n as _rule)::rules ->
try
if is_inactive_rule keyrule then raise No_match;
apply_notation_to_pattern (IndRef ind)
- (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim)
+ (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
with
- No_match ->
- let lonely_seen = add_lonely keyrule lonely_seen in
- extern_notation_ind_pattern allscopes lonely_seen vars ind args rules
+ No_match -> extern_notation_ind_pattern allscopes vars ind args rules
let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
- if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
+ if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
let c = extern_reference vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
else
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_ind_pattern allscopes [] vars ind args
- (uninterp_ind_pattern_notations scopes ind)
+ extern_notation_ind_pattern allscopes vars ind args
+ (uninterp_ind_pattern_notations ind)
with No_match ->
let c = extern_reference vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
@@ -739,6 +733,14 @@ let extern_optimal extern r r' =
| Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
| _ -> raise No_match
+(* Helper function for safe and optimal printing of primitive tokens *)
+(* such as those for Int63 *)
+let extern_prim_token_delimiter_if_required n key_n scope_n scopes =
+ match availability_of_prim_token n scope_n scopes with
+ | Some None -> CPrim n
+ | None -> CDelimiters(key_n, CAst.make (CPrim n))
+ | Some (Some key) -> CDelimiters(key, CAst.make (CPrim n))
+
(**********************************************************************)
(* mapping decl *)
@@ -771,32 +773,32 @@ let extern_ref vars ref us =
let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
-let rec extern inctx (custom,scopes as allscopes) vars r =
+let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_optimal (extern_possible_prim_token allscopes) r r'
+ extern_optimal (extern_possible_prim_token scopes) r r'
with No_match ->
try
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_optimal
- (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r))
+ (fun r -> extern_notation scopes vars r (uninterp_notations r))
r r''
with No_match ->
let loc = r'.CAst.loc in
match DAst.get r' with
- | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us)
+ | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
- | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id)
+ | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
| c ->
- match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
| None -> raise No_match
| Some coercion ->
- let scopes = (InConstrEntrySomeLevel, scopes) in
+ let scopes = (InConstrEntrySomeLevel, snd scopes) in
let c = match c with
(* The remaining cases are only for the constr entry *)
@@ -808,7 +810,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
| GEvar (n,l) ->
- extern_evar n (List.map (on_snd (extern false allscopes vars)) l)
+ extern_evar n (List.map (on_snd (extern false scopes vars)) l)
| GPatVar kind ->
if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
@@ -848,10 +850,10 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| Some c :: q ->
match locs with
| [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].")
- | (_, false) :: locs' ->
+ | { Recordops.pk_true_proj = false } :: locs' ->
(* we don't want to print locals *)
ip q locs' args acc
- | (_, true) :: locs' ->
+ | { Recordops.pk_true_proj = true } :: locs' ->
match args with
| [] -> raise No_match
(* we give up since the constructor is not complete *)
@@ -939,13 +941,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
- let n =
- match fst nv.(i) with
- | None -> None
- | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
- in
- let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ let n =
+ match nv.(i) with
+ | None -> None
+ | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
+ in
+ ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -968,8 +969,11 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
map_cast_type (extern_typ scopes vars) c')
+
| GInt i ->
- CPrim(Numeral (Uint63.to_string i,true))
+ extern_prim_token_delimiter_if_required
+ (Numeral (SPlus, NumTok.int (Uint63.to_string i)))
+ "int63" "int63_scope" (snd scopes)
in insert_coercion coercion (CAst.make ?loc c)
@@ -1069,9 +1073,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
make ?loc (pll,extern inctx scopes vars c)
-and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
+and extern_notation (custom,scopes as allscopes) vars t = function
| [] -> raise No_match
- | (keyrule,pat,n as _rule,key,need_delim)::rules ->
+ | (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
try
if is_inactive_rule keyrule then raise No_match;
@@ -1119,8 +1123,11 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
(match availability_of_entry_coercion custom (fst ntn) with
| None -> raise No_match
| Some coercion ->
- let key = if need_delim || List.mem ntn lonely_seen then key else None in
- let scopt = match key with Some _ -> sc | None -> None in
+ match availability_of_notation (sc,ntn) scopes with
+ (* Uninterpretation is not allowed in current context *)
+ | None -> raise No_match
+ (* Uninterpretation is allowed in current context *)
+ | Some (scopt,key) ->
let scopes' = Option.List.cons scopt (snd scopes) in
let l =
List.map (fun (c,(subentry,(scopt,scl))) ->
@@ -1156,16 +1163,7 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
let args = extern_args (extern true) vars args in
CAst.make ?loc @@ explicitize false argsimpls (None,e) args
with
- No_match ->
- let lonely_seen = add_lonely keyrule lonely_seen in
- extern_notation allscopes lonely_seen vars t rules
-
-and extern_recursion_order scopes vars = function
- GStructRec -> CStructRec
- | GWfRec c -> CWfRec (extern true scopes vars c)
- | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
- Option.map (extern true scopes vars) r)
-
+ No_match -> extern_notation allscopes vars t rules
let extern_glob_constr vars c =
extern false (InConstrEntrySomeLevel,(None,[])) vars c
@@ -1295,7 +1293,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
let v = Array.map3
(fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
bl tl ln in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:30:46 +0000