(* $Id$ *)
-let exp_implicit metasenv subst context expty =
+exception RefineFailure of (Stdpp.location * string) Lazy.t;;
+exception Uncertain of (Stdpp.location * string) Lazy.t;;
+exception AssertFailure of string Lazy.t;;
+
+module C = NCic
+module Ref = NReference
+
+let wrap_exc msg = function
+ | NCicUnification.Uncertain _ -> Uncertain msg
+ | NCicUnification.UnificationFailure _ -> RefineFailure msg
+ | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg
+ | e -> raise e
+;;
+
+let exp_implicit metasenv context expty =
function
- | Some `Closed -> NCicMetaSubst.mk_meta metasenv [] expty
- | Some `Type | None -> NCicMetaSubst.mk_meta metasenv context expty
+ | `Closed -> NCicMetaSubst.mk_meta metasenv [] expty
+ | `Type | `Term -> NCicMetaSubst.mk_meta metasenv context expty
| _ -> assert false
;;
-let sort_of_prod localise metasenv subst context (name,s) t (t1, t2) =
+let sort_of_prod
+ localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)
+=
let restrict metasenv subst = function
- | NCic.Meta (i,(_,(NCic.Irl 0 | NCic.Ctx []))) as t ->
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) as t ->
metasenv, subst, t
- | NCic.Meta (i,(_,lc)) as t ->
- let len = match lc with NCic.Irl len->len | NCic.Ctx l->List.lenght l in
+ | C.Meta (i,(_,lc)) as t ->
+ let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
let metasenv, subst, _ =
- NCicMetaSubst.restrict metasenv subst i (HExtlib.seq 1 len)
+ NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 len)
in
metasenv, subst, t
| t -> metasenv, subst, t
in
- let t1 = R.whd ~subst context t1 in
- let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
+ let t1 = NCicReduction.whd ~subst context t1 in
+ let t2 = NCicReduction.whd ~subst ((name,C.Decl s)::context) t2 in
let metasenv, subst, t1 = restrict metasenv subst t1 in
let metasenv, subst, t2 = restrict metasenv subst t2 in
match t1, t2 with
| C.Meta _, C.Sort _
| C.Meta _, C.Meta _
| C.Sort _, C.Meta _ -> metasenv, subst, t2
- | x, _ | _, x ->
- let y, context =
- if x == t1 then s, context else t, ((name,C.Decl s)::context)
+ | x, (C.Sort _ | C.Meta _) | _, x ->
+ let y, context, orig =
+ if x == t1 then s, context, orig_s
+ else t, ((name,C.Decl s)::context), orig_t
in
- raise (TypeCheckerFailure (lazy (Printf.sprintf
+ raise (RefineFailure (lazy (localise orig,Printf.sprintf
"%s is expected to be a type, but its type is %s that is not a sort"
- (PP.ppterm ~subst ~metasenv ~context y)
- (PP.ppterm ~subst ~metasenv ~context x))))
+ (NCicPp.ppterm ~subst ~metasenv ~context y)
+ (NCicPp.ppterm ~subst ~metasenv ~context x))))
+;;
+
+let check_allowed_sort_elimination localise r orig =
+ let mkapp he arg =
+ match he with
+ | C.Appl l -> C.Appl (l @ [arg])
+ | t -> C.Appl [t;arg] in
+ (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *)
+ let rec aux metasenv subst context ind arity1 arity2 =
+ let arity1 = NCicReduction.whd ~subst context arity1 in
+ match arity1 with
+ | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) ->
+ let metasenv, meta, _ =
+ NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) None
+ in
+ let metasenv, subst =
+ try NCicUnification.unify metasenv subst context
+ (C.Prod (name, so1, meta)) arity2
+ with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
+ "expected %s, found %s" (* XXX localizzare meglio *)
+ (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+ (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
+ in
+ aux metasenv subst ((name, C.Decl so1)::context)
+ (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta
+ | C.Sort _ (* , t ==?== C.Prod _ *) ->
+ let metasenv, meta, _ =
+ NCicMetaSubst.mk_meta metasenv (("_",C.Decl ind)::context) None
+ in
+ let metasenv, subst =
+ try NCicUnification.unify metasenv subst context
+ (C.Prod ("_", ind, meta)) arity2
+ with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
+ "expected %s, found %s" (* XXX localizzare meglio *)
+ (NCicPp.ppterm ~subst ~metasenv ~context arity1)
+ (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc)
+ in
+ (try NCicTypeChecker.check_allowed_sort_elimination
+ ~metasenv ~subst r context ind arity1 arity2
+ with exc -> raise (wrap_exc (lazy (localise orig,
+ "Sort elimination not allowed ")) exc))
+ | _ -> assert false
+ in
+ aux
;;
let rec typeof
- ?(localize=fun _ -> Stdpp.dummy) metasenv subst context term expty
+ ?(localise=fun _ -> Stdpp.dummy_loc) metasenv subst context term expty
=
- let force_ty metasenv subst context t infty = function
+ let force_ty metasenv subst context orig t infty = function
| Some expty ->
(match t with
- | NCic.Implicit _ -> metasenv, subst, t, expty
+ | C.Implicit _
+ | C.Lambda _ -> metasenv, subst, t, expty
| _ ->
let metasenv, subst =
- NCicUnification.unify metasenv subst context infty expty in
+ try NCicUnification.unify metasenv subst context infty expty
+ with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf
+ "The term %s has type %s but is here used with type %s"
+ (NCicPp.ppterm ~metasenv ~subst ~context t)
+ (NCicPp.ppterm ~metasenv ~subst ~context infty)
+ (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
+ in
metasenv, subst, t, expty)
| None -> metasenv, subst, t, infty
in
let rec typeof_aux metasenv subst context expty =
- fun t -> (*prerr_endline (PP.ppterm ~metasenv ~subst ~context t);*)
+ fun t as orig -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*)
let metasenv, subst, t, infty =
match t with
| C.Rel n ->
let infty =
(try
match List.nth context (n - 1) with
- | (_,C.Decl ty) -> S.lift n ty
- | (_,C.Def (_,ty)) -> S.lift n ty
+ | (_,C.Decl ty) -> NCicSubstitution.lift n ty
+ | (_,C.Def (_,ty)) -> NCicSubstitution.lift n ty
with Failure _ ->
- raise (RefineFailure (lazy (localize t,"unbound variable"))))
+ raise (RefineFailure (lazy (localise t,"unbound variable"))))
in
metasenv, subst, t, infty
| C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u]))
NCicPp.ppterm ~subst ~metasenv ~context t)))
| C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0))
| C.Implicit infos ->
- let metasenv,t,ty = exp_implicit metasenv subst context infos expty in
+ let metasenv,t,ty = exp_implicit metasenv context expty infos in
metasenv, subst, t, ty
| C.Meta (n,l) as t ->
let ty =
try
- let _,_,_,ty = U.lookup_subst n subst in
- with U.Subst_not_found _ -> try
- let _,_,ty = U.lookup_meta n metasenv in
- match ty with C.Implicit _ -> assert false | _ -> c,ty
- with U.Meta_not_found _ ->
+ let _,_,_,ty = NCicUtils.lookup_subst n subst in ty
+ with NCicUtils.Subst_not_found _ -> try
+ let _,_,ty = NCicUtils.lookup_meta n metasenv in
+ match ty with C.Implicit _ -> assert false | _ -> ty
+ with NCicUtils.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf
- "%s not found" (PP.ppterm ~subst ~metasenv ~context t))))
+ "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
in
- metasenv, subst, t, S.subst_meta l ty
+ metasenv, subst, t, NCicSubstitution.subst_meta l ty
| C.Const _ ->
metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t
- | C.Prod (name,s,t) as orig ->
+ | C.Prod (name,(s as orig_s),(t as orig_t)) as orig ->
let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in
- let context = (name,(NCic.Decl s))::context in
+ let context = (name,(C.Decl s))::context in
let metasenv, subst, t, s2 = typeof_aux metasenv subst context None t in
let metasenv, subst, ty =
- sort_of_prod localize metasenv subst context (name,s) t (s1,s2)
+ sort_of_prod localise metasenv subst
+ context orig_s orig_t (name,s) t (s1,s2)
in
metasenv, subst, orig, ty
- | C.Lambda (n,s,t) ->
- let sort = typeof_aux context s in
- (match R.whd ~subst context sort with
- | C.Meta _ | C.Sort _ -> ()
- | _ ->
- raise
- (TypeCheckerFailure (lazy (Printf.sprintf
- ("Not well-typed lambda-abstraction: " ^^
- "the source %s should be a type; instead it is a term " ^^
- "of type %s") (PP.ppterm ~subst ~metasenv ~context s)
- (PP.ppterm ~subst ~metasenv ~context sort)))));
- let ty = typeof_aux ((n,(C.Decl s))::context) t in
- C.Prod (n,s,ty)
+ | C.Lambda (n,(s as orig_s),t) ->
+ let exp_s, exp_ty_t =
+ match expty with
+ | None -> None, None
+ | Some expty ->
+ match NCicReduction.whd ~subst context expty with
+ | C.Prod (_,s,t) -> Some s, Some t
+ | _ -> None, None
+ in
+ let metasenv, subst, s, _ = typeof_aux metasenv subst context None 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
+ 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
+ (* XXX coerce_to_sort s *)
+ let context = (n,C.Decl s) :: context in
+ let metasenv, subst, t, ty_t =
+ typeof_aux metasenv subst context exp_ty_t t
+ in
+ metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
| C.LetIn (n,ty,t,bo) ->
- let ty_t = typeof_aux context t in
- let _ = typeof_aux context ty in
- if not (R.are_convertible ~subst context ty_t ty) then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- "The type of %s is %s but it is expected to be %s"
- (PP.ppterm ~subst ~metasenv ~context t)
- (PP.ppterm ~subst ~metasenv ~context ty_t)
- (PP.ppterm ~subst ~metasenv ~context ty))))
- else
- let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in
- S.subst ~avoid_beta_redexes:true t ty_bo
- | C.Appl (he::(_::_ as args)) ->
- let ty_he = typeof_aux context he in
- let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
- eat_prods ~subst ~metasenv context he ty_he args_with_ty
+ let metasenv, subst, ty, _ = typeof_aux metasenv subst context None ty in
+ let metasenv, subst, t, _ =
+ typeof_aux metasenv subst context (Some ty) t in
+ let context = (n, C.Def (t,ty)) :: context in
+ let metasenv, subst, bo, bo_ty =
+ typeof_aux metasenv subst context expty bo
+ in
+ metasenv, subst, C.LetIn (n, ty, t, bo),
+ NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty
+ | 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 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,outtype,term,pl) ->
- let outsort = typeof_aux context outtype in
- let _,leftno,itl,_,_ = E.get_checked_indtys r in
- let constructorsno =
- let _,_,_,cl = List.nth itl tyno in List.length cl
- in
- let parameters, arguments =
- let ty = R.whd ~subst context (typeof_aux context term) in
- let r',tl =
- match ty with
- C.Const (Ref.Ref (_,Ref.Ind _) as r') -> r',[]
- | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as r') :: tl) -> r',tl
- | _ ->
- raise
- (TypeCheckerFailure (lazy (Printf.sprintf
- "Case analysis: analysed term %s is not an inductive one"
- (PP.ppterm ~subst ~metasenv ~context term)))) in
- if not (Ref.eq r r') then
- raise
- (TypeCheckerFailure (lazy (Printf.sprintf
- ("Case analysys: analysed term type is %s, but is expected " ^^
- "to be (an application of) %s")
- (PP.ppterm ~subst ~metasenv ~context ty)
- (PP.ppterm ~subst ~metasenv ~context (C.Const r')))))
- else
- try HExtlib.split_nth leftno tl
- with
- Failure _ ->
- raise (TypeCheckerFailure (lazy (Printf.sprintf
- "%s is partially applied"
- (PP.ppterm ~subst ~metasenv ~context ty)))) in
+ | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,
+ outtype,(term as orig_term),pl) as orig ->
+ let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
+ let _, _, arity, cl = List.nth itl tyno in
+ let constructorsno = List.length cl in
+ let _, metasenv, args =
+ NCicMetaSubst.saturate metasenv 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, outtype, outsort =
+ typeof_aux metasenv subst context None outtype in
+ let parameters, arguments = HExtlib.split_nth leftno args in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
- let sort_of_ind_type =
+ let ind =
if parameters = [] then C.Const r
else C.Appl ((C.Const r)::parameters) in
- let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
- check_allowed_sort_elimination ~subst ~metasenv r context
- sort_of_ind_type type_of_sort_of_ind_ty outsort;
+ let metasenv, subst, ind, ind_ty =
+ typeof_aux metasenv subst context None ind in
+ check_allowed_sort_elimination localise r orig_term metasenv subst context
+ ind ind_ty outsort;
(* let's check if the type of branches are right *)
if List.length pl <> constructorsno then
- raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
- let j,branches_ok,p_ty, exp_p_ty =
+ raise (RefineFailure (lazy (localise orig,
+ "Wrong number of cases in a match")));
+ let _, metasenv, subst, pl_rev =
List.fold_left
- (fun (j,b,old_p_ty,old_exp_p_ty) p ->
- if b then
+ (fun (j, metasenv, subst, branches) p ->
let cons =
let cons = Ref.mk_constructor j r in
if parameters = [] then C.Const cons
else C.Appl (C.Const cons::parameters)
in
- let ty_p = typeof_aux context p in
- let ty_cons = typeof_aux context cons in
+ let metasenv, subst, cons, ty_cons =
+ typeof_aux metasenv subst context None cons in
let ty_branch =
- type_of_branch ~subst context leftno outtype cons ty_cons 0
- in
- j+1, R.are_convertible ~subst context ty_p ty_branch,
- ty_p, ty_branch
- else
- j,false,old_p_ty,old_exp_p_ty
- ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
+ NCicTypeChecker.type_of_branch
+ ~subst context leftno outtype cons ty_cons in
+ let metasenv, subst, p, _ =
+ typeof_aux metasenv subst context (Some ty_branch) p in
+ j+1, metasenv, subst, p :: branches)
+ (1, metasenv, subst, []) pl
in
- if not branches_ok then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
- "has type %s\nnot convertible with %s")
- (PP.ppterm ~subst ~metasenv ~context
- (C.Const (Ref.mk_constructor (j-1) r)))
- (PP.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
- (PP.ppterm ~metasenv ~subst ~context p_ty)
- (PP.ppterm ~metasenv ~subst ~context exp_p_ty))));
- let res = outtype::arguments@[term] in
- R.head_beta_reduce (C.Appl res)
+ metasenv, subst,
+ C.Match (r, outtype, term, List.rev pl_rev),
+ NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term]))
| C.Match _ -> assert false
-
- and type_of_branch ~subst context leftno outty cons tycons liftno =
- match R.whd ~subst context tycons with
- | C.Const (Ref.Ref (_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
- | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _))::tl) ->
- let _,arguments = HExtlib.split_nth leftno tl in
- C.Appl (S.lift liftno outty::arguments@[cons])
- | C.Prod (name,so,de) ->
- let cons =
- match S.lift 1 cons with
- | C.Appl l -> C.Appl (l@[C.Rel 1])
- | t -> C.Appl [t ; C.Rel 1]
- in
- C.Prod (name,so,
- type_of_branch ~subst ((name,(C.Decl so))::context)
- leftno outty cons de (liftno+1))
- | _ -> raise (AssertFailure (lazy "type_of_branch"))
-
- (* check_metasenv_consistency checks that the "canonical" context of a
- metavariable is consitent - up to relocation via the relocation list l -
- with the actual context *)
- and check_metasenv_consistency
- ~subst ~metasenv term context canonical_context l
- =
- match l with
- | shift, C.Irl n ->
- let context = snd (HExtlib.split_nth shift context) in
- let rec compare = function
- | 0,_,[] -> ()
- | 0,_,_::_
- | _,_,[] ->
- raise (AssertFailure (lazy (Printf.sprintf
- "Local and canonical context %s have different lengths"
- (PP.ppterm ~subst ~context ~metasenv term))))
- | m,[],_::_ ->
- raise (TypeCheckerFailure (lazy (Printf.sprintf
- "Unbound variable -%d in %s" m
- (PP.ppterm ~subst ~metasenv ~context term))))
- | m,t::tl,ct::ctl ->
- (match t,ct with
- (_,C.Decl t1), (_,C.Decl t2)
- | (_,C.Def (t1,_)), (_,C.Def (t2,_))
- | (_,C.Def (_,t1)), (_,C.Decl t2) ->
- if not (R.are_convertible ~subst tl t1 t2) then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context for %s: " ^^
- "%s expected, which is not convertible with %s")
- (PP.ppterm ~subst ~metasenv ~context term)
- (PP.ppterm ~subst ~metasenv ~context t2)
- (PP.ppterm ~subst ~metasenv ~context t1))))
- | _,_ ->
- raise
- (TypeCheckerFailure (lazy (Printf.sprintf
- ("Not well typed metavariable local context for %s: " ^^
- "a definition expected, but a declaration found")
- (PP.ppterm ~subst ~metasenv ~context term)))));
- compare (m - 1,tl,ctl)
- in
- compare (n,context,canonical_context)
- | shift, lc_kind ->
- (* we avoid useless lifting by shortening the context*)
- let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in
- let lifted_canonical_context =
- let rec lift_metas i = function
- | [] -> []
- | (n,C.Decl t)::tl ->
- (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
- | (n,C.Def (t,ty))::tl ->
- (n,C.Def ((S.subst_meta l (S.lift i t)),
- S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
- in
- lift_metas 1 canonical_context in
- let l = U.expand_local_context lc_kind in
- try
- List.iter2
- (fun t ct ->
- match (t,ct) with
- | t, (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly expensive
- reduction that can be easily avoided and that is quite
- frequent. However, this is better handled using levels to
- control reduction *)
- let optimized_t =
- match t with
- | C.Rel n ->
- (try
- match List.nth context (n - 1) with
- | (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with Failure _ -> t)
- | _ -> t
- in
- if not (R.are_convertible ~subst context optimized_t ct)
- then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context: " ^^
- "expected a term convertible with %s, found %s")
- (PP.ppterm ~subst ~metasenv ~context ct)
- (PP.ppterm ~subst ~metasenv ~context t))))
- | t, (_,C.Decl ct) ->
- let type_t = typeof_aux context t in
- if not (R.are_convertible ~subst context type_t ct) then
- raise (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context: "^^
- "expected a term of type %s, found %s of type %s")
- (PP.ppterm ~subst ~metasenv ~context ct)
- (PP.ppterm ~subst ~metasenv ~context t)
- (PP.ppterm ~subst ~metasenv ~context type_t))))
- ) l lifted_canonical_context
- with
- Invalid_argument _ ->
- raise (AssertFailure (lazy (Printf.sprintf
- "Local and canonical context %s have different lengths"
- (PP.ppterm ~subst ~metasenv ~context term))))
-
- and check_allowed_sort_elimination ~subst ~metasenv r =
- let mkapp he arg =
- match he with
- | C.Appl l -> C.Appl (l @ [arg])
- | t -> C.Appl [t;arg] in
- let rec aux context ind arity1 arity2 =
- let arity1 = R.whd ~subst context arity1 in
- let arity2 = R.whd ~subst context arity2 in
- match arity1,arity2 with
- | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
- if not (R.are_convertible ~subst context so1 so2) then
- raise (TypeCheckerFailure (lazy (Printf.sprintf
- "In outtype: expected %s, found %s"
- (PP.ppterm ~subst ~metasenv ~context so1)
- (PP.ppterm ~subst ~metasenv ~context so2)
- )));
- aux ((name, C.Decl so1)::context)
- (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
- | C.Sort _, C.Prod (name,so,ta) ->
- if not (R.are_convertible ~subst context so ind) then
- raise (TypeCheckerFailure (lazy (Printf.sprintf
- "In outtype: expected %s, found %s"
- (PP.ppterm ~subst ~metasenv ~context ind)
- (PP.ppterm ~subst ~metasenv ~context so)
- )));
- (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
- | (C.Sort C.Type _, C.Sort _)
- | (C.Sort C.Prop, C.Sort C.Prop) -> ()
- | (C.Sort C.Prop, C.Sort C.Type _) ->
- (* TODO: we should pass all these parameters since we
- * have them already *)
- let _,leftno,itl,_,i = E.get_checked_indtys r in
- let itl_len = List.length itl in
- let _,itname,ittype,cl = List.nth itl i in
- let cl_len = List.length cl in
- (* is it a singleton, non recursive and non informative
- definition or an empty one? *)
- if not
- (cl_len = 0 ||
- (itl_len = 1 && cl_len = 1 &&
- let _,_,constrty = List.hd cl in
- is_non_recursive_singleton r itname ittype constrty &&
- is_non_informative leftno constrty))
- then
- raise (TypeCheckerFailure (lazy
- ("Sort elimination not allowed")));
- | _,_ -> ())
- | _,_ -> ()
- in
- aux
-
- in
- typeof_aux context term
-
-and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
- let rec aux ty_he = function
- | [] -> ty_he
- | (arg, ty_arg)::tl ->
- match R.whd ~subst context ty_he with
- | C.Prod (_,s,t) ->
- if R.are_convertible ~subst context ty_arg s then
- aux (S.subst ~avoid_beta_redexes:true arg t) tl
- else
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Appl: wrong application of %s: the parameter %s has type"^^
- "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
- (PP.ppterm ~subst ~metasenv ~context he)
- (PP.ppterm ~subst ~metasenv ~context arg)
- (PP.ppterm ~subst ~metasenv ~context ty_arg)
- (PP.ppterm ~subst ~metasenv ~context s)
- (PP.ppcontext ~subst ~metasenv context))))
- | _ ->
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- "Appl: %s is not a function, it cannot be applied"
- (PP.ppterm ~subst ~metasenv ~context
- (let res = List.length tl in
- let eaten = List.length args_with_ty - res in
- (C.Appl
- (he::List.map fst
- (fst (HExtlib.split_nth eaten args_with_ty)))))))))
- in
- aux ty_he args_with_ty
-
-
-(*
-open Printf
-
-exception RefineFailure of string Lazy.t;;
-exception Uncertain of string Lazy.t;;
-exception AssertFailure of string Lazy.t;;
-
-(* for internal use only; the integer is the number of surplus arguments *)
-exception MoreArgsThanExpected of int * exn;;
-
-let insert_coercions = ref true
-let pack_coercions = ref true
-
-let debug = false;;
-
-let debug_print =
- if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());;
-
-let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2"
-
-let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph =
- try
-let foo () =
- CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
-in profiler_eat_prods2.HExtlib.profile foo ()
- with
- (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
- | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
-;;
-
-let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods"
-
-let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph =
- try
-let foo () =
- CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
-in profiler_eat_prods.HExtlib.profile foo ()
- with
- (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
- | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
-;;
-
-let profiler = HExtlib.profile "CicRefine.fo_unif"
-
-let fo_unif_subst subst context metasenv t1 t2 ugraph =
- try
-let foo () =
- CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
-in profiler.HExtlib.profile foo ()
- with
- (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
- | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
-;;
-
-let enrich localization_tbl t ?(f = fun msg -> msg) exn =
- let exn' =
- match exn with
- RefineFailure msg -> RefineFailure (f msg)
- | Uncertain msg -> Uncertain (f msg)
- | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg)
- | Sys.Break -> raise exn
- | _ -> prerr_endline (Printexc.to_string exn); assert false
- in
- let loc =
- try
- Cic.CicHash.find localization_tbl t
- with Not_found ->
- HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t);
- raise exn'
- in
- raise (HExtlib.Localized (loc,exn'))
-
-let relocalize localization_tbl oldt newt =
- try
- let infos = Cic.CicHash.find localization_tbl oldt in
- Cic.CicHash.remove localization_tbl oldt;
- Cic.CicHash.add localization_tbl newt infos;
- with
- Not_found -> ()
-;;
-
-let rec split l n =
- match (l,n) with
- (l,0) -> ([], l)
- | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
- | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
-;;
-
-let exp_impl metasenv subst context =
- function
- | Some `Type ->
- let (metasenv', idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
- | Some `Closed ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
- metasenv', Cic.Meta (idx, [])
- | None ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- metasenv', Cic.Meta (idx, irl)
- | _ -> assert false
-;;
-
-let is_a_double_coercion t =
- let rec subst_nth n x l =
- match n,l with
- | _, [] -> []
- | 0, _::tl -> x :: tl
- | n, hd::tl -> hd :: subst_nth (n-1) x tl
- in
- let imp = Cic.Implicit None in
- let dummyres = false,imp, imp,imp,imp in
- match t with
- | Cic.Appl l1 ->
- (match CoercGraph.coerced_arg l1 with
- | Some (Cic.Appl l2, pos1) ->
- (match CoercGraph.coerced_arg l2 with
- | Some (x, pos2) ->
- true, List.hd l1, List.hd l2, x,
- Cic.Appl (subst_nth (pos1 + 1)
- (Cic.Appl (subst_nth (pos2+1) imp l2)) l1)
- | _ -> dummyres)
- | _ -> dummyres)
- | _ -> dummyres
-;;
-
-let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn
-=
- let len = List.length tlbody_and_type in
- let msg =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst he context ^
- " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^
- ") is here applied to " ^ string_of_int len ^
- " arguments but here it can handle only up to " ^
- string_of_int (len - residuals) ^ " arguments")
- in
- enrich localization_tbl he ~f:(fun _-> msg) exn
-;;
-
-let mk_prod_of_metas metasenv context subst args =
- let rec mk_prod metasenv context' = function
- | [] ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- metasenv,Cic.Meta (idx, irl)
- | (_,argty)::tl ->
- let (metasenv, idx) =
- CicMkImplicit.mk_implicit_type metasenv subst context'
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- let meta = Cic.Meta (idx,irl) in
- let name =
- (* The name must be fresh for context. *)
- (* Nevertheless, argty is well-typed only in context. *)
- (* Thus I generate a name (name_hint) in context and *)
- (* then I generate a name --- using the hint name_hint *)
- (* --- that is fresh in context'. *)
- let name_hint =
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- ~typ:(CicMetaSubst.apply_subst subst argty)
- in
- FreshNamesGenerator.mk_fresh_name ~subst
- [] context' name_hint ~typ:(Cic.Sort Cic.Prop)
- in
- let metasenv,target =
- mk_prod metasenv ((Some (name, Cic.Decl meta))::context') tl
- in
- metasenv,Cic.Prod (name,meta,target)
- in
- mk_prod metasenv context args
-;;
-
-let rec type_of_constant uri ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.Constant (_,_,ty,_,_) -> ty,u
- | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown constant definition " ^ U.string_of_uri uri)))
-
-and type_of_variable uri ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.Variable (_,_,ty,_,_) -> ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri)))
-
-and type_of_mutual_inductive_defs uri i ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,arity,_) = List.nth dl i in
- arity,u
- | _ ->
- raise
- (RefineFailure
- (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri)))
-
-and type_of_mutual_inductive_constr uri i j ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager in
- let _ = CicTypeChecker.typecheck uri in
- let obj,u =
- try
- CicEnvironment.get_cooked_obj ugraph uri
- with Not_found -> assert false
- in
- match obj with
- C.InductiveDefinition (dl,_,_,_) ->
- let (_,_,_,cl) = List.nth dl i in
- let (_,ty) = List.nth cl (j-1) in
- ty,u
- | _ ->
- raise
- (RefineFailure
- (lazy
- ("Unkown mutual inductive definition " ^ U.string_of_uri uri)))
-
-
-(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-
-(* the check_branch function checks if a branch of a case is refinable.
- It returns a pair (outype_instance,args), a subst and a metasenv.
- outype_instance is the expected result of applying the case outtype
- to args.
- The problem is that outype is in general unknown, and we should
- try to synthesize it from the above information, that is in general
- a second order unification problem. *)
-
-and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
- let module C = Cic in
- let module R = CicReduction in
- match R.whd ~subst context expectedtype with
- C.MutInd (_,_,_) ->
- (n,context,actualtype, [term]), subst, metasenv, ugraph
- | C.Appl (C.MutInd (_,_,_)::tl) ->
- let (_,arguments) = split tl left_args_no in
- (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph
- | C.Prod (_,so,de) ->
- (* we expect that the actual type of the branch has the due
- number of Prod *)
- (match R.whd ~subst context actualtype with
- C.Prod (name',so',de') ->
- let subst, metasenv, ugraph1 =
- fo_unif_subst subst context metasenv so so' ugraph in
- let term' =
- (match CicSubstitution.lift 1 term with
- C.Appl l -> C.Appl (l@[C.Rel 1])
- | t -> C.Appl [t ; C.Rel 1]) in
- (* we should also check that the name variable is anonymous in
- the actual type de' ?? *)
- check_branch (n+1)
- ((Some (name',(C.Decl so)))::context)
- metasenv subst left_args_no de' term' de ugraph1
- | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
- | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
-
-and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
- ugraph
-=
- let rec type_of_aux subst metasenv context t ugraph =
- let module C = Cic in
- let module S = CicSubstitution in
- let module U = UriManager in
- let (t',_,_,_,_) as res =
- match t with
- (* function *)
- C.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Decl ty) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | Some (_,C.Def (_,ty)) ->
- t,S.lift n ty,subst,metasenv, ugraph
- | None ->
- enrich localization_tbl t
- (RefineFailure (lazy "Rel to hidden hypothesis"))
- with
- Failure _ ->
- enrich localization_tbl t
- (RefineFailure (lazy "Not a closed term")))
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst
- subst metasenv context exp_named_subst ugraph
- in
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let ty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1
- | C.Meta (n,l) ->
- (try
- let (canonical_context, term,ty) =
- CicUtil.lookup_subst n subst
- in
- let l',subst',metasenv',ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- (* trust or check ??? *)
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv', ugraph1
- (* type_of_aux subst metasenv
- context (CicSubstitution.subst_meta l term) *)
- with CicUtil.Subst_not_found _ ->
- let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- let l',subst',metasenv', ugraph1 =
- check_metasenv_consistency n subst metasenv context
- canonical_context l ugraph
- in
- C.Meta (n,l'),CicSubstitution.subst_meta l' ty,
- subst', metasenv',ugraph1)
- | C.Sort (C.Type tno) ->
- let tno' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | C.Sort (C.CProp tno) ->
- let tno' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt tno' tno ugraph in
- t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | C.Sort (C.Prop|C.Set) ->
- t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
- | C.Implicit infos ->
- let metasenv',t' = exp_impl metasenv subst context infos in
- type_of_aux subst metasenv' context t' ugraph
- | C.Cast (te,ty) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- let te',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' context te ugraph1
- in
- let (te', ty'), subst''',metasenv''',ugraph3 =
- coerce_to_something true localization_tbl te' inferredty ty'
- subst'' metasenv'' context ugraph2
- in
- C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3
- | C.Prod (name,s,t) ->
- let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let s',sort1,subst', metasenv',ugraph1 =
- coerce_to_sort localization_tbl
- s' sort1 subst' context metasenv' ugraph1
- in
- let context_for_t = ((Some (name,(C.Decl s')))::context) in
- let t',sort2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- let t',sort2,subst'',metasenv'',ugraph2 =
- coerce_to_sort localization_tbl
- t' sort2 subst'' context_for_t metasenv'' ugraph2
- in
- let sop,subst''',metasenv''',ugraph3 =
- sort_of_prod localization_tbl subst'' metasenv''
- context (name,s') t' (sort1,sort2) ugraph2
- in
- C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3
- | C.Lambda (n,s,t) ->
- let s',sort1,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph
- in
- let s',sort1,subst',metasenv',ugraph1 =
- coerce_to_sort localization_tbl
- s' sort1 subst' context metasenv' ugraph1
- in
- let context_for_t = ((Some (n,(C.Decl s')))::context) in
- let t',type2,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv' context_for_t t ugraph1
- in
- C.Lambda (n,s',t'),C.Prod (n,s',type2),
- subst'',metasenv'',ugraph2
- | C.LetIn (n,s,ty,t) ->
- (* only to check if s is well-typed *)
- let s',ty',subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context s ugraph in
- let ty,_,subst',metasenv',ugraph1 =
- type_of_aux subst' metasenv' context ty ugraph1 in
- let subst',metasenv',ugraph1 =
- try
- fo_unif_subst subst' context metasenv'
- ty ty' ugraph1
- with
- exn ->
- enrich localization_tbl s' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty
- context))
- in
- let context_for_t = ((Some (n,(C.Def (s',ty))))::context) in
-
- let t',inferredty,subst'',metasenv'',ugraph2 =
- type_of_aux subst' metasenv'
- context_for_t t ugraph1
- in
- (* One-step LetIn reduction.
- * Even faster than the previous solution.
- * Moreover the inferred type is closer to the expected one.
- *)
- C.LetIn (n,s',ty,t'),
- CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty,
- subst'',metasenv'',ugraph2
- | C.Appl (he::((_::_) as tl)) ->
- let he',hetype,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context he ugraph
- in
- let tlbody_and_type,subst'',metasenv'',ugraph2 =
- typeof_list subst' metasenv' context ugraph1 tl
- in
- let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 =
- eat_prods true subst'' metasenv'' context
- he' hetype tlbody_and_type ugraph2
- in
- let newappl = (C.Appl (coerced_he::coerced_args)) in
- avoid_double_coercion
- context subst''' metasenv''' ugraph3 newappl applty
- | C.Appl _ -> assert false
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph in
- let ty_uri,ugraph2 = type_of_constant uri ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutInd (uri,i,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri in
- C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let exp_named_subst',subst',metasenv',ugraph1 =
- check_exp_named_subst subst metasenv context
- exp_named_subst ugraph
- in
- let ty_uri,ugraph2 =
- type_of_mutual_inductive_constr uri i j ugraph1
- in
- let cty =
- CicSubstitution.subst_vars exp_named_subst' ty_uri
- in
- C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst',
- metasenv',ugraph2
- | C.MutCase (uri, i, outtype, term, pl) ->
- (* first, get the inductive type (and noparams)
- * in the environment *)
- let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
- let _ = CicTypeChecker.typecheck uri in
- let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
- match obj with
- C.InductiveDefinition (l,expl_params,parsno,_) ->
- List.nth l i , expl_params, parsno, u
- | _ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy ("Unkown mutual inductive definition " ^
- U.string_of_uri uri)))
- in
- if List.length constructors <> List.length pl then
- enrich localization_tbl t
- (RefineFailure
- (lazy "Wrong number of cases")) ;
- let rec count_prod t =
- match CicReduction.whd ~subst context t with
- C.Prod (_, _, t) -> 1 + (count_prod t)
- | _ -> 0
- in
- let no_args = count_prod arity in
- (* now, create a "generic" MutInd *)
- let metasenv,left_args =
- CicMkImplicit.n_fresh_metas metasenv subst context no_left_params
- in
- let metasenv,right_args =
- let no_right_params = no_args - no_left_params in
- if no_right_params < 0 then assert false
- else CicMkImplicit.n_fresh_metas
- metasenv subst context no_right_params
- in
- let metasenv,exp_named_subst =
- CicMkImplicit.fresh_subst metasenv subst context expl_params in
- let expected_type =
- if no_args = 0 then
- C.MutInd (uri,i,exp_named_subst)
- else
- C.Appl
- (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
- in
- (* check consistency with the actual type of term *)
- let term',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context term ugraph in
- let expected_type',_, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context expected_type ugraph1
- in
- let actual_type = CicReduction.whd ~subst context actual_type in
- let subst,metasenv,ugraph3 =
- try
- fo_unif_subst subst context metasenv
- expected_type' actual_type ugraph2
- with
- exn ->
- enrich localization_tbl term' exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst term'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
- context))
- in
- let rec instantiate_prod t =
- function
- [] -> t
- | he::tl ->
- match CicReduction.whd ~subst context t with
- C.Prod (_,_,t') ->
- instantiate_prod (CicSubstitution.subst he t') tl
- | _ -> assert false
- in
- let arity_instantiated_with_left_args =
- instantiate_prod arity left_args in
- (* TODO: check if the sort elimination
- * is allowed: [(I q1 ... qr)|B] *)
- let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
- List.fold_right
- (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
- let constructor =
- if left_args = [] then
- (C.MutConstruct (uri,i,j,exp_named_subst))
- else
- (C.Appl
- (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
- in
- let p',actual_type,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context p ugraph
- in
- let constructor',expected_type, subst, metasenv,ugraph2 =
- type_of_aux subst metasenv context constructor ugraph1
- in
- let outtypeinstance,subst,metasenv,ugraph3 =
- try
- check_branch 0 context metasenv subst
- no_left_params actual_type constructor' expected_type
- ugraph2
- with
- exn ->
- enrich localization_tbl constructor'
- ~f:(fun _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context metasenv subst p'
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context metasenv subst actual_type
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context metasenv subst expected_type
- context)) exn
- in
- (p'::pl,j-1,
- outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
- pl ([],List.length pl,[],subst,metasenv,ugraph3)
- in
-
- (* we are left to check that the outype matches his instances.
- The easy case is when the outype is specified, that amount
- to a trivial check. Otherwise, we should guess a type from
- its instances
- *)
-
- let outtype,outtypety, subst, metasenv,ugraph4 =
- type_of_aux subst metasenv context outtype ugraph4 in
- (match outtype with
- | C.Meta (n,l) ->
- (let candidate,ugraph5,metasenv,subst =
- let exp_name_subst, metasenv =
- let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
- in
- let uris = CicUtil.params_of_obj o in
- List.fold_right (
- fun uri (acc,metasenv) ->
- let metasenv',new_meta =
- CicMkImplicit.mk_implicit metasenv subst context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- context
- in
- (uri, Cic.Meta(new_meta,irl))::acc, metasenv'
- ) uris ([],metasenv)
- in
- let ty =
- match left_args,right_args with
- [],[] -> Cic.MutInd(uri, i, exp_name_subst)
- | _,_ ->
- let rec mk_right_args =
- function
- 0 -> []
- | n -> (Cic.Rel n)::(mk_right_args (n - 1))
- in
- let right_args_no = List.length right_args in
- let lifted_left_args =
- List.map (CicSubstitution.lift right_args_no) left_args
- in
- Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
- (lifted_left_args @ mk_right_args right_args_no))
- in
- let fresh_name =
- FreshNamesGenerator.mk_fresh_name ~subst metasenv
- context Cic.Anonymous ~typ:ty
- in
- match outtypeinstances with
- | [] ->
- let extended_context =
- let rec add_right_args =
- function
- Cic.Prod (name,ty,t) ->
- Some (name,Cic.Decl ty)::(add_right_args t)
- | _ -> []
- in
- (Some (fresh_name,Cic.Decl ty))::
- (List.rev
- (add_right_args arity_instantiated_with_left_args))@
- context
- in
- let metasenv,new_meta =
- CicMkImplicit.mk_implicit metasenv subst extended_context
- in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable
- extended_context
- in
- let rec add_lambdas b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas b t))
- | _ -> Cic.Lambda (fresh_name, ty, b)
- in
- let candidate =
- add_lambdas (Cic.Meta (new_meta,irl))
- arity_instantiated_with_left_args
- in
- (Some candidate),ugraph4,metasenv,subst
- | (constructor_args_no,_,instance,_)::tl ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let candidate,ugraph,metasenv,subst =
- List.fold_left (
- fun (candidate_oty,ugraph,metasenv,subst)
- (constructor_args_no,_,instance,_) ->
- match candidate_oty with
- | None -> None,ugraph,metasenv,subst
- | Some ty ->
- try
- let instance',subst,metasenv =
- CicMetaSubst.delift_rels subst metasenv
- constructor_args_no instance
- in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv
- instance' ty ugraph
- in
- candidate_oty,ugraph,metasenv,subst
- with
- CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable
- | RefineFailure _ | Uncertain _ ->
- None,ugraph,metasenv,subst
- ) (Some instance',ugraph4,metasenv,subst) tl
- in
- match candidate with
- | None -> None, ugraph,metasenv,subst
- | Some t ->
- let rec add_lambdas n b =
- function
- Cic.Prod (name,ty,t) ->
- Cic.Lambda (name,ty,(add_lambdas (n + 1) b t))
- | _ ->
- Cic.Lambda (fresh_name, ty,
- CicSubstitution.lift (n + 1) t)
- in
- Some
- (add_lambdas 0 t arity_instantiated_with_left_args),
- ugraph,metasenv,subst
- with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
- None,ugraph4,metasenv,subst
- in
- match candidate with
- | None -> raise (Uncertain (lazy "can't solve an higher order unification problem"))
- | Some candidate ->
- let subst,metasenv,ugraph =
- try
- fo_unif_subst subst context metasenv
- candidate outtype ugraph5
- with
- exn -> assert false(* unification against a metavariable *)
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (Cic.Appl (outtype::right_args@[term']))),
- subst,metasenv,ugraph)
- | _ -> (* easy case *)
- let tlbody_and_type,subst,metasenv,ugraph4 =
- typeof_list subst metasenv context ugraph4 (right_args @ [term'])
- in
- let _,_,_,subst,metasenv,ugraph4 =
- eat_prods false subst metasenv context
- outtype outtypety tlbody_and_type ugraph4
- in
- let _,_, subst, metasenv,ugraph5 =
- type_of_aux subst metasenv context
- (C.Appl ((outtype :: right_args) @ [term'])) ugraph4
- in
- let (subst,metasenv,ugraph6) =
- List.fold_left2
- (fun (subst,metasenv,ugraph)
- p (constructor_args_no,context,instance,args)
- ->
- let instance' =
- let appl =
- let outtype' =
- CicSubstitution.lift constructor_args_no outtype
- in
- C.Appl (outtype'::args)
- in
- CicReduction.head_beta_reduce ~delta:false
- ~upto:(List.length args) appl
- in
- try
- fo_unif_subst subst context metasenv instance instance'
- ugraph
- with
- exn ->
- enrich localization_tbl p exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst p
- context ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance'
- context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst instance
- context)))
- (subst,metasenv,ugraph5) pl' outtypeinstances
- in
- C.MutCase (uri, i, outtype, term', pl'),
- CicReduction.head_beta_reduce
- (CicMetaSubst.apply_subst subst
- (C.Appl(outtype::right_args@[term']))),
- subst,metasenv,ugraph6)
- | C.Fix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,_,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty')))
- :: types, ugraph, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context'))
- in
- fl @ [bo'] , subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.Fix (i,fl''),ty,subst,metasenv,ugraph2
- | C.CoFix (i,fl) ->
- let fl_ty',subst,metasenv,types,ugraph1,len =
- List.fold_left
- (fun (fl,subst,metasenv,types,ugraph,len) (n,ty,_) ->
- let ty',_,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context ty ugraph
- in
- fl @ [ty'],subst',metasenv',
- Some (C.Name n,(C.Decl (CicSubstitution.lift len ty'))) ::
- types, ugraph1, len+1
- ) ([],subst,metasenv,[],ugraph,0) fl
- in
- let context' = types@context in
- let fl_bo',subst,metasenv,ugraph2 =
- List.fold_left
- (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
- let bo',ty_of_bo,subst,metasenv,ugraph1 =
- type_of_aux subst metasenv context' bo ugraph in
- let expected_ty = CicSubstitution.lift len ty in
- let subst',metasenv',ugraph' =
- try
- fo_unif_subst subst context' metasenv
- ty_of_bo expected_ty ugraph1
- with
- exn ->
- enrich localization_tbl bo exn
- ~f:(function _ ->
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst bo
- context' ^ " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
- context' ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
- context))
- in
- fl @ [bo'],subst',metasenv',ugraph'
- ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty')
- in
- let ty = List.nth fl_ty' i in
- (* now we have the new ty in fl_ty', the new bo in fl_bo',
- * and we want the new fl with bo' and ty' injected in the right
- * place.
- *)
- let rec map3 f l1 l2 l3 =
- match l1,l2,l3 with
- | [],[],[] -> []
- | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3)
- | _ -> assert false
- in
- let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') )
- fl_ty' fl_bo' fl
- in
- C.CoFix (i,fl''),ty,subst,metasenv,ugraph2
- in
- relocalize localization_tbl t t';
- res
-
- (* check_metasenv_consistency checks that the "canonical" context of a
- metavariable is consitent - up to relocation via the relocation list l -
- with the actual context *)
- and check_metasenv_consistency
- metano subst metasenv context canonical_context l ugraph
- =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let lifted_canonical_context =
- let rec aux i =
- function
- [] -> []
- | (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
- | None::tl -> None::(aux (i+1) tl)
- | (Some (n,C.Def (t,ty)))::tl ->
- (Some
- (n,
- C.Def
- (S.subst_meta l (S.lift i t),
- S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl)
- in
- aux 1 canonical_context
in
- try
- List.fold_left2
- (fun (l,subst,metasenv,ugraph) t ct ->
- match (t,ct) with
- _,None ->
- l @ [None],subst,metasenv,ugraph
- | Some t,Some (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly
- expensive reduction that can be easily avoided and
- that is quite frequent. However, this is better
- handled using levels to control reduction *)
- let optimized_t =
- match t with
- Cic.Rel n ->
- (try
- match List.nth context (n - 1) with
- Some (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with
- Failure _ -> t)
- | _ -> t
- in
- let subst',metasenv',ugraph' =
- (try
-(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e'
- * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*)
- fo_unif_subst subst context metasenv optimized_t ct ugraph
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
- in
- l @ [Some t],subst',metasenv',ugraph'
- | Some t,Some (_,C.Decl ct) ->
- let t',inferredty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context t ugraph
- in
- let subst'',metasenv'',ugraph2 =
- (try
- fo_unif_subst
- subst' context metasenv' inferredty ct ugraph1
- with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' subst' ct) (match e with AssertFailure msg -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e))))))
- in
- l @ [Some t'], subst'',metasenv'',ugraph2
- | None, Some _ ->
- raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))) ([],subst,metasenv,ugraph) l lifted_canonical_context
- with
- Invalid_argument _ ->
- raise
- (RefineFailure
- (lazy (sprintf
- "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
- (CicMetaSubst.ppterm ~metasenv subst (Cic.Meta (metano, l)))
- (CicMetaSubst.ppcontext ~metasenv subst canonical_context))))
-
- and check_exp_named_subst metasubst metasenv context tl ugraph =
- let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph =
- match tl with
- [] -> [],metasubst,metasenv,ugraph
- | (uri,t)::tl ->
- let ty_uri,ugraph1 = type_of_variable uri ugraph in
- let typeofvar =
- CicSubstitution.subst_vars substs ty_uri in
- (* CSC: why was this code here? it is wrong
- (match CicEnvironment.get_cooked_obj ~trust:false uri with
- Cic.Variable (_,Some bo,_,_) ->
- raise
- (RefineFailure (lazy
- "A variable with a body can not be explicit substituted"))
- | Cic.Variable (_,None,_,_) -> ()
- | _ ->
- raise
- (RefineFailure (lazy
- ("Unkown variable definition " ^ UriManager.string_of_uri uri)))
- ) ;
- *)
- let t',typeoft,metasubst',metasenv',ugraph2 =
- type_of_aux metasubst metasenv context t ugraph1 in
- let subst = uri,t' in
- let metasubst'',metasenv'',ugraph3 =
- try
- fo_unif_subst
- metasubst' context metasenv' typeoft typeofvar ugraph2
- with _ ->
- raise (RefineFailure (lazy
- ("Wrong Explicit Named Substitution: " ^
- CicMetaSubst.ppterm metasenv' metasubst' typeoft ^
- " not unifiable with " ^
- CicMetaSubst.ppterm metasenv' metasubst' typeofvar)))
- in
- (* FIXME: no mere tail recursive! *)
- let exp_name_subst, metasubst''', metasenv''', ugraph4 =
- check_exp_named_subst_aux
- metasubst'' metasenv'' (substs@[subst]) tl ugraph3
- in
- ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4
- in
- check_exp_named_subst_aux metasubst metasenv [] tl ugraph
-
-
- and sort_of_prod localize subst metasenv context (name,s) t (t1, t2)
- ugraph
- =
- let module C = Cic in
- let context_for_t2 = (Some (name,C.Decl s))::context in
- let t1'' = CicReduction.whd ~subst context t1 in
- let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
- match (t1'', t2'') with
- | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) ->
- (* different than Coq manual!!! *)
- C.Sort s2,subst,metasenv,ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),subst,metasenv,ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
- | (C.Sort _,C.Sort (C.Type t1)) ->
- C.Sort (C.Type t1),subst,metasenv,ugraph
- | (C.Sort _,C.Sort (C.CProp t1)) ->
- C.Sort (C.CProp t1),subst,metasenv,ugraph
- | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
- | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
- (* TODO how can we force the meta to become a sort? If we don't we
- * break the invariant that refine produce only well typed terms *)
- (* TODO if we check the non meta term and if it is a sort then we
- * are likely to know the exact value of the result e.g. if the rhs
- * is a Sort (Prop | Set | CProp) then the result is the rhs *)
- let (metasenv,idx) =
- CicMkImplicit.mk_implicit_sort metasenv subst in
- let (subst, metasenv,ugraph1) =
- try
- fo_unif_subst subst context_for_t2 metasenv
- (C.Meta (idx,[])) t2'' ugraph
- with _ -> assert false (* unification against a metavariable *)
- in
- t2'',subst,metasenv,ugraph1
- | (C.Sort _,_)
- | (C.Meta _,_) ->
- enrich localization_tbl s
- (RefineFailure
- (lazy
- (sprintf
- "%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context ~metasenv subst t context)
- (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context))))
- | _,_ ->
- enrich localization_tbl t
- (RefineFailure
- (lazy
- (sprintf
- "%s is supposed to be a type, but its type is %s"
- (CicMetaSubst.ppterm_in_context ~metasenv subst s context)
- (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context))))
-
- and avoid_double_coercion context subst metasenv ugraph t ty =
- if not !pack_coercions then
- t,ty,subst,metasenv,ugraph
- else
- let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in
- if b then
- let source_carr = CoercGraph.source_of c2 in
- let tgt_carr = CicMetaSubst.apply_subst subst ty in
- (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr
- with
- | CoercGraph.SomeCoercion candidates ->
- let selected =
- HExtlib.list_findopt
- (function (metasenv,last,c) ->
- match c with
- | c when not (CoercGraph.is_composite c) ->
- debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c));
- None
- | c ->
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last head ugraph in
- debug_print (lazy ("\nprovo" ^ CicPp.ppterm c));
- (try
- debug_print
- (lazy
- ("packing: " ^
- CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c));
- let newt,_,subst,metasenv,ugraph =
- type_of_aux subst metasenv context c ugraph in
- debug_print (lazy "tipa...");
- let subst, metasenv, ugraph =
- (* COME MAI C'ERA UN IF su !pack_coercions ??? *)
- fo_unif_subst subst context metasenv newt t ugraph
- in
- debug_print (lazy "unifica...");
- Some (newt, ty, subst, metasenv, ugraph)
- with
- | RefineFailure s | Uncertain s when not !pack_coercions->
- debug_print s; debug_print (lazy "stop\n");None
- | RefineFailure s | Uncertain s ->
- debug_print s;debug_print (lazy "goon\n");
- try
- let old_pack_coercions = !pack_coercions in
- pack_coercions := false; (* to avoid diverging *)
- let refined_c1_c2_implicit,ty,subst,metasenv,ugraph =
- type_of_aux subst metasenv context c1_c2_implicit ugraph
- in
- pack_coercions := old_pack_coercions;
- let b, _, _, _, _ =
- is_a_double_coercion refined_c1_c2_implicit
- in
- if b then
- None
- else
- let head' =
- match refined_c1_c2_implicit with
- | Cic.Appl l -> HExtlib.list_last l
- | _ -> assert false
- in
- let subst, metasenv, ugraph =
- try fo_unif_subst subst context metasenv
- head head' ugraph
- with RefineFailure s| Uncertain s->
- debug_print s;assert false
- in
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv
- refined_c1_c2_implicit t ugraph
- in
- Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph)
- with
- | RefineFailure s | Uncertain s ->
- pack_coercions := true;debug_print s;None
- | exn -> pack_coercions := true; raise exn))
- candidates
- in
- (match selected with
- | Some x -> x
- | None ->
- debug_print
- (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t));
- t, ty, subst, metasenv, ugraph)
- | _ -> t, ty, subst, metasenv, ugraph)
- else
- t, ty, subst, metasenv, ugraph
-
- and typeof_list subst metasenv context ugraph l =
- let tlbody_and_type,subst,metasenv,ugraph =
- List.fold_right
- (fun x (res,subst,metasenv,ugraph) ->
- let x',ty,subst',metasenv',ugraph1 =
- type_of_aux subst metasenv context x ugraph
- in
- (x', ty)::res,subst',metasenv',ugraph1
- ) l ([],subst,metasenv,ugraph)
- in
- tlbody_and_type,subst,metasenv,ugraph
-
- and eat_prods
- allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph
- =
- (* given he:hety, gives beack all (c he) such that (c e):?->? *)
- let fix_arity n metasenv context subst he hetype ugraph =
- let hetype = CicMetaSubst.apply_subst subst hetype in
- (* instead of a dummy functional type we may create the real product
- * using args_bo_and_ty, but since coercions lookup ignores the
- * actual ariety we opt for the simple solution *)
- let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in
- match CoercGraph.look_for_coercion metasenv subst context hetype fty with
- | CoercGraph.NoCoercion -> []
- | CoercGraph.NotHandled ->
- raise (MoreArgsThanExpected (n,Uncertain (lazy "")))
- | CoercGraph.SomeCoercionToTgt candidates
- | CoercGraph.SomeCoercion candidates ->
- HExtlib.filter_map
- (fun (metasenv,last,coerc) ->
- let pp t =
- CicMetaSubst.ppterm_in_context ~metasenv subst t context in
- try
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last he ugraph in
- debug_print (lazy ("New head: "^ pp coerc));
- let tty,ugraph =
- CicTypeChecker.type_of_aux' ~subst metasenv context coerc
- ugraph
- in
- debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
- with
- | Uncertain _ | RefineFailure _
- | HExtlib.Localized (_,Uncertain _)
- | HExtlib.Localized (_,RefineFailure _) -> None
- | exn -> assert false)
- candidates
- in
- (* aux function to process the type of the head and the args in parallel *)
- let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs =
- function
- | [] -> newargs,subst,metasenv,he,hetype,ugraph
- | (hete, hety)::tl as args ->
- match (CicReduction.whd ~subst context hetype) with
- | Cic.Prod (n,s,t) ->
- let arg,subst,metasenv,ugraph =
- coerce_to_something allow_coercions localization_tbl
- hete hety s subst metasenv context ugraph in
- eat_prods_and_args
- metasenv subst context he (CicSubstitution.subst (fst arg) t)
- ugraph (newargs@[arg]) tl
- | _ ->
- let he =
- match he, newargs with
- | _, [] -> he
- | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs)
- | _ -> Cic.Appl (he::List.map fst newargs)
- in
- (*{{{*) debug_print (lazy
- let pp x =
- CicMetaSubst.ppterm_in_context ~metasenv subst x context in
- "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^
- "\n but is applyed to: " ^ String.concat ";"
- (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*)
- let possible_fixes =
- fix_arity (List.length args) metasenv context subst he hetype
- ugraph in
- match
- HExtlib.list_findopt
- (fun (he,hetype,subst,metasenv,ugraph) ->
- (* {{{ *)debug_print (lazy ("Try fix: "^
- CicMetaSubst.ppterm_in_context ~metasenv subst he context));
- debug_print (lazy (" of type: "^
- CicMetaSubst.ppterm_in_context
- ~metasenv subst hetype context)); (* }}} *)
- try
- Some (eat_prods_and_args
- metasenv subst context he hetype ugraph [] args)
- with
- | RefineFailure _ | Uncertain _
- | HExtlib.Localized (_,RefineFailure _)
- | HExtlib.Localized (_,Uncertain _) -> None)
- possible_fixes
- with
- | Some x -> x
- | None ->
- raise
- (MoreArgsThanExpected
- (List.length args, RefineFailure (lazy "")))
- in
- (* first we check if we are in the simple case of a meta closed term *)
- let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
- if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then
- (* this optimization is to postpone fix_arity (the most common case)*)
- subst,metasenv,ugraph,hetype,he,args_bo_and_ty
- else
- (* this (says CSC) is also useful to infer dependent types *)
- let pristinemenv = metasenv in
- let metasenv,hetype' =
- mk_prod_of_metas metasenv context subst args_bo_and_ty
- in
- try
- let subst,metasenv,ugraph =
- fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph
- in
- subst,metasenv,ugraph,hetype',he,args_bo_and_ty
- with RefineFailure _ | Uncertain _ ->
- subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty
- in
- let coerced_args,subst,metasenv,he,t,ugraph =
- try
- eat_prods_and_args
- metasenv subst context he hetype' ugraph1 [] args_bo_and_ty
- with
- MoreArgsThanExpected (residuals,exn) ->
- more_args_than_expected localization_tbl metasenv
- subst he context hetype' residuals args_bo_and_ty exn
- in
- he,(List.map fst coerced_args),t,subst,metasenv,ugraph
+ force_ty metasenv subst context orig t infty expty
+ in
+ typeof_aux metasenv subst context expty term
- and coerce_to_something
- allow_coercions localization_tbl t infty expty subst metasenv context ugraph
- =
- let module CS = CicSubstitution in
- let module CR = CicReduction in
- let cs_subst = CS.subst ~avoid_beta_redexes:true in
- let coerce_atom_to_something t infty expty subst metasenv context ugraph =
- debug_print (lazy ("COERCE_ATOM_TO_SOMETHING"));
- let coer =
- CoercGraph.look_for_coercion metasenv subst context infty expty
- in
- match coer with
- | CoercGraph.NoCoercion
- | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy
- "coerce_atom_to_something fails since no coercions found"))
- | CoercGraph.NotHandled when
- not (CicUtil.is_meta_closed infty) ||
- not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy
- "coerce_atom_to_something fails since carriers have metas"))
- | CoercGraph.NotHandled -> raise (RefineFailure (lazy
- "coerce_atom_to_something fails since no coercions found"))
- | CoercGraph.SomeCoercion candidates ->
- debug_print (lazy (string_of_int (List.length candidates) ^
- " candidates found"));
- let uncertain = ref false in
- let selected =
- let posibilities =
- HExtlib.filter_map
- (fun (metasenv,last,c) ->
- try
- (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst last context ^
- " <==> " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^
- "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c
- context));
- debug_print (lazy ("FO_UNIF_SUBST: " ^
- CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *)
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last t ugraph
- in
- let newt,newhety,subst,metasenv,ugraph =
- type_of_aux subst metasenv context c ugraph in
- let newt, newty, subst, metasenv, ugraph =
- avoid_double_coercion context subst metasenv ugraph newt expty
- in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv newhety expty ugraph in
- Some ((newt,newty), subst, metasenv, ugraph)
- with
- | Uncertain _ -> uncertain := true; None
- | RefineFailure _ -> None)
- candidates
- in
- match
- List.fast_sort
- (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2)
- posibilities
- with
- | [] -> None
- | x::_ -> Some x
+and eat_prods localise metasenv subst context orig_he he ty_he args =
+ let rec aux metasenv subst args_so_far ty_he = function
+ | [] -> metasenv, subst, NCic.Appl (he :: List.rev args_so_far), ty_he
+ | arg::tl ->
+ match NCicReduction.whd ~subst context ty_he with
+ | C.Prod (_,s,t) ->
+ let metasenv, subst, arg, _ =
+ typeof ~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) t tl
+ | t ->
+ let metasenv, subst, arg, ty_arg =
+ typeof ~localise metasenv subst context arg None in
+ let metasenv, meta, _ =
+ NCicMetaSubst.mk_meta metasenv
+ (("_",C.Decl ty_arg) :: context) None
in
- match selected with
- | Some x -> x
- | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails"))
- | None -> raise (RefineFailure (lazy "coerce_atom fails"))
- in
- let rec coerce_to_something_aux
- t infty expty subst metasenv context ugraph
- =
- try
- let subst, metasenv, ugraph =
- fo_unif_subst subst context metasenv infty expty ugraph
- in
- (t, expty), subst, metasenv, ugraph
- with (Uncertain _ | RefineFailure _ as exn)
- when allow_coercions && !insert_coercions ->
- let whd = CicReduction.whd ~delta:false in
- let clean t s c = whd c (CicMetaSubst.apply_subst s t) in
- let infty = clean infty subst context in
- let expty = clean expty subst context in
- let t = clean t subst context in
- (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^
- CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*)
- let (coerced,_),subst,metasenv,_ as result =
- match infty, expty, t with
- | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) ->
- (*{{{*) debug_print (lazy "FIX");
- (match fl with
- [name,i,_(* infty *),bo] ->
- let context_bo =
- Some (Cic.Name name,Cic.Decl expty)::context in
- let (rel1, _), subst, metasenv, ugraph =
- coerce_to_something_aux (Cic.Rel 1)
- (CS.lift 1 expty) (CS.lift 1 infty) subst
- metasenv context_bo ugraph in
- let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in
- let (bo,_), subst, metasenv, ugraph =
- coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1
- expty) subst
- metasenv context_bo ugraph
- in
- (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph
- | _ -> assert false (* not implemented yet *)) (*}}}*)
- | _,_, Cic.MutCase (uri,tyno,outty,m,pl) ->
- (*{{{*) debug_print (lazy "CASE");
- (* {{{ helper functions *)
- let get_cl_and_left_p uri tyno outty ugraph =
- match CicEnvironment.get_obj ugraph uri with
- | Cic.InductiveDefinition (tl, _, leftno, _),ugraph ->
- let count_pis t =
- let rec aux ctx t =
- match CicReduction.whd ~delta:false ctx t with
- | Cic.Prod (name,src,tgt) ->
- let ctx = Some (name, Cic.Decl src) :: ctx in
- 1 + aux ctx tgt
- | _ -> 0
- in
- aux [] t
- in
- let rec skip_lambda_delifting t n =
- match t,n with
- | _,0 -> t
- | Cic.Lambda (_,_,t),n ->
- skip_lambda_delifting
- (CS.subst (Cic.Implicit None) t) (n - 1)
- | _ -> assert false
- in
- let get_l_r_p n = function
- | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
- | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
- HExtlib.split_nth n args
- | _ -> assert false
- in
- let _, _, ty, cl = List.nth tl tyno in
- let pis = count_pis ty in
- let rno = pis - leftno in
- let t = skip_lambda_delifting outty rno in
- let left_p, _ = get_l_r_p leftno t in
- let instantiale_with_left cl =
- List.map
- (fun ty ->
- List.fold_left
- (fun t p -> match t with
- | Cic.Prod (_,_,t) ->
- cs_subst p t
- | _-> assert false)
- ty left_p)
- cl
- in
- let cl = instantiale_with_left (List.map snd cl) in
- cl, left_p, leftno, rno, ugraph
- | _ -> raise exn
- in
- let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
- match t,n with
- | _,0 ->
- let rec mkr n = function
- | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl
- in
- let bo =
- CicReplace.replace_lifting
- ~equality:(fun _ -> CicUtil.alpha_equivalence)
- ~context:ctx
- ~what:(matched::right_p)
- ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p))
- ~where:bo
- in
- bo
- | Cic.Lambda (name, src, tgt),_ ->
- Cic.Lambda (name, src,
- keep_lambdas_and_put_expty
- (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo)
- (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1))
- | _ -> assert false
- in
- let eq_uri, eq, eq_refl =
- match LibraryObjects.eq_URI () with
- | None -> HLog.warn "no default equality"; raise exn
- | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[])
- in
- let add_params
- metasenv subst context uri tyno cty outty mty m leftno i
- =
- let rec aux context outty par k mty m = function
- | Cic.Prod (name, src, tgt) ->
- let t,k =
- aux
- (Some (name, Cic.Decl src) :: context)
- (CS.lift 1 outty) (Cic.Rel k::par) (k+1)
- (CS.lift 1 mty) (CS.lift 1 m) tgt
- in
- Cic.Prod (name, src, t), k
- | Cic.MutInd _ ->
- let k =
- let k = Cic.MutConstruct (uri,tyno,i,[]) in
- if par <> [] then Cic.Appl (k::par) else k
- in
- Cic.Prod (Cic.Name "p",
- Cic.Appl [eq; mty; m; k],
- (CS.lift 1
- (CR.head_beta_reduce ~delta:false
- (Cic.Appl [outty;k])))),k
- | Cic.Appl (Cic.MutInd _::pl) ->
- let left_p,right_p = HExtlib.split_nth leftno pl in
- let has_rights = right_p <> [] in
- let k =
- let k = Cic.MutConstruct (uri,tyno,i,[]) in
- Cic.Appl (k::left_p@par)
- in
- let right_p =
- try match
- CicTypeChecker.type_of_aux' ~subst metasenv context k
- CicUniv.oblivion_ugraph
- with
- | Cic.Appl (Cic.MutInd _::args),_ ->
- snd (HExtlib.split_nth leftno args)
- | _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _-> assert false
- in
- if has_rights then
- CR.head_beta_reduce ~delta:false
- (Cic.Appl (outty ::right_p @ [k])),k
- else
- Cic.Prod (Cic.Name "p",
- Cic.Appl [eq; mty; m; k],
- (CS.lift 1
- (CR.head_beta_reduce ~delta:false
- (Cic.Appl (outty ::right_p @ [k]))))),k
- | _ -> assert false
- in
- aux context outty [] 1 mty m cty
- in
- let add_lambda_for_refl_m pbo rno mty m k cty =
- (* k lives in the right context *)
- if rno <> 0 then pbo else
- let rec aux mty m = function
- | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) ->
- Cic.Lambda (name,src,
- (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty)))
- | t,_ ->
- Cic.Lambda (Cic.Name "p",
- Cic.Appl [eq; mty; m; k],CS.lift 1 t)
- in
- aux mty m (pbo,cty)
- in
- let add_pi_for_refl_m new_outty mty m rno =
- if rno <> 0 then new_outty else
- let rec aux m mty = function
- | Cic.Lambda (name, src, tgt) ->
- Cic.Lambda (name, src,
- aux (CS.lift 1 m) (CS.lift 1 mty) tgt)
- | t ->
- Cic.Prod
- (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1],
- CS.lift 1 t)
- in
- aux m mty new_outty
- in (* }}} end helper functions *)
- (* constructors types with left params already instantiated *)
- let outty = CicMetaSubst.apply_subst subst outty in
- let cl, left_p, leftno,rno,ugraph =
- get_cl_and_left_p uri tyno outty ugraph
- in
- let right_p, mty =
- try
- match
- CicTypeChecker.type_of_aux' ~subst metasenv context m
- CicUniv.oblivion_ugraph
- with
- | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
- | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
- snd (HExtlib.split_nth leftno args), mty
- | _ -> assert false
- with CicTypeChecker.TypeCheckerFailure _ ->
- raise (AssertFailure(lazy "already ill-typed matched term"))
- in
- let new_outty =
- keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
- in
- debug_print
- (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
- ~metasenv subst new_outty context));
- let _,pl,subst,metasenv,ugraph =
- List.fold_right2
- (fun cty pbo (i, acc, s, menv, ugraph) ->
- (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
- * (new_)outty right_par (K_i left_par k_par) *)
- let infty_pbo, _ =
- add_params menv s context uri tyno
- cty outty mty m leftno i in
- debug_print
- (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
- ~metasenv subst infty_pbo context));
- let expty_pbo, k = (* k is (K_i left_par k_par) *)
- add_params menv s context uri tyno
- cty new_outty mty m leftno i in
- debug_print
- (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
- ~metasenv subst expty_pbo context));
- let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
- debug_print
- (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
- ~metasenv subst pbo context));
- let (pbo, _), subst, metasenv, ugraph =
- coerce_to_something_aux pbo infty_pbo expty_pbo
- s menv context ugraph
- in
- debug_print
- (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
- ~metasenv subst pbo context));
- (i-1, pbo::acc, subst, metasenv, ugraph))
- cl pl (List.length pl, [], subst, metasenv, ugraph)
- in
- let new_outty = add_pi_for_refl_m new_outty mty m rno in
- debug_print
- (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context
- ~metasenv subst new_outty context));
- let t =
- if rno = 0 then
- let refl_m=Cic.Appl[eq_refl;mty;m]in
- Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m]
- else
- Cic.MutCase(uri,tyno,new_outty,m,pl)
- in
- (t, expty), subst, metasenv, ugraph (*}}}*)
- | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ ->
- (*{{{*) debug_print (lazy "LAM");
- let name_con =
- FreshNamesGenerator.mk_fresh_name
- ~subst metasenv context ~typ:src2 Cic.Anonymous
- in
- let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in
- (* contravariant part: the argument of f:src->ty *)
- let (rel1, _), subst, metasenv, ugraph =
- coerce_to_something_aux
- (Cic.Rel 1) (CS.lift 1 src2)
- (CS.lift 1 src) subst metasenv context_src2 ugraph
- in
- (* covariant part: the result of f(c x); x:src2; (c x):src *)
- let name_t, bo =
- match t with
- | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo)
- | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1]
- in
- (* we fix the possible dependency problem in the source ty *)
- let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in
- let (bo, _), subst, metasenv, ugraph =
- coerce_to_something_aux
- bo ty ty2 subst metasenv context_src2 ugraph
- in
- let coerced = Cic.Lambda (name_t,src2, bo) in
- (coerced, expty), subst, metasenv, ugraph (*}}}*)
- | _ ->
- (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context
- ~metasenv subst infty context ^ " ==> " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst expty context));
- coerce_atom_to_something
- t infty expty subst metasenv context ugraph (*}}}*)
+ let flex_prod = C.Prod ("_", ty_arg, meta) in
+ let metasenv, subst =
+ try NCicUnification.unify metasenv subst context t flex_prod
+ with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
+ ("The term %s is here applied to %d arguments but expects " ^^
+ "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+ (List.length args) (List.length args_so_far))) exc)
+ (* XXX coerce to funclass *)
in
- debug_print (lazy ("COERCE TO SOMETHING END: "^
- CicMetaSubst.ppterm_in_context ~metasenv subst coerced context));
- result
- in
- try
- coerce_to_something_aux t infty expty subst metasenv context ugraph
- with Uncertain _ | RefineFailure _ as exn ->
- let f _ =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context metasenv subst t context ^
- " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst
- infty context ^ " but is here used with type " ^
- CicMetaSubst.ppterm_in_context metasenv subst expty context)
- in
- enrich localization_tbl ~f t exn
-
- and coerce_to_sort localization_tbl t infty subst context metasenv uragph =
- match CicReduction.whd ~delta:false ~subst context infty with
- | Cic.Meta _ | Cic.Sort _ ->
- t,infty, subst, metasenv, ugraph
- | src ->
- debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context
- ~metasenv subst src context));
- let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
- try
- let (t, ty_t), subst, metasenv, ugraph =
- coerce_to_something true
- localization_tbl t src tgt subst metasenv context ugraph
- in
- debug_print (lazy ("COERCE TO SORT END: "^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context));
- t, ty_t, subst, metasenv, ugraph
- with HExtlib.Localized (_, exn) ->
- let f _ =
- lazy ("(7)The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst t context
- ^ " is not a type since it has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv subst src context
- ^ " that is not a sort")
- in
- enrich localization_tbl ~f t exn
- in
-
- (* eat prods ends here! *)
-
- let t',ty,subst',metasenv',ugraph1 =
- type_of_aux [] metasenv context t ugraph
- in
- let substituted_t = CicMetaSubst.apply_subst subst' t' in
- let substituted_ty = CicMetaSubst.apply_subst subst' ty in
- (* Andrea: ho rimesso qui l'applicazione della subst al
- metasenv dopo che ho droppato l'invariante che il metsaenv
- e' sempre istanziato *)
- let substituted_metasenv =
- CicMetaSubst.apply_subst_metasenv subst' metasenv' in
- (* metasenv' *)
- (* substituted_t,substituted_ty,substituted_metasenv *)
- (* ANDREA: spostare tutta questa robaccia da un altra parte *)
- let cleaned_t =
- if clean_dummy_dependent_types then
- FreshNamesGenerator.clean_dummy_dependent_types substituted_t
- else substituted_t in
- let cleaned_ty =
- if clean_dummy_dependent_types then
- FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
- else substituted_ty in
- let cleaned_metasenv =
- if clean_dummy_dependent_types then
- List.map
- (function (n,context,ty) ->
- let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
- let context' =
- List.map
- (function
- None -> None
- | Some (n, Cic.Decl t) ->
- Some (n,
- Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
- | Some (n, Cic.Def (bo,ty)) ->
- let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
- let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty
- in
- Some (n, Cic.Def (bo',ty'))
- ) context
- in
- (n,context',ty')
- ) substituted_metasenv
- else
- substituted_metasenv
- in
- (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1)
-;;
-
-let undebrujin uri typesno tys t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (* here the explicit_named_substituion is assumed to be *)
- (* of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tys (typesno - 1,t))
-
-let map_first_n n start f g l =
- let rec aux acc k l =
- if k < n then
- match l with
- | [] -> raise (Invalid_argument "map_first_n")
- | hd :: tl -> f hd k (aux acc (k+1) tl)
- else
- g acc l
- in
- aux start 0 l
-
-(*CSC: this is a very rough approximation; to be finished *)
-let are_all_occurrences_positive metasenv ugraph uri tys leftno =
- let subst,metasenv,ugraph,tys =
- List.fold_right
- (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
- let subst,metasenv,ugraph,cl =
- List.fold_right
- (fun (name,ty) (subst,metasenv,ugraph,acc) ->
- let rec aux ctx k subst = function
- | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'->
- let subst,metasenv,ugraph,tl =
- map_first_n leftno
- (subst,metasenv,ugraph,[])
- (fun t n (subst,metasenv,ugraph,acc) ->
- let subst,metasenv,ugraph =
- fo_unif_subst
- subst ctx metasenv t (Cic.Rel (k-n)) ugraph
- in
- subst,metasenv,ugraph,(t::acc))
- (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl))
- tl
- in
- subst,metasenv,ugraph,(Cic.Appl (hd::tl))
- | Cic.MutInd(uri',_,_) as t when uri = uri'->
- subst,metasenv,ugraph,t
- | Cic.Prod (name,s,t) ->
- let ctx = (Some (name,Cic.Decl s))::ctx in
- let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in
- subst,metasenv,ugraph,Cic.Prod (name,s,t)
- | _ ->
- raise
- (RefineFailure
- (lazy "not well formed constructor type"))
- in
- let subst,metasenv,ugraph,ty = aux [] 0 subst ty in
- subst,metasenv,ugraph,(name,ty) :: acc)
- cl (subst,metasenv,ugraph,[])
- in
- subst,metasenv,ugraph,(name,ind,arity,cl)::acc)
- tys ([],metasenv,ugraph,[])
+ let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
+ aux metasenv subst (arg :: args_so_far) meta tl
in
- let substituted_tys =
- List.map
- (fun (name,ind,arity,cl) ->
- let cl =
- List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl
- in
- name,ind,CicMetaSubst.apply_subst subst arity,cl)
- tys
- in
- metasenv,ugraph,substituted_tys
-
-let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.oblivion_ugraph in
- match obj with
- Cic.Constant (name,Some bo,ty,args,attrs) ->
- (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
- since type_of_aux' destroys localization information (which are
- preserved by type_of_aux *)
- let loc exn' =
- try
- Cic.CicHash.find localization_tbl bo
- with Not_found ->
- HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
- raise exn' in
- let bo',boty,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] bo ugraph in
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- let subst,metasenv,ugraph =
- try
- fo_unif_subst [] [] metasenv boty ty' ugraph
- with
- RefineFailure _
- | Uncertain _ as exn ->
- let msg =
- lazy ("The term " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
- " has type " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
- " but is here used with type " ^
- CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
- in
- let exn' =
- match exn with
- RefineFailure _ -> RefineFailure msg
- | Uncertain _ -> Uncertain msg
- | _ -> assert false
- in
- raise (HExtlib.Localized (loc exn',exn'))
- in
- let bo' = CicMetaSubst.apply_subst subst bo' in
- let ty' = CicMetaSubst.apply_subst subst ty' in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
- | Cic.Constant (name,None,ty,args,attrs) ->
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph
- in
- Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
- | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
- assert (metasenv' = metasenv);
- (* Here we do not check the metasenv for correctness *)
- let bo',boty,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] bo ugraph in
- let ty',sort,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- begin
- match sort with
- Cic.Sort _
- (* instead of raising Uncertain, let's hope that the meta will become
- a sort *)
- | Cic.Meta _ -> ()
- | _ -> raise (RefineFailure (lazy "The term provided is not a type"))
- end;
- let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
- let bo' = CicMetaSubst.apply_subst subst bo' in
- let ty' = CicMetaSubst.apply_subst subst ty' in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph
- | Cic.Variable _ -> assert false (* not implemented *)
- | Cic.InductiveDefinition (tys,args,paramsno,attrs) ->
- (*CSC: this code is greately simplified and many many checks are missing *)
- (*CSC: e.g. the constructors are not required to build their own types, *)
- (*CSC: the arities are not required to have as type a sort, etc. *)
- let uri = match uri with Some uri -> uri | None -> assert false in
- let typesno = List.length tys in
- (* first phase: we fix only the types *)
- let metasenv,ugraph,tys =
- List.fold_right
- (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
- let ty',_,metasenv,ugraph =
- (* clean_dummy_dependent_types: false to avoid cleaning the names
- of the left products, that must be identical to those of the
- constructors; however, non-left products should probably be
- cleaned *)
- type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
- metasenv [] ty ugraph
- in
- metasenv,ugraph,(name,b,ty',cl)::res
- ) tys (metasenv,ugraph,[]) in
- let con_context =
- List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in
- (* second phase: we fix only the constructors *)
- let saved_menv = metasenv in
- let metasenv,ugraph,tys =
- List.fold_right
- (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
- let metasenv,ugraph,cl' =
- List.fold_right
- (fun (name,ty) (metasenv,ugraph,res) ->
- let ty =
- CicTypeChecker.debrujin_constructor
- ~cb:(relocalize localization_tbl) uri typesno [] ty in
- let ty',_,metasenv,ugraph =
- type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
- let ty' = undebrujin uri typesno tys ty' in
- metasenv@saved_menv,ugraph,(name,ty')::res
- ) cl (metasenv,ugraph,[])
- in
- metasenv,ugraph,(name,b,ty,cl')::res
- ) tys (metasenv,ugraph,[]) in
- (* third phase: we check the positivity condition *)
- let metasenv,ugraph,tys =
- are_all_occurrences_positive metasenv ugraph uri tys paramsno
- in
- Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph
-;;
-
-(* sara' piu' veloce che raffinare da zero? mah.... *)
-let pack_coercion metasenv ctx t =
- let module C = Cic in
- let rec merge_coercions ctx =
- let aux = (fun (u,t) -> u,merge_coercions ctx t) in
- function
- | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
- | C.Meta (n,subst) ->
- let subst' =
- List.map
- (function None -> None | Some t -> Some (merge_coercions ctx t)) subst
- in
- C.Meta (n,subst')
- | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty)
- | C.Prod (name,so,dest) ->
- let ctx' = (Some (name,C.Decl so))::ctx in
- C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.Lambda (name,so,dest) ->
- let ctx' = (Some (name,C.Decl so))::ctx in
- C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest)
- | C.LetIn (name,so,ty,dest) ->
- let ctx' = Some (name,(C.Def (so,ty)))::ctx in
- C.LetIn
- (name, merge_coercions ctx so, merge_coercions ctx ty,
- merge_coercions ctx' dest)
- | C.Appl l ->
- let l = List.map (merge_coercions ctx) l in
- let t = C.Appl l in
- let b,_,_,_,_ = is_a_double_coercion t in
- if b then
- let ugraph = CicUniv.oblivion_ugraph in
- let old_insert_coercions = !insert_coercions in
- insert_coercions := false;
- let newt, _, menv, _ =
- try
- type_of_aux' metasenv ctx t ugraph
- with RefineFailure _ | Uncertain _ ->
- t, t, [], ugraph
- in
- insert_coercions := old_insert_coercions;
- if metasenv <> [] || menv = [] then
- newt
- else
- (prerr_endline "PUO' SUCCEDERE!!!!!";t)
- else
- t
- | C.Var (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Var (uri, exp_named_subst)
- | C.Const (uri,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.Const (uri, exp_named_subst)
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutInd (uri,tyno,exp_named_subst)
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let exp_named_subst = List.map aux exp_named_subst in
- C.MutConstruct (uri,tyno,consno,exp_named_subst)
- | C.MutCase (uri,tyno,out,te,pl) ->
- let pl = List.map (merge_coercions ctx) pl in
- C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl)
- | C.Fix (fno, fl) ->
- let ctx' =
- List.fold_left
- (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
- ctx fl
- in
- let fl =
- List.map
- (fun (name,idx,ty,bo) ->
- (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo))
- fl
- in
- C.Fix (fno, fl)
- | C.CoFix (fno, fl) ->
- let ctx' =
- List.fold_left
- (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l)
- ctx fl
- in
- let fl =
- List.map
- (fun (name,ty,bo) ->
- (name, merge_coercions ctx ty, merge_coercions ctx' bo))
- fl
- in
- C.CoFix (fno, fl)
- in
- merge_coercions ctx t
-;;
-
-let pack_coercion_metasenv conjectures = conjectures (*
-
- TASSI: this code war written when coercions were a toy,
- now packing coercions involves unification thus
- the metasenv may change, and this pack coercion
- does not handle that.
-
- let module C = Cic in
- List.map
- (fun (i, ctx, ty) ->
- let ctx =
- List.fold_right
- (fun item ctx ->
- let item' =
- match item with
- Some (name, C.Decl t) ->
- Some (name, C.Decl (pack_coercion conjectures ctx t))
- | Some (name, C.Def (t,None)) ->
- Some (name,C.Def (pack_coercion conjectures ctx t,None))
- | Some (name, C.Def (t,Some ty)) ->
- Some (name, C.Def (pack_coercion conjectures ctx t,
- Some (pack_coercion conjectures ctx ty)))
- | None -> None
- in
- item'::ctx
- ) ctx []
- in
- ((i,ctx,pack_coercion conjectures ctx ty))
- ) conjectures
- *)
-;;
-
-let pack_coercion_obj obj = obj (*
-
- TASSI: this code war written when coercions were a toy,
- now packing coercions involves unification thus
- the metasenv may change, and this pack coercion
- does not handle that.
-
- let module C = Cic in
- match obj with
- | C.Constant (id, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (pack_coercion [] [] body)
- in
- let ty = pack_coercion [] [] ty in
- C.Constant (id, body, ty, params, attrs)
- | C.Variable (name, body, ty, params, attrs) ->
- let body =
- match body with
- | None -> None
- | Some body -> Some (pack_coercion [] [] body)
- in
- let ty = pack_coercion [] [] ty in
- C.Variable (name, body, ty, params, attrs)
- | C.CurrentProof (name, conjectures, body, ty, params, attrs) ->
- let conjectures = pack_coercion_metasenv conjectures in
- let body = pack_coercion conjectures [] body in
- let ty = pack_coercion conjectures [] ty in
- C.CurrentProof (name, conjectures, body, ty, params, attrs)
- | C.InductiveDefinition (indtys, params, leftno, attrs) ->
- let indtys =
- List.map
- (fun (name, ind, arity, cl) ->
- let arity = pack_coercion [] [] arity in
- let cl =
- List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl
- in
- (name, ind, arity, cl))
- indtys
- in
- C.InductiveDefinition (indtys, params, leftno, attrs) *)
+ aux metasenv subst [] ty_he args
;;
-
-
-(* DEBUGGING ONLY
-let type_of_aux' metasenv context term =
- try
- let (t,ty,m) =
- type_of_aux' metasenv context term in
- debug_print (lazy
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty));
- debug_print (lazy
- ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []));
- (t,ty,m)
- with
- | RefineFailure msg as e ->
- debug_print (lazy ("@@@ REFINE FAILED: " ^ msg));
- raise e
- | Uncertain msg as e ->
- debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
- raise e
-;; *)
-
-let profiler2 = HExtlib.profile "CicRefine"
-
-let type_of_aux' ?localization_tbl metasenv context term ugraph =
- profiler2.HExtlib.profile
- (type_of_aux' ?localization_tbl metasenv context term) ugraph
-
-let typecheck ~localization_tbl metasenv uri obj =
- profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj
-
-let _ = DoubleTypeInference.pack_coercion := pack_coercion;;
(* vim:set foldmethod=marker: *)
-*)
projects / helm.git / commitdiff