diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 539 |
1 files changed, 262 insertions, 277 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bacdb387..6fcd9d7a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *) +(* $Id: constrintern.ml 8654 2006-03-22 15:36:58Z msozeau $ *) open Pp open Util @@ -18,9 +18,10 @@ open Impargs open Rawterm open Pattern open Pretyping +open Cases open Topconstr open Nametab -open Symbols +open Notation (* To interpret implicits and arg scopes of recursive variables in inductive types and recursive definitions *) @@ -42,10 +43,6 @@ let for_grammar f x = let variables_bind = ref false -(* For the translator *) -let temporary_implicits_in = ref [] -let set_temporary_implicits_in l = temporary_implicits_in := l - (**********************************************************************) (* Internalisation errors *) @@ -154,10 +151,8 @@ let add_glob loc ref = i*) let sp = Nametab.sp_of_global ref in let id = let _,id = repr_path sp in string_of_id id in - let dir = Lib.file_part ref in - if dir <> None then - let dp = string_of_dirpath (out_some dir) in - dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id) + let dp = string_of_dirpath (Lib.library_part ref) in + dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id) let loc_of_notation f loc args ntn = if args=[] or ntn.[0] <> '_' then fst (unloc loc) @@ -166,20 +161,19 @@ let loc_of_notation f loc args ntn = let ntn_loc = loc_of_notation constr_loc let patntn_loc = loc_of_notation cases_pattern_loc -let dump_notation_location = - fun pos ntn ((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) +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 *) @@ -249,15 +243,14 @@ let set_var_scope loc id (_,scopt,scopes) varscopes = [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 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, - (if !Options.v7 & !interning_grammar then [] else l) + 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 @@ -273,7 +266,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id = try match List.assoc id unbndltacvars with | None -> user_err_loc (loc,"intern_var", - pr_id id ++ str " ist not bound to a term") + 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 *) @@ -287,7 +280,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,_,impls) loc id = (* [id] a goal variable *) RVar (loc,id), [], [], [] -let find_appl_head_data (_,_,_,_,impls) = function +let find_appl_head_data (_,_,_,(_,impls)) = function | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[] | x -> x,[],[],[] @@ -320,13 +313,6 @@ let intern_reference env lvar = function | Qualid (loc, qid) -> find_appl_head_data lvar (intern_qualid loc qid) | Ident (loc, id) -> - (* For old ast syntax compatibility *) - if (string_of_id id).[0] = '$' then RVar (loc,id),[],[],[] else - (* End old ast syntax compatibility *) - (* Pour traduction des implicites d'inductifs et points-fixes *) - try RVar (loc,id), List.assoc id !temporary_implicits_in, [], [] - with Not_found -> - (* Fin pour traduction *) try intern_var env lvar loc id with Not_found -> try find_appl_head_data lvar (intern_qualid loc (make_short_qualid id)) @@ -336,10 +322,10 @@ let intern_reference env lvar = function else raise e let interp_reference vars r = - let (r,_,_,_) = intern_reference (Idset.empty,None,[]) (vars,[],[],[],[]) r + let r,_,_,_ = intern_reference (Idset.empty,None,[]) (vars,[],[],([],[])) r in r -let apply_scope_env (ids,_,scopes as env) = function +let apply_scope_env (ids,_,scopes) = function | [] -> (ids,None,scopes), [] | sc::scl -> (ids,sc,scopes), scl @@ -357,6 +343,21 @@ let rec simple_adjust_scopes = function (**********************************************************************) (* 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 @@ -372,32 +373,33 @@ let check_linearity lhs ids = | None -> () -(* Warns if some pattern variable starts with uppercase *) -let check_uppercase loc ids = -(* A quoi ça sert ? Pour l'extraction vers ML ? Maintenant elle est externe - let is_uppercase_var v = - match (string_of_id v).[0] with 'A'..'Z' -> true | _ -> false - in - let warning_uppercase loc uplid = - let vars = h 0 (prlist_with_sep pr_coma pr_id uplid) in - let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in - warn (str ("the variable"^s1) ++ vars ++ - str (" start"^s2^"with an upper case letter in pattern")) in - let uplid = List.filter is_uppercase_var ids in - if uplid <> [] then warning_uppercase loc uplid -*) - () - (* 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 + +let check_inductive_length env (loc,ind,nal) = + let n = Inductiveops.inductive_nargs env ind in + if n <> List.length nal then + error_wrong_numarg_inductive_loc loc env ind n + (* 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 = +let merge_aliases (ids,subst as _aliases) id = ids@[id], if ids=[] then subst else (id, List.hd ids)::subst let alias_of = function @@ -414,13 +416,15 @@ let decode_patlist_value = function | CPatCstr (_,_,l) -> l | _ -> anomaly "Ill-formed list argument of notation" -let rec subst_pat_iterator y t = function +let rec subst_pat_iterator y t (subst,p) = match p with | PatVar (_,id) as x -> - if id = Name y then t else x + if id = Name y then t else [subst,x] | PatCstr (loc,id,l,alias) -> - PatCstr (loc,id,List.map (subst_pat_iterator y t) 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 aliases intern subst scopes a = +let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a = let rec aux aliases subst = function | AVar id -> begin @@ -430,7 +434,7 @@ let subst_cases_pattern loc aliases intern subst scopes a = 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 + 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 *) @@ -440,24 +444,28 @@ let subst_cases_pattern loc aliases intern subst scopes a = *) end | ARef (ConstructRef c) -> - [aliases], PatCstr (loc,c, [], alias_of aliases) + (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)]) | AApp (ARef (ConstructRef (ind,_ as c)),args) -> - let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let _,args = list_chop nparams args in - let (idsl,pl) = List.split (List.map (aux ([],[]) subst) args) in - aliases::List.flatten idsl, PatCstr (loc,c,pl,alias_of aliases) + 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 idslt,termin = aux ([],[]) subst terminator in + let termin = aux ([],[]) subst terminator in let l = decode_patlist_value a in let idsl,v = - List.fold_right (fun a (allidsl,t) -> - let idsl,u = aux ([],[]) ((x,(a,(scopt,subscopes)))::subst) iter in - idsl::allidsl, subst_pat_iterator ldots_var t u) - (if lassoc then List.rev l else l) ([idslt],termin) in - aliases::List.flatten 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") @@ -476,7 +484,7 @@ let rec patt_of_rawterm loc cstr = | 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 (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 @@ -506,7 +514,7 @@ let find_constructor ref = let rec unf = function | ConstRef cst -> let v = Environ.constant_value (Global.env()) cst in - unf (reference_of_constr v) + unf (global_of_constr v) | ConstructRef c -> if !dump then add_glob loc r; c, [] @@ -524,7 +532,7 @@ let maybe_constructor ref = | InternalisationError _ -> VarPat (find_pattern_variable ref) (* patt var also exists globally but does not satisfy preconditions *) | (Environ.NotEvaluableConst _ | Not_found) -> - warn (str "pattern " ++ pr_reference ref ++ + if_verbose msg_warning (str "pattern " ++ pr_reference ref ++ str " is understood as a pattern variable"); VarPat (find_pattern_variable ref) @@ -533,48 +541,63 @@ let mustbe_constructor loc ref = with (Environ.NotEvaluableConst _ | Not_found) -> raise (InternalisationError (loc,NotAConstructor ref)) -let rec intern_cases_pattern scopes aliases tmp_scope = function +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 scopes aliases' tmp_scope p + 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 - let (idsl,pl') = - List.split (List.map2 (intern_cases_pattern scopes ([],[])) argscs pl) - in - (aliases::(List.flatten idsl), PatCstr (loc,c,pl0@pl',alias_of aliases)) - | CPatNotation (loc,"- _",[CPatNumeral(_,Bignat.POS p)]) -> - let scopes = option_cons tmp_scope scopes in - ([aliases], - Symbols.interp_numeral_as_pattern loc (Bignat.NEG p) - (alias_of aliases) scopes) + 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 scopes aliases tmp_scope 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) = Symbols.interp_notation loc ntn scopes in - if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df; + 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 subst scopes c - | CPatNumeral (loc, n) -> + subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes + c + | CPatPrim (loc, p) -> let scopes = option_cons tmp_scope scopes in - ([aliases], - Symbols.interp_numeral_as_pattern loc n (alias_of aliases) scopes) + 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 (find_delimiters_scope loc key::scopes) + 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) -> - ([aliases], PatCstr (loc,c,args,alias_of aliases)) + check_constructor_length genv loc c [] []; + (ids,[subst, PatCstr (loc,c,args,alias_of aliases)]) | VarPat id -> - let aliases = merge_aliases aliases id in - ([aliases], PatVar (loc,alias_of aliases))) + let ids,subst = merge_aliases aliases id in + (ids,[subst, PatVar (loc,alias_of (ids,subst))])) | CPatAtom (loc, None) -> - ([aliases], PatVar (loc,alias_of aliases)) + (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 *) @@ -593,10 +616,10 @@ let locate_if_isevar loc na = function (try match na with | Name id -> Reserve.find_reserved_type id | Anonymous -> raise Not_found - with Not_found -> RHole (loc, BinderType na)) + with Not_found -> RHole (loc, Evd.BinderType na)) | x -> x -let check_hidden_implicit_parameters id (_,_,_,indnames,_) = +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 \ @@ -624,8 +647,8 @@ let check_projection isproj nargs r = | 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 enough parameters"); + 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")) @@ -633,12 +656,11 @@ let check_projection isproj nargs r = | _, None -> () let get_implicit_name n imps = - if !Options.v7 then None - else Some (Impargs.name_of_implicit (List.nth imps (n-1))) + Some (Impargs.name_of_implicit (List.nth imps (n-1))) let set_hole_implicit i = function - | RRef (loc,r) -> (loc,ImplicitArg (r,i)) - | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i)) + | 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 = @@ -679,18 +701,12 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Syntax extensions *) -let coerce_to_id = function - | CRef (Ident (_,id)) -> id - | c -> - user_err_loc (constr_loc c, "subst_rawconstr", - str"This expression should be a simple identifier") - 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 + let _,id' = coerce_to_id (fst (List.assoc id subst)) in id', (Idset.add id' ids,tmpsc,scopes) with Not_found -> id, env @@ -703,7 +719,7 @@ 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) = +let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) = function | AVar id -> begin @@ -739,13 +755,13 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as env) = 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) = Symbols.interp_notation loc ntn scopes in - if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df; + 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 Symbols.type_scope,scopes) + (ids,Some Notation.type_scope,scopes) let reset_tmp_scope (ids,tmp_scope,scopes) = (ids,None,scopes) @@ -753,7 +769,7 @@ let reset_tmp_scope (ids,tmp_scope,scopes) = (**********************************************************************) (* Main loop *) -let internalise sigma env allow_soapp lvar c = +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 @@ -769,20 +785,30 @@ let internalise sigma env allow_soapp lvar c = with Not_found -> raise (InternalisationError (locid,UnboundFixName (false,iddef))) in - let ids' = List.fold_right Idset.add lf ids in let idl = Array.map - (fun (id,n,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,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n), + (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 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) + 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 @@ -792,15 +818,14 @@ let internalise sigma env allow_soapp lvar c = with Not_found -> raise (InternalisationError (locid,UnboundFixName (true,iddef))) in - let ids' = List.fold_right Idset.add lf ids in let idl = Array.map (fun (id,bl,ty,bd) -> - let ((ids'',_,_),rbl) = + let ((ids',_,_),rbl) = List.fold_left intern_local_binder (env,[]) bl in - let ids''' = List.fold_right Idset.add lf ids'' 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 + 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, @@ -819,15 +844,17 @@ let internalise sigma env allow_soapp lvar c = | CLetIn (loc,(_,na),c1,c2) -> RLetIn (loc, na, intern (reset_tmp_scope env) c1, intern (push_name_env lvar env na) c2) - | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) -> - let scopes = option_cons tmp_scope scopes in - Symbols.interp_numeral loc (Bignat.NEG p) scopes + | 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 - | CNumeral (loc, n) -> + | CPrim (loc, p) -> let scopes = option_cons tmp_scope scopes in - Symbols.interp_numeral loc n scopes + 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) -> @@ -847,26 +874,22 @@ let internalise sigma env allow_soapp lvar c = 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 + 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, (po,rtnpo), tms, eqns) -> + | 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,ref ind)::inds,List.fold_left (push_name_env lvar) env nal) + (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal) tms ([],env) in let rtnpo = option_app (intern_type env') rtnpo in - RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms, - List.map (intern_eqn (List.length tms) env) eqns) - | COrderedCase (loc, tag, po, c, cl) -> - let env = reset_tmp_scope env in - ROrderedCase (loc, tag, option_app (intern_type env) po, - intern env c, - Array.of_list (List.map (intern env) cl),ref None) + 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 @@ -881,58 +904,52 @@ let internalise sigma env allow_soapp lvar c = let p' = option_app (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> - RHole (loc, QuestionMark) + RHole (loc, Evd.QuestionMark) | CPatVar (loc, n) when allow_soapp -> RPatVar (loc, n) - | CPatVar (loc, (false,n)) when Options.do_translate () -> - RVar (loc, n) - | CPatVar (loc, (false,n as x)) -> - if List.mem n (fst (let (a,_,_,_,_) = lvar in a)) & !Options.v7 then - RVar (loc, n) - else - error_unbound_patvar 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, c2) -> - RCast (loc,intern env c1,intern_type env c2) + | 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 Symbols.type_scope,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 + | 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,BinderType na))::bl) - - and intern_eqn n (ids,tmp_scope,scopes as env) (loc,lhs,rhs) = - let (idsl_substl_list,pl) = - List.split - (List.map (intern_cases_pattern scopes ([],[]) None) lhs) in - let idsl, substl = List.split (List.flatten idsl_substl_list) in - let eqn_ids = List.flatten idsl in - let subst = List.flatten substl in - (* Linearity implies the order in ids is irrelevant *) - check_linearity lhs eqn_ids; - check_uppercase loc eqn_ids; - check_number_of_pattern loc n pl; - let rhs = replace_vars_constr_expr subst rhs in - List.iter message_redundant_alias subst; - let env_ids = List.fold_right Idset.add eqn_ids ids in - (loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs) + (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 @@ -941,21 +958,23 @@ let internalise sigma env allow_soapp lvar c = 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 - begin match t with - | RRef (loc,IndRef ind) -> [],Some (loc,ind,[]) + let (_,_,nal as indsign) = + match t with + | RRef (loc,IndRef ind) -> (loc,ind,[]) | RApp (loc,RRef (_,IndRef ind),l) -> 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 - nal, Some (loc,ind,nal) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) - end + (loc,ind,nal) + | _ -> error_bad_inductive_type (loc_of_rawconstr t) in + check_inductive_length globalenv indsign; + nal, Some indsign | None -> [], None in let na = match tm', na with - | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id + | RVar (_,id), None when Idset.mem id vars -> Name id | _, None -> Anonymous | _, Some na -> na in (tm',(na,typ)), na::ids @@ -1032,114 +1051,53 @@ let extract_ids env = (Termops.ids_of_rel_context (Environ.rel_context env)) Idset.empty -let interp_rawconstr_gen_with_implicits isarity sigma env (indpars,impls) allow_soapp ltacvar c = - let tmp_scope = if isarity then Some Symbols.type_scope else None in - internalise sigma (extract_ids env, tmp_scope,[]) - allow_soapp (ltacvar,Environ.named_context env, [], indpars, impls) c - -let interp_rawconstr_gen isarity sigma env allow_soapp ltacvar c = - interp_rawconstr_gen_with_implicits isarity sigma env ([],[]) allow_soapp ltacvar c - -let interp_rawconstr sigma env c = - interp_rawconstr_gen false sigma env false ([],[]) c - -let interp_rawtype sigma env c = - interp_rawconstr_gen true sigma env false ([],[]) c +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 interp_rawtype_with_implicits sigma env impls c = - interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c +let intern_constr sigma env c = intern_gen false sigma env c -let interp_rawconstr_with_implicits sigma env vars impls c = - interp_rawconstr_gen_with_implicits false sigma env ([],impls) false - (vars,[]) c - -(* -(* The same as interp_rawconstr but with a list of variables which must not be - globalized *) - -let interp_rawconstr_wo_glob sigma env lvar c = - interp_rawconstr_gen sigma env [] (Some []) lvar 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_constr sigma env c = - understand sigma env (interp_rawconstr sigma env c) - -let interp_openconstr sigma env c = - understand_gen_tcc sigma env [] None (interp_rawconstr sigma env c) - -let interp_casted_openconstr sigma env c typ = - understand_gen_tcc sigma env [] (Some typ) (interp_rawconstr sigma env c) - -let interp_type sigma env c = - understand_type sigma env (interp_rawtype sigma env c) - -let interp_binder sigma env na t = - let t = interp_rawtype sigma env t in - understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t) - -let interp_type_with_implicits sigma env impls c = - understand_type sigma env (interp_rawtype_with_implicits sigma env impls c) +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 judgment_of_rawconstr sigma env c = - understand_judgment sigma env (interp_rawconstr sigma env c) - -let type_judgment_of_rawconstr sigma env c = - understand_type_judgment sigma env (interp_rawconstr sigma env c) - -(* To retype a list of key*constr with undefined key *) -let retype_list sigma env lst = - List.fold_right (fun (x,csr) a -> - try (x,Retyping.get_judgment_of env sigma csr)::a with - | Anomaly _ -> a) lst [] - -(* List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*) - -type ltac_sign = - identifier list * (identifier * identifier option) list - -type ltac_env = - (identifier * Term.constr) list * (identifier * identifier option) list +let interp_constr sigma env c = + interp_gen (OfType None) sigma env c -(* Interprets a constr according to two lists *) -(* of instantiations (variables and metas) *) -(* Note: typ is retyped *) -let interp_constr_gen sigma env (ltacvars,unbndltacvars) c exptyp = - let c = interp_rawconstr_gen false sigma env false - (List.map fst ltacvars,unbndltacvars) c in - let typs = retype_list sigma env ltacvars in - understand_gen sigma env typs exptyp c +let interp_type sigma env ?(impls=([],[])) c = + interp_gen IsType sigma env ~impls c -(*Interprets a casted constr according to two lists of instantiations - (variables and metas)*) -let interp_openconstr_gen sigma env (ltacvars,unbndltacvars) c exptyp = - let c = interp_rawconstr_gen false sigma env false - (List.map fst ltacvars,unbndltacvars) c in - let typs = retype_list sigma env ltacvars in - understand_gen_tcc sigma env typs exptyp c +let interp_casted_constr sigma env ?(impls=([],[])) c typ = + interp_gen (OfType (Some typ)) sigma env ~impls c -let interp_casted_constr sigma env c typ = - understand_gen sigma env [] (Some typ) (interp_rawconstr sigma env c) +let interp_open_constr sigma env c = + Default.understand_tcc sigma env (intern_constr sigma env c) -let interp_casted_constr_with_implicits sigma env impls c typ = - understand_gen sigma env [] (Some typ) - (interp_rawconstr_with_implicits sigma env [] impls c) +let interp_constr_judgment sigma env c = + Default.understand_judgment sigma env (intern_constr sigma env c) -let interp_constrpattern_gen sigma env ltacvar c = - let c = interp_rawconstr_gen false sigma env true (ltacvar,[]) c in - pattern_of_rawconstr c +type ltac_sign = identifier list * unbound_ltac_var_map let interp_constrpattern sigma env c = - interp_constrpattern_gen 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 (extract_ids env, None, []) - false (([],[]),Environ.named_context env,vl,[],impls) a 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 *) @@ -1148,6 +1106,33 @@ let interp_aconstr impls vars a = (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 *) @@ -1166,7 +1151,7 @@ let is_global id = false let global_reference id = - constr_of_reference (locate_reference (make_short_qualid id)) + constr_of_global (locate_reference (make_short_qualid id)) let construct_reference ctx id = try @@ -1175,5 +1160,5 @@ let construct_reference ctx id = global_reference id let global_reference_in_absolute_module dir id = - constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id)) + constr_of_global (Nametab.absolute_reference (Libnames.make_path dir id)) |