diff options
| -rw-r--r-- | kernel/closure.ml | 21 | ||||
| -rw-r--r-- | kernel/closure.mli | 1 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 199 |
3 files changed, 120 insertions, 101 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 075e98a7d1..004b59b103 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -90,6 +90,7 @@ let unfold_red sp = { type red_kind = BETA | DELTA | ZETA | EVAR | IOTA | CONST of constant_path list | CONSTBUT of constant_path list + | VAR of identifier let rec red_add red = function | BETA -> { red with r_beta = true } @@ -107,6 +108,7 @@ let rec red_add red = function | IOTA -> { red with r_iota = true } | EVAR -> { red with r_evar = true } | ZETA -> { red with r_zeta = true } + | VAR id -> red_add red (CONST [make_path [] id CCI]) let incr_cnt red cnt = if red then begin @@ -124,12 +126,16 @@ let red_set red = function let (b,l) = red.r_const in 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 c = List.exists (fun sp -> basename sp = id) l in + incr_cnt ((b & not c) or (c & not b)) delta | ZETA -> incr_cnt red.r_zeta zeta | EVAR -> incr_cnt red.r_zeta evar | IOTA -> incr_cnt red.r_iota iota | DELTA -> fst red.r_const (* Used for Rel/Var defined in context *) (* Not for internal use *) - | CONST _ | CONSTBUT _ -> failwith "not implemented" + | CONST _ | CONSTBUT _ | VAR _ -> failwith "not implemented" (* Gives the constant list *) let red_get_const red = @@ -294,24 +300,24 @@ let ref_value_cache info ref = -> None let defined_vars flags env = - if red_local_const (snd flags) then +(* if red_local_const (snd flags) then*) fold_named_context (fun env (id,b,t) e -> match b with | None -> e | Some body -> (id, body)::e) env [] - else [] +(* else []*) let defined_rels flags env = - if red_local_const (snd flags) then +(* if red_local_const (snd flags) then*) fold_rel_context (fun env (id,b,t) (i,subs) -> match b with | None -> (i+1, subs) | Some body -> (i+1, (i,body) :: subs)) env (0,[]) - else (0,[]) +(* else (0,[])*) let infos_under infos = { infos with i_flags = flags_under infos.i_flags } @@ -434,7 +440,8 @@ let red_allowed flags stack rk = red_top flags rk let red_allowed_ref flags stack = function - | FarRelBinding _ | VarBinding _ -> red_allowed flags stack DELTA + | 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]) @@ -1098,7 +1105,7 @@ and whnf_frterm info ft = else ft | FFlex (FVar id) as t-> - if red_under info.i_flags DELTA then + 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 diff --git a/kernel/closure.mli b/kernel/closure.mli index bf855b2624..b546942e17 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -28,6 +28,7 @@ type red_kind = | IOTA | CONST of section_path list | CONSTBUT of section_path list + | VAR of identifier (* Sets of reduction kinds. *) type reds diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3316e23816..c90dcddb13 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -12,6 +12,26 @@ open Classops open Recordops open Evarutil + +type flexible_term = FConst of constant | FRel of int | FVar of identifier +type flex_kind_of_term = + | Rigid of constr + | MaybeFlexible of flexible_term + | Flexible of existential + +let flex_kind_of_term c = + match kind_of_term c with + | IsConst c -> MaybeFlexible (FConst c) + | IsRel n -> MaybeFlexible (FRel n) + | IsVar id -> MaybeFlexible (FVar id) + | IsEvar ev -> Flexible ev + | _ -> Rigid c + +let eval_flexible_term env = function + | FConst c -> constant_opt_value env c + | FRel n -> option_app (lift n) (lookup_rel_value n env) + | FVar id -> lookup_named_value id env + let evar_apprec env isevars stack c = let rec aux s = let (t,stack as s') = Reduction.apprec env !isevars s in @@ -53,8 +73,8 @@ let rec evar_conv_x env isevars pbty term1 term2 = and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) - match (kind_of_term term1, kind_of_term term2) with - | IsEvar (sp1,al1 as ev1), IsEvar (sp2,al2 as ev2) -> + match (flex_kind_of_term term1, flex_kind_of_term term2) with + | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 () = if List.length l1 > List.length l2 then let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in @@ -73,7 +93,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f1; f2] - | IsEvar ev1, IsConst cst2 -> + | Flexible ev1, MaybeFlexible flex2 -> let f1 () = (List.length l1 <= List.length l2) & let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in @@ -81,7 +101,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (pbty,ev1,applist(term2,deb2)) & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 and f4 () = - match constant_opt_value env cst2 with + match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x env isevars pbty appr1 (evar_apprec env isevars l2 v2) @@ -89,7 +109,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f1; f4] - | IsConst cst1, IsEvar ev2 -> + | MaybeFlexible flex1, Flexible ev2 -> let f1 () = (List.length l2 <= List.length l1) & let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in @@ -97,7 +117,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (pbty,ev2,applist(term1,deb1)) & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 and f4 () = - match constant_opt_value env cst1 with + match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x env isevars pbty (evar_apprec env isevars l1 v1) appr2 @@ -105,10 +125,9 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f1; f4] - | IsConst (sp1,al1 as cst1), IsConst (sp2,al2 as cst2) -> + | MaybeFlexible flex1, MaybeFlexible flex2 -> let f2 () = - (sp1 = sp2) - & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2) + (flex1 = flex2) & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) and f3 () = (try conv_record env isevars @@ -116,12 +135,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = with Not_found -> check_conv_record appr2 appr1) with _ -> false) and f4 () = - match constant_opt_value env cst2 with + match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x env isevars pbty appr1 (evar_apprec env isevars l2 v2) | None -> - match constant_opt_value env cst1 with + match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x env isevars pbty (evar_apprec env isevars l1 v1) appr2 @@ -129,26 +148,26 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f2; f3; f4] - | IsEvar ev1, _ -> + | Flexible ev1, Rigid _ -> (List.length l1 <= List.length l2) & let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in solve_simple_eqn evar_conv_x env isevars (pbty,ev1,applist(term2,deb2)) & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 - | _, IsEvar ev2 -> + | Rigid _, Flexible ev2 -> (List.length l2 <= List.length l1) & let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in solve_simple_eqn evar_conv_x env isevars (pbty,ev2,applist(term1,deb1)) & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 - | IsConst cst1, _ -> + | MaybeFlexible flex1, Rigid _ -> let f3 () = (try conv_record env isevars (check_conv_record appr1 appr2) with _ -> false) and f4 () = - match constant_opt_value env cst1 with + match eval_flexible_term env flex1 with | Some v1 -> evar_eqappr_x env isevars pbty (evar_apprec env isevars l1 v1) appr2 @@ -156,12 +175,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f3; f4] - | _ , IsConst cst2 -> + | Rigid _ , MaybeFlexible flex2 -> let f3 () = (try (conv_record env isevars (check_conv_record appr2 appr1)) with _ -> false) and f4 () = - match constant_opt_value env cst2 with + match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x env isevars pbty appr1 (evar_apprec env isevars l2 v2) @@ -169,89 +188,81 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f3; f4] - | IsRel n, IsRel m -> - n=m - & (List.length(l1) = List.length(l2)) - & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) - - | IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 - - | _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) - - | IsVar id1, IsVar id2 -> - (id1=id2 & (List.length l1 = List.length l2) - & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)) - - | IsMeta n, IsMeta m -> - (n=m & (List.length(l1) = List.length(l2)) - & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)) - - | IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2 - - | IsLambda (_,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> - evar_conv_x env isevars CONV c1 c2 - & evar_conv_x env isevars CONV c'1 c'2 - - | IsLetIn (_,b1,_,c'1), IsLetIn (_,b2,_,c'2) -> - let f1 () = - evar_conv_x env isevars CONV b1 b2 - & evar_conv_x env isevars pbty c'1 c'2 - & (List.length l1 = List.length l2) - & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) - and f2 () = - evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) (subst1 b2 c'2,l2) - in - ise_try isevars [f1; f2] - - | IsLetIn (_,b1,_,c'1), _ -> (* On fait commuter les args avec le Let *) - evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2 - - | _, IsLetIn (_,b2,_,c'2) -> - evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2) - - | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> - evar_conv_x env isevars CONV c1 c2 - & - (let d = nf_ise1 !isevars c1 in - evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2) - - | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> - sp1=sp2 - & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 - & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 + | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with + + | IsCast (c1,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 + + | _, IsCast (c2,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) + + | IsSort s1, IsSort s2 when l1=[] & l2=[] -> base_sort_cmp pbty s1 s2 + + | IsLambda (_,c1,c'1), IsLambda (_,c2,c'2) when l1=[] & l2=[] -> + evar_conv_x env isevars CONV c1 c2 + & evar_conv_x env isevars CONV c'1 c'2 + + | IsLetIn (_,b1,_,c'1), IsLetIn (_,b2,_,c'2) -> + let f1 () = + evar_conv_x env isevars CONV b1 b2 + & evar_conv_x env isevars pbty c'1 c'2 + & (List.length l1 = List.length l2) + & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2) + and f2 () = + evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) + (subst1 b2 c'2,l2) + in + ise_try isevars [f1; f2] + + | IsLetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *) + evar_eqappr_x env isevars pbty (subst1 b1 c'1,l1) appr2 + + | _, IsLetIn (_,b2,_,c'2) -> + evar_eqappr_x env isevars pbty appr1 (subst1 b2 c'2,l2) + + | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> + evar_conv_x env isevars CONV c1 c2 + & + (let d = nf_ise1 !isevars c1 in + evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2) + + | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> + sp1=sp2 + & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 + & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 - | IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) -> - sp1=sp2 - & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 - & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 - - | IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) -> - evar_conv_x env isevars CONV p1 p2 - & evar_conv_x env isevars CONV c1 c2 - & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - - | IsFix (li1,(tys1,_,bds1)), IsFix (li2,(tys2,_,bds2)) -> - li1=li2 - & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) + | IsMutConstruct (sp1,cl1), IsMutConstruct (sp2,cl2) -> + sp1=sp2 + & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2 + & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2 + + | IsMutCase (_,p1,c1,cl1), IsMutCase (_,p2,c2,cl2) -> + evar_conv_x env isevars CONV p1 p2 + & evar_conv_x env isevars CONV c1 c2 + & (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) + & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) + + | IsFix (li1,(tys1,_,bds1)), IsFix (li2,(tys2,_,bds2)) -> + li1=li2 + & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) + & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) + & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) -> - i1=i2 - & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) - & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) - & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) + | IsCoFix (i1,(tys1,_,bds1)), IsCoFix (i2,(tys2,_,bds2)) -> + i1=i2 + & (array_for_all2 (evar_conv_x env isevars CONV) tys1 tys2) + & (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2) + & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2) - | (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _), _ -> false - | _, (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _) -> false + | (IsMeta _ | IsXtra _ | IsLambda _), _ -> false + | _, (IsMeta _ | IsXtra _ | IsLambda _) -> false - | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false - | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false + | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false + | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false - | (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), - (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false + | (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), + (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false + | (IsRel _ | IsVar _ | IsConst _ | IsEvar _), _ -> assert false + | _, (IsRel _ | IsVar _ | IsConst _ | IsEvar _) -> assert false and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = |