aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2000-01-26 15:01:55 +0000
committerherbelin2000-01-26 15:01:55 +0000
commitdaf4ef5bb4138eb2ab9b7bf39d1c6a08984b8c01 (patch)
tree08b8482a9e974697f961993d039e7274ea1e1d99
parent40183da6b54d8deef242bac074079617d4a657c2 (diff)
Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--kernel/environ.ml10
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--kernel/sign.ml11
-rw-r--r--kernel/sign.mli15
-rw-r--r--kernel/typeops.ml35
-rw-r--r--lib/util.mli3
-rw-r--r--parsing/pretty.ml3
-rw-r--r--parsing/printer.ml2
-rw-r--r--pretyping/cases.ml10
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarutil.ml29
-rw-r--r--proofs/logic.ml30
-rw-r--r--proofs/proof_trees.ml4
-rw-r--r--proofs/refiner.ml18
-rw-r--r--proofs/tacmach.ml5
-rw-r--r--tactics/auto.ml26
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml12
18 files changed, 117 insertions, 108 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7507be838a..0ef449ff42 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -33,7 +33,7 @@ type env = {
env_universes : universes }
let empty_env = {
- env_context = ENVIRON (([],[]),[]);
+ env_context = ENVIRON (nil_sign,nil_dbsign);
env_globals = {
env_constants = Spmap.empty;
env_inductives = Spmap.empty;
@@ -61,12 +61,8 @@ let change_hyps f env =
* if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
* then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
*)
-let change_name_rel env j id =
- let ENVIRON(sign,db) = context env in
- (match list_chop (j-1) db with
- db1,((_,ty)::db2) ->
- {env with env_context = ENVIRON(sign,db1@(Name id,ty)::db2)}
- | _ -> assert false)
+let change_name_rel env j id =
+ { env with env_context = change_name_env (context env) j id }
(****)
let push_rel idrel env =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b2c5df74f6..be489e047a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -439,11 +439,11 @@ let pop_vars idl env =
if n = 0 then
sign
else
- match sign with
- | (id::ids,_::tys) ->
+ if isnull_sign sign then anomaly "pop_vars"
+ else
+ let (id,_) = hd_sign sign in
if not (List.mem id idl) then anomaly "pop_vars";
- remove (pred n) (ids,tys)
- | _ -> anomaly "pop_vars"
+ remove (pred n) (tl_sign sign)
in
change_hyps (remove (List.length idl)) env
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 0b34c7edf3..00a160ffd6 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -53,6 +53,7 @@ let list_of_sign (ids,tys) =
try List.combine ids tys
with _ -> anomaly "Corrupted signature"
+
let make_sign = List.split
let do_sign f (ids,tys) = List.iter2 f ids tys
@@ -163,6 +164,9 @@ let dbindv sign cl =
and sign' = tl_sign sign in
(ty,DLAMV(Name id,Array.map (subst_var id) cl))
+(* de Bruijn environments *)
+
+let nil_dbsign = []
(* Signatures + de Bruijn environments *)
@@ -220,6 +224,13 @@ let map_var_env f (ENVIRON((dom,rang),r)) =
(fun na x (doml,rangl) -> (na::doml,(f x)::rangl))
dom rang ([],[]),r)
+let number_of_rels (ENVIRON(_,db)) = List.length db
+
+let change_name_env (ENVIRON(sign,db)) j id =
+ match list_chop (j-1) db with
+ | db1,((_,ty)::db2) -> ENVIRON(sign,db1@(Name id,ty)::db2)
+ | _ -> raise Not_found
+
let unitize_env env = map_rel_env (fun _ -> ()) env
type ('b,'a) search_result =
diff --git a/kernel/sign.mli b/kernel/sign.mli
index e2ef7d4a1e..1970285895 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
(* Signatures of named variables. *)
-type 'a signature = identifier list * 'a list
+type 'a signature
val nil_sign : 'a signature
val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
@@ -23,6 +23,7 @@ val tl_sign : 'a signature -> 'a signature
val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
val concat_sign : 'a signature -> 'a signature -> 'a signature
+
val ids_of_sign : 'a signature -> identifier list
val vals_of_sign : 'a signature -> 'a list
@@ -64,6 +65,7 @@ val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
val lookup_rel : int -> ('b,'a) sign -> (name * 'a)
val mem_glob : identifier -> ('b,'a) sign -> bool
+val nil_dbsign : 'a db_signature
val get_globals : ('b,'a) sign -> 'b signature
val get_rels : ('b,'a) sign -> 'a db_signature
val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
@@ -73,6 +75,11 @@ val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
val isnull_rel_env : ('a,'b) sign -> bool
val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
val ids_of_env : ('a, 'b) sign -> identifier list
+val number_of_rels : ('b,'a) sign -> int
+
+(*i This is for Cases i*)
+(* raise Not_found if the integer is out of range *)
+val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
type ('b,'a) search_result =
| GLOBNAME of identifier * 'b
@@ -87,3 +94,9 @@ type var_context = typed_type signature
val unitize_env : 'a assumptions -> unit assumptions
+
+
+
+
+
+
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4b20f3b0a9..1feb20e82c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -51,25 +51,22 @@ let relative env n =
(* Checks if a context of variable is included in another one. *)
-let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) =
- let rec aux = function
- | ([], [], _, _) -> true
- | (_, _, [], []) -> false
- | ((id1::idl1), (ty1::tyl1), idl2, tyl2) ->
- let rec search = function
- | ([], []) -> false
- | ((id2::idl2), (ty2::tyl2)) ->
- if id1 = id2 then
- (is_conv env sigma (body_of_type ty1) (body_of_type ty2))
- & aux (idl1,tyl1,idl2,tyl2)
- else
- search (idl2,tyl2)
- | (_, _) -> invalid_arg "hyps_inclusion"
- in
- search (idl2,tyl2)
- | (_, _, _, _) -> invalid_arg "hyps_inclusion"
- in
- aux (idl1,tyl1,idl2,tyl2)
+let rec hyps_inclusion env sigma sign1 sign2 =
+ if isnull_sign sign1 then true
+ else
+ let (id1,ty1) = hd_sign sign1 in
+ let rec search sign2 =
+ if isnull_sign sign2 then false
+ else
+ let (id2,ty2) = hd_sign sign2 in
+ if id1 = id2 then
+ (is_conv env sigma (body_of_type ty1) (body_of_type ty2))
+ &
+ hyps_inclusion env sigma (tl_sign sign1) (tl_sign sign2)
+ else
+ search (tl_sign sign2)
+ in
+ search sign2
(* Checks if the given context of variables [hyps] is included in the
current context of [env]. *)
diff --git a/lib/util.mli b/lib/util.mli
index 77c87d33fc..847842865d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -127,6 +127,9 @@ val in_some : 'a -> 'a option
val out_some : 'a option -> 'a
val option_app : ('a -> 'b) -> 'a option -> 'b option
+(* In [map_succeed f l] an element [a] is removed if [f a] raises *)
+(* [Failure _] otherwise behaves as [List.map f l] *)
+
val map_succeed : ('a -> 'b) -> 'a list -> 'b list
(*s Pretty-printing. *)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 2fc7063373..86f5981feb 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -95,7 +95,8 @@ let print_env pk =
prec (gLOB nil_sign)
let assumptions_for_print lna =
- ENVIRON(([],[]),List.map (fun na -> (na,())) lna)
+ List.fold_right (fun na env -> add_rel (na,()) env) lna
+ (ENVIRON(nil_sign,nil_dbsign))
let print_constructors_with_sep pk fsep mip =
let pterm,pterminenv =
diff --git a/parsing/printer.ml b/parsing/printer.ml
index c93fdbb480..3083154e60 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -176,7 +176,7 @@ let pr_env k env =
[< sign_env; db_env >]
let pr_ne_env header k = function
- | ENVIRON (([],[]),[]) -> [< >]
+ | ENVIRON (sign,_) as env when isnull_sign sign & isnull_rel_env env -> [< >]
| env -> let penv = pr_env k env in [< header; penv >]
let pr_env_limit n env =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3b27a32b38..b44077234d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -75,16 +75,6 @@ let rec map_append_vect f v =
-(* behaves as lam_and_popl but receives an environment instead of a
- * dbenvironment
- *)
-let elam_and_popl n env body =
- let ENVIRON(sign,dbenv)=env in
- let ndbenv,a,l = lam_and_popl n dbenv body []
- in ENVIRON(sign,ndbenv),a
-
-
-
(* behaves as lam_and_popl_named but receives an environment instead of a
* dbenvironment
*)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d4dd1da18f..60b16fc9ff 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -311,7 +311,7 @@ let rec detype avoid env t =
| Name id -> RRef (dummy_loc, RVar id)
| Anonymous -> anomaly "detype: index to an anonymous variable"
with Not_found ->
- let s = "[REL "^(string_of_int (n - List.length (get_rels env)))^"]"
+ let s = "[REL "^(string_of_int (number_of_rels env - n))^"]"
in RRef (dummy_loc, RVar (id_of_string s)))
| IsMeta n -> RRef (dummy_loc,RMeta n)
| IsVar id -> RRef (dummy_loc,RVar id)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2f07574127..11e759aee1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -201,23 +201,22 @@ let real_clean isevars sp args rhs =
(* [new_isevar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
+let append_rels_to_vars ctxt =
+ dbenv_it
+ (fun na t (subst,sign) ->
+ let na = if na = Anonymous then Name(id_of_string"_") else na in
+ let id = next_name_away na (ids_of_sign sign) in
+ ((VAR id)::subst, add_sign (id,typed_app (substl subst) t) sign))
+ ctxt ([],get_globals ctxt)
+
let new_isevar isevars env typ k =
- let (ENVIRON(sign,dbenv)) = context env in
- let t =
- List.fold_left (fun b (na,d)-> mkLambda na (incast_type d) b) typ dbenv in
- let rec aux sign = function
- | (0, t) -> (sign,t)
- | (n, DOP2(Lambda,d,(DLAM(na,b)))) ->
- let na = if na = Anonymous then Name(id_of_string"_") else na in
- let id = next_name_away na (ids_of_sign sign) in
- aux (add_sign (id,(outcast_type d)) sign) (n-1, subst1 (VAR id) b)
- | (_, _) -> anomaly "Trad.new_isevar"
- in
- let (sign',typ') = aux sign (List.length dbenv, t) in
- let env' = change_hyps (fun _ -> sign') env in
+ let ctxt = context env in
+ let subst,sign = append_rels_to_vars ctxt in
+ let typ' = substl subst typ in
+ let env' = change_hyps (fun _ -> sign) env in
let newargs =
- (List.rev(rel_list 0 (List.length dbenv)))
- @(List.map (fun id -> VAR id) (ids_of_sign sign)) in
+ (List.rev(rel_list 0 (number_of_rels ctxt)))
+ @(List.map (fun id -> VAR id) (ids_of_sign (get_globals ctxt))) in
let (sigma',evar) =
new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
isevars := sigma';
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 353472f019..668d16b305 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -155,10 +155,9 @@ let new_meta_variables =
let mk_assumption env sigma c = execute_type env sigma c
let sign_before id =
- let rec aux = function
- | [],[] -> error "no such hypothesis"
- | sign ->
- if fst(hd_sign sign) = id then tl_sign sign else aux (tl_sign sign)
+ let rec aux sign =
+ if isnull_sign sign then error "no such hypothesis";
+ if fst (hd_sign sign) = id then tl_sign sign else aux (tl_sign sign)
in
aux
@@ -373,18 +372,17 @@ let prim_refiner r sigma goal =
error "convert-hyp rule passed non-converting term"
| { name = Thin; hypspecs = ids } ->
- let rec remove_pair s = function
- | ([],[]) ->
- error ((string_of_id s) ^ " is not among the assumptions.")
- | sign ->
- let (s',ty),tlsign = uncons_sign sign in
- if s = s' then
- tlsign
- else if occur_var s ty.body then
- error ((string_of_id s) ^ " is used in the hypothesis "
- ^ (string_of_id s'))
- else
- add_sign (s',ty) (remove_pair s tlsign)
+ let rec remove_pair s sign =
+ if isnull_sign sign then
+ error ((string_of_id s) ^ " is not among the assumptions.");
+ let (s',ty),tlsign = uncons_sign sign in
+ if s = s' then
+ tlsign
+ else if occur_var s ty.body then
+ error ((string_of_id s) ^ " is used in the hypothesis "
+ ^ (string_of_id s'))
+ else
+ add_sign (s',ty) (remove_pair s tlsign)
in
let clear_aux sign s =
if occur_var s cl then
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index ffb88d104c..a02ee4faef 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -313,8 +313,8 @@ let pr_seq evd =
| Some i -> i
| None -> anomaly "pr_seq : info = None"
in
- let (x,y) as hyps = var_context env in
- let sign = List.rev(List.combine x y) in
+ let hyps = var_context env in
+ let sign = List.rev (list_of_sign hyps) in
let pc = pr_ctxt info in
let pdcl =
prlist_with_sep pr_spc
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c4cab5b6b9..3c8e390584 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -260,8 +260,7 @@ let extract_open_proof sign pf =
| {ref=Some(Local_constraints lc,[pf])} -> (proof_extractor vl) pf
| {ref=None;goal=goal} ->
- let rel_env = get_rels vl in
- let n_rels = List.length rel_env in
+ let n_rels = number_of_rels vl in
let visible_rels =
map_succeed
(fun id ->
@@ -811,14 +810,13 @@ let pr_rule = function
| Context ctxt -> pr_ctxt ctxt
| Local_constraints lc -> [< 'sTR"Local constraint change" >]
-let thin_sign osign (x,y) =
- let com_nsign = List.combine x y in
- List.split
- (map_succeed (fun (id,ty) ->
- if (not (mem_sign osign id))
- or (id,ty) <> (lookup_sign id osign) then
- (id,ty)
- else failwith "caught") com_nsign)
+let thin_sign osign sign =
+ sign_it
+ (fun id ty nsign ->
+ if (not (mem_sign osign id))
+ or (id,ty) <> (lookup_sign id osign) (* Hum, egalité sur les types *)
+ then add_sign (id,ty) nsign
+ else nsign) sign nil_sign
let rec print_proof sigma osign pf =
let {evar_env=env; evar_concl=cl;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 446d70b437..5a7c105947 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -45,9 +45,8 @@ let pf_hyps gls = var_context (sig_it gls).evar_env
let pf_concl gls = (sig_it gls).evar_concl
let pf_untyped_hyps gls =
- let env = pf_env gls in
- let (idl,tyl) = Environ.var_context env in
- (idl, List.map (fun x -> x.body) tyl)
+ let sign = Environ.var_context (pf_env gls) in
+ map_sign_typ (fun x -> x.body) sign
let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 02d76010cc..15e9069dda 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -590,8 +590,10 @@ let unify_resolve (c,clenv) gls =
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_untyped_hyps <some goal> *)
-let make_local_hint_db (lid, ltyp) =
- let hintlist = list_map_append2 make_resolve_hyp lid ltyp in
+let make_local_hint_db sign =
+ let hintlist =
+ list_map_append2 make_resolve_hyp
+ (ids_of_sign sign) (vals_of_sign sign) in
Hint_db.add_list hintlist Hint_db.empty
@@ -711,19 +713,19 @@ let decomp_empty_term c gls =
(* n is the max depth of search *)
(* local_db contains the local Hypotheses *)
-let rec search_gen decomp n db_list local_db add_sign goal =
+let rec search_gen decomp n db_list local_db extra_sign goal =
if n=0 then error "BOUND 2";
let decomp_tacs = match decomp with
| 0 -> []
| p ->
- (tclTRY_sign decomp_empty_term add_sign)
+ (tclTRY_sign decomp_empty_term extra_sign)
::
(List.map
(fun id -> tclTHEN (decomp_unary_term (VAR id))
(tclTHEN
(clear_one id)
(search_gen decomp p db_list local_db nil_sign)))
- (fst (pf_untyped_hyps goal)))
+ (ids_of_sign (pf_hyps goal)))
in
let intro_tac =
tclTHEN intro
@@ -736,7 +738,8 @@ let rec search_gen decomp n db_list local_db add_sign goal =
with Failure _ -> []
in
search_gen decomp n db_list
- (Hint_db.add_list hintl local_db) ([hid],[htyp]) g')
+ (Hint_db.add_list hintl local_db)
+ (add_sign (hid,htyp) nil_sign) g')
in
let rec_tacs =
List.map
@@ -854,7 +857,7 @@ let compileAutoArg contac = function
contac)
else
tclFAIL)
- (fst ctx) (snd ctx)) g)
+ (ids_of_sign ctx) (vals_of_sign ctx)) g)
| UsingTDB ->
(tclTHEN
(Tacticals.tryAllClauses
@@ -887,10 +890,11 @@ let rec super_search n db_list local_db argl goal =
(super_search (n-1) db_list local_db argl) argl))) goal
let search_superauto n ids argl g =
- let sigma =
- ids,
- (List.map (fun id -> pf_type_of g (pf_global g id)) ids) in
- let hyps = (concat_sign (pf_untyped_hyps g) sigma) in
+ let sigma =
+ List.fold_right
+ (fun id -> add_sign (id,pf_type_of g (pf_global g id)))
+ ids nil_sign in
+ let hyps = concat_sign (pf_untyped_hyps g) sigma in
super_search n [Stringmap.find "core" !searchtable] (make_local_hint_db hyps)
argl g
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 891f411a18..7b4a9b2cf9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -67,7 +67,7 @@ let tclTRY_sign (tac:constr->tactic) sign gl =
| [s] -> tac (VAR(s)) (* added in order to get useful error messages *)
| (s::sl) -> tclORELSE (tac (VAR(s))) (arec sl)
in
- arec (fst sign) gl
+ arec (ids_of_sign sign) gl
let tclTRY_HYPS (tac:constr->tactic) gl =
tclTRY_sign tac (pf_untyped_hyps gl) gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4791209298..1997f09bba 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -729,12 +729,12 @@ let dyn_exact cc gl = match cc with
let (assumption:tactic) = fun gl ->
let concl = pf_concl gl in
- let rec arec = function
- | ([],[]) -> error "No such assumption"
- | (s::sl,a::al) -> if pf_conv_x_leq gl a concl then
- refine (VAR(s)) gl else arec (sl,al)
- | _ -> assert false
- in
+ let rec arec sign =
+ if isnull_sign sign then error "No such assumption";
+ let (s,a) = hd_sign sign in
+ if pf_conv_x_leq gl a concl then refine (VAR(s)) gl
+ else arec (tl_sign sign)
+ in
arec (pf_untyped_hyps gl)
let dyn_assumption = function