X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=0b5cfadd27acbf686ecbb71ce1620d62d32de5f8;hb=4720c6af414c4a834a994fdb404fda2d0c04fc03;hp=c9e50be29a59792060563860f077534d71b7e170;hpb=6fa39011a07aaaf20b99929965ba93df8a81cdbb;p=helm.git diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index c9e50be29..0b5cfadd2 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -95,14 +95,6 @@ let apolynomial_normalize_ok_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con" -(** HELPERS *) - - (** - "Some" constructor's inverse - @raise Failure "unsome" if None is passed - *) -let unsome = function None -> failwith "unsome" | Some item -> item - (** CIC PREDICATES *) (** @@ -147,24 +139,17 @@ let conj_of_metano metano = @raise Failure if proof is None @return current goal's metasenv *) -let metasenv_of_status ~status:(proof, goal) = - match proof with - | None -> failwith "Ring.metasenv_of_status invoked on None goal" - | Some (_, m, _, _) -> m +let metasenv_of_status ~status:((_,m,_,_), _) = m (** @param status a proof engine status @raise Failure when proof or goal are None @return context corresponding to current goal *) -let context_of_status ~status:(proof, goal) = - let metasenv = metasenv_of_status ~status:(proof, goal) in - let _, context, _ = - match goal with - | None -> failwith "Ring.context_of_status invoked on None goal" - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - context +let context_of_status ~status:(proof, goal as status) = + let metasenv = metasenv_of_status ~status:status in + let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in + context (** CIC TERM CONSTRUCTORS *) @@ -402,50 +387,48 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); res with - | (Fail _) as e -> begin (* TODO: codice replicato perche' non funge il - binding multiplo con "as" *) - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - | (CicTypeChecker.NotWellTyped _) as e -> begin (* TODO: si puo' togliere? *) - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - | (CicUnification.UnificationFailed) as e -> begin + e -> + match e with + (Fail _) + | (CicTypeChecker.NotWellTyped _) + | (CicUnification.UnificationFailed) -> warn ( "Ring.try_tactics failed with exn: " ^ Printexc.to_string e); try_tactics ~tactics ~status - end - ) + | _ -> raise e (* [e] must not be caught ; let's re-raise it *) + ) | [] -> raise (Fail "try_tactics: no tactics left") +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 + (proof',goals@new_goals') + ) (proof,[]) new_goals continuations + with + Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + +let id_tac ~status:(proof,goal) = + (proof,[goal]) + +let status_of_single_goal_tactic_result = + function + proof,[goal] -> proof,goal + | _ -> + raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") + (** auxiliary tactic "elim_type" @param status current proof engine status @param term term to cut *) -let elim_type_tac ~status ~term = +let elim_type_tac ~term ~status = warn "in Ring.elim_type_tac"; - let status' = cut_tac ~term ~status in - elim_intros_simpl_tac ~term:(Cic.Rel 1) ~status:status' - - (** - move to next goal - @param status current proof engine status - *) -let next_goal ~status = - warn "in Ring.next_goal"; - (match status with - | ((Some (_, metasenv, _, _)) as proof, goal) -> - (match metasenv with - | _::(n, _, _)::_ -> (proof, Some n) - | _ -> raise (Fail "No other goal available")) - | _ -> assert false) + thens ~start:(cut_tac ~term) + ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof @@ -453,9 +436,10 @@ let next_goal ~status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) -let elim_type2_tac ~status ~term ~proof = +let elim_type2_tac ~term ~proof ~status = warn "in Ring.elim_type2"; - exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status)) + thens ~start:(elim_type_tac ~term) + ~continuations:[id_tac ; exact_tac ~term:proof] ~status (** Reflexivity tactic, try to solve current goal using "refl_eqT" @@ -465,7 +449,7 @@ let elim_type2_tac ~status ~term ~proof = *) let reflexivity_tac ~status:(proof, goal) = warn "in Ring.reflexivity_tac"; - let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in try apply_tac ~status:(proof, goal) ~term:refl_eqt with (Fail _) as e -> @@ -483,25 +467,22 @@ let lift ~n (a,b,c,d,e,f,g,h) = @param count number of hypotheses to remove @param status current proof engine status *) -let purge_hyps ~count ~status:(proof, goal) = +let purge_hyps_tac ~count ~status:(proof, goal as status) = let module S = ProofEngineStructuralRules in let rec aux n context status = assert(n>=0); match (n, context) with | (0, _) -> status - | (n, hd::tl) -> aux (n-1) tl (S.clear ~status ~hyp:hd) - | (_, []) -> failwith "Ring.purge_hyps: no hypotheses left" - in - let metano = - match goal with - | None -> failwith "Ring.purge_hyps invoked on None goal" - | Some n -> n + | (n, hd::tl) -> + aux (n-1) tl + (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status)) + | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in - match proof with - | None -> failwith "Ring.purge_hyps invoked on None proof" - | Some (_, metasenv, _, _) -> - let (_, context, _) = conj_of_metano metano metasenv in - aux count context (proof, goal) + let (_, metasenv, _, _) = proof in + let (_, context, _) = conj_of_metano goal metasenv in + let proof',goal' = aux count context status in + assert (goal = goal') ; + proof',[goal'] (** THE TACTIC! *) @@ -512,7 +493,6 @@ let purge_hyps ~count ~status:(proof, goal) = let ring_tac ~status:(proof, goal) = warn "in Ring tactic"; let status = (proof, goal) in - let (proof, goal) = (unsome proof), (unsome goal) in let eqt = mkMutInd (eqt_uri, 0) proof in let r = mkConst r_uri proof in let metasenv = metasenv_of_status ~status in @@ -550,8 +530,10 @@ let ring_tac ~status:(proof, goal) = ~status ~proof:t1'_eq_t1'' ~term:(Cic.Appl [eqt; r; t1''; t1]) in - incr new_hyps; (* elim_type add an hyp *) - newstatus + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false end else begin warn "t1'' and t1 are CONVERTIBLE"; status @@ -582,7 +564,9 @@ let ring_tac ~status:(proof, goal) = ~term:(Cic.Appl [eqt; r; t2''; t2]) in incr new_hyps; (* elim_type add an hyp *) - newstatus + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false end else begin warn "t2'' and t2 are CONVERTIBLE"; status @@ -593,11 +577,11 @@ let ring_tac ~status:(proof, goal) = reflexivity_tac ~status:status' with (Fail _) -> (* leave conclusion to the user *) warn "reflexivity failed, solution's left as an ex :-)"; - purge_hyps ~count:!new_hyps ~status:status')] + purge_hyps_tac ~count:!new_hyps ~status:status')] in status'')] - with (Fail _) -> - raise (Fail "Ring failure") + with (Fail s) -> + raise (Fail ("Ring failure: " ^ s)) end | _ -> (* impossible: we are applying ring exacty to 2 terms *) assert false