| 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)) ->
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,_,_)))
(* $Id$ *)
+module C = NCic
+module Ref = NReference
+
exception CircularDependency of string Lazy.t;;
exception ObjectNotFound of string Lazy.t;;
exception BadDependency of string Lazy.t;;
;;
let get_checked_decl = function
- | NReference.Ref (uri, NReference.Decl) ->
+ | Ref.Ref (uri, Ref.Decl) ->
(match get_checked_obj uri with
- | _,height,_,_, NCic.Constant (rlv,name,None,ty,att) ->
+ | _,height,_,_, C.Constant (rlv,name,None,ty,att) ->
rlv,name,ty,att,height
- | _,_,_,_, NCic.Constant (_,_,Some _,_,_) ->
+ | _,_,_,_, C.Constant (_,_,Some _,_,_) ->
prerr_endline "get_checked_decl on a definition"; assert false
| _ -> prerr_endline "get_checked_decl on a non decl 2"; assert false)
| _ -> prerr_endline "get_checked_decl on a non decl"; assert false
;;
let get_checked_def = function
- | NReference.Ref (uri, NReference.Def _) ->
+ | Ref.Ref (uri, Ref.Def _) ->
(match get_checked_obj uri with
- | _,height,_,_, NCic.Constant (rlv,name,Some bo,ty,att) ->
+ | _,height,_,_, C.Constant (rlv,name,Some bo,ty,att) ->
rlv,name,bo,ty,att,height
- | _,_,_,_, NCic.Constant (_,_,None,_,_) ->
+ | _,_,_,_, C.Constant (_,_,None,_,_) ->
prerr_endline "get_checked_def on an axiom"; assert false
| _ -> prerr_endline "get_checked_def on a non def 2"; assert false)
| _ -> prerr_endline "get_checked_def on a non def"; assert false
;;
let get_checked_indtys = function
- | NReference.Ref (uri, (NReference.Ind (_,n)|NReference.Con (n,_))) ->
+ | Ref.Ref (uri, (Ref.Ind (_,n,_)|Ref.Con (n,_,_))) ->
(match get_checked_obj uri with
- | _,_,_,_, NCic.Inductive (inductive,leftno,tys,att) ->
+ | _,_,_,_, C.Inductive (inductive,leftno,tys,att) ->
inductive,leftno,tys,att,n
| _ -> prerr_endline "get_checked_indtys on a non ind 2"; assert false)
| _ -> prerr_endline "get_checked_indtys on a non ind"; assert false
;;
let get_checked_fixes_or_cofixes = function
- | NReference.Ref (uri, (NReference.Fix (fixno,_,_)|NReference.CoFix fixno))->
+ | Ref.Ref (uri, (Ref.Fix (fixno,_,_)|Ref.CoFix fixno))->
(match get_checked_obj uri with
- | _,height,_,_, NCic.Fixpoint (_,funcs,att) ->
+ | _,height,_,_, C.Fixpoint (_,funcs,att) ->
funcs, att, height
| _ ->prerr_endline "get_checked_(co)fix on a non (co)fix 2";assert false)
- | r -> prerr_endline ("get_checked_(co)fix on " ^ NReference.string_of_reference r); assert false
-;;
-
-let get_indty_leftno = function
- | 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)
- | _ -> prerr_endline "get_indty_leftno called on a non indty";assert false
+ | r -> prerr_endline ("get_checked_(co)fix on " ^ Ref.string_of_reference r); assert false
;;
-let get_relevance (NReference.Ref (_, infos) as r) =
+let get_relevance (Ref.Ref (_, infos) as r) =
match infos with
- NReference.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
- | NReference.Decl -> let res,_,_,_,_ = get_checked_decl r in res
- | NReference.Ind _ ->
+ Ref.Def _ -> let res,_,_,_,_,_ = get_checked_def r in res
+ | Ref.Decl -> let res,_,_,_,_ = get_checked_decl r in res
+ | Ref.Ind _ ->
let _,_,tl,_,n = get_checked_indtys r in
let res,_,_,_ = List.nth tl n in
res
- | NReference.Con (_,i) ->
+ | Ref.Con (_,i,_) ->
let _,_,tl,_,n = get_checked_indtys r in
let _,_,_,cl = List.nth tl n in
let res,_,_ = List.nth cl (i - 1) in
res
- | NReference.Fix (fixno,_,_)
- | NReference.CoFix fixno ->
+ | Ref.Fix (fixno,_,_)
+ | Ref.CoFix fixno ->
let fl,_,_ = get_checked_fixes_or_cofixes r in
let res,_,_,_,_ = List.nth fl fixno in
res
NReference.reference ->
NCic.inductiveFun list * NCic.f_attr * int
-val get_indty_leftno: NReference.reference -> int
-
val invalidate: unit -> unit
val set_typecheck_obj: (NCic.obj -> unit) -> unit
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
(* $Id$ *)
-(* TODO unify exceptions *)
+module C = NCic
+module Ref = NReference
-module type Strategy =
- sig
+module type Strategy = sig
type stack_term
type env_term
- type config = int * env_term list * NCic.term * stack_term list
+ type config = int * env_term list * C.term * stack_term list
val to_env :
- reduce: (config -> config) ->
- unwind: (config -> NCic.term) ->
- config -> env_term
+ reduce: (config -> config) -> unwind: (config -> C.term) ->
+ config -> env_term
val from_stack : stack_term -> config
val from_stack_list_for_unwind :
- unwind: (config -> NCic.term) ->
- stack_term list -> NCic.term list
+ unwind: (config -> C.term) -> stack_term list -> C.term list
val from_env : env_term -> config
val from_env_for_unwind :
- unwind: (config -> NCic.term) ->
- env_term -> NCic.term
+ unwind: (config -> C.term) -> env_term -> C.term
val stack_to_env :
- reduce: (config -> config) ->
- unwind: (config -> NCic.term) ->
- stack_term -> env_term
+ reduce: (config -> config) -> unwind: (config -> C.term) ->
+ stack_term -> env_term
val compute_to_env :
- reduce: (config -> config) ->
- unwind: (config -> NCic.term) ->
- int -> env_term list ->
- NCic.term -> env_term
+ reduce: (config -> config) -> unwind: (config -> C.term) ->
+ int -> env_term list -> C.term -> env_term
val compute_to_stack :
- reduce: (config -> config) ->
- unwind: (config -> NCic.term) ->
- config -> stack_term
+ reduce: (config -> config) -> unwind: (config -> C.term) ->
+ config -> stack_term
end
;;
-module CallByValueByNameForUnwind' =
- struct
- type config = int * env_term list * NCic.term * stack_term list
- and stack_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
- and env_term = config lazy_t * NCic.term lazy_t (* cbv, cbn *)
+module CallByValueByNameForUnwind' = struct
+ type config = int * env_term list * C.term * stack_term list
+ and stack_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
+ and env_term = config lazy_t * C.term lazy_t (* cbv, cbn *)
let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c)
let from_stack (c,_) = Lazy.force c
let from_stack_list_for_unwind ~unwind:_ l =
end
;;
-
-(* {{{ module CallByValueByNameForUnwind =
- struct
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- and stack_term = config
- and env_term = config * config (* cbv, cbn *)
- and ens_term = config * config (* cbv, cbn *)
-
- let to_env c = c,c
- let to_ens c = c,c
- let from_stack config = config
- let from_stack_list_for_unwind ~unwind l = List.map unwind l
- let from_env (c,_) = c
- let from_ens (c,_) = c
- let from_env_for_unwind ~unwind (_,c) = unwind c
- let from_ens_for_unwind ~unwind (_,c) = unwind c
- let stack_to_env ~reduce ~unwind config = reduce config, (0,[],[],unwind config,[])
- let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[]), (k,e,ens,t,[])
- let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-
-(* Old Machine *)
-module CallByNameStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = unwind k e ens t
- let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t
- end
-;;
-
-module CallByNameStrategy =
- struct
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- and stack_term = config
- and env_term = config
- and ens_term = config
-
- let to_env c = c
- let to_ens c = c
- let from_stack config = config
- let from_stack_list_for_unwind ~unwind l = List.map unwind l
- let from_env c = c
- let from_ens c = c
- let from_env_for_unwind ~unwind c = unwind c
- let from_ens_for_unwind ~unwind c = unwind c
- let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[]
- let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[]
- let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-module CallByValueStrategy =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t = reduce (k,e,ens,t,[])
- end
-;;
-
-module CallByValueStrategyByNameOnConstants =
- struct
- type stack_term = Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind v = v
- let from_stack_list ~unwind l = l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens =
- function
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- end
-;;
-
-module LazyCallByValueStrategy =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let from_env_for_unwind ~unwind v = Lazy.force v
- let from_ens_for_unwind ~unwind v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- let compute_to_env ~reduce ~unwind k e ens t = lazy (reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByValueStrategyByNameOnConstants =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let from_env_for_unwind ~unwind v = Lazy.force v
- let from_ens_for_unwind ~unwind v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[]))
- let compute_to_env ~reduce ~unwind k e ens t =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[]))
- end
-;;
-
-module LazyCallByNameStrategy =
- struct
- type stack_term = Cic.term lazy_t
- type env_term = Cic.term lazy_t
- type ens_term = Cic.term lazy_t
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = lazy v
- let to_ens v = lazy v
- let from_stack ~unwind v = Lazy.force v
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = Lazy.force v
- let from_ens v = Lazy.force v
- let from_env_for_unwind ~unwind v = Lazy.force v
- let from_ens_for_unwind ~unwind v = Lazy.force v
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- let compute_to_env ~reduce ~unwind k e ens t = lazy (unwind k e ens t)
- end
-;;
-
-module
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns
-=
- struct
- type stack_term = reduce:bool -> Cic.term
- type env_term = reduce:bool -> Cic.term
- type ens_term = reduce:bool -> Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v =
- let value = lazy v in
- fun ~reduce -> Lazy.force value
- let to_ens v =
- let value = lazy v in
- fun ~reduce -> Lazy.force value
- let from_stack ~unwind v = (v ~reduce:false)
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = (v ~reduce:true)
- let from_ens v = (v ~reduce:true)
- let from_env_for_unwind ~unwind v = (v ~reduce:true)
- let from_ens_for_unwind ~unwind v = (v ~reduce:true)
- let stack_to_env ~reduce ~unwind v = v
- let compute_to_stack ~reduce ~unwind k e ens t =
- let svalue =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- ) in
- let lvalue =
- lazy (unwind k e ens t)
- in
- fun ~reduce ->
- if reduce then Lazy.force svalue else Lazy.force lvalue
- let compute_to_env ~reduce ~unwind k e ens t =
- let svalue =
- lazy (
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- ) in
- let lvalue =
- lazy (unwind k e ens t)
- in
- fun ~reduce ->
- if reduce then Lazy.force svalue else Lazy.force lvalue
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsStrategy =
- struct
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- and stack_term = config
- and env_term = config
- and ens_term = config
-
- let to_env config = config
- let to_ens config = config
- let from_stack config = config
- let from_stack_list_for_unwind ~unwind l = List.map unwind l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind config = unwind config
- let from_ens_for_unwind ~unwind config = unwind config
- let stack_to_env ~reduce ~unwind config = reduce config
- let compute_to_env ~reduce ~unwind k e ens t = (k,e,ens,t,[])
- let compute_to_stack ~reduce ~unwind config = config
- end
-;;
-
-module ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy =
- struct
- type stack_term =
- int * Cic.term list * Cic.term Cic.explicit_named_substitution * Cic.term
- type env_term = Cic.term
- type ens_term = Cic.term
- type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list
- let to_env v = v
- let to_ens v = v
- let from_stack ~unwind (k,e,ens,t) = unwind k e ens t
- let from_stack_list ~unwind l = List.map (from_stack ~unwind) l
- let from_env v = v
- let from_ens v = v
- let from_env_for_unwind ~unwind v = v
- let from_ens_for_unwind ~unwind v = v
- let stack_to_env ~reduce ~unwind (k,e,ens,t) =
- match t with
- Cic.Const _ as t -> unwind k e ens t
- | t -> reduce (k,e,ens,t,[])
- let compute_to_env ~reduce ~unwind k e ens t =
- unwind k e ens t
- let compute_to_stack ~reduce ~unwind k e ens t = (k,e,ens,t)
- end
-;;
-
-}}} *)
-
-module Reduction(RS : Strategy) =
- struct
+module Reduction(RS : Strategy) = struct
type env = RS.env_term list
type stack = RS.stack_term list
- type config = int * env * NCic.term * stack
+ type config = int * env * C.term * stack
let rec unwind (k,e,t,s) =
let t =
(RS.from_env_for_unwind ~unwind) e t
in
if s = [] then t
- else NCic.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
+ else C.Appl(t::(RS.from_stack_list_for_unwind ~unwind s))
;;
let list_nth l n = try List.nth l n with Failure _ -> assert false;;
let rec reduce ~delta ?(subst = []) context : config -> config =
let rec aux = function
- | k, e, NCic.Rel n, s when n <= k ->
+ | k, e, C.Rel n, s when n <= k ->
let k',e',t',s' = RS.from_env (list_nth e (n-1)) in
aux (k',e',t',s'@s)
- | k, _, NCic.Rel n, s as config (* when n > k *) ->
+ | k, _, C.Rel n, s as config (* when n > k *) ->
let x= try Some (List.nth context (n - 1 - k)) with Failure _ -> None in
(match x with
- | Some(_,NCic.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
+ | Some(_,C.Def(x,_)) -> aux (0,[],NCicSubstitution.lift (n - k) x,s)
| _ -> config)
- | (k, e, NCic.Meta (n,l), s) as config ->
+ | (k, e, C.Meta (n,l), s) as config ->
(try
let _,_, term,_ = NCicUtils.lookup_subst n subst in
aux (k, e, NCicSubstitution.subst_meta l term,s)
with NCicUtils.Subst_not_found _ -> config)
- | (_, _, NCic.Implicit _, _) -> assert false
- | (_, _, NCic.Sort _, _)
- | (_, _, NCic.Prod _, _)
- | (_, _, NCic.Lambda _, []) as config -> config
- | (k, e, NCic.Lambda (_,_,t), p::s) ->
+ | (_, _, C.Implicit _, _) -> assert false
+ | (_, _, C.Sort _, _)
+ | (_, _, C.Prod _, _)
+ | (_, _, C.Lambda _, []) as config -> config
+ | (k, e, C.Lambda (_,_,t), p::s) ->
aux (k+1, (RS.stack_to_env ~reduce:aux ~unwind p)::e, t,s)
- | (k, e, NCic.LetIn (_,_,m,t), s) ->
+ | (k, e, C.LetIn (_,_,m,t), s) ->
let m' = RS.compute_to_env ~reduce:aux ~unwind k e m in
aux (k+1, m'::e, t, s)
- | (_, _, NCic.Appl [], _) -> assert false
- | (k, e, NCic.Appl (he::tl), s) ->
+ | (_, _, C.Appl ([]|[_]), _) -> assert false
+ | (k, e, C.Appl (he::tl), s) ->
let tl' =
List.map (fun t->RS.compute_to_stack ~reduce:aux ~unwind (k,e,t,[])) tl
in
aux (k, e, he, tl' @ s)
- | (_, _, NCic.Const
- (NReference.Ref (_,NReference.Def height) as refer), s) as config ->
+ | (_, _, C.Const
+ (Ref.Ref (_,Ref.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 (_,
- (NReference.Decl|NReference.Ind _|NReference.Con _|NReference.CoFix _))), _) as config -> config
- | (_, _, NCic.Const (NReference.Ref
- (_,NReference.Fix (fixno,recindex,height)) as refer),s) as config ->
+ | (_, _, C.Const (Ref.Ref (_,
+ (Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config -> config
+ | (_, _, C.Const (Ref.Ref
+ (_,Ref.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))
| 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 ->
+ | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c ->
let new_s =
replace recindex s (RS.compute_to_stack ~reduce:aux ~unwind c)
in
let _,_,_,_,body = List.nth fixes fixno in
aux (0, [], body, new_s)
| _ -> config)
- | (k, e, NCic.Match (_,_,term,pl),s) as config ->
+ | (k, e, C.Match (_,_,term,pl),s) as config ->
let decofix = function
- | (_,_,NCic.Const(NReference.Ref(_,NReference.CoFix c)as refer),s)->
+ | (_,_,C.Const(Ref.Ref(_,Ref.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))),[]) ->
+ | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
aux (k, e, List.nth pl (j-1), s)
- | (_, _, NCic.Const
- (NReference.Ref (_,NReference.Con (_,j)) as refer), s') ->
- let leftno = NCicEnvironment.get_indty_leftno refer in
- let _,params = HExtlib.split_nth leftno s' in
+ | (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')->
+ let _,params = HExtlib.split_nth lno s' in
aux (k, e, List.nth pl (j-1), params@s)
| _ -> config)
in
;;
-(* {{{ ROTTO = rompe l'unificazione poiche' riduce gli argomenti di un'applicazione
- senza ridurre la testa
-module R = Reduction CallByNameStrategy;; OK 56.368s
-module R = Reduction CallByValueStrategy;; ROTTO
-module R = Reduction CallByValueStrategyByNameOnConstants;; ROTTO
-module R = Reduction LazyCallByValueStrategy;; ROTTO
-module R = Reduction LazyCallByValueStrategyByNameOnConstants;; ROTTO
-module R = Reduction LazyCallByNameStrategy;; OK 0m56.398s
-module R = Reduction
- LazyCallByValueByNameOnConstantsWhenFromStack_ByNameStrategyWhenFromEnvOrEns;;
- OK 59.058s
-module R = Reduction ClosuresOnStackByValueFromEnvOrEnsStrategy;; OK 58.583s
-module R = Reduction
- ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
-module R = Reduction(CallByValueByNameForUnwind);;
-module R = Reduction(CallByNameStrategy);;
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;}}} *)
module RS = CallByValueByNameForUnwind';;
-
module R = Reduction(RS);;
-module U = UriManager;;
let whd = R.whd
-(*
-let whd =
- let profiler_whd = HExtlib.profile ~enable:profile "are_convertible.whd" in
- fun ?(delta=true) ?(subst=[]) context t ->
- profiler_whd.HExtlib.profile (whd ~delta ~subst context) t
-*)
-
-(* mimic ocaml (<< 3.08) "=" behaviour. Tests physical equality first then
- * fallbacks to structural equality *)
let (===) x y = Pervasives.compare x y = 0 ;;
-module C = NCic
-
(* t1, t2 must be well-typed *)
let are_convertible whd ?(subst=[]) =
let rec aux test_eq_only context t1 t2 =
| (C.Match (ref1,outtype1,term1,pl1),
C.Match (ref2,outtype2,term2,pl2)) ->
- NReference.eq ref1 ref2 &&
+ Ref.eq ref1 ref2 &&
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
true
else
let height_of = function
- | NCic.Const (NReference.Ref (_,NReference.Def h))
- | NCic.Const (NReference.Ref (_,NReference.Fix (_,_,h)))
- | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Def h))::_)
- | NCic.Appl(NCic.Const(NReference.Ref(_,NReference.Fix (_,_,h)))::_) -> h
+ | C.Const (Ref.Ref (_,Ref.Def h))
+ | C.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
+ | C.Appl(C.Const(Ref.Ref(_,Ref.Def h))::_)
+ | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
| _ -> 0
in
let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
| _, 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 (_, NReference.Def height) as re), _
+ | _, C.Const (Ref.Ref (_, Ref.Def height) as re), _
when delta <= height ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def re in
head_beta_reduce ~upto ~delta bo l
(* $Id$ *)
+module C = NCic
+module Ref = NReference
+
let debug_print = fun _ -> ();;
let lift_from k n =
let rec liftaux k = function
- | NCic.Rel m as t -> if m < k then t else NCic.Rel (m + n)
- | NCic.Meta (i,(m,l)) as t when k <= m ->
- if n = 0 then t else NCic.Meta (i,(m+n,l))
- | NCic.Meta (_,(m,NCic.Irl l)) as t when k > l + m -> t
- | NCic.Meta (i,(m,l)) ->
+ | C.Rel m as t -> if m < k then t else C.Rel (m + n)
+ | C.Meta (i,(m,l)) as t when k <= m ->
+ if n = 0 then t else C.Meta (i,(m+n,l))
+ | C.Meta (_,(m,C.Irl l)) as t when k > l + m -> t
+ | C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
- NCic.Meta (i, (m, NCic.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
- | NCic.Implicit _ -> (* was the identity *) assert false
+ C.Meta (i, (m, C.Ctx (HExtlib.sharing_map (liftaux (k-m)) lctx)))
+ | C.Implicit _ -> (* was the identity *) assert false
| t -> NCicUtils.map (fun _ k -> k + 1) k liftaux t
in
liftaux k
let rec psubst ?(avoid_beta_redexes=false) map_arg args =
let nargs = List.length args in
let rec substaux k = function
- | NCic.Rel n as t ->
+ | C.Rel n as t ->
(match n with
| n when n >= (k+nargs) ->
- if nargs <> 0 then NCic.Rel (n - nargs) else t
+ if nargs <> 0 then C.Rel (n - nargs) else t
| n when n < k -> t
| n (* k <= n < k+nargs *) ->
(try lift (k-1) (map_arg (List.nth args (n-k)))
with Failure _ -> assert false))
- | NCic.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
- if nargs <> 0 then NCic.Meta (i,(m-nargs,l)) else t
- | NCic.Meta (i,(m,(NCic.Irl l as irl))) as t when k > l + m ->
- if nargs <> 0 then NCic.Meta (i,(m-nargs,irl)) else t
- | NCic.Meta (i,(m,l)) ->
+ | C.Meta (i,(m,l)) as t when m >= k + nargs - 1 ->
+ if nargs <> 0 then C.Meta (i,(m-nargs,l)) else t
+ | C.Meta (i,(m,(C.Irl l as irl))) as t when k > l + m ->
+ if nargs <> 0 then C.Meta (i,(m-nargs,irl)) else t
+ | C.Meta (i,(m,l)) ->
let lctx = NCicUtils.expand_local_context l in
(* 1-nargs < k-m, when <= 0 is still reasonable because we will
* substitute args[ k-m ... k-m+nargs-1 > 0 ] *)
- NCic.Meta (i,(m, NCic.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
- | NCic.Implicit _ -> assert false (* was identity *)
- | NCic.Appl (he::tl) as t ->
+ C.Meta (i,(m, C.Ctx (HExtlib.sharing_map (substaux (k-m)) lctx)))
+ | C.Implicit _ -> assert false (* was identity *)
+ | C.Appl (he::tl) as t ->
(* Invariant: no Appl applied to another Appl *)
let rec avoid he' = function
| [] -> he'
| arg::tl' as args->
(match he' with
- | NCic.Appl l -> NCic.Appl (l@args)
- | NCic.Lambda (_,_,bo) when avoid_beta_redexes ->
+ | C.Appl l -> C.Appl (l@args)
+ | C.Lambda (_,_,bo) when avoid_beta_redexes ->
(* map_arg is here \x.x, Obj magic is needed because
* we don't have polymorphic recursion w/o records *)
avoid (psubst
~avoid_beta_redexes Obj.magic [Obj.magic arg] bo) tl'
- | _ -> if he == he' && args == tl then t else NCic.Appl (he'::args))
+ | _ -> if he == he' && args == tl then t else C.Appl (he'::args))
in
let tl = HExtlib.sharing_map (substaux k) tl in
avoid (substaux k he) tl
(* [t_i] is lifted as usual when it crosses an abstraction *)
(* subst_meta (n, Non) t -> lift n t *)
let subst_meta = function
- | m, NCic.Irl _
- | m, NCic.Ctx [] -> lift m
- | m, NCic.Ctx l -> psubst (lift m) l
+ | m, C.Irl _
+ | m, C.Ctx [] -> lift m
+ | m, C.Ctx l -> psubst (lift m) l
;;
(* $Id$ *)
module C = NCic
-module R = NCicReduction
module Ref = NReference
+module R = NCicReduction
module S = NCicSubstitution
module U = NCicUtils
module E = NCicEnvironment
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
+(*
let raise = function
| TypeCheckerFailure s as e -> prerr_endline (Lazy.force s); raise e
| e -> raise e
;;
+*)
type recf_entry =
| Evil of int (* rno *)
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.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 len = List.length context in
let context_dcl =
match E.get_checked_obj r_uri with
- | _,_,_,_, NCic.Inductive (_,_,tys,_) ->
+ | _,_,_,_, C.Inductive (_,_,tys,_) ->
context @ List.map (fun (_,name,arity,_) -> name,C.Decl arity) tys
| _ -> assert false
in
let dummy = C.Sort C.Prop 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
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 =
) 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.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 ->
- let _, paramsno, _, _, _ = E.get_checked_indtys ref in
+ | C.Appl (C.Const (Ref.Ref (uri, Ref.Con (_,j,paramsno))) :: tl) as t ->
let ty_t = typeof ~subst ~metasenv context t in
let dc_ctx, dcl, start, stop =
specialize_and_abstract_constrs ~subst indURI indlen context ty_t in
| C.Appl []
| C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
| C.Meta _ -> true
- | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_)),outtype,term,pl) ->
+ | C.Match (Ref.Ref (uri,Ref.Ind (isinductive,_,_)),outtype,term,pl) ->
(match term with
| C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
if not isinductive then
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) ->
raise (TypeCheckerFailure (lazy "Inconsistent cached infos in reference"))
in
match E.get_checked_obj uri, ref with
- | (_,_,_,_,C.Inductive (isind1,_,tl,_)), Ref.Ref (_,Ref.Ind (isind2,i)) ->
+ | (_,_,_,_,C.Inductive(isind1,lno1,tl,_)),Ref.Ref(_,Ref.Ind (isind2,i,lno2))->
if isind1 <> isind2 then error ();
+ if lno1 <> lno2 then error ();
let _,_,arity,_ = List.nth tl i in arity
- | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j)) ->
+ | (_,_,_,_,C.Inductive (_,lno1,tl,_)), Ref.Ref (_,Ref.Con (i,j,lno2)) ->
+ if lno1 <> lno2 then error ();
let _,_,_,cl = List.nth tl i in
let _,_,arity = List.nth cl (j-1) in
arity
"the type of the definiens for %s in the context is not "^^
"convertible with the declared one.\n"^^
"inferred type:\n%s\nexpected type:\n%s")
- name
- (PP.ppterm ~subst ~metasenv ~context ty')
+ name (PP.ppterm ~subst ~metasenv ~context ty')
(PP.ppterm ~subst ~metasenv ~context ty))))
end;
d::context
(* $Id$ *)
+module C = NCic
+module Ref = NReference
+
exception Subst_not_found of int
exception Meta_not_found of int
let expand_local_context = function
- | NCic.Irl len ->
+ | C.Irl len ->
let rec aux acc = function
| 0 -> acc
- | n -> aux (NCic.Rel n::acc) (n-1)
+ | n -> aux (C.Rel n::acc) (n-1)
in
aux [] len
- | NCic.Ctx lctx -> lctx
+ | C.Ctx lctx -> lctx
;;
let lookup_subst n subst =
;;
let fold g k f acc = function
- | NCic.Meta _ -> assert false
- | NCic.Implicit _
- | NCic.Sort _
- | NCic.Const _
- | NCic.Rel _ -> acc
- | NCic.Appl [] | NCic.Appl [_] -> assert false
- | NCic.Appl l -> List.fold_left (f k) acc l
- | NCic.Prod (n,s,t)
- | NCic.Lambda (n,s,t) -> f (g (n,NCic.Decl s) k) (f k acc s) t
- | NCic.LetIn (n,ty,t,bo) -> f (g (n,NCic.Def (t,ty)) k) (f k (f k acc ty) t) bo
- | NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
+ | C.Meta _ -> assert false
+ | C.Implicit _
+ | C.Sort _
+ | C.Const _
+ | C.Rel _ -> acc
+ | C.Appl [] | C.Appl [_] -> assert false
+ | C.Appl l -> List.fold_left (f k) acc l
+ | C.Prod (n,s,t)
+ | C.Lambda (n,s,t) -> f (g (n,C.Decl s) k) (f k acc s) t
+ | C.LetIn (n,ty,t,bo) -> f (g (n,C.Def (t,ty)) k) (f k (f k acc ty) t) bo
+ | C.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
;;
let map g k f = function
- | NCic.Meta _ -> assert false
- | NCic.Implicit _
- | NCic.Sort _
- | NCic.Const _
- | NCic.Rel _ as t -> t
- | NCic.Appl [] | NCic.Appl [_] -> assert false
- | NCic.Appl l as orig ->
+ | C.Meta _ -> assert false
+ | C.Implicit _
+ | C.Sort _
+ | C.Const _
+ | C.Rel _ as t -> t
+ | C.Appl [] | C.Appl [_] -> assert false
+ | C.Appl l as orig ->
(match HExtlib.sharing_map (f k) l with
- | NCic.Appl l :: tl -> NCic.Appl (l@tl)
+ | C.Appl l :: tl -> C.Appl (l@tl)
| l1 when l == l1 -> orig
- | l1 -> NCic.Appl l1)
- | NCic.Prod (n,s,t) as orig ->
- let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
- if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
- | NCic.Lambda (n,s,t) as orig ->
- let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
- if t1 == t && s1 == s then orig else NCic.Lambda (n,s1,t1)
- | NCic.LetIn (n,ty,t,b) as orig ->
+ | l1 -> C.Appl l1)
+ | C.Prod (n,s,t) as orig ->
+ let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+ if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
+ | C.Lambda (n,s,t) as orig ->
+ let s1 = f k s in let t1 = f (g (n,C.Decl s) k) t in
+ if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
+ | C.LetIn (n,ty,t,b) as orig ->
let ty1 = f k ty in let t1 = f k t in
- let b1 = f (g (n,NCic.Def (t,ty)) k) b in
- if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1)
- | NCic.Match (r,oty,t,pl) as orig ->
+ let b1 = f (g (n,C.Def (t,ty)) k) b in
+ if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
+ | C.Match (r,oty,t,pl) as orig ->
let oty1 = f k oty in let t1 = f k t in let pl1 = HExtlib.sharing_map (f k) pl in
if oty1 == oty && t1 == t && pl1 == pl then orig
- else NCic.Match(r,oty1,t1,pl1)
+ else C.Match(r,oty1,t1,pl1)
;;
| 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 *)
+ | Ind of bool * int * int (* inductive, indtyno, leftno *)
+ | Con of int * int * int (* indtyno, constrno, leftno *)
type reference = Ref of NUri.uri * spec
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 j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
i,j
in
+*)
let get1 s dot =
let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
i
| "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))
+ | "ind" -> let b,i,l = get3 s dot in Ref (u, Ind (b=1,i,l))
+ | "con" -> let i,j,l = get3 s dot in Ref (u, Con (i,j,l))
| _ -> raise Not_found
with Not_found -> raise (IllFormedReference (lazy s))
in
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 ^ ")"
+ | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^
+ "," ^ string_of_int l ^ ")"
+ | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^
+ "," ^ string_of_int l ^ ")"
;;
let mk_constructor j = function
- | Ref (u, Ind (_,i)) ->
- reference_of_string (string_of_reference (Ref (u, Con (i,j))))
+ | Ref (u, Ind (_,i,l)) ->
+ reference_of_string (string_of_reference (Ref (u, Con (i,j,l))))
| _ -> assert false
;;
type spec =
| Decl
- | Def of int (* height *)
- | Fix of int * int * int (* fixno, recparamno, height *)
+ | 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 *)
+ | Ind of bool * int * int (* inductive, indtyno, leftno *)
+ | Con of int * int * int (* indtyno, constrno, leftno *)
type reference = private Ref of NUri.uri * spec
NCic.Const (reference_of_ouri curi Ref.Decl)
| _ -> assert false)
| Cic.MutInd (curi, tyno, ens) ->
- let is_inductive =
+ let is_inductive, lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false
in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
| Cic.MutConstruct (curi, tyno, consno, ens) ->
+ let lno =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.InductiveDefinition (_,_,lno,_) -> lno
+ | _ -> assert false
+ in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
| Cic.Var (curi, ens) ->
(match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
Cic.Variable (_,Some bo,_,_,_) ->
aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
| _ -> assert false)
| Cic.MutCase (curi, tyno, outty, t, branches) ->
- let is_inductive =
+ let is_inductive,lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false in
- let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+ let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
let t, fixpoints_t = aux k octx ctx n_fix uri t in
let branches, fixpoints =
projects / helm.git / commitdiff