~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
(* 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
+ raise (wrap_exc (lazy
+ let expty =
+ match expty with
+ `Type expty -> status#ppterm ~metasenv ~subst ~context expty
+ | `Sort -> "[[sort]]"
+ | `Prod -> "[[prod]]" in
+ (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)
in
metasenv, subst, t, expty (*}}}*)
| _,`Type expty,NCic.LetIn(name,ty,t,bo) ->
- 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
pp (lazy "LETIN");
- let name' = mk_fresh_name context 'l' 0 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
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), _ ->
- 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
(*{{{*) 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, _ =
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 `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)))
+ t orig_t ty `Sort exn
and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
t (t1, t2)