summaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml285
1 files changed, 181 insertions, 104 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index af44921e..754fb3b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -14,10 +14,10 @@ open CErrors
open Util
open Names
open Nameops
-open Constr
open Termops
open Libnames
open Globnames
+open Namegen
open Impargs
open CAst
open Constrexpr
@@ -29,7 +29,6 @@ open Pattern
open Nametab
open Notation
open Detyping
-open Misctypes
open Decl_kinds
module NamedDecl = Context.Named.Declaration
@@ -102,8 +101,8 @@ let _show_inactive_notations () =
IRuleSet.iter
(function
| NotationRule (scopt, ntn) ->
- Feedback.msg_notice (str ntn ++ show_scope scopt)
- | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+ Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
+ | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
!inactive_notations_table
let deactivate_notation nr =
@@ -114,14 +113,14 @@ let deactivate_notation nr =
| NotationRule (scopt, ntn) ->
match availability_of_notation (scopt, ntn) (scopt, []) with
| None -> user_err ~hdr:"Notation"
- (str ntn ++ spc () ++ str "does not exist"
+ (pr_notation ntn ++ spc () ++ str "does not exist"
++ (match scopt with
| None -> spc () ++ str "in the empty scope."
| Some _ -> show_scope scopt ++ str "."))
| Some _ ->
if IRuleSet.mem nr !inactive_notations_table then
Feedback.msg_warning
- (str "Notation" ++ spc () ++ str ntn ++ spc ()
+ (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ str "is already inactive" ++ show_scope scopt ++ str ".")
else inactive_notations_table := IRuleSet.add nr !inactive_notations_table
@@ -132,12 +131,13 @@ let reactivate_notation nr =
with Not_found ->
match nr with
| NotationRule (scopt, ntn) ->
- Feedback.msg_warning (str "Notation" ++ spc () ++ str ntn ++ spc ()
+ Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc ()
++ str "is already active" ++ show_scope scopt ++
str ".")
| SynDefRule kn ->
+ let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
Feedback.msg_warning
- (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+ (str "Notation" ++ spc () ++ str s
++ spc () ++ str "is already active.")
@@ -261,6 +261,14 @@ let insert_pat_alias ?loc p = function
| Anonymous -> p
| Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
+let rec insert_coercion ?loc l c = match l with
+ | [] -> c
+ | ntn::l -> CAst.make ?loc @@ CNotation (ntn,([insert_coercion ?loc l c],[],[],[]))
+
+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],[]),[])
+
(**********************************************************************)
(* conversion of references *)
@@ -271,7 +279,7 @@ let extern_evar n l = CEvar (n,l)
may be inaccurate *)
let default_extern_reference ?loc vars r =
- make @@ Qualid (shortest_qualid_of_global vars r)
+ shortest_qualid_of_global ?loc vars r
let my_extern_reference = ref default_extern_reference
@@ -326,16 +334,16 @@ let is_zero s =
in aux 0
let make_notation_gen loc ntn mknot mkprim destprim l bl =
- match ntn,List.map destprim l with
+ 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) ->
assert (bl=[]);
- mknot (loc,ntn,([mknot (loc,"( _ )",l,[])]),[])
+ mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
- | [Terminal "-"; Terminal x], [] when is_number x ->
+ | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
mkprim (loc, Numeral (x,false))
- | [Terminal x], [] when is_number x ->
+ | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
mkprim (loc, Numeral (x,true))
| _ -> mknot (loc,ntn,l,bl)
@@ -368,31 +376,39 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
(List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
) impl_st
-let lift f c =
- let loc = c.CAst.loc in
- CAst.make ?loc (f ?loc (DAst.get c))
-
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
+let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
match availability_of_prim_token p sc scopes with
| None -> raise No_match
| Some key ->
let loc = cases_pattern_loc pat in
- insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
+ insert_pat_coercion ?loc coercion
+ (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na)
with No_match ->
try
if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_pattern scopes vars pat
+ extern_notation_pattern allscopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
- lift (fun ?loc -> function
- | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id))
- | PatVar (Anonymous) -> CPatAtom None
+ let loc = pat.CAst.loc in
+ match DAst.get pat with
+ | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+ | pat ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ let allscopes = (InConstrEntrySomeLevel,scopes) in
+ let pat = match pat with
+ | PatVar (Name id) -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+ | PatVar (Anonymous) -> CAst.make ?loc (CPatAtom None)
| PatCstr(cstrsp,args,na) ->
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
+ let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
let p =
try
if !Flags.raw_print then raise Exit;
@@ -425,26 +441,32 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
| Some true_args -> CPatCstr (c, None, true_args)
| None -> CPatCstr (c, Some full_args, [])
- in (insert_pat_alias ?loc (CAst.make ?loc p) na).v
- ) pat
+ in
+ insert_pat_alias ?loc (CAst.make ?loc p) na
+ in
+ insert_pat_coercion coercion pat
+
and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
- (tmp_scope, scopes as allscopes) vars =
+ (custom, (tmp_scope, scopes) as allscopes) vars =
function
| NotationRule (sc,ntn) ->
begin
- match availability_of_notation (sc,ntn) allscopes with
+ match availability_of_entry_coercion custom (fst ntn) with
+ | None -> raise No_match
+ | Some coercion ->
+ 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,(scopt,scl)) ->
- extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars c)
subst in
let ll =
- List.map (fun (c,(scopt,scl)) ->
- let subscope = (scopt,scl@scopes') in
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ let subscope = (subentry,(scopt,scl@scopes')) in
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
@@ -454,14 +476,18 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|Some true_args -> true_args
|None -> raise No_match
in
- insert_pat_delimiters ?loc
- (make_pat_notation ?loc ntn (l,ll) l2') key
+ insert_pat_coercion coercion
+ (insert_pat_delimiters ?loc
+ (make_pat_notation ?loc ntn (l,ll) l2') key)
end
| SynDefRule kn ->
- let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
+ let qid = shortest_qualid_of_syndef ?loc vars kn in
let l1 =
- List.rev_map (fun (c,(scopt,scl)) ->
- extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
+ List.rev_map (fun (c,(subentry,(scopt,scl))) ->
+ extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
subst in
let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
let l2' = if !asymmetric_patterns then l2
@@ -471,8 +497,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat ?loc qid (List.rev_append l1 l2')
-and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
+ insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
+and extern_notation_pattern allscopes vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
@@ -485,7 +511,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
(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 (make ?loc @@ Ident id))
+ | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
with
No_match -> extern_notation_pattern allscopes vars t rules
@@ -499,35 +525,27 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
with
No_match -> extern_notation_ind_pattern allscopes vars ind args rules
-let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
+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
let c = extern_reference vars (IndRef ind) in
- let args = List.map (extern_cases_pattern_in_scope scopes vars) args 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;
- let (sc,p) = uninterp_prim_token_ind_pattern ind args in
- match availability_of_prim_token p sc scopes with
- | None -> raise No_match
- | Some key ->
- insert_pat_delimiters (CAst.make @@ CPatPrim p) key
- with No_match ->
- try
- if !Flags.raw_print || !print_no_symbol then raise No_match;
- extern_notation_ind_pattern scopes vars ind args
+ 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 scopes vars) args in
+ let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
match drop_implicits_in_patt (IndRef ind) 0 args with
|Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
|None -> CAst.make @@ CPatCstr (c, Some args, [])
let extern_cases_pattern vars p =
- extern_cases_pattern_in_scope (None,[]) vars p
+ extern_cases_pattern_in_scope (InConstrEntrySomeLevel,(None,[])) vars p
(**********************************************************************)
(* Externalising applications *)
@@ -641,12 +659,12 @@ let extern_app inctx impl (cf,f) us args =
else
explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
-let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
+let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with
| [], _ -> []
| a :: args, scopt :: subscopes ->
- (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes
+ (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all
| a :: args, [] ->
- (a, (None, scopes)) :: fill_arg_scopes args [] scopes
+ (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all
let extern_args extern env args =
let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -698,12 +716,15 @@ let rec flatten_application c = match DAst.get c with
(* mapping glob_constr to numerals (in presence of coercions, choose the *)
(* one with no delimiter if possible) *)
-let extern_possible_prim_token scopes r =
+let extern_possible_prim_token (custom,scopes) r =
try
let (sc,n) = uninterp_prim_token r in
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
match availability_of_prim_token n sc scopes with
| None -> None
- | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+ | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key))
with No_match ->
None
@@ -721,7 +742,7 @@ let extended_glob_local_binder_of_decl loc = function
| (p,bk,None,t) -> GLocalAssum (p,bk,t)
| (p,bk,Some x, t) ->
match DAst.get t with
- | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
+ | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
| _ -> GLocalDef (p,bk,x,Some t)
let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
@@ -738,7 +759,13 @@ let extern_glob_sort = function
let extern_universes = function
| Some _ as l when !print_universes -> l
| _ -> None
-
+
+let extern_ref vars ref us =
+ extern_global (select_stronger_impargs (implicits_of_global ref))
+ (extern_reference vars ref) (extern_universes us)
+
+let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
+
let rec extern inctx scopes vars r =
let r' = remove_coercions inctx r in
try
@@ -749,20 +776,35 @@ let rec extern inctx scopes vars r =
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation scopes vars r'' (uninterp_notations r'')
- with No_match -> lift (fun ?loc -> function
- | GRef (ref,us) ->
- extern_global (select_stronger_impargs (implicits_of_global ref))
- (extern_reference vars ref) (extern_universes us)
+ with No_match ->
+ let loc = r'.CAst.loc in
+ match DAst.get r' with
+ | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
+
+ | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+
+ | c ->
- | GVar id -> CRef (make ?loc @@ Ident id,None)
+ match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
- | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
+ let scopes = (InConstrEntrySomeLevel, snd scopes) in
+ let c = match c with
+
+ (* The remaining cases are only for the constr entry *)
+
+ | GRef (ref,us) -> extern_ref vars ref us
+
+ | GVar id -> extern_var ?loc id
+
+ | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
| GEvar (n,l) ->
extern_evar n (List.map (on_snd (extern false scopes vars)) l)
| GPatVar kind ->
- if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
+ if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
(match kind with
| Evar_kinds.SecondOrderPatVar n -> CPatVar n
| Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
@@ -771,7 +813,7 @@ let rec extern inctx scopes vars r =
(match DAst.get f with
| GRef (ref,us) ->
let subscopes = find_arguments_scope ref in
- let args = fill_arg_scopes args subscopes (snd scopes) in
+ let args = fill_arg_scopes args subscopes scopes in
begin
try
if !Flags.raw_print then raise Exit;
@@ -918,18 +960,19 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
- Miscops.map_cast_type (extern_typ scopes vars) c')
- ) r'
+ map_cast_type (extern_typ scopes vars) c')
+
+ in insert_coercion coercion (CAst.make ?loc c)
-and extern_typ (_,scopes) =
- extern true (Notation.current_type_scope_name (),scopes)
+and extern_typ (subentry,(_,scopes)) =
+ extern true (subentry,(Notation.current_type_scope_name (),scopes))
-and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
+and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes))
and factorize_prod scopes vars na bk aty c =
let store, get = set_temporary_memory () in
match na, DAst.get c with
- | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+ | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -957,7 +1000,7 @@ and factorize_prod scopes vars na bk aty c =
and factorize_lambda inctx scopes vars na bk aty c =
let store, get = set_temporary_memory () in
match na, DAst.get c with
- | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
+ | Name id, GCases (Constr.LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b)}] ->
@@ -1017,7 +1060,7 @@ 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 (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation (custom,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
let loc = Glob_ops.loc_of_glob_constr t in
@@ -1064,40 +1107,46 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
let e =
match keyrule with
| NotationRule (sc,ntn) ->
- (match availability_of_notation (sc,ntn) allscopes with
+ (match availability_of_entry_coercion custom (fst ntn) with
+ | None -> raise No_match
+ | Some coercion ->
+ 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 scopes in
+ let scopes' = Option.List.cons scopt (snd scopes) in
let l =
- List.map (fun (c,(scopt,scl)) ->
+ List.map (fun (c,(subentry,(scopt,scl))) ->
extern (* assuming no overloading: *) true
- (scopt,scl@scopes') vars c)
+ (subentry,(scopt,scl@scopes')) vars c)
terms in
let ll =
- List.map (fun (c,(scopt,scl)) ->
- List.map (extern true (scopt,scl@scopes') vars) c)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
termlists in
let bl =
- List.map (fun (bl,(scopt,scl)) ->
- mkCPatOr (List.map (extern_cases_pattern_in_scope (scopt,scl@scopes') vars) bl))
+ List.map (fun (bl,(subentry,(scopt,scl))) ->
+ mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
binders in
let bll =
- List.map (fun (bl,(scopt,scl)) ->
- pi3 (extern_local_binder (scopt,scl@scopes') vars bl))
+ List.map (fun (bl,(subentry,(scopt,scl))) ->
+ pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
binderlists in
- insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)
+ insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key))
| SynDefRule kn ->
+ match availability_of_entry_coercion custom InConstrEntrySomeLevel with
+ | None -> raise No_match
+ | Some coercion ->
let l =
- List.map (fun (c,(scopt,scl)) ->
- extern true (scopt,scl@scopes) vars c, None)
+ List.map (fun (c,(subentry,(scopt,scl))) ->
+ extern true (subentry,(scopt,scl@snd scopes)) vars c, None)
terms in
- let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in
- CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
+ let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in
+ insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in
if List.is_empty args then e
else
- let args = fill_arg_scopes args argsscopes scopes in
+ let args = fill_arg_scopes args argsscopes allscopes in
let args = extern_args (extern true) vars args in
CAst.make ?loc @@ explicitize false argsimpls (None,e) args
with
@@ -1111,10 +1160,10 @@ and extern_recursion_order scopes vars = function
let extern_glob_constr vars c =
- extern false (None,[]) vars c
+ extern false (InConstrEntrySomeLevel,(None,[])) vars c
let extern_glob_type vars c =
- extern_typ (None,[]) vars c
+ extern_typ (InConstrEntrySomeLevel,(None,[])) vars c
(******************************************************************)
(* Main translation function from constr -> constr_expr *)
@@ -1130,7 +1179,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
- extern false (scopt,[]) vars r
+ extern false (InConstrEntrySomeLevel,(scopt,[])) vars r
let extern_constr_in_scope goal_concl_style scope env sigma t =
extern_constr_gen false goal_concl_style (Some scope) env sigma t
@@ -1151,14 +1200,14 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
in
let vars = vars_of_env env in
- extern false (None,[]) vars r
+ extern false (InConstrEntrySomeLevel,(None,[])) vars r
(******************************************************************)
(* Main translation function from pattern -> constr_expr *)
let any_any_branch =
(* | _ => _ *)
- CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+ CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None))
let compute_displayed_name_in_pattern sigma avoid na c =
let open Namegen in
@@ -1182,7 +1231,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
GVar id
- | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
+ | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
[glob_of_pat avoid env sigma c])
@@ -1207,7 +1256,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PIf (c,b1,b2) ->
GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
- | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
+ | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
@@ -1226,16 +1275,44 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
- GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
+ | PFix ((ln,i),(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let n = Array.length tl in
+ 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),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let def_avoid, def_env, lfi =
+ Array.fold_left
+ (fun (avoid, env, l) na ->
+ let id = Namegen.next_name_away na avoid in
+ (Id.Set.add id avoid, Name id :: env, id::l))
+ (avoid, env, []) lna in
+ let ntys = Array.length tl in
+ let v = Array.map2
+ (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t))
+ bl tl in
+ GRec(GCoFix ln,Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
- extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
+ extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl) a in
- pi3 (extern_local_binder (None,[]) vars a)
+ pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:47:30 +0000