X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b535b9ebe987677505d7d9b40a2c59731a4c2606;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=1242a1cded879cb24a21c7d3be344f34a8228d1b;hpb=5f18d404d23d75d47b018631cc05221ccd2d2b1b;p=helm.git diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 1242a1cde..b535b9ebe 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -31,6 +31,9 @@ exception RefineFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; +(* for internal use only; the integer is the number of surplus arguments *) +exception MoreArgsThanExpected of int * exn;; + let insert_coercions = ref true let pack_coercions = ref true @@ -88,7 +91,7 @@ let enrich localization_tbl t ?(f = fun msg -> msg) exn = try Cic.CicHash.find localization_tbl t with Not_found -> - prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); + HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm t); raise exn' in raise (HExtlib.Localized (loc,exn')) @@ -128,41 +131,58 @@ let exp_impl metasenv subst context = | _ -> assert false ;; +let unvariant newt = + match newt with + | Cic.Appl (hd::args) -> + let uri = CicUtil.uri_of_term hd in + (match + CicEnvironment.get_obj CicUniv.oblivion_ugraph uri + with + | Cic.Constant (_,Some t,_,[],attrs),_ + when List.exists ((=) (`Flavour `Variant)) attrs -> + Cic.Appl (t::args) + | _ -> newt) + | _ -> newt +;; + let is_a_double_coercion t = - let last_of l = - let rec aux acc = function - | x::[] -> acc,x - | x::tl -> aux (acc@[x]) tl - | [] -> assert false - in - aux [] l + 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 (c1::tl) when CoercDb.is_a_coercion' c1 -> - (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> - let sib2,head = last_of tl2 in - true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl - (c2::sib2@[imp])]) + | 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' tlbody_and_type exn +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 (List.length tlbody_and_type) ^ - " arguments that are more than expected") + " (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 mk_prod_of_metas metasenv context subst args = let rec mk_prod metasenv context' = function | [] -> let (metasenv, idx) = @@ -187,14 +207,11 @@ let mk_prod_of_metas metasenv context' subst args = (* then I generate a name --- using the hint name_hint *) (* --- that is fresh in context'. *) let name_hint = - (* Cic.Name "pippo" *) FreshNamesGenerator.mk_fresh_name ~subst metasenv - (* (CicMetaSubst.apply_subst_metasenv subst metasenv) *) - (CicMetaSubst.apply_subst_context subst context') + (CicMetaSubst.apply_subst_context subst context) Cic.Anonymous ~typ:(CicMetaSubst.apply_subst subst argty) in - (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *) FreshNamesGenerator.mk_fresh_name ~subst [] context' name_hint ~typ:(Cic.Sort Cic.Prop) in @@ -203,7 +220,7 @@ let mk_prod_of_metas metasenv context' subst args = in metasenv,Cic.Prod (name,meta,target) in - mk_prod metasenv context' args + mk_prod metasenv context args ;; let rec type_of_constant uri ugraph = @@ -294,7 +311,6 @@ and type_of_mutual_inductive_constr uri i j ugraph = and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph = let module C = Cic in - (* let module R = CicMetaSubst in *) let module R = CicReduction in match R.whd ~subst context expectedtype with C.MutInd (_,_,_) -> @@ -302,7 +318,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt | C.Appl (C.MutInd (_,_,_)::tl) -> let (_,arguments) = split tl left_args_no in (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph - | C.Prod (name,so,de) -> + | 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 @@ -316,33 +332,18 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* 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) + ((Some (name',(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1 | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) -and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t - ugraph +and type_of_aux' ?(clean_dummy_dependent_types=true) + ?(localization_tbl = Cic.CicHash.create 1) metasenv subst context t ugraph = let rec type_of_aux subst metasenv context t ugraph = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in -(* - let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) = - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last t ugraph - in - try - let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph coerced - coercion_tgt - in - Some (newt, tty, subst, metasenv, ugraph) - with - | RefineFailure _ | Uncertain _ -> None - in -*) let (t',_,_,_,_) as res = match t with (* function *) @@ -351,15 +352,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t match List.nth context (n - 1) with Some (_,C.Decl ty) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (_,Some ty)) -> + | Some (_,C.Def (_,ty)) -> t,S.lift n ty,subst,metasenv, ugraph - | Some (_,C.Def (bo,None)) -> - let ty,ugraph = - (* if it is in the context it must be already well-typed*) - CicTypeChecker.type_of_aux' ~subst metasenv context - (S.lift n bo) ugraph - in - t,ty,subst,metasenv,ugraph | None -> enrich localization_tbl t (RefineFailure (lazy "Rel to hidden hypothesis")) @@ -406,7 +400,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 with CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)) - | C.Sort _ -> + | 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 @@ -418,6 +419,37 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in + let rec count_prods context ty = + match CicReduction.whd context ~subst:subst'' ty with + | Cic.Prod (n,s,t) -> + 1 + count_prods (Some (n,Cic.Decl s)::context) t + | _ -> 0 + in + let exp_prods = count_prods context ty' in + let inf_prods = count_prods context inferredty in + let te', inferredty, metasenv'', subst'', ugraph2 = + let rec aux t m s ug it = function + | 0 -> t,it,m,s,ug + | n -> + match CicReduction.whd context ~subst:s it with + | Cic.Prod (_,src,tgt) -> + let newmeta, metaty, s, m, ug = + type_of_aux s m context (Cic.Implicit None) ug + in + let s,m,ug = + fo_unif_subst s context m metaty src ug + in + let t = + match t with + | Cic.Appl l -> Cic.Appl (l @ [newmeta]) + | _ -> Cic.Appl [t;newmeta] + in + aux t m s ug (CicSubstitution.subst newmeta tgt) (n-1) + | _ -> t,it,m,s,ug + in + aux te' metasenv'' subst'' ugraph2 inferredty + (max 0 (inf_prods - exp_prods)) + in let (te', ty'), subst''',metasenv''',ugraph3 = coerce_to_something true localization_tbl te' inferredty ty' subst'' metasenv'' context ugraph2 @@ -459,12 +491,29 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 - | C.LetIn (n,s,t) -> - (* only to check if s is well-typed *) - let s',ty,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in + | 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 ("(2) 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' @@ -474,7 +523,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t * Even faster than the previous solution. * Moreover the inferred type is closer to the expected one. *) - C.LetIn (n,s',t'), + C.LetIn (n,s',ty,t'), CicSubstitution.subst ~avoid_beta_redexes:true s' inferredty, subst'',metasenv'',ugraph2 | C.Appl (he::((_::_) as tl)) -> @@ -538,6 +587,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (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) @@ -578,12 +631,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl term' exn ~f:(function _ -> - lazy ("(10)The term " ^ + lazy ("(3) 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)) + CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' + context)) in let rec instantiate_prod t = function @@ -623,7 +677,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl constructor' ~f:(fun _ -> - lazy ("(11)The term " ^ + lazy ("(4) The term " ^ CicMetaSubst.ppterm_in_context metasenv subst p' context ^ " has type " ^ CicMetaSubst.ppterm_in_context metasenv subst actual_type @@ -632,7 +686,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t context)) exn in (p'::pl,j-1, - outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3)) + outtypeinstance::outtypeinstances,subst,metasenv,ugraph3)) pl ([],List.length pl,[],subst,metasenv,ugraph3) in @@ -649,7 +703,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (let candidate,ugraph5,metasenv,subst = let exp_name_subst, metasenv = let o,_ = - CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri + CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in let uris = CicUtil.params_of_obj o in List.fold_right ( @@ -801,7 +855,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in C.Appl (outtype'::args) in - CicReduction.whd ~subst context appl + CicReduction.head_beta_reduce ~delta:false + ~upto:(List.length args) appl in try fo_unif_subst subst context metasenv instance instance' @@ -810,19 +865,19 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl p exn ~f:(function _ -> - lazy ("(12)The term " ^ + lazy ("(5) 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 + (subst,metasenv,ugraph5) pl' outtypeinstances in C.MutCase (uri, i, outtype, term', pl'), CicReduction.head_beta_reduce (CicMetaSubst.apply_subst subst - (C.Appl(outtype::right_args@[term]))), + (C.Appl(outtype::right_args@[term']))), subst,metasenv,ugraph6) | C.Fix (i,fl) -> let fl_ty',subst,metasenv,types,ugraph1,len = @@ -851,13 +906,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(13)The term " ^ + lazy ("(7) 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)) + context')) in fl @ [bo'] , subst',metasenv',ugraph' ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') @@ -904,7 +959,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t exn -> enrich localization_tbl bo exn ~f:(function _ -> - lazy ("(14)The term " ^ + lazy ("(8) The term " ^ CicMetaSubst.ppterm_in_context ~metasenv subst bo context' ^ " has type " ^ CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo @@ -949,13 +1004,13 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t [] -> [] | (Some (n,C.Decl t))::tl -> (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) - | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) - | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n, - C.Def ((S.subst_meta l (S.lift i t)), - Some (S.subst_meta l (S.lift i ty))))) :: (aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some + (n, + C.Def + (S.subst_meta l (S.lift i t), + S.subst_meta l (S.lift i ty)))) :: (aux (i+1) tl) in aux 1 canonical_context in @@ -966,11 +1021,27 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t _,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 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 t) (CicMetaSubst.ppterm ~metasenv subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) +(*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) -> @@ -1048,8 +1119,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let t1'' = CicReduction.whd ~subst context t1 in let t2'' = CicReduction.whd ~subst context_for_t2 t2 in match (t1'', t2'') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + | (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)) -> @@ -1060,8 +1130,34 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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 @@ -1109,12 +1205,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | 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 -> + (fun (metasenv,last,c) _ -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv last head ugraph in debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); @@ -1194,33 +1285,37 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in tlbody_and_type,subst,metasenv,ugraph - and eat_prods + 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 exn metasenv context subst he hetype ugraph = + let fix_arity n metasenv context subst he hetype ugraph = let hetype = CicMetaSubst.apply_subst subst hetype in - let src = CoercDb.coerc_carr_of_term hetype in - let tgt = CoercDb.Fun 0 in - match CoercGraph.look_for_coercion' metasenv subst context src tgt with - | CoercGraph.NoCoercion - | CoercGraph.NotMetaClosed - | CoercGraph.NotHandled _ -> raise exn + (* 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 - let subst,metasenv,ugraph = - fo_unif_subst subst context metasenv last he ugraph in - debug_print (lazy ("New head: "^ pp coerc)); try - let t,tty,subst,metasenv,ugraph = - type_of_aux subst metasenv context coerc ugraph in - (*{{{*)debug_print (lazy (" refined: "^ pp t)); - debug_print (lazy (" has type: "^ pp tty));(*}}}*) - Some (t,tty,subst,metasenv,ugraph) + 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 (unvariant coerc,tty,subst,metasenv,ugraph) with | Uncertain _ | RefineFailure _ | HExtlib.Localized (_,Uncertain _) @@ -1254,12 +1349,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il "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 exn = RefineFailure (lazy ("more args than expected")) in + let error = ref None in let possible_fixes = - fix_arity exn metasenv context subst he hetype ugraph in + fix_arity (List.length args) metasenv context subst he hetype + ugraph in match HExtlib.list_findopt - (fun (he,hetype,subst,metasenv,ugraph) -> + (fun (he,hetype,subst,metasenv,ugraph) _ -> (* {{{ *)debug_print (lazy ("Try fix: "^ CicMetaSubst.ppterm_in_context ~metasenv subst he context)); debug_print (lazy (" of type: "^ @@ -1268,13 +1364,21 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il try Some (eat_prods_and_args metasenv subst context he hetype ugraph [] args) - with RefineFailure _ | Uncertain _ -> None) + with + | RefineFailure _ | Uncertain _ + | HExtlib.Localized (_,RefineFailure _) + | HExtlib.Localized (_,Uncertain _) as exn -> + error := Some exn; None) possible_fixes with | Some x -> x | None -> - more_args_than_expected localization_tbl metasenv - subst he context hetype args_bo_and_ty exn + match !error with + None -> + raise + (MoreArgsThanExpected + (List.length args, RefineFailure (lazy ""))) + | Some exn -> raise exn in (* first we check if we are in the simple case of a meta closed term *) let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty = @@ -1296,8 +1400,13 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il 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 @@ -1308,19 +1417,23 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il let module CR = CicReduction in let cs_subst = CS.subst ~avoid_beta_redexes:true in let coerce_atom_to_something t infty expty subst metasenv context ugraph = + debug_print (lazy ("COERCE_ATOM_TO_SOMETHING")); let coer = CoercGraph.look_for_coercion metasenv subst context infty expty in match coer with - | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy - "coerce_atom_to_something fails since not meta closed")) | CoercGraph.NoCoercion - | CoercGraph.SomeCoercionToTgt _ - | CoercGraph.NotHandled _ -> raise (RefineFailure (lazy + | 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")); + debug_print (lazy (string_of_int (List.length candidates) ^ + " candidates found")); let uncertain = ref false in let selected = let posibilities = @@ -1330,21 +1443,32 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* {{{ *) 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 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 + 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) + fo_unif_subst subst context metasenv newhety expty ugraph + in + let b, ugraph = + CicReduction.are_convertible + ~subst ~metasenv context infty expty ugraph + in + if b then + Some ((t,infty), subst, metasenv, ugraph) + else + let newt = unvariant newt in + Some ((newt,newty), subst, metasenv, ugraph) with | Uncertain _ -> uncertain := true; None | RefineFailure _ -> None) @@ -1371,10 +1495,8 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il fo_unif_subst subst context metasenv infty expty ugraph in (t, expty), subst, metasenv, ugraph - with Uncertain _ | RefineFailure _ as exn -> - if not allow_coercions || not !insert_coercions then - enrich localization_tbl t exn - else + 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 @@ -1384,286 +1506,291 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il CicMetaSubst.ppterm_in_context ~metasenv subst t context ^ " : " ^ CicMetaSubst.ppterm_in_context ~metasenv subst infty context ^" ==> "^ CicMetaSubst.ppterm_in_context ~metasenv subst expty context));(*}}}*) - 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 + 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 - 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, + (Cic.Fix (n,[name,i,expty,bo]),expty),subst,metasenv,ugraph + | _ -> assert false (* not implemented yet *)) (*}}}*) + | _,_, Cic.MutCase (uri,tyno,outty,m,pl) -> + (*{{{*) debug_print (lazy "CASE"); + (* {{{ helper functions *) + let get_cl_and_left_p uri tyno outty ugraph = + match CicEnvironment.get_obj ugraph uri with + | Cic.InductiveDefinition (tl, _, leftno, _),ugraph -> + let count_pis t = + let rec aux ctx t = + match CicReduction.whd ~delta:false ctx t with + | Cic.Prod (name,src,tgt) -> + let ctx = Some (name, Cic.Decl src) :: ctx in + 1 + aux ctx tgt + | _ -> 0 + in + aux [] t + in + let rec skip_lambda_delifting t n = + match t,n with + | _,0 -> t + | Cic.Lambda (_,_,t),n -> + skip_lambda_delifting + (CS.subst (Cic.Implicit None) t) (n - 1) + | _ -> assert false + in + let get_l_r_p n = function + | Cic.Lambda (_,Cic.MutInd _,_) -> [],[] + | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) -> + HExtlib.split_nth n args + | _ -> assert false + in + let _, _, ty, cl = List.nth tl tyno in + let pis = count_pis ty in + let rno = pis - leftno in + let t = skip_lambda_delifting outty rno in + let left_p, _ = get_l_r_p leftno t in + let instantiale_with_left cl = + List.map + (fun ty -> + List.fold_left + (fun t p -> match t with + | Cic.Prod (_,_,t) -> + cs_subst p t + | _-> assert false) + ty left_p) + cl + in + let cl = instantiale_with_left (List.map snd cl) in + cl, left_p, leftno, rno, ugraph + | _ -> raise exn + in + let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = + match t,n with + | _,0 -> + let rec mkr n = function + | [] -> [] | _::tl -> Cic.Rel n :: mkr (n+1) tl + in + let bo = + CicReplace.replace_lifting + ~equality:(fun _ -> CicUtil.alpha_equivalence) + ~context:ctx + ~what:(matched::right_p) + ~with_what:(Cic.Rel 1::List.rev (mkr 2 right_p)) + ~where:bo + in + bo + | Cic.Lambda (name, src, tgt),_ -> + Cic.Lambda (name, src, keep_lambdas_and_put_expty (Some (name, Cic.Decl src)::ctx) tgt (CS.lift 1 bo) (List.map (CS.lift 1) right_p) (CS.lift 1 matched) (n-1)) - | _ -> assert false - in - let eq_uri, eq, eq_refl = - match LibraryObjects.eq_URI () with - | None -> HLog.warn "no default equality"; raise exn - | Some u -> u, Cic.MutInd(u,0,[]), Cic.MutConstruct (u,0,1,[]) - in - let add_params - metasenv subst context uri tyno cty outty mty m leftno i - = - let rec aux context outty par k mty m = function - | Cic.Prod (name, src, tgt) -> - let t,k = - aux - (Some (name, Cic.Decl src) :: context) - (CS.lift 1 outty) (Cic.Rel k::par) (k+1) - (CS.lift 1 mty) (CS.lift 1 m) tgt - in - Cic.Prod (name, src, t), k - | Cic.MutInd _ -> - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - if par <> [] then Cic.Appl (k::par) else k - in - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl [outty;k])))),k - | Cic.Appl (Cic.MutInd _::pl) -> - let left_p,right_p = HExtlib.split_nth leftno pl in - let has_rights = right_p <> [] in - let k = - let k = Cic.MutConstruct (uri,tyno,i,[]) in - Cic.Appl (k::left_p@par) - in - let right_p = - try match - CicTypeChecker.type_of_aux' ~subst metasenv context k - CicUniv.oblivion_ugraph - with - | Cic.Appl (Cic.MutInd _::args),_ -> - snd (HExtlib.split_nth leftno args) - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> assert false - in - if has_rights then - CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k])),k - else - Cic.Prod (Cic.Name "p", - Cic.Appl [eq; mty; m; k], - (CS.lift 1 - (CR.head_beta_reduce ~delta:false - (Cic.Appl (outty ::right_p @ [k]))))),k - | _ -> assert false - in - aux context outty [] 1 mty m cty - in - let add_lambda_for_refl_m pbo rno mty m k cty = - (* k lives in the right context *) - if rno <> 0 then pbo else - let rec aux mty m = function - | Cic.Lambda (name,src,bo), Cic.Prod (_,_,ty) -> - Cic.Lambda (name,src, - (aux (CS.lift 1 mty) (CS.lift 1 m) (bo,ty))) - | t,_ -> - Cic.Lambda (Cic.Name "p", - Cic.Appl [eq; mty; m; k],CS.lift 1 t) - in - aux mty m (pbo,cty) - in - let add_pi_for_refl_m new_outty mty m rno = - if rno <> 0 then new_outty else - let rec aux m mty = function - | Cic.Lambda (name, src, tgt) -> - Cic.Lambda (name, src, - aux (CS.lift 1 m) (CS.lift 1 mty) tgt) - | t -> - Cic.Prod - (Cic.Anonymous, Cic.Appl [eq;mty;m;Cic.Rel 1], - CS.lift 1 t) - in - aux m mty new_outty - in (* }}} end helper functions *) - (* constructors types with left params already instantiated *) - let outty = CicMetaSubst.apply_subst subst outty in - let cl, left_p, leftno,rno,ugraph = - get_cl_and_left_p uri tyno outty ugraph - in - let right_p, mty = - try - match - CicTypeChecker.type_of_aux' ~subst metasenv context m - CicUniv.oblivion_ugraph - with - | Cic.MutInd _ as mty,_ -> [], mty - | Cic.Appl (Cic.MutInd _::args) as mty,_ -> - snd (HExtlib.split_nth leftno args), mty - | _ -> assert false - with CicTypeChecker.TypeCheckerFailure _ -> assert false - in - let new_outty = + | _ -> 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 + 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 + ~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 - debug_print (lazy ("coerced: "^ CicMetaSubst.ppterm_in_context - ~metasenv subst coerced context)); - (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 + ~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 " ^ + lazy ("(9) 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 " ^ @@ -1672,16 +1799,20 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il enrich localization_tbl ~f t exn and coerce_to_sort localization_tbl t infty subst context metasenv uragph = - match CicReduction.whd ~subst:subst context infty with + 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 _ = @@ -1697,7 +1828,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* eat prods ends here! *) let t',ty,subst',metasenv',ugraph1 = - type_of_aux [] metasenv context t ugraph + type_of_aux subst metasenv context t ugraph in let substituted_t = CicMetaSubst.apply_subst subst' t' in let substituted_ty = CicMetaSubst.apply_subst subst' ty in @@ -1710,10 +1841,15 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il (* substituted_t,substituted_ty,substituted_metasenv *) (* ANDREA: spostare tutta questa robaccia da un altra parte *) let cleaned_t = - FreshNamesGenerator.clean_dummy_dependent_types substituted_t in + if clean_dummy_dependent_types then + FreshNamesGenerator.clean_dummy_dependent_types substituted_t + else substituted_t in let cleaned_ty = - FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in + 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 @@ -1726,19 +1862,31 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t)) | Some (n, Cic.Def (bo,ty)) -> let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in - let ty' = - match ty with - None -> None - | Some ty -> - Some (FreshNamesGenerator.clean_dummy_dependent_types ty) + 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 in - (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) + (cleaned_t,cleaned_ty,cleaned_metasenv,subst',ugraph1) +;; + +let type_of metasenv subst context t ug = + type_of_aux' metasenv subst context t ug +;; + +let type_of_aux' + ?clean_dummy_dependent_types ?localization_tbl metasenv context t ug += + let t,ty,m,s,ug = + type_of_aux' ?clean_dummy_dependent_types ?localization_tbl + metasenv [] context t ug + in + t,ty,m,ug ;; let undebrujin uri typesno tys t = @@ -1816,23 +1964,56 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno = metasenv,ugraph,substituted_tys let typecheck metasenv uri obj ~localization_tbl = - let ugraph = CicUniv.empty_ugraph in + 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 = fo_unif_subst [] [] metasenv boty ty' ugraph in + let subst,metasenv,ugraph = + try + fo_unif_subst [] [] metasenv boty ty' ugraph + with + RefineFailure _ + | Uncertain _ as exn -> + let msg = + lazy ("(1) 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 = + let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in - Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + (match CicReduction.whd [] sort with + Cic.Sort _ + | Cic.Meta _ -> Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph + | _ -> raise (RefineFailure (lazy ""))) | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) -> assert (metasenv' = metasenv); (* Here we do not check the metasenv for correctness *) @@ -1841,7 +2022,7 @@ let typecheck metasenv uri obj ~localization_tbl = let ty',sort,metasenv,ugraph = type_of_aux' ~localization_tbl metasenv [] ty ugraph in begin - match sort with + match CicReduction.whd ~delta:true [] sort with Cic.Sort _ (* instead of raising Uncertain, let's hope that the meta will become a sort *) @@ -1865,7 +2046,12 @@ let typecheck metasenv uri obj ~localization_tbl = List.fold_right (fun (name,b,ty,cl) (metasenv,ugraph,res) -> let ty',_,metasenv,ugraph = - type_of_aux' ~localization_tbl metasenv [] ty 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 @@ -1881,7 +2067,7 @@ let typecheck metasenv uri obj ~localization_tbl = (fun (name,ty) (metasenv,ugraph,res) -> let ty = CicTypeChecker.debrujin_constructor - ~cb:(relocalize localization_tbl) uri typesno ty in + ~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 @@ -1917,13 +2103,11 @@ let pack_coercion metasenv ctx t = | C.Lambda (name,so,dest) -> let ctx' = (Some (name,C.Decl so))::ctx in C.Lambda (name, merge_coercions ctx so, merge_coercions ctx' dest) - | C.LetIn (name,so,dest) -> - let _,ty,metasenv,ugraph = - pack_coercions := false; - type_of_aux' metasenv ctx so CicUniv.oblivion_ugraph in - pack_coercions := true; - let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in - C.LetIn (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 @@ -1990,7 +2174,13 @@ let pack_coercion metasenv ctx t = merge_coercions ctx t ;; -let pack_coercion_metasenv conjectures = +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) -> @@ -2013,9 +2203,16 @@ let pack_coercion_metasenv conjectures = in ((i,ctx,pack_coercion conjectures ctx ty)) ) conjectures + *) ;; -let pack_coercion_obj obj = +let pack_coercion_obj obj = obj (* + + TASSI: this code war written when coercions were a toy, + now packing coercions involves unification thus + the metasenv may change, and this pack coercion + does not handle that. + let module C = Cic in match obj with | C.Constant (id, body, ty, params, attrs) -> @@ -2050,7 +2247,7 @@ let pack_coercion_obj obj = (name, ind, arity, cl)) indtys in - C.InductiveDefinition (indtys, params, leftno, attrs) + C.InductiveDefinition (indtys, params, leftno, attrs) *) ;;