* http://cs.unibo.it/helm/.
*)
-
-(* 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
- prerr_endline "Entro in search_context";
- 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
- let res = find 1 context in
- prerr_endline "Ho finito context";
- res
- with Failure s ->
- prerr_endline ("SIAM QUI = " ^ s); []
-;;
-
-exception NotAProposition;;
-exception NotApplicableTheorem;;
-exception MaxDepth;;
-
-let depth = 3;;
-
-(*
-let rec auto_tac_aux mqi_handle level proof goal =
-prerr_endline ("Entro in Auto_rec; level = " ^ (string_of_int level));
-if level = 0 then
- (* (proof, [goal]) *)
- (prerr_endline ("MaxDepth");
- raise MaxDepth)
-else
- (* let us verify that the metavariable is still an open goal --
- it could have been closed by closing other goals -- and that
- it is of sort Prop *)
- let _,metasenv,_,_ = 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) ->
- prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
- prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
- (* if the goal does not have a sort Prop we return the
- current proof and a list containing the goal *)
- let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in
- if CicReduction.are_convertible
- ey (Cic.Sort Cic.Prop) ty_sort then
- (* sort Prop *)
- (* choices is a list of pairs proof and goallist *)
- let choices =
- (search_theorems_in_context (proof,goal))@
- (TacticChaser.searchTheorems mqi_handle (proof,goal))
- in
- let rec try_choices = function
- [] -> raise NotApplicableTheorem
- | (proof,goallist)::tl ->
-prerr_endline ("GOALLIST = " ^ string_of_int (List.length goallist));
- (try
- List.fold_left
- (fun proof goal ->
- auto_tac_aux mqi_handle (level-1) proof goal)
- proof goallist
- with
- | MaxDepth
- | NotApplicableTheorem
- | NotAProposition ->
- try_choices tl) in
- try_choices choices
- else
- (* CUT AND PASTE DI PROVA !! *)
- let choices =
- (search_theorems_in_context (proof,goal))@
- (TacticChaser.searchTheorems mqi_handle (proof,goal))
- in
- let rec try_choices = function
- [] -> raise NotApplicableTheorem
- | (proof,[])::tl -> proof
- | _::tl -> try_choices tl in
- try_choices choices
- (* raise NotAProposition *)
- | None -> proof
-;;
-
-let auto_tac mqi_handle =
- let module PET = ProofEngineTypes in
- let auto_tac mqi_handle (proof,goal) =
- prerr_endline "Entro in Auto";
- try
- let proof = auto_tac_aux mqi_handle depth proof goal in
- prerr_endline "AUTO_TAC HA FINITO";
- (proof,[])
- with
- | MaxDepth -> assert false (* this should happens only if depth is 0 above *)
- | NotApplicableTheorem ->
- prerr_endline("No applicable theorem");
- raise (ProofEngineTypes.Fail "No Applicable theorem")
- in
- PET.mk_tactic (auto_tac mqi_handle)
-;;
-
-*)
-
-(**** ESPERIMENTO ************************)
-
-let new_search_theorems f proof goal depth gtl =
- let local_choices = f (proof,goal)
- in
- List.map
- (function (proof, goallist) ->
- (proof, (List.map (function g -> (g,depth)) goallist)@gtl))
- local_choices
-;;
-
-exception NoOtherChoices;;
-
-let rec auto_new dbd = function
- [] -> raise NoOtherChoices
- | (proof, [])::tl -> (proof, [])::tl
- | (proof, (goal,0)::gtl)::tl -> auto_new dbd tl
- | (proof, (goal,depth)::gtl)::tl ->
- let _,metasenv,proof_obj,_ = 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) ->
- prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
- prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
- prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm proof_obj));
- let local_choices =
- new_search_theorems
- search_theorems_in_context proof goal (depth-1) gtl in
- let global_choices =
- new_search_theorems
- (fun status -> List.map snd (MetadataQuery.hint ~dbd status))
-(* (TacticChaser.searchTheorems mqi_handle) *)
- proof goal (depth-1) gtl in
- let all_choices =
- local_choices@global_choices@tl in
- let sorting_list (_,g1) (_,g2) =
- let l1 = List.length g1 in
- let l2 = List.length g2 in
- if (l1 = l2 && not(l1 = 0)) then
- (snd(List.nth g2 0)) - (snd(List.nth g1 0))
- else l1 - l2 in
- let reorder =
- List.stable_sort sorting_list all_choices
- in
- auto_new dbd reorder
- | None -> auto_new dbd ((proof,gtl)::tl)
-;;
-
-
-let auto_tac ~(dbd:Mysql.dbd) =
-(* CicMetaSubst.reset_counters (); *)
- let auto_tac dbd (proof,goal) =
- prerr_endline "Entro in Auto";
- try
- (match auto_new dbd [(proof, [(goal,depth)])] with
- | (proof,_)::_ ->
- prerr_endline "AUTO_TAC HA FINITO";
- (* CicMetaSubst.print_counters (); *)
- (proof,[])
- | _ -> assert false)
- with
- | NoOtherChoices ->
- prerr_endline("Auto failed");
- raise (ProofEngineTypes.Fail "No Applicable theorem")
- in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio
chiedere: find dovrebbe restituire una lista di hyp (?) da passare all'utonto con una
projects / helm.git / blobdiff