in
let x = List.nth tl cpos in
let _,rest =
- try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[]
+ try HExtlib.split_nth "AC 1" (cpos + sats +1) tl with Failure _ -> [],[]
in
if rest = [] then
acic2content
| Some (_,_,_,sats,cpos) ->
if cpos < List.length tl then
let _,rest =
- try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[]
+ try HExtlib.split_nth "TAC 1" (cpos+sats+1) tl with Failure _ -> [],[]
in
if rest = [] then
idref aid (List.nth (List.map k tl) cpos)
let split2_last l1 l2 =
try
let n = pred (List.length l1) in
- let before1, after1 = HEL.split_nth n l1 in
- let before2, after2 = HEL.split_nth n l2 in
+ let before1, after1 = HEL.split_nth "P2 1" n l1 in
+ let before2, after2 = HEL.split_nth "P2 2" n l2 in
before1, before2, List.hd after1, List.hd after2
with Invalid_argument _ -> failwith "A2P.split2_last"
let qs = proc_bkd_proofs (next st) synth names classes ts in
let lpsno, _ = H.get_ind_type uri tyno in
let ps, _ = H.get_ind_parameters st.context (H.cic v) in
- let _, rps = HEL.split_nth lpsno ps in
+ let _, rps = HEL.split_nth "P2 3" lpsno ps in
let rpsno = List.length rps in
let e = Cn.mk_pattern rpsno u in
let text = "" in
let classes, conclusion = Cl.classify c (H.get_type "opt_appl 3" c t) in
let csno, vsno = List.length classes, List.length vs in
if csno < vsno then
- let vvs, vs = HEL.split_nth csno vs in
+ let vvs, vs = HEL.split_nth "PO 1" csno vs in
let x = C.Appl (define c (C.Appl (t :: vvs)) :: vs) in
opt_proof g (info st "Optimizer: anticipate 2") true c x
else match conclusion, List.rev vs with
let eliminator = H.get_default_eliminator c uri tyno outty in
let lpsno, (_, _, _, constructors) = H.get_ind_type uri tyno in
let ps, sort_disp = H.get_ind_parameters c arg in
- let lps, rps = HEL.split_nth lpsno ps in
+ let lps, rps = HEL.split_nth "PO 2" lpsno ps in
let rpsno = List.length rps in
if rpsno = 0 && sort_disp = 0 then
(* FG: the transformation is not possible, we fall back into the plain case *)
let vty = match vty with
| C.Appl (C.MutInd (fu, fm, _) as hd :: args)
when UM.eq fu u && fm = m && List.length args = psno ->
- let largs, _ = X.split_nth lpsno args in
+ let largs, _ = X.split_nth "D 1" lpsno args in
C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)
| _ ->
assert false
C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
dummy
| C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
- let _, rargs = HExtlib.split_nth leftno tl in
+ let _, rargs = HExtlib.split_nth "TC 1" leftno tl in
if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
| C.Cast (te,ty) -> subst_inductive_type_with_dummy te
| C.Prod (name,so,ta) ->
let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
| Cic.InductiveDefinition (tl,_,paramsno,_) ->
- let left_args,_ = HExtlib.split_nth paramsno args in
+ let left_args,_ = HExtlib.split_nth "TC 2" paramsno args in
List.map (fun (name, isind, arity, cl) ->
let arity = CicSubstitution.subst_vars exp arity in
let arity = instantiate_parameters left_args arity in
("Too many args for constructor: " ^ String.concat " "
(List.map (fun x-> CicPp.ppterm x) args))))
in
- let left, args = HExtlib.split_nth paramsno tl in
+ let left, args = HExtlib.split_nth "TC 3" paramsno tl in
List.for_all (does_not_occur ~subst context n nn) left &&
analyse_instantiated_type rec_params args
| C.Appl ((C.MutCase (_,_,out,te,pl))::_)
let get_l_r_p n = function
| Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
| Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
- HExtlib.split_nth n args
+ HExtlib.split_nth "R 1" n args
| _ -> assert false
in
let _, _, ty, cl = List.nth tl tyno in
(CR.head_beta_reduce ~delta:false
(Cic.Appl [outty;k])))),k
| Cic.Appl (Cic.MutInd _::pl) ->
- let left_p,right_p = HExtlib.split_nth leftno pl in
+ let left_p,right_p = HExtlib.split_nth "R 2" leftno pl in
let has_rights = right_p <> [] in
let k =
let k = Cic.MutConstruct (uri,tyno,i,[]) in
CicUniv.oblivion_ugraph
with
| Cic.Appl (Cic.MutInd _::args),_ ->
- snd (HExtlib.split_nth leftno args)
+ snd (HExtlib.split_nth "R 3" leftno args)
| _ -> assert false
with CicTypeChecker.TypeCheckerFailure _-> assert false
in
with
| (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
| Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
- snd (HExtlib.split_nth leftno args), mty
+ snd (HExtlib.split_nth "R 4" leftno args), mty
| _ -> assert false
with CicTypeChecker.TypeCheckerFailure _ ->
raise (AssertFailure(lazy "already ill-typed matched term"))
in
context2pres
(match skip_initial_lambdas_internal with
- Some (`Now n) -> snd (HExtlib.split_nth n p.Con.proof_context)
+ Some (`Now n) -> snd (HExtlib.split_nth "CP 1" n p.Con.proof_context)
| _ -> p.Con.proof_context)
presacontext
in
in
aux 0 l
-let split_nth n l =
+let split_nth msg n l =
let rec aux acc n l =
match n, l with
| 0, _ -> List.rev acc, l
- | n, [] -> raise (Failure "HExtlib.split_nth")
+ | n, [] -> raise (Failure ("HExtlib.split_nth: " ^ msg))
| n, hd :: tl -> aux (hd :: acc) (n - 1) tl in
aux [] n l
* @returns two list, the first contains at least n elements, the second the
* remaining ones
* @raise Failure when List.length l < n *)
-val split_nth: int -> 'a list -> 'a list * 'a list
+(* FG: first argument: error msg *)
+val split_nth: string -> int -> 'a list -> 'a list * 'a list
(** skip [n] [l] skips the first n elements of l *)
val list_skip : int -> 'a list -> 'a list
let neighbs = UriTbl.find adjlist uri in
if Lazy.lazy_is_val neighbs.adjacency then begin
let adjacency, _ =
- HExtlib.split_nth neighbs.shown (Lazy.force neighbs.adjacency)
+ HExtlib.split_nth "MD 1" neighbs.shown (Lazy.force neighbs.adjacency)
in
List.iter
(fun dest ->
UriTbl.add adjlist dest neighborhood)
adjacency;
neighbs.shown <- weight;
- fst (HExtlib.split_nth weight adjacency), weight
+ fst (HExtlib.split_nth "MD 2" weight adjacency), weight
else begin (* nodes has been expanded at least once *)
let adjacency = Lazy.force neighbs.adjacency in
let total_nodes = List.length adjacency in
let shown_before = neighbs.shown in
neighbs.shown <- min (neighbs.shown + fat_increment) total_nodes;
let new_shown = neighbs.shown - shown_before in
- (fst (HExtlib.split_nth new_shown (List.rev adjacency))), new_shown
+ (fst (HExtlib.split_nth "MD 3" new_shown (List.rev adjacency))), new_shown
end else
[], 0 (* all children are already shown *)
end
| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,_))),[]) ->
aux (k, e, List.nth pl (j-1), s)
| (_, _, C.Const (Ref.Ref (_,Ref.Con (_,j,lno))), s')->
- let _,params = HExtlib.split_nth lno s' in
+ let _,params = HExtlib.split_nth "NR 1" lno s' in
aux (k, e, List.nth pl (j-1), params@s)
| _ -> config, true)
in
let relevance = E.get_relevance r1 in
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
- let _,relevance = HExtlib.split_nth lno relevance in
+ let _,relevance = HExtlib.split_nth "NR 2" lno relevance in
HExtlib.mk_list false lno @ relevance
| _ -> relevance
in
| HExtlib.FailureAt fail ->
let relevance =
!get_relevance ~metasenv ~subst context hd1 tl1 in
- let _,relevance = HExtlib.split_nth fail relevance in
+ let _,relevance = HExtlib.split_nth "NR 3" fail relevance in
let b,relevance = (match relevance with
| [] -> assert false
| b::tl -> b,tl) in
if (not b) then
- let _,tl1 = HExtlib.split_nth (fail+1) tl1 in
- let _,tl2 = HExtlib.split_nth (fail+1) tl2 in
+ let _,tl1 = HExtlib.split_nth "NR 4" (fail+1) tl1 in
+ let _,tl2 = HExtlib.split_nth "NR 5" (fail+1) tl2 in
try
HExtlib.list_forall_default3
(fun t1 t2 b -> not b || aux true context t1 t2)
| _::tl, [] -> (false,C.Rel ~-1)::combine tl [] (* dummy term *)
| [],_::_ -> assert false
in
- let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in
+ let lefts, _ = HExtlib.split_nth "NTC 1" (min j (List.length args)) args in
List.map (fun ((b,x),i) -> b && x = C.Rel (k-i))
(HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts))
| t -> U.fold (fun _ k -> k+1) k aux acc t
| C.Appl (C.Const (Ref.Ref (_,Ref.Ind _) as ref) :: _ ) as ty ->
let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
let _, leftno, itl, _, i = E.get_checked_indtys ref in
- let left_args,_ = HExtlib.split_nth leftno args in
+ let left_args,_ = HExtlib.split_nth "NTC 2" leftno args in
let _,_,_,cl = List.nth itl i in
List.map
(fun (rel,name,ty) -> rel, name, instantiate_parameters left_args ty) cl
| 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,lno))))::tl)
when NUri.eq uri' uri ->
- let _, rargs = HExtlib.split_nth lno tl in
+ let _, rargs = HExtlib.split_nth "NTC 3" lno tl in
if rargs = [] then dummy else C.Appl (dummy :: rargs)
| t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
in
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
- let params, arguments = HExtlib.split_nth paramsno tl in
+ let params, arguments = HExtlib.split_nth "NTC 4" paramsno tl in
let lifted_params = List.map (S.lift 1) params in
let cl =
List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl
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) ->
- let _,arguments = HExtlib.split_nth leftno tl in
+ let _,arguments = HExtlib.split_nth "NTC 5" leftno tl in
C.Appl (S.lift liftno outty::arguments@[cons])
| C.Prod (name,so,de) ->
let cons =
(PP.ppterm ~subst ~metasenv ~context ty)
(PP.ppterm ~subst ~metasenv ~context (C.Const r')))))
else
- try HExtlib.split_nth leftno tl
+ try HExtlib.split_nth "NTC 6" leftno tl
with
Failure _ ->
raise (TypeCheckerFailure (lazy (Printf.sprintf
=
match l with
| shift, C.Irl n ->
- let context = snd (HExtlib.split_nth shift context) in
+ let context = snd (HExtlib.split_nth "NTC 7" shift context) in
let rec compare = function
| 0,_,[] -> ()
| 0,_,_::_
compare (n,context,canonical_context)
| shift, lc_kind ->
(* we avoid useless lifting by shortening the context*)
- let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in
+ let l,context = (0,lc_kind), snd (HExtlib.split_nth "NTC 8" shift context) in
let lifted_canonical_context =
let rec lift_metas i = function
| [] -> []
let eaten = List.length args_with_ty - res in
(C.Appl
(he::List.map fst
- (fst (HExtlib.split_nth eaten args_with_ty)))))))))
+ (fst (HExtlib.split_nth "NTC 9" eaten args_with_ty)))))))))
in
aux ty_he args_with_ty
(List.fold_right
(fun (it_relev,_,ty,cl) i ->
let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
- let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
+ let sx_context_ty_rev,_ = HExtlib.split_nth "NTC 10" leftno (List.rev context) in
List.iter
(fun (k_relev,_,te) ->
let k_relev =
- try snd (HExtlib.split_nth leftno k_relev)
+ try snd (HExtlib.split_nth "NTC 11" leftno k_relev)
with Failure _ -> k_relev in
let te = debruijn uri len [] te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =
- HExtlib.split_nth (List.length tys) (List.rev context) in
+ HExtlib.split_nth "NTC 12" (List.length tys) (List.rev context) in
let sx_context_te_rev,_ =
- HExtlib.split_nth leftno chopped_context_rev in
+ HExtlib.split_nth "NTC 13" leftno chopped_context_rev in
(try
ignore (List.fold_left2
(fun context item1 item2 ->
let bo, context' =
eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in
let new_context_part,_ =
- HExtlib.split_nth (List.length context' - List.length context)
+ HExtlib.split_nth "NTC 14" (List.length context' - List.length context)
context' in
let k = List.fold_right shift_k new_context_part new_k in
let context, recfuns, x = k in
("Too many args for constructor: " ^ String.concat " "
(List.map (fun x-> PP.ppterm ~subst ~metasenv ~context x) args))))
in
- let _, args = HExtlib.split_nth paramsno tl in
+ let _, args = HExtlib.split_nth "NTC 15" paramsno tl in
analyse_instantiated_type rec_params args
| C.Appl ((C.Match (_,out,te,pl))::_)
| C.Match (_,out,te,pl) as t ->
let eaten = List.length args - res in
(C.Appl
(t::fst
- (HExtlib.split_nth eaten args))))))))
+ (HExtlib.split_nth "NTC 16" eaten args))))))))
in aux context ty args
;;
match CicReduction.whd context tty with
Cic.MutInd (_,_,ens) -> ens,[]
| Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
- ens,fst (HExtlib.split_nth leftno args)
+ ens,fst (HExtlib.split_nth "ON 1" leftno args)
| _ -> assert false
in
let rec aux n irl context outsort =
let ind = if args = [] then C.Const r else C.Appl (C.Const r::args) in
let metasenv, subst, term, _ =
typeof_aux metasenv subst context (Some ind) term in
- let parameters, arguments = HExtlib.split_nth leftno args in
+ let parameters, arguments = HExtlib.split_nth "NR 1" leftno args in
let outtype =
match outtype with
| C.Implicit _ as ot ->
List.fold_left
(fun (metasenv,subst,res,i) (it_relev,n,ty,cl) ->
let context,ty_sort = NCicReduction.split_prods ~subst [] ~-1 ty in
- let sx_context_ty_rev,_= HExtlib.split_nth leftno (List.rev context) in
+ let sx_context_ty_rev,_= HExtlib.split_nth "NR 2" leftno (List.rev context) in
let metasenv,subst,cl =
List.fold_right
(fun (k_relev,n,te) (metasenv,subst,res) ->
let k_relev =
- try snd (HExtlib.split_nth leftno k_relev)
+ try snd (HExtlib.split_nth "NR 3" leftno k_relev)
with Failure _ -> k_relev in
let te = NCicTypeChecker.debruijn uri len [] te in
let metasenv, subst, te, _ = check_type metasenv subst tys te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =
- HExtlib.split_nth (List.length tys) (List.rev context) in
+ HExtlib.split_nth "NR 4" (List.length tys) (List.rev context) in
let sx_context_te_rev,_ =
- HExtlib.split_nth leftno chopped_context_rev in
+ HExtlib.split_nth "NR 5" leftno chopped_context_rev in
let metasenv,subst,_ =
try
List.fold_left2
| Some bo -> aux (ctx,bo))
| (name, src)::ctx, (NCic.Appl args as bo)
when HExtlib.list_last args = NCic.Rel 1 ->
- let args, _ = HExtlib.split_nth (List.length args - 1) args in
+ let args, _ = HExtlib.split_nth "NU 1" (List.length args - 1) args in
(match delift_if_not_occur (NCic.Appl args) with
| None -> aux (ctx,NCic.Lambda(name,src, bo))
| Some bo -> aux (ctx,bo))
let relevance = match r1 with
| Ref.Ref (_,Ref.Con (_,_,lno)) ->
let relevance =
- try snd (HExtlib.split_nth lno relevance)
+ try snd (HExtlib.split_nth "NU 2" lno relevance)
with Failure _ -> []
in
HExtlib.mk_list false lno @ relevance
let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
let _,_,_,cl = List.nth tl i in
let consno = List.length cl in
- let left, right = HExtlib.split_nth lno args in
+ let left, right = HExtlib.split_nth "NTS 1" lno args in
status, (ref, consno, left, right)
;;
let l_c2 = skip_appl (purge_lambdas term) in
let l_c2_b,l_c2_a =
try
- HExtlib.split_nth (c2_pis - sat2 - 1) l_c2
+ HExtlib.split_nth "CCG 1" (c2_pis - sat2 - 1) l_c2
with
Failure _ -> assert false in
let l_c1,l_c2_a =
let patterns,outtype =
match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_)->
- let left_params, right_params = HExtlib.split_nth paramsno params in
+ let left_params, right_params = HExtlib.split_nth "DT 1" paramsno params in
let _,_,_,constructor_list = List.nth ind_type_list typeno in
let i_constr_id,_ = List.nth constructor_list (consno - 1) in
let patterns =
match S.lift 1 tty with
| C.MutInd _ as tty' -> tty'
| C.Appl l ->
- let keep,abstract = HExtlib.split_nth (paramsno +1) l in
+ let keep,abstract = HExtlib.split_nth "DT 2" (paramsno +1) l in
let keep = List.map (S.lift paramsno) keep in
C.Appl (keep@mk_rels (List.length abstract))
| _ -> assert false
projects / helm.git / commitdiff