let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
+
(*
let pp s =
prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
;;
*)
+
let pp _ = ();;
let wrap_exc msg = function
;;
-let check_allowed_sort_elimination localise r orig =
+let check_allowed_sort_elimination hdb localise r orig =
let mkapp he arg =
match he with
| C.Appl l -> C.Appl (l @ [arg])
NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type
in
let metasenv, subst =
- try NCicUnification.unify metasenv subst context
+ try NCicUnification.unify hdb metasenv subst context
arity2 (C.Prod (name, so1, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
| C.Sort _ (* , t ==?== C.Prod _ *) ->
let metasenv, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in
let metasenv, subst =
- try NCicUnification.unify metasenv subst context
+ try NCicUnification.unify hdb metasenv subst context
arity2 (C.Prod ("_", ind, meta))
with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
"expected %s, found %s" (* XXX localizzare meglio *)
aux
;;
-let rec typeof
+let rec typeof hdb
?(localise=fun _ -> Stdpp.dummy_loc)
~look_for_coercion metasenv subst context term expty
=
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context term);
- let force_ty metasenv subst context orig t infty expty =
+ let force_ty skip_lambda metasenv subst context orig t infty expty =
(*D*)inside 'F'; try let rc =
match expty with
| Some expty ->
(match t with
- | C.Implicit _
- | C.Lambda _ -> metasenv, subst, t, expty
+ | C.Implicit _ -> assert false
+ | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty
| _ ->
pp (lazy (
(NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^
(NCicPp.ppterm ~metasenv ~subst ~context expty)));
try
let metasenv, subst =
- NCicUnification.unify metasenv subst context infty expty
+ NCicUnification.unify hdb metasenv subst context infty expty
in
metasenv, subst, t, expty
with exc ->
- try_coercions ~look_for_coercion ~localise
+ try_coercions hdb ~look_for_coercion ~localise
metasenv subst context t orig infty expty true exc)
| None -> metasenv, subst, t, infty
(*D*)in outside(); rc with exc -> outside (); raise exc
metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
| C.Prod (name,(s as orig_s),(t as orig_t)) ->
let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
+ let metasenv, subst, s, s1 =
+ force_to_sort hdb ~look_for_coercion
+ metasenv subst context s orig_s localise s1 in
let context1 = (name,(C.Decl s))::context in
let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in
+ let metasenv, subst, t, s2 =
+ force_to_sort hdb ~look_for_coercion
+ metasenv subst context1 t orig_t localise s2 in
let metasenv, subst, s, t, ty =
- sort_of_prod ~look_for_coercion localise metasenv subst
+ sort_of_prod localise metasenv subst
context orig_s orig_t (name,s) t (s1,s2)
in
metasenv, subst, NCic.Prod(name,s,t), ty
- | C.Lambda (n,(s as orig_s),t) ->
- let exp_s, exp_ty_t =
+ | C.Lambda (n,(s as orig_s),t) as orig ->
+ let exp_s, exp_ty_t, force_after =
match expty with
- | None -> None, None
+ | None -> None, None, false
| Some expty ->
match NCicReduction.whd ~subst context expty with
- | C.Prod (_,s,t) -> Some s, Some t
- | _ -> None, None (** XXX FUNCLASS |-> QUALCOSA *)
+ | C.Prod (_,s,t) -> Some s, Some t, false
+ | _ -> None, None, true
in
let metasenv, subst, s, ty_s =
typeof_aux metasenv subst context None s in
let metasenv, subst, s, _ =
- force_to_sort ~look_for_coercion
+ force_to_sort hdb ~look_for_coercion
metasenv subst context s orig_s localise ty_s in
let (metasenv,subst), exp_ty_t =
match exp_s with
| Some exp_s ->
- (try NCicUnification.unify metasenv subst context s exp_s,exp_ty_t
+ (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t
with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
"Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
exp_s))) exc))
| None -> (metasenv, subst), None
in
- let context = (n,C.Decl s) :: context in
+ let context_for_t = (n,C.Decl s) :: context in
let metasenv, subst, t, ty_t =
- typeof_aux metasenv subst context exp_ty_t t
+ typeof_aux metasenv subst context_for_t exp_ty_t t
in
- metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
+ if force_after then
+ force_ty false metasenv subst context orig
+ (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
+ else
+ metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
| C.LetIn (n,(ty as orig_ty),t,bo) ->
let metasenv, subst, ty, ty_ty =
typeof_aux metasenv subst context None ty in
let metasenv, subst, ty, _ =
- force_to_sort ~look_for_coercion
+ force_to_sort hdb ~look_for_coercion
metasenv subst context ty orig_ty localise ty_ty in
let metasenv, subst, t, _ =
typeof_aux metasenv subst context (Some ty) t in
| C.Appl ((he as orig_he)::(_::_ as args)) ->
let metasenv, subst, he, ty_he =
typeof_aux metasenv subst context None he in
- eat_prods ~localise ~look_for_coercion
+ eat_prods hdb ~localise ~look_for_coercion
metasenv subst context orig_he he ty_he args
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
| C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
let _, _, arity, cl = List.nth itl tyno in
let constructorsno = List.length cl in
let _, metasenv, args =
- NCicMetaSubst.saturate metasenv context arity 0 in
+ NCicMetaSubst.saturate metasenv subst context arity 0 in
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
let metasenv, subst, ind, ind_ty =
typeof_aux metasenv subst context None ind in
let metasenv, subst =
- check_allowed_sort_elimination localise r orig_term metasenv subst
+ check_allowed_sort_elimination hdb localise r orig_term metasenv subst
context ind ind_ty outsort
in
(* let's check if the type of branches are right *)
in
pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^
NCicPp.ppterm ~metasenv ~subst ~context infty ));
- force_ty metasenv subst context orig t infty expty
+ force_ty true metasenv subst context orig t infty expty
(*D*)in outside(); rc with exc -> outside (); raise exc
in
typeof_aux metasenv subst context expty term
-and try_coercions
+and try_coercions hdb
~localise ~look_for_coercion
metasenv subst context t orig_t infty expty perform_unification exc
=
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
| (metasenv, newterm, newtype, meta)::tl ->
try
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n"));
let metasenv, subst =
- NCicUnification.unify metasenv subst context meta t
+ NCicUnification.unify hdb metasenv subst context meta t
in
+ pp (lazy ( "UNIFICATION in CTX:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context
+ ^ "\nMENV: " ^
+ NCicPp.ppmetasenv metasenv ~subst
+ ^ "\nOF: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context newtype ^ " === " ^
+ NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n"));
let metasenv, subst =
if perform_unification then
- NCicUnification.unify metasenv subst context newtype expty
+ NCicUnification.unify hdb metasenv subst context newtype expty
else metasenv, subst
in
metasenv, subst, newterm, newtype
first exc
(look_for_coercion metasenv subst context infty expty)
-and force_to_sort
+and force_to_sort hdb
~look_for_coercion metasenv subst context t orig_t localise ty
=
match NCicReduction.whd ~subst context ty with
metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
| C.Sort _ as ty -> metasenv, subst, t, ty
| ty ->
- try_coercions ~localise ~look_for_coercion metasenv subst context
+ try_coercions hdb ~localise ~look_for_coercion metasenv subst context
t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false
- (RefineFailure (lazy (localise orig_t,
+ (Uncertain (lazy (localise orig_t,
"The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
-and sort_of_prod ~look_for_coercion
+and sort_of_prod
localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)
=
- let metasenv, subst, s, t1 =
- force_to_sort
- ~look_for_coercion metasenv subst context s orig_s localise t1 in
- let metasenv, subst, t, t2 =
- force_to_sort ~look_for_coercion metasenv subst ((name,C.Decl s)::context)
- t orig_t localise t2 in
+ (* force to sort is done in the Prod case in typeof *)
match t1, t2 with
| C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2
| C.Sort (C.Type u1), C.Sort (C.Type u2) ->
- metasenv, subst, s, t, C.Sort (C.Type (u1@u2))
+ metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2))
| C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2
| C.Meta _, C.Sort _
| C.Meta _, C.Meta (_,(_,_))
(NCicPp.ppterm ~subst ~metasenv ~context y)
(NCicPp.ppterm ~subst ~metasenv ~context x))))
-and eat_prods
+and eat_prods hdb
~localise ~look_for_coercion metasenv subst context orig_he he ty_he args
=
(*D*)inside 'E'; try let rc =
match NCicReduction.whd ~subst context ty_he with
| C.Prod (_,s,t) ->
let metasenv, subst, arg, _ =
- typeof ~look_for_coercion ~localise
+ typeof hdb ~look_for_coercion ~localise
metasenv subst context arg (Some s) in
let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
aux metasenv subst (arg :: args_so_far) he t tl
| C.Meta _
| C.Appl (C.Meta _ :: _) as t ->
let metasenv, subst, arg, ty_arg =
- typeof ~look_for_coercion ~localise
+ typeof hdb ~look_for_coercion ~localise
metasenv subst context arg None in
let metasenv, meta, _ =
NCicMetaSubst.mk_meta metasenv
(("_",C.Decl ty_arg) :: context) `Type
in
let flex_prod = C.Prod ("_", ty_arg, meta) in
+ (* next line grants that ty_args is a type *)
+ let metasenv,subst, flex_prod, _ =
+ typeof hdb ~look_for_coercion ~localise metasenv subst
+ context flex_prod None in
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
^ "\nOF: " ^
NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^
NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n"));
let metasenv, subst =
- try NCicUnification.unify metasenv subst context t flex_prod
+ try NCicUnification.unify hdb metasenv subst context t flex_prod
with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
("The term %s has an inferred type %s, but is applied to the" ^^
" argument %s of type %s")
(List.length args) (List.length args_so_far))))
| ty ->
let metasenv, subst, newhead, newheadty =
- try_coercions ~localise ~look_for_coercion metasenv subst context
+ try_coercions hdb ~localise ~look_for_coercion metasenv subst context
(NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
(NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
false
projects / helm.git / blobdiff