diff options
| author | herbelin | 2000-01-26 15:01:55 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-26 15:01:55 +0000 |
| commit | daf4ef5bb4138eb2ab9b7bf39d1c6a08984b8c01 (patch) | |
| tree | 08b8482a9e974697f961993d039e7274ea1e1d99 | |
| parent | 40183da6b54d8deef242bac074079617d4a657c2 (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.ml | 10 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 8 | ||||
| -rw-r--r-- | kernel/sign.ml | 11 | ||||
| -rw-r--r-- | kernel/sign.mli | 15 | ||||
| -rw-r--r-- | kernel/typeops.ml | 35 | ||||
| -rw-r--r-- | lib/util.mli | 3 | ||||
| -rw-r--r-- | parsing/pretty.ml | 3 | ||||
| -rw-r--r-- | parsing/printer.ml | 2 | ||||
| -rw-r--r-- | pretyping/cases.ml | 10 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 29 | ||||
| -rw-r--r-- | proofs/logic.ml | 30 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 18 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | tactics/auto.ml | 26 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 12 |
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 |
