name' ^ (if last = -1 then "" else string_of_int (last + 1))
with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
+(* let eq, eq_refl =
+ let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
+ C.Const (Ref.reference_of_spec uri (Ref.Ind (true,0,2))),
+ C.Const (Ref.reference_of_spec uri Ref.Con (0,1,2))
+*)
+let eq, eq_refl =
+ let uri = NUri.uri_of_string "cic:/matita/basics/jmeq/jmeq.ind" in
+ C.Const (Ref.reference_of_spec uri (Ref.Ind(true,0,2))),
+ C.Const (Ref.reference_of_spec uri (Ref.Con(0,1,2)))
+
let rec typeof (status:#NCicCoercion.status)
?(localise=fun _ -> Stdpp.dummy_loc)
metasenv subst context term expty
(*D*)in outside true; rc with exc -> outside false; raise exc
in
let rec typeof_aux metasenv subst context expty =
- fun t as orig ->
+ fun (t as orig) ->
(*D*)inside 'R'; try let rc =
pp (lazy (status#ppterm ~metasenv ~subst ~context t ^ " ::exp:: " ^
match expty with `XTSort -> "Any sort" | `XTInd -> "Any (co)inductive type"
| [] ->
pp (lazy "WWW: no more coercions!");
raise (wrap_exc (lazy
- let expty =
+ (let expty =
match expty with
`XTSome expty -> status#ppterm ~metasenv ~subst ~context expty
| `XTSort -> "[[sort]]"
"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)
- expty)) exc)
+ expty))) exc)
| (_,metasenv, newterm, newtype, meta)::tl ->
try
pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));
pp (lazy "WWW: trying coercions -- inner check");
match infty, expty, t with
(* `XTSort|`XTProd|`XTInd + Match not implemented *)
- | _,`XTSome expty, C.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+ | _,`XTSome expty, C.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 =
match refit with
- | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
+ | Ref.Ref (_uri, Ref.Ind (_,tyno,_leftno)) ->
let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys status r in
let _, _, ty, cl = List.nth itl tyno in
- let constructorsno = List.length cl in
+ (*let constructorsno = List.length cl in*)
let count_pis t =
let rec aux ctx t =
match NCicReduction.whd status ~subst ~delta:max_int ctx t with
(List.map (NCicSubstitution.lift status 1) right_p) (NCicSubstitution.lift status 1 matched) (n-1))
| _ -> assert false
in
- (*let eq = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
- let eq_refl = C.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
- let eq = C.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
- let eq_refl = C.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
=
(NCicSubstitution.lift status 1 mty) (NCicSubstitution.lift status 1 m) tgt
in
C.Prod (name, src, t), k
- | C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
+ | C.Const (Ref.Ref (_,Ref.Ind (_,_,_leftno)) as r) ->
let k =
let k = C.Const(Ref.mk_constructor i r) in
NCicUntrusted.mk_appl k par
(NCicReduction.head_beta_reduce status ~delta:max_int
(NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
| C.Appl (C.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
- let left_p,right_p = HExtlib.split_nth leftno pl in
- let has_rights = right_p <> [] in
+ let left_p,_right_p = HExtlib.split_nth leftno pl in
+ (*let has_rights = right_p <> [] in*)
let k =
let k = C.Const(Ref.mk_constructor i r) in
NCicUntrusted.mk_appl k (left_p@par)
in (* }}} end helper functions *)
(* constructors types with left params already instantiated *)
let outty = NCicUntrusted.apply_subst status subst context outty in
- let cl, left_p, leftno,rno =
+ let cl, _left_p, leftno,rno =
get_cl_and_left_p r outty
in
let right_p, mty =
pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
metasenv, subst, coerced, expty (*}}}*)
| _ -> raise exc
- with exc2 ->
+ with _ ->
let expty =
match expty with
`XTSome expty -> expty
| x::_ -> x
| _ -> assert false))
| `XTProd -> C.Prod ("_",C.Implicit `Type,C.Implicit `Type)
+ | `XTInd -> assert false(*CSC: was not handled, OCaml 4.0 complains. ??? *)
in
pp(lazy("try_coercion " ^
status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
and guess_name status subst ctx ty =
let aux initial = "#" ^ String.make 1 initial in
match ty with
- | C.Const (NReference.Ref (u,_))
- | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
+ | C.Const (Ref.Ref (u,_))
+ | C.Appl (C.Const (Ref.Ref (u,_)) :: _) ->
aux (String.sub (NUri.name_of_uri u) 0 1).[0]
| C.Prod _ -> aux 'f'
| C.Meta (n,lc) ->
aux metasenv subst (arg :: args_so_far) he meta tl
| C.Match (_,_,C.Meta _,_)
| C.Match (_,_,C.Appl (C.Meta _ :: _),_)
- | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+ | C.Appl (C.Const (Ref.Ref (_, Ref.Fix _)) :: _) ->
raise (Uncertain (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)
(fun (_,_,rno,_,_,_) i ->
let i = len - i - 1 in
C.Const
- (if inductive then NReference.mk_fix i rno ref
- else NReference.mk_cofix i ref))
+ (if inductive then Ref.mk_fix i rno ref
+ else Ref.mk_cofix i ref))
rev_fl)
t
;;
(fun (relevance,name,k,ty,dbo) ->
let bo =
undebruijnate status inductive
- (NReference.reference_of_spec uri
- (if inductive then NReference.Fix (0,k,0)
- else NReference.CoFix 0)) dbo rev_fl
+ (Ref.reference_of_spec uri
+ (if inductive then Ref.Fix (0,k,0)
+ else Ref.CoFix 0)) dbo rev_fl
in
relevance,name,k,ty,bo)
fl
let rec aux context (metasenv,subst) = function
| C.Meta _ -> metasenv, subst
| C.Implicit _ -> metasenv, subst
- | C.Appl (C.Rel i :: args) as t
+ | C.Appl (C.Rel i :: args)
when i > List.length context - len ->
let lefts, _ = HExtlib.split_nth leftno args in
let ctxlen = List.length context in
if i <= leftno then
C.Rel i
else
- C.Const (NReference.reference_of_spec uri
- (NReference.Ind (ind,relsno - i,leftno))))
+ C.Const (Ref.reference_of_spec uri
+ (Ref.Ind (ind,relsno - i,leftno))))
(HExtlib.list_seq 1 (relsno+1))
te in
let te =