- | NCic.Implicit (`Typeof _) ->
- (let ty_t =
- try
- t (*
- NCicTypeChecker.typeof ~subst ~metasenv context t*)
- with
- NCicTypeChecker.AssertFailure msg ->
- let exc_to_be =
- fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
- pp (lazy "fine typeof (fallimento)");
- let ft = fix_sorts swap exc_to_be t in
- if ft == t then
- (prerr_endline ( ("ILLTYPED: " ^
- NCicPp.ppterm ~metasenv ~subst ~context t
- ^ "\nBECAUSE:" ^ Lazy.force msg ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv
- ));
- assert false)
- else
- (try
- pp (lazy ("typeof: " ^
- NCicPp.ppterm ~metasenv ~subst ~context ft));
- NCicTypeChecker.typeof ~subst ~metasenv context ft
- with NCicTypeChecker.AssertFailure _ ->
- assert false)
- | NCicTypeChecker.TypeCheckerFailure _ -> assert false
- in
- match NCicReduction.whd ~subst context ty_t with
- NCic.Sort _ -> metasenv,subst, t
- | NCic.Meta _ -> metasenv,subst,t (* CSC: TO BE IMPLEMENTED *)
- | _ -> raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term")))
- (*CSC: TO BE IMPLEMENTED: UnificationFailure of string Lazy.t;; *)
- (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
+ | NCic.Implicit (`Typeof _) ->
+ (match NCicReduction.whd ~subst context t with
+ NCic.Sort _ -> metasenv,subst,t
+ | NCic.Meta (i,_) when
+ let _,_,ty = NCicUtils.lookup_meta i metasenv in
+ (match ty with
+ NCic.Implicit (`Typeof _) -> true
+ | _ -> false)
+ -> metasenv,subst,t
+ | NCic.Meta (i,_) ->
+ let rec remove_and_hope i =
+ let _,ctx,ty = NCicUtils.lookup_meta i metasenv in
+ match ty with
+ NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv
+ | _ ->
+ match NCicReduction.whd ~subst ctx ty with
+ NCic.Meta (j,_) ->
+ let metasenv = remove_and_hope j in
+ List.filter (fun i',_ -> i <> i') metasenv
+ | _ -> assert false (* NON POSSO RESTRINGERE *)
+ in
+ let metasenv = remove_and_hope i in
+ let metasenv =
+ (i,(None,[],NCic.Implicit (`Typeof i)))::
+ List.filter (fun i',_ -> i <> i') metasenv
+ in
+ metasenv,subst,t
+ | NCic.Appl (NCic.Meta _::_) ->
+ raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+ | t when could_reduce t ->
+ raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+ | _ ->
+ raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))