let inside c = indent := !indent ^ String.make 1 c;;
let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
-
+let debug = ref false;;
let pp s =
- prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+ if !debug then
+ prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
+ else
+ ()
;;
-let pp _ = ();;
-
let wrap_exc msg = function
| NCicUnification.Uncertain _ -> Uncertain msg
| NCicUnification.UnificationFailure _ -> RefineFailure msg
| `Closed -> NCicMetaSubst.mk_meta metasenv [] (foo `Term)
| `Type -> NCicMetaSubst.mk_meta metasenv context (foo `Type)
| `Term -> NCicMetaSubst.mk_meta metasenv context (foo `Term)
+ | `Tagged s ->
+ NCicMetaSubst.mk_meta ~attrs:[`Name s] metasenv context (foo `Term)
| `Vector ->
raise (RefineFailure (lazy (localise t, "A vector of implicit terms " ^
"can only be used in argument position")))
| Some x ->
let m, s, x =
NCicUnification.delift_type_wrt_terms
- rdb metasenv subst context x [t]
+ rdb metasenv subst context1 (NCicSubstitution.lift 1 x)
+ [NCicSubstitution.lift 1 t]
in
m, s, Some x
in
let metasenv =
List.filter (function (j,_) -> j <> metanoouttype) metasenv in
let subst =
- (metanoouttype,(Some "outtype",context,outtype,metaoutsort))::subst in
+ (metanoouttype,([`Name "outtype"],context,outtype,metaoutsort))::subst in
let outtype = newouttype in
(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
let rec first exc = function
| [] ->
raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
- "The term %s has type %s but is here used with type %s"
+ "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
(NCicPp.ppterm ~metasenv ~subst ~context t)
(NCicPp.ppterm ~metasenv ~subst ~context infty)
(NCicPp.ppterm ~metasenv ~subst ~context expty))) exc)
match NCicReduction.whd ~subst context ty_he with
| C.Prod (_,s,t) ->
let metasenv, subst, arg, _ =
- typeof rdb ~localise
- metasenv subst context arg (Some s) in
+ typeof rdb ~localise metasenv subst context arg (Some s) in
let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
aux metasenv subst (arg :: args_so_far) he t tl
| C.Meta _
| C.Appl (C.Meta _ :: _) as t ->
let metasenv, subst, arg, ty_arg =
- typeof rdb ~localise
- metasenv subst context arg None in
+ typeof rdb ~localise metasenv subst context arg None in
let name = guess_name subst context ty_arg in
let metasenv, _, meta, _ =
NCicMetaSubst.mk_meta metasenv
let flex_prod = C.Prod (name, ty_arg, meta) in
(* next line grants that ty_args is a type *)
let metasenv,subst, flex_prod, _ =
- typeof rdb ~localise metasenv subst
- context flex_prod None in
+ typeof rdb ~localise metasenv subst context flex_prod None in
(*
pp (lazy ( "UNIFICATION in CTX:\n"^
NCicPp.ppcontext ~metasenv ~subst context
uri, height, metasenv, subst, C.Inductive (ind, leftno, itl, attr)
;;
-NCicUnification.set_refiner_typeof typeof;;
-
(* vim:set foldmethod=marker: *)