~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 basename = Str.global_replace rex "" in
+ let suffix name =
+ ignore (Str.search_forward rex name 0);
+ let n = Str.matched_string name 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
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));
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 =
~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.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 =
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));
Failure _ ->
let ty = NCicReduction.whd status ~subst context ty 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
+ t orig_t ty `Sort
(Uncertain (lazy (localise orig_t,
"The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
" is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
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)
projects / helm.git / blobdiff