statements, f::context
| A.Negated_conjecture ->
if collect_fv_from_formulae f <> [] then
- (*prerr_endline "CONTIENE FV";*)();
+ prerr_endline "CONTIENE FV";
let f =
PT.Binder
(`Forall,
in
C.InductiveDefinition (tl', params', paramsno, attrs)
+let rec metas_of_term = function
+ | Cic.Meta (i, c) -> [i,c]
+ | Cic.Var (_, ens)
+ | Cic.Const (_, ens)
+ | Cic.MutInd (_, _, ens)
+ | Cic.MutConstruct (_, _, _, ens) ->
+ List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+ | Cic.Cast (s, t)
+ | Cic.Prod (_, s, t)
+ | Cic.Lambda (_, s, t)
+ | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+ | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+ | Cic.MutCase (uri, i, s, t, l) ->
+ (metas_of_term s) @ (metas_of_term t) @
+ (List.flatten (List.map metas_of_term l))
+ | Cic.Fix (i, il) ->
+ List.flatten
+ (List.map (fun (s, i, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | Cic.CoFix (i, il) ->
+ List.flatten
+ (List.map (fun (s, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | _ -> []
+;;
+
val is_closed : Cic.term -> bool
val is_meta_closed : Cic.term -> bool
+val metas_of_term : Cic.term -> (int * Cic.term option list) list
(** @raise Failure "not enough prods" *)
val strip_prods: int -> Cic.term -> Cic.term
let build_goal_proof l initial ty se =
let se = List.map (fun i -> Cic.Meta (i,[])) se in
let proof,se =
- List.fold_left
- (fun (current_proof,se) (pos,id,subst,pred) ->
- let p,l,r = proof_of_id id in
- let p = build_proof_term p in
- let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
- build_proof_step subst current_proof p pos l r pred,
- List.map (fun x -> Subst.apply_subst subst x) se)
- (initial,se) l
+ let rec aux se current_proof = function
+ | [] -> current_proof,se
+ | (pos,id,subst,pred)::tl ->
+ let p,l,r = proof_of_id id in
+ let p = build_proof_term p in
+ let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+ let proof = build_proof_step subst current_proof p pos l r pred in
+ let proof,se = aux se proof tl in
+ Subst.apply_subst subst proof,
+ List.map (fun x -> Subst.apply_subst subst x) se
+ in
+ aux se initial l
in
canonical (contextualize_rewrites proof ty), se
;;
let simplify_goal_set env goals passive active =
let active_goals, passive_goals = goals in
+ let find (_,_,g) where =
+ List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
+ in
let simplified =
- HExtlib.filter_map
- (fun g ->
+ List.fold_left
+ (fun acc g ->
match simplify_goal env g ~passive active with
- | true, g -> Some g
- | false, g -> Some g)
- active_goals
+ | _, g -> if find g acc then acc else g::acc)
+ [] active_goals
in
+ if List.length active_goals <> List.length simplified then
+ prerr_endline "SEMPLIFICANDO HO SCARTATO...";
(simplified,passive_goals)
(*
HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
let infer_goal_set env active goals =
let active_goals, passive_goals = goals in
- match passive_goals with
- | [] -> goals
- | hd::tl ->
- let selected = hd in
- let passive_goals = tl in
- let new' = Indexing.superposition_left env (snd active) selected in
- selected::active_goals, passive_goals @ new'
+ let rec aux = function
+ | [] -> goals
+ | ((_,_,t1) as hd)::tl when
+ not (List.exists
+ (fun (_,_,t) -> Equality.meta_convertibility t t1)
+ active_goals)
+ ->
+ let selected = hd in
+ let passive_goals = tl in
+ let new' = Indexing.superposition_left env (snd active) selected in
+ selected::active_goals, passive_goals @ new'
+ | _::tl -> aux tl
+ in
+ aux passive_goals
;;
let infer_goal_set_with_current env current goals =
let goal_proof = replace goal_proof in
(* ok per le meta libere... ma per quelle che c'erano e sono rimaste?
* what mi pare buono, sostituisce solo le meta farlocche *)
+ prerr_endline (CicPp.pp goal_proof names);
let side_effects_t = List.map replace side_effects_t in
(* check/refine/... build the new proof *)
let replaced_goal =
| CicUnification.AssertFailure s ->
fail "Maybe the local context of metas in the goal was not an IRL" s
in
-
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
+ let _ =
+ let ty,_ =
+ CicTypeChecker.type_of_aux' real_menv context goal_proof
+ CicUniv.empty_ugraph
+ in
+ ty
+ in
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
-let rec metas_of_term = function
- | Cic.Meta (i, c) -> [i]
- | Cic.Var (_, ens)
- | Cic.Const (_, ens)
- | Cic.MutInd (_, _, ens)
- | Cic.MutConstruct (_, _, _, ens) ->
- List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
- | Cic.Cast (s, t)
- | Cic.Prod (_, s, t)
- | Cic.Lambda (_, s, t)
- | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
- | Cic.Appl l -> List.flatten (List.map metas_of_term l)
- | Cic.MutCase (uri, i, s, t, l) ->
- (metas_of_term s) @ (metas_of_term t) @
- (List.flatten (List.map metas_of_term l))
- | Cic.Fix (i, il) ->
- List.flatten
- (List.map (fun (s, i, t1, t2) ->
- (metas_of_term t1) @ (metas_of_term t2)) il)
- | Cic.CoFix (i, il) ->
- List.flatten
- (List.map (fun (s, t1, t2) ->
- (metas_of_term t1) @ (metas_of_term t2)) il)
- | _ -> []
-;;
+let metas_of_term t =
+ List.map fst (CicUtil.metas_of_term t)
+;;
projects / helm.git / commitdiff