- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
- (try
- let tyt =
- type_of_aux' metasenv subst context t
- in
- fo_unif_subst
- test_equality_only
- subst context metasenv tyt (S.lift_meta l meta_type)
- with AssertFailure _ ->
- (* 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)
- *)
-(*
-prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
-prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
-*)
- (subst, metasenv))
- 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'' =
- 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
- ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
- s
- | _ -> t'
- in
- (* Unifying the types may have already instantiated n. Let's check *)
- try
- let oldt = (List.assoc n subst) in
- let lifted_oldt = S.lift_meta l oldt in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt
- with
- Not_found ->
- (n,t'')::subst, metasenv
- end
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
+ (try
+ let tyt = type_of_aux' metasenv subst context t in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv tyt (S.lift_meta l meta_type)
+ with
+ UnificationFailure msg
+ | Uncertain msg ->
+ prerr_endline msg;raise (UnificationFailure msg)
+ | AssertFailure _ ->
+ prerr_endline "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)) 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'' =
+ 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
+ ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
+ s
+ | _ -> t'
+ 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.lift_meta l oldt in
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt
+ with
+ CicUtil.Subst_not_found _ ->
+ let (_, context, _) = CicUtil.lookup_meta n metasenv in
+ let subst = (n, (context, t'')) :: subst in
+ let metasenv =
+ List.filter (fun (m,_,_) -> not (n = m)) metasenv in
+ subst, metasenv
+ end