- metasenv, subst, NCic.Lambda (name, telescopic_ty, bo)
- in
- pp(lazy("LAMBDA_INTROS{ " ^
- NCicPp.ppterm ~metasenv ~subst ~context t ^ ":" ^
- NCicPp.ppterm ~metasenv ~subst ~context tty ^ " over " ^
- String.concat "," (List.map (NCicPp.ppterm ~metasenv ~subst ~context)args)));
- let rc = mk_lambda metasenv subst context 0 [] argsty in
- pp(lazy("LAMBDA_INTROS}"));
- rc
-
-and instantiate rdb test_eq_only metasenv subst context n lc t swap =
- (*D*) inside 'I'; try let rc =
- pp (lazy(string_of_int n ^ " :=?= "^
- NCicPp.ppterm ~metasenv ~subst ~context t));
- let unify test_eq_only m s c t1 t2 =
- if swap then unify rdb test_eq_only m s c t2 t1
- else unify rdb test_eq_only m s c t1 t2
- in
- let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
- let metasenv, subst, t =
- match ty with
- | 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 *)
- | _ ->
- pp (lazy (
- "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv));
- let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
- let t, ty_t =
- try t, NCicTypeChecker.typeof ~subst ~metasenv context t
- with
- | NCicTypeChecker.AssertFailure msg ->
- (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));
- ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
- with NCicTypeChecker.AssertFailure _ ->
- assert false)
- | NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (Lazy.force msg);
- prerr_endline (
- "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
- ppcontext ~metasenv ~subst context ^
- ppmetasenv ~subst metasenv);
- pp msg; assert false
- in
- let lty = NCicSubstitution.subst_meta lc ty in
- match ty_t with
- | NCic.Implicit _ ->
- raise (UnificationFailure
- (lazy "trying to unify a term with a type"))
- | ty_t ->
- pp (lazy ("On the types: " ^
- NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
- NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
- ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
- let metasenv,subst =
- try
- unify test_eq_only metasenv subst context lty ty_t
- with NCicEnvironment.BadConstraint _ as exc ->
- let ty_t = fix_sorts swap exc_to_be ty_t in
- try unify test_eq_only metasenv subst context lty ty_t
- with _ -> raise exc in
- metasenv, subst, t
+ metasenv, bo
+ | _ ->
+ (match NCicReduction.whd ~subst context ty with
+ C.Prod (n,so,ta) ->
+ let metasenv,bo =
+ lambda_intros rdb metasenv subst
+ ((n,C.Decl so)::context) (argsno - 1) ta
+ in
+ metasenv,C.Lambda (n,so,bo)
+ | _ -> assert false)
+;;
+
+let unopt exc = function None -> raise exc | Some x -> x ;;
+
+let fix metasenv subst is_sup test_eq_only exc t =
+ (*D*) inside 'f'; try let rc =
+ pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context:[] t));
+ let rec aux test_eq_only metasenv = function
+ | NCic.Prod (n,so,ta) ->
+ let metasenv,so = aux true metasenv so in
+ let metasenv,ta = aux test_eq_only metasenv ta in
+ metasenv,NCic.Prod (n,so,ta)
+ | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
+ metasenv,orig
+ | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
+ | NCic.Sort (NCic.Type u) when is_sup ->
+ metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+ | NCic.Sort (NCic.Type u) ->
+ metasenv, NCic.Sort (NCic.Type
+ (unopt exc (NCicEnvironment.inf ~strict:false u)))
+ | NCic.Meta (n,_) as orig ->
+ (try
+ let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
+ with NCicUtils.Subst_not_found _ ->
+ let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
+ metasenv, orig)
+ | t ->
+ NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t