From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- interp/constrintern.ml | 905 ++++++++++++++++++++++++++++++------------------- 1 file changed, 561 insertions(+), 344 deletions(-) (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e1ee5486..9abee4d4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: constrintern.ml 11065 2008-06-06 22:39:43Z msozeau $ *) open Pp open Util -open Options +open Flags open Names open Nameops open Libnames @@ -32,6 +32,8 @@ type var_internalisation_data = type implicits_env = (identifier * var_internalisation_data) list type full_implicits_env = identifier list * implicits_env +type raw_binder = (name * binding_kind * rawconstr option * rawconstr) + let interning_grammar = ref false (* Historically for parsing grammar rules, but in fact used only for @@ -42,8 +44,6 @@ let for_grammar f x = interning_grammar := false; a -let variables_bind = ref false - (**********************************************************************) (* Internalisation errors *) @@ -86,7 +86,7 @@ let explain_bad_patterns_number n1 n2 = let explain_bad_explicitation_number n po = match n with - | ExplByPos n -> + | ExplByPos (n,_id) -> let s = match po with | None -> str "a regular argument" | Some p -> int p in @@ -142,15 +142,110 @@ let coqdoc_unfreeze (lt,tn,lp) = token_number := tn; last_pos := lp -let add_glob loc ref = - let sp = Nametab.sp_of_global ref in - let lib_dp = Lib.library_part ref in +open Decl_kinds + +let type_of_logical_kind = function + | IsDefinition def -> + (match def with + | Definition -> "def" + | Coercion -> "coe" + | SubClass -> "subclass" + | CanonicalStructure -> "canonstruc" + | Example -> "ex" + | Fixpoint -> "def" + | CoFixpoint -> "def" + | Scheme -> "scheme" + | StructureComponent -> "proj" + | IdentityCoercion -> "coe" + | Instance -> "inst" + | Method -> "meth") + | IsAssumption a -> + (match a with + | Definitional -> "defax" + | Logical -> "prfax" + | Conjectural -> "prfax") + | IsProof th -> + (match th with + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary -> "thm") + +let type_of_global_ref gr = + if Typeclasses.is_class gr then + "class" + else + match gr with + | ConstRef cst -> + type_of_logical_kind (Decls.constant_kind cst) + | VarRef v -> + "var" ^ type_of_logical_kind (Decls.variable_kind v) + | IndRef ind -> + let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in + if mib.Declarations.mind_record then + if mib.Declarations.mind_finite then "rec" + else "corec" + else if mib.Declarations.mind_finite then "ind" + else "coind" + | ConstructRef _ -> "constr" + +let remove_sections dir = + if is_dirpath_prefix_of dir (Lib.cwd ()) then + (* Not yet (fully) discharged *) + extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + else + (* Theorem/Lemma outside its outer section of definition *) + dir + +let dump_reference loc filepath modpath ident ty = + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (unloc loc)) filepath modpath ident ty) + +let add_glob_gen loc sp lib_dp ty = let mod_dp,id = repr_path sp in - let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in + let mod_dp = remove_sections mod_dp in + let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in let filepath = string_of_dirpath lib_dp in - let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in - dump_string (Printf.sprintf "R%d %s %s\n" (fst (unloc loc)) filepath fullname) + let modpath = string_of_dirpath mod_dp_trunc in + let ident = string_of_id id in + dump_reference loc filepath modpath ident ty +let add_glob loc ref = + let sp = Nametab.sp_of_global ref in + let lib_dp = Lib.library_part ref in + let ty = type_of_global_ref ref in + add_glob_gen loc sp lib_dp ty + +let add_glob loc ref = + if !Flags.dump && loc <> dummy_loc then add_glob loc ref + +let mp_of_kn kn = + let mp,sec,l = repr_kn kn in + MPdot (mp,l) + +let add_glob_kn loc kn = + let sp = Nametab.sp_of_syntactic_definition kn in + let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in + add_glob_gen loc sp lib_dp "syndef" + +let add_glob_kn loc ref = + if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref + +let add_local loc id = () +(* let mod_dp,id = repr_path sp in *) +(* let mod_dp = remove_sections mod_dp in *) +(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *) +(* let filepath = string_of_dirpath lib_dp in *) +(* let modpath = string_of_dirpath mod_dp_trunc in *) +(* let ident = string_of_id id in *) +(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *) +(* (fst (unloc loc)) filepath modpath ident ty) *) + +let dump_binding loc id = () + let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) else snd (unloc (f (List.hd args))) @@ -169,8 +264,8 @@ let dump_notation_location pos ((path,df),sc) = let loc = next (pos >= !last_pos) in last_pos := pos; let path = string_of_dirpath path in - let sc = match sc with Some sc -> " "^sc | None -> "" in - dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc) + let _sc = match sc with Some sc -> " "^sc | None -> "" in + dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -221,18 +316,104 @@ let contract_pat_notation ntn l = (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes +let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes let set_var_scope loc id (_,scopt,scopes) varscopes = let idscopes = List.assoc id varscopes in if !idscopes <> None & - make_current_scope (out_some !idscopes) + make_current_scope (Option.get !idscopes) <> make_current_scope (scopt,scopes) then user_err_loc (loc,"set_var_scope", pr_id id ++ str " already occurs in a different scope") else idscopes := Some (scopt,scopes) +(**********************************************************************) +(* Syntax extensions *) + +let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id = + try + (* Binders bound in the notation are considered first-order objects *) + let _,id' = coerce_to_id (fst (List.assoc id subst)) in + (renaming,(Idset.add id' ids,tmpsc,scopes)), id' + with Not_found -> + (* Binders not bound in the notation do not capture variables *) + (* outside the notation (i.e. in the substitution) *) + let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in + let fvs2 = List.map snd renaming in + let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in + let id' = next_ident_away id fvs in + let renaming' = if id=id' then renaming else (id,id')::renaming in + (renaming',env), id' + +let decode_constrlist_value = function + | CAppExpl (_,_,l) -> l + | _ -> anomaly "Ill-formed list argument of notation" + +let rec subst_iterator y t = function + | RVar (_,id) as x -> if id = y then t else x + | x -> map_rawconstr (subst_iterator y t) x + +let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = + function + | AVar id -> + begin + (* subst remembers the delimiters stack in the interpretation *) + (* of the notations *) + try + let (a,(scopt,subscopes)) = List.assoc id subst in + interp (ids,scopt,subscopes@scopes) a + with Not_found -> + try + RVar (loc,List.assoc id renaming) + with Not_found -> + (* Happens for local notation joint with inductive/fixpoint defs *) + RVar (loc,id) + end + | AList (x,_,iter,terminator,lassoc) -> + (try + (* All elements of the list are in scopes (scopt,subscopes) *) + let (a,(scopt,subscopes)) = List.assoc x subst in + let termin = + subst_aconstr_in_rawconstr loc interp subst + (renaming,(ids,None,scopes)) terminator in + let l = decode_constrlist_value a in + List.fold_right (fun a t -> + subst_iterator ldots_var t + (subst_aconstr_in_rawconstr loc interp + ((x,(a,(scopt,subscopes)))::subst) + (renaming,(ids,None,scopes)) iter)) + (if lassoc then List.rev l else l) termin + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | t -> + rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + (subst_aconstr_in_rawconstr loc interp subst) + (renaming,(ids,None,scopes)) t + +let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = + let ntn,args = contract_notation ntn args in + let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + if !dump then dump_notation_location (ntn_loc loc args ntn) df; + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in + subst_aconstr_in_rawconstr loc intern subst ([],env) c + +let set_type_scope (ids,tmp_scope,scopes) = + (ids,Some Notation.type_scope,scopes) + +let reset_tmp_scope (ids,tmp_scope,scopes) = + (ids,None,scopes) + +let rec it_mkRProd env body = + match env with + (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + | [] -> body + +let rec it_mkRLambda env body = + match env with + (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + | [] -> body + (**********************************************************************) (* Discriminating between bound variables and global references *) @@ -281,52 +462,60 @@ let find_appl_head_data (_,_,_,(_,impls)) = function | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] | x -> x,[],[],[] +let error_not_enough_arguments loc = + user_err_loc (loc,"",str "Abbreviation is not applied enough") + +let check_no_explicitation l = + let l = List.filter (fun (a,b) -> b <> None) l in + if l <> [] then + let loc = fst (Option.get (snd (List.hd l))) in + user_err_loc + (loc,"",str"Unexpected explicitation of the argument of an abbreviation") + (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid = +let intern_qualid loc qid intern env args = try match Nametab.extended_locate qid with | TrueGlobal ref -> - if !dump then add_glob loc ref; - RRef (loc, ref) + add_glob loc ref; + RRef (loc, ref), args | SyntacticDef sp -> - Syntax_def.search_syntactic_definition loc sp + add_glob_kn loc sp; + 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 + check_no_explicitation args1; + let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in + subst_aconstr_in_rawconstr loc intern subst ([],env) c, args2 with Not_found -> error_global_not_found_loc loc qid (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid = - match intern_qualid loc qid with - | RRef (loc, VarRef id) -> error_global_not_found_loc loc qid +let intern_non_secvar_qualid loc qid intern env args = + match intern_qualid loc qid intern env args with + | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r -let intern_inductive r = - let loc,qid = qualid_of_reference r in - try match Nametab.extended_locate qid with - | TrueGlobal (IndRef ind) -> ind, [] - | TrueGlobal _ -> raise Not_found - | SyntacticDef sp -> - (match Syntax_def.search_syntactic_definition loc sp with - | RApp (_,RRef(_,IndRef ind),l) - when List.for_all (function RHole _ -> true | _ -> false) l -> - (ind, List.map (fun _ -> Anonymous) l) - | _ -> raise Not_found) - with Not_found -> - error_global_not_found_loc loc qid - -let intern_reference env lvar = function +let intern_applied_reference intern env lvar args = function | Qualid (loc, qid) -> - find_appl_head_data lvar (intern_qualid loc qid) + let r,args2 = intern_qualid loc qid intern env args in + find_appl_head_data lvar r, args2 | Ident (loc, id) -> - try intern_var env lvar loc id + try intern_var env lvar loc id, args with Not_found -> let qid = make_short_qualid id in - try find_appl_head_data lvar (intern_non_secvar_qualid loc qid) + try + let r,args2 = intern_non_secvar_qualid loc qid intern env args in + find_appl_head_data lvar r, args2 with e -> (* Extra allowance for non globalizing functions *) - if !interning_grammar then RVar (loc,id), [], [], [] + if !interning_grammar then (RVar (loc,id), [], [], []),args else raise e let interp_reference vars r = - let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r + let (r,_,_,_),_ = + intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) + (Idset.empty,None,[]) (vars,[],[],([],[])) [] r in r let apply_scope_env (ids,_,scopes) = function @@ -339,10 +528,16 @@ let rec adjust_scopes env scopes = function let (enva,scopes) = apply_scope_env env scopes in enva :: adjust_scopes env scopes args -let rec simple_adjust_scopes = function - | _,[] -> [] - | [],_::args -> None :: simple_adjust_scopes ([],args) - | sc::scopes,_::args -> sc :: simple_adjust_scopes (scopes,args) +let rec simple_adjust_scopes n = function + | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) [] + | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes + +let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = + let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + let npar = mib.Declarations.mind_nparams in + snd (list_chop (List.length pl1 + npar) + (simple_adjust_scopes (npar + List.length pl2) + (find_arguments_scope (ConstructRef cstr)))) (**********************************************************************) (* Cases *) @@ -368,8 +563,7 @@ let rec has_duplicate = function | x::l -> if List.mem x l then (Some x) else has_duplicate l let loc_of_lhs lhs = - join_loc (cases_pattern_expr_loc (List.hd (List.hd lhs))) - (cases_pattern_expr_loc (list_last (list_last lhs))) + join_loc (fst (List.hd lhs)) (fst (list_last lhs)) let check_linearity lhs ids = match has_duplicate ids with @@ -412,6 +606,16 @@ let message_redundant_alias (id1,id2) = (* Expanding notations *) +let error_invalid_pattern_notation loc = + user_err_loc (loc,"",str "Invalid notation for pattern") + +let chop_aconstr_constructor loc (ind,k) args = + let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in + let params,args = list_chop nparams args in + List.iter (function AHole _ -> () + | _ -> error_invalid_pattern_notation loc) params; + args + let decode_patlist_value = function | CPatCstr (_,_,l) -> l | _ -> anomaly "Ill-formed list argument of notation" @@ -445,13 +649,12 @@ let subst_cases_pattern loc alias intern subst scopes a = end | ARef (ConstructRef c) -> ([],[[], PatCstr (loc,c, [], alias)]) - | AApp (ARef (ConstructRef (ind,_ as c)),args) -> - let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in - let _,args = list_chop nparams args in + | AApp (ARef (ConstructRef cstr),args) -> + let args = chop_aconstr_constructor loc cstr args in let idslpll = List.map (aux Anonymous subst) args in let ids',pll = product_of_cases_patterns [] idslpll in let pl' = List.map (fun (subst,pl) -> - subst,PatCstr (loc,c,pl,alias)) pll in + subst,PatCstr (loc,cstr,pl,alias)) pll in ids', pl' | AList (x,_,iter,terminator,lassoc) -> (try @@ -469,65 +672,57 @@ let subst_cases_pattern loc alias intern subst scopes a = match pl with PatCstr (loc, c, pl, Anonymous) -> (subst, PatCstr (loc, c, pl, alias)) | _ -> x) v with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | t -> user_err_loc (loc,"",str "Invalid notation for pattern") + | t -> error_invalid_pattern_notation loc in aux alias subst a (* Differentiating between constructors and matching variables *) type pattern_qualid_kind = - | ConstrPat of (constructor * cases_pattern list) + | ConstrPat of constructor * (identifier list * + ((identifier * identifier) list * cases_pattern) list) list | VarPat of identifier -let rec patt_of_rawterm loc cstr = - match cstr with - | RRef (_,(ConstructRef c as x)) -> - if !dump then add_glob loc x; - (c,[]) - | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2)) - | RApp (_,RRef(_,(ConstructRef c as x)),pl) -> - if !dump then add_glob loc x; - let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in - let npar = mib.Declarations.mind_nparams in - let (params,args) = - if List.length pl <= npar then (pl,[]) else - list_chop npar pl in - (* All parameters must be _ *) - List.iter - (function RHole _ -> () - | _ -> raise Not_found) params; - let pl' = List.map - (fun c -> - let (c,pl) = patt_of_rawterm loc c in - PatCstr(loc,c,pl,Anonymous)) args in - (c,pl') - | _ -> raise Not_found - -let find_constructor ref = +let find_constructor ref f aliases pats scopes = let (loc,qid) = qualid_of_reference ref in let gref = try extended_locate qid - with Not_found -> - raise (InternalisationError (loc,NotAConstructor ref)) in - match gref with - | SyntacticDef sp -> - let sdef = Syntax_def.search_syntactic_definition loc sp in - patt_of_rawterm loc sdef - | TrueGlobal r -> - let rec unf = function - | ConstRef cst -> - let v = Environ.constant_value (Global.env()) cst in - unf (global_of_constr v) - | ConstructRef c -> - if !dump then add_glob loc r; - c, [] - | _ -> raise Not_found - in unf r + with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in + match gref with + | SyntacticDef sp -> + let (vars,a) = Syntax_def.search_syntactic_definition loc sp in + (match a with + | ARef (ConstructRef cstr) -> + assert (vars=[]); + cstr, [], pats + | AApp (ARef (ConstructRef cstr),args) -> + let args = chop_aconstr_constructor loc cstr args in + let nvars = List.length vars in + if List.length pats < nvars then error_not_enough_arguments loc; + let pats1,pats2 = list_chop nvars pats in + let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in + let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f subst scopes) args in + cstr, idspl1, pats2 + | _ -> raise Not_found) + + | TrueGlobal r -> + let rec unf = function + | ConstRef cst -> + let v = Environ.constant_value (Global.env()) cst in + unf (global_of_constr v) + | ConstructRef cstr -> + add_glob loc r; + cstr, [], pats + | _ -> raise Not_found + in unf r let find_pattern_variable = function | Ident (loc,id) -> id | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x)) -let maybe_constructor ref = - try ConstrPat (find_constructor ref) +let maybe_constructor ref f aliases scopes = + try + let c,idspl1,pl2 = find_constructor ref f aliases [] scopes in + assert (pl2 = []); + ConstrPat (c,idspl1) with (* patt var does not exists globally *) | InternalisationError _ -> VarPat (find_pattern_variable ref) @@ -537,39 +732,37 @@ let maybe_constructor ref = str " is understood as a pattern variable"); VarPat (find_pattern_variable ref) -let mustbe_constructor loc ref = - try find_constructor ref +let mustbe_constructor loc ref f aliases patl scopes = + try find_constructor ref f aliases patl scopes with (Environ.NotEvaluableConst _ | Not_found) -> raise (InternalisationError (loc,NotAConstructor ref)) -let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = - function +let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = + let intern_pat = intern_cases_pattern genv in + match pat with | CPatAlias (loc, p, id) -> let aliases' = merge_aliases aliases id in - intern_cases_pattern genv scopes aliases' tmp_scope p + intern_pat scopes aliases' tmp_scope p | CPatCstr (loc, head, pl) -> - let c,pl0 = mustbe_constructor loc head in - let argscs = - simple_adjust_scopes (find_arguments_scope (ConstructRef c), pl) in - check_constructor_length genv loc c pl0 pl; - let idslpl = - List.map2 (intern_cases_pattern genv scopes ([],[])) argscs pl in - let (ids',pll) = product_of_cases_patterns ids idslpl in + let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in + check_constructor_length genv loc c idslpl1 pl2; + let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in + let idslpl2 = List.map2 (intern_pat scopes ([],[])) argscs2 pl2 in + let (ids',pll) = product_of_cases_patterns ids (idslpl1@idslpl2) in let pl' = List.map (fun (subst,pl) -> - (subst, PatCstr (loc,c,pl0@pl,alias_of aliases))) pll in + (subst, PatCstr (loc,c,pl,alias_of aliases))) pll in ids',pl' | CPatNotation (loc,"- _",[CPatPrim(_,Numeral p)]) when Bigint.is_strictly_pos p -> - let np = Numeral (Bigint.neg p) in - intern_cases_pattern genv scopes aliases tmp_scope (CPatPrim(loc,np)) + intern_pat scopes aliases tmp_scope (CPatPrim(loc,Numeral(Bigint.neg p))) | CPatNotation (_,"( _ )",[a]) -> - intern_cases_pattern genv scopes aliases tmp_scope a + intern_pat scopes aliases tmp_scope a | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in if !dump then dump_notation_location (patntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in - let ids'',pl = subst_cases_pattern loc (alias_of aliases) (intern_cases_pattern genv) subst scopes + let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes c in ids@ids'', pl | CPatPrim (loc, p) -> @@ -579,13 +772,14 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = if !dump then dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> - intern_cases_pattern genv (find_delimiters_scope loc key::scopes) - aliases None e + intern_pat (find_delimiters_scope loc key::scopes) aliases None e | CPatAtom (loc, Some head) -> - (match maybe_constructor head with - | ConstrPat (c,args) -> - check_constructor_length genv loc c [] []; - (ids,[subst, PatCstr (loc,c,args,alias_of aliases)]) + (match maybe_constructor head intern_pat aliases scopes with + | ConstrPat (c,idspl) -> + check_constructor_length genv loc c idspl []; + let (ids',pll) = product_of_cases_patterns ids idspl in + (ids,List.map (fun (subst,pl) -> + (subst, PatCstr (loc,c,pl,alias_of aliases))) pll) | VarPat id -> let ids,subst = merge_aliases aliases id in (ids,[subst, PatVar (loc,alias_of (ids,subst))])) @@ -593,8 +787,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = (ids,[subst, PatVar (loc,alias_of aliases)]) | CPatOr (loc, pl) -> assert (pl <> []); - let pl' = - List.map (intern_cases_pattern genv scopes aliases tmp_scope) pl in + let pl' = List.map (intern_pat scopes aliases tmp_scope) pl in let (idsl,pl') = List.split pl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); @@ -632,6 +825,44 @@ let push_name_env lvar (ids,tmpsc,scopes as env) = function check_hidden_implicit_parameters id lvar; (Idset.add id ids,tmpsc,scopes) +let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function + | Anonymous -> env + | Name id -> + check_hidden_implicit_parameters id lvar; + dump_binding loc id; + (Idset.add id ids,tmpsc,scopes) + +let intern_typeclass_binders intern_type lvar env bl = + List.fold_left + (fun ((ids,ts,sc) as env,bl) ((loc, na), bk, ty) -> + let env = push_loc_name_env lvar env loc na in + let ty = locate_if_isevar loc na (intern_type env ty) in + (env, (na,bk,None,ty)::bl)) + env bl + +let intern_typeclass_binder intern_type lvar (env,bl) na b ty = + let ctx = (na, b, ty) in + let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in + let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in + intern_typeclass_binders intern_type lvar (env,ifvs) bind + +let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function + | LocalRawAssum(nal,bk,ty) -> + (match bk with + | Default k -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = locate_if_isevar loc na (intern_type env ty) in + List.fold_left + (fun ((ids,ts,sc),bl) (_,na) -> + ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl)) + (env,bl) nal + | TypeClass b -> + intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty) + | LocalRawDef((loc,na),def) -> + ((name_fold Idset.add na ids,ts,sc), + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + (**********************************************************************) (* Utilities for application *) @@ -683,7 +914,7 @@ let extract_explicit_arg imps args = user_err_loc (loc,"",str "Argument name " ++ pr_id id ++ str " occurs more than once"); id - | ExplByPos p -> + | ExplByPos (p,_id) -> let id = try let imp = List.nth imps (p-1) in @@ -699,121 +930,54 @@ let extract_explicit_arg imps args = ((id,(loc,a))::eargs,rargs) in aux args -(**********************************************************************) -(* Syntax extensions *) - -let traverse_binder subst (renaming,(ids,tmpsc,scopes as env)) id = - try - (* Binders bound in the notation are considered first-order objects *) - let _,id' = coerce_to_id (fst (List.assoc id subst)) in - (renaming,(Idset.add id' ids,tmpsc,scopes)), id' - with Not_found -> - (* Binders not bound in the notation do not capture variables *) - (* outside the notation (i.e. in the substitution) *) - let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in - let fvs2 = List.map snd renaming in - let fvs = List.flatten (List.map Idset.elements fvs1) @ fvs2 in - let id' = next_ident_away id fvs in - let renaming' = if id=id' then renaming else (id,id')::renaming in - (renaming',env), id' - -let decode_constrlist_value = function - | CAppExpl (_,_,l) -> l - | _ -> anomaly "Ill-formed list argument of notation" - -let rec subst_iterator y t = function - | RVar (_,id) as x -> if id = y then t else x - | x -> map_rawconstr (subst_iterator y t) x - -let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = - function - | AVar id -> - begin - (* subst remembers the delimiters stack in the interpretation *) - (* of the notations *) - try - let (a,(scopt,subscopes)) = List.assoc id subst in - interp (ids,scopt,subscopes@scopes) a - with Not_found -> - try - RVar (loc,List.assoc id renaming) - with Not_found -> - (* Happens for local notation joint with inductive/fixpoint defs *) - RVar (loc,id) - end - | AList (x,_,iter,terminator,lassoc) -> - (try - (* All elements of the list are in scopes (scopt,subscopes) *) - let (a,(scopt,subscopes)) = List.assoc x subst in - let termin = - subst_aconstr_in_rawconstr loc interp subst - (renaming,(ids,None,scopes)) terminator in - let l = decode_constrlist_value a in - List.fold_right (fun a t -> - subst_iterator ldots_var t - (subst_aconstr_in_rawconstr loc interp - ((x,(a,(scopt,subscopes)))::subst) - (renaming,(ids,None,scopes)) iter)) - (if lassoc then List.rev l else l) termin - with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | t -> - rawconstr_of_aconstr_with_binders loc (traverse_binder subst) - (subst_aconstr_in_rawconstr loc interp subst) - (renaming,(ids,None,scopes)) t - -let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = - let ntn,args = contract_notation ntn args in - let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !dump then dump_notation_location (ntn_loc loc args ntn) df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - subst_aconstr_in_rawconstr loc intern subst ([],env) c - -let set_type_scope (ids,tmp_scope,scopes) = - (ids,Some Notation.type_scope,scopes) - -let reset_tmp_scope (ids,tmp_scope,scopes) = - (ids,None,scopes) - (**********************************************************************) (* Main loop *) -let internalise sigma globalenv env allow_soapp lvar c = +let internalise sigma globalenv env allow_patvar lvar c = let rec intern (ids,tmp_scope,scopes as env) = function | CRef ref as x -> - let (c,imp,subscopes,l) = intern_reference env lvar ref in + let (c,imp,subscopes,l),_ = + intern_applied_reference intern env lvar [] ref in (match intern_impargs c env imp subscopes l with | [] -> c | l -> RApp (constr_loc x, c, l)) | CFix (loc, (locid,iddef), dl) -> - let lf = List.map (fun (id,_,_,_,_) -> id) dl in + let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try - (list_index iddef lf) -1 + try list_index0 iddef lf with Not_found -> raise (InternalisationError (locid,UnboundFixName (false,iddef))) in let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg c f = - let before, after = list_chop (succ (out_some n)) bl in - let ((ids',_,_),rafter) = - List.fold_left intern_local_binder (env,[]) after in - let ro = (intern (ids', tmp_scope, scopes) c) in - f ro, List.fold_left intern_local_binder (env,rafter) before + let idx = + match n with + Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl)) + | None -> 0 + in + let before, after = list_chop idx bl in + let ((ids',_,_) as env',rbefore) = + List.fold_left intern_local_binder (env,[]) before in + let ro = + match c with + | None -> RStructRec + | Some c' -> f (intern (ids', tmp_scope, scopes) c') + in + let n' = Option.map (fun _ -> List.length before) n in + n', ro, List.fold_left intern_local_binder (env',rbefore) after in - let ro, ((ids',_,_),rbl) = + let n, ro, ((ids',_,_),rbl) = (match order with - CStructRec -> - RStructRec, - List.fold_left intern_local_binder (env,[]) bl - | CWfRec c -> - intern_ro_arg c (fun r -> RWfRec r) - | CMeasureRec c -> - intern_ro_arg c (fun r -> RMeasureRec r)) - in - let ids'' = List.fold_right Idset.add lf ids' in + | CStructRec -> + intern_ro_arg None (fun _ -> RStructRec) + | CWfRec c -> + intern_ro_arg (Some c) (fun r -> RWfRec r) + | CMeasureRec c -> + intern_ro_arg (Some c) (fun r -> RMeasureRec r)) + in + let ids'' = List.fold_right Idset.add lf ids' in ((n, ro), List.rev rbl, intern_type (ids',tmp_scope,scopes) ty, intern (ids'',None,scopes) bd)) dl in @@ -824,11 +988,10 @@ let internalise sigma globalenv env allow_soapp lvar c = Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) | CCoFix (loc, (locid,iddef), dl) -> - let lf = List.map (fun (id,_,_,_) -> id) dl in + let lf = List.map (fun ((_, id),_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try - (list_index iddef lf) -1 + try list_index0 iddef lf with Not_found -> raise (InternalisationError (locid,UnboundFixName (true,iddef))) in @@ -846,18 +1009,18 @@ let internalise sigma globalenv env allow_soapp lvar c = Array.map (fun (_,ty,_) -> ty) idl, Array.map (fun (_,_,bd) -> bd) idl) | CArrow (loc,c1,c2) -> - RProd (loc, Anonymous, intern_type env c1, intern_type env c2) + RProd (loc, Anonymous, Explicit, intern_type env c1, intern_type env c2) | CProdN (loc,[],c2) -> intern_type env c2 - | CProdN (loc,(nal,ty)::bll,c2) -> - iterate_prod loc env ty (CProdN (loc, bll, c2)) nal + | CProdN (loc,(nal,bk,ty)::bll,c2) -> + iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal | CLambdaN (loc,[],c2) -> intern env c2 - | CLambdaN (loc,(nal,ty)::bll,c2) -> - iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,(_,na),c1,c2) -> + | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> + iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal + | CLetIn (loc,(loc1,na),c1,c2) -> RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_name_env lvar env na) c2) + intern (push_loc_name_env lvar env loc1 na) c2) | CNotation (loc,"- _",[CPrim (_,Numeral p)]) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) @@ -871,22 +1034,24 @@ let internalise sigma globalenv env allow_soapp lvar c = | CDelimiters (loc, key, e) -> intern (ids,None,find_delimiters_scope loc key::scopes) e | CAppExpl (loc, (isproj,ref), args) -> - let (f,_,args_scopes,_) = intern_reference env lvar ref in + let (f,_,args_scopes,_),args = + let args = List.map (fun a -> (a,None)) args in + intern_applied_reference intern env lvar args ref in check_projection isproj (List.length args) f; - RApp (loc, f, intern_args env args_scopes args) + RApp (loc, f, intern_args env args_scopes (List.map fst args)) | CApp (loc, (isproj,f), args) -> let isproj,f,args = match f with (* Compact notations like "t.(f args') args" *) | CApp (_,(Some _,f), args') when isproj=None -> isproj,f,args'@args (* Don't compact "(f args') args" to resolve implicits separately *) | _ -> isproj,f,args in - let (c,impargs,args_scopes,l) = + let (c,impargs,args_scopes,l),args = match f with - | CRef ref -> intern_reference env lvar ref + | CRef ref -> intern_applied_reference intern env lvar args ref | CNotation (loc,ntn,[]) -> let c = intern_notation intern env loc ntn [] in - find_appl_head_data lvar c - | x -> (intern env f,[],[],[]) in + find_appl_head_data lvar c, args + | x -> (intern env f,[],[],[]), args in let args = intern_impargs c env impargs args_scopes (merge_impargs l args) in check_projection isproj (List.length args) c; @@ -894,38 +1059,36 @@ let internalise sigma globalenv env allow_soapp lvar c = (* Now compact "(f args') args" *) | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args) | _ -> RApp (loc, c, args)) - | CCases (loc, rtnpo, tms, eqns) -> + | CCases (loc, sty, rtnpo, tms, eqns) -> let tms,env' = List.fold_right (fun citm (inds,env) -> let (tm,ind),nal = intern_case_item env citm in (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal) tms ([],env) in - let rtnpo = option_map (intern_type env') rtnpo in + let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, rtnpo, tms, List.flatten eqns') + RCases (loc, sty, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_map (intern_type env'') po in + let p' = Option.map (intern_type env'') po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_map (intern_type env'') po in + let p' = Option.map (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) - | CHole loc -> - RHole (loc, Evd.QuestionMark true) - | CPatVar (loc, n) when allow_soapp -> + | CHole (loc, k) -> + RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark true) + | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) - | CPatVar (loc, (false,n)) -> - error_unbound_patvar loc n | CPatVar (loc, _) -> raise (InternalisationError (loc,NegativeMetavariable)) - | CEvar (loc, n) -> - REvar (loc, n, None) + | CEvar (loc, n, l) -> + REvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> RSort(loc,s) | CCast (loc, c1, CastConv (k, c2)) -> @@ -937,29 +1100,20 @@ let internalise sigma globalenv env allow_soapp lvar c = and intern_type env = intern (set_type_scope env) - and intern_local_binder ((ids,ts,sc as env),bl) = function - | LocalRawAssum(nal,ty) -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) - let ty = locate_if_isevar loc na (intern_type env ty) in - List.fold_left - (fun ((ids,ts,sc),bl) (_,na) -> - ((name_fold Idset.add na ids,ts,sc), (na,None,ty)::bl)) - (env,bl) nal - | LocalRawDef((loc,na),def) -> - ((name_fold Idset.add na ids,ts,sc), - (na,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + and intern_local_binder env bind = + intern_local_binder_aux intern intern_type lvar env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) - and intern_multiple_pattern scopes pl = + and intern_multiple_pattern scopes n (loc,pl) = let idsl_pll = List.map (intern_cases_pattern globalenv scopes ([],[]) None) pl in + check_number_of_pattern loc n pl; product_of_cases_patterns [] idsl_pll (* Expands a disjunction of multiple pattern *) - and intern_disjunctive_multiple_pattern scopes loc mpl = + and intern_disjunctive_multiple_pattern scopes loc n mpl = assert (mpl <> []); - let mpl' = List.map (intern_multiple_pattern scopes) mpl in + let mpl' = List.map (intern_multiple_pattern scopes n) mpl in let (idsl,mpl') = List.split mpl' in let ids = List.hd idsl in check_or_pat_variables loc ids (List.tl idsl); @@ -967,10 +1121,9 @@ let internalise sigma globalenv env allow_soapp lvar c = (* Expands a pattern-matching clause [lhs => rhs] *) and intern_eqn n (ids,tmp_scope,scopes) (loc,lhs,rhs) = - let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc lhs in + let eqn_ids,pll = intern_disjunctive_multiple_pattern scopes loc n lhs in (* Linearity implies the order in ids is irrelevant *) check_linearity lhs eqn_ids; - check_number_of_pattern loc n (snd (List.hd pll)); let env_ids = List.fold_right Idset.add eqn_ids ids in List.map (fun (subst,pl) -> let rhs = replace_vars_constr_expr subst rhs in @@ -1008,23 +1161,40 @@ let internalise sigma globalenv env allow_soapp lvar c = | _, None -> Anonymous | _, Some na -> na in (tm',(na,typ)), na::ids - - and iterate_prod loc2 env ty body = function + + and iterate_prod loc2 env bk ty body nal = + let rec default env bk = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = iterate_prod loc2 (push_name_env lvar env na) ty body nal in + let body = default (push_loc_name_env lvar env loc1 na) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in - RProd (join_loc loc1 loc2, na, ty, body) + RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body - - and iterate_lam loc2 env ty body = function - | (loc1,na)::nal -> - if nal <> [] then check_capture loc1 ty na; - let body = iterate_lam loc2 (push_name_env lvar env na) ty body nal in - let ty = locate_if_isevar loc1 na (intern_type env ty) in - RLambda (join_loc loc1 loc2, na, ty, body) - | [] -> intern env body - + in + match bk with + | Default b -> default env b nal + | TypeClass b -> + let env, ibind = intern_typeclass_binder intern_type lvar + (env, []) (List.hd nal) b ty in + let body = intern_type env body in + it_mkRProd ibind body + + and iterate_lam loc2 env bk ty body nal = + let rec default env bk = function + | (loc1,na)::nal -> + if nal <> [] then check_capture loc1 ty na; + let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let ty = locate_if_isevar loc1 na (intern_type env ty) in + RLambda (join_loc loc1 loc2, na, bk, ty, body) + | [] -> intern env body + in match bk with + | Default b -> default env b nal + | TypeClass b -> + let env, ibind = intern_typeclass_binder intern_type lvar + (env, []) (List.hd nal) b ty in + let body = intern env body in + it_mkRLambda ibind body + and intern_impargs c env l subscopes args = let eargs, rargs = extract_explicit_arg l args in let rec aux n impl subscopes eargs rargs = @@ -1037,10 +1207,9 @@ let internalise sigma globalenv env allow_soapp lvar c = let eargs' = List.remove_assoc id eargs in intern enva a :: aux (n+1) impl' subscopes' eargs' rargs with Not_found -> - if rargs=[] & eargs=[] & - not (List.for_all is_status_implicit impl') then - (* Less regular arguments than expected: don't complete *) - (* with implicit arguments *) + if rargs=[] & eargs=[] & not (maximal_insertion_of imp) then + (* Less regular arguments than expected: complete *) + (* with implicit arguments if maximal insertion is set *) [] else RHole (set_hole_implicit (n,get_implicit_name n l) c) :: @@ -1051,7 +1220,7 @@ let internalise sigma globalenv env allow_soapp lvar c = | (imp::impl', []) -> if eargs <> [] then (let (id,(loc,_)) = List.hd eargs in - user_err_loc (loc,"",str "Not enough non implicit + user_err_loc (loc,"",str "Not enough non implicit arguments to accept the argument bound to " ++ pr_id id)); [] | ([], rargs) -> @@ -1082,13 +1251,13 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in - internalise sigma env (extract_ids env, tmp_scope,[]) - allow_soapp (ltacvars,Environ.named_context env, [], impls) c - + internalise sigma env (extract_ids env, tmp_scope,[]) + allow_patvar (ltacvars,Environ.named_context env, [], impls) c + let intern_constr sigma env c = intern_gen false sigma env c let intern_type sigma env c = intern_gen true sigma env c @@ -1104,17 +1273,36 @@ let intern_pattern env patt = let intern_ltac isarity ltacvars sigma env c = intern_gen isarity sigma env ~ltacvars:ltacvars c +type manual_implicits = (explicitation * (bool * bool)) list + +let implicits_of_rawterm l = + let rec aux i c = + match c with + RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true)) :: rest + else rest + | RLetIn (loc, na, t, b) -> aux i b + | _ -> [] + in aux 1 l + (*********************************************************************) (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) + ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) c = - Default.understand_gen kind sigma env - (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c) + let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in + Default.understand_gen kind sigma env c let interp_constr sigma env c = - interp_gen (OfType None) sigma env c + interp_gen (OfType None) sigma env c let interp_type sigma env ?(impls=([],[])) c = interp_gen IsType sigma env ~impls c @@ -1128,25 +1316,46 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) - -let interp_constr_evars_gen isevars env ?(impls=([],[])) kind c = - Default.understand_tcc_evars isevars env kind - (intern_gen (kind=IsType) ~impls (Evd.evars_of !isevars) env c) - -let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ = - interp_constr_evars_gen isevars env ~impls (OfType (Some typ)) c - -let interp_type_evars isevars env ?(impls=([],[])) c = - interp_constr_evars_gen isevars env IsType ~impls c - -let interp_constr_judgment_evars isevars env c = - Default.understand_judgment_tcc isevars env - (intern_constr (Evd.evars_of !isevars) env c) +let interp_constr_evars_gen_impls ?evdref + env ?(impls=([],[])) kind c = + match evdref with + | None -> + let c = intern_gen (kind=IsType) ~impls Evd.empty env c in + let imps = implicits_of_rawterm c in + Default.understand_gen kind Evd.empty env c, imps + | Some evdref -> + let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + let imps = implicits_of_rawterm c in + Default.understand_tcc_evars evdref env kind c, imps + +let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = + let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in + Default.understand_tcc_evars evdref env kind c + +let interp_casted_constr_evars_impls ?evdref + env ?(impls=([],[])) c typ = + interp_constr_evars_gen_impls ?evdref env ~impls (OfType (Some typ)) c + +let interp_type_evars_impls ?evdref env ?(impls=([],[])) c = + interp_constr_evars_gen_impls ?evdref env IsType ~impls c + +let interp_constr_evars_impls ?evdref env ?(impls=([],[])) c = + interp_constr_evars_gen_impls ?evdref env (OfType None) ~impls c + +let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = + interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c + +let interp_type_evars evdref env ?(impls=([],[])) c = + interp_constr_evars_gen evdref env IsType ~impls c + +let interp_constr_judgment_evars evdref env c = + Default.understand_judgment_tcc evdref env + (intern_constr (Evd.evars_of !evdref) env c) type ltac_sign = identifier list * unbound_ltac_var_map let interp_constrpattern sigma env c = - pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c) + pattern_of_rawconstr (intern_gen false sigma env ~allow_patvar:true c) let interp_aconstr impls vars a = let env = Global.env () in @@ -1169,50 +1378,58 @@ let interp_binder sigma env na t = let t' = locate_if_isevar (loc_of_rawconstr t) na t in Default.understand_type sigma env t' -let interp_binder_evars isevars env na t = - let t = intern_gen true (Evd.evars_of !isevars) env t in +let interp_binder_evars evdref env na t = + let t = intern_gen true (Evd.evars_of !evdref) env t in let t' = locate_if_isevar (loc_of_rawconstr t) na t in - Default.understand_tcc_evars isevars env IsType t' + Default.understand_tcc_evars evdref env IsType t' open Environ open Term -let interp_context sigma env params = - List.fold_left - (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder sigma env na t in - let d = (na,None,t) in - (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> - let t = interp_type sigma env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@params) - | LocalRawDef ((_,na),c) -> - let c = interp_constr_judgment sigma env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params)) - (env,[]) params - -let interp_context_evars isevars env params = - List.fold_left - (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> - let t = interp_binder_evars isevars env na t in - let d = (na,None,t) in - (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> - let t = interp_type_evars isevars env t in - let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in - let ctx = List.rev ctx in - (push_rel_context ctx env, ctx@params) - | LocalRawDef ((_,na),c) -> - let c = interp_constr_judgment_evars isevars env c in - let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env,d::params)) - (env,[]) params +let my_intern_constr sigma env lvar acc c = + internalise sigma env acc false lvar c + +let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c + +let intern_context sigma env params = + let lvar = (([],[]),Environ.named_context env, [], ([], [])) in + snd (List.fold_left + (intern_local_binder_aux (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) + ((extract_ids env,None,[]), []) params) + +let interp_context_gen understand_type understand_judgment env bl = + let (env, par, _, impls) = + List.fold_left + (fun (env,params,n,impls) (na, k, b, t) -> + match b with + None -> + let t' = locate_if_isevar (loc_of_rawconstr t) na t in + let t = understand_type env t' in + let d = (na,None,t) in + let impls = + if k = Implicit then + let na = match na with Name n -> Some n | Anonymous -> None in + (ExplByPos (n, na), (true, true)) :: impls + else impls + in + (push_rel d env, d::params, succ n, impls) + | Some b -> + let c = understand_judgment env b in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params, succ n, impls)) + (env,[],1,[]) (List.rev bl) + in (env, par), impls +let interp_context sigma env params = + let bl = intern_context sigma env params in + interp_context_gen (Default.understand_type sigma) + (Default.understand_judgment sigma) env bl + +let interp_context_evars evdref env params = + let bl = intern_context (Evd.evars_of !evdref) env params in + interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) + (Default.understand_judgment_tcc evdref) env bl + (**********************************************************************) (* Locating reference, possibly via an abbreviation *) @@ -1221,7 +1438,7 @@ let locate_reference qid = | TrueGlobal ref -> ref | SyntacticDef kn -> match Syntax_def.search_syntactic_definition dummy_loc kn with - | Rawterm.RRef (_,ref) -> ref + | [],ARef ref -> ref | _ -> raise Not_found let is_global id = -- cgit v1.2.3