let (===) x y = Pervasives.compare x y = 0 ;;
+let uncert_exc metasenv subst context t1 t2 =
+ Uncertain (lazy (
+ "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
+ " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
+;;
+
let fail_exc metasenv subst context t1 t2 =
UnificationFailure (lazy (
"Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
with WrongShape -> orig
in
function
- | NCic.Lambda(name, src, NCic.Appl [hd; NCic.Rel 1]) as orig ->
+ | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
delift_if_not_occur hd orig
- | NCic.Lambda(name, src, NCic.Appl (hd :: l)) as orig
+ | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
when HExtlib.list_last l = NCic.Rel 1 ->
let body =
- let args, _ = Hextlib.split_nth (List.length l - 1) l in
+ let args, _ = HExtlib.split_nth (List.length l - 1) l in
NCic.Appl (hd::args)
in
delift_if_not_occur body orig
| t -> t
;;
-
+
+module C = NCic;;
+module Ref = NReference;;
+
let rec beta_expand num test_eq_only swap metasenv subst context t arg =
let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
try
let metasenv, subst =
- unify test_eq_only metasenv subst context
- (NCicSubstitution.lift n arg) t'
+ if swap then
+ unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
+ else
+ unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
in
- (metasenv, subst), C.Rel (1 + n)
+ (metasenv, subst), NCic.Rel (1 + n)
with Uncertain _ | UnificationFailure _ ->
match t' with
- | NCic.Rel m orig ->
+ | NCic.Rel m as orig ->
(metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
(* andrea: in general, beta_expand can create badly typed
terms. This happens quite seldom in practice, UNLESS we
| NCic.Prod (name, src, tgt) as orig ->
let (metasenv, subst), src1 = aux (n,context,true) acc src in
let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
- let (metasenv,subst), tgt1 = aux k (metasenv, subst) tgt in
- if src == src1 && tgt == tgt1 then orig else
- NCic.Prod (name, src1, tgt1)
+ let ms, tgt1 = aux k (metasenv, subst) tgt in
+ if src == src1 && tgt == tgt1 then ms, orig else
+ ms, NCic.Prod (name, src1, tgt1)
| t ->
NCicUntrusted.map_term_fold_a
- (fun e (n,ctx) -> n+1,e::ctx) k aux acc t
+ (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
in
let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
let fresh_name = "Hbeta" ^ string_of_int num in
- let (metasenv,subst,_), t1 =
+ let (metasenv,subst), t1 =
aux (0, context, test_eq_only) (metasenv, subst) t in
- let t2 = eta_reduce (C.Lambda (fresh_name,argty,t1)) in
+ let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
try
ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
metasenv, subst, t2
with NCicTypeChecker.TypeCheckerFailure _ ->
- NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
+ metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
-and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+and beta_expand_many test_equality_only swap metasenv subst context t args =
let _, subst, metasenv, hd =
List.fold_right
(fun arg (num,subst,metasenv,t) ->
- let subst, metasenv, t =
- beta_expand num test_equality_only metasenv subst context t arg
+ let metasenv, subst, t =
+ beta_expand num test_equality_only swap metasenv subst context t arg
in
num+1,subst,metasenv,t)
args (1,subst,metasenv,t)
metasenv, subst, hd
and instantiate test_eq_only metasenv subst context n lc t swap =
- let unif m s c t1 t2 =
- if swap then unify m s c t2 t1 else unify m s c t1 t2
+ let unify test_eq_only m s c t1 t2 =
+ if swap then unify test_eq_only m s c t2 t1
+ else unify test_eq_only m s c t1 t2
in
let ty_t =
try NCicTypeChecker.typeof ~subst ~metasenv context t
in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
let ty = NCicSubstitution.subst_meta lc ty in
- let metasenv, subst = unify metasenv susbt context ty ty_t in
+ let metasenv, subst = unify test_eq_only metasenv subst context ty ty_t in
let (metasenv, subst), t =
NCicMetaSubst.delift metasenv subst context n lc t
in
(* Unifying the types may have already instantiated n. *)
try
- let _, _,oldt,_ = CicUtil.lookup_subst n subst in
+ let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
let oldt = NCicSubstitution.subst_meta lc oldt in
(* conjecture: always fail --> occur check *)
unify test_eq_only metasenv subst context oldt t
- with CicUtil.Subst_not_found _ ->
+ with NCicUtils.Subst_not_found _ ->
(* by cumulativity when unify(?,Type_i)
* we could ? := Type_j with j <= i... *)
let subst = (n, (name, ctx, t, ty)) :: subst in
let metasenv =
List.filter (fun (m,_) -> not (n = m)) metasenv
in
- subst, metasenv
+ metasenv, subst
-and unify metasenv subst context t1 t2 =
- let rec aux test_eq_only metasenv subst context t1 t2 =
+and unify test_eq_only metasenv subst context t1 t2 =
let fo_unif test_eq_only metasenv subst t1 t2 =
if t1 === t2 then
metasenv, subst
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
- let metasenv, subst = aux true metasenv subst context s1 s2 in
- aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
+ let metasenv, subst = unify true metasenv subst context s1 s2 in
+ unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
| (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
- let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
- let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
+ let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
+ let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
let context = (name1, C.Def (s1,ty1))::context in
- aux test_eq_only metasenv subst context t1 t2
+ unify test_eq_only metasenv subst context t1 t2
| (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
(try
List.fold_right2
(fun t1 t2 (metasenv, subst, to_restrict, i) ->
try
- aux test_eq_only metasenv subst context
- (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2),
- to_restrict, i-1
+ let metasenv, subst =
+ unify test_eq_only metasenv subst context
+ (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
+ in
+ metasenv, subst, to_restrict, i-1
with UnificationFailure _ | Uncertain _ ->
metasenv, subst, i::to_restrict, i-1)
l1 l2 (metasenv, subst, [], List.length l1)
let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
let term1 = NCicSubstitution.subst_meta lc1 term in
let term2 = NCicSubstitution.subst_meta lc2 term in
- aux test_eq_only metasenv subst context term1 term2
+ unify test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
| C.Meta (n,lc), t ->
- try
+ (try
let _,_,term,_ = NCicUtils.lookup_subst n subst in
let term = NCicSubstitution.subst_meta lc term in
- aux test_eq_only metasenv subst context term t
+ unify test_eq_only metasenv subst context term t
with NCicUtils.Subst_not_found _->
- instantiate test_eq_only metasenv subst context n lc t false
+ instantiate test_eq_only metasenv subst context n lc t false)
| t, C.Meta (n,lc) ->
- try
+ (try
let _,_,term,_ = NCicUtils.lookup_subst n subst in
let term = NCicSubstitution.subst_meta lc term in
- aux test_eq_only metasenv subst context t term
+ unify test_eq_only metasenv subst context t term
with NCicUtils.Subst_not_found _->
- instantiate test_eq_only metasenv subst context n lc t true
+ instantiate test_eq_only metasenv subst context n lc t true)
| NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- aux test_eq_only metasenv subst context (mk_appl term args) t2
+ unify test_eq_only metasenv subst context (mk_appl term args) t2
| _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
let _,_,term,_ = NCicUtils.lookup_subst i subst in
let term = NCicSubstitution.subst_meta l term in
- aux test_eq_only metasenv subst context t1 (mk_appl term args)
+ unify test_eq_only metasenv subst context t1 (mk_appl term args)
| NCic.Appl (NCic.Meta (i,_)::_ as l1),
NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
- try
+ (try
List.fold_left2
(fun (metasenv, subst) t1 t2 ->
- aux test_eq_only metasenv subst context t1 t2)
+ unify test_eq_only metasenv subst context t1 t2)
(metasenv,subst) l1 l2
with Invalid_argument _ ->
- raise (fail_exc metasenv subst context t1 t2)
+ raise (fail_exc metasenv subst context t1 t2))
| NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
(* we verify that none of the args is a Meta,
since beta expanding w.r.t a metavariable makes no sense *)
- let subst, metasenv, beta_expanded =
- beta_expand_many (* passare swap *)
- test_equality_only metasenv subst context t2 args ugraph
+ let metasenv, subst, beta_expanded =
+ beta_expand_many
+ test_eq_only false
+ metasenv subst context t2 args
in
- aux test_eq_only metasenv subst context
+ unify test_eq_only metasenv subst context
(C.Meta (i,l)) beta_expanded
+
| _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
- let subst,metasenv,beta_expanded =
- beta_expand_many
- test_equality_only
- metasenv subst context t1 args ugraph
- in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded ugraph1
- | _,_ ->
-.......
+ let metasenv, subst, beta_expanded =
+ beta_expand_many
+ test_eq_only true
+ metasenv subst context t1 args
+ in
+ unify test_eq_only metasenv subst context
+ beta_expanded (C.Meta (i,l))
+
+ (* processing this case here we avoid a useless small delta step *)
| (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
- let relevance = match r1 with
+ when Ref.eq r1 r2 ->
+ let relevance = NCicEnvironment.get_relevance r1 in
+ let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let _,relevance = HExtlib.split_nth lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
- in
- let fail = ref ~-1 in
- let res = (try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
- in res
- (* if res then true
- else
- let relevance = get_relevance_p ~subst context _hd1 tl1 in
- let _,relevance = HExtlib.split_nth !fail relevance in
- let b,relevance = (match relevance with
- | [] -> assert false
- | b::tl -> b,tl) in
- let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
- let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
- if (not b) then
- (dance ();
- try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
- else false *)
- | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
- aux test_eq_only context hd1 hd2 &&
- let relevance = get_relevance ~subst context hd1 tl1 in
- (try
- HExtlib.list_forall_default3
- (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
- tl1 tl2 true relevance
- with Invalid_argument _ -> false)
+ in
+ let metasenv, subst, _ =
+ try
+ List.fold_left2
+ (fun (metasenv, subst, relevance) t1 t2 ->
+ let b, relevance =
+ match relevance with b::tl -> b,tl | _ -> true, [] in
+ let metasenv, subst =
+ try unify test_eq_only metasenv subst context t1 t2
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ metasenv, subst, relevance)
+ (metasenv, subst, relevance) tl1 tl2
+ with Invalid_argument _ ->
+ raise (uncert_exc metasenv subst context t1 t2)
+ in
+ metasenv, subst
| (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,_,_ = NCicEnvironment.get_checked_indtys ref1 in
let _,_,ty,_ = List.nth itl tyno in
let rec remove_prods ~subst context ty =
- let ty = whd ~subst context ty in
+ let ty = NCicReduction.whd ~subst context ty in
match ty with
| C.Sort _ -> ty
| C.Prod (name,so,ta) ->
| _ -> false
in
let rec remove_prods ~subst context ty =
- let ty = whd ~subst context ty in
+ let ty = NCicReduction.whd ~subst context ty in
match ty with
| C.Sort _ -> ty
| C.Prod (name,so,ta) ->
raise (uncert_exc metasenv subst context t1 t2)
else
let metasenv, subst =
- aux test_eq_only metasenv subst context outtype1 outtype2 in
+ unify test_eq_only metasenv subst context outtype1 outtype2 in
let metasenv, subst =
- try aux test_eq_only metasenv subst context term1 term2
+ try unify test_eq_only metasenv subst context term1 term2
with UnificationFailure _ | Uncertain _ when is_prop ->
metasenv, subst
in
- try
+ (try
List.fold_left2
- (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
+ (fun (metasenv,subst) ->
+ unify test_eq_only metasenv subst context)
(metasenv, subst) pl1 pl2
with Invalid_argument _ ->
- raise (uncert_exc metasenv subst context t1 t2)
+ raise (uncert_exc metasenv subst context t1 t2))
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| _ -> raise (uncert_exc metasenv subst context t1 t2)
in
+ let height_of = function
+ | NCic.Const (Ref.Ref (_,Ref.Def h))
+ | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+ | NCic.Meta _ -> max_int
+ | _ -> 0
+ in
+ let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
+ let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+ NCicReduction.reduce_machine ~delta ~subst context m1,
+ NCicReduction.reduce_machine ~delta ~subst context m2,
+ delta
+ in
let rec unif_machines metasenv subst = function
- | ((k1,e1,NCic.Meta _ as t1,s1 as m1),(k2,e2,t2,s2 as m2),delta)
- | ((k1,e1,t1,s1 as m1),(k2,e2,NCic.Meta _ as t2,s2 as m2),delta) ->
- try
- fo_unif test_eq_only metasenv subst (R.unwind m1) (R.unwind m2)
- with UnificationFailure _ | Uncertain _ when delta > 0 ->
- let delta = delta - 1 in
- let red = R.reduce ~delta ~subst context in
- unif_machines metasenv subst (red m1,red m2,delta)
| ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
try
- let metasenv, subst =
- fo_unif test_eq_only metasenv subst
- (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[]))
- in
- let relevance =
+ let relevance = [] (* TO BE UNDERSTOOD
match t1 with
| C.Const r -> NCicEnvironment.get_relevance r
- | _ -> [] in
- try
- let rec check_stack f l1 l2 r a =
- match l1,l2,r with
- | x1::tl1, x2::tl2, r::tr ->
- check_stack f tl1 tl2 tr (f x1 x2 r a)
- | x1::tl1, x2::tl2, [] ->
- check_stack f tl1 tl2 tr (f x1 x2 true a)
- | [], [], _ -> a
- | _ -> raise (Invalid_argument "check_stack")
- in
- check_stack
- (fun t1 t2 b (metasenv,subst) ->
- try
- let t1 = RS.from_stack t1 in
- let t2 = RS.from_stack t2 in
- unif_machines metasenv subst (small_delta_step t1 t2)
- with UnificationFailure _ | Uncertain _ when not b ->
- metasenv, subst)
- s1 s2 relevance (metasenv,subst)
- with Invalid_argument _ ->
- raise (UnificationFailure (lazy ( "Can't unify " ^ NCicPp.ppterm
- ~metasenv ~subst ~context (R.unwind m1) ^ " with " ^ NCicPp.ppterm
- ~metasenv ~subst ~context (R.unwind m2))))
+ | _ -> [] *) in
+ let unif_from_stack t1 t2 b metasenv subst =
+ try
+ let t1 = NCicReduction.from_stack t1 in
+ let t2 = NCicReduction.from_stack t2 in
+ unif_machines metasenv subst (small_delta_step t1 t2)
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ let rec check_stack l1 l2 r (metasenv, subst) =
+ match l1,l2,r with
+ | x1::tl1, x2::tl2, r::tr ->
+ check_stack tl1 tl2 tr
+ (unif_from_stack x1 x2 r metasenv subst)
+ | x1::tl1, x2::tl2, [] ->
+ check_stack tl1 tl2 []
+ (unif_from_stack x1 x2 true metasenv subst)
+ | l1, l2, _ ->
+ fo_unif test_eq_only metasenv subst
+ (NCicReduction.unwind (k1,e1,t1,List.rev l1))
+ (NCicReduction.unwind (k2,e2,t2,List.rev l2))
+ in
+ check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
with UnificationFailure _ | Uncertain _ when delta > 0 ->
let delta = delta - 1 in
- let red = R.reduce ~delta ~subst context in
+ let red = NCicReduction.reduce_machine ~delta ~subst context in
unif_machines metasenv subst (red m1,red m2,delta)
in
- let height_of = function
- | NCic.Const (Ref.Ref (_,Ref.Def h))
- | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
- | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
- | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
- | NCic.Meta _ -> max_int
- | _ -> 0
- in
- let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
- let h1 = height_of t1 in
- let h2 = height_of t2 in
- let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
- R.reduce ~delta ~subst context m1,
- R.reduce ~delta ~subst context m2,
- delta
- in
try fo_unif test_eq_only metasenv subst t1 t2
- with UnificationFailure msg |Uncertain msg as exn ->
+ with UnificationFailure msg |Uncertain msg as exn
+ when not (flexible [t1;t2]) ->
try
unif_machines metasenv subst
(small_delta_step (0,[],t1,[]) (0,[],t2,[]))
with
| UnificationFailure _ -> raise (UnificationFailure msg)
| Uncertain _ -> raise exn
- in
- aux false metasenv subst context t1 t2
;;
+let unify = unify false;;
+
(*
projects / helm.git / commitdiff