diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 627 |
1 files changed, 373 insertions, 254 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fcaee5c939..009894fddb 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -12,23 +14,21 @@ open CErrors open Util open Names open Nameops -open Term open Termops open Libnames open Globnames +open Namegen open Impargs open CAst open Constrexpr open Constrexpr_ops open Notation_ops -open Topconstr open Glob_term open Glob_ops open Pattern open Nametab open Notation open Detyping -open Misctypes open Decl_kinds module NamedDecl = Context.Named.Declaration @@ -101,7 +101,7 @@ let _show_inactive_notations () = IRuleSet.iter (function | NotationRule (scopt, ntn) -> - Feedback.msg_notice (str ntn ++ show_scope scopt) + Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn))) !inactive_notations_table @@ -113,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 @@ -131,7 +131,7 @@ 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 -> @@ -185,18 +185,8 @@ let with_universes f = Flags.with_option print_universes f let with_meta_as_hole f = Flags.with_option print_meta_as_hole f let without_symbols f = Flags.with_option print_no_symbol f -(* XXX: Where to put this in the library? Util maybe? *) -let protect_ref r nf f x = - let old_ref = !r in - r := nf !r; - try let res = f x in r := old_ref; res - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - r := old_ref; - Exninfo.iraise reraise - let without_specific_symbols l = - protect_ref inactive_notations_table + Flags.with_modified_ref inactive_notations_table (fun tbl -> IRuleSet.(union (of_list l) tbl)) (**********************************************************************) @@ -224,7 +214,7 @@ let is_record indsp = let encode_record r = let indsp = global_inductive r in if not (is_record indsp) then - user_err ?loc:(loc_of_reference r) ~hdr:"encode_record" + user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); indsp @@ -268,7 +258,15 @@ let insert_pat_delimiters ?loc p = function let insert_pat_alias ?loc p = function | Anonymous -> p - | Name id -> CAst.make ?loc @@ CPatAlias (p,id) + | 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 *) @@ -280,14 +278,14 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r) + shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference let set_extern_reference f = my_extern_reference := f let get_extern_reference () = !my_extern_reference -let extern_reference ?loc vars l = !my_extern_reference ?loc vars l +let extern_reference ?loc vars l = !my_extern_reference vars l (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -298,7 +296,7 @@ let add_patt_for_params ind l = let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -320,38 +318,6 @@ let drop_implicits_in_patt cst nb_expl args = let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in impls_fit [] (imps,args) -let has_curly_brackets ntn = - String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 || - String.is_sub " { _ }" ntn (String.length ntn - 6) || - String.string_contains ~where:ntn ~what:" { _ } ") - -let rec wildcards ntn n = - 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 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 - let rec expand_ntn i = - function - | [] -> [] - | a::l -> - let a' = - let p = List.nth (wildcards !ntn' 0) i - 2 in - if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p - then begin - ntn' := - String.sub !ntn' 0 p ^ "_" ^ - String.sub !ntn' (p+5) (String.length !ntn' -p-5); - mknot (loc,"{ _ }",[a]) end - else a in - a' :: expand_ntn (i+1) l in - let l = expand_ntn 0 l in - (* side effect *) - mknot (loc,!ntn',l) - let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None @@ -366,36 +332,35 @@ let is_zero s = Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1)) in aux 0 -let make_notation_gen loc ntn mknot mkprim destprim l = - if has_curly_brackets ntn - then expand_curly_brackets loc mknot ntn l - else match ntn,List.map destprim l with +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) -> - mknot (loc,ntn,([mknot (loc,"( _ )",l)])) + assert (bl=[]); + 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) + | _ -> mknot (loc,ntn,l,bl) -let make_notation loc ntn (terms,termlists,binders as subst) = - if not (List.is_empty termlists) || not (List.is_empty binders) then +let make_notation loc ntn (terms,termlists,binders,binderlists as subst) = + if not (List.is_empty termlists) || not (List.is_empty binderlists) then CAst.make ?loc @@ CNotation (ntn,subst) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[]))) + (fun (loc,ntn,l,bl) -> CAst.make ?loc @@ CNotation (ntn,(l,[],bl,[]))) (fun (loc,p) -> CAst.make ?loc @@ CPrim p) - destPrim terms + destPrim terms binders let make_pat_notation ?loc ntn (terms,termlists as subst) args = if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else make_notation_gen loc ntn - (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) + (fun (loc,ntn,l,_) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args)) (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p) - destPatPrim terms + destPatPrim terms [] let mkPat ?loc qid l = CAst.make ?loc @@ (* Normally irrelevant test with v8 syntax, but let's do it anyway *) @@ -411,26 +376,38 @@ let pattern_printable_in_both_syntax (ind,_ as c) = ) impl_st (* 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 - (uninterp_cases_pattern_notations pat) + extern_notation_pattern allscopes vars pat + (uninterp_cases_pattern_notations pat) with No_match -> - CAst.map_with_loc (fun ?loc -> function - | PatVar (Name id) -> CPatAtom (Some (Ident (loc,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; @@ -445,7 +422,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (* we don't want to have 'x := _' in our patterns *) acc | Some c, _ -> - ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) + ((extern_reference ?loc Id.Set.empty (ConstRef c), pat) :: acc) | _ -> raise No_match in ip q tail acc | _ -> assert false @@ -453,8 +430,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = 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 + let c = extern_reference Id.Set.empty (ConstructRef cstrsp) in + if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -463,46 +440,53 @@ 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 - let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if !asymmetric_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 |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 = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in + 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 !Topconstr.asymmetric_patterns then l2 + let l2' = if !asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args @@ -510,19 +494,20 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) 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 +and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in - match t.v with - | PatCstr (cstr,_,na) -> + match DAst.get t with + | 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 vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None - | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id))) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -536,35 +521,38 @@ 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_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 -> - insert_pat_delimiters (CAst.make @@ CPatPrim p) key + insert_pat_coercion coercion (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 - (uninterp_ind_pattern_notations 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 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 *) @@ -574,6 +562,10 @@ let occur_name na aty = | Name id -> occur_var_constr_expr id aty | Anonymous -> false +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try @@ -610,7 +602,7 @@ let explicitize inctx impl (cf,f) args = is_significant_implicit (Lazy.force a)) in if visible then - (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail + (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail else tail | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) @@ -624,11 +616,17 @@ let explicitize inctx impl (cf,f) args = let expl () = match ip with | Some i -> - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl + (* Careful: It is possible to have declared implicits ending + before the principal argument *) + let is_impl = + try is_status_implicit (List.nth impl (i-1)) + with Failure _ -> false + in + if is_impl + then raise Expl else let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in let ip = Some (List.length args1) in @@ -668,19 +666,23 @@ 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 List.map map args -let match_coercion_app = function - | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args) +let match_coercion_app c = match DAst.get c with + | GApp (r, args) -> + begin match DAst.get r with + | GRef (r,_) -> Some (c.CAst.loc, r, 0, args) + | _ -> None + end | _ -> None let rec remove_coercions inctx c = @@ -702,25 +704,34 @@ let rec remove_coercions inctx c = 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 List.is_empty l then a' else CAst.make ?loc @@ GApp (a',l) + if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l) | _ -> c with Not_found -> c) | _ -> c -let rec flatten_application = function - | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l)) - | a -> a +let rec flatten_application c = match DAst.get c with + | GApp (f, l) -> + begin match DAst.get f with + | GApp(a,l') -> + let loc = c.CAst.loc in + flatten_application (DAst.make ?loc @@ GApp (a,l'@l)) + | _ -> c + end + | a -> c (**********************************************************************) (* 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 @@ -736,10 +747,12 @@ let extern_optimal_prim_token scopes r r' = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) - | (p,bk,Some x, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None) - | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t) + | (p,bk,Some x, t) -> + match DAst.get t with + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) + | _ -> GLocalDef (p,bk,x,Some t) -let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u) +let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -753,7 +766,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 @@ -764,29 +783,44 @@ 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 -> CAst.map_with_loc (fun ?loc -> function - | GRef (ref,us) -> - extern_global (select_stronger_impargs (implicits_of_global ref)) - (extern_reference ?loc 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 -> + + match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> - | GVar id -> CRef (Ident (loc,id),None) + let scopes = (InConstrEntrySomeLevel, snd scopes) in + let c = match c with - | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None) + (* 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,[])) | GApp (f,args) -> - (match f with - | {loc = rloc; v = GRef (ref,us) } -> + (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; @@ -823,7 +857,7 @@ let rec extern inctx scopes vars r = (* we give up since the constructor is not complete *) | (arg, scopes) :: tail -> let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) + ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc) in CRecord (List.rev (ip projs locals args [])) with @@ -831,7 +865,7 @@ let rec extern inctx scopes vars r = let args = extern_args (extern true) vars args in extern_app inctx (select_stronger_impargs (implicits_of_global ref)) - (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args + (Some ref,extern_reference ?loc vars ref) (extern_universes us) args end | _ -> @@ -839,19 +873,17 @@ let rec extern inctx scopes vars r = (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) | GLetIn (na,b,t,c) -> - CLetIn ((loc,na),sub_extern false scopes vars b, + CLetIn (make ?loc na,sub_extern false scopes vars b, Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in - CProdN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_prod scopes (add_vname vars na) na bk t c | GLambda (na,bk,t,c) -> let t = extern_typ scopes vars t in - let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in - CLambdaN ([(Loc.tag na)::idl,Default bk,t],c) + factorize_lambda inctx scopes (add_vname vars na) na bk t c | GCases (sty,rtntypopt,tml,eqns) -> let vars' = @@ -859,40 +891,40 @@ let rec extern inctx scopes vars r = (cases_predicate_names tml) vars in 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, { v = GVar id } -> + let na' = match na, DAst.get tm with + | Anonymous, GVar id -> begin match rtntypopt with | None -> None | Some ntn -> if occur_glob_constr id ntn then - Some (Loc.tag Anonymous) + Some (CAst.make Anonymous) else None end | Anonymous, _ -> None - | Name id, { v = GVar id' } when Id.equal id id' -> None - | Name _, _ -> Some (Loc.tag na) in + | Name id, GVar id' when Id.equal id id' -> None + | Name _, _ -> Some (CAst.make na) in (sub_extern false scopes vars tm, na', - Option.map (fun (loc,(ind,nal)) -> - let args = List.map (fun x -> CAst.make @@ PatVar x) nal in + Option.map (fun {CAst.loc;v=(ind,nal)} -> + let args = List.map (fun x -> DAst.make @@ PatVar x) nal in let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) eqns in + let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map (fun na -> (Loc.tag na)) nal, - (Option.map (fun _ -> (Loc.tag na)) typopt, + CLetTuple (List.map CAst.make nal, + (Option.map (fun _ -> (make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern inctx scopes (List.fold_left add_vname vars nal) b) | GIf (c,(na,typopt),b1,b2) -> CIf (sub_extern false scopes vars c, - (Option.map (fun _ -> (Loc.tag na)) typopt, + (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) @@ -910,13 +942,13 @@ let rec extern inctx scopes vars r = let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) + | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, + ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in - CFix ((loc,idv.(n)),Array.to_list listdecl) + CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> let listdecl = Array.mapi (fun i fi -> @@ -924,10 +956,10 @@ let rec extern inctx scopes vars r = let (_,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 - ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), + ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in - CCoFix ((loc,idv.(n)),Array.to_list listdecl)) + CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) | GSort s -> CSort (extern_glob_sort s) @@ -935,44 +967,86 @@ 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') + | GProj (p, c) -> + let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in + CProj (pr, sub_extern inctx scopes vars c) -and extern_typ (_,scopes) = - extern true (Notation.current_type_scope_name (),scopes) + in insert_coercion coercion (CAst.make ?loc c) -and sub_extern inctx (_,scopes) = extern inctx (None,scopes) +and extern_typ (subentry,(_,scopes)) = + extern true (subentry,(Notation.current_type_scope_name (),scopes)) + +and sub_extern inctx (subentry,(_,scopes)) = extern inctx (subentry,(None,scopes)) and factorize_prod scopes vars na bk aty c = - let c = extern_typ scopes vars c in - match na, c with - | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + let store, get = set_temporary_memory () in + match na, DAst.get c with + | 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)}] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in + let b = extern_typ scopes vars b in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let binder = CLocalPattern (make ?loc:c.loc (p,None)) in + (match b.v with + | CProdN (bl,b) -> CProdN (binder::bl,b) + | _ -> CProdN ([binder],b)) + | _ -> assert false) + | _, _ -> + let c = extern_typ scopes vars c in + match na, c.v with + | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> + CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + | _, CProdN (bl,b) -> + CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) + | _, _ -> + CProdN ([CLocalAssum([make na],Default bk,aty)],c) and factorize_lambda inctx scopes vars na bk aty c = - let c = sub_extern inctx scopes vars c in - match c with - | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) } - when binding_kind_eq bk bk' && constr_expr_eq aty ty - && not (occur_name na ty) (* avoid na in ty escapes scope *) -> - nal,c - | _ -> - [],c + let store, get = set_temporary_memory () in + match na, DAst.get c with + | 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)}] -> + let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in + let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in + let b = sub_extern inctx scopes vars b in + let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in + let binder = CLocalPattern (make ?loc:c.loc (p,None)) in + (match b.v with + | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) + | _ -> CLambdaN ([binder],b)) + | _ -> assert false) + | _, _ -> + let c = sub_extern inctx scopes vars c in + match c.v with + | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) + when binding_kind_eq bk bk' && constr_expr_eq aty ty + && not (occur_name na ty) (* avoid na in ty escapes scope *) -> + CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) + | CLambdaN (bl,b) -> + CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) + | _ -> + CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) and extern_local_binder scopes vars = function [] -> ([],[],[]) - | { v = GLocalDef (na,bk,bd,ty)}::l -> + | b :: l -> + match DAst.get b with + | GLocalDef (na,bk,bd,ty) -> let (assums,ids,l) = extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, - CLocalDef((Loc.tag na), extern false scopes vars bd, + CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) - | { v = GLocalAssum (na,bk,ty)}::l -> + | GLocalAssum (na,bk,ty) -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) @@ -980,35 +1054,35 @@ and extern_local_binder scopes vars = function match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - CLocalAssum((Loc.tag na)::nal,k,ty')::l) + CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) + CLocalAssum([CAst.make na],Default bk,ty) :: l)) - | { v = GLocalPattern ((p,_),_,bk,ty)}::l -> + | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in - let p = extern_cases_pattern vars p in + let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) + (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], - extern inctx scopes vars c) +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 try if is_inactive_rule keyrule then raise No_match; (* Adjusts to the number of arguments expected by the notation *) - let (t,args,argsscopes,argsimpls) = match t.v ,n with + let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with | GApp (f,args), Some n when List.length args >= n -> let args1, args2 = List.chop n args in let subscopes, impls = - match f.v with + match DAst.get f with | GRef (ref,us) -> let subscopes = try List.skipn n (find_arguments_scope ref) @@ -1021,54 +1095,65 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function subscopes,impls | _ -> [], [] in - (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)), + (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), args2, subscopes, impls - | GApp ({ v = GRef (ref,us) } as f, args), None -> + | GApp (f, args), None -> + begin match DAst.get f with + | GRef (ref,us) -> let subscopes = find_arguments_scope ref in let impls = select_impargs_size (List.length args) (implicits_of_global ref) in f, args, subscopes, impls - | GRef (ref,us), Some 0 -> CAst.make @@ GApp (t,[]), [], [], [] + | _ -> t, [], [], [] + end + | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], [] | _, None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) - let terms,termlists,binders = + let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) 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 bll = - List.map (fun (bl,(scopt,scl)) -> - pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) + let bl = + List.map (fun (bl,(subentry,(scopt,scl))) -> + mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl)) binders in - insert_delimiters (make_notation loc ntn (l,ll,bll)) key) + let bll = + List.map (fun (bl,(subentry,(scopt,scl))) -> + pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) + binderlists in + insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) | SynDefRule kn -> 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 (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in + let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in 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 @@ -1082,10 +1167,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 *) @@ -1098,11 +1183,10 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) - let t = EConstr.of_constr t in - let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in + 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 @@ -1111,29 +1195,32 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = - let t = EConstr.of_constr t in - let avoid = if goal_concl_style then ids_of_context env else [] in - let r = Detyping.detype goal_concl_style avoid env sigma t in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in + let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r let extern_sort sigma s = extern_glob_sort (detype_sort sigma s) let extern_closed_glob ?lax goal_concl_style env sigma t = - let avoid = if goal_concl_style then ids_of_context env else [] in + let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in let r = 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 = (* | _ => _ *) - Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.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 + compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c -let rec glob_of_pat env sigma pat = CAst.make @@ match pat with +let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PRef ref -> GRef (ref,None) | PVar id -> GVar id | PEvar (evk,l) -> @@ -1143,7 +1230,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | None -> Id.of_string "__" | Some id -> id in - GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l) + GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1151,33 +1238,39 @@ let rec glob_of_pat env sigma pat = CAst.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 (CAst.make @@ GRef (ConstRef (Projection.constant p),None), - [glob_of_pat env sigma c]) + | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None), + [glob_of_pat avoid env sigma c]) | PApp (f,args) -> - GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) + GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), - List.map (glob_of_pat env sigma) args) + GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), + List.map (glob_of_pat avoid env sigma) args) | PProd (na,t,c) -> - GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c) | PLetIn (na,b,t,c) -> - GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, - glob_of_pat (na::env) sigma c) + let na',avoid' = Namegen.compute_displayed_let_name_in sigma Namegen.RenamingForGoal avoid na c in + let env' = Termops.add_name na' env in + GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t, + glob_of_pat avoid' env' sigma c) | PLambda (na,t,c) -> - GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in + let env' = Termops.add_name na' env in + GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c) | PIf (c,b1,b2) -> - GIf (glob_of_pat env sigma c, (Anonymous,None), - glob_of_pat env sigma b1, glob_of_pat env sigma b2) - | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) -> - let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in - GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b) + 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=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) -> let mat = match bl, info.cip_ind with | [], _ -> [] | _, Some ind -> - let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in + let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in simple_cases_matrix_of_branches ind bl' | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in @@ -1186,21 +1279,47 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> - return_type_of_predicate ind nargs (glob_of_pat env sigma p) + 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 env sigma tm,indnames],mat) - | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) - | PCoFix c -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))).v + 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 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 sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in - let where = Option.map EConstr.of_constr where in - let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in + 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) |