X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=e52fff6e4452f671c2cc6e5634c41b2e03504716;hb=3064844b2f594cfce55c0140ecb4d15e35364486;hp=1db11951fed63c9ac2383026412d9e859afe776a;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 1db11951f..e52fff6e4 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -27,11 +27,12 @@ (** perform debugging output? *) let debug = false +let debug_print = fun _ -> () (** debugging print *) let warn s = if debug then - prerr_endline ("DECOMPOSE: " ^ s) + debug_print ("DECOMPOSE: " ^ s) @@ -56,18 +57,19 @@ let induction_tac ~term status = ;; *) -let elim_type_tac ~term = - let elim_type_tac ~term status = +let elim_type_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ?depth ?using what = + let elim_type_tac 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 ]) + ~start: (P.cut_tac what) + ~continuations:[ P.elim_intros_simpl_tac ?depth ?using ~mk_fresh_name_callback (C.Rel 1) ; T.id_tac ]) status in - ProofEngineTypes.mk_tactic (elim_type_tac ~term) + ProofEngineTypes.mk_tactic elim_type_tac ;; @@ -83,57 +85,6 @@ 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 = let decompose_tac uris_choice_callback term status = let (proof, goal) = status in @@ -145,9 +96,9 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = 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) *) @@ -157,7 +108,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::applist)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> (uri,typeno,exp_named_subst)::(List.fold_left search_inductive_types urilist applist) | _ -> urilist - (* N.B: in un caso tipo (and A !C:Prop.(or B C)) l'or *non* viene selezionato! *) + (* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) in let rec purge_duplicates urilist = let rec aux triple urilist = @@ -187,7 +138,9 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = 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) @@ -196,7 +149,7 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = warn ("elim " ^ CicPp.ppterm termty); ProofEngineTypes.apply_tactic (T.then_ - ~start:(P.elim_intros_simpl_tac ~term:term') + ~start:(P.elim_intros_simpl_tac term') ~continuation:( (* clear the hyp that has just been eliminated *) ProofEngineTypes.mk_tactic (fun status -> @@ -206,12 +159,18 @@ let decompose_tac ?(uris_choice_callback=(function l -> l)) term = 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 + let hyp_name = + match List.nth context new_nr_of_hyp_still_to_elim with + None + | Some (Cic.Anonymous,_) -> assert false + | Some (Cic.Name name,_) -> name + in 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) + then begin debug_print ("%%%%%%% no clear"); T.id_tac end + else begin debug_print ("%%%%%%% clear " ^ (string_of_int (new_nr_of_hyp_still_to_elim))); (S.clear ~hyp:hyp_name) end) ~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 )))