diff options
| -rw-r--r-- | .depend | 8 | ||||
| -rw-r--r-- | dev/changements.txt | 6 | ||||
| -rw-r--r-- | kernel/closure.ml | 6 | ||||
| -rw-r--r-- | kernel/closure.mli | 4 | ||||
| -rw-r--r-- | kernel/environ.ml | 37 | ||||
| -rw-r--r-- | kernel/environ.mli | 16 | ||||
| -rw-r--r-- | kernel/names.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 1622 | ||||
| -rw-r--r-- | kernel/reduction.mli | 171 | ||||
| -rw-r--r-- | kernel/term.ml | 1 | ||||
| -rw-r--r-- | kernel/term.mli | 1 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 16 | ||||
| -rw-r--r-- | lib/util.mli | 4 |
15 files changed, 1892 insertions, 9 deletions
@@ -6,6 +6,8 @@ kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/generic.cmi: kernel/names.cmi lib/util.cmi kernel/names.cmi: lib/pp.cmi kernel/printer.cmi: lib/pp.cmi kernel/term.cmi +kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/term.cmi: lib/coqast.cmi kernel/generic.cmi kernel/names.cmi \ kernel/univ.cmi @@ -33,6 +35,12 @@ kernel/generic.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \ kernel/generic.cmi 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/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi kernel/names.cmi lib/pp.cmi kernel/printer.cmi \ + kernel/term.cmi kernel/reduction.cmi +kernel/reduction.cmx: kernel/closure.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/generic.cmx kernel/names.cmx lib/pp.cmx kernel/printer.cmi \ + kernel/term.cmx kernel/reduction.cmi kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi kernel/sign.cmi kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \ diff --git a/dev/changements.txt b/dev/changements.txt index c488bed58..0d007bd30 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -33,4 +33,8 @@ Changements dans les fonctions : app_tl_vect -> array_app_tl cons_vect -> array_cons - Std.comp -> Util.compose + Std + comp -> Util.compose + rev_append -> List.rev_append + +
\ No newline at end of file diff --git a/kernel/closure.ml b/kernel/closure.ml index a543f486c..fa174d610 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -849,12 +849,14 @@ let search_frozen_cst info op vars = (* cache of constants: the body is computed only when needed. *) type 'a clos_infos = (fconstr, 'a) infos -let create_clos_infos flgs sigma = +let create_clos_infos flgs env = { i_flags = flgs; i_repr = (fun old_info c -> inject c); - i_env = sigma; + i_env = env; i_tab = Hashtbl.create 17 } +let clos_infos_env infos = infos.i_env + (* Head normal form. *) let fhnf info v = let uv = unfreeze info v in diff --git a/kernel/closure.mli b/kernel/closure.mli index 3f3665191..52f2ad038 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -97,8 +97,7 @@ val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr -(* Lazy reduction - *) +(* Lazy reduction *) type 'a freeze type 'a frterm = | FRel of int @@ -161,6 +160,7 @@ type case_status = (* Constant cache *) type 'a clos_infos val create_clos_infos : flags -> 'a unsafe_env -> 'a clos_infos +val clos_infos_env : 'a clos_infos -> 'a unsafe_env (* Reduction function *) val norm_val : 'a clos_infos -> fconstr -> constr diff --git a/kernel/environ.ml b/kernel/environ.ml index 06881e130..485d1baa3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -3,8 +3,43 @@ open Names open Sign +open Term type 'a unsafe_env = { context : context; - sigma : 'a evar_map } + sigma : 'a evar_map; + metamap : (int * constr) list +} +(* First character of a constr *) + +let lowercase_first_char id = String.lowercase (first_char id) + +let rec hdchar = function + | DOP2(Prod,_,DLAM(_,c)) -> hdchar c + | DOP2(Cast,c,_) -> hdchar c + | DOPN(AppL,cl) -> hdchar (array_hd cl) + | DOP2(Lambda,_,DLAM(_,c)) -> hdchar c + | DOPN(Const _,_) as x -> + let c = lowercase_first_char (basename (path_of_const x)) in + if c = "?" then "y" else c + | DOPN(Abst _,_) as x -> + lowercase_first_char (basename (path_of_abst x)) + | DOPN(MutInd (sp,i) as x,_) -> + if i=0 then + lowercase_first_char (basename sp) + else + let na = id_of_global x in lowercase_first_char na + | DOPN(MutConstruct(sp,i) as x,_) -> + let na = id_of_global x in String.lowercase(List.hd(explode_id na)) + | VAR id -> lowercase_first_char id + | DOP0(Sort s) -> sort_hdchar s + | _ -> "y" + +let id_of_name_using_hdchar a = function + | Anonymous -> id_of_string (hdchar a) + | Name id -> id + +let named_hd a = function + | Anonymous -> Name (id_of_string (hdchar a)) + | x -> x diff --git a/kernel/environ.mli b/kernel/environ.mli index ce2329734..98d9e7b88 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -5,6 +5,7 @@ open Names open Term open Constant open Inductive +open Univ type 'a unsafe_env @@ -19,8 +20,23 @@ val lookup_var : identifier -> 'a unsafe_env -> constr val loopup_rel : int -> 'a unsafe_env -> name * constr val lookup_constant : section_path -> 'a unsafe_env -> constant +val id_of_global : 'a unsafe_env -> sorts oper -> identifier +val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier +val named_hd : 'a unsafe_env -> constr -> name -> name + +val translucent_abst : 'a unsafe_env -> constr -> bool +val evaluable_abst : 'a unsafe_env -> constr -> bool +val abst_value : 'a unsafe_env -> constr -> constr + +val translucent_const : 'a unsafe_env -> constr -> bool +val evaluable_const : 'a unsafe_env -> constr -> bool +val const_value : 'a unsafe_env -> constr -> constr + val const_abst_opt_value : 'a unsafe_env -> constr -> constr option +val mind_nparams : 'a unsafe_env -> constr -> int val mindsp_nparams : 'a unsafe_env -> section_path -> int +val sort_cmp : 'a unsafe_env -> conv_pb -> sorts -> sorts -> bool * universes + diff --git a/kernel/names.ml b/kernel/names.ml index e9de197fe..b471573f6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -65,6 +65,12 @@ let id_ord id1 id2 = let id_without_number id = id.index = (-1) +let first_char id = + if id.atom = "" then + failwith "lowercase_first_char" + else + String.make 1 id.atom.[0] + module IdOrdered = struct type t = identifier diff --git a/kernel/names.mli b/kernel/names.mli index 5d8791ba9..0ca83f70d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -17,6 +17,7 @@ val atompart_of_id : identifier -> string val index_of_id : identifier -> int val id_ord : identifier -> identifier -> int val id_without_number : identifier -> bool +val first_char : identifier -> string module Idset : Set.S with type elt = identifier diff --git a/kernel/reduction.ml b/kernel/reduction.ml new file mode 100644 index 000000000..5b88d5e69 --- /dev/null +++ b/kernel/reduction.ml @@ -0,0 +1,1622 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Generic +open Term +open Univ +open Evd +open Environ +open Closure + +let mt_evd = Evd.mt_evd + +exception Redelimination +exception Induc +exception Elimconst + +type 'a reduction_function = 'a unsafe_env -> constr -> constr +type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list + -> constr * constr list + +(*************************************) +(*** Reduction Functions Operators ***) +(*************************************) + +let rec under_casts f = function + | DOP2(Cast,c,t) -> DOP2(Cast,under_casts f c, t) + | c -> f c + +let rec whd_stack x stack = + match x with + | DOPN(AppL,cl) -> whd_stack cl.(0) (array_app_tl cl stack) + | DOP2(Cast,c,_) -> whd_stack c stack + | _ -> (x,stack) + +let stack_reduction_of_reduction red_fun x stack = + let t = red_fun (applistc x stack) in + whd_stack t [] + +let rec strong whdfun t = + match whdfun t with + | DOP0 _ as t -> t + (* Cas ad hoc *) + | DOP1(oper,c) -> DOP1(oper,strong whdfun c) + | DOP2(oper,c1,c2) -> DOP2(oper,strong whdfun c1,strong whdfun c2) + | DOPN(oper,cl) -> DOPN(oper,Array.map (strong whdfun) cl) + | DOPL(oper,cl) -> DOPL(oper,List.map (strong whdfun) cl) + | DLAM(na,c) -> DLAM(na,strong whdfun c) + | DLAMV(na,c) -> DLAMV(na,Array.map (strong whdfun) c) + | VAR _ as t -> t + | Rel _ as t -> t + +let rec strong_prodspine redfun c = + match redfun c with + | DOP2(Prod,a,DLAM(na,b)) -> + DOP2(Prod,a,DLAM(na,strong_prodspine redfun b)) + | x -> x + + +(****************************************************************************) +(* Reduction Functions *) +(****************************************************************************) + + +(* call by value reduction functions *) +let cbv_norm_flags flags env t = + cbv_norm (create_cbv_infos flags env) t + +let cbv_beta env = cbv_norm_flags beta env +let cbv_betaiota env = cbv_norm_flags betaiota env +let cbv_betadeltaiota env = cbv_norm_flags betadeltaiota env + +let compute = cbv_betadeltaiota + + +(* lazy reduction functions. The infos must be created for each term *) +let clos_norm_flags flgs env t = + norm_val (create_clos_infos flgs env) (inject t) + +let nf_beta env = clos_norm_flags beta env +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 t = + whd_val (create_clos_infos flgs env) (inject t) + +(* +let whd_beta = whd_flags beta mt_evd +let whd_betaiota = whd_flags betaiota mt_evd +let whd_betadeltaiota = whd_flags betadeltaiota + +let whd_beta_stack = stack_reduction_of_reduction whd_beta +let whd_betaiota_stack = stack_reduction_of_reduction whd_betaiota +let whd_betadeltaiota_stack env = + stack_reduction_of_reduction (whd_betadeltaiota env) +*) + + +(* Red reduction tactic: reduction to a product *) +let red_product env c = + let rec redrec x = + match x with + | DOPN(AppL,cl) -> + DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl)) + | DOPN(Const _,_) when evaluable_const env x -> const_value env x + | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x + | DOP2(Cast,c,_) -> redrec c + | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b)) + | _ -> error "Term not reducible" + in + nf_betaiota env (redrec c) + + +(* Substitute only a list of locations locs, the empty list is interpreted + as substitute all, if 0 is in the list then no substitution is done + the list may contain only negative occurrences that will not be substituted *) +(* Aurait sa place dans term.ml mais term.ml ne connait pas printer.ml *) +let subst_term_occ locs c t = + let rec substcheck except k occ c t = + if except or List.exists (function u -> u>=occ) locs + then substrec except k occ c t + else (occ,t) +and substrec except k occ c t = + if eq_constr t c then + if except then if List.mem (-occ) locs then (occ+1,t) + else (occ+1,Rel(k)) + else if List.mem occ locs then (occ+1,Rel(k)) + else (occ+1,t) + else match t with + DOPN(Const sp,tl) -> occ,t + | DOPN(MutConstruct _,tl) -> occ,t + | DOPN(MutInd _,tl) -> occ,t + + | DOPN(i,cl) -> let (occ',cl') = + Array.fold_left (fun (nocc',lfd) f -> + let (nocc'',f') = substcheck except k nocc' c f + in (nocc'',f'::lfd)) (occ,[]) cl + in (occ',DOPN(i,Array.of_list (List.rev cl'))) + + | DOP2(i,t1,t2) -> let (nocc1,t1')=substrec except k occ c t1 in + let (nocc2,t2')=substcheck except k nocc1 c t2 + in nocc2,DOP2(i,t1',t2') + | DOP1(i,t) -> let (nocc,t')= substrec except k occ c t in + nocc,DOP1(i,t') + + | DLAM(n,t) -> let (occ',t') = substcheck except (k+1) occ (lift 1 c) t + in (occ',DLAM(n,t')) + + | DLAMV(n,cl) -> let (occ',cl') = + Array.fold_left (fun (nocc',lfd) f -> + let (nocc'',f') = substcheck except (k+1) nocc' (lift 1 c) f + in (nocc'',f'::lfd)) (occ,[]) cl + in (occ',DLAMV(n,Array.of_list (List.rev cl') )) + | _ -> occ,t + in if locs = [] then subst_term c t + else if List.mem 0 locs then t + else let except = List.for_all (fun n -> n<0) locs in + let (nbocc,t') = substcheck except 1 1 c t in + if List.exists (fun o -> o>=nbocc or o<= -nbocc) locs then + errorlabstrm "subst_occ" + [< 'sTR "Only "; 'iNT (nbocc-1); 'sTR " occurrences of"; + 'bRK(1,1); Printer.prterm c; 'sPC; + 'sTR "in"; 'bRK(1,1); Printer.prterm t>] + else t' + + +(* linear substitution (following pretty-printer) of the value of name in c. + * n is the number of the next occurence of name. + * ol is the occurence list to find. *) +let rec substlin env name n ol c = + match c with + DOPN(Const sp,_) -> + if (path_of_const c)=name then + if (List.hd ol)=n then + if evaluable_const env c then ((n+1),(List.tl ol), const_value env c) + else + errorlabstrm "substlin" + [< 'sTR(string_of_path sp); + 'sTR " is not a defined constant" >] + else ((n+1),ol,c) + else (n,ol,c) + + | DOPN(Abst _,_) -> + if (path_of_abst c)=name then + if (List.hd ol)=n then ((n+1),(List.tl ol), abst_value env c) + else ((n+1),ol,c) + else (n,ol,c) + +(* INEFFICIENT: OPTIMIZE *) + | DOPN(AppL,tl) -> + let c1 = array_hd tl and cl = array_tl tl in + Array.fold_left (fun (n1,ol1,c1') c2 -> + (match ol1 with + [] -> (n1,[],applist(c1',[c2])) + | _ -> + let (n2,ol2,c2') = substlin env name n1 ol1 c2 + in (n2,ol2,applist(c1',[c2'])))) + (substlin env name n ol c1) cl + + | DOP2(Lambda,c1,DLAM(na,c2)) -> + let (n1,ol1,c1') = substlin env name n ol c1 + in (match ol1 with + [] -> (n1,[],DOP2(Lambda,c1',DLAM(na,c2))) + | _ -> + let (n2,ol2,c2') = substlin env name n1 ol1 c2 + in (n2,ol2,DOP2(Lambda,c1',DLAM(na,c2')))) + | DOP2(Prod,c1,DLAM(na,c2)) -> + let (n1,ol1,c1') = substlin env name n ol c1 + in (match ol1 with + [] -> (n1,[],DOP2(Prod,c1',DLAM(na,c2))) + | _ -> + let (n2,ol2,c2') = substlin env name n1 ol1 c2 + in (n2,ol2,DOP2(Prod,c1',DLAM(na,c2')))) + | DOPN(MutCase _,_) -> let (ci,p,d,llf) = destCase c in + let rec substlist nn oll = function + [] -> (nn,oll,[]) + | f::lfe -> + let (nn1,oll1,f') = substlin env name nn oll f in + (match oll1 with + [] -> (nn1,[],f'::lfe) + | _ -> + let (nn2,oll2,lfe') = substlist nn1 oll1 lfe + in (nn2,oll2,f'::lfe')) + in + let (n1,ol1,p') = substlin env name n ol p in (* ATTENTION ERREUR *) + (match ol1 with (* si P pas affiche *) + [] -> (n1,[],mkMutCaseA ci p' d llf) + | _ -> + let (n2,ol2,d') = substlin env name n1 ol1 d in + (match ol2 with + [] -> (n2,[],mkMutCaseA ci p' d' llf) + | _ -> + let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) + in (n3,ol3,mkMutCase ci p' d' lf'))) + + | DOP2(Cast,c1,c2) -> + let (n1,ol1,c1') = substlin env name n ol c1 + in (match ol1 with + [] -> (n1,[],DOP2(Cast,c1',c2)) + | _ -> + let (n2,ol2,c2') = substlin env name n1 ol1 c2 + in (n2,ol2,DOP2(Cast,c1',c2'))) + | DOPN(Fix _,_) -> + (warning "do not consider occurrences inside fixpoints"; (n,ol,c)) + + | DOPN(CoFix _,_) -> + (warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) + + | _ -> (n,ol,c) + + +let unfold env name = + let flag = (UNIFORM,{ r_beta = true; + r_delta = (fun op -> op=(Const name) or op=(Abst name)); + r_iota = true }) + in clos_norm_flags flag env + + +(* unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr) + * Unfolds the constant name in a term c following a list of occurrences occl. + * at the occurrences of occ_list. If occ_list is empty, unfold all occurences. + * Performs a betaiota reduction after unfolding. *) +let unfoldoccs env (occl,name) c = + match occl with + [] -> unfold env name c + | l -> + match substlin env name 1 (Sort.list (<) l) c with + (_,[],uc) -> nf_betaiota env uc + | (1,_,_) -> error ((string_of_path name)^" does not occur") + | _ -> error ("bad occurrence numbers of "^(string_of_path name)) + + +(* Unfold reduction tactic: *) +let unfoldn loccname env c = + List.fold_left (fun c occname -> unfoldoccs env occname c) c loccname + + + +(* Re-folding constants tactics: refold com in term c *) +let fold_one_com env com c = + let rcom = red_product env com in + subst1 com (subst_term rcom c) + +let fold_commands cl env c = + List.fold_right (fold_one_com env) (List.rev cl) c + + +(* Pattern *) +(* + * gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only + * the specified occurrences. + *) +let abstract_scheme env (locc,a,ta) t = + let na = named_hd env ta Anonymous in + if occur_meta ta then + error "cannot find a type for the generalisation" + else if occur_meta a then + DOP2(Lambda,ta,DLAM(na,t)) + else + DOP2(Lambda, ta, DLAM(na,subst_term_occ locc a t)) + + +let pattern_occs env loccs_trm_typ c = + let abstr_trm = List.fold_right (abstract_scheme env) loccs_trm_typ c in + applist(abstr_trm, List.map (fun (_,t,_) -> t) loccs_trm_typ) + + +(*************************************) +(*** Reduction using substitutions ***) +(*************************************) + +(* 1. Beta Reduction *) + +let rec stacklam recfun env t stack = + match (stack,t) with + | ((h::stacktl), (DOP2(Lambda,_,DLAM(_,c)))) -> + stacklam recfun (h::env) c stacktl + | _ -> recfun (substl env t) stack + + +let beta_applist (c,l) = stacklam (fun c l -> applist(c,l)) [] c l + + +let whd_beta_stack = + let rec whrec x stack = match x with + DOP2(Lambda,c1,DLAM(name,c2)) -> + (match stack with + [] -> (x,[]) + | a1::rest -> stacklam whrec [a1] c2 rest) + + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Cast,c,_) -> whrec c stack + | x -> (x,stack) + in whrec + + + +let whd_beta x = applist(whd_beta_stack x []) + +(*** +let whd_betaimplicit_stack = whrec + where rec whrec x stack = + match x with + DOP2(Lambda,DOP0(Implicit),DLAM(name,c2)) -> + (match stack with + [] -> x,[] + | a1::rest -> stacklam (fun l x -> whrec x l)[a1] rest c2) + + | DOPN(AppL,cl) -> whrec (hd_vect cl) (app_tl_vect cl stack) + | DOP2(Cast,c,_) -> whrec c stack + | x -> x,stack + + +let whd_betaimplicit x = applist(whd_betaimplicit_stack x []) +***) + + +(* 2. Delta Reduction *) + +let whd_const_stack namelist env = + let rec whrec x l = + match x with + (DOPN(Const sp,_)) as c -> + if List.mem sp namelist then + if evaluable_const env c then + whrec (const_value env c) l + else error "whd_const_stack" + else x,l + + | (DOPN(Abst sp,_)) as c -> + if List.mem sp namelist then + if evaluable_abst env c then + whrec (abst_value env c) l + else error "whd_const_stack" + else x,l + + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | x -> x,l + in whrec + + +let whd_const namelist env c = applist(whd_const_stack namelist env c []) + + +let whd_delta_stack env = + let rec whrec x l = + match x with + (DOPN(Const _,_)) as c -> + if evaluable_const env c then + whrec (const_value env c) l + else x,l + | (DOPN(Abst _,_)) as c -> + if evaluable_abst env c then + whrec (abst_value env c) l + else x,l + + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | x -> x,l + in whrec + + +let whd_delta env c = applist(whd_delta_stack env c []) + + +let whd_betadelta_stack env = + let rec whrec x l = + match x with + DOPN(Const _,_) -> + if evaluable_const env x then whrec (const_value env x) l + else (x,l) + | DOPN(Abst _,_) -> + if evaluable_abst env x then whrec (abst_value env x) l + else (x,l) + + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match l with + [] -> (x,l) + | (a::m) -> stacklam whrec [a] c m) + | x -> (x,l) + + in whrec + + +let whd_betadelta env c = applist(whd_betadelta_stack env c []) + + +let whd_betadeltat_stack env = + let rec whrec x l = + match x with + DOPN(Const _,_) -> + if translucent_const env x then whrec (const_value env x) l + else (x,l) + + | DOPN(Abst _,_) -> + if translucent_abst env x then whrec (abst_value env x) l + else (x,l) + + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match l with + [] -> (x,l) + | (a::m) -> stacklam whrec [a] c m) + | x -> (x,l) + + in whrec + + +let whd_betadeltat env c = applist(whd_betadeltat_stack env c []) + + +let whd_betadeltaeta_stack env = + let rec whrec x stack = + match x with + DOPN(Const _,_) -> + if evaluable_const env x then whrec (const_value env x) stack + else (x,stack) + | DOPN(Abst _,_) -> + if evaluable_abst env x then whrec (abst_value env x) stack + else (x,stack) + + | DOP2(Cast,c,_) -> whrec c stack + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> (match applist (whrec c []) with + (DOPN(AppL,cl)) -> + (match whrec (array_last cl) [] with + (Rel 1,[]) -> let napp = (Array.length cl) -1 in + if napp = 0 then (x,stack) else + let lc = Array.sub cl 0 napp in + let u = if napp = 1 then lc.(0) else DOPN(AppL,lc) + in if noccurn 1 u then (pop u,[]) else (x,stack) + | _ -> (x,stack)) + | _ -> (x,stack)) + | (a::m) -> stacklam whrec [a] c m) + + | x -> (x,stack) + + in whrec + + +let whd_betadeltaeta env x = applist(whd_betadeltaeta_stack env x []) + + + +(* 3. Iota reduction *) + +type 'a miota_args = + {mP : constr; (* the result type *) + mconstr : constr; (* the constructor *) + mci : case_info; (* special info to re-build pattern *) + mcargs : 'a list; (* the constructor's arguments *) + mlf : 'a array} (* the branch code vector *) + + +let reducible_mind_case c = + match c with + DOPN(MutConstruct _,_) | DOPN(CoFix _,_) -> true + | _ -> false + + + +let contract_cofix = function + | DOPN(CoFix(bodynum),bodyvect) -> + let nbodies = (Array.length bodyvect) -1 in + let make_Fi j = DOPN(CoFix(j),bodyvect) in + sAPPViList bodynum (array_last bodyvect) + (list_tabulate make_Fi nbodies) + | _ -> assert false + + +let reduce_mind_case env mia = + match mia.mconstr with + (DOPN(MutConstruct((indsp,tyindx),i),_)) -> + let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in + let nparams = mind_nparams env ind in + let real_cargs = snd (list_chop nparams mia.mcargs) in + applist (mia.mlf.(i-1),real_cargs) + | (DOPN(CoFix _,_)) as cofix -> + let cofix_def = contract_cofix cofix + in mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf + | _ -> assert false + + +(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce + + Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] + + *) +let contract_fix = function + | DOPN(Fix(recindices,bodynum),bodyvect) -> + let nbodies = Array.length recindices in + let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in + sAPPViList bodynum (array_last bodyvect) (list_tabulate make_Fi nbodies) + | _ -> assert false + + +let fix_recarg fix stack = + match fix with + | DOPN(Fix(recindices,bodynum),_) -> + if 0 <= bodynum & bodynum < Array.length recindices then + let recargnum = Array.get recindices bodynum in + (try Some(recargnum, List.nth stack recargnum) + with Failure "nth" | Invalid_argument "List.nth" -> None) + else None + | _ -> assert false + + +let reduce_fix whfun fix stack = + match fix with + | DOPN(Fix(recindices,bodynum),bodyvect) -> + (match fix_recarg fix stack with + None -> (false,(fix,stack)) + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg') = whfun recarg [] in + let stack' = list_assign stack recargnum (applist recarg') in + (match recarg'hd with + DOPN(MutConstruct _,_) -> + (true,(contract_fix fix,stack')) + | _ -> (false,(fix,stack')))) + | _ -> assert false + +(* NB : Cette fonction alloue pau c'est l'appel + ``let (recarg'hd,_ as recarg') = whfun recarg [] in'' + -------------------- +qui coute cher dans whd_betadeltaiota *) + +(**) + +let whd_betaiota_stack env = + let rec whrec x stack = + match x with + DOP2(Cast,c,_) -> whrec c stack + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> (x,stack) + | (a::m) -> stacklam whrec [a] c m) + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase x in + let (c,cargs) = whrec d [] + in if reducible_mind_case c + then whrec (reduce_mind_case env + {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack + else (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix whrec x stack + in if reduced then whrec fix stack + else (fix,stack) + + | x -> (x,stack) + + in whrec + + +let whd_betaiota env x = applist (whd_betaiota_stack env x []) + + +let whd_betadeltatiota_stack env = + let rec whrec x stack = + match x with + DOPN(Const _,_) -> + if translucent_const env x then + whrec (const_value env x) stack + else (x,stack) + + | DOPN(Abst _,_) -> + if translucent_abst env x then whrec (abst_value env x) stack + else (x,stack) + + | DOP2(Cast,c,_) -> whrec c stack + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> (x,stack) + | (a::m) -> stacklam whrec [a] c m) + + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase x in + let (c,cargs) = whrec d [] + in if reducible_mind_case c + then whrec (reduce_mind_case env + {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack + else (mkMutCaseA ci p (applist(c,cargs)) lf,stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix whrec x stack + in if reduced then whrec fix stack + else (fix,stack) + + | x -> (x,stack) + + in whrec + + +let whd_betadeltatiota env x = applist(whd_betadeltatiota_stack env x []) + + +let whd_betadeltaiota_stack env = + let rec bdi_rec x stack = + match x with + DOPN(Const _,_) -> + if evaluable_const env x then bdi_rec (const_value env x) stack + else (x,stack) + + | DOPN(Abst _,_) -> + if evaluable_abst env x then bdi_rec (abst_value env x) stack else (x,stack) + + | DOP2(Cast,c,_) -> bdi_rec c stack + + | DOPN(AppL,cl) -> bdi_rec (array_hd cl) (array_app_tl cl stack) + + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> (x,stack) + | (a::m) -> stacklam bdi_rec [a] c m) + + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase x in + let (c,cargs) = bdi_rec d [] + in if reducible_mind_case c + then bdi_rec (reduce_mind_case env + {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack + else (mkMutCaseA ci p (applist(c,cargs)) lf,stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix bdi_rec x stack + in if reduced then bdi_rec fix stack + else (fix,stack) + + | x -> (x,stack) + + in bdi_rec + + +let whd_betadeltaiota env x = applist(whd_betadeltaiota_stack env x []) + + +let whd_betadeltaiotaeta_stack env = + let rec whrec x stack = + match x with + DOPN(Const _,_) -> + if evaluable_const env x then whrec (const_value env x) stack + else (x,stack) + | DOPN(Abst _,_) -> + if evaluable_abst env x then whrec (abst_value env x) stack + else (x,stack) + + | DOP2(Cast,c,_) -> whrec c stack + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> + (match applist (whrec c []) with + (DOPN(AppL,cl)) -> + (match whrec (array_last cl) [] with + (Rel 1,[]) -> + let napp = (Array.length cl) -1 in + if napp = 0 then (x,stack) else + let lc = Array.sub cl 0 napp in + let u = if napp = 1 then lc.(0) else DOPN(AppL,lc) + in if noccurn 1 u then (pop u,[]) else (x,stack) + | _ -> (x,stack)) + | _ -> (x,stack)) + | (a::m) -> stacklam whrec [a] c m) + + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase x in + let (c,cargs) = whrec d [] + in if reducible_mind_case c + then whrec (reduce_mind_case env + {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) stack + else (mkMutCaseA ci p (applist(c,cargs)) lf,stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix whrec x stack + in if reduced then whrec fix stack + else (fix,stack) + + | x -> (x,stack) + + in whrec + + +let whd_betadeltaiotaeta env x = applist(whd_betadeltaiotaeta_stack env x []) + + + +(********************************************************************) +(* Conversion *) +(********************************************************************) + +type 'a conversion_function = + 'a unsafe_env -> constr -> constr -> bool * universes + +(* Conversion between [lft1]term1 and [lft2]term2 *) + +let rec ccnv cv_pb infos lft1 lft2 term1 term2 = + eqappr cv_pb infos (lft1, fhnf infos term1) (lft2, fhnf infos term2) + +(* Conversion between [lft1]([^n1]hd1 v1) and [lft2]([^n2]hd2 v2) *) + +and eqappr cv_pb infos appr1 appr2 = + let (lft1,(n1,hd1,v1)) = appr1 + 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 + (* case of leaves *) + | (FOP0(Sort s1), FOP0(Sort s2)) -> + (Array.length v1 = 0) & (Array.length v2 = 0) + & sort_cmp (clos_infos_env infos) cv_pb s1 s2 + + | (FVAR x1, FVAR x2) -> + (x1=x2) + & (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + + | (FRel n, FRel m) -> + (reloc_rel n el1=reloc_rel m el2) + & (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + + | (FOP0(Meta(n)), FOP0(Meta(m))) -> + (n=m) + & (array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + + | (FOP0 Implicit, FOP0 Implicit) -> + Array.length v1 = 0 & Array.length v2 = 0 + + (* 2 constants or 2 abstractions *) + | (FOPN(Const sp1,al1), FOPN(Const sp2,al2)) -> + uni_or_if (pb_is_univ_adjust cv_pb) + (fun () -> (* try first intensional equality *) + (sp1 == sp2 or sp1=sp2) + & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2) + & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (fun () -> (* else expand the second occurrence (arbitrary heuristic) *) + (match search_frozen_cst infos (Const sp2) al2 with + Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) + | None -> (match search_frozen_cst infos (Const sp1) al1 with + Some def1 -> eqappr cv_pb infos + (lft1, fhnf_apply infos n1 def1 v1) appr2 + | None -> false))) + | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) -> + uni_or_if (pb_is_univ_adjust cv_pb) + (fun () -> (* try first intensional equality *) + sp1=sp2 + & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2) + & (for_all2eq_vect (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (fun () -> (* else expand the second occurrence (arbitrary heuristic) *) + (match search_frozen_cst infos (Abst sp2) al2 with + Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) + | None -> (match search_frozen_cst infos (Abst sp1) al2 with + Some def1 -> eqappr cv_pb infos + (lft1, fhnf_apply infos n1 def1 v1) appr2 + | None -> false))) + + (* only one constant or abstraction *) + | (FOPN((Const _ | Abst _) as op,al1), _) -> + (match search_frozen_cst infos op al1 with + | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 + | None -> false) + | (_, FOPN((Const _ | Abst _) as op,al2)) -> + (match search_frozen_cst infos op al2 with + | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) + | None -> false) + + (* other constructors *) + | (FOP2(Lambda,c1,c2), FOP2(Lambda,c'1,c'2)) -> + (Array.length v1 = 0) & (Array.length v2 = 0) + & ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1 + & ccnv (pb_equal cv_pb) infos el1 el2 c2 c'2 + + | (FOP2(Prod,c1,c2), FOP2(Prod,c'1,c'2)) -> + (Array.length v1 = 0) & (Array.length v2 = 0) + & ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1 (* Luo's system *) + & ccnv cv_pb infos el1 el2 c2 c'2 + + (* Inductive types: MutInd MutConstruct MutCase Fix Cofix *) + + (* Le cas MutCase doit venir avant le cas general DOPN car, a + priori, 2 termes a base de MutCase peuvent etre convertibles + sans que les annotations des MutCase le soient *) + + | (FOPN(MutCase _,cl1), FOPN(MutCase _,cl2)) -> + array_for_all2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2 + & array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2 + + | (FOPN(op1,cl1), FOPN(op2,cl2)) -> + (op1 = op2) + & array_for_all2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2 + & array_for_all2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2 + + (* binders *) + | (FLAM(_,c1,_,_), FLAM(_,c2,_,_)) -> + (Array.length v1 = 0) & (Array.length v2 = 0) + & ccnv cv_pb infos (el_lift el1) (el_lift el2) c1 c2 + + | (FLAMV(_,vc1,_,_), FLAMV(_,vc2,_,_)) -> + (Array.length v1 = 0) & (Array.length v2 = 0) + & for_all2eq_vect (ccnv cv_pb infos (el_lift el1) (el_lift el2)) + vc1 vc2 + + | _ -> false + + +let fconv cv_pb env t1 t2 = + let t1 = strong strip_outer_cast t1 + and t2 = strong strip_outer_cast t2 in + if eq_constr t1 t2 then + true + else + let infos = create_clos_infos hnf_flags env in + ccnv cv_pb infos ELID ELID (inject t1) (inject t2) + +let conv env term1 term2 = uni_pred (fconv CONV env term1) term2 +let conv_leq env term1 term2 = uni_pred (fconv CONV_LEQ env term1) term2 +let conv_x env term1 term2 = fconv CONV_X env term1 term2 +let conv_x_leq env term1 term2 = fconv CONV_X_LEQ env term1 term2 + + +(********************************************************************) +(* Special-Purpose Reduction *) +(********************************************************************) + +let whd_meta mvmap = function + (DOP0(Meta p) as u) -> (try List.assoc p mvmap with Not_found -> u) + | x -> x + + +(* Try to replace all metas. Does not replace metas in the metas' values + * Differs from (strong whd_meta). *) +let plain_instance s c = + let rec irec u = + match u with + DOP0(Meta p) -> (try List.assoc p s with Not_found -> u) + | DOP1(oper,c) -> DOP1(oper, irec c) + | DOP2(oper,c1,c2) -> DOP2(oper, irec c1, irec c2) + | DOPN(oper,cl) -> DOPN(oper, Array.map irec cl) + | DOPL(oper,cl) -> DOPL(oper, List.map irec cl) + | DLAM(x,c) -> DLAM(x, irec c) + | DLAMV(x,v) -> DLAMV(x, Array.map irec v) + | _ -> u + in if s=[] then c else irec c + + +(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) +let instance s c = + if s=[] then c else nf_betaiota (plain_instance s c) + + + +(* pseudo-reduction rule: + * [hnf_prod_app env s (Prod(_,B)) N --> B[N] + * with an HNF on the first argument to produce a product. + * if this does not work, then we use the string S as part of our + * error message. + *) +let hnf_prod_app env s t n = + match whd_betadeltaiota env t with + DOP2(Prod,_,b) -> sAPP b n + | _ -> + errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ; + 'sTR s ; 'fNL >] + + +let hnf_prod_appvect env s t nL = it_vect (hnf_prod_app env s) t nL +let hnf_prod_applist env s t nL = List.fold_left (hnf_prod_app env s) t nL + +let hnf_lam_app env s t n = + match whd_betadeltaiota env t with + DOP2(Lambda,_,b) -> sAPP b n + | _ -> + errorlabstrm s [< 'sTR"Needed a product, but didn't find one in " ; + 'sTR s ; 'fNL >] + +let hnf_lam_appvect env s t nL = it_vect (hnf_lam_app env s) t nL +let hnf_lam_applist env s t nL = List.fold_left (hnf_lam_app env s) t nL + +let splay_prod env = + let rec decrec m c = + match whd_betadeltaiota env c with + DOP2(Prod,a,DLAM(n,c_0)) -> decrec ((n,a)::m) c_0 + | t -> m,t + in decrec [] + + + +let decomp_prod env = + let rec decrec m c = + match whd_betadeltaiota env c with + (DOP0(Sort _) as x) -> m,x + | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m+1) c_0 + | _ -> error "decomp_prod: Not a product" + in decrec 0 + + +let decomp_n_prod env n = + let rec decrec m ln c = if m = 0 then (ln,c) else + match whd_betadeltaiota env c with + DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m-1) ((n,a)::ln) c_0 + | _ -> error "decomp_n_prod: Not enough products" + in decrec n [] + + + + +(* Special iota reduction... *) + +let contract_cofix_use_function f cofix = + match cofix with + | DOPN(CoFix(bodynum),bodyvect) -> + let nbodies = (Array.length bodyvect) -1 in + let make_Fi j = DOPN(CoFix(j),bodyvect) in + let lbodies = list_assign (tabulate_list make_Fi nbodies) bodynum f + in sAPPViList bodynum (last_vect bodyvect) lbodies + | _ -> assert false + + +let reduce_mind_case_use_function f mia = + match mia.mconstr with + (DOPN(MutConstruct((indsp,tyindx),i),_)) -> + let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in + let nparams = mind_nparams ind in + let real_cargs = snd(chop_list nparams mia.mcargs) + in applist (mia.mlf.(i-1),real_cargs) + | (DOPN(CoFix _,_)) as cofix -> + let cofix_def = contract_cofix_use_function f cofix + in mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf + | _ -> assert false + + +let special_red_case env whfun p c ci lf = + let rec redrec c l = + let (constr,cargs) = whfun c l in + match constr with + (DOPN(Const _,_)) as g -> + if (evaluable_const env g) + then + let gvalue = (const_value env g) + in if reducible_mind_case gvalue + then reduce_mind_case_use_function g + {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf} + else redrec gvalue cargs + else raise Redelimination + | _ -> + if reducible_mind_case constr + then reduce_mind_case + {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf} + else raise Redelimination + in redrec c [] + + +(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make +the reduction using this extra information *) + +let contract_fix_use_function f fix = + match fix with + | DOPN(Fix(recindices,bodynum),bodyvect) -> + let nbodies = Array.length recindices in + let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in + let lbodies = list_assign (tabulate_list make_Fi nbodies) bodynum f in + sAPPViList bodynum (last_vect bodyvect) lbodies + | _ -> assert false + + +let reduce_fix_use_function f whfun fix stack = + match fix with + |DOPN (Fix(recindices,bodynum),bodyvect) -> + (match fix_recarg fix stack with + None -> (false,(fix,stack)) + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg')= whfun recarg [] in + let stack' = list_assign stack recargnum (applist recarg') in + (match recarg'hd with + DOPN(MutConstruct _,_) -> + (true,(contract_fix_use_function f fix,stack')) + | _ -> (false,(fix,stack')))) + | _ -> assert false + + + +(* Check that c is an "elimination constant" + [xn:An]..[x1:A1](<P>MutCase (Rel i) of f1..fk end g1 ..gp) +or [xn:An]..[x1:A1](Fix(f|t) (Rel i1) ..(Rel ip)) + with i1..ip distinct variables not occuring in t +keep relevenant information ([i1,Ai1;..;ip,Aip],n,b) +with b = true in case of a fixpoint in order to compute +an equivalent of Fix(f|t)[xi<-ai] as +[yip:Bip]..[yi1:Bi1](F bn..b1) + == [yip:Bip]..[yi1:Bi1](Fix(f|t)[xi<-ai] (Rel 1)..(Rel p)) +with bj=aj if j<>ik and bj=(Rel c) and Bic=Aic[xn..xic-1 <- an..aic-1] + *) + +let compute_consteval c = + let rec srec n labs c = + match whd_betadeltaeta_stack mt_evd c [] with + (DOP2(Lambda,t,DLAM(_,g)),[]) -> srec (n+1) (t::labs) g + | (DOPN(Fix((nv,i)),bodies),l) -> + if (List.length l) > n then raise Elimconst + else + let li = + List.map (function + Rel k -> + if for_all_vect (noccurn k) bodies + then (k, List.nth labs (k-1)) else raise Elimconst + | _ -> raise Elimconst) l + in if (distinct (List.map fst li)) then (li,n,true) + else raise Elimconst + | (DOPN(MutCase _,_) as mc,lapp) -> + (match destCase mc with + (_,_,Rel _,_) -> ([],n,false) + | _ -> raise Elimconst) + | _ -> raise Elimconst + in + try Some (srec 0 [] c) + with Elimconst -> None + + +let is_elim env c = + let (sp, cl) = destConst c in + if (evaluable_const env c) + & (defined_const env c) + & (not((is_existential c))) + then + let (_,cb) = const_of_path sp in + ((match cb.cONSTEVAL with + Some _ -> () + | None -> + (match cb.cONSTBODY with + Some{contents=COOKED b} -> + cb.cONSTEVAL <- Some(compute_consteval b) + | Some{contents=RECIPE _} -> + anomalylabstrm "Reduction.is_elim" + [< 'sTR"Found an uncooked transparent constant," ; 'sPC ; + 'sTR"which is supposed to be impossible" >] + | _ -> assert false)); + (match (cb.cONSTEVAL) with + Some (Some x) -> x + | Some None -> raise Elimconst + | _ -> assert false)) + else raise Elimconst + + +(* takes the fn first elements of the list and gives them back lifted by ln + and in reverse order *) + +let rev_firstn_liftn fn ln = + let rec rfprec p res l = + if p = 0 then res + else + match l with + [] -> invalid_arg "Reduction.rev_firstn_liftn" + | a::rest -> rfprec (p-1) ((lift ln a)::res) rest + in rfprec fn [] + +let make_elim_fun env f largs = + try let (lv,n,b) = is_elim env f and ll = List.length largs + in if ll < n then raise Redelimination else + if b then + let labs,_ = chop_list n largs in + let p = List.length lv in + let la' = map_i (fun q aq -> + try (Rel (p+1-(index (n+1-q) (List.map fst lv)))) + with Failure _ -> aq) 1 + (List.map (lift p) labs) in + it_list_i (fun i c (k,a) -> + DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a), + DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv + else f + with Elimconst | Failure _ -> raise Redelimination + + +let rec red_elim_const env k largs = + if not(evaluable_const env k) then raise Redelimination else + let f = make_elim_fun env k largs in + match whd_betadeltaeta_stack env (const_value env k) largs with + (DOPN(MutCase _,_) as mc,lrest) -> + let (ci,p,c,lf) = destCase mc in + (special_red_case env (construct_const env) p c ci lf, lrest) + + | (DOPN(Fix _,_) as fix,lrest) -> + let (b,(c,rest)) = reduce_fix_use_function f (construct_const env) fix lrest + in if b then (nf_beta c, rest) else raise Redelimination + + | _ -> assert false + +and construct_const env c stack = + let rec hnfstack x stack = + match x with + (DOPN(Const _,_)) as k -> + (try + let (c',lrest) = red_elim_const env k stack + in hnfstack c' lrest + with Redelimination -> + if evaluable_const env k + then let cval = const_value env k + in (match cval with + DOPN (CoFix _,_) -> (k,stack) + | _ -> hnfstack cval stack) + else raise Redelimination) + + | (DOPN(Abst _,_) as a) -> + if evaluable_abst a then hnfstack (abst_value a) stack + else raise Redelimination + + | DOP2(Cast,c,_) -> hnfstack c stack + | DOPN(AppL,cl) -> hnfstack (hd_vect cl) (app_tl_vect cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> assert false + | c'::rest -> stacklam hnfstack [c'] c rest) + | DOPN(MutCase _,_) as c_0 -> + let (ci,p,c,lf) = destCase c_0 in + hnfstack (special_red_case env (construct_const env) p c ci lf) stack + | DOPN(MutConstruct _,_) as c_0 -> c_0,stack + | DOPN(CoFix _,_) as c_0 -> c_0,stack + | DOPN(Fix (_) ,_) as fix -> + let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack + in if reduced then hnfstack fix stack' else raise Redelimination + | _ -> raise Redelimination + in hnfstack c stack + + + +(* Hnf reduction tactic: *) +let hnf_constr env c = + let rec redrec x largs = + match x with + DOP2(Lambda,t,DLAM(n,c)) -> + (match largs with + [] -> applist(x,largs) + | a::rest -> stacklam redrec [a] c rest) + | DOPN(AppL,cl) -> redrec (hd_vect cl) (app_tl_vect cl largs) + | DOPN(Const _,_) -> + (try + let (c',lrest) = red_elim_const env x largs + in redrec c' lrest + with Redelimination -> + if evaluable_const env x + then + let c = const_value env x + in match c with + DOPN(CoFix _,_) -> x + | _ -> redrec c largs + else applist(x,largs)) + | DOPN(Abst _,_) -> + if evaluable_abst x then redrec (abst_value x) largs + else applist(x,largs) + + | DOP2(Cast,c,_) -> redrec c largs + | DOPN(MutCase _,_) -> + let (ci,p,c,lf) = destCase x in + (try + redrec (special_red_case env (whd_betadeltaiota_stack env) p c ci lf) largs + with Redelimination -> applist(x,largs)) + | (DOPN(Fix _,_)) -> + let (reduced,(fix,stack)) = + reduce_fix (whd_betadeltaiota_stack env) x largs + in if reduced then redrec fix stack else applist(x,largs) + + | _ -> applist(x,largs) + + in redrec c [] + + +(* Simpl reduction tactic: same as simplify, but also reduces elimination constants *) +let whd_nf env c = + let rec nf_app c stack = + match c with + DOP2(Lambda,c1,DLAM(name,c2)) -> + (match stack with + [] -> (c,[]) + | a1::rest -> stacklam nf_app [a1] c2 rest) + + | DOPN(AppL,cl) -> nf_app (hd_vect cl) (app_tl_vect cl stack) + | DOP2(Cast,c,_) -> nf_app c stack + | DOPN(Const _,_) -> + (try + let (c',lrest) = red_elim_const env c stack + in nf_app c' lrest + with Redelimination -> (c,stack)) + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase c in + (try + nf_app (special_red_case env nf_app p d ci lf) stack + with Redelimination -> (c,stack)) + | DOPN(Fix _,_) -> + let (reduced,(fix,rest)) = reduce_fix nf_app c stack + in if reduced then nf_app fix rest + else (fix,stack) + + | _ -> (c,stack) + + in applist (nf_app c []) + + +let nf env c = strong (whd_nf env) c + + +(* Generic reduction: reduction functions used in reduction tactics *) +type red_expr = + | Red + | Hnf + | Simpl + | Cbv of flags + | Lazy of flags + | Unfold of (int list * section_path) list + | Fold of constr list + | Change of constr + | Pattern of (int list * constr * constr) list + + +let reduction_of_redexp = function + | Red -> red_product + | Hnf -> hnf_constr + | Simpl -> nf + | Cbv f -> cbv_norm_flags f + | Lazy f -> clos_norm_flags f + | Unfold ubinds -> unfoldn ubinds + | Fold cl -> fold_commands cl + | Change t -> (fun _ _ -> t) + | Pattern lp -> (fun _ -> pattern_occs lp) + + + + +(* Other reductions *) + +let one_step_reduce env = + let rec redrec largs x = + match x with + DOP2(Lambda,t,DLAM(n,c)) -> + (match largs with + [] -> error "Not reducible 1" + | a::rest -> applistc (subst1 a c) rest) + | DOPN(AppL,cl) -> redrec (app_tl_vect cl largs) (hd_vect cl) + | DOPN(Const _,_) -> + (try + let (c',l) = red_elim_const env x largs + in applistc c' l + with Redelimination -> + if evaluable_const env x then + applistc (const_value env x) largs + else error "Not reductible 1") + | DOPN(Abst _,_) -> + if evaluable_abst x then applistc (abst_value x) largs + else error "Not reducible 0" + + | DOPN(MutCase _,_) -> + let (ci,p,c,lf) = destCase x in + (try applistc (special_red_case env (whd_betadeltaiota_stack env) p c ci lf) largs + with Redelimination -> error "Not reducible 2") + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix (whd_betadeltaiota_stack env) x largs + in if reduced then applistc fix stack else error "Not reducible 3" + + | DOP2(Cast,c,_) -> redrec largs c + | _ -> error "Not reducible 3" + + in redrec [] + + +(* One step of approximation *) + +let rec apprec env c stack = + let (t,stack) = whd_betaiota_stack c stack in + match t with + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase t in + let (cr,crargs) = whd_betadeltaiota_stack env d [] in + let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in + if reducible_mind_case cr + then apprec env rslt stack + else (t,stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix (whd_betadeltaiota_stack env) t stack in + if reduced then apprec env fix stack + else (fix,stack) + + | _ -> (t,stack) + + +let hnf env c = apprec env c [] + + +(* A reduction function like whd_betaiota but which keeps casts + * and does not reduce redexes containing meta-variables. + * ASSUMES THAT APPLICATIONS ARE BINARY ONES. + * Used in Programs. + * Added by JCF, 29/1/98. *) + +let whd_programs_stack = + let rec whrec x stack = + match x with + DOPN(AppL,cl) -> + if occur_meta cl.(1) then + (x,stack) + else + whrec (hd_vect cl) (app_tl_vect cl stack) + | DOP2(Lambda,_,DLAM(_,c)) -> + (match stack with + [] -> (x,stack) + | (a::m) -> stacklam whrec [a] c m) + | DOPN(MutCase _,_) -> + let (ci,p,d,lf) = destCase x in + if occur_meta d then + (x,stack) + else + let (c,cargs) = whrec d [] in + if reducible_mind_case c then + whrec (reduce_mind_case + {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}) + stack + else + (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + + | DOPN(Fix _,_) -> + let (reduced,(fix,stack)) = reduce_fix whrec x stack in + if reduced then whrec fix stack else (fix,stack) + + | x -> (x,stack) + + in whrec + + +let whd_programs x = applist(whd_programs_stack x []) + + +(* Used in several tactics, moved from tactics.ml *) +(* -- Eduardo *) + +(* + * put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name + * return name, B and t' +*) + +let reduce_to_mind env t = + let rec elimrec t l = + match whd_castapp_stack t [] with + (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l) + | (DOPN(Const _,_),_) -> + (try let t' = nf_betaiota (one_step_reduce env t) + in elimrec t' l + with UserError _ -> errorlabstrm "tactics__reduce_to_mind" + [< 'sTR"Not an inductive product : it is a constant." >]) + | (DOPN(MutCase _,_),_) -> + (try let t' = nf_betaiota (one_step_reduce env t) + in elimrec t' l + with UserError _ -> errorlabstrm "tactics__reduce_to_mind" + [< 'sTR"Not an inductive product: it is a case analysis term" >]) + | (DOP2(Cast,c,_),[]) -> elimrec c l + | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l) + | _ -> error "Not an inductive product" + in elimrec t [] + + +let reduce_to_ind env t = + let (mind,redt,c) = reduce_to_mind env t + in ((mind_path mind),redt,c) + + + +let find_mrectype env c = + let (t,l) = whd_betadeltaiota_stack env c [] in + match t with + DOPN(MutInd (sp,i),_) -> (t,l) + | _ -> raise Induc + + +let find_minductype env c = + let (t,l) = whd_betadeltaiota_stack env c [] in + match t with + DOPN(MutInd (sp,i),_) + when mind_type_finite (snd (mind_of_path sp)) i -> (t,l) + | _ -> raise Induc + + +let find_mcoinductype env c = + let (t,l) = whd_betadeltaiota_stack env c [] in + match t with + DOPN(MutInd (sp,i),_) + when not (mind_type_finite (snd (mind_of_path sp)) i) -> (t,l) + | _ -> raise Induc + + +let minductype_spec env c = + try let (x,l) = find_minductype env c + in if l<>[] then anomaly "minductype_spec: Not a recursive type 1" + else x + with Induc -> anomaly "minductype_spec: Not a recursive type 2" + + +let mrectype_spec env c = + try let (x,l) = find_mrectype env c + in if l<>[] then anomaly "mrectype_spec: Not a recursive type 1" + else x + with Induc -> anomaly "mrectype_spec: Not a recursive type 2" + + +let check_mrectype_spec env c = + try let (x,l) = find_mrectype env c + in if l<>[] then error "check_mrectype: Not a recursive type 1" else x + with Induc -> error "check_mrectype: Not a recursive type 2" + + + + +exception IsType + +let info_arity env = + let rec srec c = + match whd_betadeltaiota env c with + DOP0(Sort(Prop(Null))) -> false + | DOP0(Sort(Prop(Pos))) -> true + | DOP2(Prod,_,DLAM(_,c')) -> srec c' + | DOP2(Lambda,_,DLAM(_,c')) -> srec c' + | _ -> raise IsType + in srec + +let is_type_arity env = + let rec srec c = + match whd_betadeltaiota env c with + DOP0(Sort(Type(_))) -> true + | DOP2(Prod,_,DLAM(_,c')) -> srec c' + | DOP2(Lambda,_,DLAM(_,c')) -> srec c' + | _ -> false + in srec + +let is_logic_arity env c = try (not (info_arity env c)) + with IsType -> false + +let is_info_arity env c = try (info_arity env c) + with IsType -> true + +let is_info_cast_type env c = + match c with DOP2(Cast,c,t) -> + (try info_arity env t + with IsType -> try info_arity env c with IsType -> true) + | _ -> try info_arity env c with IsType -> true + +let contents_of_cast_type env c = + if is_info_cast_type env c then Pos else Null + +let is_info_sort = is_info_arity mt_evd + +(* calcul des arguments implicites *) + +(* la seconde liste est ordonne'e *) + +let ord_add x l = +let rec aux l = match l with [] -> [x] + | y::l' -> if y > x then x::l + else if x = y then l + else y::(aux l') +in aux l + + +let add_free_rels_until depth m acc = +let rec frec depth loc acc = function + Rel n -> if (n <= depth) & (n > loc) then (ord_add (depth-n+1) acc) else acc + | DOPN(_,cl) -> it_vect (frec depth loc) acc cl + | DOPL(_,cl) -> List.fold_left (frec depth loc) acc cl + | DOP2(_,c1,c2) -> frec depth loc (frec depth loc acc c1) c2 + | DOP1(_,c) -> frec depth loc acc c + | DLAM(_,c) -> frec (depth+1) (loc+1) acc c + | DLAMV(_,cl) -> it_vect (frec (depth+1) (loc+1)) acc cl + | VAR _ -> acc + | DOP0 _ -> acc +in frec depth 0 acc m + + +(* calcule la liste des arguments implicites *) + +let poly_args t = + let rec aux n t = match (whd_betadeltaiota mt_evd t) with + (DOP2(Prod,a,DLAM(_,b))) -> add_free_rels_until n a (aux (n+1) b) + | (DOP2(Cast,t',_)) -> aux n t' + | _ -> [] + +in match (strip_outer_cast (whd_betadeltaiota mt_evd t)) + with (DOP2(Prod,a,DLAM(_,b))) -> aux 1 b + | _ -> [] + + + +(* Expanding existential variables (trad.ml, progmach.ml) *) +(* 1- whd_ise fails if an existential is undefined *) +let rec whd_ise env = function + (DOPN(Const sp,_) as k) -> + if Evd.in_dom env sp then + if defined_const env k then + whd_ise env (const_value env k) + else +(* + let pk = Printer.prterm k in + let pkt = Printer.prterm (const_type env k) in + errorlabstrm "whd_ise" + [< 'sTR"Undefined evar "; pk; 'sTR" : "; pkt >] +*) + errorlabstrm "whd_ise" + [< 'sTR"There is an unknown subterm I cannot solve" >] + else k + | DOP2(Cast,c,_) -> whd_ise env c + | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ))) + | c -> c + + +(* 2- undefined existentials are left unchanged *) +let rec whd_ise1 env = function + (DOPN(Const sp,_) as k) -> + if Evd.in_dom env sp & defined_const env k then + whd_ise1 env (const_value env k) + else k + | DOP2(Cast,c,_) -> whd_ise1 env c + | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ))) + | c -> c + + +let nf_ise1 env = strong (whd_ise1 env) + +(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables + * Similarly we have is_fmachine1_metas and is_resolve1_metas *) + +let rec whd_ise1_metas env = function + (DOPN(Const sp,_) as k) -> + if Evd.in_dom env sp then + if defined_const env k then + whd_ise1_metas env (const_value env k) + else + let m = DOP0(Meta (newMETA())) in + DOP2(Cast,m,const_type env k) + else + k + | DOP2(Cast,c,_) -> whd_ise1_metas env c + | c -> c + + +(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) + +let under_outer_cast f = function + | DOP2 (Cast,b,t) -> DOP2 (Cast,f b,f t) + | c -> f c + +let rec strip_all_casts t = + match t with + | DOP2 (Cast, b, _) -> strip_all_casts b + | DOP0 _ as t -> t + (* Cas ad hoc *) + | DOPN(Fix _ as f,v) -> + let n = Array.length v in + let ts = Array.sub v 0 (n-1) in + let b = v.(n-1) in + DOPN(f, Array.append + (Array.map strip_all_casts ts) + [|under_outer_cast strip_all_casts b|]) + | DOPN(CoFix _ as f,v) -> + let n = Array.length v in + let ts = Array.sub v 0 (n-1) in + let b = v.(n-1) in + DOPN(f, Array.append + (Array.map strip_all_casts ts) + [|under_outer_cast strip_all_casts b|]) + | DOP1(oper,c) -> DOP1(oper,strip_all_casts c) + | DOP2(oper,c1,c2) -> DOP2(oper,strip_all_casts c1,strip_all_casts c2) + | DOPN(oper,cl) -> DOPN(oper,Array.map strip_all_casts cl) + | DOPL(oper,cl) -> DOPL(oper,List.map strip_all_casts cl) + | DLAM(na,c) -> DLAM(na,strip_all_casts c) + | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c) + | VAR _ as t -> t + | Rel _ as t -> t diff --git a/kernel/reduction.mli b/kernel/reduction.mli new file mode 100644 index 000000000..f8646c902 --- /dev/null +++ b/kernel/reduction.mli @@ -0,0 +1,171 @@ + +(* $Id$ *) + +open Names +open Generic +open Term +open Univ +open Environ +open Closure +open Evd + +exception Redelimination +exception Induc +exception Elimconst + +type 'a reduction_function = 'a unsafe_env -> constr -> constr +type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list + -> constr * constr list + +val whd_stack : 'a stack_reduction_function + +(* Reduction Function Operators *) +val under_casts : 'a reduction_function -> 'a reduction_function +val strong : 'a reduction_function -> 'a reduction_function +val strong_prodspine : 'a reduction_function -> 'a reduction_function +val stack_reduction_of_reduction : + 'a reduction_function -> 'a stack_reduction_function + +(************************* + ** Reduction Functions ** + *************************) + +(* Generic Optimized Reduction Functions using Closures *) + +(* 1. lazy strategy *) +val clos_norm_flags : Closure.flags -> 'c unsafe_env -> 'a reduction_function +(* Same as (strong whd_beta[delta][iota]), but much faster on big terms *) +val nf_beta : 'a reduction_function +val nf_betaiota : 'a reduction_function +val nf_betadeltaiota : 'c unsafe_env -> 'a reduction_function + +(* 2. call by value strategy *) +val cbv_norm_flags : flags -> 'c unsafe_env -> 'a reduction_function +val cbv_beta : 'a reduction_function +val cbv_betaiota : 'a reduction_function +val cbv_betadeltaiota : 'c unsafe_env -> 'a reduction_function + +(* 3. lazy strategy, weak head reduction *) +val whd_beta : 'a reduction_function +val whd_betaiota : 'a reduction_function +val whd_betadeltaiota : 'c unsafe_env -> 'a reduction_function + +val whd_beta_stack : 'a stack_reduction_function +val whd_betaiota_stack : 'a stack_reduction_function +val whd_betadeltaiota_stack : 'c unsafe_env -> 'a stack_reduction_function + + +(* Head normal forms *) +val whd_const_stack : section_path list -> 'c unsafe_env -> 'a stack_reduction_function +val whd_const : section_path list -> 'c unsafe_env -> 'a reduction_function +val whd_delta_stack : 'c unsafe_env -> 'a stack_reduction_function +val whd_delta : 'c unsafe_env -> 'a reduction_function +val whd_betadelta_stack : 'c unsafe_env -> 'a stack_reduction_function +val whd_betadelta : 'c unsafe_env -> 'a reduction_function +val whd_betadeltat_stack : 'c unsafe_env -> 'a stack_reduction_function +val whd_betadeltat : 'c unsafe_env -> 'a reduction_function +val whd_betadeltatiota_stack : 'c unsafe_env -> 'a stack_reduction_function +val whd_betadeltatiota : 'c unsafe_env -> 'a reduction_function +val whd_betadeltaiotaeta_stack : 'c unsafe_env -> 'a stack_reduction_function +val whd_betadeltaiotaeta : 'c unsafe_env -> 'a reduction_function + +val beta_applist : (constr * constr list) -> constr + + +(* Special-Purpose Reduction Functions *) +val whd_meta : (int * constr) list -> 'a reduction_function +val plain_instance : (int * constr) list -> 'a reduction_function +val instance : (int * constr) list -> 'a reduction_function + +val whd_ise : 'a unsafe_env -> 'a reduction_function +val whd_ise1 : 'a unsafe_env -> 'a reduction_function +val nf_ise1 : 'a unsafe_env -> 'a reduction_function +val whd_ise1_metas : 'a unsafe_env -> 'a reduction_function + +val red_elim_const : 'c unsafe_env -> 'a stack_reduction_function +val one_step_reduce : 'c unsafe_env -> constr -> constr + +val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr +val hnf_prod_appvect : + 'c unsafe_env -> string -> constr -> constr array -> constr +val hnf_prod_applist : 'c unsafe_env -> string -> constr -> constr list -> constr +val hnf_lam_app : 'c unsafe_env -> string -> constr -> constr -> constr +val hnf_lam_appvect : 'c unsafe_env -> string -> constr -> constr array -> constr +val hnf_lam_applist : 'c unsafe_env -> string -> constr -> constr list -> constr +val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr +val decomp_prod : 'c unsafe_env -> constr -> int * constr +val decomp_n_prod : + 'c unsafe_env -> int -> constr -> ((name * constr) list) * constr + +val is_info_arity : 'c unsafe_env -> constr -> bool +val is_info_sort : constr -> bool +val is_logic_arity : 'c unsafe_env -> constr -> bool +val is_type_arity : 'c unsafe_env -> constr -> bool +val is_info_cast_type : 'c unsafe_env -> constr -> bool +val contents_of_cast_type : 'c unsafe_env -> constr -> contents +val poly_args : constr -> int list +val reduce_to_mind : 'c unsafe_env -> constr -> constr * constr * constr +val reduce_to_ind : 'c unsafe_env -> constr -> + section_path*constr*constr + +val whd_programs : 'a reduction_function + +(* Generic reduction: reduction functions associated to tactics *) +type red_expr = + | Red + | Hnf + | Simpl + | Cbv of flags + | Lazy of flags + | Unfold of (int list * section_path) list + | Fold of constr list + | Change of constr + | Pattern of (int list * constr * constr) list + + +val nf : 'c unsafe_env -> 'a reduction_function +val unfoldn : + (int list * section_path) list -> 'c unsafe_env -> 'a reduction_function +val fold_one_com : 'c unsafe_env -> constr -> 'a reduction_function +val fold_commands : constr list -> 'c unsafe_env -> 'a reduction_function +val subst_term_occ : int list -> constr -> constr -> constr +val pattern_occs : (int list * constr * constr) list -> constr -> constr +val hnf_constr : 'c unsafe_env -> constr -> constr +val compute : 'c unsafe_env -> 'a reduction_function +val reduction_of_redexp : red_expr -> 'c unsafe_env -> constr -> constr + + + +(* Conversion Functions (uses closures, lazy strategy) *) + +type 'a conversion_function = + 'a unsafe_env -> constr -> constr -> bool * universes + +val fconv : conv_pb -> 'a conversion_function +(* fconv has 4 instances: + * conv = fconv CONV : conversion test, and adjust universes constraints + * conv_x = fconv CONV_X : id. , without adjusting univ + (used in tactics) + * conv_leq = fconv CONV_LEQ : cumulativity test, adjust universes + * conv_x_leq = fconv CONV_X_LEQ : id. , without adjusting + (in tactics) + *) +val conv : 'a conversion_function +val conv_leq : 'a conversion_function +val conv_x : 'a conversion_function +val conv_x_leq : 'a conversion_function + +(* Obsolete Reduction Functions *) + +val hnf : 'a unsafe_env -> constr -> constr * constr list +val apprec : 'a stack_reduction_function +val red_product : 'a reduction_function +val find_mrectype : 'a unsafe_env -> constr -> constr * constr list +val find_minductype : 'a unsafe_env -> constr -> constr * constr list +val find_mcoinductype : 'a unsafe_env -> constr -> constr * constr list +val check_mrectype_spec : 'a unsafe_env -> constr -> constr +val minductype_spec : 'a unsafe_env -> constr -> constr +val mrectype_spec : 'a unsafe_env -> constr -> constr + +(* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) +val strip_all_casts : constr -> constr diff --git a/kernel/term.ml b/kernel/term.ml index 0e8a8cdaa..bdf461340 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1228,6 +1228,7 @@ let rec unmatchable=function DLAMV(ne,(Array.map unmatchable tab)) | a -> a + (***************************) (* hash-consing functions *) (***************************) diff --git a/kernel/term.mli b/kernel/term.mli index d5a9b11d3..1a3f29c73 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -465,7 +465,6 @@ val pb_is_univ_adjust : conv_pb -> bool val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb val sort_hdchar : sorts -> string -(* val sort_cmp : conv_pb -> sorts -> sorts -> bool *) (***************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index 0bfaddbcc..391629672 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -10,3 +10,5 @@ val dummy_univ : universe val prop_univ : universe val prop_univ_univ : universe val prop_univ_univ_univ : universe + +type universes diff --git a/lib/util.ml b/lib/util.ml index 625ceed87..77a26062d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -76,7 +76,21 @@ let list_chop n l = | (_, []) -> failwith "chop_list" in chop_aux [] (n,l) - + +let list_tabulate f len = + let rec tabrec n = + if n = len then [] else (f n)::(tabrec (n+1)) + in + tabrec 0 + +let list_assign l n e = + let rec assrec stk = function + | ((h::t), 0) -> List.rev_append stk (e::t) + | ((h::t), n) -> assrec (h::stk) (t, n-1) + | ([], _) -> failwith "list_assign" + in + assrec [] (l,n) + (* Arrays *) let array_exists f v = diff --git a/lib/util.mli b/lib/util.mli index 92aabea5d..c539bdf67 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -24,7 +24,9 @@ val parse_section_path : string -> string list * string * string val intersect : 'a list -> 'a list -> 'a list val subtract : 'a list -> 'a list -> 'a list -val list_chop : int -> 'a list -> 'a list * 'a list +val list_chop : int -> 'a list -> 'a list * 'a list +val list_tabulate : (int -> 'a) -> int -> 'a list +val list_assign : 'a list -> int -> 'a -> 'a list (* Arrays *) |