X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic_unification%2FcicRefine.ml;fp=components%2Fcic_unification%2FcicRefine.ml;h=065dbc33d9cd8a3e2d6a6a175962809e63a9997e;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml new file mode 100644 index 000000000..065dbc33d --- /dev/null +++ b/components/cic_unification/cicRefine.ml @@ -0,0 +1,2158 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + +open Printf + +exception RefineFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; + +(* for internal use only; the integer is the number of surplus arguments *) +exception MoreArgsThanExpected of int * exn;; + +let insert_coercions = ref true +let pack_coercions = ref true + +let debug = false;; + +let debug_print = + if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());; + +let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" + +let fo_unif_subst_eat_prods2 subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods2.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + +let profiler_eat_prods = HExtlib.profile "CicRefine.fo_unif_eat_prods" + +let fo_unif_subst_eat_prods subst context metasenv t1 t2 ugraph = + try +let foo () = + CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph +in profiler_eat_prods.HExtlib.profile foo () + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + +let profiler = HExtlib.profile "CicRefine.fo_unif" + +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 localization_tbl t ?(f = fun msg -> msg) exn = + let exn' = + match exn with + RefineFailure msg -> RefineFailure (f msg) + | Uncertain msg -> Uncertain (f msg) + | AssertFailure msg -> prerr_endline (Lazy.force msg); AssertFailure (f msg) + | Sys.Break -> raise exn + | _ -> prerr_endline (Printexc.to_string exn); assert false + in + let loc = + try + Cic.CicHash.find localization_tbl t + with Not_found -> + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + raise exn' + in + raise (HExtlib.Localized (loc,exn')) + +let relocalize localization_tbl oldt newt = + try + let infos = Cic.CicHash.find localization_tbl oldt in + Cic.CicHash.remove localization_tbl oldt; + Cic.CicHash.add localization_tbl newt infos; + with + Not_found -> () +;; + +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 (AssertFailure (lazy "split: list too short")) +;; + +let exp_impl metasenv subst context = + function + | 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) + | Some `Closed -> + let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in + metasenv', Cic.Meta (idx, []) + | 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) + | _ -> assert false +;; + +let is_a_double_coercion t = + let last_of l = + let rec aux acc = function + | x::[] -> acc,x + | x::tl -> aux (acc@[x]) tl + | [] -> assert false + in + aux [] l + in + let imp = Cic.Implicit None in + let dummyres = false,imp, imp,imp,imp in + match t with + | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> + (match last_of tl with + | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> + let sib2,head = last_of tl2 in + true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl + (c2::sib2@[imp])]) + | _ -> dummyres) + | _ -> dummyres + +let more_args_than_expected localization_tbl metasenv subst he context hetype' residuals tlbody_and_type exn += + let len = List.length tlbody_and_type in + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context ^ + " (that has type "^ CicMetaSubst.ppterm_in_context ~metasenv subst hetype' context ^ + ") is here applied to " ^ string_of_int len ^ + " arguments but here it can handle only up to " ^ + string_of_int (len - residuals) ^ " arguments") + in + enrich localization_tbl he ~f:(fun _-> msg) exn +;; + +let mk_prod_of_metas metasenv context subst args = + let rec mk_prod metasenv context' = function + | [] -> + 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'. *) + let name_hint = + FreshNamesGenerator.mk_fresh_name ~subst metasenv + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + ~typ:(CicMetaSubst.apply_subst subst argty) + in + 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 + mk_prod metasenv context args +;; + +let rec type_of_constant 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.Constant (_,_,ty,_,_) -> ty,u + | C.CurrentProof (_,_,_,ty,_,_) -> ty,u + | _ -> + raise + (RefineFailure + (lazy ("Unknown constant definition " ^ 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))) + + +(* 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 ugraph = + let module C = Cic in + (* 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' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t + ugraph += + 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 + let (t',_,_,_,_) as res = + 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 (_,ty)) -> + t,S.lift n ty,subst,metasenv, ugraph + | None -> + enrich localization_tbl t + (RefineFailure (lazy "Rel to hidden hypothesis")) + with + Failure _ -> + enrich localization_tbl t + (RefineFailure (lazy "Not a closed 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 + (try + let ugraph1 = CicUniv.add_gt tno' tno ugraph in + t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | C.Sort _ -> + t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph + | C.Implicit infos -> + let metasenv',t' = exp_impl metasenv subst context infos in + type_of_aux subst metasenv' context t' ugraph + | 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 (te', ty'), subst''',metasenv''',ugraph3 = + coerce_to_something true localization_tbl te' inferredty ty' + subst'' metasenv'' context ugraph2 + in + C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 + | C.Prod (name,s,t) -> + let s',sort1,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context s ugraph + in + let s',sort1,subst', metasenv',ugraph1 = + coerce_to_sort localization_tbl + s' sort1 subst' context metasenv' ugraph1 + in + let context_for_t = ((Some (name,(C.Decl s')))::context) 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 localization_tbl + t' sort2 subst'' context_for_t metasenv'' ugraph2 + in + let sop,subst''',metasenv''',ugraph3 = + sort_of_prod localization_tbl subst'' metasenv'' + context (name,s') t' (sort1,sort2) ugraph2 + in + 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,subst',metasenv',ugraph1 = + coerce_to_sort localization_tbl + s' sort1 subst' context metasenv' ugraph1 + in + let context_for_t = ((Some (n,(C.Decl s')))::context) 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,ty,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 ty,_,subst',metasenv',ugraph1 = + type_of_aux subst' metasenv' context ty ugraph1 in + let subst',metasenv',ugraph1 = + try + fo_unif_subst subst' context metasenv' + ty ty' ugraph1 + with + exn -> + enrich localization_tbl s' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' s' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty' + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv:metasenv' subst' ty + context)) + in + let context_for_t = ((Some (n,(C.Def (s',ty))))::context) 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',ty,t'), + CicSubstitution.subst ~avoid_beta_redexes:true 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 = + typeof_list subst' metasenv' context ugraph1 tl + in + let coerced_he,coerced_args,applty,subst''',metasenv''',ugraph3 = + eat_prods true subst'' metasenv'' context + he' hetype tlbody_and_type ugraph2 + in + let newappl = (C.Appl (coerced_he::coerced_args)) in + avoid_double_coercion + context subst''' metasenv''' ugraph3 newappl applty + | C.Appl _ -> assert false + | 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 + | _ -> + enrich localization_tbl t + (RefineFailure + (lazy ("Unkown mutual inductive definition " ^ + U.string_of_uri uri))) + in + if List.length constructors <> List.length pl then + enrich localization_tbl t + (RefineFailure + (lazy "Wrong number of cases")) ; + 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 = + try + fo_unif_subst subst context metasenv + expected_type' actual_type ugraph2 + with + exn -> + enrich localization_tbl term' exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst term' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context)) + 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_right + (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) -> + 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 = + try + check_branch 0 context metasenv subst + no_left_params actual_type constructor' expected_type + ugraph2 + with + exn -> + enrich localization_tbl constructor' + ~f:(fun _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst p' + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context metasenv subst actual_type + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context metasenv subst expected_type + context)) exn + in + (p'::pl,j-1, + outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) + pl ([],List.length pl,[],subst,metasenv,ugraph3) + 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 + *) + + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 in + (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 + | RefineFailure _ | 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 = + try + fo_unif_subst subst context metasenv + candidate outtype ugraph5 + with + exn -> assert false(* unification against a metavariable *) + 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 tlbody_and_type,subst,metasenv,ugraph4 = + typeof_list subst metasenv context ugraph4 (right_args @ [term']) + in + let _,_,_,subst,metasenv,ugraph4 = + eat_prods false subst metasenv context + outtype 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_left2 + (fun (subst,metasenv,ugraph) + p (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 + try + fo_unif_subst subst context metasenv instance instance' + ugraph + with + exn -> + enrich localization_tbl p exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst p + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst instance' + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst instance + context))) + (subst,metasenv,ugraph5) pl' 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,len = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph,len) (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 (CicSubstitution.lift len ty'))) + :: types, ugraph, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl + 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 bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph in + let expected_ty = CicSubstitution.lift len ty in + let subst',metasenv',ugraph' = + try + fo_unif_subst subst context' metasenv + ty_of_bo expected_ty ugraph1 + with + exn -> + enrich localization_tbl bo exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo + context' ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo + context' ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty + context)) + 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,len = + List.fold_left + (fun (fl,subst,metasenv,types,ugraph,len) (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 (CicSubstitution.lift len ty'))) :: + types, ugraph1, len+1 + ) ([],subst,metasenv,[],ugraph,0) fl + in + let context' = types@context in + let fl_bo',subst,metasenv,ugraph2 = + List.fold_left + (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) -> + let bo',ty_of_bo,subst,metasenv,ugraph1 = + type_of_aux subst metasenv context' bo ugraph in + let expected_ty = CicSubstitution.lift len ty in + let subst',metasenv',ugraph' = + try + fo_unif_subst subst context' metasenv + ty_of_bo expected_ty ugraph1 + with + exn -> + enrich localization_tbl bo exn + ~f:(function _ -> + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst bo + context' ^ " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo + context' ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty + context)) + 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 + in + relocalize localization_tbl t t'; + res + + (* 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 = + function + [] -> [] + | (Some (n,C.Decl t))::tl -> + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) + | None::tl -> None::(aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some + (n, + C.Def + (S.subst_meta l (S.lift i t), + 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,_)) -> + (*CSC: the following optimization is to avoid a possibly + expensive reduction that can be easily avoided and + that is quite frequent. However, this is better + handled using levels to control reduction *) + let optimized_t = + match t with + Cic.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with + Failure _ -> t) + | _ -> t + in + let subst',metasenv',ugraph' = + (try +(*prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' + * il Rel corrispondente. Si puo' ottimizzare il caso t = rel.");*) + fo_unif_subst subst context metasenv optimized_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 ~metasenv subst optimized_t) (CicMetaSubst.ppterm ~metasenv 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 metasenv' subst' inferredty) (CicMetaSubst.ppterm metasenv' subst' t) (CicMetaSubst.ppterm metasenv' 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 ~metasenv subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext ~metasenv 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 ~metasenv subst (Cic.Meta (metano, l))) + (CicMetaSubst.ppcontext ~metasenv 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)::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 subst = uri,t' 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 metasenv' metasubst' typeoft ^ + " not unifiable with " ^ + CicMetaSubst.ppterm metasenv' 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 localization_tbl subst metasenv context (name,s) t (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 + (try + 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 + with + CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) + | (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 + * break 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) = + try + fo_unif_subst subst context_for_t2 metasenv + (C.Meta (idx,[])) t2'' ugraph + with _ -> assert false (* unification against a metavariable *) + in + t2'',subst,metasenv,ugraph1 + | (C.Sort _,_) + | (C.Meta _,_) -> + enrich localization_tbl s + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst t context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)))) + | _,_ -> + enrich localization_tbl t + (RefineFailure + (lazy + (sprintf + "%s is supposed to be a type, but its type is %s" + (CicMetaSubst.ppterm_in_context ~metasenv subst s context) + (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)))) + + and avoid_double_coercion context subst metasenv ugraph t ty = + if not !pack_coercions then + t,ty,subst,metasenv,ugraph + else + let b, c1, c2, head, c1_c2_implicit = is_a_double_coercion t in + if b then + let source_carr = CoercGraph.source_of c2 in + let tgt_carr = CicMetaSubst.apply_subst subst ty in + (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr + with + | CoercGraph.SomeCoercion candidates -> + let selected = + HExtlib.list_findopt + (function (metasenv,last,c) -> + match c with + | c when not (CoercGraph.is_composite c) -> + debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); + None + | c -> + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last head ugraph in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); + (try + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c)); + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context c ugraph in + debug_print (lazy "tipa..."); + let subst, metasenv, ugraph = + (* COME MAI C'ERA UN IF su !pack_coercions ??? *) + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print (lazy "unifica..."); + Some (newt, ty, subst, metasenv, ugraph) + with + | RefineFailure s | Uncertain s when not !pack_coercions-> + debug_print s; debug_print (lazy "stop\n");None + | RefineFailure s | Uncertain s -> + debug_print s;debug_print (lazy "goon\n"); + try + let old_pack_coercions = !pack_coercions in + pack_coercions := false; (* to avoid diverging *) + let refined_c1_c2_implicit,ty,subst,metasenv,ugraph = + type_of_aux subst metasenv context c1_c2_implicit ugraph + in + pack_coercions := old_pack_coercions; + let b, _, _, _, _ = + is_a_double_coercion refined_c1_c2_implicit + in + if b then + None + else + let head' = + match refined_c1_c2_implicit with + | Cic.Appl l -> HExtlib.list_last l + | _ -> assert false + in + let subst, metasenv, ugraph = + try fo_unif_subst subst context metasenv + head head' ugraph + with RefineFailure s| Uncertain s-> + debug_print s;assert false + in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv + refined_c1_c2_implicit t ugraph + in + Some (refined_c1_c2_implicit,ty,subst,metasenv,ugraph) + with + | RefineFailure s | Uncertain s -> + pack_coercions := true;debug_print s;None + | exn -> pack_coercions := true; raise exn)) + candidates + in + (match selected with + | Some x -> x + | None -> + debug_print + (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); + t, ty, subst, metasenv, ugraph) + | _ -> t, ty, subst, metasenv, ugraph) + else + t, ty, subst, metasenv, ugraph + + and typeof_list subst metasenv context ugraph l = + let tlbody_and_type,subst,metasenv,ugraph = + 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 + ) l ([],subst,metasenv,ugraph) + in + tlbody_and_type,subst,metasenv,ugraph + + and eat_prods + allow_coercions subst metasenv context he hetype args_bo_and_ty ugraph + = + (* given he:hety, gives beack all (c he) such that (c e):?->? *) + let fix_arity n metasenv context subst he hetype ugraph = + let hetype = CicMetaSubst.apply_subst subst hetype in + let src = CoercDb.coerc_carr_of_term hetype in + let tgt = CoercDb.Fun 0 in + match CoercGraph.look_for_coercion' metasenv subst context src tgt with + | CoercGraph.NoCoercion -> [] + | CoercGraph.NotMetaClosed + | CoercGraph.NotHandled _ -> + raise (MoreArgsThanExpected (n,Uncertain (lazy ""))) + | CoercGraph.SomeCoercionToTgt candidates + | CoercGraph.SomeCoercion candidates -> + HExtlib.filter_map + (fun (metasenv,last,coerc) -> + let pp t = + CicMetaSubst.ppterm_in_context ~metasenv subst t context in + try + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last he ugraph in + debug_print (lazy ("New head: "^ pp coerc)); + let tty,ugraph = + CicTypeChecker.type_of_aux' ~subst metasenv context coerc + ugraph + in + debug_print (lazy (" has type: "^ pp tty)); + Some (coerc,tty,subst,metasenv,ugraph) + with + | Uncertain _ | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) + candidates + in + (* aux function to process the type of the head and the args in parallel *) + let rec eat_prods_and_args metasenv subst context he hetype ugraph newargs = + function + | [] -> newargs,subst,metasenv,he,hetype,ugraph + | (hete, hety)::tl as args -> + match (CicReduction.whd ~subst context hetype) with + | Cic.Prod (n,s,t) -> + let arg,subst,metasenv,ugraph = + coerce_to_something allow_coercions localization_tbl + hete hety s subst metasenv context ugraph in + eat_prods_and_args + metasenv subst context he (CicSubstitution.subst (fst arg) t) + ugraph (newargs@[arg]) tl + | _ -> + let he = + match he, newargs with + | _, [] -> he + | Cic.Appl l, _ -> Cic.Appl (l@List.map fst newargs) + | _ -> Cic.Appl (he::List.map fst newargs) + in + (*{{{*) debug_print (lazy + let pp x = + CicMetaSubst.ppterm_in_context ~metasenv subst x context in + "Fixing arity of: "^ pp he ^ "\n that has type: "^ pp hetype^ + "\n but is applyed to: " ^ String.concat ";" + (List.map (fun (t,_)->pp t) args_bo_and_ty)); (*}}}*) + let possible_fixes = + fix_arity (List.length args) metasenv context subst he hetype + ugraph in + match + HExtlib.list_findopt + (fun (he,hetype,subst,metasenv,ugraph) -> + (* {{{ *)debug_print (lazy ("Try fix: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst he context)); + debug_print (lazy (" of type: "^ + CicMetaSubst.ppterm_in_context + ~metasenv subst hetype context)); (* }}} *) + try + Some (eat_prods_and_args + metasenv subst context he hetype ugraph [] args) + with + | RefineFailure _ | Uncertain _ + | HExtlib.Localized (_,RefineFailure _) + | HExtlib.Localized (_,Uncertain _) -> None) + possible_fixes + with + | Some x -> x + | None -> + raise + (MoreArgsThanExpected + (List.length args, RefineFailure (lazy ""))) + in + (* first we check if we are in the simple case of a meta closed term *) + let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = + if CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst hetype) then + (* this optimization is to postpone fix_arity (the most common case)*) + subst,metasenv,ugraph,hetype,he,args_bo_and_ty + else + (* this (says CSC) is also useful to infer dependent types *) + let pristinemenv = metasenv in + let metasenv,hetype' = + mk_prod_of_metas metasenv context subst args_bo_and_ty + in + try + let subst,metasenv,ugraph = + fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph + in + subst,metasenv,ugraph,hetype',he,args_bo_and_ty + with RefineFailure _ | Uncertain _ -> + subst,pristinemenv,ugraph,hetype,he,args_bo_and_ty + in + let coerced_args,subst,metasenv,he,t,ugraph = + try + eat_prods_and_args + metasenv subst context he hetype' ugraph1 [] args_bo_and_ty + with + MoreArgsThanExpected (residuals,exn) -> + more_args_than_expected localization_tbl metasenv + subst he context hetype' residuals args_bo_and_ty exn + in + he,(List.map fst coerced_args),t,subst,metasenv,ugraph + + and coerce_to_something + allow_coercions localization_tbl t infty expty subst metasenv context ugraph + = + let module CS = CicSubstitution in + let module CR = CicReduction in + let cs_subst = CS.subst ~avoid_beta_redexes:true in + let coerce_atom_to_something t infty expty subst metasenv context ugraph = + debug_print (lazy ("COERCE_ATOM_TO_SOMETHING")); + let coer = + CoercGraph.look_for_coercion metasenv subst context infty expty + in + match coer with + | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy + "coerce_atom_to_something fails since not meta closed")) + | CoercGraph.NoCoercion + | CoercGraph.SomeCoercionToTgt _ + | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + "coerce_atom_to_something fails since no coercions found")) + | CoercGraph.SomeCoercion candidates -> + debug_print (lazy (string_of_int (List.length candidates) ^ + " candidates found")); + let uncertain = ref false in + let selected = + let posibilities = + HExtlib.filter_map + (fun (metasenv,last,c) -> + try + (* {{{ *) debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst last context ^ + " <==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ + "####" ^ CicMetaSubst.ppterm_in_context ~metasenv subst c + context)); + debug_print (lazy ("FO_UNIF_SUBST: " ^ + CicPp.ppterm last ^ " <==> " ^ CicPp.ppterm t)); (* }}} *) + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last t ugraph + in + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context c ugraph in + let newt, newty, subst, metasenv, ugraph = + avoid_double_coercion context subst metasenv ugraph newt expty + in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv newhety expty ugraph in + Some ((newt,newty), subst, metasenv, ugraph) + with + | Uncertain _ -> uncertain := true; None + | RefineFailure _ -> None) + candidates + in + match + List.fast_sort + (fun (_,_,m1,_) (_,_,m2,_) -> List.length m1 - List.length m2) + posibilities + with + | [] -> None + | x::_ -> Some x + in + match selected with + | Some x -> x + | None when !uncertain -> raise (Uncertain (lazy "coerce_atom fails")) + | None -> raise (RefineFailure (lazy "coerce_atom fails")) + in + let rec coerce_to_something_aux + t infty expty subst metasenv context ugraph + = + try + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv infty expty ugraph + in + (t, expty), subst, metasenv, ugraph + with (Uncertain _ | RefineFailure _ as exn) + when allow_coercions && !insert_coercions -> + let whd = CicReduction.whd ~delta:false in + let clean t s c = whd c (CicMetaSubst.apply_subst s t) in + let infty = clean infty subst context in + let expty = clean expty subst context in + let t = clean t subst context in + (*{{{*) debug_print (lazy ("COERCE_TO_SOMETHING: " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*) + let (coerced,_),subst,metasenv,_ as result = + match infty, expty, t with + | Cic.Prod (nameprod,src,ty), Cic.Prod (_,src2,ty2),Cic.Fix (n,fl) -> + (*{{{*) debug_print (lazy "FIX"); + (match fl with + [name,i,_(* infty *),bo] -> + let context_bo = + Some (Cic.Name name,Cic.Decl expty)::context in + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux (Cic.Rel 1) + (CS.lift 1 expty) (CS.lift 1 infty) subst + metasenv context_bo ugraph in + let bo = cs_subst rel1 (CS.lift_from 2 1 bo) in + let (bo,_), subst, metasenv, ugraph = + coerce_to_something_aux bo (CS.lift 1 infty) (CS.lift 1 + expty) subst + metasenv context_bo ugraph + in + (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph + | _ -> assert false (* not implemented yet *)) (*}}}*) + | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> + (*{{{*) debug_print (lazy "CASE"); + (* {{{ helper functions *) + let get_cl_and_left_p uri tyno outty ugraph = + match CicEnvironment.get_obj ugraph uri with + | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> + let count_pis t = + let rec aux ctx t = + match CicReduction.whd ~delta:false ctx t with + | Cic.Prod (name,src,tgt) -> + let ctx = Some (name, Cic.Decl src) :: ctx in + 1 + aux ctx tgt + | _ -> 0 + in + aux [] t + in + let rec skip_lambda_delifting t n = + match t,n with + | _,0 -> t + | Cic.Lambda (_,_,t),n -> + skip_lambda_delifting + (CS.subst (Cic.Implicit None) t) (n - 1) + | _ -> assert false + in + let get_l_r_p n = function + | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] + | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> + HExtlib.split_nth n args + | _ -> assert false + in + let _, _, ty, cl = List.nth tl tyno in + let pis = count_pis ty in + let rno = pis - leftno in + let t = skip_lambda_delifting outty rno in + let left_p, _ = get_l_r_p leftno t in + let instantiale_with_left cl = + List.map + (fun ty -> + List.fold_left + (fun t p -> match t with + | Cic.Prod (_,_,t) -> + cs_subst p t + | _-> assert false) + ty left_p) + cl + in + let cl = instantiale_with_left (List.map snd cl) in + cl, left_p, leftno, rno, ugraph + | _ -> raise exn + in + let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = + match t,n with + | _,0 -> + let rec mkr n = function + | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl + in + let bo = + CicReplace.replace_lifting + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:ctx + ~what:(matched::right_p) + ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) + ~where:bo + in + bo + | Cic.Lambda (name, src, tgt),_ -> + Cic.Lambda (name, src, + keep_lambdas_and_put_expty + (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo) + (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1)) + | _ -> assert false + in + let eq_uri, eq, eq_refl = + match LibraryObjects.eq_URI () with + | None -> HLog.warn "no default equality"; raise exn + | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) + in + let add_params + metasenv subst context uri tyno cty outty mty m leftno i + = + let rec aux context outty par k mty m = function + | Cic.Prod (name, src, tgt) -> + let t,k = + aux + (Some (name, Cic.Decl src) :: context) + (CS.lift 1 outty) (Cic.Rel k::par) (k+1) + (CS.lift 1 mty) (CS.lift 1 m) tgt + in + Cic.Prod (name, src, t), k + | Cic.MutInd _ -> + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + if par <> [] then Cic.Appl (k::par) else k + in + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl [outty;k])))),k + | Cic.Appl (Cic.MutInd _::pl) -> + let left_p,right_p = HExtlib.split_nth leftno pl in + let has_rights = right_p <> [] in + let k = + let k = Cic.MutConstruct (uri,tyno,i,[]) in + Cic.Appl (k::left_p@par) + in + let right_p = + try match + CicTypeChecker.type_of_aux' ~subst metasenv context k + CicUniv.oblivion_ugraph + with + | Cic.Appl (Cic.MutInd _::args),_ -> + snd (HExtlib.split_nth leftno args) + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _-> assert false + in + if has_rights then + CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k])),k + else + Cic.Prod (Cic.Name "p", + Cic.Appl [eq; mty; m; k], + (CS.lift 1 + (CR.head_beta_reduce ~delta:false + (Cic.Appl (outty ::right_p @ [k]))))),k + | _ -> assert false + in + aux context outty [] 1 mty m cty + in + let add_lambda_for_refl_m pbo rno mty m k cty = + (* k lives in the right context *) + if rno <> 0 then pbo else + let rec aux mty m = function + | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> + Cic.Lambda (name,src, + (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) + | t,_ -> + Cic.Lambda (Cic.Name "p", + Cic.Appl [eq; mty; m; k],CS.lift 1 t) + in + aux mty m (pbo,cty) + in + let add_pi_for_refl_m new_outty mty m rno = + if rno <> 0 then new_outty else + let rec aux m mty = function + | Cic.Lambda (name, src, tgt) -> + Cic.Lambda (name, src, + aux (CS.lift 1 m) (CS.lift 1 mty) tgt) + | t -> + Cic.Prod + (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], + CS.lift 1 t) + in + aux m mty new_outty + in (* }}} end helper functions *) + (* constructors types with left params already instantiated *) + let outty = CicMetaSubst.apply_subst subst outty in + let cl, left_p, leftno,rno,ugraph = + get_cl_and_left_p uri tyno outty ugraph + in + let right_p, mty = + try + match + CicTypeChecker.type_of_aux' ~subst metasenv context m + CicUniv.oblivion_ugraph + with + | Cic.MutInd _ as mty,_ -> [], mty + | Cic.Appl (Cic.MutInd _::args) as mty,_ -> + snd (HExtlib.split_nth leftno args), mty + | _ -> assert false + with CicTypeChecker.TypeCheckerFailure _ -> assert false + in + let new_outty = + keep_lambdas_and_put_expty context outty expty right_p m (rno+1) + in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let _,pl,subst,metasenv,ugraph = + List.fold_right2 + (fun cty pbo (i, acc, s, menv, ugraph) -> + (* Pi k_par, (Pi H:m=(K_i left_par k_par)), + * (new_)outty right_par (K_i left_par k_par) *) + let infty_pbo, _ = + add_params menv s context uri tyno + cty outty mty m leftno i in + debug_print + (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context + ~metasenv subst infty_pbo context)); + let expty_pbo, k = (* k is (K_i left_par k_par) *) + add_params menv s context uri tyno + cty new_outty mty m leftno i in + debug_print + (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context + ~metasenv subst expty_pbo context)); + let pbo = add_lambda_for_refl_m pbo rno mty m k cty in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + let (pbo, _), subst, metasenv, ugraph = + coerce_to_something_aux pbo infty_pbo expty_pbo + s menv context ugraph + in + debug_print + (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst pbo context)); + (i-1, pbo::acc, subst, metasenv, ugraph)) + cl pl (List.length pl, [], subst, metasenv, ugraph) + in + let new_outty = add_pi_for_refl_m new_outty mty m rno in + debug_print + (lazy ("CASE: new_outty: " ^ CicMetaSubst.ppterm_in_context + ~metasenv subst new_outty context)); + let t = + if rno = 0 then + let refl_m=Cic.Appl[eq_refl;mty;m]in + Cic.Appl [Cic.MutCase(uri,tyno,new_outty,m,pl);refl_m] + else + Cic.MutCase(uri,tyno,new_outty,m,pl) + in + (t, expty), subst, metasenv, ugraph (*}}}*) + | Cic.Prod (nameprod, src, ty),Cic.Prod (_, src2, ty2), _ -> + (*{{{*) debug_print (lazy "LAM"); + let name_con = + FreshNamesGenerator.mk_fresh_name + ~subst metasenv context ~typ:src2 Cic.Anonymous + in + let context_src2 = (Some (name_con, Cic.Decl src2) :: context) in + (* contravariant part: the argument of f:src->ty *) + let (rel1, _), subst, metasenv, ugraph = + coerce_to_something_aux + (Cic.Rel 1) (CS.lift 1 src2) + (CS.lift 1 src) subst metasenv context_src2 ugraph + in + (* covariant part: the result of f(c x); x:src2; (c x):src *) + let name_t, bo = + match t with + | Cic.Lambda (n,_,bo) -> n, cs_subst rel1 (CS.lift_from 2 1 bo) + | _ -> name_con, Cic.Appl[CS.lift 1 t;rel1] + in + (* we fix the possible dependency problem in the source ty *) + let ty = cs_subst rel1 (CS.lift_from 2 1 ty) in + let (bo, _), subst, metasenv, ugraph = + coerce_to_something_aux + bo ty ty2 subst metasenv context_src2 ugraph + in + let coerced = Cic.Lambda (name_t,src2, bo) in + (coerced, expty), subst, metasenv, ugraph (*}}}*) + | _ -> + (*{{{*)debug_print (lazy ("ATOM: "^CicMetaSubst.ppterm_in_context + ~metasenv subst infty context ^ " ==> " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst expty context)); + coerce_atom_to_something + t infty expty subst metasenv context ugraph (*}}}*) + in + debug_print (lazy ("COERCE TO SOMETHING END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst coerced context)); + result + in + try + coerce_to_something_aux t infty expty subst metasenv context ugraph + with Uncertain _ | RefineFailure _ as exn -> + let f _ = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context metasenv subst t context ^ + " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst + infty context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context metasenv subst expty context) + in + enrich localization_tbl ~f t exn + + and coerce_to_sort localization_tbl t infty subst context metasenv uragph = + match CicReduction.whd ~delta:false ~subst context infty with + | Cic.Meta _ | Cic.Sort _ -> + t,infty, subst, metasenv, ugraph + | src -> + debug_print (lazy ("COERCE TO SORT: "^CicMetaSubst.ppterm_in_context + ~metasenv subst src context)); + let tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in + try + let (t, ty_t), subst, metasenv, ugraph = + coerce_to_something true + localization_tbl t src tgt subst metasenv context ugraph + in + debug_print (lazy ("COERCE TO SORT END: "^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context)); + t, ty_t, subst, metasenv, ugraph + with HExtlib.Localized (_, exn) -> + let f _ = + lazy ("(7)The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst t context + ^ " is not a type since it has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv subst src context + ^ " that is not a sort") + in + enrich localization_tbl ~f t exn + 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' = 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,ugraph1) +;; + +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)) + +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 + 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 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 + 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 + name,ind,CicMetaSubst.apply_subst subst arity,cl) + tys + in + metasenv,ugraph,substituted_tys + +let typecheck metasenv uri obj ~localization_tbl = + let ugraph = CicUniv.empty_ugraph in + match obj with + Cic.Constant (name,Some bo,ty,args,attrs) -> + (* CSC: ugly code. Here I need to retrieve in advance the loc of bo + since type_of_aux' destroys localization information (which are + preserved by type_of_aux *) + let loc exn' = + try + Cic.CicHash.find localization_tbl bo + with Not_found -> + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo); + raise exn' in + let bo',boty,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] bo ugraph in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv [] ty ugraph in + let subst,metasenv,ugraph = + try + fo_unif_subst [] [] metasenv boty ty' ugraph + with + RefineFailure _ + | Uncertain _ as exn -> + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^ + " has type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^ + " but is here used with type " ^ + CicMetaSubst.ppterm_in_context ~metasenv [] ty' []) + in + let exn' = + match exn with + RefineFailure _ -> RefineFailure msg + | Uncertain _ -> Uncertain msg + | _ -> assert false + in + raise (HExtlib.Localized (loc exn',exn')) + 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' ~localization_tbl 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' ~localization_tbl metasenv [] bo ugraph in + let ty',sort,metasenv,ugraph = + type_of_aux' ~localization_tbl 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' ~localization_tbl 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 saved_menv = metasenv in + 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 + ~cb:(relocalize localization_tbl) uri typesno [] ty in + let ty',_,metasenv,ugraph = + type_of_aux' ~localization_tbl metasenv con_context ty ugraph in + let ty' = undebrujin uri typesno tys ty' in + metasenv@saved_menv,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 +;; + +(* sara' piu' veloce che raffinare da zero? mah.... *) +let pack_coercion metasenv ctx t = + let module C = Cic in + let rec merge_coercions ctx = + let aux = (fun (u,t) -> u,merge_coercions ctx t) in + function + | C.Rel _ | C.Sort _ | C.Implicit _ as t -> t + | C.Meta (n,subst) -> + let subst' = + List.map + (function None -> None | Some t -> Some (merge_coercions ctx t)) subst + in + C.Meta (n,subst') + | C.Cast (te,ty) -> C.Cast (merge_coercions ctx te, merge_coercions ctx ty) + | C.Prod (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Prod (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.Lambda (name,so,dest) -> + let ctx' = (Some (name,C.Decl so))::ctx in + C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) + | C.LetIn (name,so,ty,dest) -> + let ctx' = Some (name,(C.Def (so,ty)))::ctx in + C.LetIn + (name, merge_coercions ctx so, merge_coercions ctx ty, + merge_coercions ctx' dest) + | C.Appl l -> + let l = List.map (merge_coercions ctx) l in + let t = C.Appl l in + let b,_,_,_,_ = is_a_double_coercion t in + if b then + let ugraph = CicUniv.oblivion_ugraph in + let old_insert_coercions = !insert_coercions in + insert_coercions := false; + let newt, _, menv, _ = + try + type_of_aux' metasenv ctx t ugraph + with RefineFailure _ | Uncertain _ -> + t, t, [], ugraph + in + insert_coercions := old_insert_coercions; + if metasenv <> [] || menv = [] then + newt + else + (prerr_endline "PUO' SUCCEDERE!!!!!";t) + else + t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Var (uri, exp_named_subst) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.Const (uri, exp_named_subst) + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutInd (uri,tyno,exp_named_subst) + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst = List.map aux exp_named_subst in + C.MutConstruct (uri,tyno,consno,exp_named_subst) + | C.MutCase (uri,tyno,out,te,pl) -> + let pl = List.map (merge_coercions ctx) pl in + C.MutCase (uri,tyno,merge_coercions ctx out, merge_coercions ctx te, pl) + | C.Fix (fno, fl) -> + let ctx' = + List.fold_left + (fun l (n,_,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,idx,ty,bo) -> + (name,idx,merge_coercions ctx ty,merge_coercions ctx' bo)) + fl + in + C.Fix (fno, fl) + | C.CoFix (fno, fl) -> + let ctx' = + List.fold_left + (fun l (n,ty,_) -> (Some (C.Name n,C.Decl ty))::l) + ctx fl + in + let fl = + List.map + (fun (name,ty,bo) -> + (name, merge_coercions ctx ty, merge_coercions ctx' bo)) + fl + in + C.CoFix (fno, fl) + in + merge_coercions ctx t +;; + +let pack_coercion_metasenv conjectures = conjectures (* + + TASSI: this code war written when coercions were a toy, + now packing coercions involves unification thus + the metasenv may change, and this pack coercion + does not handle that. + + let module C = Cic in + List.map + (fun (i, ctx, ty) -> + let ctx = + List.fold_right + (fun item ctx -> + let item' = + match item with + Some (name, C.Decl t) -> + Some (name, C.Decl (pack_coercion conjectures ctx t)) + | Some (name, C.Def (t,None)) -> + Some (name,C.Def (pack_coercion conjectures ctx t,None)) + | Some (name, C.Def (t,Some ty)) -> + Some (name, C.Def (pack_coercion conjectures ctx t, + Some (pack_coercion conjectures ctx ty))) + | None -> None + in + item'::ctx + ) ctx [] + in + ((i,ctx,pack_coercion conjectures ctx ty)) + ) conjectures + *) +;; + +let pack_coercion_obj obj = obj (* + + TASSI: this code war written when coercions were a toy, + now packing coercions involves unification thus + the metasenv may change, and this pack coercion + does not handle that. + + let module C = Cic in + match obj with + | C.Constant (id, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] [] body) + in + let ty = pack_coercion [] [] ty in + C.Constant (id, body, ty, params, attrs) + | C.Variable (name, body, ty, params, attrs) -> + let body = + match body with + | None -> None + | Some body -> Some (pack_coercion [] [] body) + in + let ty = pack_coercion [] [] ty in + C.Variable (name, body, ty, params, attrs) + | C.CurrentProof (name, conjectures, body, ty, params, attrs) -> + let conjectures = pack_coercion_metasenv conjectures in + let body = pack_coercion conjectures [] body in + let ty = pack_coercion conjectures [] ty in + C.CurrentProof (name, conjectures, body, ty, params, attrs) + | C.InductiveDefinition (indtys, params, leftno, attrs) -> + let indtys = + List.map + (fun (name, ind, arity, cl) -> + let arity = pack_coercion [] [] arity in + let cl = + List.map (fun (name, ty) -> (name,pack_coercion [] [] ty)) cl + in + (name, ind, arity, cl)) + indtys + in + C.InductiveDefinition (indtys, params, leftno, attrs) *) +;; + + +(* DEBUGGING ONLY +let type_of_aux' metasenv context term = + try + 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 + | RefineFailure msg as e -> + debug_print (lazy ("@@@ REFINE FAILED: " ^ msg)); + raise e + | Uncertain msg as e -> + debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg)); + raise e +;; *) + +let profiler2 = HExtlib.profile "CicRefine" + +let type_of_aux' ?localization_tbl metasenv context term ugraph = + profiler2.HExtlib.profile + (type_of_aux' ?localization_tbl metasenv context term) ugraph + +let typecheck ~localization_tbl metasenv uri obj = + profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj + +let _ = DoubleTypeInference.pack_coercion := pack_coercion;; +(* vim:set foldmethod=marker: *)