-(* Da rimuovere, solo per debug*)
-let print_context ctx =
- let print_name =
- function
- Cic.Name n -> n
- | Cic.Anonymous -> "_"
- in
- List.fold_right
- (fun i (output,context) ->
- let (newoutput,context') =
- match i with
- Some (n,Cic.Decl t) ->
- print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
- | Some (n,Cic.Def (t,None)) ->
- print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
- | None ->
- "_ ?= _\n", None::context
- | Some (_,Cic.Def (_,Some _)) -> assert false
- in
- output^newoutput,context'
- ) ctx ("",[])
- ;;
-
-
-let search_theorems_in_context status =
- let (proof, goal) = status in
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let module PET = ProofEngineTypes in
- let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let rec find n = function
- [] -> []
- | hd::tl ->
- let res =
- try
- Some (PET.apply_tactic
- (PT.apply_tac ~term:(C.Rel n)) status )
- with
- PET.Fail _ -> None in
- (match res with
- Some res -> res::(find (n+1) tl)
- | None -> find (n+1) tl)
- in
- try
- find 1 context
- with Failure s ->
- []
-;;
-
-let depth = 5;;
-let width = 3;;
-
-let new_search_theorems f proof goal depth gtl sign =
- let choices = f (proof,goal)
- in
- List.map
- (function (proof, goallist) ->
- (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
- choices
-;;
-
-exception NoOtherChoices;;
-let rec auto dbd = function
- [] -> []
- | (proof, [], sign)::tl -> (proof, [], sign)::tl
- | (proof, (goal,0)::_, _)::tl -> auto dbd tl
- | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
- (* first we check if the metavariable has not been already
- closed as a side effect by some other application *)
- let facts = (depth = 1) in
- let name,metasenv,p,statement = proof in
- let meta_inf =
- (try
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- Some (ey, ty)
- with _ -> None) in
- match meta_inf with
- Some (ey, ty) ->
- (* the goal is still there *)
- (*
- debug_print ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
- debug_print ("CURRENT PROOF = " ^ (CicPp.ppterm p));
- debug_print ("CURRENT HYP = " ^ (fst (print_context ey)));
- *)
- (* if the goal contains metavariables we use the input
- signature for at_most constraints *)
- let is_meta_closed = CicUtil.is_meta_closed ty in
- let sign, new_sign =
- if is_meta_closed then
- None, Some (MetadataConstraints.signature_of ty)
- else sign,sign in (* maybe the union ? *)
- let local_choices =
- new_search_theorems
- search_theorems_in_context
- proof goal (depth-1) [] new_sign in
- let global_choices =
- new_search_theorems
- (fun status ->
- List.map snd
- (MetadataQuery.hint
- ~dbd ~facts:facts ?signature:sign status))
- proof goal (depth-1) [] new_sign in
- (* we proceed depth-first on the current goal. This is
- a MAJOR optimization, since in case of success, and
- if the goal is meta_closed, we may just drop the alternatives
- tl1, avoiding useless backtracking. *)
- let all_choices =
- local_choices@global_choices in
- (match (auto dbd all_choices)
- with
- [] -> auto dbd tl
- | (proof,[],_)::tl1 ->
- let all_choices =
- let gtl' = List.map fst gtl in
- if (gtl = [] || is_meta_closed) then
- (proof,gtl,sign)::tl
- else
- let tl2 =
- (List.map
- (function (p,l,s) -> (p,l@gtl,s)) tl1)
- in
- (proof,gtl,sign)::tl2@tl in
- auto dbd all_choices
- | _ -> assert false)
- | None -> auto dbd ((proof,gtl,sign)::tl)
-;;