let restrict to_be_restricted =
let rec erase i n =
function
- [] -> []
- | _::tl when List.mem (n,i) to_be_restricted ->
- None::(erase (i+1) n tl)
+ [] -> []
+ | _::tl when List.mem (n,i) to_be_restricted ->
+ None::(erase (i+1) n tl)
| he::tl -> he::(erase (i+1) n tl) in
let rec aux =
function
- [] -> []
- | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
+ [] -> []
+ | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
aux
;;
C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
(*CSC: deliftato la regola per il LetIn *)
else
- (match List.nth context (m-k-1) with
- Some (_,C.Def t) -> deliftaux k (S.lift m t)
- | Some (_,C.Decl t) ->
+ (match List.nth context (m-k-1) with
+ Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t)
+ | Some (_,C.Decl t) ->
(* It may augment to_be_restricted *)
ignore (deliftaux k (S.lift m t)) ;
C.Rel ((position (m-k) l) + k)
- | None -> raise RelToHiddenHypothesis)
+ | None -> raise RelToHiddenHypothesis)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
(* First possibility: restriction *)
(* Second possibility: unification *)
(* Third possibility: convertibility *)
- R.are_convertible context t1' t2'
+ R.are_convertible context t1' t2'
) true ln lm
in
if ok then subst,metasenv else raise UnificationFailed
| (C.Meta (n,l), t)
| (t, C.Meta (n,l)) ->
let subst',metasenv' =
- try
- let oldt = (List.assoc n subst) in
- let lifted_oldt = S.lift_meta l oldt in
- fo_unif_subst subst context metasenv lifted_oldt t
- with Not_found ->
- let t',metasenv' = delift context metasenv l t in
- (n, t')::subst, metasenv'
+ try
+ let oldt = (List.assoc n subst) in
+ let lifted_oldt = S.lift_meta l oldt in
+ fo_unif_subst subst context metasenv lifted_oldt t
+ with Not_found ->
+ let t',metasenv' = delift context metasenv l t in
+ (n, t')::subst, metasenv'
in
- let (_,_,meta_type) =
- List.find (function (m,_,_) -> m=n) metasenv' in
- let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ let (_,_,meta_type) =
+ List.find (function (m,_,_) -> m=n) metasenv' in
+ let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
+ fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
| (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
| (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
if UriManager.eq uri1 uri2 then
in
fo_unif_l subst' metasenv' (l1,l2)
in
- fo_unif_l subst metasenv (lr1, lr2)
+ fo_unif_l subst metasenv (lr1, lr2)
| (C.Const _, _)
| (_, C.Const _)
| (C.MutInd _, _)
let subst', metasenv' =
fo_unif_subst subst context metasenv outt1 outt2 in
let subst'',metasenv'' =
- fo_unif_subst subst' context metasenv' t1 t2 in
+ fo_unif_subst subst' context metasenv' t1 t2 in
List.fold_left2
- (function (subst,metasenv) ->
+ (function (subst,metasenv) ->
fo_unif_subst subst context metasenv
) (subst'',metasenv'') pl1 pl2
| (C.Fix _, _)
let restrict canonical_context m k l =
let rec erase i =
function
- [] -> []
- | None::tl -> None::(erase (i+1) tl)
- | he::tl ->
- let i' = (List.nth l (i-1)) in
- if i' <= k
- then he::(erase (i+1) tl) (* local variable *)
- else
- let acc =
- (try List.nth canonical_context (i'-k-1)
- with Failure _ -> None) in
- if acc = None
- then None::(erase (i+1) tl)
- else he::(erase (i+1) tl) in
+ [] -> []
+ | None::tl -> None::(erase (i+1) tl)
+ | he::tl ->
+ let i' = (List.nth l (i-1)) in
+ if i' <= k
+ then he::(erase (i+1) tl) (* local variable *)
+ else
+ let acc =
+ (try List.nth canonical_context (i'-k-1)
+ with Failure _ -> None) in
+ if acc = None
+ then None::(erase (i+1) tl)
+ else he::(erase (i+1) tl) in
let rec aux =
function
- [] -> []
- | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
- | hd::tl -> hd::(aux tl)
+ [] -> []
+ | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
+ | hd::tl -> hd::(aux tl)
in
aux
;;
| C.Sort _ -> metasenv
| C.Implicit -> metasenv
| C.Cast (te,ty) ->
- let metasenv' = aux metasenv k te in
- aux metasenv' k ty
+ let metasenv' = aux metasenv k te in
+ aux metasenv' k ty
| C.Prod (_,s,t)
| C.Lambda (_,s,t)
| C.LetIn (_,s,t) ->
- let metasenv' = aux metasenv k s in
- aux metasenv' (k+1) t
+ let metasenv' = aux metasenv k s in
+ aux metasenv' (k+1) t
| C.Appl l ->
- List.fold_left
- (function metasenv -> aux metasenv k) metasenv l
+ List.fold_left
+ (function metasenv -> aux metasenv k) metasenv l
| C.Const _
| C.MutInd _
| C.MutConstruct _ -> metasenv
| C.MutCase (_,_,_,outty,t,pl) ->
- let metasenv' = aux metasenv k outty in
- let metasenv'' = aux metasenv' k t in
- List.fold_left
- (function metasenv -> aux metasenv k) metasenv'' pl
+ let metasenv' = aux metasenv k outty in
+ let metasenv'' = aux metasenv' k t in
+ List.fold_left
+ (function metasenv -> aux metasenv k) metasenv'' pl
| C.Fix (i, fl) ->
let len = List.length fl in
List.fold_left
(fun metasenv f ->
- let (_,_,ty,bo) = f in
- let metasenv' = aux metasenv k ty in
- aux metasenv' (k+len) bo
+ let (_,_,ty,bo) = f in
+ let metasenv' = aux metasenv k ty in
+ aux metasenv' (k+len) bo
) metasenv fl
| C.CoFix (i, fl) ->
- let len = List.length fl in
+ let len = List.length fl in
List.fold_left
(fun metasenv f ->
- let (_,ty,bo) = f in
- let metasenv' = aux metasenv k ty in
- aux metasenv' (k+len) bo
+ let (_,ty,bo) = f in
+ let metasenv' = aux metasenv k ty in
+ aux metasenv' (k+len) bo
) metasenv fl
in aux metasenv 0
;;
C.Rel _ as t -> t,metasenv
| C.Var _ as t -> t,metasenv
| C.Meta (i,l) ->
- (try
+ (try
S.lift_meta l (List.assoc i !unwinded), metasenv
with Not_found ->
if List.mem i !frozen then raise OccurCheck
else
let saved_frozen = !frozen in
- frozen := i::!frozen ;
+ frozen := i::!frozen ;
let res =
try
- let t = List.assoc i subst in
+ let t = List.assoc i subst in
let t',metasenv' = um_aux metasenv t in
- let _,metasenv'' =
+ let _,metasenv'' =
let (_,canonical_context,_) =
List.find (function (m,_,_) -> m=i) metasenv
in
(* not constrained variable, i.e. free in subst*)
let l',metasenv' =
List.fold_right
- (fun t (tl,metasenv) ->
+ (fun t (tl,metasenv) ->
match t with
None -> None::tl,metasenv
| Some t ->
- let t',metasenv' = um_aux metasenv t in
- (Some t')::tl, metasenv'
- ) l ([],metasenv)
+ let t',metasenv' = um_aux metasenv t in
+ (Some t')::tl, metasenv'
+ ) l ([],metasenv)
in
C.Meta (i,l'), metasenv'
in
| C.Appl (he::tl) ->
let tl',metasenv' =
List.fold_right
- (fun t (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- t'::tl, metasenv'
- ) tl ([],metasenv)
+ (fun t (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ t'::tl, metasenv'
+ ) tl ([],metasenv)
in
begin
match um_aux metasenv' he with
| C.Const (uri,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.Const (uri,exp_named_subst'),metasenv'
| C.MutInd (uri,typeno,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.MutInd (uri,typeno,exp_named_subst'),metasenv'
| C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
let exp_named_subst', metasenv' =
List.fold_right
- (fun (uri,t) (tl,metasenv) ->
- let t',metasenv' = um_aux metasenv t in
- (uri,t')::tl, metasenv'
- ) exp_named_subst ([],metasenv)
+ (fun (uri,t) (tl,metasenv) ->
+ let t',metasenv' = um_aux metasenv t in
+ (uri,t')::tl, metasenv'
+ ) exp_named_subst ([],metasenv)
in
C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
| C.MutCase (sp,i,outty,t,pl) ->
let t',metasenv'' = um_aux metasenv' t in
let pl',metasenv''' =
List.fold_right
- (fun p (pl,metasenv) ->
- let p',metasenv' = um_aux metasenv p in
- p'::pl, metasenv'
- ) pl ([],metasenv'')
+ (fun p (pl,metasenv) ->
+ let p',metasenv' = um_aux metasenv p in
+ p'::pl, metasenv'
+ ) pl ([],metasenv'')
in
C.MutCase (sp, i, outty', t', pl'),metasenv'''
| C.Fix (i, fl) ->
let liftedfl,metasenv' =
List.fold_right
(fun (name, i, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, i, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
+ let ty',metasenv' = um_aux metasenv ty in
+ let bo',metasenv'' = um_aux metasenv' bo in
+ (name, i, ty', bo')::fl,metasenv''
+ ) fl ([],metasenv)
in
C.Fix (i, liftedfl),metasenv'
| C.CoFix (i, fl) ->
let liftedfl,metasenv' =
List.fold_right
(fun (name, ty, bo) (fl,metasenv) ->
- let ty',metasenv' = um_aux metasenv ty in
- let bo',metasenv'' = um_aux metasenv' bo in
- (name, ty', bo')::fl,metasenv''
- ) fl ([],metasenv)
+ let ty',metasenv' = um_aux metasenv ty in
+ let bo',metasenv'' = um_aux metasenv' bo in
+ (name, ty', bo')::fl,metasenv''
+ ) fl ([],metasenv)
in
C.CoFix (i, liftedfl),metasenv'
in
projects / helm.git / blobdiff