X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=27cb1cc33cacf6663db8ec41a6f6edb12c76a858;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=29aa1c4f1ed5157aea052a7f37f34946232745ce;hpb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;p=helm.git diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 29aa1c4f1..27cb1cc33 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -23,17 +23,14 @@ * http://cs.unibo.it/helm/. *) -(** DEBUGGING *) - - (** perform debugging output? *) -let debug = false - - (** debugging print *) -let warn s = - if debug then - prerr_endline ("DECOMPOSE: " ^ s) - - +module C = Cic +module P = PrimitiveTactics +module T = Tacticals +module S = ProofEngineStructuralRules +module F = FreshNamesGenerator +module E = ProofEngineTypes +module H = ProofEngineHelpers +module Q = MetadataQuery (* let induction_tac ~term status = @@ -56,169 +53,164 @@ let induction_tac ~term status = ;; *) +(* unexported tactics *******************************************************) + +let get_name context index = + try match List.nth context (pred index) with + | Some (Cic.Name name, _) -> Some name + | _ -> None + with Invalid_argument "List.nth" -> None + +let rec scan_tac ~old_context_length ~index ~tactic = + let scan_tac status = + let (proof, goal) = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let context_length = List.length context in + let rec aux index = + match get_name context index with + | _ when index <= 0 -> (proof, [goal]) + | None -> aux (pred index) + | Some what -> + let tac = T.then_ ~start:(tactic ~what) + ~continuation:(scan_tac ~old_context_length:context_length ~index ~tactic) + in + try E.apply_tactic tac status + with E.Fail _ -> aux (pred index) + in aux (index + context_length - old_context_length - 1) + in + E.mk_tactic scan_tac + +let rec check_inductive_types types = function + | C.MutInd (uri, typeno, _) -> List.mem (uri, typeno) types + | C.Appl (hd :: tl) -> check_inductive_types types hd + | _ -> false + +let elim_clear_tac ~mk_fresh_name_callback ~types ~what = + let elim_clear_tac status = + let (proof, goal) = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let index, ty = H.lookup_type metasenv context what in + if check_inductive_types types ty then + let tac = T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index)) + ~continuation:(S.clear what) + in + E.apply_tactic tac status + else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) + in + E.mk_tactic elim_clear_tac + +(* elim type ****************************************************************) + +let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth + ?using what += + let elim what = + P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what + in + let elim_type_tac status = + let tac = + T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac] + in + E.apply_tactic tac status + in + E.mk_tactic elim_type_tac + +(* decompose ****************************************************************) + +(* robaglia --------------------------------------------------------------- *) -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 -;; - - -(* Decompose related stuff *) - -exception InteractiveUserUriChoiceNotRegistered - -let interactive_user_uri_choice = - (ref (fun ~selection_mode -> raise InteractiveUserUriChoiceNotRegistered) : - (selection_mode:[`SINGLE | `EXTENDED] -> - ?ok:string -> - ?enable_button_for_non_vars:bool -> - 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) - ) -;; -*) + (** perform debugging output? *) +let debug = false +let debug_print = fun _ -> () -let decompose_tac ?(uris_choice_callback=(function l -> l)) term status = - let (proof, goal) = status in - let module C = Cic in - let module R = CicReduction in - let module P = PrimitiveTactics in - let module T = Tacticals in - let module S = ProofEngineStructuralRules in - 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 = - (* 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) *) - match termty with - (C.MutInd (uri,typeno,exp_named_subst)) (* when (not (List.mem (uri,typeno,exp_named_subst) urilist)) *) -> - (uri,typeno,exp_named_subst)::urilist - | (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! *) - in - let rec purge_duplicates urilist = - let rec aux triple urilist = - match urilist with - [] -> [] - | hd::tl -> - if (hd = triple) - then aux triple tl - else hd::(aux triple tl) - in - match urilist with - [] -> [] - | hd::tl -> hd::(purge_duplicates (aux hd tl)) - in - purge_duplicates (search_inductive_types [] termty) + (** debugging print *) +let warn s = debug_print (lazy ("DECOMPOSE: " ^ (Lazy.force s))) + +(* search in term the Inductive Types and return a list of uris as triples like this: (uri,typeno,exp_named_subst) *) +let search_inductive_types ty = + let rec aux types = function + | C.MutInd (uri, typeno, _) when (not (List.mem (uri, typeno) types)) -> + (uri, typeno) :: types + | C.Appl applist -> List.fold_left aux types applist + | _ -> types + in + aux [] ty +(* N.B: in un caso tipo (and A forall C:Prop.(or B C)) l'or *non* viene selezionato! *) + +(* roba seria ------------------------------------------------------------- *) + +let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) + ?(user_types=[]) ~dbd what = + let decompose_tac status = + let (proof, goal) = status in + let _, metasenv,_,_ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + let types = List.rev_append user_types (Q.decomposables dbd) in + let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in + let old_context_length = List.length context in + let tac = T.then_ ~start:(tactic ~what) + ~continuation:(scan_tac ~old_context_length ~index:1 ~tactic) in + E.apply_tactic tac status + in + E.mk_tactic decompose_tac + +(* +module R = CicReduction - let urilist = - (* list of triples (uri,typeno,exp_named_subst) of Inductive Types found in term and chosen by the user *) - (* 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 = + 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)); + warn (lazy ("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 - warn ("elim_clear termty= " ^ CicPp.ppterm termty); + let termty,_ = + CicTypeChecker.type_of_aux' metasenv context term' + CicUniv.empty_ugraph in + warn (lazy ("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_ - ~start:(P.elim_intros_simpl_tac ~term:term') + warn (lazy ("elim " ^ CicPp.ppterm termty)); + ProofEngineTypes.apply_tactic + (T.then_ + ~start:(P.elim_intros_simpl_tac term') ~continuation:( (* clear the hyp that has just been eliminated *) - (fun 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)); + warn (lazy ("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_ + 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) - ~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) + then begin debug_print (lazy ("%%%%%%% no clear")); T.id_tac end + else begin debug_print (lazy ("%%%%%%% 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 - )) + ))) 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)); + warn (lazy ("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 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 -;; - - +*)