X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=15645951e29a0af9920195a60dca96ff8ce9d2ec;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=cd401a2ec94cdaa66a0200c3bb516907b9ef3460;hpb=f5b6be7239a35e1d0aba504605b5a0df5cf06726;p=helm.git diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index cd401a2ec..15645951e 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -36,7 +36,8 @@ let warn s = (* -let induction_tac ~term ~status:((proof,goal) as status) = +let induction_tac ~term status = + let (proof, goal) = status in let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in @@ -51,19 +52,22 @@ let induction_tac ~term ~status:((proof,goal) as status) = ~tactic:(T.then_ ~start:(VariousTactics.generalize_tac ~term) (* chissa' se cosi' funziona? *) ~continuation:(P.intros)) ~continuation:(P.elim_intros_simpl ~term) - ~status + status ;; *) - -let elim_type_tac ~term ~status = - let module C = Cic in - let module P = PrimitiveTactics in - let module T = Tacticals in - T.thens - ~start: (P.cut_tac term) - ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ] - ~status +let elim_type_tac ~term = + let elim_type_tac ~term status = + let module C = Cic in + let module P = PrimitiveTactics in + let module T = Tacticals in + ProofEngineTypes.apply_tactic + (T.thens + ~start: (P.cut_tac term) + ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]) + status + in + ProofEngineTypes.mk_tactic (elim_type_tac ~term) ;; @@ -79,58 +83,9 @@ let interactive_user_uri_choice = title:string -> msg:string -> string list -> string list) ref) ;; -exception IllFormedUri of string - -let cic_textual_parser_uri_of_string uri' = - try - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then - CicTextualParser0.ConUri (UriManager.uri_of_string uri') - else - if String.sub uri' (String.length uri' - 4) 4 = ".var" then - CicTextualParser0.VarUri (UriManager.uri_of_string uri') - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in - CicTextualParser0.IndTyUri (uri'',typeno) - with - _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in - CicTextualParser0.IndConUri (uri'',typeno,consno) - ) - with - _ -> raise (IllFormedUri uri') -;; - -(* -let constructor_uri_of_string uri = - match cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false -;; - -let call_back uris = -(* N.B.: nella finestra c'e' un campo "nessuno deei precedenti, prova questo" che non ha senso? *) -(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) -(* domanda: due triple possono essere diverse solo per avere exp_named_subst diverse?? *) - let module U = UriManager in - List.map - (constructor_uri_of_string) - (!interactive_user_uri_choice - ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false - ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" - (List.map - (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)) - uris) - ) -;; -*) - -let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof,goal) as status) = +let decompose_tac ?(uris_choice_callback=(function l -> l)) term = + let decompose_tac uris_choice_callback term status = + let (proof, goal) = status in let module C = Cic in let module R = CicReduction in let module P = PrimitiveTactics in @@ -139,9 +94,9 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof let _,metasenv,_,_ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in - let termty = CicTypeChecker.type_of_aux' metasenv context term in - - let rec make_list termty = + let termty,_ = + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let rec make_list termty = (* N.B.: altamente inefficente? *) let rec search_inductive_types urilist termty = (* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) @@ -174,47 +129,55 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term ~status:((proof (* N.B.: due to a bug in uris_choice_callback exp_named_subst are not significant (they all are []) *) uris_choice_callback (make_list termty) in - let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim ~status:((proof,goal) as status) = + let rec elim_clear_tac ~term' ~nr_of_hyp_still_to_elim status = + let (proof, goal) = status in warn ("nr_of_hyp_still_to_elim=" ^ (string_of_int nr_of_hyp_still_to_elim)); if nr_of_hyp_still_to_elim <> 0 then let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let old_context_len = List.length context in - let termty = CicTypeChecker.type_of_aux' metasenv context term' in + let termty,_ = + CicTypeChecker.type_of_aux' metasenv context term' + CicUniv.empty_ugraph in warn ("elim_clear termty= " ^ CicPp.ppterm termty); match termty with C.MutInd (uri,typeno,exp_named_subst) | C.Appl((C.MutInd (uri,typeno,exp_named_subst))::_) when (List.mem (uri,typeno,exp_named_subst) urilist) -> warn ("elim " ^ CicPp.ppterm termty); - T.then_ + ProofEngineTypes.apply_tactic + (T.then_ ~start:(P.elim_intros_simpl_tac ~term:term') ~continuation:( (* clear the hyp that has just been eliminated *) - (fun ~status:((proof,goal) as status) -> + ProofEngineTypes.mk_tactic (fun status -> + let (proof, goal) = status in let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let new_context_len = List.length context in warn ("newcon=" ^ (string_of_int new_context_len) ^ " & oldcon=" ^ (string_of_int old_context_len) ^ " & old_nr_of_hyp=" ^ (string_of_int nr_of_hyp_still_to_elim)); let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim + (new_context_len - old_context_len) - 1 in - T.then_ + ProofEngineTypes.apply_tactic + (T.then_ ~start:( if (term'==term) (* if it's the first application of elim, there's no need to clear the hyp *) then begin prerr_endline ("%%%%%%% no clear"); T.id_tac end else begin prerr_endline ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:(List.nth context (new_nr_of_hyp_still_to_elim))) end) - ~continuation:(elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim) - ~status - )) - ~status + ~continuation:(ProofEngineTypes.mk_tactic (elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim))) + status + ))) + status | _ -> let new_nr_of_hyp_still_to_elim = nr_of_hyp_still_to_elim - 1 in warn ("fail; hyp=" ^ (string_of_int new_nr_of_hyp_still_to_elim)); - elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim ~status + elim_clear_tac ~term':(C.Rel new_nr_of_hyp_still_to_elim) ~nr_of_hyp_still_to_elim:new_nr_of_hyp_still_to_elim status else (* no hyp to elim left in this goal *) - T.id_tac ~status + ProofEngineTypes.apply_tactic T.id_tac status in - elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 ~status + elim_clear_tac ~term':term ~nr_of_hyp_still_to_elim:1 status + in + ProofEngineTypes.mk_tactic (decompose_tac uris_choice_callback term) ;;