open Printf
+exception RefineFailure of string;;
+
exception Impossible of int;;
exception NotRefinable of string;;
exception Uncertain of string;;
exception ListTooShort;;
exception WrongUriToMutualInductiveDefinitions of string;;
exception RelToHiddenHypothesis;;
-exception MetasenvInconsistency;;
exception WrongArgumentNumber;;
let fdebug = ref 0;;
| C.Meta (n,l) ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let subst',metasenv' =
- check_metasenv_consistency subst metasenv context canonical_context l
+ check_metasenv_consistency n subst metasenv context canonical_context l
in
CicSubstitution.lift_meta l ty, subst', metasenv'
| 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
(* 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 context canonical_context l =
+ and check_metasenv_consistency
+ metano subst metasenv context canonical_context l
+ =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
| Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
- with _ -> raise MetasenvInconsistency)
+ 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 MetasenvInconsistency)
- | _, _ ->
- raise MetasenvInconsistency
+ 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"
+ (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext subst canonical_context)))
) (subst,metasenv) l lifted_canonical_context
and check_exp_named_subst metasubst metasenv context =
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 s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
C.Sort C.Type,subst,metasenv
- | (C.Meta _,_) | (_,C.Meta _) ->
+ | (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 *)
- let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
+ 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
- C.Meta (idx, irl), subst, metasenv
+ t2'',subst,metasenv
| (_,_) ->
raise (NotRefinable (sprintf
- "Two types were expected, found %s of type %s and %s of type %s"
+ "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
(CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
(CicPp.ppterm t2'')))
and eat_prods subst metasenv context hetype tlbody_and_type =
- (* TODO to be reviewed *)
- List.fold_left
- (fun (resty, subst, metasenv) (arg, argty) ->
- let context' = Some (Cic.Anonymous, Cic.Decl argty) :: context in
- let (metasenv, idx) = CicMkImplicit.mk_implicit metasenv context' in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context'
- in
- let newmeta = Cic.Meta (idx, irl) in
- let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in
- let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
- let (subst, metasenv) =
- CicUnification.fo_unif_subst subst context metasenv resty prod
- in
- (CicMetaSubst.subst subst arg newmeta, subst, metasenv))
- (hetype, subst, metasenv) tlbody_and_type
+ let rec aux context' args (resty,subst,metasenv) =
+ function
+ [] -> resty,subst,metasenv
+ | (arg,argty)::tl ->
+ let args' =
+ List.map
+ (function
+ None -> assert false
+ | Some t -> Some (CicMetaSubst.lift subst 1 t)
+ ) args in
+ let argty' = CicMetaSubst.lift subst (List.length args) argty in
+ let name =
+ (* 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_type metasenv (context'' @ context) in
+ let irl =
+ (Some (Cic.Rel 1))::args' @
+ (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
+ context)
+ in
+ let newmeta = Cic.Meta (idx, irl) in
+ let prod = Cic.Prod (name, argty, newmeta) in
+ let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
+ let (subst, metasenv) =
+ CicUnification.fo_unif_subst subst context metasenv resty prod
+ in
+ aux context'' (Some arg :: args)
+ (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
+ in
+ aux [] [] (hetype,subst,metasenv) tlbody_and_type
in
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
in
- (* we get rid of the metavariables that have been instantiated *)
- let metasenv'' =
- List.filter
- (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst'))
- metasenv'
+ let substituted_t = CicMetaSubst.apply_subst subst' t in
+ let substituted_ty = CicMetaSubst.apply_subst subst' ty in
+ let substituted_metasenv =
+ CicMetaSubst.apply_subst_metasenv subst' metasenv'
in
- (CicMetaSubst.apply_subst subst' t,
- CicMetaSubst.apply_subst subst' ty,
- CicMetaSubst.apply_subst_metasenv subst' metasenv'')
+ let cleaned_t =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+ let cleaned_ty =
+ FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+ let cleaned_metasenv =
+ 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' =
+ match ty with
+ None -> None
+ | Some ty ->
+ Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+ in
+ Some (n, Cic.Def (bo',ty'))
+ ) context
+ in
+ (n,context',ty')
+ ) substituted_metasenv
+ in
+ (cleaned_t,cleaned_ty,cleaned_metasenv)
+
;;
(* DEBUGGING ONLY *)
projects / helm.git / blobdiff