let type_of_aux' metasenv subst context term =
try
CicMetaSubst.type_of_aux' metasenv subst context term
- with CicMetaSubst.MetaSubstFailure msg ->
+ with
+ | CicMetaSubst.MetaSubstFailure msg ->
raise (AssertFailure
((sprintf
"Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
- (CicPp.ppterm (CicMetaSubst.apply_subst subst term))
+ (CicMetaSubst.ppterm subst term)
(CicMetaSubst.ppcontext subst context) msg)))
(* NUOVA UNIFICAZIONE *)
fo_unif_subst subst context metasenv t2 t1
| (C.Meta (n,l), t)
| (t, C.Meta (n,l)) ->
- let subst',metasenv' =
+ let subst'',metasenv' =
try
let oldt = (List.assoc n subst) in
let lifted_oldt = S.lift_meta l oldt in
fo_unif_subst subst context metasenv lifted_oldt t
with Not_found ->
- let t',metasenv' = CicMetaSubst.delift context metasenv l t in
- (n, t')::subst, metasenv'
+ let t',metasenv',subst' =
+ CicMetaSubst.delift n subst context metasenv l t
+ in
+ (n, t')::subst', metasenv'
in
- let (_,_,meta_type) =
- List.find (function (m,_,_) -> m=n) metasenv' in
- let tyt = type_of_aux' metasenv' subst' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in
+ (try
+ let tyt =
+ type_of_aux' metasenv' subst'' context t
+ in
+ fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
+ with CicTypeChecker.SortExpectedMetaFound _ ->
+ (* 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'))
| (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
(* a new substitution which is already unwinded and ready to be applied and *)
(* a new metasenv in which some hypothesis in the contexts of the *)
(* metavariables may have been restricted. *)
-let fo_unif metasenv context t1 t2 =
- let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
- CicMetaSubst.unwind_subst metasenv' subst_to_unwind
-;;
+let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;;
let fo_unif_subst subst context metasenv t1 t2 =
let enrich_msg msg =
sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
- (CicPp.ppterm (CicMetaSubst.apply_subst subst t1))
+ (CicMetaSubst.ppterm subst t1)
(try
CicPp.ppterm (type_of_aux' metasenv subst context t1)
with _ -> "MALFORMED")
- (CicPp.ppterm (CicMetaSubst.apply_subst subst t2))
+ (CicMetaSubst.ppterm subst t2)
(try
CicPp.ppterm (type_of_aux' metasenv subst context t2)
with _ -> "MALFORMED")
(CicMetaSubst.ppcontext subst context)
- (CicMetaSubst.ppmetasenv subst metasenv) msg
+ (CicMetaSubst.ppmetasenv metasenv subst) msg
in
try
fo_unif_subst subst context metasenv t1 t2