exception Bad_pattern of string Lazy.t
-let new_meta_of_proof ~proof:(_, metasenv, _, _) =
- CicMkImplicit.new_meta metasenv []
+let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
+ CicMkImplicit.new_meta metasenv subst
let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty = 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
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)
) metasenv'
in
- let bo' = subst_in bo in
+ let bo' = lazy (subst_in (Lazy.force bo)) in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
* metavariable therein *)
let ty' = subst_in ty in
- let newproof = uri,metasenv'',bo',ty' 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) = proof in
- let bo' = subst_in bo 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' = lazy (subst_in (Lazy.force bo)) in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
* metavariable therein *)
(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
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty' 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 =
(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 ->
in
find subst metasenv ugraph context wanted t
-let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
+let select_in_term
+ ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where)
+=
let add_ctx context name entry = (Some (name, entry)) :: context in
let map2 error_msg f l1 l2 =
try
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)
| Some where -> aux context where term
in
match wanted with
- None -> [],metasenv,ugraph,roots
+ None -> subst,metasenv,ugraph,roots
| Some wanted ->
- let rec find_in_roots =
+ let rec find_in_roots subst =
function
- [] -> [],metasenv,ugraph,[]
+ [] -> subst,metasenv,ugraph,[]
| (context',where)::tl ->
- let subst,metasenv,ugraph,tl' = find_in_roots tl in
+ let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
let subst,metasenv,ugraph,found =
let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
in
subst,metasenv,ugraph,found @ tl'
in
- find_in_roots roots
+ find_in_roots subst roots
+;;
(** create a pattern from a term and a list of subterms.
* the pattern is granted to have a ? for every subterm that has no selected
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, ty, t) ->
let b1,s = aux s in
- let b2,t = aux t in
- if b1||b2 then
- true, Cic.LetIn (name, 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 ->
*
* @raise Bad_pattern
* *)
- let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
+ let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty)
~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
=
let what, hyp_patterns, goal_pattern = pattern in
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
+ select_in_term ~metasenv ~subst ~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 ->
let subst,metasenv,ugraph,terms =
- select_in_term ~metasenv ~context ~ugraph ~term
+ select_in_term ~subst ~metasenv ~context ~ugraph ~term
~pattern:(what, Some pat)
in
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
+ let selected_ty = [] in
subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
(entry::context)
| Some pat ->
let subst,metasenv,ugraph,terms_bo =
- select_in_term ~metasenv ~context ~ugraph ~term:bo
+ select_in_term ~subst ~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 ~subst ~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))
- ) context (subst,metasenv,ugraph,[],[]))
+ ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[]))
in
subst,metasenv,ugraph,res
in
subst,metasenv,ugraph,context_terms, ty_terms
+;;
(** locate_in_term equality what where context
* [what] must match a subterm of [where] according to [equality]
| 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 ([],[])
in
res @ locate_in_term what ~where:ty context
-(* saturate_term newmeta metasenv context ty goal_arity *)
-(* Given a type [ty] (a backbone), it returns its suffix of length *)
-(* [goal_arity] head and a new metasenv in which there is new a META for each *)
-(* hypothesis, a list of arguments for the new applications and the index of *)
-(* the last new META introduced. The nth argument in the list of arguments is *)
-(* just the nth new META. *)
-let saturate_term newmeta metasenv context ty goal_arity =
- let module C = Cic in
- let module S = CicSubstitution in
- assert (goal_arity >= 0);
- let rec aux newmeta ty =
- match ty with
- C.Cast (he,_) -> aux newmeta he
-(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
- (* If the expected type is a Type, then also Set is OK ==>
- * we accept any term of type Type *)
- (*CSC: BUG HERE: in this way it is possible for the term of
- * type Type to be different from a Sort!!! *)
- | C.Prod (name,(C.Sort (C.Type _) as s),t) ->
- (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *)
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let newargument = C.Meta (newmeta+1,irl) in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 2) (S.subst newargument t)
- in
- res,
- (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
- newargument::arguments,lastmeta
-*)
- | C.Prod (name,s,t) ->
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let newargument = C.Meta (newmeta,irl) in
- let res,newmetasenv,arguments,lastmeta,prod_no =
- aux (newmeta + 1) (S.subst newargument t)
- in
- if prod_no + 1 = goal_arity then
- let head = CicReduction.normalize ~delta:false context ty in
- head,[],[],lastmeta,goal_arity + 1
- else
- (** NORMALIZE RATIONALE
- * we normalize the target only NOW since we may be in this case:
- * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k
- * and we want a mesasenv with ?1:A1 and ?2:A2 and not
- * ?1, ?2, ?3 (that is the one we whould get if we start from the
- * beta-normalized A1 -> A2 -> A3 -> P **)
- let s' = CicReduction.normalize ~delta:false context s in
- res,(newmeta,context,s')::newmetasenv,newargument::arguments,
- lastmeta,prod_no + 1
- | t ->
- let head = CicReduction.normalize ~delta:false context t in
- match CicReduction.whd context head with
- C.Prod _ as head' -> aux newmeta head'
- | _ -> head,[],[],newmeta,0
- in
- (* WARNING: here we are using the invariant that above the most *)
- (* recente new_meta() there are no used metas. *)
- let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in
- res,metasenv @ newmetasenv,arguments,lastmeta
-
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
aux 1 context
-(* FG: **********************************************************************)
+let find_hyp name =
+ let rec find_hyp n =
+ function
+ [] -> assert false
+ | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+ Cic.Rel n, CicSubstitution.lift n ty
+ | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+ | _::tl -> find_hyp (n+1) tl
+ in
+ find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+ List.sort
+ (fun (id1,_) (id2,_) ->
+ let t1,_ = find_hyp id1 context in
+ let t2,_ = find_hyp id2 context in
+ match t1,t2 with
+ Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+ | _,_ -> assert false) hpatterns
+ in
+ t,hpatterns,cpattern
+;;
-let list_rev_map_filter f l =
- let rec aux a = function
- | [] -> a
- | hd :: tl ->
- begin match f hd with
- | None -> aux a tl
- | Some b -> aux (b :: a) tl
- end
- in
- aux [] l
+(* FG: **********************************************************************)
let get_name context index =
try match List.nth context (pred index) with
| _ :: tl -> aux (succ i) tl
in
aux 1 context
+
+let split_with_whd (c, t) =
+ let add s v c = Some (s, Cic.Decl v) :: c in
+ let rec aux whd a n c = function
+ | Cic.Prod (s, v, t) -> aux false ((c, v) :: a) (succ n) (add s v c) t
+ | v when whd -> (c, v) :: a, n
+ | 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) ->
+ List.map fst (CicUtil.metas_of_term ty)
+ | Some (_,Cic.Def (t,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