diff options
-rw-r--r-- | .depend | 57 | ||||
-rw-r--r-- | Makefile | 18 | ||||
-rw-r--r-- | contrib/ring/ring.ml | 4 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 2 | ||||
-rw-r--r-- | dev/top_printers.ml | 2 | ||||
-rw-r--r-- | kernel/closure.ml | 1488 | ||||
-rw-r--r-- | kernel/closure.mli | 149 | ||||
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/esubst.ml | 111 | ||||
-rw-r--r-- | kernel/esubst.mli | 34 | ||||
-rw-r--r-- | kernel/inductive.ml | 8 | ||||
-rw-r--r-- | kernel/inductive.mli | 5 | ||||
-rw-r--r-- | kernel/reduction.ml | 16 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
-rw-r--r-- | kernel/term.ml | 151 | ||||
-rw-r--r-- | kernel/term.mli | 102 | ||||
-rw-r--r-- | kernel/typeops.ml | 4 | ||||
-rw-r--r-- | pretyping/cbv.ml | 396 | ||||
-rw-r--r-- | pretyping/cbv.mli | 55 | ||||
-rw-r--r-- | pretyping/detyping.ml | 3 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
-rw-r--r-- | pretyping/pattern.ml | 3 | ||||
-rw-r--r-- | pretyping/retyping.ml | 1 | ||||
-rw-r--r-- | pretyping/tacred.ml | 3 | ||||
-rw-r--r-- | pretyping/typing.ml | 2 | ||||
-rw-r--r-- | tactics/refine.ml | 3 |
26 files changed, 1350 insertions, 1275 deletions
@@ -1,11 +1,12 @@ -kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ - lib/pp.cmi kernel/term.cmi +kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ + kernel/names.cmi lib/pp.cmi kernel/term.cmi kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi +kernel/esubst.cmi: lib/util.cmi kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi @@ -78,6 +79,8 @@ parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ kernel/inductive.cmi kernel/names.cmi pretyping/rawterm.cmi \ kernel/term.cmi +pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \ + kernel/evd.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ library/libobject.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ @@ -224,10 +227,10 @@ dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx lib/system.cmx \ proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx kernel/univ.cmx \ toplevel/vernacentries.cmx toplevel/vernacinterp.cmx -kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \ +kernel/closure.cmo: kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ kernel/univ.cmi lib/util.cmi kernel/closure.cmi -kernel/closure.cmx: kernel/declarations.cmx kernel/environ.cmx kernel/evd.cmx \ +kernel/closure.cmx: kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ kernel/univ.cmx lib/util.cmx kernel/closure.cmi kernel/cooking.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \ @@ -246,6 +249,8 @@ kernel/environ.cmo: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \ kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx lib/pp.cmx \ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ kernel/environ.cmi +kernel/esubst.cmo: lib/util.cmi kernel/esubst.cmi +kernel/esubst.cmx: lib/util.cmx kernel/esubst.cmi kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \ kernel/evd.cmi kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \ @@ -275,13 +280,13 @@ kernel/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi kernel/reduction.cmo: kernel/closure.cmi kernel/declarations.cmi \ - kernel/environ.cmi kernel/evd.cmi kernel/instantiate.cmi kernel/names.cmi \ - lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ - kernel/reduction.cmi + kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ + kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/reduction.cmi kernel/reduction.cmx: kernel/closure.cmx kernel/declarations.cmx \ - kernel/environ.cmx kernel/evd.cmx kernel/instantiate.cmx kernel/names.cmx \ - lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ - kernel/reduction.cmi + kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \ + kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/reduction.cmi kernel/safe_typing.cmo: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/evd.cmi kernel/indtypes.cmi \ kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ @@ -298,10 +303,10 @@ kernel/sign.cmo: kernel/names.cmi lib/options.cmi kernel/term.cmi \ lib/util.cmi kernel/sign.cmi kernel/sign.cmx: kernel/names.cmx lib/options.cmx kernel/term.cmx \ lib/util.cmx kernel/sign.cmi -kernel/term.cmo: lib/hashcons.cmi kernel/names.cmi lib/pp.cmi kernel/univ.cmi \ - lib/util.cmi kernel/term.cmi -kernel/term.cmx: lib/hashcons.cmx kernel/names.cmx lib/pp.cmx kernel/univ.cmx \ - lib/util.cmx kernel/term.cmi +kernel/term.cmo: kernel/esubst.cmi lib/hashcons.cmi kernel/names.cmi \ + lib/pp.cmi kernel/univ.cmi lib/util.cmi kernel/term.cmi +kernel/term.cmx: kernel/esubst.cmx lib/hashcons.cmx kernel/names.cmx \ + lib/pp.cmx kernel/univ.cmx lib/util.cmx kernel/term.cmi kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ kernel/type_errors.cmi @@ -582,6 +587,14 @@ pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \ pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ pretyping/cases.cmi +pretyping/cbv.cmo: kernel/closure.cmi kernel/declarations.cmi \ + kernel/environ.cmi kernel/esubst.cmi kernel/evd.cmi \ + kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi pretyping/cbv.cmi +pretyping/cbv.cmx: kernel/closure.cmx kernel/declarations.cmx \ + kernel/environ.cmx kernel/esubst.cmx kernel/evd.cmx \ + kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ library/global.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \ lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi pretyping/retyping.cmi \ @@ -686,14 +699,14 @@ pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \ pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \ kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx \ library/summary.cmx pretyping/syntax_def.cmi -pretyping/tacred.cmo: kernel/closure.cmi library/declare.cmi \ - kernel/environ.cmi kernel/inductive.cmi kernel/instantiate.cmi \ - kernel/names.cmi lib/pp.cmi kernel/reduction.cmi library/summary.cmi \ - kernel/term.cmi lib/util.cmi pretyping/tacred.cmi -pretyping/tacred.cmx: kernel/closure.cmx library/declare.cmx \ - kernel/environ.cmx kernel/inductive.cmx kernel/instantiate.cmx \ - kernel/names.cmx lib/pp.cmx kernel/reduction.cmx library/summary.cmx \ - kernel/term.cmx lib/util.cmx pretyping/tacred.cmi +pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \ + library/declare.cmi kernel/environ.cmi kernel/inductive.cmi \ + kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ + library/summary.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi +pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \ + library/declare.cmx kernel/environ.cmx kernel/inductive.cmx \ + kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \ + library/summary.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi @@ -35,8 +35,8 @@ LOCALINCLUDES= -I config -I tools -I scripts -I lib -I kernel -I library \ -I contrib/extraction INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB) -BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) -OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) +BYTEFLAGS=-rectypes $(INCLUDES) $(CAMLDEBUG) +OPTFLAGS=-rectypes $(INCLUDES) $(CAMLTIMEPROF) OCAMLDEP=ocamldep DEPFLAGS=$(LOCALINCLUDES) @@ -67,12 +67,12 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo -KERNEL=kernel/names.cmo kernel/univ.cmo kernel/term.cmo \ +KERNEL=kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo \ kernel/sign.cmo kernel/declarations.cmo \ kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \ - kernel/closure.cmo kernel/reduction.cmo kernel/inductive.cmo\ - kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ - kernel/cooking.cmo kernel/safe_typing.cmo + kernel/closure.cmo kernel/reduction.cmo \ + kernel/inductive.cmo kernel/type_errors.cmo kernel/typeops.cmo \ + kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \ library/lib.cmo library/goptions.cmo \ @@ -80,7 +80,7 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/nametab.cmo \ library/impargs.cmo library/indrec.cmo library/declare.cmo PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \ - pretyping/retyping.cmo pretyping/tacred.cmo \ + pretyping/retyping.cmo pretyping/cbv.cmo pretyping/tacred.cmo \ pretyping/pretype_errors.cmo pretyping/typing.cmo \ pretyping/classops.cmo pretyping/recordops.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ @@ -155,11 +155,11 @@ COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) world: $(COQBINARIES) states theories contrib tools $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) - $(COQMKTOP) -opt $(OPTFLAGS) -o $@ + $(COQMKTOP) -opt $(INCLUDES) $(CAMLDEBUG) -o $@ $(STRIP) $@ $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) - $(COQMKTOP) -top $(BYTEFLAGS) -o $@ + $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ # coqmktop diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 7b3b8f6f6..1cfbf965c 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -217,7 +217,7 @@ let _ = (constr_of amult) (constr_of aone) (constr_of azero) - (mkXtra "not a term") + mkImplicit (constr_of aeq) (constr_of t) (cset_of_comarg_list l))) @@ -253,7 +253,7 @@ let _ = (constr_of amult) (constr_of aone) (constr_of azero) - (mkXtra "not a term") + mkImplicit (constr_of aeq) (constr_of t) ConstrSet.empty)) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 4d4b05d78..0f55481c3 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -485,8 +485,6 @@ let print_term inner_types l env csr = (Array.mapi (fun j x -> (x,t.(j),b.(j)) ) (Array.of_list f) ) [<>] >] ) - | T.IsXtra _ -> - Util.anomaly "Xtra node in a term!!!" | T.IsEvar _ -> Util.anomaly "Evar node in a term!!!" in diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 95c85866d..7cb08e06b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -82,7 +82,6 @@ let constr_display csr = | IsMeta n -> "Meta("^(string_of_int n)^")" | IsVar id -> "Var("^(string_of_id id)^")" | IsSort s -> "Sort("^(sort_display s)^")" - | IsXtra s -> "Xtra("^s^")" | IsCast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")" | IsProd (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" @@ -145,7 +144,6 @@ let print_pure_constr csr = | IsMeta n -> print_string "Meta("; print_int n; print_string ")" | IsVar id -> print_string (string_of_id id) | IsSort s -> sort_display s - | IsXtra s -> print_string ("Xtra("^s^")") | IsCast (c,t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() diff --git a/kernel/closure.ml b/kernel/closure.ml index d6e4589ca..7762b18bb 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -9,6 +9,8 @@ open Environ open Instantiate open Univ open Evd +open Esubst + let stats = ref false let share = ref true @@ -29,6 +31,15 @@ let stop() = 'sTR" zeta="; 'iNT !zeta; 'sTR" evar="; 'iNT !evar; 'sTR" iota="; 'iNT !iota; 'sTR" prune="; 'iNT !prune; 'sTR"]" >] +let with_stats c = + if !stats then begin + reset(); + let r = Lazy.force c in + stop(); + r + end else + Lazy.force c + type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of section_path @@ -152,7 +163,7 @@ let red_set red = function let c = List.mem sp l in incr_cnt ((b & not c) or (c & not b)) delta | VAR id -> (* En attendant d'avoir des sp pour les Var *) - let (b,_,l) = red.r_const in + let (b,_,l) = red.r_const in let c = List.mem id l in incr_cnt ((b & not c) or (c & not b)) delta | ZETA -> incr_cnt red.r_zeta zeta @@ -213,59 +224,6 @@ let red_under (md,r) rk = | WITHBACK -> true | _ -> red_set r rk -(* (bounded) explicit substitutions of type 'a *) -type 'a subs = - | ESID of int (* ESID(n) = %n END bounded identity *) - | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) - | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) - (* with n vars *) - | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) - -(* operations of subs: collapses constructors when possible. - * Needn't be recursive if we always use these functions - *) - -let subs_cons(x,s) = CONS(x,s) - -let subs_liftn n = function - | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) - | LIFT (p,lenv) -> LIFT (p+n, lenv) - | lenv -> LIFT (n,lenv) - -let subs_lift a = subs_liftn 1 a - -let subs_shft = function - | (0, s) -> s - | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) - | (n, s) -> SHIFT (n,s) - -(* Expands de Bruijn k in the explicit substitution subs - * lams accumulates de shifts to perform when retrieving the i-th value - * the rules used are the following: - * - * [id]k --> k - * [S.t]1 --> t - * [S.t]k --> [S](k-1) if k > 1 - * [^n o S] k --> [^n]([S]k) - * [(%n S)] k --> k if k <= n - * [(%n S)] k --> [^n]([S](k-n)) - * - * the result is (Inr (k+lams,p)) when the variable is just relocated - * where p is None if the variable points insider subs and Some(k) if the - * variable points k bindings beyond subs. - *) -let rec exp_rel lams k subs = - match (k,subs) with - | (1, CONS (def,_)) -> Inl(lams,def) - | (_, CONS (_,l)) -> exp_rel lams (pred k) l - | (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None) - | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l - | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s - | (_, ESID n) when k<=n -> Inr(lams+k,None) - | (_, ESID n) -> Inr(lams+k,Some (k-n)) - -let expand_rel k subs = exp_rel 0 k subs - (* Flags of reduction and cache of constants: 'a is a type that may be * mapped to constr. 'a infos implements a cache for constants and * abstractions, storing a representation (of type 'a) of the body of @@ -302,6 +260,8 @@ type ('a, 'b) infos = { i_vars : (identifier * constr) list; i_tab : ('a table_key, 'a) Hashtbl.t } +let info_flags info = info.i_flags + let ref_value_cache info ref = try Some (Hashtbl.find info.i_tab ref) @@ -344,383 +304,9 @@ let defined_rels flags env = env (0,[]) (* else (0,[])*) -let infos_under infos = { infos with i_flags = flags_under infos.i_flags } - - -(**** Call by value reduction ****) - -(* The type of terms with closure. The meaning of the constructors and - * the invariants of this datatype are the following: - * VAL(k,c) represents the constr c with a delayed shift of k. c must be - * in normal form and neutral (i.e. not a lambda, a construct or a - * (co)fix, because they may produce redexes by applying them, - * or putting them in a case) - * LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated - * only when the abstraction is applied, and then we use the rule - * ([S]([x:a]b) c) --> [S.c]b - * This corresponds to the usual strategy of weak reduction - * FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under - * the substitution S, and then applied to args. Here again, - * weak reduction. - * CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th - * inductive type sp. - * - * Note that any term has not an equivalent in cbv_value: for example, - * a product (x:A)B must be in normal form because only VAL may - * represent it, and the argument of VAL is always in normal - * form. This remark precludes coding a head reduction with these - * functions. Anyway, does it make sense to head reduce with a - * call-by-value strategy ? - *) -type cbv_value = - | VAL of int * constr - | LAM of name * constr * constr * cbv_value subs - | FIXP of fixpoint * cbv_value subs * cbv_value list - | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of int * inductive_path * cbv_value array * cbv_value list - -(* les vars pourraient etre des constr, - cela permet de retarder les lift: utile ?? *) - -(* relocation of a value; used when a value stored in a context is expanded - * in a larger context. e.g. [%k (S.t)](k+1) --> [^k]t (t is shifted of k) - *) -let rec shift_value n = function - | VAL (k,v) -> VAL ((k+n),v) - | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s)) - | FIXP (fix,s,args) -> - FIXP (fix,subs_shft (n,s), List.map (shift_value n) args) - | COFIXP (cofix,s,args) -> - COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args) - | CONSTR (i,spi,vars,args) -> - CONSTR (i, spi, Array.map (shift_value n) vars, - List.map (shift_value n) args) - - -(* Contracts a fixpoint: given a fixpoint and a substitution, - * returns the corresponding fixpoint body, and the substitution in which - * it should be evaluated: its first variables are the fixpoint bodies - * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) - * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) - *) -let contract_fixp env ((reci,i),(_,_,bds as bodies)) = - let make_body j = FIXP(((reci,j),bodies), env, []) in - let n = Array.length bds in - let rec subst_bodies_from_i i subs = - if i=n then subs - else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) - in - subst_bodies_from_i 0 env, bds.(i) - -let contract_cofixp env (i,(_,_,bds as bodies)) = - let make_body j = COFIXP((j,bodies), env, []) in - let n = Array.length bds in - let rec subst_bodies_from_i i subs = - if i=n then subs - else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) - in - subst_bodies_from_i 0 env, bds.(i) - - -(* type of terms with a hole. This hole can appear only under App or Case. - * TOP means the term is considered without context - * APP(l,stk) means the term is applied to l, and then we have the context st - * this corresponds to the application stack of the KAM. - * The members of l are values: we evaluate arguments before the function. - * CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk - * t is the type of the case and br are the branches, all of them under - * the subs S, pat is information on the patterns of the Case - * (Weak reduction: we propagate the sub only when the selected branch - * is determined) - * - * Important remark: the APPs should be collapsed: - * (APP (l,(APP ...))) forbidden - *) - -type cbv_stack = - | TOP - | APP of cbv_value list * cbv_stack - | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - -(* Adds an application list. Collapse APPs! *) -let stack_app appl stack = - match (appl, stack) with - | ([], _) -> stack - | (_, APP(args,stk)) -> APP(appl@args,stk) - | _ -> APP(appl, stack) - -(* Tests if we are in a case (modulo some applications) *) -let under_case_stack = function - | (CASE _ | APP(_,CASE _)) -> true - | _ -> false - -(* Tells if the reduction rk is allowed by flags under a given stack. - * The stack is useful when flags is (SIMPL,r) because in that case, - * we perform bdi-reduction under the Case, or r-reduction otherwise - *) -let red_allowed flags stack rk = - if under_case_stack stack then - red_under flags rk - else - red_top flags rk - -let red_allowed_ref flags stack = function - | FarRelBinding _ -> red_allowed flags stack DELTA - | VarBinding id -> red_allowed flags stack (VAR id) - | EvarBinding _ -> red_allowed flags stack EVAR - | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp]) - -(* Transfer application lists from a value to the stack - * useful because fixpoints may be totally applied in several times - *) -let strip_appl head stack = - match head with - | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack) - | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack) - | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack) - | _ -> (head, stack) - - -(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last - * argument is []. - * Because we must put all the applied terms in the stack. - *) -let reduce_const_body redfun v stk = - if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk - - -(* Tests if fixpoint reduction is possible. A reduction function is given as - argument *) -let rec check_app_constr redfun = function - | ([], _) -> false - | ((CONSTR _)::_, 0) -> true - | (t::_, 0) -> (* TODO: partager ce calcul *) - (match redfun t with - | CONSTR _ -> true - | _ -> false) - | (_::l, n) -> check_app_constr redfun (l,(pred n)) - -let fixp_reducible redfun flgs ((reci,i),_) stk = - if red_allowed flgs stk IOTA then - match stk with (* !!! for Acc_rec: reci.(i) = -2 *) - | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i)) - | _ -> false - else - false - -let cofixp_reducible redfun flgs _ stk = - if red_allowed flgs stk IOTA then - match stk with - | (CASE _ | APP(_,CASE _)) -> true - | _ -> false - else - false - -let mindsp_nparams env (sp,i) = - let mib = lookup_mind sp env in - (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams - -(* The main recursive functions - * - * Go under applications and cases (pushed in the stack), expand head - * constants or substitued de Bruijn, and try to make appear a - * constructor, a lambda or a fixp in the head. If not, it is a value - * and is completely computed here. The head redexes are NOT reduced: - * the function returns the pair of a cbv_value and its stack. * - * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last - * argument is []. Because we must put all the applied terms in the - * stack. *) - -let rec norm_head info env t stack = - (* no reduction under binders *) - match kind_of_term t with - (* stack grows (remove casts) *) - | IsApp (head,args) -> (* Applied terms are normalized immediately; - they could be computed when getting out of the stack *) - let nargs = Array.map (cbv_stack_term info TOP env) args in - norm_head info env head (stack_app (Array.to_list nargs) stack) - | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) - | IsCast (ct,_) -> norm_head info env ct stack - - (* constants, axioms - * the first pattern is CRUCIAL, n=0 happens very often: - * when reducing closed terms, n is always 0 *) - | IsRel i -> (match expand_rel i env with - | Inl (0,v) -> - reduce_const_body (cbv_norm_more info env) v stack - | Inl (n,v) -> - reduce_const_body - (cbv_norm_more info env) (shift_value n v) stack - | Inr (n,None) -> - (VAL(0, mkRel n), stack) - | Inr (n,Some p) -> - norm_head_ref (n-p) info env stack (FarRelBinding p)) - - | IsVar id -> norm_head_ref 0 info env stack (VarBinding id) - - | IsConst (sp,vars) -> - let normt = (sp,Array.map (cbv_norm_term info env) vars) in - norm_head_ref 0 info env stack (ConstBinding normt) - - | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env)) - - | IsLetIn (x, b, t, c) -> - (* zeta means letin are contracted; delta without zeta means we *) - (* allow substitution but leave let's in place *) - let zeta = red_allowed info.i_flags stack ZETA in - let env' = - if zeta or red_allowed info.i_flags stack DELTA then - subs_cons (cbv_stack_term info TOP env b,env) - else - subs_lift env in - if zeta then - norm_head info env' c stack - else - let normt = - mkLetIn (x, cbv_norm_term info env b, - cbv_norm_term info env t, - cbv_norm_term info env' c) in - (VAL(0,normt), stack) (* Considérer une coupure commutative ? *) - - (* non-neutral cases *) - | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack) - | IsFix fix -> (FIXP(fix,env,[]), stack) - | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack) - | IsMutConstruct ((spi,i),vars) -> - (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack) - - (* neutral cases *) - | (IsSort _ | IsMeta _ | IsXtra _ ) -> (VAL(0, t), stack) - | IsMutInd (sp,vars) -> - (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack) - | IsProd (x,t,c) -> - (VAL(0, mkProd (x, cbv_norm_term info env t, - cbv_norm_term info (subs_lift env) c)), - stack) - -and norm_head_ref k info env stack normt = - if red_allowed_ref info.i_flags stack normt then - match ref_value_cache info normt with - | Some body -> - reduce_const_body (cbv_norm_more info env) (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k info normt), stack) - else (VAL(0,make_constr_ref k info normt), stack) - -and make_constr_ref n info = function - | FarRelBinding p -> mkRel (n+p) - | VarBinding id -> mkVar id - | EvarBinding ((ev,args),env) -> - mkEvar (ev,Array.map (cbv_norm_term info env) args) - | ConstBinding cst -> mkConst cst - -(* cbv_stack_term performs weak reduction on constr t under the subs - * env, with context stack, i.e. ([env]t stack). First computes weak - * head normal form of t and checks if a redex appears with the stack. - * If so, recursive call to reach the real head normal form. If not, - * we build a value. - *) -and cbv_stack_term info stack env t = - match norm_head info env t stack with - (* a lambda meets an application -> BETA *) - | (LAM (x,a,b,env), APP (arg::args, stk)) - when red_allowed info.i_flags stk BETA -> - let subs = subs_cons (arg,env) in - cbv_stack_term info (stack_app args stk) subs b - - (* a Fix applied enough -> IOTA *) - | (FIXP(fix,env,_), stk) - when fixp_reducible (cbv_norm_more info env) info.i_flags fix stk -> - let (envf,redfix) = contract_fixp env fix in - cbv_stack_term info stk envf redfix - - (* constructor guard satisfied or Cofix in a Case -> IOTA *) - | (COFIXP(cofix,env,_), stk) - when cofixp_reducible (cbv_norm_more info env) info.i_flags cofix stk-> - let (envf,redfix) = contract_cofixp env cofix in - cbv_stack_term info stk envf redfix - - (* constructor in a Case -> IOTA - (use red_under because we know there is a Case) *) - | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,_,env,stk))) - when red_under info.i_flags IOTA -> - let nparams = mindsp_nparams info.i_env sp in - let real_args = snd (list_chop nparams args) in - cbv_stack_term info (stack_app real_args stk) env br.(n-1) - - (* constructor of arity 0 in a Case -> IOTA ( " " )*) - | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk)) - when red_under info.i_flags IOTA -> - cbv_stack_term info stk env br.(n-1) - - (* may be reduced later by application *) - | (head, TOP) -> head - | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) - | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) - | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl) - - (* definitely a value *) - | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk) - - -(* if we are in SIMPL mode, maybe v isn't reduced enough *) -and cbv_norm_more info env v = - match (v, info.i_flags) with - | (VAL(k,t), ((SIMPL|WITHBACK),_)) -> - cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t - | _ -> v - - -(* When we are sure t will never produce a redex with its stack, we - * normalize (even under binders) the applied terms and we build the - * final term - *) -and apply_stack info t = function - | TOP -> t - | APP (args,st) -> - apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st - | CASE (ty,br,ci,env,st) -> - apply_stack info - (mkMutCase (ci, cbv_norm_term info env ty, t, - Array.map (cbv_norm_term info env) br)) - st - - -(* performs the reduction on a constr, and returns a constr *) -and cbv_norm_term info env t = - (* reduction under binders *) - cbv_norm_value info (cbv_stack_term info TOP env t) - -(* reduction of a cbv_value to a constr *) -and cbv_norm_value info = function (* reduction under binders *) - | VAL (n,v) -> lift n v - | LAM (x,a,b,env) -> - mkLambda (x, cbv_norm_term info env a, - cbv_norm_term info (subs_lift env) b) - | FIXP ((lij,(lty,lna,bds)),env,args) -> - applistc - (mkFix (lij, - (Array.map (cbv_norm_term info env) lty, lna, - Array.map (cbv_norm_term info - (subs_liftn (Array.length lty) env)) bds))) - (List.map (cbv_norm_value info) args) - | COFIXP ((j,(lty,lna,bds)),env,args) -> - applistc - (mkCoFix (j, - (Array.map (cbv_norm_term info env) lty, lna, - Array.map (cbv_norm_term info - (subs_liftn (Array.length lty) env)) bds))) - (List.map (cbv_norm_value info) args) - | CONSTR (n,spi,vars,args) -> - applistc - (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars)) - (List.map (cbv_norm_value info) args) - -type 'a cbv_infos = (cbv_value, 'a) infos - -(* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs env sigma = +let create mk_cl flgs env sigma = { i_flags = flgs; - i_repr = (fun old_info s c -> cbv_stack_term old_info TOP s c); + i_repr = mk_cl; i_env = env; i_evc = sigma; i_rels = defined_rels flgs env; @@ -728,633 +314,619 @@ let create_cbv_infos flgs env sigma = i_tab = Hashtbl.create 17 } -(* with profiling *) -let cbv_norm infos constr = - let repr_fun = cbv_stack_term infos TOP in - if !stats then begin - reset(); - let r= cbv_norm_term infos (ESID 0) constr in - stop(); - r - end else - cbv_norm_term infos (ESID 0) constr - +let infos_under infos = { infos with i_flags = flags_under infos.i_flags } -(**** End of call by value ****) (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) -type 'a stack = - | EmptyStack - | ConsStack of 'a array * int * 'a stack +type 'a stack_member = + | Zapp of 'a array * int + | Zcase of case_info * 'a * 'a array + | Zfix of 'a * 'a stack + | Zshift of int + | Zupdate of 'a -let empty_stack = EmptyStack +and 'a stack = 'a stack_member list -let decomp_stack = function - | EmptyStack -> None - | ConsStack (v, n, s) -> - Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s))) +let empty_stack = [] -let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s) +let append_stackn v p s = if Array.length v = p then s else Zapp(v,p)::s +let append_stack v s = append_stackn v 0 s -let rec app_stack = function - | f, EmptyStack -> f - | f, ConsStack (v, n, s) -> - let args = if n=0 then v else Array.sub v n (Array.length v - n) in - app_stack (appvect (f, args), s) +(* Collapse the shifts in the stack *) +let zshift n s = + match (n,s) with + (0,_) -> s + | (_,Zshift(k)::s) -> Zshift(n+k)::s + | _ -> Zshift(n)::s + +let rec stack_args_size = function + | Zapp(v,n)::s -> Array.length v - n + stack_args_size s + | Zshift(_)::s -> stack_args_size s + | Zupdate(_)::s -> stack_args_size s + | _ -> 0 + +(* Parameterization: check the a given reduction is allowed in the + context of the stack *) +let can_red info stk r = + red_top info.i_flags r || + (fst info.i_flags = SIMPL && + List.exists (function (Zcase _|Zfix _) -> true | _ -> false) stk) -let rec list_of_stack = function - | EmptyStack -> [] - | ConsStack (v, n, s) -> - let args = if n=0 then v else Array.sub v n (Array.length v - n) in - Array.fold_right (fun a l -> a::l) args (list_of_stack s) +(* When used as an argument stack (only Zapp can appear) *) +let decomp_stack = function + | Zapp(v,n)::s -> Some (v.(n), append_stackn v (n+1) s) + | [] -> None + | _ -> assert false +let decomp_stackn = function + | Zapp(v,n)::s -> + ((if n = 0 then v else Array.sub v n (Array.length v - n)), s) + | _ -> assert false let array_of_stack s = let rec stackrec = function - | EmptyStack -> [] - | ConsStack (v, n, s) -> - let args = if n=0 then v else Array.sub v n (Array.length v - n) in + | [] -> [] + | stk -> + let (args,s) = decomp_stackn stk in args :: (stackrec s) in Array.concat (stackrec s) - +let rec list_of_stack = function + | [] -> [] + | stk -> + let (args,s) = decomp_stackn stk in + Array.fold_right (fun a l -> a::l) args (list_of_stack s) +let rec app_stack = function + | f, [] -> f + | f, stk -> + let (args,s) = decomp_stackn stk in + app_stack (appvect (f, args), s) let rec stack_assign s p c = match s with - | EmptyStack -> EmptyStack - | ConsStack (v, n, s) -> + | Zapp(v,n)::s -> let q = Array.length v - n in if p >= q then - ConsStack (v, n, stack_assign s (p-q) c) + Zapp (v, n) :: stack_assign s (p-q) c else let v' = Array.sub v n q in v'.(p) <- c; - ConsStack (v', 0, s) - + Zapp (v',0) :: s + | _ -> s let rec stack_tail p s = if p = 0 then s else match s with - | EmptyStack -> failwith "stack_shop" - | ConsStack (v, n, s) -> + | Zapp (v, n) :: s -> let q = Array.length v - n in if p >= q then stack_tail (p-q) s - else ConsStack (v, n+p, s) - + else Zapp (v, n+p) :: s + | _ -> failwith "stack_tail" let rec stack_nth s p = match s with - | EmptyStack -> raise Not_found - | ConsStack (v, n, s) -> + | Zapp (v, n) :: s -> let q = Array.length v - n in if p >= q then stack_nth s (p-q) else v.(p+n) + | _ -> raise Not_found -let rec stack_args_size = function - | EmptyStack -> 0 - | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s +(**********************************************************************) +(* Lazy reduction: the one used in kernel operations *) -(* Version avec listes -type stack = constr list - -let decomp_stack = function - | [] -> None - | v :: s -> Some (v,s) - -let append_stack v s = v@s -*) - -(* Lazy reduction: the one used in kernel operations *) - -(* type of shared terms. freeze and frterm are mutually recursive. +(* type of shared terms. fconstr and frterm are mutually recursive. * Clone of the Generic.term structure, but completely mutable, and * annotated with booleans (true when we noticed that the term is * normal and neutral) FLIFT is a delayed shift; allows sharing - * between 2 lifted copies of a given term FFROZEN is a delayed + * between 2 lifted copies of a given term FCLOS is a delayed * substitution applied to a constr *) +type red_state = Norm | Cstr | Whnf | Red -type freeze = { - mutable norm: bool; - mutable term: frterm } +type fconstr = { + mutable norm: red_state; + mutable term: fterm } -and frterm = +and fterm = | FRel of int | FAtom of constr - | FCast of freeze * freeze - | FFlex of frreference - | FInd of inductive_path * freeze array - | FConstruct of constructor_path * freeze array - | FApp of freeze * freeze array - | FFix of (int array * int) * (freeze array * name list * freeze array) - * constr array * freeze subs - | FCoFix of int * (freeze array * name list * freeze array) - * constr array * freeze subs - | FCases of case_info * freeze * freeze * freeze array - | FLambda of name * freeze * freeze * constr * freeze subs - | FProd of name * freeze * freeze * constr * freeze subs - | FLetIn of name * freeze * freeze * freeze * constr * freeze subs - | FLIFT of int * freeze - | FFROZEN of constr * freeze subs - -and frreference = + | FCast of fconstr * fconstr + | FFlex of freference + | FInd of inductive_path * fconstr array + | FConstruct of constructor_path * fconstr array + | FApp of fconstr * fconstr array + | FFix of (int array * int) * (fconstr array * name list * fconstr array) + * constr array * fconstr subs + | FCoFix of int * (fconstr array * name list * fconstr array) + * constr array * fconstr subs + | FCases of case_info * fconstr * fconstr * fconstr array + | FLambda of name * fconstr * fconstr * constr * fconstr subs + | FProd of name * fconstr * fconstr * constr * fconstr subs + | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs + | FLIFT of int * fconstr + | FCLOS of constr * fconstr subs + +and freference = (* only vars as args of FConst ... exploited for caching *) - | FConst of section_path * freeze array - | FEvar of (existential * freeze subs) + | FConst of section_path * fconstr array + | FEvar of (existential * fconstr subs) | FVar of identifier | FFarRel of int (* index in the rel_context part of _initial_ environment *) -let reloc_flex r el = r - -let frterm_of v = v.term -let is_val v = v.norm - -(* Copies v2 in v1 and returns v1. The only side effect is here! The - * invariant of the reduction functions is that the interpretation of - * v2 as a constr (e.g term_of_freeze below) is a reduct of the - * interpretation of v1. - * - * The implementation without side effect, but losing sharing, - * simply returns v2. *) - -let freeze_assign v1 v2 = - if !share then begin - v1.norm <- v2.norm; - v1.term <- v2.term; - v1 - end else - v2 - -(* lift a freeze and yields a frterm. No loss of sharing: the - * resulting term takes advantage of any reduction performed in v. - * i.e.: if (lift_frterm n v) yields w, reductions in w are reported - * in w.term (yes: w.term, not only in w) The lifts are collapsed, - * because we often insert lifts of 0. *) - -let rec lift_frterm n v = - match v.term with - | FLIFT (k,f) -> lift_frterm (k+n) f - | FAtom _ as ft -> { norm = true; term = ft } - (* gene: closed terms *) - | _ -> { norm = v.norm; term = FLIFT (n,v) } - - -(* lift a freeze, keep sharing, but spare records when possible (case - * n=0 ... ) The difference with lift_frterm is that reductions in v - * are reported only in w, and not necessarily in w.term (with - * notations above). *) -let lift_freeze n v = - match (n, v.term) with - | (0, _) | (_, FAtom _ ) -> v (* identity lift or closed term *) - | _ -> lift_frterm n v - - -let freeze env t = { norm = false; term = FFROZEN (t,env) } -let freeze_vect env v = Array.map (freeze env) v -let freeze_list env l = List.map (freeze env) l - -let freeze_rec env (tys,lna,bds) = - let env' = subs_liftn (Array.length bds) env in - (Array.map (freeze env) tys, lna, Array.map (freeze env') bds) - - -(* pourrait peut-etre remplacer freeze ?! (et alors FFROZEN - * deviendrait inutile) *) -(* traverse_term : freeze subs -> constr -> freeze *) -let rec traverse_term env t = +let fterm_of v = v.term +let set_whnf v = if v.norm = Red then v.norm <- Whnf +let set_cstr v = if v.norm = Red then v.norm <- Cstr +let set_norm v = v.norm <- Norm +let is_val v = v.norm = Norm + +(* Put an update mark in the stack, only if needed *) +let zupdate m s = + if !share & m.norm = Red then Zupdate(m)::s else s + +(* Could issue a warning if no is still Red, pointing out that we loose + sharing. *) +let update v1 (no,t) = + if !share then + (v1.norm <- no; + v1.term <- t; + v1) + else {norm=no;term=t} + +let rec lft_fconstr n ft = + match ft.term with + FLIFT(k,m) -> lft_fconstr (n+k) m + | _ -> {norm=ft.norm; term=FLIFT(n,ft)} +let lift_fconstr k f = + if k=0 then f else lft_fconstr k f +let lift_fconstr_vect k v = + if k=0 then v else Array.map (fun f -> lft_fconstr k f) v + +let clos_rel e i = + match expand_rel i e with + | Inl(n,mt) -> lift_fconstr n mt + | Inr(k,None) -> {norm=Norm; term= FRel k} + | Inr(k,Some p) -> + lift_fconstr (k-p) {norm=Norm;term=FFlex(FFarRel p)} + +(* Optimization: do not enclose variables in a closure. + Makes variable access much faster *) +let mk_clos e t = match kind_of_term t with - | IsRel i -> (match expand_rel i env with - | Inl (lams,v) -> (lift_frterm lams v) - | Inr (k,None) -> { norm = true; term = FRel k } - | Inr (k,Some p) -> - lift_frterm (k-p) - { norm = false; term = FFlex (FFarRel p) }) - | IsVar x -> { norm = false; term = FFlex (FVar x) } - | IsMeta _ | IsSort _ | IsXtra _ -> { norm = true; term = FAtom t } + | IsRel i -> clos_rel e i + | IsVar x -> { norm = Norm; term = FFlex (FVar x) } + | IsMeta _ | IsSort _ -> { norm = Norm; term = FAtom t } + | (IsMutInd _|IsMutConstruct _|IsFix _|IsCoFix _ + |IsLambda _|IsProd _) -> + {norm = Cstr; term = FCLOS(t,e)} + | (IsApp _|IsMutCase _|IsCast _|IsConst _|IsEvar _|IsLetIn _) -> + {norm = Red; term = FCLOS(t,e)} + +let mk_clos_vect env v = Array.map (mk_clos env) v + +(* Translate the head constructor of t from constr to fconstr. This + function is parameterized by the function to apply on the direct + subterms. + Could be used insted of mk_clos. *) +let mk_clos_deep clos_fun env t = + match kind_of_term t with + | IsRel i -> clos_rel env i + | (IsVar _|IsMeta _ | IsSort _) -> mk_clos env t | IsCast (a,b) -> - { norm = false; - term = FCast (traverse_term env a, traverse_term env b)} + { norm = Red; + term = FCast (clos_fun env a, clos_fun env b)} | IsApp (f,v) -> - { norm = false; - term = FApp (traverse_term env f, Array.map (traverse_term env) v) } + { norm = Red; + term = FApp (clos_fun env f, Array.map (clos_fun env) v) } | IsMutInd (sp,v) -> - { norm = false; term = FInd (sp, Array.map (traverse_term env) v) } + { norm = Cstr; term = FInd (sp, Array.map (clos_fun env) v) } | IsMutConstruct (sp,v) -> - { norm = false; term = FConstruct (sp,Array.map (traverse_term env) v)} + { norm = Cstr; term = FConstruct (sp,Array.map (clos_fun env) v)} | IsConst (sp,v) -> - { norm = false; - term = FFlex (FConst (sp,Array.map (traverse_term env) v)) } + { norm = Red; + term = FFlex (FConst (sp,Array.map (clos_fun env) v)) } | IsEvar (_,v as ev) -> - assert (array_for_all (fun a -> isVar a or isRel a) v); - { norm = false; + { norm = Red; term = FFlex (FEvar (ev, env)) } | IsMutCase (ci,p,c,v) -> - { norm = false; - term = FCases (ci, traverse_term env p, traverse_term env c, - Array.map (traverse_term env) v) } + { norm = Red; + term = FCases (ci, clos_fun env p, clos_fun env c, + Array.map (clos_fun env) v) } | IsFix (op,(tys,lna,bds)) -> let env' = subs_liftn (Array.length bds) env in - { norm = false; - term = FFix (op, (Array.map (traverse_term env) tys, lna, - Array.map (traverse_term env') bds), + { norm = Cstr; + term = FFix (op, (Array.map (clos_fun env) tys, lna, + Array.map (clos_fun env') bds), bds, env) } | IsCoFix (op,(tys,lna,bds)) -> let env' = subs_liftn (Array.length bds) env in - { norm = false; - term = FCoFix (op, (Array.map (traverse_term env) tys, lna, - Array.map (traverse_term env') bds), + { norm = Cstr; + term = FCoFix (op, (Array.map (clos_fun env) tys, lna, + Array.map (clos_fun env') bds), bds, env) } | IsLambda (n,t,c) -> - { norm = false; - term = FLambda (n, traverse_term env t, - traverse_term (subs_lift env) c, + { norm = Cstr; + term = FLambda (n, clos_fun env t, + clos_fun (subs_lift env) c, c, env) } | IsProd (n,t,c) -> - { norm = false; - term = FProd (n, traverse_term env t, - traverse_term (subs_lift env) c, + { norm = Cstr; + term = FProd (n, clos_fun env t, + clos_fun (subs_lift env) c, c, env) } | IsLetIn (n,b,t,c) -> - { norm = false; - term = FLetIn (n, traverse_term env b, traverse_term env t, - traverse_term (subs_lift env) c, + { norm = Red; + term = FLetIn (n, clos_fun env b, clos_fun env t, + clos_fun (subs_lift env) c, c, env) } -(* Back to regular terms: remove all FFROZEN, keep casts (since this - * fun is not dedicated to the Calculus of Constructions). - *) -let rec lift_term_of_freeze lfts v = +(* The inverse of mk_clos_deep: move back to constr *) +let rec to_constr constr_fun lfts v = match v.term with - | FRel i -> mkRel (reloc_rel i lfts) - | FFlex (FVar x) -> mkVar x - | FFlex (FFarRel p) -> mkRel (reloc_rel p lfts) - | FAtom c -> c - | FCast (a,b) -> - mkCast (lift_term_of_freeze lfts a, lift_term_of_freeze lfts b) - | FFlex (FConst (op, ve)) -> - mkConst (op, Array.map (lift_term_of_freeze lfts) ve) - | FFlex (FEvar ((n,args), env)) -> - let f a = lift_term_of_freeze lfts (traverse_term env a) in - mkEvar (n, Array.map f args) - | FInd (op, ve) -> - mkMutInd (op, Array.map (lift_term_of_freeze lfts) ve) - | FConstruct (op, ve) -> - mkMutConstruct (op, Array.map (lift_term_of_freeze lfts) ve) - | FCases (ci, p, c, ve) -> - mkMutCase (ci, lift_term_of_freeze lfts p, - lift_term_of_freeze lfts c, - Array.map (lift_term_of_freeze lfts) ve) - | FFix (op,(tys,lna,bds),_,_) -> - let lfts' = el_liftn (Array.length bds) lfts in - mkFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna, - Array.map (lift_term_of_freeze lfts') bds)) - | FCoFix (op,(tys,lna,bds),_,_) -> - let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna, - Array.map (lift_term_of_freeze lfts') bds)) - | FApp (f,ve) -> - mkApp (lift_term_of_freeze lfts f, - Array.map (lift_term_of_freeze lfts) ve) - | FLambda (n,t,c,_,_) -> - mkLambda (n, lift_term_of_freeze lfts t, - lift_term_of_freeze (el_lift lfts) c) - | FProd (n,t,c,_,_) -> - mkProd (n, lift_term_of_freeze lfts t, - lift_term_of_freeze (el_lift lfts) c) - | FLetIn (n,b,t,c,_,_) -> - mkLetIn (n, lift_term_of_freeze lfts b, - lift_term_of_freeze lfts t, - lift_term_of_freeze (el_lift lfts) c) - | FLIFT (k,a) -> lift_term_of_freeze (el_shft k lfts) a - | FFROZEN (t,env) -> - let unfv = freeze_assign v (traverse_term env t) in - lift_term_of_freeze lfts unfv - - -(* This function defines the correspondance between constr and freeze *) -let term_of_freeze v = lift_term_of_freeze ELID v -let applist_of_freeze appl = Array.to_list (Array.map term_of_freeze appl) - - -(* fstrong applies unfreeze_fun recursively on the (freeze) term and - * yields a term. Assumes that the unfreeze_fun never returns a - * FFROZEN term. - *) -let rec fstrong unfreeze_fun lfts v = - match (unfreeze_fun v).term with - | FRel i -> mkRel (reloc_rel i lfts) - | FFlex (FFarRel p) -> mkRel (reloc_rel p lfts) - | FFlex (FVar x) -> mkVar x - | FAtom c -> c + | FRel i -> IsRel (reloc_rel i lfts) + | FFlex (FFarRel p) -> IsRel (reloc_rel p lfts) + | FFlex (FVar x) -> IsVar x + | FAtom c -> + (match kind_of_term c with + | IsSort s -> IsSort s + | IsMeta m -> IsMeta m + | _ -> assert false) | FCast (a,b) -> - mkCast (fstrong unfreeze_fun lfts a, fstrong unfreeze_fun lfts b) + IsCast (constr_fun lfts a, constr_fun lfts b) | FFlex (FConst (op,ve)) -> - mkConst (op, Array.map (fstrong unfreeze_fun lfts) ve) + IsConst (op, Array.map (constr_fun lfts) ve) | FFlex (FEvar ((n,args),env)) -> - let f a = fstrong unfreeze_fun lfts (freeze env a) in - mkEvar (n, Array.map f args) + let f a = constr_fun lfts (mk_clos env a) in + IsEvar (n, Array.map f args) | FInd (op,ve) -> - mkMutInd (op, Array.map (fstrong unfreeze_fun lfts) ve) + IsMutInd (op, Array.map (constr_fun lfts) ve) | FConstruct (op,ve) -> - mkMutConstruct (op, Array.map (fstrong unfreeze_fun lfts) ve) + IsMutConstruct (op, Array.map (constr_fun lfts) ve) | FCases (ci,p,c,ve) -> - mkMutCase (ci, fstrong unfreeze_fun lfts p, - fstrong unfreeze_fun lfts c, - Array.map (fstrong unfreeze_fun lfts) ve) + IsMutCase (ci, constr_fun lfts p, + constr_fun lfts c, + Array.map (constr_fun lfts) ve) | FFix (op,(tys,lna,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna, - Array.map (fstrong unfreeze_fun lfts') bds)) + IsFix (op, (Array.map (constr_fun lfts) tys, lna, + Array.map (constr_fun lfts') bds)) | FCoFix (op,(tys,lna,bds),_,_) -> let lfts' = el_liftn (Array.length bds) lfts in - mkCoFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna, - Array.map (fstrong unfreeze_fun lfts') bds)) + IsCoFix (op, (Array.map (constr_fun lfts) tys, lna, + Array.map (constr_fun lfts') bds)) | FApp (f,ve) -> - mkApp (fstrong unfreeze_fun lfts f, - Array.map (fstrong unfreeze_fun lfts) ve) + IsApp (constr_fun lfts f, + Array.map (constr_fun lfts) ve) | FLambda (n,t,c,_,_) -> - mkLambda (n, fstrong unfreeze_fun lfts t, - fstrong unfreeze_fun (el_lift lfts) c) + IsLambda (n, constr_fun lfts t, + constr_fun (el_lift lfts) c) | FProd (n,t,c,_,_) -> - mkProd (n, fstrong unfreeze_fun lfts t, - fstrong unfreeze_fun (el_lift lfts) c) + IsProd (n, constr_fun lfts t, + constr_fun (el_lift lfts) c) | FLetIn (n,b,t,c,_,_) -> - mkLetIn (n, fstrong unfreeze_fun lfts b, - fstrong unfreeze_fun lfts t, - fstrong unfreeze_fun (el_lift lfts) c) - | FLIFT (k,a) -> fstrong unfreeze_fun (el_shft k lfts) a - | FFROZEN _ -> anomaly "Closure.fstrong" - - -(* Build a freeze, which represents the substitution of arg in t - * Used to constract a beta-redex: - * [^depth](FLamda(S,t)) arg -> [(^depth o S).arg]t - *) -let rec contract_subst depth t subs arg = - freeze (subs_cons (arg, subs_shft (depth,subs))) t - + IsLetIn (n, constr_fun lfts b, + constr_fun lfts t, + constr_fun (el_lift lfts) c) + | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a + | FCLOS (t,env) -> + let fr = mk_clos_deep mk_clos env t in + let unfv = update v (fr.norm,fr.term) in + to_constr constr_fun lfts unfv + +(* This function defines the correspondance between constr and + fconstr. When we find a closure whose substitution is the identity, + then we directly return the constr to avoid possibly huge + reallocation. *) +let term_of_fconstr = + let rec term_of_fconstr_lift lfts v = + match v.term with + | FCLOS(t,env) when is_subs_id env & is_lift_id lfts -> t + | _ -> mk_constr (to_constr term_of_fconstr_lift lfts v) in + term_of_fconstr_lift ELID -(* Calculus of Constructions *) -type fconstr = freeze - -(* Remove head lifts, applications and casts *) -let rec strip_frterm n v stack = - match v.term with - | FLIFT (k,f) -> strip_frterm (k+n) f stack - | FApp (f,args) -> - strip_frterm n f - (append_stack (Array.map (lift_freeze n) args) stack) - | FCast (f,_) -> (strip_frterm n f stack) - | _ -> (n, v, stack) - -let strip_freeze v = strip_frterm 0 v empty_stack +(* fstrong applies unfreeze_fun recursively on the (freeze) term and + * yields a term. Assumes that the unfreeze_fun never returns a + * FCLOS term. +let rec fstrong unfreeze_fun lfts v = + to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) +*) -(* Same as contract_fixp, but producing a freeze *) +(* TODO: the norm flags are not handled properly *) +let rec zip zfun m stk = + match stk with + | [] -> m + | Zapp(_)::_ -> + let (args,s) = decomp_stackn stk in + zip zfun {norm=m.norm; term=FApp(m, Array.map zfun args)} s + | Zcase(ci,p,br)::s -> + let t = FCases(ci, zfun p, m, Array.map zfun br) in + zip zfun {norm=m.norm; term=t} s + | Zfix(fx,par)::s -> + zip zfun fx (par @ append_stack [|m|] s) + | Zshift(n)::s -> + zip zfun (lift_fconstr n m) s + | Zupdate(rf)::s -> + zip zfun (update rf (m.norm,m.term)) s + +let fapp_stack (m,stk) = zip (fun x -> x) m stk + +(*********************************************************************) + +(* The assertions in the functions below are granted because they are + called only when m is a constructor, a cofix + (strip_update_shift_app), a fix (get_nth_arg) or an abstraction + (strip_update_shift, through get_arg). *) + +(* optimised for the case where there are no shifts... *) +let strip_update_shift head stk = + assert (head.norm <> Red); + let rec strip_rec h depth = function + | Zshift(k)::s -> strip_rec (lift_fconstr k h) (depth+k) s + | Zupdate(m)::s -> + strip_rec (update m (h.norm,h.term)) depth s + | stk -> (depth,stk) in + strip_rec head 0 stk + +(* optimised for the case where there are no shifts... *) +let strip_update_shift_app head stk = + assert (head.norm <> Red); + let rec strip_rec rstk h depth = function + | Zshift(k) as e :: s -> + strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s + | (Zapp(_)::_) as stk -> + let (args,s) = decomp_stackn stk in + strip_rec (Zapp(args,0)::rstk) + {norm=h.norm;term=FApp(h,args)} depth s + | Zupdate(m)::s -> + strip_rec rstk (update m (h.norm,h.term)) depth s + | stk -> (depth,List.rev rstk, stk) in + strip_rec [] head 0 stk + + +let rec get_nth_arg head n stk = + assert (head.norm <> Red); + let rec strip_rec rstk h depth n = function + | Zshift(k) as e :: s -> + strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s + | Zapp(v, p)::s' -> + let q = Array.length v - p in + if n >= q + then + let v' = if p = 0 then v else Array.sub v p q in + strip_rec (Zapp(v',0)::rstk) + {norm=h.norm;term=FApp(h,v')} depth (n-q) s' + else + let rstk' = + if n = 0 then rstk else Zapp(Array.sub v p n,0)::rstk in + (Some (List.rev rstk', v.(p+n)), append_stackn v (p+n+1) s') + | Zupdate(m)::s -> + strip_rec rstk (update m (h.norm,h.term)) depth n s + | s -> (None, List.rev rstk @ s) in + strip_rec [] head 0 n stk + +(* Beta reduction: look for an applied argument in the stack. + Since the encountered update marks are removed, h must be a whnf *) +let get_arg h stk = + let (depth,stk') = strip_update_shift h stk in + match stk' with + Zapp(v,p)::s -> (Some(depth,v.(p)), append_stackn v (p+1) s) + | _ -> (None, zshift depth stk') + + +(* Iota reduction: extract the arguments to be passed to the Case + branches *) +let rec reloc_rargs_rec depth stk = + match stk with + Zapp(_)::_ -> + let (args,s) = decomp_stackn stk in + Zapp(lift_fconstr_vect depth args,0) :: reloc_rargs_rec depth s + | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s + | _ -> stk + +let reloc_rargs depth stk = + if depth = 0 then stk else reloc_rargs_rec depth stk + +let rec drop_parameters depth n stk = + match stk with + Zapp(v,p)::s -> + let q = Array.length v - p in + if n > q then drop_parameters depth (n-q) s + else if n = q then reloc_rargs depth s + else reloc_rargs depth (Zapp(v,p+n)::s) + | Zshift(k)::s -> drop_parameters (depth-k) n s + | [] -> assert (n=0); [] + | _ -> assert false (* we know that n < stack_args_size(stk) *) + + +(* Iota reduction: expansion of a fixpoint. + * Given a fixpoint and a substitution, returns the corresponding + * fixpoint body, and the substitution in which it should be + * evaluated: its first variables are the fixpoint bodies + * + * FCLOS(fix Fi {F0 := T0 .. Fn-1 := Tn-1}, S) + * -> (S. FCLOS(F0,S) . ... . FCLOS(Fn-1,S), Ti) + *) (* does not deal with FLIFT *) let contract_fix_vect fix = let (thisbody, make_body, env, nfix) = match fix with | FFix ((reci,i),def,bds,env) -> (bds.(i), - (fun j -> { norm = false; term = FFix ((reci,j),def,bds,env) }), + (fun j -> { norm = Whnf; term = FFix ((reci,j),def,bds,env) }), env, Array.length bds) | FCoFix (i,def,bds,env) -> (bds.(i), - (fun j -> { norm = false; term = FCoFix (j,def,bds,env) }), + (fun j -> { norm = Whnf; term = FCoFix (j,def,bds,env) }), env, Array.length bds) | _ -> anomaly "Closure.contract_fix_vect: not a (co)fixpoint" in let rec subst_bodies_from_i i env = if i = nfix then - freeze env thisbody + mk_clos env thisbody else subst_bodies_from_i (i+1) (subs_cons (make_body i, env)) in subst_bodies_from_i 0 env -(* CoFix reductions are context dependent. Therefore, they cannot be shared. *) -let copy_case ci p ft bl = - (* Is the copy of bl necessary ?? I'd guess no HH *) - { norm = false; term = FCases (ci,p,ft,Array.copy bl) } - - -(* Check if the case argument enables iota-reduction *) -type case_status = - | CONSTRUCTOR of int * fconstr stack - | COFIX of int * int * (fconstr array * name list * fconstr array) * - fconstr stack * constr array * freeze subs - | IRREDUCTIBLE - - -let constr_or_cofix env v = - let (lft_hd, head, appl) = strip_freeze v in - match head.term with - | FConstruct ((indsp,i),_) -> - let args = stack_tail (mindsp_nparams env indsp) appl in - CONSTRUCTOR (i, args) - | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env) - | _ -> IRREDUCTIBLE - -let fix_reducible env unf_fun n stack = - if n < stack_args_size stack & n >= 0 (* e.g for Acc_rec: n = -2 *) then - let v = unf_fun (stack_nth stack n) in - match constr_or_cofix env v with - | CONSTRUCTOR _ -> true - | _ -> false - else - false - - -(* unfreeze computes the weak head normal form of v (according to the - * flags in info) and updates the mutable term. - *) -let rec unfreeze info v = - freeze_assign v (whnf_frterm info v) - -(* weak head normal form - * Sharing info: the physical location of the ouput of this function - * doesn't matter (only the values of its fields do). - *) -and whnf_frterm info ft = - if ft.norm then begin - incr prune; ft - end else - match ft.term with - | FFROZEN (t,env) -> whnf_term info env t - | FLIFT (k,f) -> - let uf = unfreeze info f in - { norm = uf.norm; term = FLIFT(k, uf) } - | FCast (f,_) -> whnf_frterm info f (* remove outer casts *) - | FApp (f,appl) -> whnf_apply info f (append_stack appl empty_stack) - | FFlex (FConst (sp,vars)) -> - let cst = (sp, Array.map term_of_freeze vars) in - if red_under info.i_flags (CONST [sp]) then - (match ref_value_cache info (ConstBinding cst) with - | Some def -> - let udef = unfreeze info def in - lift_frterm 0 udef - | None -> - { norm = true (* because only mkVar *); term = ft.term }) - else - ft - | FFlex (FEvar ((_,vars),_ as ev)) -> - if red_under info.i_flags EVAR then - (match ref_value_cache info (EvarBinding ev) with - | Some def -> - let udef = unfreeze info def in - lift_frterm 0 udef - | None -> - { norm = true (* because only mkVar/Rel *);term = ft.term }) - else - ft - | FFlex (FVar id) as t-> - if red_under info.i_flags (VAR id) then - match ref_value_cache info (VarBinding id) with - | Some def -> - let udef = unfreeze info def in - lift_frterm 0 udef - | None -> { norm = true; term = t } - else ft - | FFlex (FFarRel k) as t -> - if red_under info.i_flags DELTA then - match ref_value_cache info (FarRelBinding k) with - | Some def -> - let udef = unfreeze info def in - lift_frterm 0 udef - | None -> { norm = true; term = t } - else ft - - | FCases (ci,p,co,bl) -> - if red_under info.i_flags IOTA then - let c = unfreeze (infos_under info) co in - (match constr_or_cofix info.i_env c with - | CONSTRUCTOR (n,real_args) when n <= Array.length bl -> - whnf_apply info bl.(n-1) real_args - | COFIX (lft_hd,bnum,def,appl,bds,env) -> - let cofix = contract_fix_vect (FCoFix (bnum,def,bds,env)) in - let red_cofix = - whnf_apply info (lift_freeze lft_hd cofix) appl in - whnf_frterm info (copy_case ci p red_cofix bl) - | _ -> - { norm = is_val p & is_val co & array_for_all is_val bl; - term = ft.term }) - else - ft - - | FLetIn (na,b,fd,fc,d,subs) -> - let c = unfreeze info b in - if red_under info.i_flags ZETA then - whnf_frterm info (contract_subst 0 d subs c) - else - { norm = false; - term = FLetIn (na,c,fd,fc,d,subs) } - - | FRel _ | FAtom _ -> { norm = true; term = ft.term } - - | FFix _ | FCoFix _ | FInd _ | FConstruct _ | FLambda _ | FProd _ -> ft - -(* Weak head reduction: case of the application (head appl) *) -and whnf_apply info head stack = - let head = unfreeze info head in - if stack = empty_stack then - head - else - let (lft_hd,whd,lstack) = strip_frterm 0 head stack in - match whd.term with - | FLambda (_,_,_,t,subs) when red_under info.i_flags BETA -> - (match decomp_stack lstack with - | Some (c, stack') -> - let vbody = contract_subst lft_hd t subs c in - whnf_apply info vbody stack' - | None -> assert false) - | FFix ((reci,bnum), _, _, _) as fx - when red_under info.i_flags IOTA - & fix_reducible info.i_env - (unfreeze (infos_under info)) reci.(bnum) lstack -> - let fix = contract_fix_vect fx in - whnf_apply info (lift_freeze lft_hd fix) lstack - | _ -> - let appl = array_of_stack stack in - { norm = (is_val head) & (array_for_all is_val appl); - term = FApp (head, appl) } - -(* essayer whnf_frterm info (traverse_term env t) a la place? - * serait moins lazy: traverse_term ne supprime pas les Cast a la volee, etc. - *) -and whnf_term info env t = +(*********************************************************************) +(* A machine that inspects the head of a term until it finds an + atom or a subterm that may produce a redex (abstraction, + constructor, cofix, letin, constant), or a neutral term (product, + inductive) *) +let rec knh m stk = + if is_val m then (m,stk) else + match m.term with + | FLIFT(k,a) -> knh a (zshift k stk) + | FCLOS(t,e) -> knht e t (Zupdate(m)::stk) + | FApp(a,b) -> knh a (append_stack b (zupdate m stk)) + | FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk) + | FFix((ri,n),_,_,_) -> + (set_whnf m; + match get_nth_arg m ri.(n) stk with + (Some(pars,arg),stk') -> knh arg (Zfix(m,pars)::stk') + | (None, stk') -> (m,stk')) + | FCast(t,_) -> knh t stk +(* cases where knh stops *) + | (FFlex _|FLetIn _) -> (m, stk) + | (FRel _|FAtom _) -> (set_norm m; (m, stk)) + | (FLambda _|FConstruct _|FCoFix _|FInd _|FProd _) -> + (set_whnf m; (m, stk)) + +(* The same for pure terms *) +and knht e t stk = match kind_of_term t with - | IsRel i -> - (match expand_rel i env with - | Inl (lams,v) -> - let uv = unfreeze info v in - lift_frterm lams uv - | Inr (n,None) -> - { norm = true; term = FRel n } - | Inr (n,Some k) -> - whnf_frterm info - (lift_frterm (n-k) { norm = false; term = FFlex(FFarRel k) })) - - | IsVar x -> whnf_frterm info { norm = false; term = FFlex(FVar x) } - - | IsSort _ | IsXtra _ | IsMeta _ -> {norm = true; term = FAtom t } - | IsCast (c,_) -> whnf_term info env c (* remove outer casts *) - - | IsApp (f,ve) -> - whnf_frterm info - { norm = false; term = FApp (freeze env f, freeze_vect env ve)} - | IsConst (op,v) -> - whnf_frterm info - { norm = false; term = FFlex (FConst (op, freeze_vect env v)) } - | IsEvar ev -> - whnf_frterm info { norm = false; term = FFlex (FEvar (ev, env)) } - | IsMutCase (ci,p,c,ve) -> - whnf_frterm info - { norm = false; - term = FCases (ci, freeze env p, freeze env c, freeze_vect env ve)} - - | IsMutInd (op,v) -> - { norm = (v=[||]); term = FInd (op, freeze_vect env v) } - | IsMutConstruct (op,v) -> - { norm = (v=[||]); term = FConstruct (op, freeze_vect env v) } - - | IsFix (op,(_,_,bds as def)) -> - { norm = false; term = FFix (op, freeze_rec env def, bds, env) } - | IsCoFix (op,(_,_,bds as def)) -> - { norm = false; term = FCoFix (op, freeze_rec env def, bds, env) } - - | IsLambda (n,t,c) -> - { norm = false; - term = FLambda (n, freeze env t, freeze (subs_lift env) c, - c, env) } - | IsProd (n,t,c) -> - { norm = false; - term = FProd (n, freeze env t, freeze (subs_lift env) c, - c, env) } - - | IsLetIn (n,b,t,c) -> - whnf_frterm info - { norm = false; - term = FLetIn (n, freeze env b, freeze env t, - freeze (subs_lift env) c, c, env) } + | IsApp(a,b) -> + knht e a (append_stack (mk_clos_vect e b) stk) + | IsMutCase(ci,p,t,br) -> + knht e t (Zcase(ci, mk_clos e p, mk_clos_vect e br)::stk) + | IsFix _ -> knh (mk_clos_deep mk_clos e t) stk + | IsCast(a,b) -> knht e a stk + | IsRel n -> knh (clos_rel e n) stk + | (IsLambda _|IsProd _|IsMutConstruct _|IsCoFix _|IsMutInd _| + IsLetIn _|IsConst _|IsVar _|IsEvar _|IsMeta _|IsSort _) -> + (mk_clos_deep mk_clos e t, stk) + + +(***********************************************************************) + +(* Computes a normal form from the result of knh. *) +let rec knr info m stk = + match m.term with + | FLambda(_,_,_,f,e) when can_red info stk BETA -> + (match get_arg m stk with + (Some(depth,arg),s) -> knit info (subs_shift_cons(depth,e,arg)) f s + | (None,s) -> (m,s)) + | FFlex(FConst(sp,args)) when can_red info stk (CONST [sp]) -> + let cst = (sp, Array.map term_of_fconstr args) in + (match ref_value_cache info (ConstBinding cst) with + Some v -> kni info v stk + | None -> (set_norm m; (m,stk))) + | FFlex(FEvar ev) when can_red info stk EVAR -> +(* In the case of evars, if it is not defined, then we do not set the + flag to Norm, because it may be instantiated later on *) + (match ref_value_cache info (EvarBinding ev) with + Some v -> kni info v stk + | None -> (m,stk)) + | FFlex(FVar id) when can_red info stk (VAR id) -> + (match ref_value_cache info (VarBinding id) with + Some v -> kni info v stk + | None -> (set_norm m; (m,stk))) + | FFlex(FFarRel k) when can_red info stk DELTA -> + (match ref_value_cache info (FarRelBinding k) with + Some v -> kni info v stk + | None -> (set_norm m; (m,stk))) + | FConstruct((sp,c),args) when can_red info stk IOTA -> + (match strip_update_shift_app m stk with + (depth, args, Zcase((cn,_),_,br)::s) -> + let npar = stack_args_size args - cn.(c-1) in + assert (npar>=0); + let rargs = drop_parameters depth npar args in + kni info br.(c-1) (rargs@s) + | (_, cargs, Zfix(fx,par)::s) -> + let rarg = fapp_stack(m,cargs) in + let stk' = par @ append_stack [|rarg|] s in + let efx = contract_fix_vect fx.term in + kni info efx stk' + | (_,args,s) -> (m,args@s)) + | FCoFix _ when can_red info stk IOTA -> + (match strip_update_shift_app m stk with + (_, args, (Zcase((cn,_),_,br)::s as stk')) -> + let efx = contract_fix_vect m.term in + kni info efx (args@s) + | (_,args,s) -> (m,args@s)) + | FLetIn (_,v,_,_,bd,e) when can_red info stk ZETA -> + knit info (subs_cons(v,e)) bd stk + | _ -> (m,stk) + +(* Computes the normal form of a term *) +and kni info m stk = + let (hm,s) = knh m stk in + knr info hm s +and knit info e t stk = + let (ht,s) = knht e t stk in + knr info ht s + +let kh info v stk = fapp_stack(kni info v stk) + +(***********************************************************************) + +(* Computes the strong normal form of a term. + 1- Calls kni + 2- tries to rebuild the term. If a closure still has to be computed, + calls itself recursively. *) +let rec kl info m = + let (nm,s) = kni info m [] in + down_or_up info nm s + +(* no redex: go up for atoms and already normalized terms, go down + otherwise. *) +and down_or_up info m stk = + let nm = + if is_val m then (incr prune; m) else + let nt = + match m.term with + | FLambda(na,ty,bd,f,e) -> + FLambda(na, kl info ty, kl info bd, f, e) + | FLetIn(na,a,b,c,f,e) -> + FLetIn(na, kl info a, kl info b, kl info c, f, e) + | FProd(na,dom,rng,f,e) -> + FProd(na, kl info dom, kl info rng, f, e) + | FInd(ind,args) -> + FInd(ind, Array.map (kl info) args) + | FConstruct(c,args) -> + FConstruct(c, Array.map (kl info) args) + | FCoFix(n,(ftys,na,fbds),bds,e) -> + FCoFix(n,(Array.map (kl info) ftys, na, + Array.map (kl info) fbds),bds,e) + | FFlex(FConst(sp,args)) -> + FFlex(FConst(sp, Array.map (kl info) args)) + | FFlex(FEvar((i,args),e)) -> + FFlex(FEvar((i,args),e)) + | t -> t in + {norm=Norm;term=nt} in +(* Precondition: m.norm = Norm *) + zip (kl info) nm stk + + +(* Initialization and then normalization *) + +(* weak reduction *) +let whd_val info v = + with_stats (lazy (term_of_fconstr (kh info v []))) -(* parameterized norm *) +(* strong reduction *) let norm_val info v = - if !stats then begin - reset(); - let r = fstrong (unfreeze info) ELID v in - stop(); - r - end else - fstrong (unfreeze info) ELID v + with_stats (lazy (term_of_fconstr (kl info v))) -let whd_val info v = - let uv = unfreeze info v in - term_of_freeze uv +let inject = mk_clos (ESID 0) + +(* cache of constants: the body is computed only when needed. *) +type 'a clos_infos = (fconstr, 'a) infos -let inject = freeze (ESID 0) +let create_clos_infos flgs env sigma = + create (fun _ -> mk_clos) flgs env sigma -let search_frozen_value info = function +let unfold_reference info = function | FConst (op,v) -> let cst = (op, Array.map (norm_val info) v) in ref_value_cache info (ConstBinding cst) @@ -1362,26 +934,22 @@ let search_frozen_value info = function | FVar id -> ref_value_cache info (VarBinding id) | FFarRel p -> ref_value_cache info (FarRelBinding p) -(* cache of constants: the body is computed only when needed. *) -type 'a clos_infos = (fconstr, 'a) infos - +(* Head normal form. *) -let create_clos_infos flgs env sigma = - { i_flags = flgs; - i_repr = (fun old_info s c -> freeze s c); - i_env = env; - i_evc = sigma; - i_rels = defined_rels flgs env; - i_vars = defined_vars flgs env; - i_tab = Hashtbl.create 17 } +(* TODO: optimise *) +let rec strip_applstack k acc m = + match m.term with + FApp(a,b) -> + strip_applstack k (append_stack (lift_fconstr_vect k b) acc) a + | FLIFT(n,a) -> + strip_applstack (k+n) acc a + | FCLOS _ -> assert false + | _ -> (k,m,acc) -let clos_infos_env infos = infos.i_env -(* Head normal form. *) let fhnf info v = - let uv = unfreeze info v in - strip_freeze uv + strip_applstack 0 [] (kh info v []) -let fhnf_apply infos k head appl = - let v = whnf_apply infos (lift_freeze k head) appl in - strip_freeze v +let fhnf_apply info k head appl = + let stk = zshift k appl in + strip_applstack 0 [] (kh info head stk) diff --git a/kernel/closure.mli b/kernel/closure.mli index e3476db21..b4001f077 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -7,12 +7,15 @@ open Names open Term open Evd open Environ +open Esubst (*i*) (* Flags for profiling reductions. *) val stats : bool ref val share : bool ref +val with_stats: 'a Lazy.t -> 'a + type evaluable_global_reference = | EvalVarRef of identifier | EvalConstRef of section_path @@ -75,16 +78,23 @@ val betadeltaiota : flags val hnf_flags : flags val unfold_flags : evaluable_global_reference -> flags -(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. - [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = - $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. - [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *) -type 'a subs = - | ESID of int - | CONS of 'a * 'a subs - | SHIFT of int * 'a subs - | LIFT of int * 'a subs +(***********************************************************************) + +type 'a table_key = + | ConstBinding of constant + | EvarBinding of (existential * 'a subs) + | VarBinding of identifier + | FarRelBinding of int +type ('a,'b) infos +val ref_value_cache: ('a,'b) infos -> 'a table_key -> 'a option +val info_flags: ('a,'b) infos -> flags +val infos_under: ('a,'b) infos -> ('a,'b) infos +val create: + (('a,'b) infos -> 'a subs -> constr -> 'a) -> + flags -> env -> 'b evar_map -> ('a,'b) infos + +(***********************************************************************) (*s A [stack] is a context of arguments, arguments are pushed by [append_stack] one array at a time but popped with [decomp_stack] one by one *) @@ -92,6 +102,7 @@ type 'a subs = type 'a stack val empty_stack : 'a stack val append_stack : 'a array -> 'a stack -> 'a stack + val decomp_stack : 'a stack -> ('a * 'a stack) option val list_of_stack : 'a stack -> 'a list val array_of_stack : 'a stack -> 'a array @@ -102,27 +113,20 @@ val stack_tail : int -> 'a stack -> 'a stack val stack_nth : 'a stack -> int -> 'a (***********************************************************************) -(*s Call-by-value reduction *) - -(* Entry point for cbv normalization of a constr *) -type 'a cbv_infos -val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos -val cbv_norm : 'a cbv_infos -> constr -> constr - (*s Lazy reduction. *) (* [fconstr] is the type of frozen constr *) type fconstr -(* [fconstr] can be accessed by using the function [frterm_of] and by - matching on type [frterm] *) +(* [fconstr] can be accessed by using the function [fterm_of] and by + matching on type [fterm] *) -type frterm = +type fterm = | FRel of int | FAtom of constr | FCast of fconstr * fconstr - | FFlex of frreference + | FFlex of freference | FInd of inductive_path * fconstr array | FConstruct of constructor_path * fconstr array | FApp of fconstr * fconstr array @@ -135,26 +139,26 @@ type frterm = | FProd of name * fconstr * fconstr * constr * fconstr subs | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs | FLIFT of int * fconstr - | FFROZEN of constr * fconstr subs + | FCLOS of constr * fconstr subs -and frreference = +and freference = | FConst of section_path * fconstr array | FEvar of (existential * fconstr subs) | FVar of identifier | FFarRel of int -val frterm_of : fconstr -> frterm (* To lazy reduce a constr, create a ['a clos_infos] with [create_cbv_infos], inject the term to reduce with [inject]; then use a reduction function *) +val inject : constr -> fconstr +val fterm_of : fconstr -> fterm +val term_of_fconstr : fconstr -> constr + (* Global and local constant cache *) type 'a clos_infos val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos -val clos_infos_env : 'a clos_infos -> env - -val inject : constr -> fconstr (* Reduction function *) @@ -164,92 +168,35 @@ val norm_val : 'a clos_infos -> fconstr -> constr (* [whd_val] is for weak head normalization *) val whd_val : 'a clos_infos -> fconstr -> constr +(* Conversion auxiliary functions to do step by step normalisation *) + (* [fhnf] and [fnf_apply] are for weak head normalization but staying - in [fcontr] world to perform step by step weak head normalization *) + in [fconstr] world to perform step by step weak head normalization *) val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr stack val fhnf_apply : 'a clos_infos -> int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack -(* [search_frozen_value] unfolds references in a [fconstr] *) -val search_frozen_value : 'a clos_infos -> frreference -> fconstr option - - -(*i This is for cbv debug *) -type cbv_value = - | VAL of int * constr - | LAM of name * constr * constr * cbv_value subs - | FIXP of fixpoint * cbv_value subs * cbv_value list - | COFIXP of cofixpoint * cbv_value subs * cbv_value list - | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list - -val shift_value : int -> cbv_value -> cbv_value - -type cbv_stack = - | TOP - | APP of cbv_value list * cbv_stack - | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - -val stack_app : cbv_value list -> cbv_stack -> cbv_stack -val under_case_stack : cbv_stack -> bool -val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack - -val red_allowed : flags -> cbv_stack -> red_kind -> bool -val reduce_const_body : - (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack - -(* recursive functions... *) -val cbv_stack_term : 'a cbv_infos -> - cbv_stack -> cbv_value subs -> constr -> cbv_value -val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr -val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value -val norm_head : 'a cbv_infos -> - cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack -val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr -val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr -(* End of cbv debug section i*) +(* [unfold_reference] unfolds references in a [fconstr] *) +val unfold_reference : 'a clos_infos -> freference -> fconstr option +(***********************************************************************) (*i This is for lazy debug *) -type freeze = fconstr -val is_val : freeze -> bool -val lift_frterm : int -> freeze -> freeze -val lift_freeze : int -> freeze -> freeze +val lift_fconstr : int -> fconstr -> fconstr +val lift_fconstr_vect : int -> fconstr array -> fconstr array -val freeze : freeze subs -> constr -> freeze -val freeze_vect : freeze subs -> constr array -> freeze array -val freeze_list : freeze subs -> constr list -> freeze list +val mk_clos : fconstr subs -> constr -> fconstr +val mk_clos_vect : fconstr subs -> constr array -> fconstr array +val mk_clos_deep : + (fconstr subs -> constr -> fconstr) -> + fconstr subs -> constr -> fconstr -val traverse_term : freeze subs -> constr -> freeze -val lift_term_of_freeze : lift_spec -> freeze -> constr +val knr: 'a clos_infos -> fconstr -> fconstr stack -> + fconstr * fconstr stack +val kl: 'a clos_infos -> fconstr -> fconstr -(* Back to constr *) -val fstrong : (freeze -> freeze) -> lift_spec -> freeze -> constr -val term_of_freeze : freeze -> constr -val applist_of_freeze : freeze array -> constr list - -(* contract a substitution *) -val contract_subst : int -> constr -> freeze subs -> freeze -> freeze - -val strip_frterm : - int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack -val strip_freeze : fconstr -> int * fconstr * fconstr stack - -(* Auxiliary functions for (co)fixpoint reduction *) -val contract_fix_vect : frterm -> fconstr -val copy_case : case_info -> fconstr -> fconstr -> fconstr array -> fconstr - -(* Iota analysis: reducible ? *) -type case_status = - | CONSTRUCTOR of int * fconstr stack - | COFIX of int * int * (fconstr array * name list * fconstr array) * - fconstr stack * constr array * freeze subs - | IRREDUCTIBLE - -(* recursive functions... *) -val unfreeze : 'a clos_infos -> fconstr -> fconstr -val whnf_frterm : 'a clos_infos -> fconstr -> fconstr -val whnf_term : 'a clos_infos -> fconstr subs -> constr -> fconstr -val whnf_apply : 'a clos_infos -> fconstr -> fconstr stack -> fconstr +val to_constr : + (lift -> fconstr -> 'a) -> lift -> fconstr -> ('a,'a) kind_of_term (* End of cbn debug section i*) diff --git a/kernel/environ.ml b/kernel/environ.ml index 6bec01ecd..f88860935 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -255,7 +255,7 @@ let hdchar env c = | IsCoFix (i,(_,ln,_)) -> let id = match List.nth ln i with Name id -> id | _ -> assert false in lowercase_first_char id - | IsMeta _|IsXtra _|IsEvar _|IsMutCase (_, _, _, _) -> "y" + | IsMeta _|IsEvar _|IsMutCase (_, _, _, _) -> "y" in hdrec 0 c diff --git a/kernel/esubst.ml b/kernel/esubst.ml new file mode 100644 index 000000000..0ab021e4c --- /dev/null +++ b/kernel/esubst.ml @@ -0,0 +1,111 @@ + +(* $Id$ *) + +open Util + +(*********************) +(* Lifting *) +(*********************) + +(* Explicit lifts and basic operations *) +type lift = + | ELID + | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *) + | ELLFT of int * lift (* ELLFT(n,l) == apply l to de Bruijn > n *) + (* i.e under n binders *) + +(* compose a relocation of magnitude n *) +let rec el_shft n = function + | ELSHFT(el,k) -> el_shft (k+n) el + | el -> if n = 0 then el else ELSHFT(el,n) + + +(* cross n binders *) +let rec el_liftn n = function + | ELID -> ELID + | ELLFT(k,el) -> el_liftn (n+k) el + | el -> if n=0 then el else ELLFT(n, el) + +let el_lift el = el_liftn 1 el + +(* relocation of de Bruijn n in an explicit lift *) +let rec reloc_rel n = function + | ELID -> n + | ELLFT(k,el) -> + if n <= k then n else (reloc_rel (n-k) el) + k + | ELSHFT(el,k) -> (reloc_rel (n+k) el) + +let rec is_lift_id = function + | ELID -> true + | ELSHFT(e,n) -> n=0 & is_lift_id e + | ELLFT (_,e) -> is_lift_id e + +(*********************) +(* Substitutions *) +(*********************) + +(* (bounded) explicit substitutions of type 'a *) +type 'a subs = + | ESID of int (* ESID(n) = %n END bounded identity *) + | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) + | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) + (* with n vars *) + | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) + +(* operations of subs: collapses constructors when possible. + * Needn't be recursive if we always use these functions + *) + +let subs_cons(x,s) = CONS(x,s) + +let subs_liftn n = function + | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) + | LIFT (p,lenv) -> LIFT (p+n, lenv) + | lenv -> LIFT (n,lenv) + +let subs_lift a = subs_liftn 1 a + +let subs_shft = function + | (0, s) -> s + | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) + | (n, s) -> SHIFT (n,s) + +let subs_shift_cons = function + (0, s, t) -> CONS(t,s) +| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1)) +| (k, s, t) -> CONS(t,SHIFT(k, s));; + +(* Tests whether a substitution is extensionnaly equal to the identity *) +let rec is_subs_id = function + ESID _ -> true + | LIFT(_,s) -> is_subs_id s + | SHIFT(0,s) -> is_subs_id s + | _ -> false + +(* Expands de Bruijn k in the explicit substitution subs + * lams accumulates de shifts to perform when retrieving the i-th value + * the rules used are the following: + * + * [id]k --> k + * [S.t]1 --> t + * [S.t]k --> [S](k-1) if k > 1 + * [^n o S] k --> [^n]([S]k) + * [(%n S)] k --> k if k <= n + * [(%n S)] k --> [^n]([S](k-n)) + * + * the result is (Inr (k+lams,p)) when the variable is just relocated + * where p is None if the variable points inside subs and Some(k) if the + * variable points k bindings beyond subs. + *) +let rec exp_rel lams k subs = + match (k,subs) with + | (1, CONS (def,_)) -> Inl(lams,def) + | (_, CONS (_,l)) -> exp_rel lams (pred k) l + | (_, LIFT (n,_)) when k<=n -> Inr(lams+k,None) + | (_, LIFT (n,l)) -> exp_rel (n+lams) (k-n) l + | (_, SHIFT (n,s)) -> exp_rel (n+lams) k s + | (_, ESID n) when k<=n -> Inr(lams+k,None) + | (_, ESID n) -> Inr(lams+k,Some (k-n)) + +let expand_rel k subs = exp_rel 0 k subs + diff --git a/kernel/esubst.mli b/kernel/esubst.mli new file mode 100644 index 000000000..ea5df0a28 --- /dev/null +++ b/kernel/esubst.mli @@ -0,0 +1,34 @@ + +(* $Id$ *) + +(*s Compact representation of explicit relocations. \\ + [ELSHFT(l,n)] == lift of [n], then apply [lift l]. + [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) +type lift = + | ELID + | ELSHFT of lift * int + | ELLFT of int * lift + +val el_shft : int -> lift -> lift +val el_liftn : int -> lift -> lift +val el_lift : lift -> lift +val reloc_rel : int -> lift -> int +val is_lift_id : lift -> bool + +(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. + [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = + $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. + [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *) +type 'a subs = + | ESID of int + | CONS of 'a * 'a subs + | SHIFT of int * 'a subs + | LIFT of int * 'a subs + +val subs_cons: 'a * 'a subs -> 'a subs +val subs_shft: int * 'a subs -> 'a subs +val subs_lift: 'a subs -> 'a subs +val subs_liftn: int -> 'a subs -> 'a subs +val subs_shift_cons: int * 'a subs * 'a -> 'a subs +val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union +val is_subs_id: 'a subs -> bool diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 620f31eaa..a5920f870 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -345,14 +345,6 @@ let build_branch_type env dep p cs = (* [Rel (n+m);...;Rel(n+1)] *) -let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) - -let rel_list n m = - let rec reln l p = - if p>m then l else reln (mkRel(n+p)::l) (p+1) - in - reln [] 1 - let extended_rel_list n hyps = let rec reln l p = function | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps diff --git a/kernel/inductive.mli b/kernel/inductive.mli index e7504bf16..4980b9196 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -116,11 +116,6 @@ val build_dependent_constructor : constructor_summary -> constr the constructor argument of a dependent predicate in a cases branch *) val build_dependent_inductive : inductive_family -> constr -(*s [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *) -(* (this is iota operator in C. Paulin habilitation thesis) *) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> constr list - (*s [extended_rel_vect n hyps] and [extended_rel_list n hyps] generalizes [rel_vect] when local definitions may occur in parameters *) val extended_rel_vect : int -> rel_context -> constr array diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 21ab932eb..7c244c280 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -11,6 +11,7 @@ open Declarations open Environ open Instantiate open Closure +open Esubst exception Elimconst @@ -78,7 +79,6 @@ let nf_betaiota env = clos_norm_flags betaiota env let nf_betadeltaiota env = clos_norm_flags betadeltaiota env (* lazy weak head reduction functions *) -(* Pb: whd_val parcourt tout le terme, meme si aucune reduction n'a lieu *) let whd_flags flgs env sigma t = whd_val (create_clos_infos flgs env sigma) (inject t) @@ -710,7 +710,7 @@ and eqappr cv_pb infos appr1 appr2 = and (lft2,(n2,hd2,v2)) = appr2 in let el1 = el_shft n1 lft1 and el2 = el_shft n2 lft2 in - match (frterm_of hd1, frterm_of hd2) with + match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> (match kind_of_term a1, kind_of_term a2 with @@ -722,10 +722,6 @@ and eqappr cv_pb infos appr1 appr2 = bool_and_convert (n=m) (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) - | IsXtra s1, IsXtra s2 -> - bool_and_convert (s1=s2) - (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2) | _ -> fun _ -> raise NotConvertible) (* 2 index known to be bound to no constant *) @@ -742,22 +738,22 @@ and eqappr cv_pb infos appr1 appr2 = (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) (* else expand the second occurrence (arbitrary heuristic) *) (fun u -> - match search_frozen_value infos fl2 with + match unfold_reference infos fl2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) u - | None -> (match search_frozen_value infos fl1 with + | None -> (match unfold_reference infos fl1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 u | None -> raise NotConvertible)) (* only one constant, existential, defined var or defined rel *) | (FFlex fl1, _) -> - (match search_frozen_value infos fl1 with + (match unfold_reference infos fl1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible) | (_, FFlex fl2) -> - (match search_frozen_value infos fl2 with + (match unfold_reference infos fl2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) | None -> fun _ -> raise NotConvertible) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f98ee5bdd..eecde292a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -138,8 +138,6 @@ let rec execute mf env cstr = let (j, cst0) = cast_rel env Evd.empty cj tj in (j, Constraint.union cst cst0) - | IsXtra _ -> anomaly "Safe_typing: found an Extra" - and execute_fix mf env lar lfi vdef = let (larj,cst1) = execute_array mf env lar in let lara = Array.map (assumption_of_judgment env Evd.empty) larj in diff --git a/kernel/term.ml b/kernel/term.ml index d75bea008..533f013e4 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -7,6 +7,7 @@ open Util open Pp open Names open Univ +open Esubst (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *) @@ -70,13 +71,12 @@ type kind_of_term = | IsRel of int | IsMeta of int | IsVar of identifier - | IsXtra of string | IsSort of sorts | IsCast of constr * constr | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr - | IsApp of constr * constr array + | IsApp of constr * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -88,7 +88,6 @@ type kind_of_term = val mkRel : int -> constr val mkMeta : int -> constr val mkVar : identifier -> constr -val mkXtra : string -> constr val mkSort : sorts -> constr val mkCast : constr * constr -> constr val mkProd : name * constr * constr -> constr @@ -119,34 +118,54 @@ module Internal : InternalSig = struct *) -type constr = kind_of_term - -and existential = existential_key * constr array -and constant = constant_path * constr array -and constructor = constructor_path * constr array -and inductive = inductive_path * constr array -and rec_declaration = constr array * name list * constr array -and fixpoint = (int array * int) * rec_declaration -and cofixpoint = int * rec_declaration - -and kind_of_term = +module Polymorph = +struct +(* [constr array] is an instance matching definitional [named_context] in + the same order (i.e. last argument first) *) +type 'constr existential = existential_key * 'constr array +type 'constr constant = constant_path * 'constr array +type 'constr constructor = constructor_path * 'constr array +type 'constr inductive = inductive_path * 'constr array +type ('constr, 'types) rec_declaration = + 'types array * name list * 'constr array +type ('constr, 'types) fixpoint = + (int array * int) * ('constr, 'types) rec_declaration +type ('constr, 'types) cofixpoint = + int * ('constr, 'types) rec_declaration + +(* [IsVar] is used for named variables and [IsRel] for variables as + de Bruijn indices. *) + +end +open Polymorph + +type ('constr, 'types) kind_of_term = | IsRel of int | IsMeta of int | IsVar of identifier - | IsXtra of string | IsSort of sorts - | IsCast of constr * constr - | IsProd of name * constr * constr - | IsLambda of name * constr * constr - | IsLetIn of name * constr * constr * constr - | IsApp of constr * constr array - | IsEvar of existential - | IsConst of constant - | IsMutInd of inductive - | IsMutConstruct of constructor - | IsMutCase of case_info * constr * constr * constr array - | IsFix of fixpoint - | IsCoFix of cofixpoint + | IsCast of 'constr * 'constr + | IsProd of name * 'types * 'constr + | IsLambda of name * 'types * 'constr + | IsLetIn of name * 'constr * 'types * 'constr + | IsApp of 'constr * 'constr array + | IsEvar of 'constr existential + | IsConst of 'constr constant + | IsMutInd of 'constr inductive + | IsMutConstruct of 'constr constructor + | IsMutCase of case_info * 'constr * 'constr * 'constr array + | IsFix of ('constr, 'types) fixpoint + | IsCoFix of ('constr, 'types) cofixpoint + +type constr = (constr,constr) kind_of_term + +type existential = existential_key * constr array +type constant = constant_path * constr array +type constructor = constructor_path * constr array +type inductive = inductive_path * constr array +type rec_declaration = constr array * name list * constr array +type fixpoint = (int array * int) * rec_declaration +type cofixpoint = int * rec_declaration (***************************) (* hash-consing functions *) @@ -158,7 +177,6 @@ let comp_term t1 t2 = | IsMeta m1, IsMeta m2 -> m1 = m2 | IsVar id1, IsVar id2 -> id1 == id2 | IsSort s1, IsSort s2 -> s1 == s2 - | IsXtra s1, IsXtra s2 -> s1 == s2 | IsCast (c1,t1), IsCast (c2,t2) -> c1 == c2 & t1 == t2 | IsProd (n1,t1,c1), IsProd (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 | IsLambda (n1,t1,c1), IsLambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2 @@ -185,7 +203,6 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t = | IsRel _ | IsMeta _ -> t | IsVar x -> IsVar (sh_id x) | IsSort s -> IsSort (sh_sort s) - | IsXtra s -> IsXtra (sh_str s) | IsCast (c,t) -> IsCast (sh_rec c, sh_rec t) | IsProd (na,t,c) -> IsProd (sh_na na, sh_rec t, sh_rec c) | IsLambda (na,t,c) -> IsLambda (sh_na na, sh_rec t, sh_rec c) @@ -228,9 +245,6 @@ let mkMeta n = IsMeta n (* Constructs a Variable named id *) let mkVar id = IsVar id -(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *) -let mkXtra s = IsXtra s - (* Construct a type *) let mkSort s = IsSort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) @@ -283,6 +297,7 @@ let mkFix fix = IsFix fix let mkCoFix cofix = IsCoFix cofix let kind_of_term c = c +let mk_constr c = c (* end @@ -346,11 +361,6 @@ let destVar c = match kind_of_term c with | IsVar id -> id | _ -> invalid_arg "destVar" -(* Destructs an XTRA *) -let destXtra c = match kind_of_term c with - | IsXtra s -> s - | _ -> invalid_arg "destXtra" - (* Destructs a type *) let isSort c = match kind_of_term c with | IsSort s -> true @@ -502,7 +512,7 @@ let destCoFix c = match kind_of_term c with the usual representation of the constructions; it is not recursive *) let fold_constr f acc c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> acc | IsCast (c,t) -> f (f acc c) t | IsProd (_,t,c) -> f (f acc t) c | IsLambda (_,t,c) -> f (f acc t) c @@ -526,7 +536,7 @@ let fold_constr f acc c = match kind_of_term c with each binder traversal; it is not recursive *) let fold_constr_with_binders g f n acc c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> acc | IsCast (c,t) -> f n (f n acc c) t | IsProd (_,t,c) -> f (g n) (f n acc t) c | IsLambda (_,t,c) -> f (g n) (f n acc t) c @@ -549,7 +559,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with not specified *) let iter_constr f c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> () + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> () | IsCast (c,t) -> f c; f t | IsProd (_,t,c) -> f t; f c | IsLambda (_,t,c) -> f t; f c @@ -570,7 +580,7 @@ let iter_constr f c = match kind_of_term c with subterms are processed is not specified *) let iter_constr_with_binders g f n c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> () + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> () | IsCast (c,t) -> f n c; f n t | IsProd (_,t,c) -> f n t; f (g n) c | IsLambda (_,t,c) -> f n t; f (g n) c @@ -591,7 +601,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with not specified *) let map_constr f c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c | IsCast (c,t) -> mkCast (f c, f t) | IsProd (na,t,c) -> mkProd (na, f t, f c) | IsLambda (na,t,c) -> mkLambda (na, f t, f c) @@ -612,7 +622,7 @@ let map_constr f c = match kind_of_term c with subterms are processed is not specified *) let map_constr_with_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c) @@ -637,7 +647,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with and the order with which subterms are processed is not specified *) let map_constr_with_named_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) @@ -688,7 +698,7 @@ let array_map_left_pair f a g b = end let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c | IsCast (c,t) -> let c' = f l c in mkCast (c', f l t) | IsProd (na,t,c) -> let t' = f l t in mkProd (na, t', f (g l) c) | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c) @@ -714,7 +724,7 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with (* strong *) let map_constr_with_full_binders g f l c = match kind_of_term c with - | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ -> c | IsCast (c,t) -> mkCast (f l c, f l t) | IsProd (na,t,c) -> mkProd (na, f l t, f (g (na,None,t) l) c) | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g (na,None,t) l) c) @@ -744,7 +754,6 @@ let compare_constr f c1 c2 = | IsMeta m1, IsMeta m2 -> m1 = m2 | IsVar id1, IsVar id2 -> id1 = id2 | IsSort s1, IsSort s2 -> s1 = s2 - | IsXtra s1, IsXtra s2 -> s1 = s2 | IsCast (c1,_), _ -> f c1 c2 | _, IsCast (c2,_) -> f c1 c2 | IsProd (_,t1,c1), IsProd (_,t2,c2) -> f t1 t2 & f c1 c2 @@ -858,35 +867,6 @@ let noccur_with_meta n m term = (* Lifting *) (*********************) -(* Explicit lifts and basic operations *) -type lift_spec = - | ELID - | ELSHFT of lift_spec * int (* ELSHFT(l,n) == lift of n, then apply lift l *) - | ELLFT of int * lift_spec (* ELLFT(n,l) == apply l to de Bruijn > n *) - (* i.e under n binders *) - -(* compose a relocation of magnitude n *) -let rec el_shft n = function - | ELSHFT(el,k) -> el_shft (k+n) el - | el -> if n = 0 then el else ELSHFT(el,n) - - -(* cross n binders *) -let rec el_liftn n = function - | ELID -> ELID - | ELLFT(k,el) -> el_liftn (n+k) el - | el -> if n=0 then el else ELLFT(n, el) - -let el_lift el = el_liftn 1 el - -(* relocation of de Bruijn n in an explicit lift *) -let rec reloc_rel n = function - | ELID -> n - | ELLFT(k,el) -> - if n <= k then n else (reloc_rel (n-k) el) + k - | ELSHFT(el,k) -> (reloc_rel (n+k) el) - - (* The generic lifting function *) let rec exliftn el c = match kind_of_term c with | IsRel i -> mkRel(reloc_rel i el) @@ -1007,9 +987,6 @@ let mkMeta = mkMeta (* Constructs a Variable named id *) let mkVar = mkVar -(* Construct an XTRA term (XTRA is an extra slot for whatever you want) *) -let mkXtra = mkXtra - (* Construct a type *) let mkSort = mkSort let mkProp = mkSort mk_Prop @@ -1239,6 +1216,15 @@ let prod_appvect t nL = Array.fold_left prod_app t nL let prod_applist t nL = List.fold_left prod_app t nL +(* [Rel (n+m);...;Rel(n+1)] *) +let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) + +let rel_list n m = + let rec reln l p = + if p>m then l else reln (mkRel(n+p)::l) (p+1) + in + reln [] 1 + (*********************************) (* Other term destructors *) (*********************************) @@ -1693,7 +1679,6 @@ type constr_operator = | OpMutConstruct of constructor_path | OpMutCase of case_info | OpRec of fix_kind * name list - | OpXtra of string let splay_constr c = match kind_of_term c with | IsRel n -> OpRel n, [||] @@ -1704,7 +1689,7 @@ let splay_constr c = match kind_of_term c with | IsProd (x, t1, t2) -> OpProd x, [|t1;t2|] | IsLambda (x, t1, t2) -> OpLambda x, [|t1;t2|] | IsLetIn (x, b, t1, t2) -> OpLetIn x, [|b;t1;t2|] - | IsApp (f,a) -> OpApp, Array.append [|f|] a + | IsApp (f,a) -> OpApp, Array.append [|f|] a | IsConst (sp, a) -> OpConst sp, a | IsEvar (sp, a) -> OpEvar sp, a | IsMutInd (ind_sp, l) -> OpMutInd ind_sp, l @@ -1712,7 +1697,6 @@ let splay_constr c = match kind_of_term c with | IsMutCase (ci,p,c,bl) -> OpMutCase ci, Array.append [|p;c|] bl | IsFix (fi,(tl,lna,bl)) -> OpRec (RFix fi,lna), Array.append tl bl | IsCoFix (fi,(tl,lna,bl)) -> OpRec (RCoFix fi,lna), Array.append tl bl - | IsXtra s -> OpXtra s, [||] let gather_constr = function | OpRel n, [||] -> mkRel n @@ -1737,7 +1721,6 @@ let gather_constr = function | OpRec (RCoFix i,lna), a -> let n = Array.length a / 2 in mkCoFix (i,(Array.sub a 0 n, lna, Array.sub a n n)) - | OpXtra s, [||] -> mkXtra s | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] let rec mycombine l1 l3 = @@ -1778,7 +1761,6 @@ let splay_constr_with_binders c = match kind_of_term c with (List.rev lna) (Array.to_list (Array.mapi lift tl)) in OpRec (RCoFix fi,lna), ctxt, bl - | IsXtra s -> OpXtra s, [], [||] let gather_constr_with_binders = function | OpRel n, [], [||] -> mkRel n @@ -1805,7 +1787,6 @@ let gather_constr_with_binders = function let (lna, tl) = mysplit ctxt in let tl = Array.mapi (fun i -> lift (-i)) (Array.of_list tl) in mkCoFix (i,(tl, List.rev lna, bl)) - | OpXtra s, [], [||] -> mkXtra s | _ -> errorlabstrm "Term.gather_term" [< 'sTR "ill-formed splayed constr">] let generic_fold_left f acc bl tl = diff --git a/kernel/term.mli b/kernel/term.mli index 858ba2465..8672f10a4 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -31,6 +31,26 @@ type case_printing = (* the integer is the number of real args, needed for reduction *) type case_info = int array * case_printing +(* Concrete type for making pattern-matching. *) +module Polymorph : +sig +(* [constr array] is an instance matching definitional [named_context] in + the same order (i.e. last argument first) *) +type 'constr existential = existential_key * 'constr array +type 'constr constant = constant_path * 'constr array +type 'constr constructor = constructor_path * 'constr array +type 'constr inductive = inductive_path * 'constr array +type ('constr, 'types) rec_declaration = + 'types array * name list * 'constr array +type ('constr, 'types) fixpoint = + (int array * int) * ('constr, 'types) rec_declaration +type ('constr, 'types) cofixpoint = + int * ('constr, 'types) rec_declaration + +(* [IsVar] is used for named variables and [IsRel] for variables as + de Bruijn indices. *) +end + (********************************************************************) (* type of global reference *) @@ -74,46 +94,39 @@ type arity = rel_declaration list * sorts manipulation of terms. Some of these functions may be overlapped with previous ones. *) -(* Concrete type for making pattern-matching. *) +open Polymorph +type ('constr, 'types) kind_of_term = + | IsRel of int + | IsMeta of int + | IsVar of identifier + | IsSort of sorts + | IsCast of 'constr * 'constr + | IsProd of name * 'types * 'constr + | IsLambda of name * 'types * 'constr + | IsLetIn of name * 'constr * 'types * 'constr + | IsApp of 'constr * 'constr array + | IsEvar of 'constr existential + | IsConst of 'constr constant + | IsMutInd of 'constr inductive + | IsMutConstruct of 'constr constructor + | IsMutCase of case_info * 'constr * 'constr * 'constr array + | IsFix of ('constr, 'types) fixpoint + | IsCoFix of ('constr, 'types) cofixpoint -(* [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) type existential = existential_key * constr array type constant = constant_path * constr array type constructor = constructor_path * constr array type inductive = inductive_path * constr array -type rec_declaration = constr array * name list * constr array +type rec_declaration = types array * name list * constr array type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration -(* [IsVar] is used for named variables and [IsRel] for variables as - de Bruijn indices. *) - -type kind_of_term = - | IsRel of int - | IsMeta of int - | IsVar of identifier - | IsXtra of string - | IsSort of sorts - | IsCast of constr * constr - | IsProd of name * types * constr - | IsLambda of name * types * constr - | IsLetIn of name * constr * types * constr - | IsApp of constr * constr array - | IsEvar of existential - | IsConst of constant - | IsMutInd of inductive - | IsMutConstruct of constructor - | IsMutCase of case_info * constr * constr * constr array - | IsFix of fixpoint - | IsCoFix of cofixpoint - (* User view of [constr]. For [IsApp], it is ensured there is at least one argument and the function is not itself an applicative term *) -val kind_of_term : constr -> kind_of_term - +val kind_of_term : constr -> (constr, types) kind_of_term +val mk_constr : (constr, types) kind_of_term -> constr (*s Term constructors. *) @@ -126,9 +139,6 @@ val mkMeta : int -> constr (* Constructs a Variable *) val mkVar : identifier -> constr -(* Construct an [XTRA] term. *) -val mkXtra : string -> constr - (* Construct a type *) val mkSort : sorts -> constr val mkProp : constr @@ -252,9 +262,6 @@ val isMeta : constr -> bool (* Destructs a variable *) val destVar : constr -> identifier -(* Destructs an XTRA *) -val destXtra : constr -> string - (* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *) val destSort : constr -> sorts @@ -478,17 +485,9 @@ val subst_vars : identifier list -> constr -> constr if two names are identical, the one of least indice is keeped *) val substn_vars : int -> identifier list -> constr -> constr -(*s Compact representation of implicit lifts. \\ - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) -type lift_spec = - | ELID - | ELSHFT of lift_spec * int - | ELLFT of int * lift_spec -val el_shft : int -> lift_spec -> lift_spec -val el_liftn : int -> lift_spec -> lift_spec -val el_lift : lift_spec -> lift_spec -val reloc_rel : int -> lift_spec -> int +(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *) +val rel_vect : int -> int -> constr array +val rel_list : int -> int -> constr list (*s Occur check functions. *) @@ -552,19 +551,22 @@ type constr_operator = | OpMutConstruct of constructor_path | OpMutCase of case_info | OpRec of fix_kind * Names.name list - | OpXtra of string + val splay_constr : constr -> constr_operator * constr array val gather_constr : constr_operator * constr array -> constr - +(* +val splay_constr : ('a,'a)kind_of_term -> constr_operator * 'a array +val gather_constr : constr_operator * 'a array -> ('a,'a) kind_of_term +*) val splay_constr_with_binders : constr -> - constr_operator * (name * constr option * constr) list * constr array + constr_operator * rel_declaration list * constr array val gather_constr_with_binders : - constr_operator * (name * constr option * constr) list * constr array + constr_operator * rel_declaration list * constr array -> constr val generic_fold_left : - ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list + ('a -> constr -> 'a) -> 'a -> rel_declaration list -> constr array -> 'a (*s Functionals working on the immediate subterm of a construction *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 65be6547b..7b6e58c83 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -679,8 +679,6 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsMeta _ -> true | IsVar _ | IsSort _ -> List.for_all (check_rec_call env n lst) l - - | IsXtra _ -> List.for_all (check_rec_call env n lst) l ) and check_rec_call_fix_body env n lst decr recArgsDecrArg body = @@ -885,7 +883,7 @@ let type_fixpoint env sigma lna lar vdefj = let control_only_guard env sigma = let rec control_rec c = match kind_of_term c with | IsRel _ | IsVar _ -> () - | IsSort _ | IsMeta _ | IsXtra _ -> () + | IsSort _ | IsMeta _ -> () | IsCoFix (_,(tys,_,bds) as cofix) -> check_cofix env sigma cofix; Array.iter control_rec tys; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml new file mode 100644 index 000000000..15a50bcc4 --- /dev/null +++ b/pretyping/cbv.ml @@ -0,0 +1,396 @@ + +(* $Id$ *) + +open Util +open Pp +open Term +open Names +open Environ +open Instantiate +open Univ +open Evd +open Closure +open Esubst + +(**** Call by value reduction ****) + +(* The type of terms with closure. The meaning of the constructors and + * the invariants of this datatype are the following: + * VAL(k,c) represents the constr c with a delayed shift of k. c must be + * in normal form and neutral (i.e. not a lambda, a construct or a + * (co)fix, because they may produce redexes by applying them, + * or putting them in a case) + * LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated + * only when the abstraction is applied, and then we use the rule + * ([S]([x:a]b) c) --> [S.c]b + * This corresponds to the usual strategy of weak reduction + * FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under + * the substitution S, and then applied to args. Here again, + * weak reduction. + * CONSTR(n,(sp,i),vars,args) is the n-th constructor of the i-th + * inductive type sp. + * + * Note that any term has not an equivalent in cbv_value: for example, + * a product (x:A)B must be in normal form because only VAL may + * represent it, and the argument of VAL is always in normal + * form. This remark precludes coding a head reduction with these + * functions. Anyway, does it make sense to head reduce with a + * call-by-value strategy ? + *) +type cbv_value = + | VAL of int * constr + | LAM of name * constr * constr * cbv_value subs + | FIXP of fixpoint * cbv_value subs * cbv_value list + | COFIXP of cofixpoint * cbv_value subs * cbv_value list + | CONSTR of int * inductive_path * cbv_value array * cbv_value list + +(* les vars pourraient etre des constr, + cela permet de retarder les lift: utile ?? *) + +(* relocation of a value; used when a value stored in a context is expanded + * in a larger context. e.g. [%k (S.t)](k+1) --> [^k]t (t is shifted of k) + *) +let rec shift_value n = function + | VAL (k,v) -> VAL ((k+n),v) + | LAM (x,a,b,s) -> LAM (x,a,b,subs_shft (n,s)) + | FIXP (fix,s,args) -> + FIXP (fix,subs_shft (n,s), List.map (shift_value n) args) + | COFIXP (cofix,s,args) -> + COFIXP (cofix,subs_shft (n,s), List.map (shift_value n) args) + | CONSTR (i,spi,vars,args) -> + CONSTR (i, spi, Array.map (shift_value n) vars, + List.map (shift_value n) args) + + +(* Contracts a fixpoint: given a fixpoint and a substitution, + * returns the corresponding fixpoint body, and the substitution in which + * it should be evaluated: its first variables are the fixpoint bodies + * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) + * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) + *) +let contract_fixp env ((reci,i),(_,_,bds as bodies)) = + let make_body j = FIXP(((reci,j),bodies), env, []) in + let n = Array.length bds in + let rec subst_bodies_from_i i subs = + if i=n then subs + else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) + in + subst_bodies_from_i 0 env, bds.(i) + +let contract_cofixp env (i,(_,_,bds as bodies)) = + let make_body j = COFIXP((j,bodies), env, []) in + let n = Array.length bds in + let rec subst_bodies_from_i i subs = + if i=n then subs + else subst_bodies_from_i (i+1) (subs_cons (make_body i, subs)) + in + subst_bodies_from_i 0 env, bds.(i) + + +(* type of terms with a hole. This hole can appear only under App or Case. + * TOP means the term is considered without context + * APP(l,stk) means the term is applied to l, and then we have the context st + * this corresponds to the application stack of the KAM. + * The members of l are values: we evaluate arguments before the function. + * CASE(t,br,pat,S,stk) means the term is in a case (which is himself in stk + * t is the type of the case and br are the branches, all of them under + * the subs S, pat is information on the patterns of the Case + * (Weak reduction: we propagate the sub only when the selected branch + * is determined) + * + * Important remark: the APPs should be collapsed: + * (APP (l,(APP ...))) forbidden + *) + +type cbv_stack = + | TOP + | APP of cbv_value list * cbv_stack + | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack + +(* Adds an application list. Collapse APPs! *) +let stack_app appl stack = + match (appl, stack) with + | ([], _) -> stack + | (_, APP(args,stk)) -> APP(appl@args,stk) + | _ -> APP(appl, stack) + +(* Tests if we are in a case (modulo some applications) *) +let under_case_stack = function + | (CASE _ | APP(_,CASE _)) -> true + | _ -> false + +(* Tells if the reduction rk is allowed by flags under a given stack. + * The stack is useful when flags is (SIMPL,r) because in that case, + * we perform bdi-reduction under the Case, or r-reduction otherwise + *) +let red_allowed flags stack rk = + if under_case_stack stack then + red_under flags rk + else + red_top flags rk + +let red_allowed_ref flags stack = function + | FarRelBinding _ -> red_allowed flags stack DELTA + | VarBinding id -> red_allowed flags stack (VAR id) + | EvarBinding _ -> red_allowed flags stack EVAR + | ConstBinding (sp,_) -> red_allowed flags stack (CONST [sp]) + +(* Transfer application lists from a value to the stack + * useful because fixpoints may be totally applied in several times + *) +let strip_appl head stack = + match head with + | FIXP (fix,env,app) -> (FIXP(fix,env,[]), stack_app app stack) + | COFIXP (cofix,env,app) -> (COFIXP(cofix,env,[]), stack_app app stack) + | CONSTR (i,spi,vars,app) -> (CONSTR(i,spi,vars,[]), stack_app app stack) + | _ -> (head, stack) + + +(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last + * argument is []. + * Because we must put all the applied terms in the stack. + *) +let reduce_const_body redfun v stk = + if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk + + +(* Tests if fixpoint reduction is possible. A reduction function is given as + argument *) +let rec check_app_constr redfun = function + | ([], _) -> false + | ((CONSTR _)::_, 0) -> true + | (t::_, 0) -> (* TODO: partager ce calcul *) + (match redfun t with + | CONSTR _ -> true + | _ -> false) + | (_::l, n) -> check_app_constr redfun (l,(pred n)) + +let fixp_reducible redfun flgs ((reci,i),_) stk = + if red_allowed flgs stk IOTA then + match stk with (* !!! for Acc_rec: reci.(i) = -2 *) + | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i)) + | _ -> false + else + false + +let cofixp_reducible redfun flgs _ stk = + if red_allowed flgs stk IOTA then + match stk with + | (CASE _ | APP(_,CASE _)) -> true + | _ -> false + else + false + +let mindsp_nparams env (sp,i) = + let mib = lookup_mind sp env in + (Declarations.mind_nth_type_packet mib i).Declarations.mind_nparams + +(* The main recursive functions + * + * Go under applications and cases (pushed in the stack), expand head + * constants or substitued de Bruijn, and try to make appear a + * constructor, a lambda or a fixp in the head. If not, it is a value + * and is completely computed here. The head redexes are NOT reduced: + * the function returns the pair of a cbv_value and its stack. * + * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last + * argument is []. Because we must put all the applied terms in the + * stack. *) + +let rec norm_head info env t stack = + (* no reduction under binders *) + match kind_of_term t with + (* stack grows (remove casts) *) + | IsApp (head,args) -> (* Applied terms are normalized immediately; + they could be computed when getting out of the stack *) + let nargs = Array.map (cbv_stack_term info TOP env) args in + norm_head info env head (stack_app (Array.to_list nargs) stack) + | IsMutCase (ci,p,c,v) -> norm_head info env c (CASE(p,v,ci,env,stack)) + | IsCast (ct,_) -> norm_head info env ct stack + + (* constants, axioms + * the first pattern is CRUCIAL, n=0 happens very often: + * when reducing closed terms, n is always 0 *) + | IsRel i -> (match expand_rel i env with + | Inl (0,v) -> + reduce_const_body (cbv_norm_more info env) v stack + | Inl (n,v) -> + reduce_const_body + (cbv_norm_more info env) (shift_value n v) stack + | Inr (n,None) -> + (VAL(0, mkRel n), stack) + | Inr (n,Some p) -> + norm_head_ref (n-p) info env stack (FarRelBinding p)) + + | IsVar id -> norm_head_ref 0 info env stack (VarBinding id) + + | IsConst (sp,vars) -> + let normt = (sp,Array.map (cbv_norm_term info env) vars) in + norm_head_ref 0 info env stack (ConstBinding normt) + + | IsEvar ev -> norm_head_ref 0 info env stack (EvarBinding (ev,env)) + + | IsLetIn (x, b, t, c) -> + (* zeta means letin are contracted; delta without zeta means we *) + (* allow substitution but leave let's in place *) + let zeta = red_allowed (info_flags info) stack ZETA in + let env' = + if zeta or red_allowed (info_flags info) stack DELTA then + subs_cons (cbv_stack_term info TOP env b,env) + else + subs_lift env in + if zeta then + norm_head info env' c stack + else + let normt = + mkLetIn (x, cbv_norm_term info env b, + cbv_norm_term info env t, + cbv_norm_term info env' c) in + (VAL(0,normt), stack) (* Considérer une coupure commutative ? *) + + (* non-neutral cases *) + | IsLambda (x,a,b) -> (LAM(x,a,b,env), stack) + | IsFix fix -> (FIXP(fix,env,[]), stack) + | IsCoFix cofix -> (COFIXP(cofix,env,[]), stack) + | IsMutConstruct ((spi,i),vars) -> + (CONSTR(i,spi, Array.map (cbv_stack_term info TOP env) vars,[]), stack) + + (* neutral cases *) + | (IsSort _ | IsMeta _) -> (VAL(0, t), stack) + | IsMutInd (sp,vars) -> + (VAL(0, mkMutInd (sp, Array.map (cbv_norm_term info env) vars)), stack) + | IsProd (x,t,c) -> + (VAL(0, mkProd (x, cbv_norm_term info env t, + cbv_norm_term info (subs_lift env) c)), + stack) + +and norm_head_ref k info env stack normt = + if red_allowed_ref (info_flags info) stack normt then + match ref_value_cache info normt with + | Some body -> + reduce_const_body (cbv_norm_more info env) (shift_value k body) stack + | None -> (VAL(0,make_constr_ref k info normt), stack) + else (VAL(0,make_constr_ref k info normt), stack) + +and make_constr_ref n info = function + | FarRelBinding p -> mkRel (n+p) + | VarBinding id -> mkVar id + | EvarBinding ((ev,args),env) -> + mkEvar (ev,Array.map (cbv_norm_term info env) args) + | ConstBinding cst -> mkConst cst + +(* cbv_stack_term performs weak reduction on constr t under the subs + * env, with context stack, i.e. ([env]t stack). First computes weak + * head normal form of t and checks if a redex appears with the stack. + * If so, recursive call to reach the real head normal form. If not, + * we build a value. + *) +and cbv_stack_term info stack env t = + match norm_head info env t stack with + (* a lambda meets an application -> BETA *) + | (LAM (x,a,b,env), APP (arg::args, stk)) + when red_allowed (info_flags info) stk BETA -> + let subs = subs_cons (arg,env) in + cbv_stack_term info (stack_app args stk) subs b + + (* a Fix applied enough -> IOTA *) + | (FIXP(fix,env,_), stk) + when fixp_reducible (cbv_norm_more info env) (info_flags info) fix stk -> + let (envf,redfix) = contract_fixp env fix in + cbv_stack_term info stk envf redfix + + (* constructor guard satisfied or Cofix in a Case -> IOTA *) + | (COFIXP(cofix,env,_), stk) + when cofixp_reducible (cbv_norm_more info env) (info_flags info) cofix stk-> + let (envf,redfix) = contract_cofixp env cofix in + cbv_stack_term info stk envf redfix + + (* constructor in a Case -> IOTA + (use red_under because we know there is a Case) *) + | (CONSTR(n,sp,_,_), APP(args,CASE(_,br,(arity,_),env,stk))) + when red_under (info_flags info) IOTA -> + let ncargs = arity.(n-1) in + let real_args = list_lastn ncargs args in + cbv_stack_term info (stack_app real_args stk) env br.(n-1) + + (* constructor of arity 0 in a Case -> IOTA ( " " )*) + | (CONSTR(n,_,_,_), CASE(_,br,_,env,stk)) + when red_under (info_flags info) IOTA -> + cbv_stack_term info stk env br.(n-1) + + (* may be reduced later by application *) + | (head, TOP) -> head + | (FIXP(fix,env,_), APP(appl,TOP)) -> FIXP(fix,env,appl) + | (COFIXP(cofix,env,_), APP(appl,TOP)) -> COFIXP(cofix,env,appl) + | (CONSTR(n,spi,vars,_), APP(appl,TOP)) -> CONSTR(n,spi,vars,appl) + + (* definitely a value *) + | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk) + + +(* if we are in SIMPL mode, maybe v isn't reduced enough *) +and cbv_norm_more info env v = + match (v, (info_flags info)) with + | (VAL(k,t), ((SIMPL|WITHBACK),_)) -> + cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t + | _ -> v + + +(* When we are sure t will never produce a redex with its stack, we + * normalize (even under binders) the applied terms and we build the + * final term + *) +and apply_stack info t = function + | TOP -> t + | APP (args,st) -> + apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st + | CASE (ty,br,ci,env,st) -> + apply_stack info + (mkMutCase (ci, cbv_norm_term info env ty, t, + Array.map (cbv_norm_term info env) br)) + st + + +(* performs the reduction on a constr, and returns a constr *) +and cbv_norm_term info env t = + (* reduction under binders *) + cbv_norm_value info (cbv_stack_term info TOP env t) + +(* reduction of a cbv_value to a constr *) +and cbv_norm_value info = function (* reduction under binders *) + | VAL (n,v) -> lift n v + | LAM (x,a,b,env) -> + mkLambda (x, cbv_norm_term info env a, + cbv_norm_term info (subs_lift env) b) + | FIXP ((lij,(lty,lna,bds)),env,args) -> + applistc + (mkFix (lij, + (Array.map (cbv_norm_term info env) lty, lna, + Array.map (cbv_norm_term info + (subs_liftn (Array.length lty) env)) bds))) + (List.map (cbv_norm_value info) args) + | COFIXP ((j,(lty,lna,bds)),env,args) -> + applistc + (mkCoFix (j, + (Array.map (cbv_norm_term info env) lty, lna, + Array.map (cbv_norm_term info + (subs_liftn (Array.length lty) env)) bds))) + (List.map (cbv_norm_value info) args) + | CONSTR (n,spi,vars,args) -> + applistc + (mkMutConstruct ((spi,n), Array.map (cbv_norm_value info) vars)) + (List.map (cbv_norm_value info) args) + +(* with profiling *) +let cbv_norm infos constr = + with_stats (lazy (cbv_norm_term infos (ESID 0) constr)) + + +type 'a cbv_infos = (cbv_value, 'a) infos + +(* constant bodies are normalized at the first expansion *) +let create_cbv_infos flgs env sigma = + create + (fun old_info s c -> cbv_stack_term old_info TOP s c) + flgs + env + sigma diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli new file mode 100644 index 000000000..08e067f5a --- /dev/null +++ b/pretyping/cbv.mli @@ -0,0 +1,55 @@ + +(*i $Id$ i*) + +(*i*) +open Pp +open Names +open Term +open Evd +open Environ +open Closure +open Esubst +(*i*) + +(***********************************************************************) +(*s Call-by-value reduction *) + +(* Entry point for cbv normalization of a constr *) +type 'a cbv_infos +val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos +val cbv_norm : 'a cbv_infos -> constr -> constr + +(***********************************************************************) +(*i This is for cbv debug *) +type cbv_value = + | VAL of int * constr + | LAM of name * constr * constr * cbv_value subs + | FIXP of fixpoint * cbv_value subs * cbv_value list + | COFIXP of cofixpoint * cbv_value subs * cbv_value list + | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list + +val shift_value : int -> cbv_value -> cbv_value + +type cbv_stack = + | TOP + | APP of cbv_value list * cbv_stack + | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack + +val stack_app : cbv_value list -> cbv_stack -> cbv_stack +val under_case_stack : cbv_stack -> bool +val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack + +val red_allowed : flags -> cbv_stack -> red_kind -> bool +val reduce_const_body : + (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack + +(* recursive functions... *) +val cbv_stack_term : 'a cbv_infos -> + cbv_stack -> cbv_value subs -> constr -> cbv_value +val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr +val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value +val norm_head : 'a cbv_infos -> + cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack +val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr +val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr +(* End of cbv debug section i*) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index dc4330b5e..e376abb25 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -283,9 +283,6 @@ let rec detype avoid env t = in RVar (dummy_loc, id_of_string s)) | IsMeta n -> RMeta (dummy_loc, n) | IsVar id -> RVar (dummy_loc, id) - | IsXtra s -> warning "bdize: Xtra should no longer occur in constr"; - RVar(dummy_loc, id_of_string ("XTRA"^s)) - (* ope("XTRA",((str s):: pl@(List.map detype cl)))*) | IsSort (Prop c) -> RSort (dummy_loc,RProp c) | IsSort (Type _) -> RSort (dummy_loc,RType) | IsCast (c1,c2) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8dab70441..82746d287 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -257,8 +257,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | (IsMeta _ | IsXtra _ | IsLambda _), _ -> false - | _, (IsMeta _ | IsXtra _ | IsLambda _) -> false + | (IsMeta _ | IsLambda _), _ -> false + | _, (IsMeta _ | IsLambda _) -> false | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 625e28d56..b83019b45 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -269,7 +269,7 @@ let rec sub_match nocc pat c = let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))) | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _ - | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ -> + | IsRel _|IsMeta _|IsVar _|IsSort _ -> (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) @@ -320,7 +320,6 @@ let rec pattern_of_constr t = | IsFix f -> PFix f | IsCoFix _ -> error "pattern_of_constr: (co)fix currently not supported" - | IsXtra _ -> anomaly "No longer supported" and pattern_of_ref ref inst = let args = Declare.extract_instance ref inst in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index ee8c1f764..657f3d1e0 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -73,7 +73,6 @@ let rec type_of env cstr= (Array.to_list args)) | IsCast (c,t) -> t | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr) - | IsXtra _ -> error "type_of: Unexpected constr" and sort_of env t = match kind_of_term t with diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index baf120029..1b4b89f8b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -10,6 +10,7 @@ open Environ open Reduction open Closure open Instantiate +open Cbv (************************************************************************) (* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick *) @@ -584,7 +585,7 @@ let rec substlin env name n ol c = | IsCoFix _ -> (warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) - | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ + | (IsRel _|IsMeta _|IsVar _|IsSort _ |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c) let unfold env sigma name = diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d3f7eb0ed..afdaf5823 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -115,8 +115,6 @@ let rec execute mf env sigma cstr = let j, _ = cast_rel env sigma cj tj in j - | IsXtra _ -> anomaly "Typing: found an Extra" - and execute_fix mf env sigma lar lfi vdef = let larj = execute_array mf env sigma lar in let lara = Array.map (assumption_of_judgment env sigma) larj in diff --git a/tactics/refine.ml b/tactics/refine.ml index 8ec991c0f..6c87782fc 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -213,8 +213,7 @@ let rec compute_metamap env c = match kind_of_term c with TH (c,[],[]) (* Autres cas. *) - | IsXtra _|IsCoFix _ -> - invalid_arg "Tcc.compute_metamap" + | IsCoFix _ -> invalid_arg "Tcc.compute_metamap" (* tcc_aux : term_with_holes -> tactic |