From 4ae46ae1b0353b51bc77b621077fdbcd5f2d075e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 17 Nov 2009 08:18:43 +0000 Subject: [PATCH] Closing the goal. --- helm/software/components/ng_tactics/nnAuto.ml | 204 ++++++++++++++++-- 1 file changed, 191 insertions(+), 13 deletions(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 4d6d7f886..70e6ed24e 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -14,8 +14,10 @@ open Printf let debug = ref false let debug_print ?(depth=0) s = if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () -let print ?(depth=0) s = +(* let print= debug_print *) + let print ?(depth=0) s = prerr_endline (String.make depth '\t'^Lazy.force s) + let debug_do f = if !debug then f () else () open Continuationals.Stack @@ -51,6 +53,190 @@ let auto_paramod_tac ~params status = NTactics.distribute_tac (auto_paramod ~params) status ;; +(*************** subsumption ****************) +module IntSet = Set.Make(struct type t = int let compare = compare end) +(* exceptions *) + +let get_sgoalty status g = + let _,_,metasenv,subst,_ = status#obj in + try + let _, ctx, ty = NCicUtils.lookup_meta g metasenv in + let ty = NCicUntrusted.apply_subst subst ctx ty in + let ctx = NCicUntrusted.apply_subst_context + ~fix_projections:true subst ctx + in + NTacStatus.mk_cic_term ctx ty + with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty") +;; + +let deps status g = + let gty = get_sgoalty status g in + metas_of_term status gty +;; + +let menv_closure status gl = + let rec closure acc = function + | [] -> acc + | x::l when IntSet.mem x acc -> closure acc l + | x::l -> closure (IntSet.add x acc) (deps status x @ l) + in closure IntSet.empty gl +;; + +let close_wrt_context = + List.fold_left + (fun ty ctx_entry -> + match ctx_entry with + | name, NCic.Decl t -> NCic.Prod(name,t,ty) + | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty) +;; + +let args_for_context ?(k=1) ctx = + let _,args = + List.fold_left + (fun (n,l) ctx_entry -> + match ctx_entry with + | name, NCic.Decl t -> n+1,NCic.Rel(n)::l + | name, NCic.Def(bo, _) -> n+1,l) + (k,[]) ctx in + args + +let constant_for_meta ctx ty i = + let name = "cic:/foo"^(string_of_int i)^".con" in + let uri = NUri.uri_of_string name in + let ty = close_wrt_context ty ctx in + (* prerr_endline (NCicPp.ppterm [] [] [] ty); *) + let attr = (`Generated,`Definition,`Local) in + let obj = NCic.Constant([],name,None,ty,attr) in + (* Constant of relevance * string * term option * term * c_attr *) + (uri,0,[],[],obj) + +(* not used *) +let refresh metasenv = + List.fold_left + (fun (metasenv,subst) (i,(iattr,ctx,ty)) -> + let ikind = NCicUntrusted.kind_of_meta iattr in + let metasenv,j,instance,ty = + NCicMetaSubst.mk_meta ~attrs:iattr + metasenv ctx ~with_type:ty ikind in + let s_entry = i,(iattr, ctx, instance, ty) in + let metasenv = List.filter (fun x,_ -> i <> x) metasenv in + metasenv,s_entry::subst) + (metasenv,[]) metasenv + +(* close metasenv returns a ground instance of all the metas in the +metasenv, insantiatied with axioms, and the list of these axioms *) +let close_metasenv metasenv subst = + (* + let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in + *) + let metasenv = NCicUntrusted.sort_metasenv subst metasenv in + List.fold_left + (fun (subst,objs) (i,(iattr,ctx,ty)) -> + let ty = NCicUntrusted.apply_subst subst ctx ty in + let ctx = + NCicUntrusted.apply_subst_context ~fix_projections:true + subst ctx in + let (uri,_,_,_,obj) as okind = + constant_for_meta ctx ty i in + try + NCicEnvironment.check_and_add_obj okind; + let iref = NReference.reference_of_spec uri NReference.Decl in + let iterm = + let args = args_for_context ctx in + if args = [] then NCic.Const iref + else NCic.Appl(NCic.Const iref::args) + in + (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *) + let s_entry = i, ([], ctx, iterm, ty) + in s_entry::subst,okind::objs + with _ -> assert false) + (subst,[]) metasenv +;; + +let ground_instances status gl = + let _,_,metasenv,subst,_ = status#obj in + let subset = menv_closure status gl in + let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in +(* + let submenv = metasenv in +*) + let subst, objs = close_metasenv submenv subst in + try + List.iter + (fun i -> + let (_, ctx, t, _) = List.assoc i subst in + debug_print (lazy (NCicPp.ppterm ctx [] [] t)); + List.iter + (fun (uri,_,_,_,_) as obj -> + NCicEnvironment.invalidate_item (`Obj (uri, obj))) + objs; + ()) + gl + with + Not_found -> assert false + (* (ctx,t) *) +;; + +let replace_meta i args target = + let rec aux k = function + (* TODO: local context *) + | NCic.Meta (j,lc) when i = j -> + (match args with + | [] -> NCic.Rel 1 + | _ -> let args = + List.map (NCicSubstitution.subst_meta lc) args in + NCic.Appl(NCic.Rel k::args)) + | NCic.Meta (j,lc) as m -> + (match lc with + _,NCic.Irl _ -> m + | n,NCic.Ctx l -> + NCic.Meta + (i,(0,NCic.Ctx + (List.map (fun t -> + aux k (NCicSubstitution.lift n t)) l)))) + | t -> NCicUtils.map (fun _ k -> k+1) k aux t + in + aux 1 target +;; + +let close_wrt_metasenv subst = + List.fold_left + (fun ty (i,(iattr,ctx,mty)) -> + let mty = NCicUntrusted.apply_subst subst ctx mty in + let ctx = + NCicUntrusted.apply_subst_context ~fix_projections:true + subst ctx in + let cty = close_wrt_context mty ctx in + let name = "foo"^(string_of_int i) in + let ty = NCicSubstitution.lift 1 ty in + let args = args_for_context ~k:1 ctx in + (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *) + let ty = replace_meta i args ty + in + NCic.Prod(name,cty,ty)) +;; + +let close status g = + let _,_,metasenv,subst,_ = status#obj in + let subset = menv_closure status [g] in + let subset = IntSet.remove g subset in + let elems = IntSet.elements subset in + let _, ctx, ty = NCicUtils.lookup_meta g metasenv in + let ty = NCicUntrusted.apply_subst subst ctx ty in + print (lazy ("Elements for " ^ (NCicPp.ppterm ctx [] metasenv ty))); + print (lazy (String.concat ", " (List.map string_of_int elems))); + let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in + let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in +(* + let submenv = metasenv in +*) + let ty = close_wrt_metasenv subst ty submenv in + print (lazy (NCicPp.ppterm ctx [] [] ty)); + ty +;; + + + (* =================================== auto =========================== *) (****************** AUTO ******************** @@ -1024,9 +1210,6 @@ type goal = int * sort (* goal, depth, sort *) type fail = goal * cic_term type candidate = int * Ast.term (* unique candidate number, candidate *) -module IntSet = Set.Make(struct type t = int let compare = compare end) -(* exceptions *) - exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive atoms of the input goals *) exception Proved of #NTacStatus.tac_status @@ -1185,17 +1368,13 @@ let do_something signature flags s gno depth gty cache = equational_and_applicative_case signature flags s gno depth gty cache ;; -let deps status g = - let gty = get_goalty status g in - metas_of_term status gty -;; - module M = struct type t = int let compare = Pervasives.compare end ;; + module MS = HTopoSort.Make(M) ;; @@ -1311,7 +1490,8 @@ auto_main flags signature cache depth status: unit = let gty = get_goalty status g in let status, gty = apply_subst status (ctx_of gty) gty in debug_print ~depth (lazy("Depth = " ^ (string_of_int depth))); - print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); + debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty)); + close status g; (* let closed = metas_of_term status gty = [] in *) let alternatives, cache = do_something signature flags status g depth gty cache in @@ -1322,7 +1502,7 @@ auto_main flags signature cache depth status: unit = (fun unsat ((_,t),_,_,status,_) -> let depth' = if t=(Ast.Implicit `JustOne) then depth else depth+1 in - print (~depth:depth') + debug_print (~depth:depth') (lazy ("Case: " ^ CicNotationPp.pp_term t)); try auto_clusters flags signature cache depth' status; unsat @@ -1336,7 +1516,6 @@ auto_main flags signature cache depth status: unit = (try auto_clusters flags signature cache depth status; unsat with Gaveup f -> - let debug_print = print in debug_print ~depth (lazy ("Unsat1 at depth " ^ (string_of_int depth) ^ ": " ^ @@ -1344,7 +1523,6 @@ auto_main flags signature cache depth status: unit = (* TODO: cache failures *) IntSet.union f unsat) | Gaveup f -> - let debug_print = print in debug_print (~depth:depth') (lazy ("Unsat2 at depth " ^ (string_of_int depth') ^ ": " ^ -- 2.39.2