X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=b0a9f452eda2fef9b064517aa663a8c1b40eb3ae;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=62f1ce322c4a98be3b42ef890700b6588e903de5;hpb=90c15accf8c385a3dc44aa5f6df13f707514e2cd;p=helm.git diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 62f1ce322..b0a9f452e 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -23,9 +23,9 @@ * http://cs.unibo.it/helm/. *) -open CicReduction +(* open CicReduction open ProofEngineTypes -open UriManager +open UriManager *) (** DEBUGGING *) @@ -34,247 +34,316 @@ let debug = false let debug_print = fun _ -> () (** debugging print *) -let warn s = - if debug then - debug_print ("TACTICALS WARNING: " ^ s) - - -(** TACTIC{,AL}S *) - - (* not a tactical, but it's used only here (?) *) +let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s))) let id_tac = - let tac (proof,goal) = (proof,[goal]) + let id_tac (proof,goal) = + let _, metasenv, _, _ = proof in + let _, _, _ = CicUtil.lookup_meta goal metasenv in + (proof,[goal]) in - mk_tactic tac + ProofEngineTypes.mk_tactic id_tac + +let fail_tac = + let fail_tac (proof,goal) = + let _, metasenv, _, _ = proof in + let _, _, _ = CicUtil.lookup_meta goal metasenv in + raise (ProofEngineTypes.Fail (lazy "fail tactical")) + in + ProofEngineTypes.mk_tactic fail_tac + +type goal = ProofEngineTypes.goal + + (** TODO needed until tactics start returning both opened and closed goals + * First part of the function performs a diff among goals ~before tactic + * application and ~after it. Second part will add as both opened and closed + * the goals which are returned as opened by the tactic *) +let goals_diff ~before ~after ~opened = + let sort_opened opened add = + opened @ (List.filter (fun g -> not (List.mem g opened)) add) + in + let remove = + List.fold_left + (fun remove e -> if List.mem e after then remove else e :: remove) + [] before + in + let add = + List.fold_left + (fun add e -> if List.mem e before then add else e :: add) + [] + after + in + let add, remove = (* adds goals which have been both opened _and_ closed *) + List.fold_left + (fun (add, remove) opened_goal -> + if List.mem opened_goal before + then opened_goal :: add, opened_goal :: remove + else add, remove) + (add, remove) + opened + in + sort_opened opened add, remove + +module type T = +sig + type tactic + val first: tactics: (string * tactic) list -> tactic + val thens: start: tactic -> continuations: tactic list -> tactic + val then_: start: tactic -> continuation: tactic -> tactic + val seq: tactics: tactic list -> tactic + val repeat_tactic: tactic: tactic -> tactic + val do_tactic: n: int -> tactic: tactic -> tactic + val try_tactic: tactic: tactic -> tactic + val solve_tactics: tactics: (string * tactic) list -> tactic + + val tactic: tactic -> tactic + val skip: tactic + val dot: tactic + val semicolon: tactic + val branch: tactic + val shift: tactic + val pos: int -> tactic + val merge: tactic + val focus: int list -> tactic + val unfocus: tactic +end + +module Make (S: Continuationals.Status) : T with type tactic = S.tactic = +struct + module C = Continuationals.Make (S) + + type tactic = S.tactic + + let fold_eval status ts = + let istatus = + List.fold_left (fun istatus t -> S.focus ~-1 (C.eval t istatus)) status ts + in + S.inject istatus (** naive implementation of ORELSE tactical, try a sequence of tactics in turn: if one fails pass to the next one and so on, eventually raises (failure "no tactics left") - TODO warning: not tail recursive due to "try .. with" boxing - - Galla: is this exactly Coq's "First"? - *) -let try_tactics ~tactics = - let rec try_tactics ~(tactics: (string * tactic) list) status = - warn "in Tacticals.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Tacticals.try_tactics IS TRYING " ^ descr); - (try - let res = apply_tactic tac status in - warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); - res - with - e -> - match e with - (Fail _) - | (CicTypeChecker.TypeCheckerFailure _) - | (CicUnification.UnificationFailure _) -> - warn ( - "Tacticals.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics status - | _ -> raise e (* [e] must not be caught ; let's re-raise it *) - ) - | [] -> raise (Fail "try_tactics: no tactics left") - in - mk_tactic (try_tactics ~tactics) - - -let thens ~start ~continuations = - let thens ~start ~continuations status = - let (proof,new_goals) = apply_tactic start status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = apply_tactic tactic (proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> -(* FG: more debugging information *) - let debug = Printf.sprintf "thens: expected %i new goals, found %i" - (List.length continuations) (List.length new_goals) + let first ~tactics = + let rec first ~(tactics: (string * tactic) list) istatus = + info (lazy "in Tacticals.first"); + match tactics with + | (descr, tac)::tactics -> + info (lazy ("Tacticals.first IS TRYING " ^ descr)); + (try + let res = S.apply_tactic tac istatus in + info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!")); + res + with + e -> + match e with + | (ProofEngineTypes.Fail _) + | (CicTypeChecker.TypeCheckerFailure _) + | (CicUnification.UnificationFailure _) -> + info (lazy ( + "Tacticals.first failed with exn: " ^ + Printexc.to_string e)); + first ~tactics istatus + | _ -> raise e) (* [e] must not be caught ; let's re-raise it *) + | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left")) in - raise (Fail debug) - in - mk_tactic (thens ~start ~continuations ) - - -let then_ ~start ~continuation = - let then_ ~start ~continuation status = - let (proof,new_goals) = apply_tactic start status in - List.fold_left - (fun (proof,goals) goal -> - let (proof',new_goals') = apply_tactic continuation (proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals - in - mk_tactic (then_ ~start ~continuation) - -let rec seq ~tactics = - match tactics with - | [] -> assert false - | [tac] -> tac - | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) - -(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) - -(* This keep on appling tactic until it fails *) -(* When generates more than one goal, you have a tree of - application on the tactic, repeat_tactic works in depth on this tree *) - -let repeat_tactic ~tactic = - let rec repeat_tactic ~tactic status = - warn "in repeat_tactic"; - try let (proof, goallist) = apply_tactic tactic status in - let rec step proof goallist = - match goallist with - [] -> (proof, []) - | head::tail -> - let (proof', goallist') = repeat_tactic ~tactic (proof, head) in - let (proof'', goallist'') = step proof' tail in - proof'', goallist'@goallist'' + S.mk_tactic (first ~tactics) + + let thens ~start ~continuations = + S.mk_tactic + (fun istatus -> + fold_eval istatus + ([ C.Tactical (C.Tactic start); C.Branch ] + @ (HExtlib.list_concat ~sep:[ C.Shift ] + (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations)) + @ [ C.Merge ])) + + let then_ ~start ~continuation = + S.mk_tactic + (fun istatus -> + let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in + let opened,closed = S.goals ostatus in + match opened with + [] -> ostatus + | _ -> + fold_eval (S.focus ~-1 ostatus) + [ C.Semicolon; + C.Tactical (C.Tactic continuation) ]) + + let seq ~tactics = + S.mk_tactic + (fun istatus -> + fold_eval istatus + (HExtlib.list_concat ~sep:[ C.Semicolon ] + (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics))) + + (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno + * applicato la tattica *) + + let rec step f output_status opened closed = + match opened with + | [] -> output_status, [], closed + | head :: tail -> + let status = S.focus head output_status in + let output_status' = f status in + let opened', closed' = S.goals output_status' in + let output_status'', opened'', closed'' = + step f output_status' tail [] + in + output_status'', opened' @ opened'', closed' @ closed'' + + (* This keep on appling tactic until it fails. When generates more + * than one goal, you have a tree of application on the tactic, repeat_tactic + * works in depth on this tree *) + let repeat_tactic ~tactic = + let rec repeat_tactic ~tactic status = + info (lazy "in repeat_tactic"); + try + let output_status = S.apply_tactic tactic status in + let opened, closed = S.goals output_status in + let output_status, opened', closed' = + step (repeat_tactic ~tactic) output_status opened closed + in + S.set_goals (opened', closed') output_status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy + ("Tacticals.repeat_tactic failed after nth time with exception: " + ^ Printexc.to_string e)); + S.apply_tactic S.id_tactic status + in + S.mk_tactic (repeat_tactic ~tactic) + + (* This tries to apply tactic n times *) + let do_tactic ~n ~tactic = + let rec do_tactic ~n ~tactic status = + if n = 0 then + S.apply_tactic S.id_tactic status + else + try + let output_status = S.apply_tactic tactic status in + let opened, closed = S.goals output_status in + let output_status, opened', closed' = + step (do_tactic ~n:(n-1) ~tactic) output_status opened closed + in + S.set_goals (opened', closed') output_status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy + ("Tacticals.do_tactic failed after nth time with exception: " + ^ Printexc.to_string e)) ; + S.apply_tactic S.id_tactic status in - step proof goallist - with - (Fail _) as e -> - warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - apply_tactic id_tac status - in - mk_tactic (repeat_tactic ~tactic) -;; - - - -(* This tries to apply tactic n times *) -let do_tactic ~n ~tactic = - let rec do_tactic ~n ~tactic status = - warn "in do_tactic"; - try - let (proof, goallist) = - if (n>0) then apply_tactic tactic status - else apply_tactic id_tac status in -(* else (proof, []) in *) -(* perche' non va bene questo? stessa questione di ##### ? *) - let rec step proof goallist = - match goallist with - [] -> (proof, []) - | head::tail -> - let (proof', goallist') = - do_tactic ~n:(n-1) ~tactic (proof, head) in - let (proof'', goallist'') = step proof' tail in - proof'', goallist'@goallist'' + S.mk_tactic (do_tactic ~n ~tactic) + + (* This applies tactic and catches its possible failure *) + let try_tactic ~tactic = + let rec try_tactic ~tactic status = + info (lazy "in Tacticals.try_tactic"); + try + S.apply_tactic tactic status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy ( + "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e)); + S.apply_tactic S.id_tactic status in - step proof goallist - with - (Fail _) as e -> - warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - apply_tactic id_tac status - in - mk_tactic (do_tactic ~n ~tactic) -;; - - - -(* This applies tactic and catches its possible failure *) -let try_tactic ~tactic = - let rec try_tactic ~tactic status = - warn "in Tacticals.try_tactic"; - try - apply_tactic tactic status - with - (Fail _) as e -> - warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); - apply_tactic id_tac status - in - mk_tactic (try_tactic ~tactic) -;; - -let fail = mk_tactic (fun _ -> raise (Fail "fail tactical")) - -(* This tries tactics until one of them doesn't _solve_ the goal *) -(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) -let solve_tactics ~tactics = - let rec solve_tactics ~(tactics: (string * tactic) list) status = - warn "in Tacticals.solve_tactics"; - match tactics with - | (descr, currenttactic)::moretactics -> - warn ("Tacticals.solve_tactics is trying " ^ descr); - (try - let (proof, goallist) = apply_tactic currenttactic status in - match goallist with - [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ - " solved the goal!!!"); -(* questo significa che non ci sono piu' goal, o che current_tactic non ne - ha aperti di nuovi? (la 2a!) ##### - nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) - (proof, goallist) - | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); - solve_tactics ~tactics:(moretactics) status - with - (Fail _) as e -> - warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ - Printexc.to_string e); - solve_tactics ~tactics status - ) - | [] -> raise (Fail "solve_tactics cannot solve the goal"); - apply_tactic id_tac status - in - mk_tactic (solve_tactics ~tactics) -;; - - - - - - - - - - - (** tattica di prova per debuggare i tatticali *) -(* -let thens' ~start ~continuations status = - let (proof,new_goals) = start status in - try - List.fold_left2 - (fun (proof,goals) goal tactic -> - let (proof',new_goals') = tactic (proof,goal) in - (proof',goals@new_goals') - ) (proof,[]) new_goals continuations - with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") - -let prova_tac = - let apply_T_tac status = - let (proof, goal) = status in - let curi,metasenv,pbo,pty = proof in - let metano,context,gty = CicUtil.lookup_meta goal metasenv in - let rel = - let rec find n = - function - [] -> assert false - | (Some (Cic.Name name,_))::_ when name = "T" -> n - | _::tl -> find (n+1) tl - in - debug_print ("eseguo find"); - find 1 context + S.mk_tactic (try_tactic ~tactic) + + (* This tries tactics until one of them doesn't _solve_ the goal *) + (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) + let solve_tactics ~tactics = + let rec solve_tactics ~(tactics: (string * tactic) list) status = + info (lazy "in Tacticals.solve_tactics"); + match tactics with + | (descr, currenttactic)::moretactics -> + info (lazy ("Tacticals.solve_tactics is trying " ^ descr)); + (try + let output_status = S.apply_tactic currenttactic status in + let opened, closed = S.goals output_status in + match opened with + | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ + " solved the goal!!!")); + (* questo significa che non ci sono piu' goal, o che current_tactic non ne ha + * aperti di nuovi? (la 2a!) ##### nel secondo caso basta per dire che + * solve_tactics has solved the goal? (si!) *) + output_status + | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic")); + solve_tactics ~tactics:(moretactics) status + with + (ProofEngineTypes.Fail _) as e -> + info (lazy ( + "Tacticals.solve_tactics: current tactic failed with exn: " + ^ Printexc.to_string e)); + solve_tactics ~tactics status + ) + | [] -> + raise (ProofEngineTypes.Fail + (lazy "solve_tactics cannot solve the goal")) in - debug_print ("eseguo apply"); - apply_tac ~term:(Cic.Rel rel) status - in -(* do_tactic ~n:2 *) - repeat_tactic - ~tactic: - (then_ - ~start:(intros_tac ~name:"pippo") - ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)])) -(* id_tac *) -;; -*) - + S.mk_tactic (solve_tactics ~tactics) + + let cont_proxy cont = S.mk_tactic (C.eval cont) + + let tactic t = cont_proxy (C.Tactical (C.Tactic t)) + let skip = cont_proxy (C.Tactical C.Skip) + let dot = cont_proxy C.Dot + let semicolon = cont_proxy C.Semicolon + let branch = cont_proxy C.Branch + let shift = cont_proxy C.Shift + let pos i = cont_proxy (C.Pos i) + let merge = cont_proxy C.Merge + let focus goals = cont_proxy (C.Focus goals) + let unfocus = cont_proxy C.Unfocus +end + +module ProofEngineStatus = +struct + module Stack = Continuationals.Stack + + type input_status = + ProofEngineTypes.status (* (proof, goal) *) * Stack.t + + type output_status = + (ProofEngineTypes.proof * goal list * goal list) * Stack.t + + type tactic = ProofEngineTypes.tactic + + let id_tactic = id_tac + + let mk_tactic f = + ProofEngineTypes.mk_tactic + (fun (proof, goal) as pstatus -> + let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in + let istatus = pstatus, stack in +(* let ostatus = f istatus in + let ((proof, opened, _), _) = ostatus in *) + let (proof, _, _), stack = f istatus in + let opened = Continuationals.Stack.open_goals stack in + proof, opened) + + let apply_tactic tac ((proof, _) as pstatus, stack) = + let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in +(* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *) + let before = ProofEngineTypes.goals_of_proof proof in + let after = ProofEngineTypes.goals_of_proof proof' in + let opened_goals, closed_goals = goals_diff ~before ~after ~opened in +(* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *) + (proof', opened_goals, closed_goals), stack + + let goals ((_, opened, closed), _) = opened, closed + let set_goals (opened, closed) ((proof, _, _), stack) = + (proof, opened, closed), stack + + let get_stack = snd + let set_stack stack (opstatus, _) = opstatus, stack + + let inject ((proof, _), stack) = ((proof, [], []), stack) + let focus goal ((proof, _, _), stack) = (proof, goal), stack +end + +module ProofEngineTacticals = Make (ProofEngineStatus) + +include ProofEngineTacticals