1
1
(************************************************************************)
2
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
3
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4
4
(* \VV/ **************************************************************)
5
5
(* // * This file is distributed under the terms of the *)
6
6
(* * GNU Lesser General Public License Version 2.1 *)
7
7
(************************************************************************)
9
(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *)
9
(* $Id: constrintern.ml 14656 2011-11-16 08:46:31Z herbelin $ *)
322
322
with Not_found -> RHole (loc, Evd.BinderType na))
325
let reset_hidden_inductive_implicit_test (ltacvars,namedctxvars,ntnvars,impls) =
326
let f = function id,(Inductive _,b,c,d) -> id,(Inductive [],b,c,d) | x -> x in
327
(ltacvars,namedctxvars,ntnvars,List.map f impls)
325
329
let check_hidden_implicit_parameters id (_,_,_,impls) =
326
330
if List.exists (function
327
331
| (_,(Inductive indparams,_,_,_)) -> List.mem id indparams
461
465
let renaming' = if id=id' then renaming else (id,id')::renaming in
462
466
(renaming',env), Name id'
468
let make_letins loc = List.fold_right (fun (na,b,t) c -> RLetIn (loc,na,b,c))
470
let rec subordinate_letins letins = function
471
(* binders come in reverse order; the non-let are returned in reverse order together *)
472
(* with the subordinated let-in in writing order *)
473
| (na,_,Some b,t)::l ->
474
subordinate_letins ((na,b,t)::letins) l
475
| (na,bk,None,t)::l ->
476
let letins',rest = subordinate_letins [] l in
477
letins',((na,bk,t),letins)::rest
464
481
let rec subst_iterator y t = function
465
482
| RVar (_,id) as x -> if id = y then t else x
466
483
| x -> map_rawconstr (subst_iterator y t) x
505
522
(* All elements of the list are in scopes (scopt,subscopes) *)
506
523
let (bl,(scopt,subscopes)) = List.assoc x binders in
507
524
let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in
525
let letins,bl = subordinate_letins [] bl in
508
526
let termin = aux subst' (renaming,env) terminator in
509
List.fold_left (fun t binder ->
527
let res = List.fold_left (fun t binder ->
510
528
subst_iterator ldots_var t
511
529
(aux (terms,Some(x,binder)) subinfos iter))
531
make_letins loc letins res
513
532
with Not_found ->
514
533
anomaly "Inconsistent substitution of recursive notation")
515
534
| AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
516
let (na,bk,_,t) = snd (Option.get binderopt) in
517
RProd (loc,na,bk,t,aux subst' infos c')
535
let (na,bk,t),letins = snd (Option.get binderopt) in
536
RProd (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
518
537
| ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
519
let (na,bk,_,t) = snd (Option.get binderopt) in
520
RLambda (loc,na,bk,t,aux subst' infos c')
538
let (na,bk,t),letins = snd (Option.get binderopt) in
539
RLambda (loc,na,bk,t,make_letins loc letins (aux subst' infos c'))
522
541
rawconstr_of_aconstr_with_binders loc (traverse_binder subst)
523
542
(aux subst') subinfos t
846
865
if List.length pats < nvars then error_not_enough_arguments loc;
847
866
let pats1,pats2 = list_chop nvars pats in
848
867
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) vars pats1 in
849
let idspl1 = List.map (subst_cases_pattern loc (alias_of aliases) f (subst,[]) scopes) args in
868
let idspl1 = List.map (subst_cases_pattern loc Anonymous f (subst,[]) scopes) args in
850
869
cstr, idspl1, pats2
851
870
| _ -> raise Not_found)
1242
1261
let tms,env' = List.fold_right
1243
1262
(fun citm (inds,env) ->
1244
1263
let (tm,ind),nal = intern_case_item env citm in
1245
(tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
1264
(tm,ind)::inds,List.fold_left
1265
(push_name_env (reset_hidden_inductive_implicit_test lvar))
1246
1267
tms ([],env) in
1247
1268
let rtnpo = Option.map (intern_type env') rtnpo in
1248
1269
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
1251
1272
let env' = reset_tmp_scope env in
1252
1273
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
1253
1274
let p' = Option.map (fun p ->
1254
let env'' = List.fold_left (push_name_env lvar) env ids in
1275
let env'' = List.fold_left
1276
(push_name_env (reset_hidden_inductive_implicit_test lvar))
1255
1278
intern_type env'' p) po in
1256
1279
RLetTuple (loc, List.map snd nal, (na', p'), b',
1257
1280
intern (List.fold_left (push_name_env lvar) env nal) c)
1259
1282
let env' = reset_tmp_scope env in
1260
1283
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
1261
1284
let p' = Option.map (fun p ->
1262
let env'' = List.fold_left (push_name_env lvar) env ids in
1285
let env'' = List.fold_left
1286
(push_name_env (reset_hidden_inductive_implicit_test lvar))
1263
1288
intern_type env'' p) po in
1264
1289
RIf (loc, c', (na', p'), intern env b1, intern env b2)
1265
1290
| CHole (loc, k) ->
added
removed
interp/constrintern.ml
