From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- interp/constrextern.ml | 28 +++++++++++------------ interp/constrextern.mli | 4 ++-- interp/constrintern.ml | 49 +++++++++++++++++++++++++++++++---------- interp/constrintern.mli | 4 ++-- interp/coqlib.ml | 6 ++--- interp/coqlib.mli | 4 ++-- interp/dumpglob.ml | 34 ++++++++++++++++++---------- interp/dumpglob.mli | 4 ++-- interp/genarg.ml | 4 ++-- interp/genarg.mli | 4 ++-- interp/implicit_quantifiers.ml | 4 ++-- interp/implicit_quantifiers.mli | 4 ++-- interp/modintern.ml | 4 ++-- interp/modintern.mli | 4 ++-- interp/notation.ml | 30 +++++++++++++------------ interp/notation.mli | 4 ++-- interp/ppextend.ml | 4 ++-- interp/ppextend.mli | 4 ++-- interp/reserve.ml | 4 ++-- interp/reserve.mli | 4 ++-- interp/smartlocate.ml | 2 +- interp/smartlocate.mli | 2 +- interp/syntax_def.ml | 4 ++-- interp/syntax_def.mli | 4 ++-- interp/topconstr.ml | 5 +++-- interp/topconstr.mli | 4 ++-- 26 files changed, 133 insertions(+), 95 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 1716cfad..dc339622 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in - let (ids,bl) = extern_local_binder scopes vars bl in + let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in let n = match fst nv.(i) with | None -> None - | Some x -> Some (dummy_loc, out_name (List.nth ids x)) + | Some x -> Some (dummy_loc, out_name (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty, @@ -745,7 +745,7 @@ let rec extern inctx scopes vars r = | RCoFix n -> let listdecl = Array.mapi (fun i fi -> - let (ids,bl) = extern_local_binder scopes vars blv.(i) in + let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i), @@ -795,24 +795,24 @@ and factorize_lambda inctx scopes vars aty c = | c -> ([],sub_extern inctx scopes vars c) and extern_local_binder scopes vars = function - [] -> ([],[]) + [] -> ([],[],[]) | (na,bk,Some bd,ty)::l -> - let (ids,l) = + let (assums,ids,l) = extern_local_binder scopes (name_fold Idset.add na vars) l in - (na::ids, + (assums,na::ids, LocalRawDef((dummy_loc,na), extern false scopes vars bd) :: l) | (na,bk,None,ty)::l -> let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with - (ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,LocalRawAssum(nal,k,ty')::l) when same ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> - (na::ids, + (na::assums,na::ids, LocalRawAssum((dummy_loc,na)::nal,k,ty')::l) - | (ids,l) -> - (na::ids, + | (assums,ids,l) -> + (na::assums,na::ids, LocalRawAssum([(dummy_loc,na)],Default bk,ty) :: l)) and extern_eqn inctx scopes vars (loc,ids,pl,c) = @@ -870,7 +870,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function termlists in let bll = List.map (fun (bl,(scopt,scl)) -> - snd (extern_local_binder (scopt,scl@scopes') vars bl)) + pi3 (extern_local_binder (scopt,scl@scopes') vars bl)) binders in insert_delimiters (make_notation loc ntn (l,ll,bll)) key) | SynDefRule kn -> @@ -1007,4 +1007,4 @@ let extern_constr_pattern env pat = let extern_rel_context where env sign = let a = detype_rel_context where [] (names_of_rel_context env) sign in let vars = vars_of_env env in - snd (extern_local_binder (None,[]) vars a) + pi3 (extern_local_binder (None,[]) vars a) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 248abeda..d0ccde2a 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* RHole (loc, Evd.BinderType na)) | x -> x +let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) = + let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in + (ltacvars,namedctxvars,ntnvars,List.map f impls) + let check_hidden_implicit_parameters id (_,_,_,impls) = if List.exists (function | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams @@ -461,6 +465,19 @@ let traverse_binder (terms,_,_ as subst) let renaming' = if id=id' then renaming else (id,id')::renaming in (renaming',env), Name id' +let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c)) + +let rec subordinate_letins letins = function + (* binders come in reverse order; the non-let are returned in reverse order together *) + (* with the subordinated let-in in writing order *) + | (na,_,Some b,t)::l -> + subordinate_letins ((na,b,t)::letins) l + | (na,bk,None,t)::l -> + let letins',rest = subordinate_letins [] l in + letins',((na,bk,t),letins)::rest + | [] -> + letins,[] + 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 @@ -505,19 +522,21 @@ let subst_aconstr_in_rawconstr loc intern lvar subst infos c = (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = List.assoc x binders in let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in + let letins,bl = subordinate_letins [] bl in let termin = aux subst' (renaming,env) terminator in - List.fold_left (fun t binder -> + let res = List.fold_left (fun t binder -> subst_iterator ldots_var t (aux (terms,Some(x,binder)) subinfos iter)) - termin bl + termin bl in + make_letins loc letins res with Not_found -> anomaly "Inconsistent substitution of recursive notation") | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> - let (na,bk,_,t) = snd (Option.get binderopt) in - RProd (loc,na,bk,t,aux subst' infos c') + let (na,bk,t),letins = snd (Option.get binderopt) in + RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> - let (na,bk,_,t) = snd (Option.get binderopt) in - RLambda (loc,na,bk,t,aux subst' infos c') + let (na,bk,t),letins = snd (Option.get binderopt) in + RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c')) | t -> rawconstr_of_aconstr_with_binders loc (traverse_binder subst) (aux subst') subinfos t @@ -846,7 +865,7 @@ let find_constructor ref f aliases pats scopes = 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 + let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in cstr, idspl1, pats2 | _ -> raise Not_found) @@ -1242,7 +1261,9 @@ let internalize sigma globalenv env allow_patvar lvar c = 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) + (tm,ind)::inds,List.fold_left + (push_name_env (reset_hidden_inductive_implicit_test 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 @@ -1251,7 +1272,9 @@ let internalize sigma globalenv env allow_patvar lvar c = let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let p' = Option.map (fun p -> - let env'' = List.fold_left (push_name_env lvar) env ids in + let env'' = List.fold_left + (push_name_env (reset_hidden_inductive_implicit_test lvar)) + env ids in intern_type env'' p) po in RLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) @@ -1259,7 +1282,9 @@ let internalize sigma globalenv env allow_patvar lvar c = let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in let p' = Option.map (fun p -> - let env'' = List.fold_left (push_name_env lvar) env ids in + let env'' = List.fold_left + (push_name_env (reset_hidden_inductive_implicit_test lvar)) + env ids in intern_type env'' p) po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 02a51e7e..767ec9ff 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* " ty) + let bl,el = interval loc in + dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" + bl el fp mp "<>" ty) let dump_moddef loc mp ty = if dump () then + let bl,el = interval loc in let (dp, l) = Lib.split_modpath mp in let mp = Names.string_of_dirpath (Names.make_dirpath l) in - dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp) + dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp) let dump_libref loc dp ty = - dump_string (Printf.sprintf "R%d %s <> <> %s\n" - (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) + let bl,el = interval loc in + dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n" + bl el (Names.string_of_dirpath dp) ty) let cook_notation df sc = (* We encode notations so that they are space-free and still human-readable *) diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 049bad5a..d3215c7d 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit diff --git a/interp/genarg.ml b/interp/genarg.ml index 310420aa..dd75bbfc 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* raise Not_found - | sce :: scopes -> - let sc,sco = match sce with - | Scope sc -> sc, Some sc - | SingleNotation _ -> default_scope, None in - try - let (pat,df) = find sc in - pat,(df,sco) - with Not_found -> - find_interpretation find scopes + | Scope scope :: scopes -> + (try let (pat,df) = find scope in pat,(df,Some scope) + with Not_found -> find_interpretation ntn find scopes) + | SingleNotation ntn'::scopes when ntn' = ntn -> + (try let (pat,df) = find default_scope in pat,(df,None) + with Not_found -> + (* e.g. because single notation only for constr, not cases_pattern *) + find_interpretation ntn find scopes) + | SingleNotation _::scopes -> + find_interpretation ntn find scopes let find_notation ntn sc = Gmap.find ntn (find_scope sc).notations @@ -361,7 +362,8 @@ let find_prim_token g loc p sc = let interp_prim_token_gen g loc p local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation (find_prim_token g loc p) scopes + let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in + try find_interpretation p_as_ntn (find_prim_token g loc p) scopes with Not_found -> user_err_loc (loc,"interp_prim_token", (match p with @@ -376,7 +378,7 @@ let interp_prim_token_cases_pattern loc p name = let rec interp_notation loc ntn local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation (find_notation ntn) scopes + try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err_loc (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) diff --git a/interp/notation.mli b/interp/notation.mli index 72b576eb..33ffe7b4 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match_ alp metas sigma c1 c2 + | RSort (_,RType _), ASort (RType None) -> sigma | RSort (_,s1), ASort s2 when s1 = s2 -> sigma | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match | a, AHole _ -> sigma diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 5e49d2ea..ce9de27b 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*