;;
let check_for_duplicates metas msg =
- if List.length metas <>
- List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
- begin
+ let rec aux = function
+ | [] -> true
+ | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
+ let b = aux metas in
+ if not b then
+ begin
prerr_endline ("DUPLICATI " ^ msg);
prerr_endline (CicMetaSubst.ppmetasenv [] metas);
assert false
- end
+ end
+ else ()
+;;
+
+let check_metasenv msg menv =
+ List.iter
+ (fun (i,ctx,ty) ->
+ try ignore(CicTypeChecker.type_of_aux' menv ctx ty
+ CicUniv.empty_ugraph)
+ with
+ | CicUtil.Meta_not_found _ ->
+ prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
+ assert false
+ | _ -> ()
+ ) menv
+;;
+
+(* the metasenv returned by res must included in the original one,
+due to matching. If it fails, it is probably because we are not
+demodulating with a unit equality *)
+
+let not_unit_eq ctx eq =
+ let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in
+ let b =
+ List.exists
+ (fun (_,_,ty) ->
+ try
+ let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+ in s = Cic.Sort(Cic.Prop)
+ with _ ->
+ prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
+ in b
+(*
+if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *)
+;;
+
+let check_demod_res res metasenv msg =
+ match res with
+ | Some (_, _, menv, _, _) ->
+ let b =
+ List.for_all
+ (fun (i,_,_) ->
+ (List.exists (fun (j,_,_) -> i=j) metasenv)) menv
+ in
+ if (not b) then
+ begin
+ prerr_endline ("extended context " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ end;
+ b
+ | None -> false
;;
let check_res res msg =
match res with
- Some (t, subst, menv, ug, eq_found) ->
+ | Some (t, subst, menv, ug, eq_found) ->
let eqs = Equality.string_of_equality (snd eq_found) in
+ check_metasenv msg menv;
check_disjoint_invariant subst menv msg;
check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
| [] -> None
| candidate::tl ->
let pos, equality = candidate in
+ (* if not_unit_eq context equality then
+ begin
+ prerr_endline "not a unit";
+ prerr_endline (Equality.string_of_equality equality)
+ end; *)
let (_, proof, (ty, left, right, o), metas,_) =
Equality.open_equality equality
in
let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
-(*
+ let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
let p="proof = "^
- (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
+ (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n"
in
-*)
+
check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
+ check_for_duplicates metasenv "gia nel metasenv";
+ check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p)
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
+ check_metasenv "founif :" metasenv';
Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
in
let c, other =
try do_match c
with Founif.MatchingFailure -> None
in
- if Utils.debug_res then ignore (check_res res "find2");
+ if Utils.debug_res then ignore (check_res res "find2");
match res with
| Some (_, s, _, _, _) ->
let c' = apply_subst s c in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let cmp = !Utils.compare_terms in
+ let check = match termty with C.Implicit None -> false | _ -> true in
function
| [] -> []
| candidate::tl ->
let pos, equality = candidate in
- let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
+ let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
+ if check && not (fst (CicReduction.are_convertible
+ ~metasenv context termty ty ugraph)) then (
+ find_all_matches metasenv context ugraph lift_amount term termty tl
+ ) else
let do_match c =
let subst', metasenv', ugraph' =
unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
in
(C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
in
+
let c, other =
if pos = Utils.Left then left, right
else right, left
subsumption_aux true x y z
;;
+(* the target must be disjoint from the equations in the table *)
let subsumption_aux_all use_unification env table target =
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let _, context, ugraph = env in
let metasenv = tmetas in
+ check_for_duplicates metasenv "subsumption_aux_all";
let predicate, unif_fun =
if use_unification then
Unification, Founif.unification
let unification_all x y z =
subsumption_aux_all true x y z
;;
+
let rec demodulation_aux bag ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
-(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
+ check_for_duplicates metasenv "in input a demodulation aux";
let candidates =
get_candidates
~env:(metasenv,context,ugraph) (* Unification *) Matching table term
+ in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates
in
let res =
match term with
| C.Meta _ -> None
| term ->
- let termty, ugraph =
- if typecheck then
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- else
- C.Implicit None, ugraph
- in
- let res =
- find_matches bag metasenv context ugraph lift_amount term termty candidates
+ let res =
+ try
+ let termty, ugraph =
+ if typecheck then
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ else
+ C.Implicit None, ugraph
+ in
+ find_matches bag metasenv context ugraph
+ lift_amount term termty candidates
+ with _ ->
+ prerr_endline "type checking error";
+ prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ prerr_endline ("term: " ^ (CicPp.ppterm term));
+ assert false;
+ (* None *)
in
- if Utils.debug_res then ignore(check_res res "demod1");
- if res <> None then
+ let res =
+ (if Utils.debug_res then
+ ignore(check_res res "demod1");
+ if check_demod_res res metasenv "demod" then res else None) in
+ if res <> None then
res
else
match term with
(res, tl @ [S.lift 1 t])
else
let r =
- demodulation_aux bag ~from:"1" metasenv context ugraph table
+ demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
lift_amount t
in
match r with
| Some (_, subst, menv, ug, eq_found) ->
Some (C.Appl ll, subst, menv, ug, eq_found)
)
+(*
| C.Prod (nn, s, t) ->
let r1 =
demodulation_aux bag ~from:"2"
subst, menv, ug, eq_found)
)
| C.Lambda (nn, s, t) ->
+ prerr_endline "siam qui";
let r1 =
demodulation_aux bag
metasenv context ugraph table lift_amount s in (
Some (C.Lambda (nn, s', (S.lift 1 t)),
subst, menv, ug, eq_found)
)
+*)
| t ->
None
in
| C.Meta (i, l) -> res, lifted_term
| term ->
let termty, ugraph =
- C.Implicit None, ugraph
-(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+(* C.Implicit None, ugraph *)
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
in
let candidates = get_candidates Unification table term in
let r =
(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
(*****************************************************************************)
+(* new: demodulation of non_equality terms *)
+let build_newg bag context goal rule expansion =
+ let goalproof,_,_ = goal in
+ let (t,subst,menv,ug,eq_found) = expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = apply_subst subst t in
+ let ty = apply_subst subst ty in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Founif.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+let rec demod bag env table goal =
+ let goalproof,menv,t = goal in
+ let _, context, ugraph = env in
+ let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+ match res with
+ | Some newt ->
+ let newg =
+ build_newg bag context goal Equality.Demodulation newt
+ in
+ let _,_,newt = newg in
+ if Equality.meta_convertibility t newt then
+ false, goal
+ else
+ true, snd (demod bag env table newg)
+ | None ->
+ false, goal
+;;
+
let open_goal g =
match g with
| (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
(* assert (LibraryObjects.is_eq_URI uri); *)
proof,menv,eq,ty,l,r
| _ -> assert false
-;;
let ty_of_goal (_,_,ty) = ty ;;
* C[x] ---> (eq ty unchanged C[x])
* [posu] is the side of the [unchanged] term in the original goal
*)
+
let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
let _,_,eq,ty,l,r = open_goal goal in
let unchanged = if posu = Utils.Left then l else r in
projects / helm.git / commitdiff