exception Bad_pattern of string Lazy.t
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _) =
+let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty, attrs = proof in
+ let uri,metasenv,initial_subst,bo,ty, attrs = proof in
(* empty context is ok for term since it wont be used by apply_subst *)
(* hack: since we do not know the context and the type of term, we
create a substitution with cc =[] and type = Implicit; they will be
* since the parser does not reject as statements terms with
* metavariable therein *)
let ty' = subst_in ty in
- let newproof = uri,metasenv'',bo',ty', attrs in
+ let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
(newproof, metasenv'')
(*CSC: commento vecchio *)
(*CSC: ci ripasso sopra apply_subst!!! *)
(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
(*CSC: [newmetasenv]. *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty, attrs) = proof in
+let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
+ let (uri,_,initial_subst,bo,ty, attrs) = proof in
+ let subst_in = CicMetaSubst.apply_subst subst in
let bo' = subst_in bo in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty', attrs in
+ (* qui da capire se per la fase transitoria si fa initial_subst @ subst
+ * oppure subst *)
+ let newproof = uri,metasenv',subst,bo',ty', attrs in
(newproof, metasenv')
let compare_metasenvs ~oldmetasenv ~newmetasenv =
if b1||b2 then true,Cic.Cast (te, ty)
else
not_found
- | Cic.Prod (name, s, t) ->
+ | Cic.Prod (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Prod (name, s, t)
+ true, Cic.Prod (Cic.Anonymous, s, t)
else
not_found
- | Cic.Lambda (name, s, t) ->
+ | Cic.Lambda (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Lambda (name, s, t)
+ true, Cic.Lambda (Cic.Anonymous, s, t)
else
not_found
- | Cic.LetIn (name, s, t) ->
+ | Cic.LetIn (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.LetIn (name, s, t)
+ true, Cic.LetIn (Cic.Anonymous, s, t)
else
not_found
| Cic.Appl terms ->
let find_pattern_for name =
try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
with Not_found -> None in
+ (* Multiple hypotheses with the same name can be in the context.
+ In this case we need to pick the last one, but we will perform
+ a fold_right on the context. Thus we pre-process hyp_patterns. *)
+ let full_hyp_pattern =
+ let rec aux blacklist =
+ function
+ [] -> []
+ | None::tl -> None::aux blacklist tl
+ | Some (name,_)::tl ->
+ if List.mem name blacklist then
+ None::aux blacklist tl
+ else
+ find_pattern_for name::aux (name::blacklist) tl
+ in
+ aux [] context
+ in
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
- (fun entry (subst,metasenv,ugraph,res,context) ->
+ (fun (pattern,entry) (subst,metasenv,ugraph,res,context) ->
match entry with
- None -> subst,metasenv,ugraph,(None::res),(None::context)
+ None -> subst,metasenv,ugraph,None::res,None::context
| Some (name,Cic.Decl term) ->
- (match find_pattern_for name with
+ (match pattern with
| None ->
subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
| Some pat ->
subst,metasenv,ugraph,((Some (`Decl terms))::res),
(entry::context))
| Some (name,Cic.Def (bo, ty)) ->
- (match find_pattern_for name with
+ (match pattern with
| None ->
let selected_ty=match ty with None -> None | Some _ -> Some [] in
subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
in
subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
(entry::context))
- ) context (subst,metasenv,ugraph,[],[]))
+ ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[]))
in
subst,metasenv,ugraph,res
in
| v -> aux true a n c (CicReduction.whd c v)
in
aux false [] 0 c t
+
+let split_with_normalize (c, t) =
+ let add s v c = Some (s, Cic.Decl v) :: c in
+ let rec aux a n c = function
+ | Cic.Prod (s, v, t) -> aux ((c, v) :: a) (succ n) (add s v c) t
+ | v -> (c, v) :: a, n
+ in
+ aux [] 0 c (CicReduction.normalize c t)
+
+ (* menv sorting *)
+module OT =
+ struct
+ type t = Cic.conjecture
+ let compare (i,_,_) (j,_,_) = Pervasives.compare i j
+ end
+module MS = HTopoSort.Make(OT)
+let relations_of_menv m c =
+ let i, ctx, ty = c in
+ let m = List.filter (fun (j,_,_) -> j <> i) m in
+ let m_ty = List.map fst (CicUtil.metas_of_term ty) in
+ let m_ctx =
+ List.flatten
+ (List.map
+ (function
+ | None -> []
+ | Some (_,Cic.Decl t)
+ | Some (_,Cic.Def (t,None)) ->
+ List.map fst (CicUtil.metas_of_term ty)
+ | Some (_,Cic.Def (t,Some ty)) ->
+ List.map fst (CicUtil.metas_of_term ty) @
+ List.map fst (CicUtil.metas_of_term t))
+ ctx)
+ in
+ let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
+ List.filter (fun (i,_,_) -> List.exists ((=) i) metas) m
+;;
+let sort_metasenv (m : Cic.metasenv) =
+ (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
+;;
projects / helm.git / blobdiff