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 WrongArgumentNumber;;
+exception AssertFailure of string;;
let debug_print = prerr_endline
match (l,n) with
(l,0) -> ([], l)
| (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
- | (_,_) -> raise ListTooShort
+ | (_,_) -> raise (AssertFailure "split: list too short")
;;
let rec type_of_constant uri =
match CicEnvironment.get_cooked_obj uri with
C.Constant (_,_,ty,_) -> ty
| C.CurrentProof (_,_,_,ty,_) -> ty
- | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri))
and type_of_variable uri =
let module C = Cic in
let module U = UriManager in
match CicEnvironment.get_cooked_obj uri with
C.Variable (_,_,ty,_) -> ty
- | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown variable definition " ^ UriManager.string_of_uri uri))
and type_of_mutual_inductive_defs uri i =
let module C = Cic in
C.InductiveDefinition (dl,_,_) ->
let (_,_,arity,_) = List.nth dl i in
arity
- | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
and type_of_mutual_inductive_constr uri i j =
let module C = Cic in
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty
- | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
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
(* 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")
+ | _ -> raise (AssertFailure "Wrong number of arguments"))
+ | _ -> raise (AssertFailure "Prod or MutInd expected")
and type_of_aux' metasenv context t =
let rec type_of_aux subst metasenv context =
let module C = Cic in
let module S = CicSubstitution in
let module U = UriManager in
- let module Un = CicUnification in
function
C.Rel n ->
(try
| 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
+ | None -> raise (RefineFailure "Rel to hidden hypothesis")
with
- _ -> raise (NotRefinable "Not a close term")
+ _ -> raise (RefineFailure "Not a close term")
)
| C.Var (uri,exp_named_subst) ->
let subst',metasenv' =
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)
+ (* TASSI: CONSTRAINT *)
+ | C.Sort (C.Type t) ->
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_gt t' t ) then
+ assert false (* t' is fresh! an error in CicUniv *)
+ else
+ C.Sort (C.Type t'),subst,metasenv
+ (* TASSI: CONSTRAINT *)
+ | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
+ | C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) ->
let _,subst',metasenv' =
type_of_aux subst metasenv context ty in
in
ty,subst''',metasenv'''
with
- _ -> raise (NotRefinable "Cast"))
+ _ -> raise (RefineFailure "Cast"))
| C.Prod (name,s,t) ->
let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
let sort2,subst'',metasenv'' =
C.Meta _
| C.Sort _ -> ()
| _ ->
- raise (NotRefinable (sprintf
+ raise (RefineFailure (sprintf
"Not well-typed lambda-abstraction: the source %s should be a type;
instead it is a term of type %s" (CicPp.ppterm s)
(CicPp.ppterm sort1)))
) tl ([],subst',metasenv')
in
eat_prods subst'' metasenv'' context hetype tlbody_and_type
- | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
+ | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
List.nth l i , expl_params, parsno
| _ ->
raise
- (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+ (RefineFailure
+ ("Unkown mutual inductive definition " ^ 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)
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
in
aux 1 canonical_context
in
+ try
List.fold_left2
(fun (subst,metasenv) t ct ->
match (t,ct) with
| Some t,Some (_,C.Def (ct,_)) ->
(try
fo_unif_subst subst context metasenv t 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)))))
+ with e -> raise (RefineFailure (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 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
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)))))
+ with e -> raise (RefineFailure (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 AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
| None, Some _ ->
- raise (NotRefinable (sprintf
+ raise (RefineFailure (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
+ with
+ Invalid_argument _ ->
+ raise
+ (RefineFailure
+ (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 subst (Cic.Meta (metano, l)))
+ (CicMetaSubst.ppcontext subst canonical_context)))
and check_exp_named_subst metasubst metasenv context =
let rec check_exp_named_subst_aux metasubst metasenv substs =
(match CicEnvironment.get_cooked_obj ~trust:false uri with
Cic.Variable (_,Some bo,_,_) ->
raise
- (NotRefinable
+ (RefineFailure
"A variable with a body can not be explicit substituted")
| Cic.Variable (_,None,_,_) -> ()
- | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+ | _ ->
+ raise
+ (RefineFailure
+ ("Unkown variable definition " ^ UriManager.string_of_uri uri))
) ;
let typeoft,metasubst',metasenv' =
type_of_aux metasubst metasenv context t
in
check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
with _ ->
- raise (NotRefinable "Wrong Explicit Named Substitution")
+ raise (RefineFailure "Wrong Explicit Named Substitution")
in
check_exp_named_subst_aux metasubst metasenv []
(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,subst,metasenv
- | (C.Sort s1, C.Sort s2) ->
- (*CSC manca la gestione degli universi!!! *)
- C.Sort C.Type,subst,metasenv
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+ let t' = CicUniv.fresh() in
+ if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+ assert false ; (* not possible, error in CicUniv *)
+ C.Sort (C.Type t'),subst,metasenv
+ | (C.Sort _,C.Sort (C.Type t1)) ->
+ (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+ C.Sort (C.Type t1),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
in
t2'',subst,metasenv
| (_,_) ->
- raise (NotRefinable (sprintf
+ raise (RefineFailure (sprintf
"Two sorts 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'')))
in
let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
let (subst, metasenv) =
- CicUnification.fo_unif_subst subst context metasenv hetype hetype'
+ fo_unif_subst subst context metasenv hetype hetype'
in
let rec eat_prods metasenv subst context hetype =
function
| (hete, hety)::tl ->
(match hetype with
Cic.Prod (n,s,t) ->
- (try
let subst,metasenv =
- CicUnification.fo_unif_subst subst context metasenv s hety
+ fo_unif_subst subst context metasenv hety s
in
eat_prods metasenv subst context
(CicMetaSubst.subst subst hete t) tl
- with
- e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e)))
| _ -> assert false
)
in
eat_prods metasenv subst context hetype' tlbody_and_type
in
t,subst,metasenv
-
(*
let rec aux context' args (resty,subst,metasenv) =
function
in
aux [] [] (hetype,subst,metasenv) tlbody_and_type
*)
-
in
let ty,subst',metasenv' =
type_of_aux [] metasenv context t
*)
(t,ty,m)
with
- | CicUnification.AssertFailure msg as e ->
- debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
- debug_print msg;
+ | RefineFailure msg as e ->
+ debug_print ("@@@ REFINE FAILED: " ^ msg);
+ raise e
+ | Uncertain msg as e ->
+ debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
raise e
- | e ->
- debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
- raise e
;;
-
projects / helm.git / blobdiff