X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=ed14180aa670c7f41c6f8f28706ef53db6b4b419;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=eb084204cc3adca745d143fe3f591d39e1fd4adb;hpb=f2163ee9bd4011de2bdaf047d357e135736dfdec;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index eb084204c..ed14180aa 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -11,2188 +11,722 @@ (* $Id$ *) -(* -open Printf - -exception RefineFailure of string Lazy.t;; -exception Uncertain of string Lazy.t;; +exception RefineFailure of (Stdpp.location * string) Lazy.t;; +exception Uncertain of (Stdpp.location * 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;; +module C = NCic +module Ref = NReference -let insert_coercions = ref true -let pack_coercions = ref true +let indent = ref "";; +let inside c = indent := !indent ^ String.make 1 c;; +let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -let debug = false;; -let debug_print = - if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ());; +let pp s = + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; -let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" +let pp _ = ();; -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 wrap_exc msg = function + | NCicUnification.Uncertain _ -> Uncertain msg + | NCicUnification.UnificationFailure _ -> RefineFailure msg + | NCicTypeChecker.TypeCheckerFailure _ -> RefineFailure msg + | e -> raise e ;; -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) +let exp_implicit metasenv context expty = + let foo x = match expty with Some t -> `WithType t | None -> x in + function + | `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term) + | `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type) + | `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term) | _ -> assert false ;; -let is_a_double_coercion t = - let rec subst_nth n x l = - match n,l with - | _, [] -> [] - | 0, _::tl -> x :: tl - | n, hd::tl -> hd :: subst_nth (n-1) x tl - in - let imp = Cic.Implicit None in - let dummyres = false,imp, imp,imp,imp in - match t with - | Cic.Appl l1 -> - (match CoercGraph.coerced_arg l1 with - | Some (Cic.Appl l2, pos1) -> - (match CoercGraph.coerced_arg l2 with - | Some (x, pos2) -> - true, List.hd l1, List.hd l2, x, - Cic.Appl (subst_nth (pos1 + 1) - (Cic.Appl (subst_nth (pos2+1) imp l2)) l1) - | _ -> dummyres) - | _ -> 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' +let check_allowed_sort_elimination hdb localise r orig = + let mkapp he arg = + match he with + | C.Appl l -> C.Appl (l @ [arg]) + | t -> C.Appl [t;arg] in + (* ctx, ind_type @ lefts, sort_of_ind_ty@lefts, outsort *) + let rec aux metasenv subst context ind arity1 arity2 = + (*D*)inside 'S'; try let rc = + let arity1 = NCicReduction.whd ~subst context arity1 in + pp (lazy(NCicPp.ppterm ~subst ~metasenv ~context arity1 ^ " elimsto " ^ + NCicPp.ppterm ~subst ~metasenv ~context arity2 ^ "\nMENV:\n"^ + NCicPp.ppmetasenv ~subst metasenv)); + match arity1 with + | C.Prod (name,so1,de1) (* , t ==?== C.Prod _ *) -> + let metasenv, _, meta, _ = + NCicMetaSubst.mk_meta metasenv ((name,C.Decl so1)::context) `Type in - metasenv,Cic.Meta (idx, irl) - | (_,argty)::tl -> - let (metasenv, idx) = - CicMkImplicit.mk_implicit_type metasenv subst context' + let metasenv, subst = + try NCicUnification.unify hdb metasenv subst context + arity2 (C.Prod (name, so1, meta)) + with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf + "expected %s, found %s" (* XXX localizzare meglio *) + (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod (name, so1, meta))) + (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc) in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context' + aux metasenv subst ((name, C.Decl so1)::context) + (mkapp (NCicSubstitution.lift 1 ind) (C.Rel 1)) de1 meta + | C.Sort _ (* , t ==?== C.Prod _ *) -> + let metasenv, _, meta, _ = NCicMetaSubst.mk_meta metasenv [] `Type in + let metasenv, subst = + try NCicUnification.unify hdb metasenv subst context + arity2 (C.Prod ("_", ind, meta)) + with exc -> raise (wrap_exc (lazy (localise orig, Printf.sprintf + "expected %s, found %s" (* XXX localizzare meglio *) + (NCicPp.ppterm ~subst ~metasenv ~context (C.Prod ("_", ind, meta))) + (NCicPp.ppterm ~subst ~metasenv ~context arity2))) exc) 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 + (try NCicTypeChecker.check_allowed_sort_elimination + ~metasenv ~subst r context ind arity1 arity2; + metasenv, subst + with exc -> raise (wrap_exc (lazy (localise orig, + "Sort elimination not allowed ")) exc)) + | _ -> assert false + (*D*)in outside(); rc with exc -> outside (); raise exc 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 = 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 (_,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")) + aux +;; -and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t - ugraph +let rec typeof hdb + ?(localise=fun _ -> Stdpp.dummy_loc) + ~look_for_coercion metasenv subst context term expty = - 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 (C.CProp 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 (C.Prop|C.Set) -> - 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, - outtypeinstance::outtypeinstances,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.oblivion_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 + let force_ty skip_lambda metasenv subst context orig t infty expty = + (*D*)inside 'F'; try let rc = + match expty with + | Some expty -> + (match t with + | C.Implicit _ -> assert false + | C.Lambda _ when skip_lambda -> metasenv, subst, t, expty + | _ -> + pp (lazy ( + (NCicPp.ppterm ~metasenv ~subst ~context infty) ^ " === " ^ + (NCicPp.ppterm ~metasenv ~subst:[] ~context expty))); + try + let metasenv, subst = + NCicUnification.unify hdb metasenv subst context infty expty 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.head_beta_reduce ~delta:false - ~upto:(List.length args) 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 + metasenv, subst, t, expty + with exc -> + try_coercions hdb ~look_for_coercion ~localise + metasenv subst context t orig infty expty true exc) + | None -> metasenv, subst, t, infty + (*D*)in outside(); rc with exc -> outside (); raise exc + in + let rec typeof_aux metasenv subst context expty = + fun t as orig -> + (*D*)inside 'R'; try let rc = + pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t)); + pp (lazy (if expty = None then "NONE" else "SOME")); + if (List.exists (fun (i,_) -> i=29) subst) then + pp (lazy (NCicPp.ppsubst ~metasenv subst)); + let metasenv, subst, t, infty = + match t with + | C.Rel n -> + let infty = + (try + match List.nth context (n - 1) with + | (_,C.Decl ty) -> NCicSubstitution.lift n ty + | (_,C.Def (_,ty)) -> NCicSubstitution.lift n ty + with Failure _ -> + raise (RefineFailure (lazy (localise t,"unbound variable")))) + in + metasenv, subst, t, infty + | C.Sort (C.Type [false,u]) -> metasenv,subst,t,(C.Sort (C.Type [true, u])) + | C.Sort (C.Type _) -> + raise (AssertFailure (lazy ("Cannot type an inferred type: "^ + NCicPp.ppterm ~subst ~metasenv ~context t))) + | C.Sort _ -> metasenv,subst,t,(C.Sort (C.Type NCicEnvironment.type0)) + | C.Implicit infos -> + let metasenv,_,t,ty = exp_implicit metasenv context expty infos in + metasenv, subst, t, ty + | C.Meta (n,l) as t -> + let ty = + try + let _,_,_,ty = NCicUtils.lookup_subst n subst in ty + with NCicUtils.Subst_not_found _ -> try + let _,_,ty = NCicUtils.lookup_meta n metasenv in + match ty with C.Implicit _ -> + prerr_endline (string_of_int n); + prerr_endline (NCicPp.ppmetasenv ~subst metasenv); + prerr_endline (NCicPp.ppsubst ~metasenv subst); + assert false | _ -> ty + with NCicUtils.Meta_not_found _ -> + raise (AssertFailure (lazy (Printf.sprintf + "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t)))) + in + metasenv, subst, t, NCicSubstitution.subst_meta l ty + | C.Const _ -> + metasenv, subst, t, NCicTypeChecker.typeof ~subst ~metasenv context t + | C.Prod (name,(s as orig_s),(t as orig_t)) -> + let metasenv, subst, s, s1 = typeof_aux metasenv subst context None s in + let metasenv, subst, s, s1 = + force_to_sort hdb ~look_for_coercion + metasenv subst context s orig_s localise s1 in + let context1 = (name,(C.Decl s))::context in + let metasenv, subst, t, s2 = typeof_aux metasenv subst context1 None t in + let metasenv, subst, t, s2 = + force_to_sort hdb ~look_for_coercion + metasenv subst context1 t orig_t localise s2 in + let metasenv, subst, s, t, ty = + sort_of_prod localise metasenv subst + context orig_s orig_t (name,s) t (s1,s2) + in + metasenv, subst, NCic.Prod(name,s,t), ty + | C.Lambda (n,(s as orig_s),t) as orig -> + let exp_s, exp_ty_t, force_after = + match expty with + | None -> None, None, false + | Some expty -> + match NCicReduction.whd ~subst context expty with + | C.Prod (_,s,t) -> Some s, Some t, false + | _ -> None, None, true + in + let metasenv, subst, s, ty_s = + typeof_aux metasenv subst context None s in + let metasenv, subst, s, _ = + force_to_sort hdb ~look_for_coercion + metasenv subst context s orig_s localise ty_s in + let (metasenv,subst), exp_ty_t = + match exp_s with + | Some exp_s -> + (try NCicUnification.unify hdb metasenv subst context s exp_s,exp_ty_t + with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf + "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv + ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context + exp_s))) exc)) + | None -> (metasenv, subst), None + in + let context_for_t = (n,C.Decl s) :: context in + let metasenv, subst, t, ty_t = + typeof_aux metasenv subst context_for_t exp_ty_t t + in + if force_after then + force_ty false metasenv subst context orig + (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty + else + metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t) + | C.LetIn (n,(ty as orig_ty),t,bo) -> + let metasenv, subst, ty, ty_ty = + typeof_aux metasenv subst context None ty in + let metasenv, subst, ty, _ = + force_to_sort hdb ~look_for_coercion + metasenv subst context ty orig_ty localise ty_ty in + let metasenv, subst, t, _ = + typeof_aux metasenv subst context (Some ty) t in + let context1 = (n, C.Def (t,ty)) :: context in + let metasenv, subst, bo, bo_ty = + typeof_aux metasenv subst context1 None bo + in + let bo_ty = NCicSubstitution.subst ~avoid_beta_redexes:true t bo_ty in + metasenv, subst, C.LetIn (n, ty, t, bo), bo_ty + | C.Appl ((he as orig_he)::(_::_ as args)) -> + let upto = + match orig_he with C.Meta _ -> List.length args | _ -> 0 + in + let metasenv, subst, he, ty_he = + typeof_aux metasenv subst context None he in + let metasenv, subst, t, ty = + eat_prods hdb ~localise ~look_for_coercion + metasenv subst context orig_he he ty_he args + in + let t = if upto > 0 then NCicReduction.head_beta_reduce ~upto t else t in + metasenv, subst, t, ty + | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2")) + | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r, + outtype,(term as orig_term),pl) as orig -> + let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in + let _, _, arity, cl = List.nth itl tyno in + let constructorsno = List.length cl in + let _, metasenv, args = + NCicMetaSubst.saturate metasenv subst context arity 0 in + let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in + let metasenv, subst, term, _ = + typeof_aux metasenv subst context (Some ind) term in + let parameters, arguments = HExtlib.split_nth leftno args in + let outtype = + match outtype with + | C.Implicit _ as ot -> + let rec aux = function + | [] -> NCic.Lambda ("_",NCic.Implicit `Type,ot) + | _::tl -> NCic.Lambda ("_",NCic.Implicit `Type,aux tl) 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) + aux arguments + | _ -> outtype + in + let metasenv, subst, outtype, outsort = + typeof_aux metasenv subst context None outtype in + + (* next lines are to do a subst-expansion of the outtype, so + that when it becomes a beta-abstraction, the beta-redex is + fired during substitution *) + (*CSC: this is instantiate! should we move it from tactics to the + refiner? I think so! *) + let metasenv,metanoouttype,newouttype,metaoutsort = + NCicMetaSubst.mk_meta metasenv context `Term in + let metasenv,subst = + NCicUnification.unify hdb metasenv subst context outsort metaoutsort in + let metasenv = + List.filter (function (j,_) -> j <> metanoouttype) metasenv in + let subst = + (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in + let outtype = newouttype in + + (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) + let ind = + if parameters = [] then C.Const r + else C.Appl ((C.Const r)::parameters) in + let metasenv, subst, ind, ind_ty = + typeof_aux metasenv subst context None ind in + let metasenv, subst = + check_allowed_sort_elimination hdb localise r orig_term metasenv subst + context ind ind_ty outsort 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 || s2 = C.Set) -> - (* 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.CProp t1), C.Sort (C.CProp 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.CProp t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort (C.Type t1), C.Sort (C.CProp 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.CProp t'),subst,metasenv,ugraph2 - with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | (C.Sort (C.CProp 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.Sort _,C.Sort (C.CProp t1)) -> - C.Sort (C.CProp 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 - (* instead of a dummy functional type we may create the real product - * using args_bo_and_ty, but since coercions lookup ignores the - * actual ariety we opt for the simple solution *) - let fty = Cic.Prod(Cic.Anonymous, Cic.Sort Cic.Prop, Cic.Sort Cic.Prop) in - match CoercGraph.look_for_coercion metasenv subst context hetype fty with - | CoercGraph.NoCoercion -> [] - | 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) + (* let's check if the type of branches are right *) + if List.length pl <> constructorsno then + raise (RefineFailure (lazy (localise orig, + "Wrong number of cases in a match"))); +(* + let metasenv, subst = + match expty with + | None -> metasenv, subst + | Some expty -> + NCicUnification.unify hdb metasenv subst context resty expty + in +*) + let _, metasenv, subst, pl_rev = + List.fold_left + (fun (j, metasenv, subst, branches) p -> + let cons = + let cons = Ref.mk_constructor j r in + if parameters = [] then C.Const cons + else C.Appl (C.Const cons::parameters) 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 + let metasenv, subst, cons, ty_cons = + typeof_aux metasenv subst context None cons in + let ty_branch = + NCicTypeChecker.type_of_branch + ~subst context leftno outtype cons ty_cons in + pp (lazy ("TYPEOFBRANCH: " ^ + NCicPp.ppterm ~metasenv ~subst ~context p ^ " ::: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ty_branch )); + let metasenv, subst, p, _ = + typeof_aux metasenv subst context (Some ty_branch) p in + j+1, metasenv, subst, p :: branches) + (1, metasenv, subst, []) pl in - match coer with - | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ -> raise (RefineFailure (lazy - "coerce_atom_to_something fails since no coercions found")) - | CoercGraph.NotHandled when - not (CicUtil.is_meta_closed infty) || - not (CicUtil.is_meta_closed expty) -> raise (Uncertain (lazy - "coerce_atom_to_something fails since carriers have metas")) - | 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")) + let resty = C.Appl (outtype::arguments@[term]) in + let resty = NCicReduction.head_beta_reduce ~subst resty in + metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty + | C.Match _ -> assert false 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 + pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ + NCicPp.ppterm ~metasenv ~subst ~context infty )); + force_ty true metasenv subst context orig t infty expty + (*D*)in outside(); rc with exc -> outside (); raise exc + in + typeof_aux metasenv subst context expty term + +and try_coercions hdb + ~localise ~look_for_coercion + metasenv subst context t orig_t infty expty perform_unification exc += + (* we try with a coercion *) + let rec first exc = function + | [] -> + raise (wrap_exc (lazy (localise orig_t, Printf.sprintf + "The term %s has type %s but is here used with type %s" + (NCicPp.ppterm ~metasenv ~subst ~context t) + (NCicPp.ppterm ~metasenv ~subst ~context infty) + (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) + | (metasenv, newterm, newtype, meta)::tl -> + try + pp (lazy ( "UNIFICATION in CTX:\n"^ + NCicPp.ppcontext ~metasenv ~subst context + ^ "\nMENV: " ^ + NCicPp.ppmetasenv metasenv ~subst + ^ "\nOF: " ^ + NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n")); + let metasenv, subst = + NCicUnification.unify hdb metasenv subst context meta t 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 _ | Cic.Meta _) as mty,_ -> [], mty - | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ -> - snd (HExtlib.split_nth leftno args), mty - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> - raise (AssertFailure(lazy "already ill-typed matched term")) - 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) + pp (lazy ( "UNIFICATION in CTX:\n"^ + NCicPp.ppcontext ~metasenv ~subst context + ^ "\nMENV: " ^ + NCicPp.ppmetasenv metasenv ~subst + ^ "\nOF: " ^ + NCicPp.ppterm ~metasenv ~subst ~context newtype ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context expty ^ "\n")); + let metasenv, subst = + if perform_unification then + NCicUnification.unify hdb metasenv subst context newtype expty + else metasenv, subst + in + metasenv, subst, newterm, newtype + with + | NCicUnification.UnificationFailure _ -> first exc tl + | NCicUnification.Uncertain _ as exc -> first exc tl + in + first exc + (look_for_coercion metasenv subst context infty expty) + +and force_to_sort hdb + ~look_for_coercion metasenv subst context t orig_t localise ty += + match NCicReduction.whd ~subst context ty with + | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> + metasenv, subst, t, ty + | C.Meta (i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ??? + metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *) + | C.Meta (i,(_,lc)) -> + let len = match lc with C.Irl len->len | C.Ctx l->List.length l in + let metasenv, subst, newmeta = + if len > 0 then + NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1)) + else metasenv, subst, i + in + metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0)) + | C.Sort _ as ty -> metasenv, subst, t, ty + | ty -> + try_coercions hdb ~localise ~look_for_coercion metasenv subst context + t orig_t ty (NCic.Sort (NCic.Type NCicEnvironment.type0)) false + (Uncertain (lazy (localise orig_t, + "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t + ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty))) + +and sort_of_prod + localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) += + (* force to sort is done in the Prod case in typeof *) + match t1, t2 with + | C.Sort _, C.Sort C.Prop -> metasenv, subst, s, t, t2 + | C.Sort (C.Type u1), C.Sort (C.Type u2) -> + metasenv, subst, s, t, C.Sort (C.Type (NCicEnvironment.max u1 u2)) + | C.Sort C.Prop,C.Sort (C.Type _) -> metasenv, subst, s, t, t2 + | C.Meta _, C.Sort _ + | C.Meta _, C.Meta (_,(_,_)) + | C.Sort _, C.Meta (_,(_,_)) -> metasenv, subst, s, t, t2 + | x, (C.Sort _ | C.Meta _) | _, x -> + let y, context, orig = + if x == t1 then s, context, orig_s + else t, ((name,C.Decl s)::context), orig_t in - enrich localization_tbl ~f t exn + raise (RefineFailure (lazy (localise orig,Printf.sprintf + "%s is expected to be a type, but its type is %s that is not a sort" + (NCicPp.ppterm ~subst ~metasenv ~context y) + (NCicPp.ppterm ~subst ~metasenv ~context x)))) - 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 = - if clean_dummy_dependent_types then - FreshNamesGenerator.clean_dummy_dependent_types substituted_t - else substituted_t in - let cleaned_ty = - if clean_dummy_dependent_types then - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty - else substituted_ty in - let cleaned_metasenv = - if clean_dummy_dependent_types then - 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 - else - substituted_metasenv +and eat_prods hdb + ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args += + (*D*)inside 'E'; try let rc = + let rec aux metasenv subst args_so_far he ty_he = function + | []->metasenv, subst, NCicUntrusted.mk_appl he (List.rev args_so_far), ty_he + | arg::tl -> + match NCicReduction.whd ~subst context ty_he with + | C.Prod (_,s,t) -> + let metasenv, subst, arg, _ = + typeof hdb ~look_for_coercion ~localise + metasenv subst context arg (Some s) in + let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in + aux metasenv subst (arg :: args_so_far) he t tl + | C.Meta _ + | C.Appl (C.Meta _ :: _) as t -> + let metasenv, subst, arg, ty_arg = + typeof hdb ~look_for_coercion ~localise + metasenv subst context arg None in + let metasenv, _, meta, _ = + NCicMetaSubst.mk_meta metasenv + (("_",C.Decl ty_arg) :: context) `Type + in + let flex_prod = C.Prod ("_", ty_arg, meta) in + (* next line grants that ty_args is a type *) + let metasenv,subst, flex_prod, _ = + typeof hdb ~look_for_coercion ~localise metasenv subst + context flex_prod None in + pp (lazy ( "UNIFICATION in CTX:\n"^ + NCicPp.ppcontext ~metasenv ~subst context + ^ "\nOF: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context flex_prod ^ "\n")); + let metasenv, subst = + try NCicUnification.unify hdb metasenv subst context t flex_prod + with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf + ("The term %s has an inferred type %s, but is applied to the" ^^ + " argument %s of type %s") + (NCicPp.ppterm ~metasenv ~subst ~context he) + (NCicPp.ppterm ~metasenv ~subst ~context t) + (NCicPp.ppterm ~metasenv ~subst ~context arg) + (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc) + (* XXX coerce to funclass *) + in + let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in + aux metasenv subst (arg :: args_so_far) he meta tl + | C.Match (_,_,C.Meta _,_) + | C.Match (_,_,C.Appl (C.Meta _ :: _),_) + | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) -> + raise (Uncertain (lazy (localise orig_he, Printf.sprintf + ("The term %s is here applied to %d arguments but expects " ^^ + "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) + (List.length args) (List.length args_so_far)))) + | ty -> + let metasenv, subst, newhead, newheadty = + try_coercions hdb ~localise ~look_for_coercion metasenv subst context + (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty + (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) + false + (RefineFailure (lazy (localise orig_he, Printf.sprintf + ("The term %s is here applied to %d arguments but expects " ^^ + "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he) + (List.length args) (List.length args_so_far)))) + in + aux metasenv subst [] newhead newheadty (arg :: tl) in - (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) + aux metasenv subst [] he ty_he args + (*D*)in outside(); rc with exc -> outside (); raise exc ;; -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.oblivion_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 = - (* clean_dummy_dependent_types: false to avoid cleaning the names - of the left products, that must be identical to those of the - constructors; however, non-left products should probably be - cleaned *) - type_of_aux' ~clean_dummy_dependent_types:false ~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 +let rec first f l1 l2 = + match l1,l2 with + | x1::tl1, x2::tl2 -> + (try f x1 x2 with Not_found -> first f tl1 tl2) + | _ -> raise Not_found ;; -(* 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 rec find add dt t = + if dt == add then t + else + let dl, l = + match dt, t with + | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l)) + | C.Appl dl,C.Appl l -> dl,l + | C.Lambda (_,ds,dt), C.Lambda (_,s,t) + | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t] + | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t] + | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l) + | _ -> raise Not_found + in + first (find add) dl l ;; -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 relocalise old_localise dt t add = + old_localise + (try find add dt t with Not_found -> assert false) ;; -let pack_coercion_obj obj = obj (* +let undebruijnate inductive ref t rev_fl = + NCicSubstitution.psubst (fun x -> x) + (List.rev (HExtlib.list_mapi + (fun (_,_,rno,_,_,_) i -> + NCic.Const + (if inductive then NReference.mk_fix i rno ref + else NReference.mk_cofix i ref)) + rev_fl)) + t +;; - 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) +let typeof_obj hdb + ?(localise=fun _ -> Stdpp.dummy_loc) + ~look_for_coercion (uri,height,metasenv,subst,obj) += +prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj)); + let check_type metasenv subst context (ty as orig_ty) = (* XXX fattorizza *) + let metasenv, subst, ty, sort = + typeof hdb ~localise ~look_for_coercion metasenv subst context ty None + in + let metasenv, subst, ty, sort = + force_to_sort hdb ~look_for_coercion + metasenv subst context ty orig_ty localise sort + in + metasenv, subst, ty, sort + in + match obj with + | C.Constant (relevance, name, bo, ty , attr) -> + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in + let metasenv, subst, bo, ty, height = + match bo with + | Some bo -> + let metasenv, subst, bo, ty = + typeof hdb ~localise ~look_for_coercion + metasenv subst [] bo (Some ty) + in + let height = (* XXX recalculate *) height in + metasenv, subst, Some bo, ty, height + | None -> metasenv, subst, None, ty, 0 + in + uri, height, metasenv, subst, + C.Constant (relevance, name, bo, ty, attr) + | C.Fixpoint (inductive, fl, attr) -> + let len = List.length fl in + let types, metasenv, subst, rev_fl = + List.fold_left + (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) -> + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in + let dbo = NCicTypeChecker.debruijn uri len [] bo in + let localise = relocalise localise dbo bo in + (name,C.Decl ty)::types, + metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl + ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *) 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) + let metasenv, subst, fl = + List.fold_left + (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) -> + let metasenv, subst, dbo, ty = + typeof hdb ~localise ~look_for_coercion + metasenv subst types dbo (Some ty) + in + metasenv, subst, (relevance,name,k,ty,dbo)::fl) + (metasenv, subst, []) rev_fl 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 = + let height = (* XXX recalculate *) height in + let fl = 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 + (fun (relevance,name,k,ty,dbo) -> + let bo = + undebruijnate inductive + (NReference.reference_of_spec uri + (if inductive then NReference.Fix (0,k,0) + else NReference.CoFix 0)) dbo rev_fl + in + relevance,name,k,ty,bo) + fl in - C.InductiveDefinition (indtys, params, leftno, attrs) *) + uri, height, metasenv, subst, + C.Fixpoint (inductive, fl, attr) + | C.Inductive (ind, leftno, itl, attr) -> + let len = List.length itl in + let metasenv,subst,rev_itl,tys = + List.fold_left + (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) -> + let metasenv, subst, ty, _ = check_type metasenv subst [] ty in + metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx + ) (metasenv,subst,[],[]) itl in + let metasenv,subst,itl,_ = + List.fold_left + (fun (metasenv,subst,res,i) (it_relev,n,ty,cl) -> + let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in + let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in + let metasenv,subst,cl = + List.fold_right + (fun (k_relev,n,te) (metasenv,subst,res) -> + let k_relev = + try snd (HExtlib.split_nth leftno k_relev) + with Failure _ -> k_relev in + let te = NCicTypeChecker.debruijn uri len [] te in + let metasenv, subst, te, _ = check_type metasenv subst tys te in + let context,te = NCicReduction.split_prods ~subst tys leftno te in + let _,chopped_context_rev = + HExtlib.split_nth (List.length tys) (List.rev context) in + let sx_context_te_rev,_ = + HExtlib.split_nth leftno chopped_context_rev in + let metasenv,subst,_ = + try + List.fold_left2 + (fun (metasenv,subst,context) item1 item2 -> + let (metasenv,subst),convertible = + try + match item1,item2 with + (n1,C.Decl ty1),(n2,C.Decl ty2) -> + if n1 = n2 then + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context ty1 ty2,true + else + (metasenv,subst),false + | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> + if n1 = n2 then + let metasenv,subst = + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context ty1 ty2 + in + NCicUnification.unify hdb ~test_eq_only:true metasenv + subst context bo1 bo2,true + else + (metasenv,subst),false + | _,_ -> (metasenv,subst),false + with + | NCicUnification.Uncertain _ + | NCicUnification.UnificationFailure _ -> + (metasenv,subst),false + in + let term2 = + match item2 with + _,C.Decl t -> t + | _,C.Def (b,_) -> b in + if not convertible then + raise (RefineFailure (lazy (localise term2, + ("Mismatch between the left parameters of the constructor " ^ + "and those of its inductive type")))) + else + metasenv,subst,item1::context + ) (metasenv,subst,[]) sx_context_ty_rev sx_context_te_rev + with Invalid_argument "List.fold_left2" -> assert false in + let con_sort= NCicTypeChecker.typeof ~subst ~metasenv context te in + (match + NCicReduction.whd ~subst context con_sort, + NCicReduction.whd ~subst [] ty_sort + with + (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> + if not (NCicEnvironment.universe_leq u1 u2) then + raise + (RefineFailure + (lazy(localise te, "The type " ^ + NCicPp.ppterm ~metasenv ~subst ~context s1 ^ + " of the constructor is not included in the inductive"^ + " type sort " ^ + NCicPp.ppterm ~metasenv ~subst ~context s2))) + | C.Sort _, C.Sort C.Prop + | C.Sort _, C.Sort C.Type _ -> () + | _, _ -> + raise + (RefineFailure + (lazy (localise te, + "Wrong constructor or inductive arity shape")))); + (* let's check also the positivity conditions *) + if + not + (NCicTypeChecker.are_all_occurrences_positive + ~subst context uri leftno (i+leftno) leftno (len+leftno) te) + then + raise + (RefineFailure + (lazy (localise te, + "Non positive occurence in " ^ NUri.string_of_uri uri))) + else + let relsno = List.length itl + leftno in + let te = + NCicSubstitution.psubst + (fun i -> + if i <= leftno then + NCic.Rel i + else + NCic.Const (NReference.reference_of_spec uri + (NReference.Ind (ind,relsno - i,leftno)))) + (HExtlib.list_seq 1 (relsno+1)) + te in + let te = + List.fold_right + (fun (name,decl) te -> + match decl with + NCic.Decl ty -> NCic.Prod (name,ty,te) + | NCic.Def (bo,ty) -> NCic.LetIn (name,ty,bo,te) + ) sx_context_te_rev te + in + metasenv,subst,(k_relev,n,te)::res + ) cl (metasenv,subst,[]) + in + metasenv,subst,(it_relev,n,ty,cl)::res,i+1 + ) (metasenv,subst,[],1) rev_itl + in + uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr) ;; - -(* 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: *) -*)