* http://cs.unibo.it/helm/.
*)
+open Printf
+
+exception RefineFailure of string;;
+
exception Impossible of int;;
exception NotRefinable of string;;
exception Uncertain of string;;
exception WrongUriToConstant of string;;
exception WrongUriToVariable of string;;
+exception ListTooShort;;
exception WrongUriToMutualInductiveDefinitions of string;;
exception RelToHiddenHypothesis;;
-exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
-exception FreeMetaFound of int;;
+exception WrongArgumentNumber;;
let fdebug = ref 0;;
let debug t context =
(*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
;;
+let debug_print = prerr_endline
+
+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 ListTooShort
+;;
+
let rec type_of_constant uri =
let module C = Cic in
let module R = CicReduction in
| _ -> raise (WrongUriToMutualInductiveDefinitions (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 =
+ let module C = Cic in
+ let module R = CicMetaSubst in
+ let module Un = CicUnification in
+ match R.whd subst context expectedtype with
+ C.MutInd (_,_,_) ->
+ (n,context,actualtype, [term]), subst, metasenv
+ | C.Appl (C.MutInd (_,_,_)::tl) ->
+ let (_,arguments) = split tl left_args_no in
+ (n,context,actualtype, arguments@[term]), subst, metasenv
+ | C.Prod (name,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 =
+ Un.fo_unif_subst subst context metasenv so so' 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
+ | _ -> raise WrongArgumentNumber)
+ | _ -> raise (NotRefinable "Prod or MutInd expected")
+
and type_of_aux' metasenv context t =
let rec type_of_aux subst metasenv context =
let module C = Cic in
(try
match List.nth context (n - 1) with
Some (_,C.Decl t) -> S.lift n t,subst,metasenv
- | Some (_,C.Def bo) ->
+ | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+ | Some (_,C.Def (bo,None)) ->
type_of_aux subst metasenv context (S.lift n bo)
| None -> raise RelToHiddenHypothesis
with
decr fdebug ;
ty,subst',metasenv'
| C.Meta (n,l) ->
- let (_,canonical_context,ty) =
- try
- List.find (function (m,_,_) -> n = m) metasenv
- with
- Not_found -> raise (FreeMetaFound n)
- in
+ 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
- | 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 inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' context ty
+ type_of_aux subst' metasenv' context te
in
(try
let subst''',metasenv''' =
C.Prod (n,s,type2),subst'''',metasenv''''
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let _,subst',metasenv' = type_of_aux subst metasenv context s in
+ let ty,subst',metasenv' = type_of_aux subst metasenv context s in
let inferredty,subst'',metasenv'' =
- type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
+ type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
in
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
(type_of_mutual_inductive_constr uri i j)
in
cty,subst',metasenv'
- | C.MutCase _
- | C.Fix _
- | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+ | 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 =
+ match CicEnvironment.get_cooked_obj ~trust:true uri with
+ C.InductiveDefinition (l,expl_params,parsno) ->
+ List.nth l i , expl_params, parsno
+ | _ ->
+ raise
+ (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+ let rec count_prod t =
+ match CicMetaSubst.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 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 context no_right_params in
+ let metasenv,exp_named_subst =
+ CicMkImplicit.fresh_subst metasenv 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 actual_type,subst,metasenv =
+ type_of_aux subst metasenv context term in
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context expected_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
+ (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+ let (_,outtypeinstances,subst,metasenv) =
+ List.fold_left
+ (fun (j,outtypeinstances,subst,metasenv) p ->
+ 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 actual_type,subst,metasenv =
+ type_of_aux subst metasenv context p in
+ let expected_type, subst, metasenv =
+ type_of_aux subst metasenv context constructor in
+ let outtypeinstance,subst,metasenv =
+ check_branch
+ 0 context metasenv subst
+ no_left_params actual_type constructor expected_type in
+ (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
+ (1,[],subst,metasenv) pl 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 *)
+ (* easy case *)
+ let _, subst, metasenv =
+ type_of_aux subst metasenv context
+ (C.Appl ((outtype :: right_args) @ [term]))
+ in
+ let (subst,metasenv) =
+ List.fold_left
+ (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+(*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv) =
+ type_of_aux subst metasenv context appl
+ in
+*)
+ CicMetaSubst.whd subst context appl
+ in
+ Un.fo_unif_subst subst context metasenv instance instance')
+ (subst,metasenv) outtypeinstances in
+ CicMetaSubst.whd subst
+ context (C.Appl(outtype::right_args@[term])),subst,metasenv
+ | C.Fix (i,fl) ->
+ let subst,metasenv,types =
+ List.fold_left
+ (fun (subst,metasenv,types) (n,_,ty,_) ->
+ let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+ ) (subst,metasenv,[]) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,x,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ Un.fo_unif_subst subst context' metasenv
+ 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) ->
+ let subst,metasenv,types =
+ List.fold_left
+ (fun (subst,metasenv,types) (n,ty,_) ->
+ let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+ subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+ ) (subst,metasenv,[]) fl
+ in
+ let len = List.length types in
+ let context' = types@context in
+ let subst,metasenv =
+ List.fold_left
+ (fun (subst,metasenv) (name,ty,bo) ->
+ let ty_of_bo,subst,metasenv =
+ type_of_aux subst metasenv context' bo
+ in
+ Un.fo_unif_subst subst context' metasenv
+ ty_of_bo (CicMetaSubst.lift subst len ty)
+ ) (subst,metasenv) fl in
+
+ let (_,ty,_) = List.nth fl i in
+ ty,subst,metasenv
(* 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.Decl t))::tl ->
(Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
- | (Some (n,C.Def t))::tl ->
- (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ | (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 (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
List.fold_left2
(fun (subst,metasenv) t ct ->
match (t,ct) with
- _,None -> subst,metasenv
- | Some t,Some (_,C.Def ct) ->
+ _,None ->
+ subst,metasenv
+ | 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
in
(try
- CicUnification.fo_unif_subst subst context metasenv inferredty ct
- with _ -> raise MetasenvInconsistency)
- | _, _ -> raise MetasenvInconsistency
+ CicUnification.fo_unif_subst
+ subst' context metasenv' inferredty 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"
+ (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' = CicUnification.unwind_subst metasenv subst in
- let t1' = CicUnification.apply_subst subst' t1 in
- let t2' = CicUnification.apply_subst subst' t2 in
- let t1'' = CicReduction.whd context t1' in
- let t2'' = CicReduction.whd ((Some (name,C.Decl s))::context) t2' 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 context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set) -> (* 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,subst,metasenv
| (C.Sort s1, C.Sort s2) ->
(*CSC manca la gestione degli universi!!! *)
- C.Sort C.Type,subst',metasenv'
- | (C.Meta _,_)
- | (_,C.Meta _) ->
- raise
- (Uncertain
- ("Two sorts were expected, found " ^ CicPp.ppterm t1'' ^ " and " ^
- CicPp.ppterm t2''))
+ 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 *)
+ 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
- ("Prod: sort1= "^ CicPp.ppterm t1'' ^ " ; sort2= "^ CicPp.ppterm t2''))
+ raise (NotRefinable (sprintf
+ "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 =
+ 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
- and eat_prods subst metasenv context hetype =
- function
- [] -> hetype,subst,metasenv
- | (hete, hety)::tl ->
- (match (CicReduction.whd context hetype) with
- Cic.Prod (n,s,t) ->
- let subst',metasenv' =
- try
- CicUnification.fo_unif_subst subst context metasenv s hety
- with _ ->
- raise (NotRefinable "Appl: wrong parameter-type")
- 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")
- )
in
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
in
- let subst'',metasenv'' = CicUnification.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''
+ 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
- CicUnification.apply_subst subst'' t,
- CicUnification.apply_subst subst'' ty,
- 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 *)
let type_of_aux' metasenv context term =
try
- let (t,ty,s,m) =
- type_of_aux' metasenv context term
- in
- List.iter
- (function (i,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
- List.iter
- (function (i,_,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
- prerr_endline
- ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
- (t,ty,s,m)
+ let (t,ty,m) = type_of_aux' metasenv context term in
+ debug_print
+ ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
+(*
+ debug_print
+ ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
+*)
+ (t,ty,m)
with
- e ->
- List.iter
- (function (i,_,t) ->
- prerr_endline ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
- metasenv ;
- prerr_endline ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
+ | CicUnification.AssertFailure msg as e ->
+ debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
+ debug_print msg;
+ raise e
+ | CicUnification.UnificationFailure msg as e ->
+ debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
+ debug_print msg;
+ raise e
+ | e ->
+ debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
raise e
;;
+
projects / helm.git / blobdiff