(* 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;; let insert_coercions = ref true let pack_coercions = ref true let debug_print = fun _ -> ();; (*let debug_print x = prerr_endline (Lazy.force x);;*) 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) | _ -> assert false in let loc = try Cic.CicHash.find localization_tbl t with Not_found -> prerr_endline ("!!! 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 CoercGraph.is_a_coercion c1 -> (match last_of tl with | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> let sib2,head = last_of tl2 in true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl (c2::sib2@[Cic.Implicit None])]) | _ -> dummyres) | _ -> dummyres let more_args_than_expected localization_tbl subst he context hetype' tlbody_and_type exn = let msg = lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst he context ^ " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^ ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ " arguments that are more than expected") 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 = (* 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 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 try_coercion t subst metasenv context ugraph coercion_tgt c = let coerced = Cic.Appl[c;t] in try let newt,_,subst,metasenv,ugraph = type_of_aux subst metasenv context coerced ugraph in let newt, tty, subst, metasenv, ugraph = avoid_double_coercion context subst metasenv ugraph newt coercion_tgt in Some (newt, tty, subst, metasenv, ugraph) with | RefineFailure _ | Uncertain _ -> None in 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 (_,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 -> enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) with _ -> enrich localization_tbl t (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 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 (try let subst''',metasenv''',ugraph3 = fo_unif_subst subst'' context metasenv'' inferredty ty' ugraph2 in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with exn -> enrich localization_tbl te' ~f:(fun _ -> lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst'' te' context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst'' inferredty context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context subst'' ty' context)) exn ) | 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 context metasenv uragph = if not !insert_coercions then t,type_to_coerce,subst,metasenv,ugraph else let coercion_src = carr type_to_coerce subst context in match coercion_src with | Cic.Sort _ -> t,type_to_coerce,subst,metasenv,ugraph | 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 context in let boh = CoercGraph.look_for_coercion coercion_src coercion_tgt in (match boh with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl t (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl t (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt (try_coercion t subst metasenv context ugraph coercion_tgt) candidates in match selected with | Some x -> x | None -> enrich localization_tbl t (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))) 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 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 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 = if not !insert_coercions then s',sort1, subst', metasenv', ugraph1 else match CicReduction.whd ~subst:subst' context sort1 with | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 | coercion_src -> let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in let boh = CoercGraph.look_for_coercion coercion_src coercion_tgt in match boh with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.NotMetaClosed -> enrich localization_tbl s' (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt (try_coercion s' subst' metasenv' context ugraph1 coercion_tgt) candidates in match selected with | Some x -> x | None -> enrich localization_tbl s' (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) 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,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 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 = 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 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 subst term' context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst actual_type context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context 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_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 (* 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 | 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 = 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 subst p context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst instance' context ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context 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 = 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 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 subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context subst ty_of_bo context' ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context 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 = 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 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 subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context subst ty_of_bo context' ^ " but is here used with type " ^ CicMetaSubst.ppterm_in_context 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) | (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)::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 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 * 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 | _,_ -> 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 avoid_double_coercion context subst metasenv ugraph t ty = 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 source_carr tgt_carr with | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt (function | c when not (CoercGraph.is_composite c) -> debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); None | c -> let newt = match c with | Cic.Appl l -> Cic.Appl (l @ [head]) | _ -> Cic.Appl [c;head] in debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); (try debug_print (lazy ("packing: " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); let newt,_,subst,metasenv,ugraph = type_of_aux subst metasenv context newt 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 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 := true; 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 = (* aux function to add coercions to funclass *) let rec fix_arity metasenv context subst he hetype args_bo_and_ty ugraph = (* {{{ body *) 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 s | Uncertain s as exn when allow_coercions && !insert_coercions -> (* {{{ we search a coercion of the head (saturated) to funclass *) let metasenv = pristinemenv in debug_print (lazy ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' (* ^ " cause: " ^ Lazy.force s *))); let how_many_args_are_needed = let rec aux n = function | Cic.Prod(_,_,t) -> aux (n+1) t | _ -> n in aux 0 (CicMetaSubst.apply_subst subst hetype) in let args, remainder = HExtlib.split_nth how_many_args_are_needed args_bo_and_ty in let args = List.map fst args in let x = if args <> [] then match he with | Cic.Appl l -> Cic.Appl (l@args) | _ -> Cic.Appl (he::args) else he in let x,xty,subst,metasenv,ugraph = type_of_aux subst metasenv context x ugraph in let carr_src = CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) in let carr_tgt = CoercDb.Fun 0 in match CoercGraph.look_for_coercion' carr_src carr_tgt with | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt (fun coerc -> let t = Cic.Appl [coerc;x] in debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm subst t)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) let t,tty,subst,metasenv,ugraph = type_of_aux subst metasenv context t ugraph in try let metasenv, hetype' = mk_prod_of_metas metasenv context subst remainder in debug_print (lazy (" unif: " ^ CicMetaSubst.ppterm subst tty ^ " = " ^ CicMetaSubst.ppterm subst hetype')); let subst,metasenv,ugraph = fo_unif_subst_eat_prods subst context metasenv tty hetype' ugraph in debug_print (lazy " success!"); Some (subst,metasenv,ugraph,tty,t,remainder) with | Uncertain _ | RefineFailure _ | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> try let subst,metasenv,ugraph,hetype',he,args_bo_and_ty = fix_arity metasenv context subst t tty remainder ugraph in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None with Uncertain _ | RefineFailure _ -> None) candidates with | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> subst,metasenv,ugraph,hetype',he,args_bo_and_ty | None -> more_args_than_expected localization_tbl subst he context hetype args_bo_and_ty exn (* }}} end coercion to funclass stuff *) (* }}} end fix_arity *) in (* aux function to process the type of the head and the args in parallel *) let rec eat_prods_and_args pristinemenv metasenv subst context pristinehe he hetype ugraph newargs = (* {{{ body *) function | [] -> newargs,subst,metasenv,he,hetype,ugraph | (hete, hety)::tl -> match (CicReduction.whd ~subst context hetype) with | Cic.Prod (n,s,t) -> let arg,subst,metasenv,ugraph1 = try let subst,metasenv,ugraph1 = fo_unif_subst_eat_prods2 subst context metasenv hety s ugraph in (hete,hety),subst,metasenv,ugraph1 (* {{{ we search a coercion from hety to s if fails *) with RefineFailure _ | Uncertain _ as exn when allow_coercions && !insert_coercions -> let coer, tgt_carr = let carr t subst context = CicReduction.whd ~delta:false 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, c_s in (match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> enrich localization_tbl hete (RefineFailure (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*)))) | CoercGraph.NotMetaClosed -> enrich localization_tbl hete (Uncertain (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*)))) | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt (fun c -> try let t = Cic.Appl[c;hete] in let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context t ugraph in let newt, newty, subst, metasenv, ugraph = avoid_double_coercion context subst metasenv ugraph newt tgt_carr in let subst,metasenv,ugraph1 = fo_unif_subst subst context metasenv newhety s ugraph in Some ((newt,newty), subst, metasenv, ugraph) with Uncertain _ | RefineFailure _ -> None) candidates in (match selected with | Some x -> x | None -> enrich localization_tbl hete ~f:(fun _ -> (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*)))) exn)) | exn -> enrich localization_tbl hete ~f:(fun _ -> (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: " ^ Printexc.to_string exn))) exn (* }}} end coercion stuff *) in eat_prods_and_args pristinemenv metasenv subst context pristinehe he (CicSubstitution.subst (fst arg) t) ugraph1 (newargs@[arg]) tl | _ -> try let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = fix_arity pristinemenv context subst he hetype (newargs@[hete,hety]@tl) ugraph in eat_prods_and_args metasenv metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) more_args_than_expected localization_tbl subst he context hetype args_bo_and_ty exn (* }}} *) 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 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 *) try fix_arity metasenv context subst he hetype args_bo_and_ty ugraph with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) more_args_than_expected localization_tbl subst he context hetype args_bo_and_ty exn in let coerced_args,subst,metasenv,he,t,ugraph = eat_prods_and_args metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty in he,(List.map fst coerced_args),t,subst,metasenv,ugraph 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 (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) -> 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 = 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' ~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 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,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,dest) -> let ctx' = Some (name,(C.Def (so,None)))::ctx in C.LetIn (name, merge_coercions ctx so, 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 (* prerr_endline "CANDIDATO!!!!"; *) if b then let ugraph = CicUniv.empty_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 _ -> prerr_endline (CicPp.ppterm t); 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_obj obj = 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 = 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 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: *)