~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 _ ->
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
| 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
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 *)
"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));
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
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 =
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 ->
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
=
~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
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 =
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));
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)
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)
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 " ^
projects / helm.git / blobdiff