let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);;
-let ouri_of_reference (NReference.Ref (_,u,_)) = ouri_of_nuri u;;
+let ouri_of_reference (NReference.Ref (u,_)) = ouri_of_nuri u;;
let nn_2_on = function
| "_" -> Cic.Anonymous
| NCic.Sort NCic.CProp -> Cic.Sort Cic.CProp
| NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
| NCic.Implicit _ -> assert false
- | NCic.Const (NReference.Ref (_,u,NReference.Ind (_,i))) ->
+ | NCic.Const (NReference.Ref (u,NReference.Ind (_,i))) ->
Cic.MutInd (ouri_of_nuri u,i,[])
- | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) ->
+ | NCic.Const (NReference.Ref (u,NReference.Con (i,j))) ->
Cic.MutConstruct (ouri_of_nuri u,i,j,[])
- | NCic.Const (NReference.Ref (_,u,NReference.Def))
- | NCic.Const (NReference.Ref (_,u,NReference.Decl)) ->
+ | NCic.Const (NReference.Ref (u,NReference.Def _))
+ | NCic.Const (NReference.Ref (u,NReference.Decl)) ->
Cic.Const (ouri_of_nuri u,[])
- | NCic.Match (NReference.Ref (_,u,NReference.Ind (_,i)),oty,t,pl) ->
+ | NCic.Match (NReference.Ref (u,NReference.Ind (_,i)),oty,t,pl) ->
Cic.MutCase (ouri_of_nuri u,i, convert_term k oty, convert_term k t,
List.map (convert_term k) pl)
- | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_)))
- | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) ->
+ | NCic.Const (NReference.Ref (u,NReference.Fix (i,_,_)))
+ | NCic.Const (NReference.Ref (u,NReference.CoFix i)) ->
if NUri.eq u uri then
Cic.Rel (n_fl - i + k)
else
;;
let get_checked_def = function
- | NReference.Ref (_, uri, NReference.Def) ->
+ | NReference.Ref (uri, NReference.Def _) ->
(match get_checked_obj uri with
| _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
rlv,name,bo,ty,att,height
;;
let get_checked_indtys = function
- | NReference.Ref (_, uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
+ | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
(match get_checked_obj uri with
| _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
inductive,leftno,tys,att,n
;;
let get_checked_fixes_or_cofixes = function
- | NReference.Ref (_, uri, (NReference.Fix (fixno,_)|NReference.CoFix fixno))->
+ | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))->
(match get_checked_obj uri with
| _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
funcs, att, height
;;
let get_indty_leftno = function
- | NReference.Ref (_, uri, NReference.Ind _)
- | NReference.Ref (_, uri, NReference.Con _) ->
+ | NReference.Ref (uri, NReference.Ind _)
+ | NReference.Ref (uri, NReference.Con _) ->
(match get_checked_obj uri with
| _,_,_,_, NCic.Inductive (_,left,_,_) -> left
| _ ->prerr_endline "get_indty_leftno called on a non ind 2";assert false)
let r2s pp_fix_name r =
try
match r with
- | R.Ref (_,u,R.Ind (_,i)) ->
+ | R.Ref (u,R.Ind (_,i)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,name,_,_ = List.nth itl i in name
| _ -> assert false)
- | R.Ref (_,u,R.Con (i,j)) ->
+ | R.Ref (u,R.Con (i,j)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Inductive (_,_,itl,_) ->
let _,_,_,cl = List.nth itl i in
let _,name,_ = List.nth cl (j-1) in name
| _ -> assert false)
- | R.Ref (_,u,(R.Decl | R.Def )) ->
+ | R.Ref (u,(R.Decl | R.Def _)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Constant (_,name,_,_,_) -> name
| _ -> assert false)
- | R.Ref (_,u,(R.Fix (i,_)|R.CoFix i)) ->
+ | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) ->
(match NCicLibrary.get_obj u with
| _,_,_,_, C.Fixpoint (_,fl,_) ->
if pp_fix_name then
in
aux (k, e, he, tl' @ s)
| (_, _, NCic.Const
- (NReference.Ref (height,_,NReference.Def) as refer), s) as config ->
- if delta > height then config else
+ (NReference.Ref (_,NReference.Def height) as refer), s) as config ->
+ if delta >= height then config else
let _,_,body,_,_,_ = NCicEnvironment.get_checked_def refer in
aux (0, [], body, s)
- | (_, _, NCic.Const (NReference.Ref (_,_,
+ | (_, _, NCic.Const (NReference.Ref (_,
(NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
| (_, _, NCic.Const (NReference.Ref
- (height,_,NReference.Fix (fixno,recindex)) as refer),s) as config ->
- if delta > height then config else
+ (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config ->
+ if delta >= height then config else
(match
try Some (RS.from_stack (List.nth s recindex))
with Failure _ -> None
| Some recparam ->
let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
match reduce ~delta:0 ~subst context recparam with
- | (_,_,NCic.Const (NReference.Ref (_,_,NReference.Con _)), _) as c ->
+ | (_,_,NCic.Const (NReference.Ref (_,NReference.Con _)), _) as c ->
let new_s =
replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
in
| _ -> config)
| (k, e, NCic.Match (_,_,term,pl),s) as config ->
let decofix = function
- | (_,_,NCic.Const(NReference.Ref(_,_,NReference.CoFix c)as refer),s)->
+ | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)->
let cofixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in
let _,_,_,_,body = List.nth cofixes c in
reduce ~delta:0 ~subst context (0,[],body,s)
| config -> config
in
(match decofix (reduce ~delta:0 ~subst context (k,e,term,[])) with
- | (_, _, NCic.Const (NReference.Ref (_,_,NReference.Con (_,j))),[]) ->
+ | (_, _, NCic.Const (NReference.Ref (_,NReference.Con (_,j))),[]) ->
aux (k, e, List.nth pl (j-1), s)
| (_, _, NCic.Const
- (NReference.Ref (_,_,NReference.Con (_,j)) as refer), s') ->
+ (NReference.Ref (_,NReference.Con (_,j)) as refer), s') ->
let leftno = NCicEnvironment.get_indty_leftno refer in
let _,params = HExtlib.split_nth leftno s' in
aux (k, e, List.nth pl (j-1), params@s)
(* t1, t2 must be well-typed *)
let are_convertible whd ?(subst=[]) =
- let rec aux test_equality_only context t1 t2 =
- let rec aux2 test_equality_only t1 t2 =
+ let rec aux test_eq_only context t1 t2 =
+ let rec alpha_eq test_eq_only t1 t2 =
if t1 === t2 then
true
else
match (t1,t2) with
| (C.Sort (C.Type a), C.Sort (C.Type b)) -> a <= b
- | (C.Sort s1,C.Sort (C.Type _)) -> (not test_equality_only)
+ | (C.Sort s1,C.Sort (C.Type _)) -> (not test_eq_only)
| (C.Sort s1, C.Sort s2) -> s1 = s2
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux true context s1 s2 &&
- aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
+ aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
| (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
aux true context s1 s2 &&
- aux test_equality_only ((name1, C.Decl s1)::context) t1 t2
+ aux test_eq_only ((name1, C.Decl s1)::context) t1 t2
| (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
- aux test_equality_only context ty1 ty2 &&
- aux test_equality_only context s1 s2 &&
- aux test_equality_only ((name1, C.Def (s1,ty1))::context) t1 t2
+ aux test_eq_only context ty1 ty2 &&
+ aux test_eq_only context s1 s2 &&
+ aux test_eq_only ((name1, C.Def (s1,ty1))::context) t1 t2
| (C.Meta (n1,(s1, C.Irl i1)), C.Meta (n2,(s2, C.Irl i2)))
when n1 = n2 && s1 = s2 -> true
let l1 = NCicUtils.expand_local_context l1 in
let l2 = NCicUtils.expand_local_context l2 in
(try List.for_all2
- (fun t1 t2 -> aux test_equality_only context
+ (fun t1 t2 -> aux test_eq_only context
(NCicSubstitution.lift s1 t1)
(NCicSubstitution.lift s2 t2))
l1 l2
(try
let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
let term = NCicSubstitution.subst_meta l1 term in
- aux test_equality_only context term t2
+ aux test_eq_only context term t2
with NCicUtils.Subst_not_found _ -> false)
| _, C.Meta (n2,l2) ->
(try
let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
let term = NCicSubstitution.subst_meta l2 term in
- aux test_equality_only context t1 term
+ aux test_eq_only context t1 term
with NCicUtils.Subst_not_found _ -> false)
| (C.Appl l1, C.Appl l2) ->
- (try List.for_all2 (aux test_equality_only context) l1 l2
+ (try List.for_all2 (aux test_eq_only context) l1 l2
with Invalid_argument _ -> false)
| (C.Match (ref1,outtype1,term1,pl1),
C.Match (ref2,outtype2,term2,pl2)) ->
NReference.eq ref1 ref2 &&
- aux test_equality_only context outtype1 outtype2 &&
- aux test_equality_only context term1 term2 &&
- (try List.for_all2 (aux test_equality_only context) pl1 pl2
+ aux test_eq_only context outtype1 outtype2 &&
+ aux test_eq_only context term1 term2 &&
+ (try List.for_all2 (aux test_eq_only context) pl1 pl2
with Invalid_argument _ -> false)
| (C.Implicit _, _) | (_, C.Implicit _) -> assert false
| (_,_) -> false
in
- if aux2 test_equality_only t1 t2 then
+ if alpha_eq test_eq_only t1 t2 then
true
else
let height_of = function
- | NCic.Const (NReference.Ref (h,_,_)) -> h
- | NCic.Appl (NCic.Const (NReference.Ref (h,_,_))::_) -> h
+ | NCic.Const (NReference.Ref (_,NReference.Def h)) -> h
+ | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h))) -> h
+ | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_) -> h
+ | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
| _ -> 0
in
- let min_delta (k1,env1,t1,s1) (k2,env2,t2,s2) =
+ let small_delta_step (k1,env1,t1,s1 as m1) (k2,env2,t2,s2 as m2) =
let h1 = height_of t1 and h2 = height_of t2 in
if h1 > h2 then
- R.reduce ~delta:(h2+1) ~subst context (k1,env1,t1,s1),
- (k2,env2,t2,s2), h2+1
+ R.reduce ~delta:h2 ~subst context (k1,env1,t1,s1), m2, h2
else if h1 < h2 then
- (k1,env1,t1,s1),
- R.reduce ~delta:(h1+1) ~subst context (k2,env2,t2,s2),
- h1+1
+ m1, R.reduce ~delta:h1 ~subst context (k2,env2,t2,s2), h1
else
- R.reduce ~delta:(max 0 (h1-1)) ~subst context (k1,env1,t1,s1),
- R.reduce ~delta:(max 0 (h1-1)) ~subst context (k2,env2,t2,s2),
- (max 0 (h1-1))
+ let delta = max 0 (h1-1) in
+ R.reduce ~delta ~subst context (k1,env1,t1,s1),
+ R.reduce ~delta ~subst context (k2,env2,t2,s2),
+ delta
in
- let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) todo =
- (aux2 test_equality_only
+ let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
+ (alpha_eq test_eq_only
(R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
- try
- match List.combine s1 s2 @ todo with
- | [] -> true
- | (t1,t2) :: todo ->
+ try
+ List.for_all
+ (fun (t1,t2) ->
let t1 = RS.from_stack t1 and t2 = RS.from_stack t2 in
- convert_machines (min_delta t1 t2) todo
- with Invalid_argument _ -> false) ||
- (delta > 0 &&
- let delta = delta - 1 in
- let red = R.reduce ~delta ~subst context in
- convert_machines (red m1,red m2,delta) todo)
+ convert_machines (small_delta_step t1 t2))
+ (List.combine s1 s2)
+ with Invalid_argument _ -> false) ||
+ (let red delta = R.reduce ~delta ~subst context in
+ if delta = 0 then
+ alpha_eq test_eq_only (R.unwind (red 0 m1)) (R.unwind (red 0 m2))
+ else
+ let delta = delta - 1 in
+ convert_machines (red delta m1,red delta m2,delta))
in
- convert_machines (min_delta (0,[],t1,[]) (0,[],t2,[])) []
+ convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
in
aux false
;;
| _, C.Lambda(_,_,bo), arg::tl ->
let bo = NCicSubstitution.subst arg bo in
head_beta_reduce ~delta ~upto:(upto - 1) bo tl
- | _, C.Const (NReference.Ref (height, _, NReference.Def) as re), _
+ | _, C.Const (NReference.Ref (_, NReference.Def height) as re), _
when delta <= height ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
head_beta_reduce ~upto ~delta bo l
let l1 = HExtlib.sharing_map (aux (k-s)) l in
if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
| C.Meta _ -> t
- | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no)))
- | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
+ | C.Const (Ref.Ref (uri1,(Ref.Fix (no,_,_) | Ref.CoFix no)))
+ | C.Const (Ref.Ref (uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
C.Rel (k + number_of_types - no)
| t -> U.map (fun _ k -> k+1) k aux t
in
let specialize_inductive_type_constrs ~subst context ty_term =
match R.whd ~subst context ty_term with
- | C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref)
- | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
+ | C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref)
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
let left_args,_ = HExtlib.split_nth leftno args in
let dummy = C.Sort (C.Type ~-1) in
(*CSC: mettere in cicSubstitution *)
let rec subst_inductive_type_with_dummy _ = function
- | C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
- | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))))::tl)
+ | C.Const (Ref.Ref (uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
+ | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0))))::tl)
when NUri.eq uri' uri -> dummy
| t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
in
match R.whd context te with
- | C.Const (Ref.Ref (_,uri',Ref.Ind _))
- | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_)
+ | C.Const (Ref.Ref (uri',Ref.Ind _))
+ | C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind _)))::_)
when NUri.eq uri' uri -> true
| C.Prod (name,source,dest) when
does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
List.for_all (does_not_occur ~subst context n nn) tl
- | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as r)::tl) ->
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (_,i)) as r)::tl) ->
let _,paramsno,tyl,_,i = E.get_checked_indtys r in
let _,name,ity,cl = List.nth tyl i in
let ok = List.length tyl = 1 in
*)
eat_prods ~subst ~metasenv context he ty_he args_with_ty
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
- | C.Match (Ref.Ref (_,_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
+ | C.Match (Ref.Ref (_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
let outsort = typeof_aux context outtype in
let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
let constructorsno =
let ty = R.whd ~subst context (typeof_aux context term) in
let r',tl =
match ty with
- C.Const (Ref.Ref (_,_,Ref.Ind _) as r') -> r',[]
- | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _) as r') :: tl) -> r',tl
+ C.Const (Ref.Ref (_,Ref.Ind _) as r') -> r',[]
+ | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as r') :: tl) -> r',tl
| _ ->
raise
(TypeCheckerFailure (lazy (Printf.sprintf
and type_of_branch ~subst context leftno outty cons tycons liftno =
match R.whd ~subst context tycons with
- | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
- | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) ->
+ | C.Const (Ref.Ref (_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
+ | C.Appl (C.Const (Ref.Ref (_,Ref.Ind _))::tl) ->
let _,arguments = HExtlib.split_nth leftno tl in
C.Appl (S.lift liftno outty::arguments@[cons])
| C.Prod (name,so,de) ->
| _,C.Decl _ -> ()
| _,C.Def (bo,_) -> aux k (S.lift m bo))
| C.Meta _ -> ()
- | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) ->
+ | C.Appl (C.Const ((Ref.Ref (uri,Ref.Fix (i,recno,_))) as r)::args) ->
if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args
then
let fl,_,_ = E.get_checked_fixes_or_cofixes r in
) bos
in
List.iter (fun (bo,k) -> aux k bo) bos_and_ks
- | C.Match (Ref.Ref (_,uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
+ | C.Match (Ref.Ref (uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
(match R.whd ~subst context term with
| C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
let ty = typeof ~subst ~metasenv context term in
| C.Sort _
| C.Implicit _
| C.Prod _
- | C.Const (Ref.Ref (_,_,Ref.Ind _))
+ | C.Const (Ref.Ref (_,Ref.Ind _))
| C.LetIn _ -> raise (AssertFailure (lazy "17"))
| C.Lambda (name,so,de) ->
does_not_occur ~subst context n nn so &&
aux ((name,C.Decl so)::context) (n + 1) (nn + 1) h de
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h && List.for_all (does_not_occur ~subst context n nn) tl
- | C.Const (Ref.Ref (_,_,Ref.Con _)) -> true
- | C.Appl (C.Const (Ref.Ref (_,uri, Ref.Con (_,j)) as ref) :: tl) as t ->
+ | C.Const (Ref.Ref (_,Ref.Con _)) -> true
+ | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j)) as ref) :: tl) as t ->
let _, paramsno, _, _, _ = E.get_checked_indtys ref in
let ty_t = typeof ~subst ~metasenv context t in
let dc_ctx, dcl, start, stop =
does_not_occur ~subst context n nn out &&
does_not_occur ~subst context n nn te &&
List.for_all (aux context n nn h) pl
- | C.Const (Ref.Ref (_,u,(Ref.Fix _| Ref.CoFix _)) as ref)
- | C.Appl(C.Const (Ref.Ref(_,u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
+ | C.Const (Ref.Ref (u,(Ref.Fix _| Ref.CoFix _)) as ref)
+ | C.Appl(C.Const (Ref.Ref(u,(Ref.Fix _| Ref.CoFix _)) as ref) :: _) as t ->
let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
let fl,_,_ = E.get_checked_fixes_or_cofixes ref in
let len = List.length fl in
| C.Appl (he::_) ->
is_really_smaller r_uri r_len ~subst ~metasenv k he
| C.Rel _
- | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
+ | C.Const (Ref.Ref (_,Ref.Con _)) -> false
| C.Appl []
- | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
+ | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
| C.Meta _ -> true
- | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
+ | C.Match (Ref.Ref (uri,_) as ref,outtype,term,pl) ->
(match term with
| C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
(* TODO: add CoInd to references so that this call is useless *)
and returns_a_coinductive ~subst context ty =
match R.whd ~subst context ty with
- | C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)
- | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)::_) ->
+ | C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind (false,_)) as ref)::_) ->
let _, _, itl, _, _ = E.get_checked_indtys ref in
Some (uri,List.length itl)
| C.Prod (n,so,de) ->
returns_a_coinductive ~subst ((n,C.Decl so)::context) de
| _ -> None
-and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
+and type_of_constant ((Ref.Ref (uri,_)) as ref) =
match E.get_checked_obj uri, ref with
- | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind (_,i)) ->
+ | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Ind (_,i)) ->
let _,_,arity,_ = List.nth tl i in arity
- | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j)) ->
+ | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j)) ->
let _,_,_,cl = List.nth tl i in
let _,_,arity = List.nth cl (j-1) in
arity
- | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
+ | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,(Ref.Fix (i,_,_)|Ref.CoFix i)) ->
let _,_,_,arity,_ = List.nth fl i in
arity
- | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty
+ | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,(Ref.Def _|Ref.Decl)) -> ty
| _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
;;
match List.hd context with _,C.Decl t -> t | _ -> assert false
in
match R.whd ~subst (List.tl context) he with
- | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)
- | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) :: _) ->
+ | C.Const (Ref.Ref (uri,Ref.Ind _) as ref)
+ | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as ref) :: _) ->
let _,_,itl,_,_ = E.get_checked_indtys ref in
uri, List.length itl
| _ -> assert false
type spec =
| Decl
- | Def
- | Fix of int * int (* fixno, recparamno *)
+ | Def of int (* height *)
+ | Fix of int * int * int (* fixno, recparamno, height *)
| CoFix of int
| Ind of bool * int (* inductive, indtyno *)
| Con of int * int (* indtyno, constrno *)
-type reference = Ref of int * NUri.uri * spec
+type reference = Ref of NUri.uri * spec
let eq = (==);;
;;
let reference_of_string =
- let counter = ref 0 in
- let c () = incr counter; !counter in
+ let get3 s dot =
+ let comma2 = String.rindex s ',' in
+ let comma = String.rindex_from s (comma2-1) ',' in
+ let s_i = String.sub s (dot+5) (comma-dot-5) in
+ let s_j = String.sub s (comma+1) (comma2-comma-1) in
+ let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in
+ let i = int_of_string s_i in
+ let j = int_of_string s_j in
+ let h = int_of_string s_h in
+ i,j,h
+ in
let get2 s dot =
let comma = String.rindex s ',' in
let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
let suffix = String.sub s (dot+1) 3 in
let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in
match suffix with
- | "dec" -> Ref (c (), u, Decl)
- | "def" -> Ref (c (), u, Def)
- | "fix" -> let i,j = get2 s dot in Ref (c (), u, Fix (i,j))
- | "cfx" -> let i = get1 s dot in Ref (c (), u, CoFix (i))
- | "ind" -> let b,i = get2 s dot in Ref (c (), u, Ind (b=1,i))
- | "con" -> let i,j = get2 s dot in Ref (c (), u, Con (i,j))
+ | "dec" -> Ref (u, Decl)
+ | "def" -> let i = get1 s dot in Ref (u, Def i)
+ | "fix" -> let i,j,h = get3 s dot in Ref (u, Fix (i,j,h))
+ | "cfx" -> let i = get1 s dot in Ref (u, CoFix (i))
+ | "ind" -> let b,i = get2 s dot in Ref (u, Ind (b=1,i))
+ | "con" -> let i,j = get2 s dot in Ref (u, Con (i,j))
| _ -> raise Not_found
with Not_found -> raise (IllFormedReference (lazy s))
in
new_reference
;;
-let string_of_reference (Ref (_,u,indinfo)) =
+let string_of_reference (Ref (u,indinfo)) =
let s = NUri.string_of_uri u in
let dot = String.rindex s '.' in
let s2 = String.sub s 0 dot in
match indinfo with
| Decl -> s2 ^ ".dec"
- | Def -> s2 ^ ".def"
- | Fix (i,j) -> s2 ^ ".fix(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
+ | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")"
+ | Fix (i,j,h) ->
+ s2 ^ ".fix(" ^ string_of_int i ^ "," ^
+ string_of_int j ^ "," ^ string_of_int h ^ ")"
| CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
| Ind (b,i)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^")"
| Con (i,j) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")"
;;
let mk_constructor j = function
- | Ref (d, u, Ind (_,i)) ->
- reference_of_string (string_of_reference (Ref (d, u, Con (i,j))))
+ | Ref (u, Ind (_,i)) ->
+ reference_of_string (string_of_reference (Ref (u, Con (i,j))))
| _ -> assert false
;;
let mk_fix i j = function
- | Ref (d, u, Fix _) ->
- reference_of_string (string_of_reference (Ref (d, u, Fix (i,j))))
+ | Ref (u, Fix (_,_,h)) ->
+ reference_of_string (string_of_reference (Ref (u, Fix (i,j,h))))
| _ -> assert false
;;
let mk_cofix i = function
- | Ref (d, u, CoFix _) ->
- reference_of_string (string_of_reference (Ref (d, u, CoFix i)))
+ | Ref (u, CoFix _) ->
+ reference_of_string (string_of_reference (Ref (u, CoFix i)))
| _ -> assert false
;;
type spec =
| Decl
- | Def
- | Fix of int * int (* fixno, recparamno *)
+ | Def of int (* height *)
+ | Fix of int * int * int (* fixno, recparamno, height *)
| CoFix of int
| Ind of bool * int (* inductive, indtyno *)
| Con of int * int (* indtyno, constrno *)
-type reference = private Ref of int * NUri.uri * spec
+type reference = private Ref of NUri.uri * spec
val eq: reference -> reference -> bool
val string_of_reference: reference -> string
let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
(* porcatissima *)
-type reference = Ref of int * NUri.uri * NReference.spec
+type reference = Ref of NUri.uri * NReference.spec
let reference_of_ouri u indinfo =
let u = nuri_of_ouri u in
NReference.reference_of_string
- (NReference.string_of_reference (Obj.magic (Ref (max_int,u,indinfo))))
+ (NReference.string_of_reference (Obj.magic (Ref (u,indinfo))))
;;
type ctx =
| NCic.Prod (_,s1,t1), NCic.Prod (_,s2,t2) -> aux s1 s2; aux t1 t2
| NCic.LetIn (_,s1,ty1,t1), NCic.LetIn (_,s2,ty2,t2) ->
aux s1 s2; aux ty1 ty2; aux t1 t2
- | NCic.Const (NReference.Ref (_,uu1,xp1)),
- NCic.Const (NReference.Ref (_,uu2,xp2)) when
- let NReference.Ref (_,u1,_) = ref in
- let NReference.Ref (_,u2,_) = ref' in
+ | NCic.Const (NReference.Ref (uu1,xp1)),
+ NCic.Const (NReference.Ref (uu2,xp2)) when
+ let NReference.Ref (u1,_) = ref in
+ let NReference.Ref (u2,_) = ref' in
NUri.eq uu1 u1 && NUri.eq uu2 u2 && xp1 = xp2
-> ()
| NCic.Const r1, NCic.Const r2 when NReference.eq r1 r2 -> ()
(function (ref',obj') ->
let recno, fixno =
match ref with
- NReference.Ref (_,_,NReference.Fix (fixno,recno)) -> recno,fixno
- | NReference.Ref (_,_,NReference.CoFix (fixno)) -> ~-1,fixno
+ NReference.Ref (_,NReference.Fix (fixno,recno,_)) -> recno,fixno
+ | NReference.Ref (_,NReference.CoFix (fixno)) -> ~-1,fixno
| _ -> assert false in
let recno',fixno' =
match ref' with
- NReference.Ref (_,_,NReference.Fix (fixno',recno)) -> recno,fixno'
- | NReference.Ref (_,_,NReference.CoFix (fixno')) -> ~-1,fixno'
+ NReference.Ref (_,NReference.Fix (fixno',recno,_)) -> recno,fixno'
+ | NReference.Ref (_,NReference.CoFix (fixno')) -> ~-1,fixno'
| _ -> assert false in
if recno = recno' && fixno = fixno' && same_obj ref ref' (obj,obj') then (
(*
begin
match obj, ref with
| (_,_,_,_,NCic.Fixpoint (true,fl,_)) ,
- NReference.Ref (x,y,NReference.Fix _) ->
+ NReference.Ref (y,NReference.Fix _) ->
ignore(List.fold_left (fun i (_,name,rno,_,_) ->
let ref = NReference.mk_fix i rno ref in
Hashtbl.add cache name (ref,obj);
i+1
) 0 fl)
| (_,_,_,_,NCic.Fixpoint (false,fl,_)) ,
- NReference.Ref (x,y,NReference.CoFix _) ->
+ NReference.Ref (y,NReference.CoFix _) ->
ignore(List.fold_left (fun i (_,name,rno,_,_) ->
let ref = NReference.mk_cofix i ref in
Hashtbl.add cache name (ref,obj);
(fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in
let r = (* recno is dummy here, must be lifted by the ctx len *)
- reference_of_ouri buri (Ref.Fix (idx,recno))
+ reference_of_ouri buri (Ref.Fix (idx,recno,1))
in
bctx @ [Fix (lazy (r,name,ty))],
fixpoints_ty@fixpoints,ty::tys,idx-1)
let free_decls = Lazy.force free_decls in
let bctx =
List.map (function ce -> match strictify ce with
- | `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) ->
+ | `Fix (Ref.Ref (_,Ref.Fix (idx, recno,height)),name, ty) ->
Fix (lazy (reference_of_ouri buri
- (Ref.Fix (idx,recno+free_decls)),name,ty))
+ (Ref.Fix (idx,recno+free_decls,height)),name,ty))
| _ -> assert false) bad_bctx @ ctx
in
let n_fl = List.length fl in
let obj =
nuri_of_ouri buri,max_int,[],[],
NCic.Fixpoint (true, fl, (`Generated, `Definition)) in
- let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in
+ let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno,1)) in
let obj,r =
let _,name,_,_,_ = List.nth fl fixno in
match find_in_cache name obj r with
aux_ens k curi octx ctx n_fix uri ens
(match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
| Cic.Constant (_,Some _,_,_,_) ->
- NCic.Const (reference_of_ouri curi Ref.Def)
+ NCic.Const (reference_of_ouri curi (Ref.Def 1))
| Cic.Constant (_,None,_,_,_) ->
NCic.Const (reference_of_ouri curi Ref.Decl)
| _ -> assert false)
projects / helm.git / commitdiff