X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=5ea64913d0debbeacac87bcd4673a060f134c88c;hb=a864255e782859e2b3b7da08297f5d3fe2ee710d;hp=8414698e783f25c0a4da517720caa5602a52e0f9;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 8414698e7..5ea64913d 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -42,8 +42,10 @@ let warn s = (* not a tactical, but it's used only here (?) *) -let id_tac ~status:(proof,goal) = - (proof,[goal]) +let id_tac = + let tac (proof,goal) = (proof,[goal]) + in + mk_tactic tac (** @@ -55,13 +57,14 @@ let id_tac ~status:(proof,goal) = Galla: is this exactly Coq's "First"? *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = +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 = tac ~status in + let res = apply_tactic tac status in warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); res with @@ -73,34 +76,39 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = warn ( "Tacticals.try_tactics failed with exn: " ^ Printexc.to_string e); - try_tactics ~tactics ~status + 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 ~status = - let (proof,new_goals) = start ~status in +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') = tactic ~status:(proof,goal) in + let (proof',new_goals') = apply_tactic tactic (proof,goal) in (proof',goals@new_goals') ) (proof,[]) new_goals continuations with Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + in + mk_tactic (thens ~start ~continuations ) - -let then_ ~start ~continuation ~status = - let (proof,new_goals) = start ~status in +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') = continuation ~status:(proof,goal) in + let (proof',new_goals') = apply_tactic continuation (proof,goal) in (proof',goals@new_goals') ) (proof,[]) new_goals - + in + mk_tactic (then_ ~start ~continuation) (* Galla *) (* si suppone che tutte le tattiche sollevino solamente Fail? *) @@ -112,14 +120,15 @@ let then_ ~start ~continuation ~status = (* When generates more than one goal, you have a tree of application on the tactic, repeat_tactic works in depth on this tree *) -let rec repeat_tactic ~tactic ~status = +let repeat_tactic ~tactic = + let rec repeat_tactic ~tactic status = warn "in repeat_tactic"; - try let (proof, goallist) = tactic ~status in + 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 ~status:(proof, head) in + let (proof', goallist') = repeat_tactic ~tactic (proof, head) in let (proof'', goallist'') = step proof' tail in proof'', goallist'@goallist'' in @@ -127,25 +136,29 @@ let rec repeat_tactic ~tactic ~status = with (Fail _) as e -> warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac ~status + apply_tactic id_tac status + in + mk_tactic (repeat_tactic ~tactic) ;; (* This tries to apply tactic n times *) - -let rec do_tactic ~n ~tactic ~status = +let do_tactic ~n ~tactic = + let rec do_tactic ~n ~tactic status = warn "in do_tactic"; try let (proof, goallist) = - if (n>0) then tactic ~status - else id_tac ~status in -(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *) + 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 ~status:(proof, head) in + let (proof', goallist') = + do_tactic ~n:(n-1) ~tactic (proof, head) in let (proof'', goallist'') = step proof' tail in proof'', goallist'@goallist'' in @@ -153,48 +166,57 @@ let rec do_tactic ~n ~tactic ~status = with (Fail _) as e -> warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; - id_tac ~status + apply_tactic id_tac status + in + mk_tactic (do_tactic ~n ~tactic) ;; (* This applies tactic and catches its possible failure *) - -let rec try_tactic ~tactic ~status = +let try_tactic ~tactic = + let rec try_tactic ~tactic status = warn "in Tacticals.try_tactic"; try - tactic ~status + apply_tactic tactic status with (Fail _) as e -> warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); - id_tac ~status + apply_tactic id_tac status + in + 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 rec solve_tactics ~(tactics: (string * tactic) list) ~status = +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) = currenttactic ~status in + 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!) *) + [] -> 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 + 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 + 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"); - id_tac ~status + apply_tactic id_tac status + in + mk_tactic (solve_tactics ~tactics) ;; @@ -208,19 +230,20 @@ let rec solve_tactics ~(tactics: (string * tactic) list) ~status = (** tattica di prova per debuggare i tatticali *) (* -let thens' ~start ~continuations ~status = - let (proof,new_goals) = start ~status in +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 ~status:(proof,goal) in + 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:((proof,goal) as status) = + 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 = @@ -234,7 +257,7 @@ let prova_tac = find 1 context in prerr_endline ("eseguo apply"); - apply_tac ~term:(Cic.Rel rel) ~status + apply_tac ~term:(Cic.Rel rel) status in (* do_tactic ~n:2 *) repeat_tactic