diff options
Diffstat (limited to 'checker/closure.ml')
| -rw-r--r-- | checker/closure.ml | 52 |
1 files changed, 23 insertions, 29 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index ccbfbc4c..7ccf06b9 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -38,7 +38,7 @@ let incr_cnt red cnt = if red then begin if !stats then incr cnt; true - end else + end else false let with_stats c = @@ -127,13 +127,13 @@ module RedFlags = (struct { red with r_const = Idpred.remove id l1, l2 } let red_add_transparent red tr = - { red with r_const = tr } + { red with r_const = tr } let mkflags = List.fold_left red_add no_red let red_set red = function | BETA -> incr_cnt red.r_beta beta - | CONST kn -> + | CONST kn -> let (_,l) = red.r_const in let c = Cpred.mem kn l in incr_cnt c delta @@ -165,7 +165,7 @@ let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] let betaiota = mkflags [fBETA;fIOTA] let beta = mkflags [fBETA] let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] -let unfold_red kn = +let unfold_red kn = let flag = match kn with | EvalVarRef id -> fVAR id | EvalConstRef kn -> fCONST kn @@ -187,7 +187,7 @@ let betadeltaiota_red = { r_const = true,[],[]; r_zeta = true; r_evar = true; - r_iota = true } + r_iota = true } let betaiota_red = { r_beta = true; @@ -195,7 +195,7 @@ let betaiota_red = { r_zeta = false; r_evar = false; r_iota = true } - + let beta_red = { r_beta = true; r_const = false,[],[]; @@ -231,7 +231,7 @@ let unfold_red kn = (* Sets of reduction kinds. Main rule: delta implies all consts (both global (= by kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's). - Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of + Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of a LetIn expression is Letin reduction *) type red_kind = @@ -278,7 +278,7 @@ let red_local_const = red_delta_set (* to know if a redex is allowed, only a subset of red_kind is used ... *) let red_set red = function | BETA -> incr_cnt red.r_beta beta - | CONST [kn] -> + | CONST [kn] -> let (b,l,_) = red.r_const in let c = List.mem kn l in incr_cnt ((b & not c) or (c & not b)) delta @@ -339,7 +339,7 @@ type 'a infos = { let info_flags info = info.i_flags let ref_value_cache info ref = - try + try Some (Hashtbl.find info.i_tab ref) with Not_found -> try @@ -360,7 +360,7 @@ let ref_value_cache info ref = let defined_vars flags env = (* if red_local_const (snd flags) then*) - fold_named_context + fold_named_context (fun (id,b,_) e -> match b with | None -> e @@ -370,7 +370,7 @@ let defined_vars flags env = let defined_rels flags env = (* if red_local_const (snd flags) then*) - fold_rel_context + fold_rel_context (fun (id,b,t) (i,subs) -> match b with | None -> (i+1, subs) @@ -380,6 +380,11 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env +let eq_table_key k1 k2 = + match k1,k2 with + | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2 + | _,_ -> k1=k2 + let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; @@ -417,8 +422,8 @@ let neutr = function | (Whnf|Norm) -> Whnf | (Red|Cstr) -> Red -type fconstr = { - mutable norm: red_state; +type fconstr = { + mutable norm: red_state; mutable term: fterm } and fterm = @@ -456,7 +461,7 @@ let update v1 (no,t) = else {norm=no;term=t} (**********************************************************************) -(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) type stack_member = | Zapp of fconstr array @@ -496,9 +501,6 @@ let rec decomp_stack = function | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) | _ -> None -let rec decomp_stackn = function - | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s) - | _ -> assert false let array_of_stack s = let rec stackrec = function | [] -> [] @@ -507,7 +509,7 @@ let array_of_stack s = in Array.concat (stackrec s) let rec stack_assign s p c = match s with | Zapp args :: s -> - let q = Array.length args in + let q = Array.length args in if p >= q then Zapp args :: stack_assign s (p-q) c else @@ -515,7 +517,7 @@ let rec stack_assign s p c = match s with nargs.(p) <- c; Zapp nargs :: s) | _ -> s -let rec stack_tail p s = +let rec stack_tail p s = if p = 0 then s else match s with | Zapp args :: s -> @@ -547,8 +549,6 @@ 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 lift_fconstr_list k l = - if k=0 then l else List.map (fun f -> lft_fconstr k f) l let clos_rel e i = match expand_rel i e with @@ -780,7 +780,7 @@ let term_of_fconstr = (* fstrong applies unfreeze_fun recursively on the (freeze) term and * yields a term. Assumes that the unfreeze_fun never returns a - * FCLOS term. + * FCLOS term. let rec fstrong unfreeze_fun lfts v = to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v) *) @@ -857,12 +857,6 @@ let get_nth_arg head 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 decomp_stack stk' with - Some (v, s') -> (Some (depth,v), s') - | None -> (None, zshift depth stk') - let rec get_args n tys f e stk = match stk with Zupdate r :: s -> @@ -979,7 +973,7 @@ let rec knr info m stk = | FLambda(n,tys,f,e) when red_set info.i_flags fBETA -> (match get_args n tys f e stk with Inl e', s -> knit info e' f s - | Inr lam, s -> (lam,s)) + | Inr lam, s -> (lam,s)) | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info (ConstKey kn) with Some v -> kni info v stk |