X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=1ee47c74e97998dbfd552416ad7b12aec0589411;hb=8e905c34eb47a3f5fa67afa7997576d57588a50f;hp=366697ece6adff18d955b417a488bddef1015a79;hpb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;p=helm.git diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 366697ece..1ee47c74e 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 () -> @@ -49,10 +52,14 @@ let rec mk_lambdas l t = | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t) ;; -let rec mk_arrows l t = - match l with - [] -> t - | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id "_", Some hd), mk_arrows tl t) +let rec mk_arrows xs ys selection target = + match selection,xs,ys with + [],[],[] -> target + | false :: l,x::xs,y::ys -> mk_arrows xs ys l target + | true :: l,x::xs,y::ys -> + CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), + mk_arrows xs ys l target) + | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; let subst_metasenv_and_fix_names status = @@ -64,133 +71,103 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; -let mk_inverter name it leftno status baseuri = - prerr_endline ("leftno = " ^ string_of_int leftno); +let mk_inverter name it leftno ?selection outsort status baseuri = + 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 = List.rev_map (function name,_ -> mk_id name) params in - prerr_endline ("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); + pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*) + let args,sort= split_arity ~subst:[] [] ty in + pp (lazy ("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 ("lunghezza args = " ^ string_of_int (List.length args)));*) let nparams = List.length args in - prerr_endline ("nparams = " ^ string_of_int nparams); - - 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 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 - - 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 - - (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *) - - (* check: assuming we have more than one right parameter *) - (* pred := P yr- *) - let pred = mk_appl ((mk_id "P")::id_ys) in - - let selection = HExtlib.mk_list true (List.length ys) in - let prods = - let rec prodaux = function - [],[],[] -> pred - | false :: l,x::xs,y::ys -> prodaux (l,xs,ys) - | true :: l,x::xs,y::ys -> - CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), - prodaux (l,xs,ys)) - | _ -> assert false - in prodaux (selection,id_rs,id_ys) - in - - let lambdas = mk_lambdas (ys@["p"]) prods in - - let hyplist = - let rec hypaux k = function - 0 -> [] - | 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)); - let theorem = mk_prods xs - (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))), - 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 - let t = mk_appl ( [mk_id (ind_name ^ "_ind"); lambdas] @ - List.map mk_id hyplist @ - CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in - - prerr_endline ("NINVERTER 0"); - let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri - (baseuri ^ name ^ ".def", - 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in - prerr_endline ("NINVERTER 1"); - let uri,height,nmenv,nsubst,nobj = theorem in - let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in - let status = status#set_obj theorem in - let status = status#set_stack ninitial_stack in - let status = subst_metasenv_and_fix_names status in - - let cut_theorem = - mk_arrows (List.map - (fun x -> let x = mk_id x in mk_appl [mk_id "eq"; - CicNotationPt.Implicit `JustOne; - x;x]) rs) (mk_appl (mk_id "P"::List.map mk_id rs)) in - let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), - 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 branches = - let rec branch_aux k = function - 0 -> [NTactics.apply_tac ("",0,mk_id "H")] - | n -> NTactics.apply_tac ("",0,mk_id ("H"^(string_of_int k)))::(branch_aux (k+1) (n-1)) - in branch_aux 1 ncons - in*) - - let status = NTactics.block_tac - (NTactics.branch_tac:: - NTactics.case_tac "inv":: - (intros @ - [NTactics.apply_tac ("",0,cut); - NTactics.branch_tac; - NTactics.case_tac "end"; - (*NTactics.intro_tac "Hcut";*) - NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl_eq"); - NTactics.shift_tac; - NTactics.case_tac "cut"; - NTactics.apply_tac ("",0,t); - (* NTactics.branch_tac] - @ branches @ - [NTactics.merge_tac; *) - NTactics.merge_tac; - NTactics.merge_tac; - NTactics.skip_tac])) status in - status,status#obj + pp (lazy ("nparams = " ^ string_of_int nparams)); + if nparams <= leftno + 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 + pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs))); + let ls, rs = HExtlib.split_nth leftno xs 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) (nparams+1)) 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 + + (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *) + + (* check: assuming we have more than one right parameter *) + (* pred := P yr- *) + let pred = mk_appl ((mk_id "P")::id_ys) in + + let selection = match selection with + None -> HExtlib.mk_list true (List.length ys) + | Some s -> s + in + let prods = mk_arrows id_rs id_ys selection pred in + + let lambdas = mk_lambdas (ys@["p"]) prods in + + let hyplist = + let rec hypaux k = function + 0 -> [] + | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1) + in (hypaux 1 ncons) + in + pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys))); + + let outsort, suffix = NCicElim.ast_of_sort outsort in + let theorem = mk_prods xs + (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))), + 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 + let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ + List.map mk_id hyplist @ + CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in + + let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def", + 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some + (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in + let uri,height,nmenv,nsubst,nobj = theorem in + let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in + let status = status#set_obj theorem in + let status = status#set_stack ninitial_stack in + let status = subst_metasenv_and_fix_names status in + + let cut_theorem = + let rs = List.map (fun x -> mk_id x) rs in + 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 "cut")] in + let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in + + let status = NTactics.block_tac + (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.shift_tac; + NTactics.case_tac "cut"; + NTactics.apply_tac ("",0,t) + (* ; + NTactics.merge_tac; + NTactics.merge_tac; + NTactics.skip_tac*)])) status in + status,status#obj ;; - -let ast_of_sort s = - match s with - NCic.Prop -> `Prop,"ind" - | NCic.Type u -> - let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in - (try - if String.sub u 0 4 = "Type" then - `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u - else if String.sub u 0 5 = "CProp" then - `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u - else - (prerr_endline u; - assert false) - with Failure _ -> assert false) -;;