exception RelToHiddenHypothesis;;
exception WrongArgumentNumber;;
-let fdebug = ref 0;;
-let debug t context =
- let rec debug_aux t i =
- let module C = Cic in
- let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
- in
- if !fdebug = 0 then
- raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
- (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
-;;
-
let debug_print = prerr_endline
+let fo_unif_subst subst context metasenv t1 t2 =
+ try
+ CicUnification.fo_unif_subst subst context metasenv t1 t2
+ with
+ (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+ | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
let rec split l n =
match (l,n) with
(l,0) -> ([], l)
(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
+ 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])
_ -> raise (NotRefinable "Not a close term")
)
| C.Var (uri,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let ty =
CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
in
- decr fdebug ;
ty,subst',metasenv'
| C.Meta (n,l) ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
in
(try
let subst''',metasenv''' =
- Un.fo_unif_subst subst'' context metasenv'' inferredty ty
+ fo_unif_subst subst'' context metasenv'' inferredty ty
in
ty,subst''',metasenv'''
with
eat_prods subst'' metasenv'' context hetype tlbody_and_type
| C.Appl _ -> raise (NotRefinable "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let cty =
CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
in
- decr fdebug ;
cty,subst',metasenv'
| C.MutInd (uri,i,exp_named_subst) ->
- incr fdebug ;
let subst',metasenv' =
check_exp_named_subst subst metasenv context exp_named_subst in
let cty =
CicSubstitution.subst_vars exp_named_subst
(type_of_mutual_inductive_defs uri i)
in
- decr fdebug ;
cty,subst',metasenv'
| C.MutConstruct (uri,i,j,exp_named_subst) ->
let subst',metasenv' =
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
+ 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) =
*)
CicMetaSubst.whd subst context appl
in
- Un.fo_unif_subst subst context metasenv instance instance')
+ fo_unif_subst subst context metasenv instance instance')
(subst,metasenv) outtypeinstances in
CicMetaSubst.whd subst
context (C.Appl(outtype::right_args@[term])),subst,metasenv
let ty_of_bo,subst,metasenv =
type_of_aux subst metasenv context' bo
in
- Un.fo_unif_subst subst context' metasenv
+ 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
let ty_of_bo,subst,metasenv =
type_of_aux subst metasenv context' bo
in
- Un.fo_unif_subst subst context' metasenv
+ fo_unif_subst subst context' metasenv
ty_of_bo (CicMetaSubst.lift subst len ty)
) (subst,metasenv) fl in
subst,metasenv
| Some t,Some (_,C.Def (ct,_)) ->
(try
- CicUnification.fo_unif_subst subst context metasenv t ct
+ 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)))))
| Some t,Some (_,C.Decl ct) ->
let inferredty,subst',metasenv' =
type_of_aux subst metasenv context t
in
(try
- CicUnification.fo_unif_subst
+ 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 _ ->
in
try
let metasubst'',metasenv'' =
- CicUnification.fo_unif_subst
- metasubst' context metasenv' typeoft typeofvar
+ fo_unif_subst metasubst' context metasenv' typeoft typeofvar
in
check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
with _ ->
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''
+ fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
in
t2'',subst,metasenv
| (_,_) ->
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
+ fo_unif_subst subst context metasenv resty prod
in
aux context'' (Some arg :: args)
(CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
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