-and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let t1 = deref subst t1 in
- let t2 = deref subst t2 in
- let (&&&) a b = (a && b) || ((not a) && (not b)) in
-(* let bef = Sys.time () in *)
- let b,ugraph =
- if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
- false,ugraph
- else
-let foo () =
- R.are_convertible ~subst ~metasenv context t1 t2 ugraph
-in profiler_are_convertible.HExtlib.profile foo ()
- in
-(* let aft = Sys.time () in
-if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
-CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
-CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
- if b then
- subst, metasenv, ugraph
- else
- match (t1, t2) with
- | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
- let _,subst,metasenv,ugraph1 =
- (try
- List.fold_left2
- (fun (j,subst,metasenv,ugraph) t1 t2 ->
- match t1,t2 with
- None,_
- | _,None -> j+1,subst,metasenv,ugraph
- | Some t1', Some t2' ->
- (* First possibility: restriction *)
- (* Second possibility: unification *)
- (* Third possibility: convertibility *)
- let b, ugraph1 =
- R.are_convertible
- ~subst ~metasenv context t1' t2' ugraph
- in
- if b then
- j+1,subst,metasenv, ugraph1
- else
- (try
- let subst,metasenv,ugraph2 =
- fo_unif_subst
- test_equality_only
- subst context metasenv t1' t2' ugraph
- in
- j+1,subst,metasenv,ugraph2
- with
- Uncertain _
- | UnificationFailure _ ->
-debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
- let metasenv, subst =
- CicMetaSubst.restrict
- subst [(n,j)] metasenv in
- j+1,subst,metasenv,ugraph1)
- ) (1,subst,metasenv,ugraph) ln lm
- with
- Exit ->
- raise
- (UnificationFailure (lazy "1"))
- (*
- (sprintf
- "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))) *)
- | Invalid_argument _ ->
- raise
- (UnificationFailure (lazy "2")))
- (*
- (sprintf
- "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
- in subst,metasenv,ugraph1
- | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
- fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
- | (C.Meta (n,l), t)
- | (t, C.Meta (n,l)) ->
- let swap =
- match t1,t2 with
- C.Meta (n,_), C.Meta (m,_) when n < m -> false
- | _, C.Meta _ -> false
- | _,_ -> true
- in
- let lower = fun x y -> if swap then y else x in
- let upper = fun x y -> if swap then x else y in
- let fo_unif_subst_ordered
- test_equality_only subst context metasenv m1 m2 ugraph =
- fo_unif_subst test_equality_only subst context metasenv
- (lower m1 m2) (upper m1 m2) ugraph
- in
- begin
- let subst,metasenv,ugraph1 =
- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
- (try
- let tyt,ugraph1 =
- type_of_aux' metasenv subst context t ugraph
- in
- fo_unif_subst
- test_equality_only
- subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
- with
- UnificationFailure _ as e -> raise e
- | Uncertain msg -> raise (UnificationFailure msg)
- | AssertFailure _ ->
- debug_print (lazy "siamo allo huge hack");
- (* TODO huge hack!!!!
- * we keep on unifying/refining in the hope that
- * the problem will be eventually solved.
- * In the meantime we're breaking a big invariant:
- * the terms that we are unifying are no longer well
- * typed in the current context (in the worst case
- * we could even diverge) *)
- (subst, metasenv,ugraph)) in
- let t',metasenv,subst =
- try
- CicMetaSubst.delift n subst context metasenv l t
- with
- (CicMetaSubst.MetaSubstFailure msg)->
- raise (UnificationFailure msg)
- | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
- in
- let t'',ugraph2 =
- match t' with
- C.Sort (C.Type u) when not test_equality_only ->
- let u' = CicUniv.fresh () in
- let s = C.Sort (C.Type u') in
- (try
- let ugraph2 =
- CicUniv.add_ge (upper u u') (lower u u') ugraph1
- in
- s,ugraph2
- with
- CicUniv.UniverseInconsistency msg ->
- raise (UnificationFailure msg))
- | _ -> t',ugraph1
- in
- (* Unifying the types may have already instantiated n. Let's check *)
- try
- let (_, oldt,_) = CicUtil.lookup_subst n subst in
- let lifted_oldt = S.subst_meta l oldt in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt ugraph2
- with
- CicUtil.Subst_not_found _ ->
- let (_, context, ty) = CicUtil.lookup_meta n metasenv in
- let subst = (n, (context, t'',ty)) :: subst in
- let metasenv =
- List.filter (fun (m,_,_) -> not (n = m)) metasenv in
- subst, metasenv, ugraph2
- end
- | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
- | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
- if UriManager.eq uri1 uri2 then
- fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
- exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure (lazy
- (sprintf
- "Can't unify %s with %s due to different constants"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
- if UriManager.eq uri1 uri2 && i1 = i2 then
- fo_unif_subst_exp_named_subst
- test_equality_only
- subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s due to different inductive principles"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
- C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
- if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
- fo_unif_subst_exp_named_subst
- test_equality_only
- subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s due to different inductive constructors"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
- | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
- subst context metasenv te t2 ugraph
- | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
- subst context metasenv t1 te ugraph
- | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
- in
- fo_unif_subst test_equality_only
- subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
- | (C.LetIn (_,s1,ty1,t1), t2)
- | (t2, C.LetIn (_,s1,ty1,t1)) ->
- fo_unif_subst
- test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
- | (C.Appl l1, C.Appl l2) ->
- (* andrea: this case should be probably rewritten in the
- spirit of deref *)
- (match l1,l2 with
- | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
- (try
- List.fold_left2
- (fun (subst,metasenv,ugraph) t1 t2 ->
- fo_unif_subst
- test_equality_only subst context metasenv t1 t2 ugraph)
- (subst,metasenv,ugraph) l1 l2
- with (Invalid_argument msg) ->
- raise (UnificationFailure (lazy msg)))
- | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
- (* we verify that none of the args is a Meta,
- since beta expanding with respoect to a metavariable
- makes no sense *)
- (*
- (try
- let (_,t,_) = CicUtil.lookup_subst i subst in
- let lifted = S.subst_meta l t in
- let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
- fo_unif_subst
- test_equality_only
- subst context metasenv reduced t2 ugraph
- with CicUtil.Subst_not_found _ -> *)
- let subst,metasenv,beta_expanded,ugraph1 =
- beta_expand_many
- test_equality_only metasenv subst context t2 args ugraph
- in
- fo_unif_subst test_equality_only subst context metasenv
- (C.Meta (i,l)) beta_expanded ugraph1
- | _, C.Meta (i,l)::args when not(exists_a_meta args) ->
- (* (try
- let (_,t,_) = CicUtil.lookup_subst i subst in
- let lifted = S.subst_meta l t in
- let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
- fo_unif_subst
- test_equality_only
- subst context metasenv t1 reduced ugraph
- with CicUtil.Subst_not_found _ -> *)
- let subst,metasenv,beta_expanded,ugraph1 =
- beta_expand_many
- test_equality_only
- metasenv subst context t1 args ugraph
+ | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+ (try
+ let l1 = NCicUtils.expand_local_context l1 in
+ let l2 = NCicUtils.expand_local_context l2 in
+ let metasenv, subst, to_restrict, _ =
+ List.fold_right2
+ (fun t1 t2 (metasenv, subst, to_restrict, i) ->
+ try
+ let metasenv, subst =
+ unify hdb 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)
+ in
+ if to_restrict <> [] then
+ let metasenv, subst, _ =
+ NCicMetaSubst.restrict metasenv subst n1 to_restrict
+ in
+ metasenv, subst
+ else metasenv, subst
+ with
+ | Invalid_argument _ -> assert false
+ | NCicMetaSubst.MetaSubstFailure msg ->
+ try
+ let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+ let term1 = NCicSubstitution.subst_meta lc1 term in
+ let term2 = NCicSubstitution.subst_meta lc2 term in
+ unify hdb test_eq_only metasenv subst context term1 term2
+ with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+ | _, NCic.Meta (n, _) when is_locked n subst ->
+ (let (metasenv, subst), i =
+ match NCicReduction.whd ~subst context t1 with
+ | NCic.Appl (NCic.Meta (i,l)::args) when
+ not (NCicMetaSubst.flexible subst args)
+ ->
+ let metasenv, lambda_Mj =
+ lambda_intros metasenv subst context t1 args