X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=4b4b7246d29023962c35dddc3e8dfc2b6a05b72b;hb=9b27b913b9084226d0af5306562d0a1c5ccdaaf7;hp=7c58ae87e5fca689fd807990ab6a45cdc0395055;hpb=806ecbdd749ecf2a1cabff52b41cf748fe022401;p=helm.git diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 7c58ae87e..4b4b7246d 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -11,6 +11,9 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) +(* let pp m = prerr_endline (Lazy.force m);;*) +let pp _ = ();; + let fresh_name = let i = ref 0 in function () -> @@ -69,30 +72,31 @@ let subst_metasenv_and_fix_names status = ;; let mk_inverter name it leftno ?selection outsort status baseuri = - prerr_endline ("leftno = " ^ string_of_int leftno); + pp (lazy ("leftno = " ^ string_of_int leftno)); let _,ind_name,ty,cl = it in - prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty); + pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty)); let ncons = List.length cl in - (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + (**)let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in let params = List.rev_map (function name,_ -> mk_id name) params in - prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*) + pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**) let args,sort= split_arity ~subst:[] [] ty in - prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort); - (*let args = List.rev_map (function name,_ -> mk_id name) args in - prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*) + pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort)); + (**)let args = List.rev_map (function name,_ -> mk_id name) args in + pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**) let nparams = List.length args in - prerr_endline ("nparams = " ^ string_of_int nparams); - if nparams <= leftno + + pp (lazy ("nparams = " ^ string_of_int nparams)); + if nparams = 0 then raise (Failure "inverter: the type must have at least one right parameter") else - let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in - prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs)); + let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in + pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs))); let ls, rs = HExtlib.split_nth leftno xs in - prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls)); - prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs)); - let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in + pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls))); + pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs))); + let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in - let id_xs = List.map mk_id xs in + let _id_xs = List.map mk_id xs in let id_ls = List.map mk_id ls in let id_rs = List.map mk_id rs in let id_ys = List.map mk_id ys in @@ -117,7 +121,7 @@ let mk_inverter name it leftno ?selection outsort status baseuri = | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1) in (hypaux 1 ncons) in - prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys)); + pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys))); let outsort, suffix = NCicElim.ast_of_sort outsort in let theorem = mk_prods xs @@ -125,11 +129,10 @@ let mk_inverter name it leftno ?selection outsort status baseuri = mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *) Some (CicNotationPt.Implicit `JustOne)), mk_appl (mk_id "P"::id_rs))))) - in + in let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ - List.map mk_id hyplist @ - CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in - + List.map mk_id hyplist @ + HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some @@ -145,26 +148,26 @@ let mk_inverter name it leftno ?selection outsort status baseuri = mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), - CicNotationPt.Implicit (`Tagged "end")); + +CicNotationPt.Implicit (`Tagged "end")); CicNotationPt.Implicit (`Tagged "cut")] in - let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in - + let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in let status = NTactics.block_tac - (NTactics.branch_tac:: - NTactics.case_tac "inv":: + (NTactics.branch_tac :: + NTactics.case_tac "inv" :: (intros @ [NTactics.apply_tac ("",0,cut); NTactics.branch_tac; NTactics.case_tac "end"; NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl_eq"); + NTactics.apply_tac ("",0,mk_id "refl"); NTactics.shift_tac; - NTactics.case_tac "cut"; - NTactics.apply_tac ("",0,t) - (* ; + (*NTactics.case_tac "cut";*) + NTactics.apply_tac ("",0,t); NTactics.merge_tac; NTactics.merge_tac; - NTactics.skip_tac*)])) status in + NTactics.skip_tac])) status in + pp (lazy "inv 3"); status,status#obj ;;