X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=953ed64445d7bbbf7d9cf7a2f3d4efd464ddcb7a;hb=5a369548a2f04fb59b5cbb94526325aae9bf415a;hp=080e280b5f25325f1faf2daaa141ad8b2e3f5414;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 080e280b5..953ed6444 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 *) @@ -339,8 +324,11 @@ let abstract_poly ~terms ~proof = newvar end in - (List.map aux terms, - btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof) + let aterms = List.map aux terms in (* abstract vars *) + let varmap = (* build varmap *) + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof + in + (aterms, varmap) (** given a list of abstract terms (i.e. apolynomials) build the ring "segments" @@ -381,68 +369,24 @@ let build_segments ~terms ~proof = [lxy_false; varmap; rtheory; t])) aterms -(** AUX TACTIC{,AL}S *) +let id_tac ~status:(proof,goal) = + (proof,[goal]) - (** - 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 - *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Ring.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Ring.try_tactics IS TRYING " ^ descr); - (try - let res = tac ~status in - 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 - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - ) - | [] -> raise (Fail "try_tactics: no tactics left") +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) + Tacticals.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 @@ -450,8 +394,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 = - exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status)) +let elim_type2_tac ~term ~proof ~status = + warn "in Ring.elim_type2"; + Tacticals.thens ~start:(elim_type_tac ~term) + ~continuations:[id_tac ; exact_tac ~term:proof] ~status (** Reflexivity tactic, try to solve current goal using "refl_eqT" @@ -461,7 +407,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 -> @@ -479,25 +425,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! *) @@ -508,7 +451,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 @@ -526,7 +468,7 @@ let ring_tac ~status:(proof, goal) = t2; t2'; t2''; t2'_eq_t2'']); try let new_hyps = ref 0 in (* number of new hypotheses created *) - try_tactics + Tacticals.try_tactics ~status ~tactics:[ "reflexivity", reflexivity_tac; @@ -546,8 +488,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 @@ -557,7 +501,7 @@ let ring_tac ~status:(proof, goal) = lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') in let status'' = - try_tactics (* try to solve 1st subgoal *) + Tacticals.try_tactics (* try to solve 1st subgoal *) ~status:status' ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; @@ -578,7 +522,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 @@ -589,11 +535,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