X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=338928e8d9fc723edcd188c9d43da186b424a141;hpb=d46d2dfe4aecc2fa820311753003567d57b19d31;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 338928e8d..d3a297d43 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,76 +25,235 @@ open Printf -exception RefineFailure of string;; +exception RefineFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; -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;; +let debug_print = fun _ -> () -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 profiler = HExtlib.profile "CicRefine.fo_unif" -let debug_print = prerr_endline +let fo_unif_subst subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; +let enrich f = + function + RefineFailure msg -> raise (RefineFailure (f msg)) + | Uncertain msg -> raise (Uncertain (f msg)) + | _ -> assert false + 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 + | (_,_) -> raise (AssertFailure (lazy "split: list too short")) ;; -let rec type_of_constant uri = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - match CicEnvironment.get_cooked_obj uri with - C.Constant (_,_,ty,_) -> ty - | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) +let exp_impl metasenv subst context term = + let rec aux metasenv context = function + | (Cic.Rel _) as t -> metasenv, t + | (Cic.Sort _) as t -> metasenv, t + | Cic.Const (uri, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.Const (uri, subst') + | Cic.Var (uri, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.Var (uri, subst') + | Cic.MutInd (uri, i, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.MutInd (uri, i, subst') + | Cic.MutConstruct (uri, i, j, subst) -> + let metasenv', subst' = do_subst metasenv context subst in + metasenv', Cic.MutConstruct (uri, i, j, subst') + | Cic.Meta (n,l) -> + let metasenv', l' = do_local_context metasenv context l in + metasenv', Cic.Meta (n, l') + | Cic.Implicit (Some `Type) -> + let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) + | Cic.Implicit (Some `Closed) -> + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) + | Cic.Implicit None -> + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + metasenv', Cic.Meta (idx, irl) + | Cic.Implicit _ -> assert false + | Cic.Cast (te, ty) -> + let metasenv', ty' = aux metasenv context ty in + let metasenv'', te' = aux metasenv' context te in + metasenv'', Cic.Cast (te', ty') + | Cic.Prod (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.Prod (name, s', t) + | Cic.Lambda (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.Lambda (name, s', t) + | Cic.LetIn (name, s, t) -> + let metasenv', s' = aux metasenv context s in + metasenv', Cic.LetIn (name, s', t) + | Cic.Appl l when List.length l > 1 -> + let metasenv', l' = + List.fold_right + (fun term (metasenv, terms) -> + let new_metasenv, term = aux metasenv context term in + new_metasenv, term :: terms) + l (metasenv, []) + in + metasenv', Cic.Appl l' + | Cic.Appl _ -> assert false + | Cic.MutCase (uri, i, outtype, term, patterns) -> + let metasenv', l' = + List.fold_right + (fun term (metasenv, terms) -> + let new_metasenv, term = aux metasenv context term in + new_metasenv, term :: terms) + (outtype :: term :: patterns) (metasenv, []) + in + let outtype', term', patterns' = + match l' with + | outtype' :: term' :: patterns' -> outtype', term', patterns' + | _ -> assert false + in + metasenv', Cic.MutCase (uri, i, outtype', term', patterns') + | Cic.Fix (i, funs) -> + let metasenv', types = + List.fold_right + (fun (name, _, typ, _) (metasenv, types) -> + let new_metasenv, new_type = aux metasenv context typ in + (new_metasenv, (name, new_type) :: types)) + funs (metasenv, []) + in + let rec combine = function + | ((name, index, _, body) :: funs_tl), + ((_, typ) :: typ_tl) -> + (name, index, typ, body) :: combine (funs_tl, typ_tl) + | [], [] -> [] + | _ -> assert false + in + let funs' = combine (funs, types) in + metasenv', Cic.Fix (i, funs') + | Cic.CoFix (i, funs) -> + let metasenv', types = + List.fold_right + (fun (name, typ, _) (metasenv, types) -> + let new_metasenv, new_type = aux metasenv context typ in + (new_metasenv, (name, new_type) :: types)) + funs (metasenv, []) + in + let rec combine = function + | ((name, _, body) :: funs_tl), + ((_, typ) :: typ_tl) -> + (name, typ, body) :: combine (funs_tl, typ_tl) + | [], [] -> [] + | _ -> assert false + in + let funs' = combine (funs, types) in + metasenv', Cic.CoFix (i, funs') + and do_subst metasenv context subst = + List.fold_right + (fun (uri, term) (metasenv, substs) -> + let metasenv', term' = aux metasenv context term in + (metasenv', (uri, term') :: substs)) + subst (metasenv, []) + and do_local_context metasenv context local_context = + List.fold_right + (fun term (metasenv, local_context) -> + let metasenv', term' = + match term with + | None -> metasenv, None + | Some term -> + let metasenv', term' = aux metasenv context term in + metasenv', Some term' + in + metasenv', term' :: local_context) + local_context (metasenv, []) + in + aux metasenv context term +;; -and type_of_variable uri = +let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.get_cooked_obj uri with - C.Variable (_,_,ty,_) -> ty - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + let _ = CicTypeChecker.typecheck uri in + let obj,u = + try + CicEnvironment.get_cooked_obj ugraph uri + with Not_found -> assert false + in + match obj with + C.Constant (_,_,ty,_,_) -> ty,u + | C.CurrentProof (_,_,_,ty,_,_) -> ty,u + | _ -> + raise + (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) -and type_of_mutual_inductive_defs uri i = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - match CicEnvironment.get_cooked_obj uri with - C.InductiveDefinition (dl,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) +and type_of_variable uri ugraph = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let _ = CicTypeChecker.typecheck uri in + let obj,u = + try + CicEnvironment.get_cooked_obj ugraph uri + with Not_found -> assert false + in + match obj with + C.Variable (_,_,ty,_,_) -> ty,u + | _ -> + raise + (RefineFailure + (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri))) + +and type_of_mutual_inductive_defs uri i ugraph = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let _ = CicTypeChecker.typecheck uri in + let obj,u = + try + CicEnvironment.get_cooked_obj ugraph uri + with Not_found -> assert false + in + match obj with + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity,u + | _ -> + raise + (RefineFailure + (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri))) + +and type_of_mutual_inductive_constr uri i j ugraph = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let _ = CicTypeChecker.typecheck uri in + let obj,u = + try + CicEnvironment.get_cooked_obj ugraph uri + with Not_found -> assert false + in + match obj with + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in + let (_,ty) = List.nth cl (j-1) in + ty,u + | _ -> + raise + (RefineFailure + (lazy + ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) -and type_of_mutual_inductive_constr uri i j = - let module C = Cic in - let module R = CicReduction in - let module U = UriManager in - match CicEnvironment.get_cooked_obj uri with - C.InductiveDefinition (dl,_,_) -> - let (_,_,_,cl) = List.nth dl i in - let (_,ty) = List.nth cl (j-1) in - ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -106,508 +265,1107 @@ and type_of_mutual_inductive_constr uri i j = 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 = +and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph = 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") + (* let module R = CicMetaSubst in *) + let module R = CicReduction in + match R.whd ~subst context expectedtype with + C.MutInd (_,_,_) -> + (n,context,actualtype, [term]), subst, metasenv, ugraph + | C.Appl (C.MutInd (_,_,_)::tl) -> + let (_,arguments) = split tl left_args_no in + (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph + | 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, ugraph1 = + fo_unif_subst subst context metasenv so so' ugraph 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 ugraph1 + | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) + | _ -> raise (AssertFailure (lazy "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 - match List.nth context (n - 1) with - Some (_,C.Decl t) -> S.lift n t,subst,metasenv - | 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 - _ -> 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 - 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) - | 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 te - in - (try - let subst''',metasenv''' = - Un.fo_unif_subst subst'' context metasenv'' inferredty ty - in - ty,subst''',metasenv''' - with - _ -> raise (NotRefinable "Cast")) - | C.Prod (name,s,t) -> - let sort1,subst',metasenv' = type_of_aux subst metasenv context s in - 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) - | 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) t - in - let sort2,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'''' = - sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2) - in - 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 - let inferredty,subst'',metasenv'' = - 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. *) - CicSubstitution.subst s inferredty,subst',metasenv' - | C.Appl (he::tl) when List.length tl > 0 -> - let hetype,subst',metasenv' = type_of_aux subst metasenv context he in - let tlbody_and_type,subst'',metasenv'' = - List.fold_right - (fun x (res,subst,metasenv) -> - let ty,subst',metasenv' = - type_of_aux subst metasenv context x - in - (x, ty)::res,subst',metasenv' - ) tl ([],subst',metasenv') - in - 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' = - check_exp_named_subst subst metasenv context exp_named_subst in - let cty = - CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_constr uri i j) - in - cty,subst',metasenv' - | 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 +and type_of_aux' metasenv context t ugraph = + let metasenv, t = exp_impl metasenv [] context t in + let rec type_of_aux subst metasenv context t ugraph = + let module C = Cic in + let module S = CicSubstitution in + let module U = UriManager in + (* this stops on binders, so we have to call it every time *) + match t with + (* function *) + C.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Decl ty) -> + t,S.lift n ty,subst,metasenv, ugraph + | Some (_,C.Def (_,Some ty)) -> + t,S.lift n ty,subst,metasenv, ugraph + | Some (_,C.Def (bo,None)) -> + let ty,ugraph = + (* if it is in the context it must be already well-typed*) + CicTypeChecker.type_of_aux' ~subst metasenv context + (S.lift n bo) ugraph + in + t,ty,subst,metasenv,ugraph + | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) + with + _ -> raise (RefineFailure (lazy "Not a close term"))) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst + subst metasenv context exp_named_subst ugraph + in + let ty_uri,ugraph1 = type_of_variable uri ugraph in + let ty = + CicSubstitution.subst_vars exp_named_subst' ty_uri + in + C.Var (uri,exp_named_subst'),ty,subst',metasenv',ugraph1 + | C.Meta (n,l) -> + (try + let (canonical_context, term,ty) = + CicUtil.lookup_subst n subst + in + let l',subst',metasenv',ugraph1 = + check_metasenv_consistency n subst metasenv context + canonical_context l ugraph + in + (* trust or check ??? *) + C.Meta (n,l'),CicSubstitution.subst_meta l' ty, + subst', metasenv', ugraph1 + (* type_of_aux subst metasenv + context (CicSubstitution.subst_meta l term) *) + with CicUtil.Subst_not_found _ -> + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in + let l',subst',metasenv', ugraph1 = + check_metasenv_consistency n subst metasenv context + canonical_context l ugraph + in + C.Meta (n,l'),CicSubstitution.subst_meta l' ty, + subst', metasenv',ugraph1) + | C.Sort (C.Type tno) -> + let tno' = CicUniv.fresh() in + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + | C.Sort _ -> + t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph + | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | C.Cast (te,ty) -> + let ty',_,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context ty ugraph + in + let te',inferredty,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' context te ugraph1 + in + let subst''',metasenv''',ugraph3 = + fo_unif_subst subst'' context metasenv'' + inferredty ty' ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + | C.Prod (name,s,t) -> + let carr t subst context = CicMetaSubst.apply_subst subst t in + let coerce_to_sort + in_source tgt_sort t type_to_coerce subst ctx metasenv uragph + = + let coercion_src = carr type_to_coerce subst ctx in + match coercion_src with + | Cic.Sort _ -> + t,type_to_coerce,subst,metasenv,ugraph (* - (* 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 + | Cic.Meta _ as meta when not in_source -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let subst, metasenv, ugraph = + fo_unif_subst + subst ctx metasenv meta coercion_tgt ugraph + in + t, Cic.Sort tgt_sort, subst, metasenv, ugraph *) - CicMetaSubst.whd subst context appl + | Cic.Meta _ as meta -> + t, meta, subst, metasenv, ugraph + | Cic.Cast _ as cast -> + t, cast, subst, metasenv, ugraph + | term -> + let coercion_tgt = carr (Cic.Sort tgt_sort) subst ctx in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + (match boh with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + raise + (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) + | CoercGraph.NotMetaClosed -> + raise + (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) + | CoercGraph.SomeCoercion c -> + Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) + in + let s',sort1,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph + in + let s',sort1,subst', metasenv',ugraph1 = + coerce_to_sort true (Cic.Type(CicUniv.fresh())) + s' sort1 subst' context metasenv' ugraph1 + in + let context_for_t = ((Some (name,(C.Decl s')))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t in + let t',sort2,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' + context_for_t t ugraph1 + in + let t',sort2,subst'',metasenv'',ugraph2 = + coerce_to_sort false (Cic.Type(CicUniv.fresh())) + t' sort2 subst'' context_for_t metasenv'' ugraph2 + in + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod subst'' metasenv'' + context (name,s') (sort1,sort2) ugraph2 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 + C.Prod (name,s',t'),sop,subst''',metasenv''',ugraph3 + | C.Lambda (n,s,t) -> + + let s',sort1,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph in + let s',sort1 = + match CicReduction.whd ~subst:subst' context sort1 with + C.Meta _ + | C.Sort _ -> s',sort1 + | coercion_src -> + let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in + let search = CoercGraph.look_for_coercion in + let boh = search coercion_src coercion_tgt in + match boh with + | CoercGraph.SomeCoercion c -> + Cic.Appl [c;s'], coercion_tgt + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ + | CoercGraph.NotMetaClosed -> + raise (RefineFailure (lazy (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)))) + in + let context_for_t = ((Some (n,(C.Decl s')))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t in + let t',type2,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' context_for_t t ugraph1 + in + C.Lambda (n,s',t'),C.Prod (n,s',type2), + subst'',metasenv'',ugraph2 + | C.LetIn (n,s,t) -> + (* only to check if s is well-typed *) + let s',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph + in + let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in + let metasenv',t = exp_impl metasenv' subst' context_for_t t in + + let t',inferredty,subst'',metasenv'',ugraph2 = + type_of_aux subst' metasenv' + context_for_t t ugraph1 + in + (* One-step LetIn reduction. + * Even faster than the previous solution. + * Moreover the inferred type is closer to the expected one. + *) + C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty, + subst'',metasenv'',ugraph2 + | C.Appl (he::((_::_) as tl)) -> + let he',hetype,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context he ugraph + in + let tlbody_and_type,subst'',metasenv'',ugraph2 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) tl ([],subst',metasenv',ugraph1) + in + let tl',applty,subst''',metasenv''',ugraph3 = + try + eat_prods true subst'' metasenv'' context + hetype tlbody_and_type ugraph2 + with + exn -> + enrich + (fun msg -> + lazy ("The application " ^ + CicMetaSubst.ppterm_in_context subst'' t context ^ + " is not well typed:\n" ^ Lazy.force msg)) exn + in + C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 + | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph in + let ty_uri,ugraph2 = type_of_constant uri ugraph1 in + let cty = + CicSubstitution.subst_vars exp_named_subst' ty_uri + in + C.Const (uri,exp_named_subst'),cty,subst',metasenv',ugraph2 + | C.MutInd (uri,i,exp_named_subst) -> + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph + in + let ty_uri,ugraph2 = type_of_mutual_inductive_defs uri i ugraph1 in + let cty = + CicSubstitution.subst_vars exp_named_subst' ty_uri in + C.MutInd (uri,i,exp_named_subst'),cty,subst',metasenv',ugraph2 + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let exp_named_subst',subst',metasenv',ugraph1 = + check_exp_named_subst subst metasenv context + exp_named_subst ugraph + in + let ty_uri,ugraph2 = + type_of_mutual_inductive_constr uri i j ugraph1 + in + let cty = + CicSubstitution.subst_vars exp_named_subst' ty_uri + in + C.MutConstruct (uri,i,j,exp_named_subst'),cty,subst', + metasenv',ugraph2 + | 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,ugraph = + let _ = CicTypeChecker.typecheck uri in + let obj,u = CicEnvironment.get_cooked_obj ugraph uri in + match obj with + C.InductiveDefinition (l,expl_params,parsno,_) -> + List.nth l i , expl_params, parsno, u + | _ -> + raise + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ + U.string_of_uri uri))) 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 + let rec count_prod t = + match CicReduction.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 subst 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 subst context no_right_params + in + let metasenv,exp_named_subst = + CicMkImplicit.fresh_subst metasenv subst 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 term',actual_type,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context term ugraph in + let expected_type',_, subst, metasenv,ugraph2 = + type_of_aux subst metasenv context expected_type ugraph1 + in + let actual_type = CicReduction.whd ~subst context actual_type in + let subst,metasenv,ugraph3 = + fo_unif_subst subst context metasenv + expected_type' actual_type ugraph2 + in + let rec instantiate_prod t = + function + [] -> t + | he::tl -> + match CicReduction.whd ~subst context t with + C.Prod (_,_,t') -> + instantiate_prod (CicSubstitution.subst he t') tl + | _ -> assert false + in + let arity_instantiated_with_left_args = + instantiate_prod arity left_args in + (* TODO: check if the sort elimination + * is allowed: [(I q1 ... qr)|B] *) + let (pl',_,outtypeinstances,subst,metasenv,ugraph4) = + List.fold_left + (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) 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 p',actual_type,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context p ugraph + in + let constructor',expected_type, subst, metasenv,ugraph2 = + type_of_aux subst metasenv context constructor ugraph1 + in + let outtypeinstance,subst,metasenv,ugraph3 = + check_branch 0 context metasenv subst no_left_params + actual_type constructor' expected_type ugraph2 + in + (pl @ [p'],j+1, + outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) + ([],1,[],subst,metasenv,ugraph3) pl 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 + + (* 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 + *) + + (match outtype with + | C.Meta (n,l) -> + (let candidate,ugraph5,metasenv,subst = + let exp_name_subst, metasenv = + let o,_ = + CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + in + let uris = CicUtil.params_of_obj o in + List.fold_right ( + fun uri (acc,metasenv) -> + let metasenv',new_meta = + CicMkImplicit.mk_implicit metasenv subst context + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable + context + in + (uri, Cic.Meta(new_meta,irl))::acc, metasenv' + ) uris ([],metasenv) + in + let ty = + match left_args,right_args with + [],[] -> Cic.MutInd(uri, i, exp_name_subst) + | _,_ -> + let rec mk_right_args = + function + 0 -> [] + | n -> (Cic.Rel n)::(mk_right_args (n - 1)) + in + let right_args_no = List.length right_args in + let lifted_left_args = + List.map (CicSubstitution.lift right_args_no) left_args + in + Cic.Appl (Cic.MutInd(uri,i,exp_name_subst):: + (lifted_left_args @ mk_right_args right_args_no)) + in + let fresh_name = + FreshNamesGenerator.mk_fresh_name ~subst metasenv + context Cic.Anonymous ~typ:ty + in + match outtypeinstances with + | [] -> + let extended_context = + let rec add_right_args = + function + Cic.Prod (name,ty,t) -> + Some (name,Cic.Decl ty)::(add_right_args t) + | _ -> [] + in + (Some (fresh_name,Cic.Decl ty)):: + (List.rev + (add_right_args arity_instantiated_with_left_args))@ + context + in + let metasenv,new_meta = + CicMkImplicit.mk_implicit metasenv subst extended_context + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable + extended_context + in + let rec add_lambdas b = + function + Cic.Prod (name,ty,t) -> + Cic.Lambda (name,ty,(add_lambdas b t)) + | _ -> Cic.Lambda (fresh_name, ty, b) + in + let candidate = + add_lambdas (Cic.Meta (new_meta,irl)) + arity_instantiated_with_left_args + in + (Some candidate),ugraph4,metasenv,subst + | (constructor_args_no,_,instance,_)::tl -> + try + let instance',subst,metasenv = + CicMetaSubst.delift_rels subst metasenv + constructor_args_no instance + in + let candidate,ugraph,metasenv,subst = + List.fold_left ( + fun (candidate_oty,ugraph,metasenv,subst) + (constructor_args_no,_,instance,_) -> + match candidate_oty with + | None -> None,ugraph,metasenv,subst + | Some ty -> + try + let instance',subst,metasenv = + CicMetaSubst.delift_rels subst metasenv + constructor_args_no instance + in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv + instance' ty ugraph + in + candidate_oty,ugraph,metasenv,subst + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> + None,ugraph,metasenv,subst + ) (Some instance',ugraph4,metasenv,subst) tl + in + match candidate with + | None -> None, ugraph,metasenv,subst + | Some t -> + let rec add_lambdas n b = + function + Cic.Prod (name,ty,t) -> + Cic.Lambda (name,ty,(add_lambdas (n + 1) b t)) + | _ -> + Cic.Lambda (fresh_name, ty, + CicSubstitution.lift (n + 1) t) + in + Some + (add_lambdas 0 t arity_instantiated_with_left_args), + ugraph,metasenv,subst + with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + None,ugraph4,metasenv,subst + in + match candidate with + | None -> raise (Uncertain (lazy "can't solve an higher order unification problem")) + | Some candidate -> + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv + candidate outtype ugraph5 + in + C.MutCase (uri, i, outtype, term', pl'), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (Cic.Appl (outtype::right_args@[term']))), + subst,metasenv,ugraph) + | _ -> (* easy case *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 + in + let tlbody_and_type,subst,metasenv,ugraph4 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + in + let _,_,subst,metasenv,ugraph4 = + eat_prods false subst metasenv context + outtypety tlbody_and_type ugraph4 + in + let _,_, subst, metasenv,ugraph5 = + type_of_aux subst metasenv context + (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 + in + let (subst,metasenv,ugraph6) = + List.fold_left + (fun (subst,metasenv,ugraph) + (constructor_args_no,context,instance,args) -> + let instance' = + let appl = + let outtype' = + CicSubstitution.lift constructor_args_no outtype + in + C.Appl (outtype'::args) + in + CicReduction.whd ~subst context appl + in + fo_unif_subst subst context metasenv + instance instance' ugraph) + (subst,metasenv,ugraph5) outtypeinstances + in + C.MutCase (uri, i, outtype, term', pl'), + CicReduction.head_beta_reduce + (CicMetaSubst.apply_subst subst + (C.Appl(outtype::right_args@[term]))), + subst,metasenv,ugraph6) + | C.Fix (i,fl) -> + let fl_ty',subst,metasenv,types,ugraph1 = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph) (n,_,ty,_) -> + let ty',_,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context ty ugraph + in + fl @ [ty'],subst',metasenv', + Some (C.Name n,(C.Decl ty')) :: types, ugraph + ) ([],subst,metasenv,[],ugraph) fl + in + let len = List.length types in + let context' = types@context in + let fl_bo',subst,metasenv,ugraph2 = + List.fold_left + (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) -> + let metasenv, bo = exp_impl metasenv subst context' bo in + let bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph + in + let subst',metasenv',ugraph' = + fo_unif_subst subst context' metasenv + ty_of_bo (CicSubstitution.lift len ty) ugraph1 + in + fl @ [bo'] , subst',metasenv',ugraph' + ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') + in + let ty = List.nth fl_ty' i in + (* now we have the new ty in fl_ty', the new bo in fl_bo', + * and we want the new fl with bo' and ty' injected in the right + * place. + *) + let rec map3 f l1 l2 l3 = + match l1,l2,l3 with + | [],[],[] -> [] + | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) + | _ -> assert false + in + let fl'' = map3 (fun ty' bo' (name,x,ty,bo) -> (name,x,ty',bo') ) + fl_ty' fl_bo' fl + in + C.Fix (i,fl''),ty,subst,metasenv,ugraph2 + | C.CoFix (i,fl) -> + let fl_ty',subst,metasenv,types,ugraph1 = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph) (n,ty,_) -> + let ty',_,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context ty ugraph + in + fl @ [ty'],subst',metasenv', + Some (C.Name n,(C.Decl ty')) :: types, ugraph1 + ) ([],subst,metasenv,[],ugraph) fl + in + let len = List.length types in + let context' = types@context in + let fl_bo',subst,metasenv,ugraph2 = + List.fold_left + (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> + let metasenv, bo = exp_impl metasenv subst context' bo in + let bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph + in + let subst',metasenv',ugraph' = + fo_unif_subst subst context' metasenv + ty_of_bo (CicSubstitution.lift len ty) ugraph1 + in + fl @ [bo'],subst',metasenv',ugraph' + ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') + in + let ty = List.nth fl_ty' i in + (* now we have the new ty in fl_ty', the new bo in fl_bo', + * and we want the new fl with bo' and ty' injected in the right + * place. + *) + let rec map3 f l1 l2 l3 = + match l1,l2,l3 with + | [],[],[] -> [] + | h1::tl1,h2::tl2,h3::tl3 -> (f h1 h2 h3) :: (map3 f tl1 tl2 tl3) + | _ -> assert false + in + let fl'' = map3 (fun ty' bo' (name,ty,bo) -> (name,ty',bo') ) + fl_ty' fl_bo' fl + in + C.CoFix (i,fl''),ty,subst,metasenv,ugraph2 - (* 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 - metano subst metasenv context canonical_context l - = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution 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 + metano subst metasenv context canonical_context l ugraph + = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in let lifted_canonical_context = - let rec aux i = + let rec aux i = + function + [] -> [] + | (Some (n,C.Decl t))::tl -> + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) + | (Some (n,C.Def (t,None)))::tl -> + (Some (n,C.Def ((S.subst_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.subst_meta l (S.lift i t)), + Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) + in + aux 1 canonical_context + in + try + List.fold_left2 + (fun (l,subst,metasenv,ugraph) t ct -> + match (t,ct) with + _,None -> + l @ [None],subst,metasenv,ugraph + | Some t,Some (_,C.Def (ct,_)) -> + let subst',metasenv',ugraph' = + (try + fo_unif_subst subst context metasenv t ct ugraph + with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + in + l @ [Some t],subst',metasenv',ugraph' + | Some t,Some (_,C.Decl ct) -> + let t',inferredty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context t ugraph + in + let subst'',metasenv'',ugraph2 = + (try + fo_unif_subst + subst' context metasenv' inferredty ct ugraph1 + with e -> raise (RefineFailure (lazy (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 -> Lazy.force msg | RefineFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) + in + l @ [Some t'], subst'',metasenv'',ugraph2 + | None, Some _ -> + raise (RefineFailure (lazy (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,ugraph) l lifted_canonical_context + with + Invalid_argument _ -> + raise + (RefineFailure + (lazy (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 tl ugraph = + let rec check_exp_named_subst_aux metasubst metasenv substs tl ugraph = + match tl with + [] -> [],metasubst,metasenv,ugraph + | ((uri,t) as subst)::tl -> + let ty_uri,ugraph1 = type_of_variable uri ugraph in + let typeofvar = + CicSubstitution.subst_vars substs ty_uri in + (* CSC: why was this code here? it is wrong + (match CicEnvironment.get_cooked_obj ~trust:false uri with + Cic.Variable (_,Some bo,_,_) -> + raise + (RefineFailure (lazy + "A variable with a body can not be explicit substituted")) + | Cic.Variable (_,None,_,_) -> () + | _ -> + raise + (RefineFailure (lazy + ("Unkown variable definition " ^ UriManager.string_of_uri uri))) + ) ; + *) + let t',typeoft,metasubst',metasenv',ugraph2 = + type_of_aux metasubst metasenv context t ugraph1 + in + let metasubst'',metasenv'',ugraph3 = + try + fo_unif_subst + metasubst' context metasenv' typeoft typeofvar ugraph2 + with _ -> + raise (RefineFailure (lazy + ("Wrong Explicit Named Substitution: " ^ + CicMetaSubst.ppterm metasubst' typeoft ^ + " not unifiable with " ^ + CicMetaSubst.ppterm metasubst' typeofvar))) + in + (* FIXME: no mere tail recursive! *) + let exp_name_subst, metasubst''', metasenv''', ugraph4 = + check_exp_named_subst_aux + metasubst'' metasenv'' (substs@[subst]) tl ugraph3 + in + ((uri,t')::exp_name_subst), metasubst''', metasenv''', ugraph4 + in + check_exp_named_subst_aux metasubst metasenv [] tl ugraph + + + and sort_of_prod subst metasenv context (name,s) (t1, t2) ugraph = + let module C = Cic in + let context_for_t2 = (Some (name,C.Decl s))::context in + let t1'' = CicReduction.whd ~subst context t1 in + let t2'' = CicReduction.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 s2,subst,metasenv,ugraph + | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),subst,metasenv,ugraph2 + | (C.Sort _,C.Sort (C.Type t1)) -> + C.Sort (C.Type t1),subst,metasenv,ugraph + | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph + | (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 subst in + let (subst, metasenv,ugraph1) = + fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' ugraph + in + t2'',subst,metasenv,ugraph1 + | _,_ -> + raise + (RefineFailure + (lazy + (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'')))) + + and eat_prods + allow_coercions subst metasenv context hetype tlbody_and_type ugraph + = + let rec mk_prod metasenv context = function - [] -> [] - | (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,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 + [] -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + metasenv,Cic.Meta (idx, irl) + | (_,argty)::tl -> + let (metasenv, idx) = + CicMkImplicit.mk_implicit_type metasenv subst context + in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let meta = Cic.Meta (idx,irl) in + let name = + (* The name must be fresh for 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 = + (* Cic.Name "pippo" *) + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) + in + (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) + FreshNamesGenerator.mk_fresh_name ~subst + [] context name_hint ~typ:(Cic.Sort Cic.Prop) + in + let metasenv,target = + mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl + in + metasenv,Cic.Prod (name,meta,target) in - List.fold_left2 - (fun (subst,metasenv) t ct -> - match (t,ct) with - _,None -> - subst,metasenv - | Some t,Some (_,C.Def (ct,_)) -> - (try - CicUnification.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 - 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 + let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in + let (subst, metasenv,ugraph1) = + try + fo_unif_subst subst context metasenv hetype hetype' ugraph + with exn -> + debug_print (lazy (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s" + (CicPp.ppterm hetype) + (CicPp.ppterm hetype') + (CicMetaSubst.ppmetasenv [] metasenv) + (CicMetaSubst.ppsubst subst))); + raise exn - and check_exp_named_subst metasubst metasenv context = - let rec check_exp_named_subst_aux metasubst metasenv substs = - function - [] -> metasubst,metasenv - | ((uri,t) as subst)::tl -> - let typeofvar = - CicSubstitution.subst_vars substs (type_of_variable uri) in - (match CicEnvironment.get_cooked_obj ~trust:false uri with - Cic.Variable (_,Some bo,_,_) -> - raise - (NotRefinable - "A variable with a body can not be explicit substituted") - | Cic.Variable (_,None,_,_) -> () - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) - ) ; - let typeoft,metasubst',metasenv' = - type_of_aux metasubst metasenv context t - in - try - let metasubst'',metasenv'' = - CicUnification.fo_unif_subst - metasubst' context metasenv' typeoft typeofvar + in + let rec eat_prods metasenv subst context hetype ugraph = + function + | [] -> [],metasenv,subst,hetype,ugraph + | (hete, hety)::tl -> + (match hetype with + Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph1 = + try + let subst,metasenv,ugraph1 = + fo_unif_subst subst context metasenv hety s ugraph + in + hete,subst,metasenv,ugraph1 + with exn when allow_coercions -> + (* we search a coercion from hety to s *) + let coer = + let carr t subst context = + CicMetaSubst.apply_subst subst t + in + let c_hety = carr hety subst context in + let c_s = carr s subst context in + CoercGraph.look_for_coercion c_hety c_s + in + match coer with + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ -> + let msg e = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)) + in + enrich msg exn + | CoercGraph.NotMetaClosed -> + raise (Uncertain (lazy "Coercions on meta")) + | CoercGraph.SomeCoercion c -> + (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph + in + let coerced_args,metasenv',subst',t',ugraph2 = + eat_prods metasenv subst context + (CicSubstitution.subst arg t) ugraph1 tl + in + arg::coerced_args,metasenv',subst',t',ugraph2 + | _ -> assert false + ) + in + let coerced_args,metasenv,subst,t,ugraph2 = + eat_prods metasenv subst context hetype' ugraph1 tlbody_and_type + in + coerced_args,t,subst,metasenv,ugraph2 + in + + (* eat prods ends here! *) + + let t',ty,subst',metasenv',ugraph1 = + type_of_aux [] metasenv context t ugraph + in + let substituted_t = CicMetaSubst.apply_subst subst' t' in + let substituted_ty = CicMetaSubst.apply_subst subst' ty in + (* Andrea: ho rimesso qui l'applicazione della subst al + metasenv dopo che ho droppato l'invariante che il metsaenv + e' sempre istanziato *) + let substituted_metasenv = + CicMetaSubst.apply_subst_metasenv subst' metasenv' in + (* metasenv' *) + (* substituted_t,substituted_ty,substituted_metasenv *) + (* ANDREA: spostare tutta questa robaccia da un altra parte *) + 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 - check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl - with _ -> - raise (NotRefinable "Wrong Explicit Named Substitution") + (n,context',ty') + ) substituted_metasenv in - check_exp_named_subst_aux metasubst metasenv [] + (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) +;; - 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 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 s2,subst,metasenv - | (C.Sort s1, C.Sort s2) -> - (*CSC manca la gestione degli universi!!! *) - 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 (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''))) +let type_of_aux' metasenv context term ugraph = + try + type_of_aux' metasenv context term ugraph + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) - 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 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 +let undebrujin uri typesno tys t = + snd + (List.fold_right + (fun (name,_,_,_) (i,t) -> + (* here the explicit_named_substituion is assumed to be *) + (* of length 0 *) + let t' = Cic.MutInd (uri,i,[]) in + let t = CicSubstitution.subst t' t in + i - 1,t + ) tys (typesno - 1,t)) - in - let ty,subst',metasenv' = - type_of_aux [] metasenv context t +let map_first_n n start f g l = + let rec aux acc k l = + if k < n then + match l with + | [] -> raise (Invalid_argument "map_first_n") + | hd :: tl -> f hd k (aux acc (k+1) tl) + else + g acc l in - 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 - 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) + aux start 0 l + +(*CSC: this is a very rough approximation; to be finished *) +let are_all_occurrences_positive metasenv ugraph uri tys leftno = + let number_of_types = List.length tys in + let subst,metasenv,ugraph,tys = + List.fold_right + (fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) -> + let subst,metasenv,ugraph,cl = + List.fold_right + (fun (name,ty) (subst,metasenv,ugraph,acc) -> + let rec aux ctx k subst = function + | Cic.Appl((Cic.MutInd (uri',_,_)as hd)::tl) when uri = uri'-> + let subst,metasenv,ugraph,tl = + map_first_n leftno + (subst,metasenv,ugraph,[]) + (fun t n (subst,metasenv,ugraph,acc) -> + let subst,metasenv,ugraph = + fo_unif_subst + subst ctx metasenv t (Cic.Rel (k-n)) ugraph + in + subst,metasenv,ugraph,(t::acc)) + (fun (s,m,g,acc) tl -> assert(acc=[]);(s,m,g,tl)) + tl + in + subst,metasenv,ugraph,(Cic.Appl (hd::tl)) + | Cic.MutInd(uri',_,_) as t when uri = uri'-> + subst,metasenv,ugraph,t + | Cic.Prod (name,s,t) -> + let ctx = (Some (name,Cic.Decl s))::ctx in + let subst,metasenv,ugraph,t = aux ctx (k+1) subst t in + subst,metasenv,ugraph,Cic.Prod (name,s,t) + | _ -> + raise + (RefineFailure + (lazy "not well formed constructor type")) in - Some (n, Cic.Def (bo',ty')) - ) context + let subst,metasenv,ugraph,ty = aux [] 0 subst ty in + subst,metasenv,ugraph,(name,ty) :: acc) + cl (subst,metasenv,ugraph,[]) + in + subst,metasenv,ugraph,(name,ind,arity,cl)::acc) + tys ([],metasenv,ugraph,[]) + in + let substituted_tys = + List.map + (fun (name,ind,arity,cl) -> + let cl = + List.map (fun (name, ty) -> name,CicMetaSubst.apply_subst subst ty) cl in - (n,context',ty') - ) substituted_metasenv - in - (cleaned_t,cleaned_ty,cleaned_metasenv) - -;; + name,ind,CicMetaSubst.apply_subst subst arity,cl) + tys + in + metasenv,ugraph,substituted_tys + +let typecheck metasenv uri obj = + let ugraph = CicUniv.empty_ugraph in + match obj with + Cic.Constant (name,Some bo,ty,args,attrs) -> + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph + | Cic.Constant (name,None,ty,args,attrs) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> + assert (metasenv' = metasenv); + (* Here we do not check the metasenv for correctness *) + let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in + let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + begin + match sort with + Cic.Sort _ + (* instead of raising Uncertain, let's hope that the meta will become + a sort *) + | Cic.Meta _ -> () + | _ -> raise (RefineFailure (lazy "The term provided is not a type")) + end; + let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in + let bo' = CicMetaSubst.apply_subst subst bo' in + let ty' = CicMetaSubst.apply_subst subst ty' in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + Cic.CurrentProof (name,metasenv,bo',ty',args,attrs),metasenv,ugraph + | Cic.Variable _ -> assert false (* not implemented *) + | Cic.InductiveDefinition (tys,args,paramsno,attrs) -> + (*CSC: this code is greately simplified and many many checks are missing *) + (*CSC: e.g. the constructors are not required to build their own types, *) + (*CSC: the arities are not required to have as type a sort, etc. *) + let uri = match uri with Some uri -> uri | None -> assert false in + let typesno = List.length tys in + (* first phase: we fix only the types *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in + metasenv,ugraph,(name,b,ty',cl)::res + ) tys (metasenv,ugraph,[]) in + let con_context = + List.rev_map (fun (name,_,ty,_)-> Some (Cic.Name name,Cic.Decl ty)) tys in + (* second phase: we fix only the constructors *) + let metasenv,ugraph,tys = + List.fold_right + (fun (name,b,ty,cl) (metasenv,ugraph,res) -> + let metasenv,ugraph,cl' = + List.fold_right + (fun (name,ty) (metasenv,ugraph,res) -> + let ty = CicTypeChecker.debrujin_constructor uri typesno ty in + let ty',_,metasenv,ugraph = + type_of_aux' metasenv con_context ty ugraph in + let ty' = undebrujin uri typesno tys ty' in + metasenv,ugraph,(name,ty')::res + ) cl (metasenv,ugraph,[]) + in + metasenv,ugraph,(name,b,ty,cl')::res + ) tys (metasenv,ugraph,[]) in + (* third phase: we check the positivity condition *) + let metasenv,ugraph,tys = + are_all_occurrences_positive metasenv ugraph uri tys paramsno + in + Cic.InductiveDefinition (tys,args,paramsno,attrs),metasenv,ugraph -(* DEBUGGING ONLY *) +(* DEBUGGING ONLY let type_of_aux' metasenv context term = try - 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); -*) + let (t,ty,m) = + type_of_aux' metasenv context term in + debug_print (lazy + ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty)); + debug_print (lazy + ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m [])); (t,ty,m) with - | CicUnification.AssertFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; - debug_print msg; + | RefineFailure msg as e -> + debug_print (lazy ("@@@ REFINE FAILED: " ^ msg)); raise e - | CicUnification.UnificationFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:"; - debug_print msg; + | Uncertain msg as e -> + debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); raise e - | e -> - debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; - raise e -;; +;; *) + +let profiler2 = HExtlib.profile "CicRefine" + +let type_of_aux' metasenv context term ugraph = + profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph +let typecheck metasenv uri obj = + profiler2.HExtlib.profile (typecheck metasenv uri) obj