| C.Sort s ->
C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
subst,metasenv
- | C.Implicit -> raise (Impossible 21)
+ | C.Implicit _ -> raise (Impossible 21)
| C.Cast (te,ty) ->
let _,subst',metasenv' =
type_of_aux subst metasenv context ty in
let sort2,subst'',metasenv'' =
type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
in
- sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
- subst'',metasenv''
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
let type2,subst'',metasenv'' =
type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
in
(* only to check if the product is well-typed *)
- let _ =
+ let _,subst'''',metasenv'''' =
sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
in
- C.Prod (n,s,type2),subst''',metasenv'''
+ C.Prod (n,s,type2),subst'''',metasenv''''
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
let ty,subst',metasenv' = type_of_aux subst metasenv context s in
| Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
- with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
+ with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
(try
CicUnification.fo_unif_subst
subst' context metasenv' inferredty ct
- with _ -> raise (NotRefinable (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" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
+ with e -> raise (NotRefinable (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 subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| None, Some _ ->
raise (NotRefinable (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"
and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
+ let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicMetaSubst.whd subst context t1 in
- let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
+ let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
- C.Sort s2
+ C.Sort s2,subst,metasenv
| (C.Sort s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
- C.Sort C.Type
- | (C.Meta _,_) | (_,C.Meta _) ->
+ C.Sort C.Type,subst,metasenv
+ | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
+ | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
(* TODO how can we force the meta to become a sort? If we don't we
* brake 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 *)
- (C.Sort C.Type)
-(* t2'' *)
+ let (metasenv,idx) =
+ CicMkImplicit.mk_implicit_sort metasenv in
+ let (subst, metasenv) =
+ CicUnification.fo_unif_subst subst context_for_t2 metasenv
+ (C.Meta (idx,[])) t2''
+ in
+ t2'',subst,metasenv
| (_,_) ->
raise (NotRefinable (sprintf
"Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
) args in
let argty' = CicMetaSubst.lift subst (List.length args) argty in
let name =
- FreshNamesGenerator.mk_fresh_name
- (CicMetaSubst.apply_subst_metasenv subst metasenv)
- (CicMetaSubst.apply_subst_context subst context)
- Cic.Anonymous
- (CicMetaSubst.apply_subst subst argty) in
+ (* The name must be fresh for (context'@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'@context). *)
+ let name_hint =
+ FreshNamesGenerator.mk_fresh_name
+ (CicMetaSubst.apply_subst_metasenv subst metasenv)
+ (CicMetaSubst.apply_subst_context subst context)
+ Cic.Anonymous
+ (CicMetaSubst.apply_subst subst argty)
+ in
+ (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+ FreshNamesGenerator.mk_fresh_name
+ [] (context'@context) name_hint (Cic.Sort Cic.Prop)
+ in
let context'' = Some (name, Cic.Decl argty') :: context' in
let (metasenv, idx) =
- CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+ CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
let irl =
(Some (Cic.Rel 1))::args' @
(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
projects / helm.git / blobdiff