X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=7cdeb875e19d585baad9e65c3df1482f5cae410d;hb=1410ea677188e9e11d748c69e208d1e90b0a324e;hp=8deb72797c5d690b0de62f48f4476584c4828938;hpb=f1ef0a9e283af00cace679efd5775062c2a8f05c;p=helm.git diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml index 8deb72797..7cdeb875e 100644 --- a/matitaB/components/ng_refiner/nCicRefiner.ml +++ b/matitaB/components/ng_refiner/nCicRefiner.ml @@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t = ~unify:(fun m s c t1 t2 -> try Some (NCicUnification.unify status m s c t1 t2) with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) - metasenv subst context 0 (0,NCic.Irl 0) typ + metasenv subst context ~-1 (0,NCic.Irl 0) typ with NCicMetaSubst.MetaSubstFailure _ | NCicMetaSubst.Uncertain _ -> @@ -139,6 +139,32 @@ let check_allowed_sort_elimination status localise r orig = aux ;; +(* CSC: temporary thing, waiting for better times *) +let mk_fresh_name context name = +try + let rex = Str.regexp "[0-9']*$" in + let rex2 = Str.regexp "'*$" in + let basename = Str.global_replace rex "" in + let suffix name = + ignore (Str.search_forward rex name 0); + let n = Str.matched_string name in + let n = Str.global_replace rex2 "" n in + if n = "" then 0 else int_of_string n +in + let name' = basename name in + let name' = if name' = "_" then "H" else name' in + let last = + List.fold_left + (fun last (name,_) -> + if basename name = name' then + max last (suffix name) + else + last + ) (-1) context + in + name' ^ (if last = -1 then "" else string_of_int (last + 1)) +with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false + let rec typeof (status:#NCicCoercion.status) ?(localise=fun _ -> Stdpp.dummy_loc) metasenv subst context term expty @@ -166,7 +192,7 @@ let rec typeof (status:#NCicCoercion.status) | NCicUnification.Uncertain _ | NCicUnification.UnificationFailure _ as exc -> try_coercions status ~localise - metasenv subst context t orig infty expty true exc) + metasenv subst context t orig infty (`Type expty) exc) | None -> metasenv, subst, t, infty (*D*)in outside true; rc with exc -> outside false; raise exc in @@ -464,14 +490,17 @@ and check_type status ~localise metasenv subst context (ty as orig_ty) = and try_coercions status ~localise - metasenv subst context t orig_t infty expty perform_unification exc + metasenv subst context t orig_t infty expty exc = let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in try - pp (lazy "WWW: trying coercions -- preliminary unification"); - let metasenv, subst = - NCicUnification.unify status metasenv subst context infty expty - in metasenv, subst, t, expty + (match expty with + `Type expty -> + pp (lazy "WWW: trying coercions -- preliminary unification"); + let metasenv, subst = + NCicUnification.unify status metasenv subst context infty expty + in metasenv, subst, t, expty + | _ -> raise (Failure "Special case Prod or Sort")) with | exn -> (* we try with a coercion *) @@ -482,7 +511,7 @@ and try_coercions status "The term\n%s\nhas type\n%s\nbut is here used with type\n%s" (status#ppterm ~metasenv ~subst ~context t) (status#ppterm ~metasenv ~subst ~context infty) - (status#ppterm ~metasenv ~subst ~context expty))) exc) + expty)) exc) | (_,metasenv, newterm, newtype, meta)::tl -> try pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm)); @@ -494,21 +523,28 @@ and try_coercions status status#ppterm ~metasenv ~subst ~context t ^ " === " ^ status#ppterm ~metasenv ~subst ~context meta ^ "\n")); let metasenv, subst = - NCicUnification.unify status metasenv subst context t meta - in - pp (lazy ( "UNIFICATION in CTX:\n"^ - status#ppcontext ~metasenv ~subst context - ^ "\nMENV: " ^ - status#ppmetasenv metasenv ~subst - ^ "\nOF: " ^ - status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^ - status#ppterm ~metasenv ~subst ~context expty ^ "\n")); - let metasenv, subst = - if perform_unification then - NCicUnification.unify status metasenv subst context newtype expty - else metasenv, subst - in - metasenv, subst, newterm, newtype + NCicUnification.unify status metasenv subst context t meta in + match expty with + `Type expty -> + pp (lazy ( "UNIFICATION in CTX:\n"^ + status#ppcontext ~metasenv ~subst context + ^ "\nMENV: " ^ + status#ppmetasenv metasenv ~subst + ^ "\nOF: " ^ + status#ppterm ~metasenv ~subst ~context newtype ^ " === " ^ + status#ppterm ~metasenv ~subst ~context expty ^ "\n")); + let metasenv,subst = + NCicUnification.unify status metasenv subst context newtype expty + in + metasenv, subst, newterm, newtype + | `Sort -> + (match NCicReduction.whd status ~subst context newtype with + NCic.Sort _ -> metasenv,subst,newterm,newtype + | _ -> first exc tl) + | `Prod -> + (match NCicReduction.whd status ~subst context newtype with + NCic.Prod _ -> metasenv,subst,newterm,newtype + | _ -> first exc tl) with | NCicUnification.UnificationFailure _ -> first exc tl | NCicUnification.Uncertain _ as exc -> first exc tl @@ -517,7 +553,8 @@ and try_coercions status try pp (lazy "WWW: trying coercions -- inner check"); match infty, expty, t with - | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> + (* `Sort|`Prod + Match not implemented *) + | _,`Type expty, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) -> (*{{{*) pp (lazy "CASE"); (* {{{ helper functions *) let get_cl_and_left_p refit outty = @@ -572,6 +609,7 @@ and try_coercions status cl, left_p, leftno, rno | _ -> raise exn in + (*{{{*) pp (lazy "CASE"); let rec keep_lambdas_and_put_expty ctx t bo right_p matched n = match t,n with | _,0 -> @@ -598,8 +636,8 @@ and try_coercions status in (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*) - let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in - let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in + let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in + let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in let add_params metasenv subst context cty outty mty m i = @@ -777,7 +815,7 @@ and try_coercions status ~context ~metasenv ~subst pbo)); let metasenv, subst, pbo, _ = try_coercions status ~localise menv s context pbo - orig_t (*??*) infty_pbo expty_pbo perform_unification exc + orig_t (*??*) infty_pbo (`Type expty_pbo) exc in pp (lazy ("CASE: pbo2: " ^ status#ppterm @@ -802,24 +840,29 @@ and try_coercions status let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) in metasenv, subst, t, expty (*}}}*) - | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> - let rec mk_fresh_name ctx firstch n = - let candidate = (String.make 1 firstch) ^ (string_of_int n) in - if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate - else mk_fresh_name ctx firstch (n+1) + | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> + pp (lazy "LETIN"); + let name' = mk_fresh_name context name in + let context_bo = (name', NCic.Def (t,ty)) :: context in + let metasenv, subst, bo2, _ = + try_coercions status ~localise metasenv subst context_bo + bo orig_t (NCicSubstitution.lift status 1 infty) + (`Type (NCicSubstitution.lift status 1 expty)) exc in + let coerced = NCic.LetIn (name',ty,t,bo2) in + pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); + metasenv, subst, coerced, expty + | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ -> (*{{{*) pp (lazy "LAM"); pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t)); - let name_con = mk_fresh_name context 'c' 0 - (*FreshNamesGenerator.mk_fresh_name - ~subst metasenv context ~typ:src2 Cic.Anonymous*) - in + let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in + let name_con = mk_fresh_name context namename in let context_src2 = ((name_con, NCic.Decl src2) :: context) in (* contravariant part: the argument of f:src->ty *) let metasenv, subst, rel1, _ = try_coercions status ~localise metasenv subst context_src2 (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) - (NCicSubstitution.lift status 1 src) perform_unification exc + (`Type (NCicSubstitution.lift status 1 src)) exc in (* covariant part: the result of f(c x); x:src2; (c x):src *) let name_t, bo = @@ -831,13 +874,23 @@ and try_coercions status let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in let metasenv, subst, bo, _ = try_coercions status ~localise metasenv subst context_src2 - bo orig_t ty ty2 perform_unification exc + bo orig_t ty (`Type ty2) exc in let coerced = NCic.Lambda (name_t,src2, bo) in pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced)); metasenv, subst, coerced, expty (*}}}*) | _ -> raise exc with exc2 -> + let expty = + match expty with + `Type expty -> expty + | `Sort -> + NCic.Sort (NCic.Type + (match NCicEnvironment.get_universes () with + | x::_ -> x + | _ -> assert false)) + | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type) + in pp(lazy("try_coercion " ^ status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^ status#ppterm ~metasenv ~subst ~context expty)); @@ -852,15 +905,19 @@ and force_to_sort status metasenv subst context t orig_t localise ty = metasenv, subst, t, ty with Failure _ -> + let msg = + (lazy (localise orig_t, + "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^ + " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in let ty = NCicReduction.whd status ~subst context ty in + let exn = + if NCicUnification.could_reduce status ~subst context ty then + Uncertain msg + else + RefineFailure msg + in try_coercions status ~localise metasenv subst context - t orig_t ty (NCic.Sort (NCic.Type - (match NCicEnvironment.get_universes status with - | x::_ -> x - | _ -> assert false))) false - (Uncertain (lazy (localise orig_t, - "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^ - " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty))) + t orig_t ty `Sort exn and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s) t (t1, t2) @@ -987,8 +1044,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig let metasenv, subst, newhead, newheadty = try_coercions status ~localise metasenv subst context (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty - (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term)) - false + `Prod (RefineFailure (lazy (localise orig_he, Printf.sprintf ("The term %s is here applied to %d arguments but expects " ^^ "only %d arguments") (status#ppterm ~metasenv ~subst ~context he) @@ -1204,7 +1260,7 @@ let typeof_obj NCicReduction.whd status ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> - if not (NCicEnvironment.universe_leq status u1 u2) then + if not (NCicEnvironment.universe_leq u1 u2) then raise (RefineFailure (lazy(localise te, "The type " ^