lazy (fst (reduce ~delta:0 c)),
(fun delta -> fst (reduce ~delta c)),
lazy (unwind c)
lazy (fst (reduce ~delta:0 c)),
(fun delta -> fst (reduce ~delta c)),
lazy (unwind c)
let from_stack_list_for_unwind ~unwind:_ l =
List.map (fun (_,_,c) -> Lazy.force c) l
let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
let from_stack_list_for_unwind ~unwind:_ l =
List.map (fun (_,_,c) -> Lazy.force c) l
let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta
- let rec unwind (k,e,t,s) =
+ let rec unwind status (k,e,t,s) =
let rec aux = function
| k, e, C.Rel n, s when n <= k ->
let k',e',t',s' = RS.from_env ~delta (list_nth e (n-1)) in
let rec aux = function
| k, e, C.Rel n, s when n <= k ->
let k',e',t',s' = RS.from_env ~delta (list_nth e (n-1)) in
| k, _, C.Rel n, s as config (* when n > k *) ->
let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
(match x with
| k, _, C.Rel n, s as config (* when n > k *) ->
let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
(match x with
- | Some(_,C.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
+ | Some(_,C.Def(x,_)) -> aux (0,[],NCicSubstitution.lift status (n - k) x,s)
| _ -> config, true)
| (k, e, C.Meta (n,l), s) as config ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in
| _ -> config, true)
| (k, e, C.Meta (n,l), s) as config ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in
- aux (k, e, NCicSubstitution.subst_meta l term,s)
+ aux (k, e, NCicSubstitution.subst_meta status l term,s)
with NCicUtils.Subst_not_found _ -> config, true)
| (_, _, C.Implicit _, _) -> assert false
| (_, _, C.Sort _, _)
| (_, _, C.Prod _, _)
| (_, _, C.Lambda _, []) as config -> config, true
| (k, e, C.Lambda (_,_,t), p::s) ->
with NCicUtils.Subst_not_found _ -> config, true)
| (_, _, C.Implicit _, _) -> assert false
| (_, _, C.Sort _, _)
| (_, _, C.Prod _, _)
| (_, _, C.Lambda _, []) as config -> config, true
| (k, e, C.Lambda (_,_,t), p::s) ->
- aux (k+1, (RS.stack_to_env ~reduce:(reduce ~subst context) ~unwind p)::e, t,s)
+ aux (k+1, (RS.stack_to_env ~reduce:(reduce status ~subst context) ~unwind:(unwind status) p)::e, t,s)
| (k, e, C.LetIn (_,_,m,t), s) ->
| (k, e, C.LetIn (_,_,m,t), s) ->
aux (k+1, m'::e, t, s)
| (_, _, C.Appl ([]|[_]), _) -> assert false
| (k, e, C.Appl (he::tl), s) ->
let tl' =
List.map (fun t->RS.compute_to_stack
aux (k+1, m'::e, t, s)
| (_, _, C.Appl ([]|[_]), _) -> assert false
| (k, e, C.Appl (he::tl), s) ->
let tl' =
List.map (fun t->RS.compute_to_stack
- ~reduce:(reduce ~subst context) ~unwind (k,e,t,[])) tl
+ ~reduce:(reduce status ~subst context) ~unwind:(unwind status) (k,e,t,[])) tl
- let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
+ let _,_,body,_,_,_ = NCicEnvironment.get_checked_def status refer in
aux (0, [], body, s)
| (_, _, C.Const (Ref.Ref (_,
(Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config ->
aux (0, [], body, s)
| (_, _, C.Const (Ref.Ref (_,
(Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config ->
None -> config, true
| Some arg ->
let fixes,(_,_,pragma),_ =
None -> config, true
| Some arg ->
let fixes,(_,_,pragma),_ =
| (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
let new_s =
replace recindex s
| (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
let new_s =
replace recindex s
let _,_,_,_,body = List.nth fixes fixno in
aux (0, [], body, new_s)
| _ -> config, true)
let _,_,_,_,body = List.nth fixes fixno in
aux (0, [], body, new_s)
| _ -> config, true)
let decofix = function
| (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)->
let cofixes,_,_ =
let decofix = function
| (_,_,C.Const(Ref.Ref(_,Ref.CoFix c)as refer),s)->
let cofixes,_,_ =
let _,_,_,_,body = List.nth cofixes c in
let _,_,_,_,body = List.nth cofixes c in
- let c,_ = reduce ~delta:0 ~subst context (0,[],body,s) in
+ let c,_ = reduce status ~delta:0 ~subst context (0,[],body,s) in
c
| config -> config
in
let match_head = k,e,term,[] in
c
| config -> config
in
let match_head = k,e,term,[] in
(match decofix reduced with
| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
aux (k, e, List.nth pl (j-1), s)
(match decofix reduced with
| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
aux (k, e, List.nth pl (j-1), s)
- let whd ?(delta=0) ~subst context t =
- unwind (fst (reduce ~delta ~subst context (0, [], t, [])))
+ let whd status ?(delta=0) ~subst context t =
+ unwind status (fst (reduce status ~delta ~subst context (0, [], t, [])))
l1 l2
with Invalid_argument "List.for_all2" ->
prerr_endline ("Meta " ^ string_of_int n1 ^
" occurrs with local contexts of different lenght\n"^
l1 l2
with Invalid_argument "List.for_all2" ->
prerr_endline ("Meta " ^ string_of_int n1 ^
" occurrs with local contexts of different lenght\n"^
- NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
- NCicPp.ppterm ~metasenv ~subst ~context t2);
+ status#ppterm ~metasenv ~subst ~context t1 ^ " === " ^
+ status#ppterm ~metasenv ~subst ~context t2);
assert false) -> true
| C.Meta (n1,l1), _ ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
assert false) -> true
| C.Meta (n1,l1), _ ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
aux test_eq_only context term t2
with NCicUtils.Subst_not_found _ -> false)
| _, C.Meta (n2,l2) ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
aux test_eq_only context term t2
with NCicUtils.Subst_not_found _ -> false)
| _, C.Meta (n2,l2) ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
aux test_eq_only context t1 term
with NCicUtils.Subst_not_found _ -> false)
| (C.Appl ((C.Const r1) as hd1::tl1), C.Appl (C.Const r2::tl2))
when (Ref.eq r1 r2 &&
aux test_eq_only context t1 term
with NCicUtils.Subst_not_found _ -> false)
| (C.Appl ((C.Const r1) as hd1::tl1), C.Appl (C.Const r2::tl2))
when (Ref.eq r1 r2 &&
- List.length (E.get_relevance r1) >= List.length tl1) ->
- let relevance = E.get_relevance r1 in
+ List.length (E.get_relevance status r1) >= List.length tl1) ->
+ let relevance = E.get_relevance status r1 in
(* if the types were convertible the following optimization is sound
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
(* if the types were convertible the following optimization is sound
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let _,relevance = HExtlib.split_nth fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
let _,relevance = HExtlib.split_nth fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
| (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
aux test_eq_only context hd1 hd2 &&
| (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
aux test_eq_only context hd1 hd2 &&
| (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
C.Match (ref2,outtype2,term2,pl2)) ->
| (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
C.Match (ref2,outtype2,term2,pl2)) ->
- let _,_,itl,_,_ = E.get_checked_indtys ref1 in
+ let _,_,itl,_,_ = E.get_checked_indtys status ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
match ty with
| C.Sort _ -> ty
| C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta
match ty with
| C.Sort _ -> ty
| C.Prod (name,so,ta) -> remove_prods ~subst ((name,(C.Decl so))::context) ta
(is_prop || aux test_eq_only context term1 term2) &&
(try List.for_all2 (aux test_eq_only context) pl1 pl2
with Invalid_argument _ -> false)
(is_prop || aux test_eq_only context term1 term2) &&
(try List.for_all2 (aux test_eq_only context) pl1 pl2
with Invalid_argument _ -> false)
- | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | (C.Implicit _, _) | (_, C.Implicit _) -> true
+ (* CSC: was assert false, but it happens when looking for coercions
+ during pretty printing of terms yet to be refined *)
- let alpha_eq test_eq_only =
- alpha_eq ~test_lambda_source:false aux test_eq_only metasenv subst context
+ let alpha_eq status test_eq_only =
+ alpha_eq status ~test_lambda_source:false aux test_eq_only metasenv subst
+ context
- R.reduce ~delta:max_int ~subst context m1,
- R.reduce ~delta:max_int ~subst context m2
+ R.reduce status ~delta:max_int ~subst context m1,
+ R.reduce status ~delta:max_int ~subst context m2
in
let small_delta_step
((_,_,t1,_ as m1), norm1 as x1) ((_,_,t2,_ as m2), norm2 as x2)
=
assert(not (norm1 && norm2));
if norm1 then
in
let small_delta_step
((_,_,t1,_ as m1), norm1 as x1) ((_,_,t2,_ as m2), norm2 as x2)
=
assert(not (norm1 && norm2));
if norm1 then
- R.reduce ~delta ~subst context m1,
- R.reduce ~delta ~subst context m2
+ R.reduce status ~delta ~subst context m1,
+ R.reduce status ~delta ~subst context m2
in
let rec convert_machines test_eq_only
((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2)
=
in
let rec convert_machines test_eq_only
((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2)
=
- (alpha_eq test_eq_only
- (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
+ (alpha_eq status test_eq_only
+ (R.unwind status (k1,e1,t1,[])) (R.unwind status (k2,e2,t2,[])) &&
| _, C.Meta (n,ctx), _ ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in
| _, C.Meta (n,ctx), _ ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in
| _, C.Lambda(_,_,bo), arg::tl ->
| _, C.Lambda(_,_,bo), arg::tl ->
- let bo = NCicSubstitution.subst arg bo in
- head_beta_reduce ~delta ~upto:(upto - 1) ~subst bo tl
+ let bo = NCicSubstitution.subst status arg bo in
+ head_beta_reduce status ~delta ~upto:(upto - 1) ~subst bo tl
| _, C.Const (Ref.Ref (_, Ref.Def height) as re), _
when delta <= height ->
| _, C.Const (Ref.Ref (_, Ref.Def height) as re), _
when delta <= height ->
- let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
- head_beta_reduce ~upto ~delta ~subst bo l
+ let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status re in
+ head_beta_reduce status ~upto ~delta ~subst bo l
-let head_beta_reduce ?(delta=max_int) ?(upto= -1) ?(subst=[]) t =
- head_beta_reduce ~delta ~upto ~subst t []
+let head_beta_reduce status ?(delta=max_int) ?(upto= -1) ?(subst=[]) t =
+ head_beta_reduce status ~delta ~upto ~subst t []
- NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
- NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
+ NCicUtils.set_head_beta_reduce
+ (fun status ~upto t -> head_beta_reduce status ~upto t);
-let rec split_prods ~subst context n te =
- match (n, R.whd ~subst context te) with
+let rec split_prods status ~subst context n te =
+ match (n, R.whd status ~subst context te) with
| (0, _) -> context,te
| (n, C.Sort _) when n <= 0 -> context,te
| (n, C.Prod (name,so,ta)) ->
| (0, _) -> context,te
| (n, C.Sort _) when n <= 0 -> context,te
| (n, C.Prod (name,so,ta)) ->