X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=563fe392858b4f09ca26158bbcdd1c87e1290085;hb=7bf186f42e827e6e4112eba7ae5ca3e727f59026;hp=e0f920fff9e93bdecc4aa93873f6a50b2217d8f8;hpb=cf1817cb5d753cb4c0f14725be867e9f96da84a4;p=helm.git diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml index e0f920fff..563fe3928 100644 --- a/matita/components/ng_refiner/nCicRefiner.ml +++ b/matita/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 @@ -463,26 +489,33 @@ and check_type status ~localise metasenv subst context (ty as orig_ty) = metasenv, subst, ty and try_coercions status - ~localise - metasenv subst context t orig_t infty expty perform_unification exc + ~localise 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 *) let rec first exc = function | [] -> + let expty = + match expty with + `Type expty -> status#ppterm ~metasenv ~subst ~context expty + | `Sort -> "[[sort]]" + | `Prod -> "[[prod]]" in pp (lazy "WWW: no more coercions!"); raise (wrap_exc (lazy (localise orig_t, Printf.sprintf "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 +527,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 +557,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 = @@ -778,7 +819,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 @@ -803,35 +844,29 @@ and try_coercions status let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) in metasenv, subst, t, expty (*}}}*) - | _,_,NCic.LetIn(name,ty,t,bo) -> + | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> pp (lazy "LETIN"); - let context_bo = (name, NCic.Def (t,ty)) :: context in + 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) - (NCicSubstitution.lift status 1 expty) perform_unification exc + (`Type (NCicSubstitution.lift status 1 expty)) exc in - let coerced = NCic.LetIn (name,ty,t,bo2) 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),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) - in + | 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 = @@ -843,13 +878,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)); @@ -864,15 +909,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 () 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) @@ -999,8 +1048,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)