From 71146049dd3d7087ebf392203b97f0c10c2fe90f Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 23 May 2006 18:25:58 +0000 Subject: Erreur commit constrintern.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8854 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrintern.ml | 1165 ------------------------------------------------ 1 file changed, 1165 deletions(-) delete mode 100644 interp/constrintern.ml (limited to 'interp/constrintern.ml') diff --git a/interp/constrintern.ml b/interp/constrintern.ml deleted file mode 100644 index 936d960d7..000000000 --- a/interp/constrintern.ml +++ /dev/null @@ -1,1165 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 1 then "s" else "" in - str "Expecting " ++ int n1 ++ str " pattern" ++ str s ++ str " but found " - ++ int n2 - -let explain_bad_explicitation_number n po = - match n with - | ExplByPos n -> - let s = match po with - | None -> str "a regular argument" - | Some p -> int p in - str "Bad explicitation number: found " ++ int n ++ - str" but was expecting " ++ s - | ExplByName id -> - let s = match po with - | None -> str "a regular argument" - | Some p -> (*pr_id (name_of_position p) in*) failwith "" in - str "Bad explicitation name: found " ++ pr_id id ++ - str" but was expecting " ++ s - -let explain_internalisation_error = function - | VariableCapture id -> explain_variable_capture id - | WrongExplicitImplicit -> explain_wrong_explicit_implicit - | NegativeMetavariable -> explain_negative_metavariable - | NotAConstructor ref -> explain_not_a_constructor ref - | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id - | NonLinearPattern id -> explain_non_linear_pattern id - | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2 - | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po - -let error_unbound_patvar loc n = - user_err_loc - (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ - str " is unbound") - -let error_bad_inductive_type loc = - user_err_loc (loc,"",str - "This should be an inductive type applied to names or \"_\"") - -(**********************************************************************) -(* Dump of globalization (to be used by coqdoc) *) -let token_number = ref 0 -let last_pos = ref 0 - -type coqdoc_state = Lexer.location_table * int * int - -let coqdoc_freeze () = - let lt = Lexer.location_table() in - let state = (lt,!token_number,!last_pos) in - token_number := 0; - last_pos := 0; - state - -let coqdoc_unfreeze (lt,tn,lp) = - Lexer.restore_location_table lt; - token_number := tn; - last_pos := lp - -let split_global ref = - let sp = Nametab.sp_of_global ref in - let lib_dp = Lib.library_part ref in - let mod_dp,id = repr_path sp 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 add_glob loc ref = - let file,fields,id = split_global ref in - let filepath = string_of_dirpath file in - let modpath = string_of_qualid (make_qualid fields id) in - dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath modpath) - -let loc_of_notation f loc args ntn = - if args=[] or ntn.[0] <> '_' then fst (unloc loc) - else snd (unloc (f (List.hd args))) - -let ntn_loc = loc_of_notation constr_loc -let patntn_loc = loc_of_notation cases_pattern_loc - -let dump_notation_location pos ((path,df),sc) = - let rec next growing = - let loc = Lexer.location_function !token_number in - let (bp,_) = unloc loc in - if growing then if bp >= pos then loc else (incr token_number;next true) - else if bp = pos then loc - else if bp > pos then (decr token_number;next false) - else (incr token_number;next true) in - 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) - -(**********************************************************************) -(* Contracting "{ _ }" in notations *) - -let rec wildcards ntn n = - if 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 n = String.length ntn then [] - else if ntn.[n] = ' ' then wildcards ntn (n+1) else spaces ntn (n+1) - -let expand_notation_string ntn n = - let pos = List.nth (wildcards ntn 0) n in - let hd = if pos = 0 then "" else String.sub ntn 0 pos in - let tl = - if pos = String.length ntn then "" - else String.sub ntn (pos+1) (String.length ntn - pos -1) in - hd ^ "{ _ }" ^ tl - -(* This contracts the special case of "{ _ }" for sumbool, sumor notations *) -(* Remark: expansion of squash at definition is done in metasyntax.ml *) -let contract_notation ntn l = - let ntn' = ref ntn in - let rec contract_squash n = function - | [] -> [] - | CNotation (_,"{ _ }",[a]) :: l -> - ntn' := expand_notation_string !ntn' n; - contract_squash n (a::l) - | a :: l -> - a::contract_squash (n+1) l in - let l = contract_squash 0 l in - (* side effect; don't inline *) - !ntn',l - -let contract_pat_notation ntn l = - let ntn' = ref ntn in - let rec contract_squash n = function - | [] -> [] - | CPatNotation (_,"{ _ }",[a]) :: l -> - ntn' := expand_notation_string !ntn' n; - contract_squash n (a::l) - | a :: l -> - a::contract_squash (n+1) l in - let l = contract_squash 0 l in - (* side effect; don't inline *) - !ntn',l - -(**********************************************************************) -(* Remembering the parsing scope of variables in notations *) - -let make_current_scope (scopt,scopes) = option_cons scopt 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 (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) - -(**********************************************************************) -(* Discriminating between bound variables and global references *) - -(* [vars1] is a set of name to avoid (used for the tactic language); - [vars2] is the set of global variables, env is the set of variables - abstracted until this point *) - -let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = - let (vars1,unbndltacvars) = ltacvars in - (* Is [id] an inductive type potentially with implicit *) - try - let l,impl,argsc = List.assoc id impls in - let l = List.map - (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in - RVar (loc,id), impl, argsc, l - with Not_found -> - (* Is [id] bound in current env or is an ltac var bound to constr *) - if Idset.mem id env or List.mem id vars1 - then - RVar (loc,id), [], [], [] - (* Is [id] a notation variable *) - else if List.mem_assoc id vars3 - then - (set_var_scope loc id genv vars3; RVar (loc,id), [], [], []) - else - - (* Is [id] bound to a free name in ltac (this is an ltac error message) *) - try - match List.assoc id unbndltacvars with - | None -> user_err_loc (loc,"intern_var", - str "variable " ++ pr_id id ++ str " should be bound to a term") - | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 - with Not_found -> - (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id vars2 in - try - (* [id] a section variable *) - (* Redundant: could be done in intern_qualid *) - let ref = VarRef id in - RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, [] - with _ -> - (* [id] a goal variable *) - RVar (loc,id), [], [], [] - -let find_appl_head_data (_,_,_,(_,impls)) = function - | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] - | x -> x,[],[],[] - -(* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid = - try match Nametab.extended_locate qid with - | TrueGlobal ref -> - if !dump then add_glob loc ref; - RRef (loc, ref) - | SyntacticDef sp -> - Syntax_def.search_syntactic_definition loc sp - with Not_found -> - error_global_not_found_loc loc qid - -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 - | Qualid (loc, qid) -> - find_appl_head_data lvar (intern_qualid loc qid) - | Ident (loc, id) -> - try intern_var env lvar loc id - with Not_found -> - try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id)) - with e -> - (* Extra allowance for non globalizing functions *) - if !interning_grammar then RVar (loc,id), [], [], [] - else raise e - -let interp_reference vars r = - let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r - in r - -let apply_scope_env (ids,_,scopes) = function - | [] -> (ids,None,scopes), [] - | sc::scl -> (ids,sc,scopes), scl - -let rec adjust_scopes env scopes = function - | [] -> [] - | a::args -> - 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) - -(**********************************************************************) -(* Cases *) - -let product_of_cases_patterns ids idspl = - List.fold_right (fun (ids,pl) (ids',ptaill) -> - (ids@ids', - (* Cartesian prod of the or-pats for the nth arg and the tail args *) - List.flatten ( - List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl))) - idspl (ids,[[],[]]) - -let simple_product_of_cases_patterns pl = - List.fold_right (fun pl ptaill -> - List.flatten (List.map (fun (subst,p) -> - List.map (fun (subst',ptail) -> (subst@subst',p::ptail)) ptaill) pl)) - pl [[],[]] - -(* Check linearity of pattern-matching *) -let rec has_duplicate = function - | [] -> None - | x::l -> if List.mem x l then (Some x) else has_duplicate l - -let loc_of_lhs lhs = - join_loc (cases_pattern_loc (List.hd lhs)) (cases_pattern_loc (list_last lhs)) - -let check_linearity lhs ids = - match has_duplicate ids with - | Some id -> - raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id)) - | None -> - () - -(* Match the number of pattern against the number of matched args *) -let check_number_of_pattern loc n l = - let p = List.length l in - if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p))) - -let check_or_pat_variables loc ids idsl = - if List.exists ((<>) ids) idsl then - user_err_loc (loc, "", str - "The components of this disjunctive pattern must bind the same variables") - -let check_constructor_length env loc cstr pl pl0 = - let n = List.length pl + List.length pl0 in - let nargs = Inductiveops.constructor_nrealargs env cstr in - let nhyps = Inductiveops.constructor_nrealhyps env cstr in - if n <> nargs && n <> nhyps (* i.e. with let's *) then - error_wrong_numarg_constructor_loc loc env cstr nargs - -(* Manage multiple aliases *) - - (* [merge_aliases] returns the sets of all aliases encountered at this - point and a substitution mapping extra aliases to the first one *) -let merge_aliases (ids,subst as _aliases) id = - ids@[id], if ids=[] then subst else (id, List.hd ids)::subst - -let alias_of = function - | ([],_) -> Anonymous - | (id::_,_) -> Name id - -let message_redundant_alias (id1,id2) = - if_verbose warning - ("Alias variable "^(string_of_id id1)^" is merged with "^(string_of_id id2)) - -(* Expanding notations *) - -let decode_patlist_value = function - | CPatCstr (_,_,l) -> l - | _ -> anomaly "Ill-formed list argument of notation" - -let rec subst_pat_iterator y t (subst,p) = match p with - | PatVar (_,id) as x -> - if id = Name y then t else [subst,x] - | PatCstr (loc,id,l,alias) -> - let l' = List.map (fun a -> (subst_pat_iterator y t ([],a))) l in - let pl = simple_product_of_cases_patterns l' in - List.map (fun (subst',pl) -> subst'@subst,PatCstr (loc,id,pl,alias)) pl - -let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a = - let rec aux aliases subst = 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 - intern (subscopes@scopes) ([],[]) scopt a - with Not_found -> - if id = ldots_var then [],[[], PatVar (loc,Name id)] else - anomaly ("Unbound pattern notation variable: "^(string_of_id id)) - (* - (* Happens for local notation joint with inductive/fixpoint defs *) - if aliases <> ([],[]) then - anomaly "Pattern notation without constructors"; - [[id],[]], PatVar (loc,Name id) - *) - end - | ARef (ConstructRef c) -> - (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)]) - | 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 - let idslpll = List.map (aux ([],[]) subst) args in - let ids',pll = product_of_cases_patterns ids idslpll in - let pl' = List.map (fun (subst,pl) -> - subst,PatCstr (loc,c,pl,alias_of aliases)) pll in - ids', pl' - | 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 = aux ([],[]) subst terminator in - let l = decode_patlist_value a in - let idsl,v = - List.fold_right (fun a (tids,t) -> - let uids,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in - let pll = List.map (subst_pat_iterator ldots_var t) u in - tids@uids, List.flatten pll) - (if lassoc then List.rev l else l) termin in - ids@idsl, v - with Not_found -> - anomaly "Inconsistent substitution of recursive notation") - | t -> user_err_loc (loc,"",str "Invalid notation for pattern") - in aux aliases subst a - -(* Differentiating between constructors and matching variables *) -type pattern_qualid_kind = - | ConstrPat of (constructor * cases_pattern 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 (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 - -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) - with - (* patt var does not exists globally *) - | InternalisationError _ -> VarPat (find_pattern_variable ref) - (* patt var also exists globally but does not satisfy preconditions *) - | (Environ.NotEvaluableConst _ | Not_found) -> - if_verbose msg_warning (str "pattern " ++ pr_reference ref ++ - str " is understood as a pattern variable"); - VarPat (find_pattern_variable ref) - -let mustbe_constructor loc ref = - try find_constructor ref - with (Environ.NotEvaluableConst _ | Not_found) -> - raise (InternalisationError (loc,NotAConstructor ref)) - -let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope = - function - | CPatAlias (loc, p, id) -> - let aliases' = merge_aliases aliases id in - intern_cases_pattern genv 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 pl' = List.map (fun (subst,pl) -> - (subst, PatCstr (loc,c,pl0@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)) - | CPatNotation (_,"( _ )",[a]) -> - intern_cases_pattern genv scopes aliases tmp_scope a - | CPatNotation (loc, ntn, args) -> - let ntn,args = contract_pat_notation ntn args in - let scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Notation.interp_notation loc ntn 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 - subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes - c - | CPatPrim (loc, p) -> - let scopes = option_cons tmp_scope scopes in - let a = alias_of aliases in - let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in - 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 - | 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)]) - | VarPat id -> - let ids,subst = merge_aliases aliases id in - (ids,[subst, PatVar (loc,alias_of (ids,subst))])) - | CPatAtom (loc, None) -> - (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 (idsl,pl') = List.split pl' in - let ids = List.hd idsl in - check_or_pat_variables loc ids (List.tl idsl); - (ids,List.flatten pl') - -(**********************************************************************) -(* Fix and CoFix *) - -(**********************************************************************) -(* Utilities for binders *) - -let check_capture loc ty = function - | Name id when occur_var_constr_expr id ty -> - raise (InternalisationError (loc,VariableCapture id)) - | _ -> - () - -let locate_if_isevar loc na = function - | RHole _ -> - (try match na with - | Name id -> Reserve.find_reserved_type id - | Anonymous -> raise Not_found - with Not_found -> RHole (loc, Evd.BinderType na)) - | x -> x - -let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = - if List.mem id indnames then - errorlabstrm "" (str "A parameter or name of an inductive type " ++ - pr_id id ++ str " must not be used as a bound variable in the type \ -of its constructor") - -let push_name_env lvar (ids,tmpsc,scopes as env) = function - | Anonymous -> env - | Name id -> - check_hidden_implicit_parameters id lvar; - (Idset.add id ids,tmpsc,scopes) - -(**********************************************************************) -(* Utilities for application *) - -let merge_impargs l args = - List.fold_right (fun a l -> - match a with - | (_,Some (_,(ExplByName id as x))) when - List.exists (function (_,Some (_,y)) -> x=y | _ -> false) args -> l - | _ -> a::l) - l args - -let check_projection isproj nargs r = - match (r,isproj) with - | RRef (loc, ref), Some _ -> - (try - let n = Recordops.find_projection_nparams ref + 1 in - if nargs <> n then - user_err_loc (loc,"",str "Projection has not the right number of explicit parameters"); - with Not_found -> - user_err_loc - (loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection")) - | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection") - | _, None -> () - -let get_implicit_name n imps = - Some (Impargs.name_of_implicit (List.nth imps (n-1))) - -let set_hole_implicit i = function - | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i)) - | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i)) - | _ -> anomaly "Only refs have implicits" - -let exists_implicit_name id = - List.exists (fun imp -> is_status_implicit imp & id = name_of_implicit imp) - -let extract_explicit_arg imps args = - let rec aux = function - | [] -> [],[] - | (a,e)::l -> - let (eargs,rargs) = aux l in - match e with - | None -> (eargs,a::rargs) - | Some (loc,pos) -> - let id = match pos with - | ExplByName id -> - if not (exists_implicit_name id imps) then - user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id); - if List.mem_assoc id eargs then - user_err_loc (loc,"",str "Argument name " ++ pr_id id - ++ str " occurs more than once"); - id - | ExplByPos p -> - let id = - try - let imp = List.nth imps (p-1) in - if not (is_status_implicit imp) then failwith "imp"; - name_of_implicit imp - with Failure _ (* "nth" | "imp" *) -> - user_err_loc (loc,"",str"Wrong argument position: " ++ int p) - in - if List.mem_assoc id eargs then - user_err_loc (loc,"",str"Argument at position " ++ int p ++ - str " is mentioned more than once"); - id in - ((id,(loc,a))::eargs,rargs) - in aux args - -(**********************************************************************) -(* Syntax extensions *) - -let traverse_binder subst id (ids,tmpsc,scopes as env) = - try - (* Binders bound in the notation are consider first-order object *) - (* and binders not bound in the notation do not capture variables *) - (* outside the notation *) - let _,id' = coerce_to_id (fst (List.assoc id subst)) in - id', (Idset.add id' ids,tmpsc,scopes) - with Not_found -> - id, env - -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 (ids,_,scopes as _env) = - 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 -> - (* 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 (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) - (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) (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 scopes = option_cons tmp_scope scopes in - let ((ids,c),df) = Notation.interp_notation loc ntn 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 rec intern (ids,tmp_scope,scopes as env) = function - | CRef ref as x -> - let (c,imp,subscopes,l) = intern_reference 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 dl = Array.of_list dl in - let n = - try - (list_index iddef lf) -1 - with Not_found -> - raise (InternalisationError (locid,UnboundFixName (false,iddef))) - in - let idl = Array.map - (fun (id,(n,order),bl,ty,bd) -> - let ro, ((ids',_,_),rbl) = - (match order with - CStructRec -> - RStructRec, - List.fold_left intern_local_binder (env,[]) bl - | CWfRec c -> - 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 = RWfRec (intern (ids', tmp_scope, scopes) c) in - ro, List.fold_left intern_local_binder (env,rafter) before) - 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 - RRec (loc,RFix - (Array.map (fun (ro,_,_,_) -> ro) idl,n), - Array.of_list lf, - Array.map (fun (_,bl,_,_) -> bl) idl, - 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 dl = Array.of_list dl in - let n = - try - (list_index iddef lf) -1 - with Not_found -> - raise (InternalisationError (locid,UnboundFixName (true,iddef))) - in - let idl = Array.map - (fun (id,bl,ty,bd) -> - let ((ids',_,_),rbl) = - List.fold_left intern_local_binder (env,[]) bl in - let ids'' = List.fold_right Idset.add lf ids' in - (List.rev rbl, - intern_type (ids',tmp_scope,scopes) ty, - intern (ids'',None,scopes) bd)) dl in - RRec (loc,RCoFix n, - Array.of_list lf, - Array.map (fun (bl,_,_) -> bl) idl, - 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) - | CProdN (loc,[],c2) -> - intern_type env c2 - | CProdN (loc,(nal,ty)::bll,c2) -> - iterate_prod loc env 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) -> - RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_name_env lvar env na) c2) - | CNotation (loc,"- _",[CPrim (_,Numeral p)]) - when Bigint.is_strictly_pos p -> - intern env (CPrim (loc,Numeral (Bigint.neg p))) - | CNotation (_,"( _ )",[a]) -> intern env a - | CNotation (loc,ntn,args) -> - intern_notation intern env loc ntn args - | CPrim (loc, p) -> - let scopes = option_cons tmp_scope scopes in - let c,df = Notation.interp_prim_token loc p scopes in - if !dump then dump_notation_location (fst (unloc loc)) df; - 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 - check_projection isproj (List.length args) f; - RApp (loc, f, intern_args env args_scopes 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) = - match f with - | CRef ref -> intern_reference env lvar ref - | CNotation (loc,ntn,[]) -> - let c = intern_notation intern env loc ntn [] in - find_appl_head_data lvar c - | x -> (intern env f,[],[],[]) in - let args = - intern_impargs c env impargs args_scopes (merge_impargs l args) in - check_projection isproj (List.length args) c; - (match c with - (* 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) -> - 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 eqns' = List.map (intern_eqn (List.length tms) env) eqns in - RCases (loc, 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 - 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 - RIf (loc, c', (na', p'), intern env b1, intern env b2) - | CHole loc -> - RHole (loc, Evd.QuestionMark) - | CPatVar (loc, n) when allow_soapp -> - 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) - | CSort (loc, s) -> - RSort(loc,s) - | CCast (loc, c1, k, c2) -> - RCast (loc,intern env c1,k,intern_type env c2) - - | CDynamic (loc,d) -> RDynamic (loc,d) - - and intern_type (ids,_,scopes) = - intern (ids,Some Notation.type_scope,scopes) - - 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_eqn n (ids,tmp_scope,scopes as _env) (loc,lhs,rhs) = - let idsl_pll = - List.map (intern_cases_pattern globalenv scopes ([],[]) None) lhs in - - let eqn_ids,pll = product_of_cases_patterns [] idsl_pll 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 - List.iter message_redundant_alias subst; - let rhs' = intern (env_ids,tmp_scope,scopes) rhs in - (loc,eqn_ids,pl,rhs')) pll - - and intern_case_item (vars,_,scopes as env) (tm,(na,t)) = - let tm' = intern env tm in - let ids,typ = match t with - | Some t -> - let tids = names_of_cases_indtype t in - let tids = List.fold_right Idset.add tids Idset.empty in - let t = intern_type (tids,None,scopes) t in - let (_,_,_,nal as indsign) = - match t with - | RRef (loc,IndRef ind) -> (loc,ind,0,[]) - | RApp (loc,RRef (_,IndRef ind),l) -> - let nparams, nrealargs = inductive_nargs globalenv ind in - let nindargs = nparams + nrealargs in - if List.length l <> nindargs then - error_wrong_numarg_inductive_loc loc globalenv ind nindargs; - let nal = List.map (function - | RHole _ -> Anonymous - | RVar (_,id) -> Name id - | c -> - user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in - let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then - user_err_loc (loc,"", - str "The parameters of inductive type must be implicit"); - (loc,ind,nparams,realnal) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) in - nal, Some indsign - | None -> - [], None in - let na = match tm', na with - | RVar (_,id), None when Idset.mem id vars -> Name id - | _, None -> Anonymous - | _, Some na -> na in - (tm',(na,typ)), na::ids - - and iterate_prod loc2 env ty body = 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 ty = locate_if_isevar loc1 na (intern_type env ty) in - RProd (join_loc loc1 loc2, na, 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 - - 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 = - let (enva,subscopes') = apply_scope_env env subscopes in - match (impl,rargs) with - | (imp::impl', rargs) when is_status_implicit imp -> - begin try - let id = name_of_implicit imp in - let (_,a) = List.assoc id eargs in - 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 *) - [] - else - RHole (set_hole_implicit (n,get_implicit_name n l) c) :: - aux (n+1) impl' subscopes' eargs rargs - end - | (imp::impl', a::rargs') -> - intern enva a :: aux (n+1) impl' subscopes' eargs rargs' - | (imp::impl', []) -> - if eargs <> [] then - (let (id,(loc,_)) = List.hd eargs in - user_err_loc (loc,"",str "Not enough non implicit - arguments to accept the argument bound to " ++ pr_id id)); - [] - | ([], rargs) -> - assert (eargs = []); - intern_args env subscopes rargs - in aux 1 l subscopes eargs rargs - - and intern_args env subscopes = function - | [] -> [] - | a::args -> - let (enva,subscopes) = apply_scope_env env subscopes in - (intern enva a) :: (intern_args env subscopes args) - - in - try - intern env c - with - InternalisationError (loc,e) -> - user_err_loc (loc,"internalize",explain_internalisation_error e) - -(**************************************************************************) -(* Functions to translate constr_expr into rawconstr *) -(**************************************************************************) - -let extract_ids env = - List.fold_right Idset.add - (Termops.ids_of_rel_context (Environ.rel_context env)) - Idset.empty - -let intern_gen isarity sigma env - ?(impls=([],[])) ?(allow_soapp=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 - -let intern_constr sigma env c = intern_gen false sigma env c - -let intern_ltac isarity ltacvars sigma env c = - intern_gen isarity sigma env ~ltacvars:ltacvars c - -(*********************************************************************) -(* Functions to parse and interpret constructions *) - -let interp_gen kind sigma env - ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) - c = - Default.understand_gen kind sigma env - (intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars sigma env c) - -let interp_constr sigma env c = - interp_gen (OfType None) sigma env c - -let interp_type sigma env ?(impls=([],[])) c = - interp_gen IsType sigma env ~impls c - -let interp_casted_constr sigma env ?(impls=([],[])) c typ = - interp_gen (OfType (Some typ)) sigma env ~impls c - -let interp_open_constr sigma env c = - Default.understand_tcc sigma env (intern_constr sigma env c) - -let interp_constr_judgment sigma env c = - Default.understand_judgment sigma env (intern_constr sigma 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) - -let interp_aconstr impls vars a = - let env = Global.env () in - (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = List.map (fun id -> (id,ref None)) vars in - let c = internalise Evd.empty (Global.env()) (extract_ids env, None, []) - false (([],[]),Environ.named_context env,vl,([],impls)) a in - (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_rawconstr vars c in - (* Returns [a] and the ordered list of variables with their scopes *) - (* Variables occurring in binders have no relevant scope since bound *) - List.map - (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl, - a - -(* Interpret binders and contexts *) - -let interp_binder sigma env na t = - let t = intern_gen true sigma env t in - Default.understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na 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 - -(**********************************************************************) -(* Locating reference, possibly via an abbreviation *) - -let locate_reference qid = - match Nametab.extended_locate qid with - | TrueGlobal ref -> ref - | SyntacticDef kn -> - match Syntax_def.search_syntactic_definition dummy_loc kn with - | Rawterm.RRef (_,ref) -> ref - | _ -> raise Not_found - -let is_global id = - try - let _ = locate_reference (make_short_qualid id) in true - with Not_found -> - false - -let global_reference id = - constr_of_global (locate_reference (make_short_qualid id)) - -let construct_reference ctx id = - try - Term.mkVar (let _ = Sign.lookup_named id ctx in id) - with Not_found -> - global_reference id - -let global_reference_in_absolute_module dir id = - constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id)) - -- cgit v1.2.3