From dfee894b6cc036014bbbf1f508621840f44144d7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 13:53:01 +0000 Subject: [PATCH 1/1] short names --- helm/software/components/ng_tactics/nAuto.ml | 40 ++++++++------------ 1 file changed, 16 insertions(+), 24 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 422a1be41..d8e92cbad 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -38,10 +38,10 @@ let auto_paramod ~params:(l,_) status goal = match NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l with - | [] -> raise (NTacStatus.Error (lazy "no proof found",None)) + | [] -> raise (Error (lazy "no proof found",None)) | (pt, metasenv, subst)::_ -> let status = status#set_obj (n,h,metasenv,subst,o) in - instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt) + instantiate status goal (mk_cic_term (ctx_of gty) pt) ;; let auto_paramod_tac ~params status = @@ -935,7 +935,7 @@ type cache_examination_result = type sort = T | P type goal = int * int * sort (* goal, depth, sort *) -type fail = goal * NTacStatus.cic_term +type fail = goal * cic_term type candidate = int * NCic.term (* unique candidate number, candidate *) type op = @@ -943,11 +943,11 @@ type op = | D of goal (* goal has to be cached as a success obtained using candidate as the first * step *) - | S of goal * NTacStatus.cic_term * candidate (* int was minsize *) + | S of goal * cic_term * candidate (* int was minsize *) type 'a elem = (* menv, subst, size, operations done (only S), operations to do, * failures to cache if any op fails *) - (#NTacStatus.tac_status as 'a) * int * op list * op list * fail list + (#tac_status as 'a) * int * op list * op list * fail list type 'a auto_status = (* list of computations that may lead to the solution: all op list will @@ -956,7 +956,7 @@ type 'a auto_status = type 'a auto_result = | Gaveup - | Proved of (#NTacStatus.tac_status as 'a) * 'a auto_status (* alt. proofs *) + | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *) type flags = { do_types : bool; (* solve goals in Type *) @@ -985,21 +985,21 @@ let try_candidate status t g = let ast_for_t = match t with | NCic.Rel i -> assert false - | NCic.Const ref -> CicNotationPt.NRef ref + | NCic.Const ref -> Ast.NRef ref | _ -> assert false in let status = NTactics.focus_tac [g] status in let status = NTactics.apply_tac ("",0,ast_for_t) status in - let open_goals = Continuationals.Stack.head_goals status#stack in + let open_goals = head_goals status#stack in incr candidate_no; Some ((!candidate_no,t),status,open_goals) - with NTacStatus.Error (msg,exn) -> debug_print msg; None + with Error (msg,exn) -> debug_print msg; None ;; let get_candidates status context gty = let universe = status#auto_cache in - let _, gty = NTacStatus.term_of_cic_term status gty (NTacStatus.ctx_of gty) in + let _, gty = term_of_cic_term status gty (ctx_of gty) in let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty in @@ -1061,8 +1061,8 @@ let equational_and_applicative_case ;; let calculate_goal_ty (goalno,_,_) status = - try Some (NTacStatus.get_goalty status goalno) - with NTacStatus.Error _ -> None + try Some (get_goalty status goalno) + with Error _ -> None ;; let d_goals l = let rec aux acc = function @@ -1100,7 +1100,6 @@ let auto_main context flags signature elems cache = aux tables flags cache elems) *) | [] -> - (* complete failure *) debug_print (lazy "gave up"); Gaveup | (s, _, _, [],_)::orlist -> @@ -1137,7 +1136,7 @@ let auto_main context flags signature elems cache = debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno)); aux ((s,size,don,todo, fl)::orlist, cache) | Some gty -> - debug_print (lazy ("EXAMINE: "^ NTacStatus.ppterm s gty)); + debug_print (lazy ("EXAMINE: "^ ppterm s gty)); match cache_examine cache gty with | `Failed_in d when d >= depth -> debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno)); @@ -1162,7 +1161,7 @@ let auto_main context flags signature elems cache = let cache = cache_add_underinspection cache gty depth in debug_print (lazy ("INSPECTING: " ^ string_of_int gno ^ "("^ string_of_int size ^ "): "^ - NTacStatus.ppterm s gty)); + ppterm s gty)); (* elems are possible computations for proving gty *) let elems = equational_and_applicative_case @@ -1206,15 +1205,8 @@ let auto_main context flags signature elems cache = ;; let auto_tac ~params status = - prerr_endline "I teoremi noti sono"; - NDiscriminationTree.DiscriminationTree.iter status#auto_cache - (fun _ t -> - List.iter - (fun t -> - prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t)) - (NDiscriminationTree.TermSet.elements t)); let cache = Cache.empty in - let goals = Continuationals.Stack.head_goals status#stack in + let goals = head_goals status#stack in let depth = 3 in (* XXX fix sort *) let goals = List.map (fun i -> D(i,depth,P)) goals in let elems = [status,0,[],goals,[]] in @@ -1227,7 +1219,7 @@ let auto_tac ~params status = do_types = false; } in match auto_main context flags signature elems cache with - | Gaveup -> raise (NTacStatus.Error (lazy "auto gave up", None)) + | Gaveup -> raise (Error (lazy "auto gave up", None)) | Proved (s, (_orlist, _cache)) -> let stack = match s#stack with -- 2.39.2