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;;
let module C = Cic in
let module R = CicMetaSubst in
let module Un = CicUnification in
- match R.whd metasenv subst context expectedtype with
+ match R.whd subst context expectedtype with
C.MutInd (_,_,_) ->
(n,context,actualtype, [term]), subst, metasenv
| C.Appl (C.MutInd (_,_,_)::tl) ->
| C.Prod (name,so,de) ->
(* we expect that the actual type of the branch has the due
number of Prod *)
- (match R.whd metasenv subst context actualtype with
+ (match R.whd subst context actualtype with
C.Prod (name',so',de') ->
let subst, metasenv =
Un.fo_unif_subst subst context metasenv so so' in
| 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'
+ CicSubstitution.lift_meta l ty, subst', metasenv'
| C.Sort s ->
C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
subst,metasenv
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)
+ sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
+ subst'',metasenv''
| 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 _,subst'''',metasenv'''' =
+ let _ =
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
raise
(WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
let rec count_prod t =
- match CicMetaSubst.whd metasenv subst context t with
+ match CicMetaSubst.whd subst context t with
C.Prod (_, _, t) -> 1 + (count_prod t)
| _ -> 0 in
let no_args = count_prod arity in
let _, subst, metasenv =
type_of_aux subst metasenv context expected_type
in
- let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
+ let actual_type = CicMetaSubst.whd subst context actual_type in
let subst,metasenv =
Un.fo_unif_subst subst context metasenv expected_type actual_type
in
type_of_aux subst metasenv context appl
in
*)
- CicMetaSubst.whd metasenv subst context appl
+ CicMetaSubst.whd subst context appl
in
Un.fo_unif_subst subst context metasenv instance instance')
(subst,metasenv) outtypeinstances in
- CicMetaSubst.whd metasenv subst
+ CicMetaSubst.whd subst
context (C.Appl(outtype::right_args@[term])),subst,metasenv
| C.Fix (i,fl) ->
let subst,metasenv,types =
type_of_aux subst metasenv context' bo
in
Un.fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+ ty_of_bo (CicMetaSubst.lift subst len ty)
) (subst,metasenv) fl in
-
let (_,_,ty,_) = List.nth fl i in
ty,subst,metasenv
| C.CoFix (i,fl) ->
type_of_aux subst metasenv context' bo
in
Un.fo_unif_subst subst context' metasenv
- ty_of_bo (CicMetaSubst.lift metasenv subst len ty)
+ ty_of_bo (CicMetaSubst.lift subst len ty)
) (subst,metasenv) fl in
let (_,ty,_) = List.nth fl i 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 (n,C.Def (t,None)))::tl ->
(Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
- | (Some (_,C.Def (_,Some _)))::_ -> assert false
+ | (Some (n,C.Def (t,Some ty)))::tl ->
+ (Some (n,
+ C.Def ((S.lift_meta l (S.lift i t)),
+ Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
in
aux 1 canonical_context
in
| Some t,Some (_,C.Def (ct,_)) ->
(try
CicUnification.fo_unif_subst subst context metasenv t ct
- with _ -> raise MetasenvInconsistency)
+ 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))))
| 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 _ -> 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))))
+ | 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
- (* ti could be a metavariable in the domain of the substitution *)
- let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
- let t1' = CicMetaSubst.apply_subst subst' t1 in
- let t2' = CicMetaSubst.apply_subst subst' t2 in
- let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
- let t2'' =
- CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
- in
+ let t1'' = CicMetaSubst.whd subst context t1 in
+ let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) 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 from Coq manual!!! *)
- C.Sort s2,subst',metasenv'
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
+ C.Sort s2
| (C.Sort s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
- C.Sort C.Type,subst',metasenv'
+ C.Sort C.Type
| (C.Meta _,_) | (_,C.Meta _) ->
- let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- C.Meta (idx, irl), subst, metasenv'
+ (* 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'' *)
| (_,_) ->
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 =
- function
- [] -> hetype,subst,metasenv
- | (hete, hety)::tl ->
- (match (CicMetaSubst.whd metasenv subst context hetype) with
- Cic.Prod (n,s,t) ->
- let subst',metasenv' =
- CicUnification.fo_unif_subst subst context metasenv s hety
- in
- CicReduction.fdebug := -1 ;
- eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
- | Cic.Meta _ as t ->
- raise
- (Uncertain
- ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
- | _ -> raise (NotRefinable "Appl: wrong Prod-type")
- )
+ and eat_prods subst metasenv context hetype 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 context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
+ let (metasenv, idx) =
+ CicMkImplicit.mk_implicit 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 (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
+ 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
- let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' 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''
- in
- CicMetaSubst.apply_subst subst'' t,
- CicMetaSubst.apply_subst subst'' ty,
- subst'', metasenv'''
+ (CicMetaSubst.apply_subst subst' t,
+ CicMetaSubst.apply_subst subst' ty,
+ CicMetaSubst.apply_subst_metasenv subst' metasenv')
;;
(* DEBUGGING ONLY *)
let type_of_aux' metasenv context term =
try
- let (t,ty,s,m) = type_of_aux' metasenv context term in
+ let (t,ty,m) = type_of_aux' metasenv context term in
+ debug_print
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
(*
- List.iter
- (function (i,t) ->
- debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
- List.iter
- (function (i,_,t) ->
- debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
-*)
debug_print
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
- (t,ty,s,m)
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
+*)
+ (t,ty,m)
with
| CicUnification.AssertFailure msg as e ->
debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
debug_print msg;
raise e
| e ->
-(*
- List.iter
- (function (i,_,t) ->
- debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
- metasenv ;
-*)
debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
raise e
;;