List.map
(function
Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
- | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None))
| None -> None
- | Some (n,Cic.Def (bo,Some ty)) ->
- Some (n,Cic.Def (subst_in bo,Some (subst_in ty)))
+ | Some (n,Cic.Def (bo,ty)) ->
+ Some (n,Cic.Def (subst_in bo,subst_in ty))
) canonical_context
in
i,canonical_context',(subst_in ty)
(function
None -> None
| Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
- | Some (i,Cic.Def (t,None)) ->
- Some (i,Cic.Def (subst_in t,None))
- | Some (i,Cic.Def (bo,Some ty)) ->
- Some (i,Cic.Def (subst_in bo,Some (subst_in ty)))
+ | Some (i,Cic.Def (bo,ty)) ->
+ Some (i,Cic.Def (subst_in bo,subst_in ty))
) canonical_context
in
(m,canonical_context',subst_in ty)::i
(CicSubstitution.lift 1 w) t2
in
subst,metasenv,ugraph,rest1 @ rest2
- | Cic.LetIn (name, t1, t2) ->
+ | Cic.LetIn (name, t1, t2, t3) ->
let subst,metasenv,ugraph,rest1 =
find subst metasenv ugraph context w t1 in
let subst,metasenv,ugraph,rest2 =
- find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context)
- (CicSubstitution.lift 1 w) t2
+ find subst metasenv ugraph context w t2 in
+ let subst,metasenv,ugraph,rest3 =
+ find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context)
+ (CicSubstitution.lift 1 w) t3
in
- subst,metasenv,ugraph,rest1 @ rest2
+ subst,metasenv,ugraph,rest1 @ rest2 @ rest3
| Cic.Appl l ->
List.fold_left
(fun (subst,metasenv,ugraph,acc) t ->
aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
| Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
| Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
- | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) ->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (Cic.Name n1, s1, t1),
- Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2->
- aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
- | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
+ | Cic.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) ->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (Cic.Name n1, s1, ty1, t1),
+ Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2->
+ aux context s1 s2 @
+ aux context ty1 ty2 @
+ aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+ | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> []
| Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2
| Cic.Var (_, subst1), Cic.Var (_, subst2)
| Cic.Const (_, subst1), Cic.Const (_, subst2)
true, Cic.Lambda (Cic.Anonymous, s, t)
else
not_found
- | Cic.LetIn (_, s, t) ->
+ | Cic.LetIn (_, s, ty, t) ->
let b1,s = aux s in
- let b2,t = aux t in
- if b1||b2 then
- true, Cic.LetIn (Cic.Anonymous, s, t)
+ let b2,ty = aux ty in
+ let b3,t = aux t in
+ if b1||b2||b3 then
+ true, Cic.LetIn (Cic.Anonymous, s, ty, t)
else
not_found
| Cic.Appl terms ->
| Some (name,Cic.Def (bo, ty)) ->
(match pattern with
| None ->
- let selected_ty=match ty with None -> None | Some _ -> Some [] in
+ let selected_ty = [] in
subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
(entry::context)
| Some pat ->
select_in_term ~metasenv ~context ~ugraph ~term:bo
~pattern:(what, Some pat) in
let subst,metasenv,ugraph,terms_ty =
- match ty with
- None -> subst,metasenv,ugraph,None
- | Some ty ->
- let subst,metasenv,ugraph,res =
- select_in_term ~metasenv ~context ~ugraph ~term:ty
- ~pattern:(what, Some pat)
- in
- subst,metasenv,ugraph,Some res
+ let subst,metasenv,ugraph,res =
+ select_in_term ~metasenv ~context ~ugraph ~term:ty
+ ~pattern:(what, Some pat)
+ in
+ subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
(entry::context))
| Cic.Prod (name, s, t)
| Cic.Lambda (name, s, t) ->
aux context s @ aux (add_ctx context name (Cic.Decl s)) t
- | Cic.LetIn (name, s, t) ->
- aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
+ | Cic.LetIn (name, s, ty, t) ->
+ aux context s @
+ aux context ty @
+ aux (add_ctx context name (Cic.Def (s,ty))) t
| Cic.Appl tl -> auxs context tl
| Cic.MutCase (_, _, out, t, pat) ->
aux context out @ aux context t @ auxs context pat
context',res
| Some (_, Cic.Def (bo,ty)) ->
let res = res @ locate_in_term what ~where:bo context in
- let res =
- match ty with
- None -> res
- | Some ty ->
- res @ locate_in_term what ~where:ty context in
+ let res = res @ locate_in_term what ~where:ty context in
let context' = entry::context in
context',res
) context ([],[])
let lookup_type metasenv context hyp =
let rec aux p = function
| Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
- p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+ | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t
| _ :: tail -> aux (succ p) tail
| [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
in
(List.map
(function
| None -> []
- | Some (_,Cic.Decl t)
- | Some (_,Cic.Def (t,None)) ->
+ | Some (_,Cic.Decl t) ->
List.map fst (CicUtil.metas_of_term ty)
- | Some (_,Cic.Def (t,Some ty)) ->
+ | Some (_,Cic.Def (t,ty)) ->
List.map fst (CicUtil.metas_of_term ty) @
List.map fst (CicUtil.metas_of_term t))
ctx)