helm/software/components/ng_tactics/nInversion.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 let fresh_name =
  15  let i = ref 0 in
  16  function () ->
  17   incr i;
  18   "z" ^ string_of_int !i
  19 ;;
  20
  21 let mk_id id =
  22  let id = if id = "_" then fresh_name () else id in
  23   CicNotationPt.Ident (id,None)
  24 ;;
  25
  26 let rec split_arity ~subst context te =
  27   match NCicReduction.whd ~subst context te with
  28    | NCic.Prod (name,so,ta) ->
  29        split_arity ~subst ((name, (NCic.Decl so))::context) ta
  30    | t -> context, t
  31 ;;
  32
  33 let mk_appl =
  34  function
  35     [] -> assert false
  36   | [x] -> x
  37   | l -> CicNotationPt.Appl l
  38 ;;
  39
  40 let rec mk_prods l t =
  41   match l with
  42     [] -> t
  43   | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
  44 ;;
  45
  46 let rec mk_lambdas l t =
  47   match l with
  48     [] -> t
  49   | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
  50 ;;
  51
  52 let rec mk_arrows l t =
  53   match l with
  54     [] -> t
  55   | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id "_", Some hd), mk_arrows tl t)
  56 ;;
  57
  58 let subst_metasenv_and_fix_names status =
  59   let u,h,metasenv, subst,o = status#obj in
  60   let o =
  61     NCicUntrusted.map_obj_kind ~skip_body:true
  62      (NCicUntrusted.apply_subst subst []) o
  63   in
  64    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
  65 ;;
  66
  67 let mk_inverter name it leftno status baseuri =
  68  prerr_endline ("leftno = " ^ string_of_int leftno);
  69  let _,ind_name,ty,cl = it in
  70  prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
  71  let ncons = List.length cl in
  72  (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
  73  let params = List.rev_map (function name,_ -> mk_id name) params in
  74  prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
  75  let args,sort = split_arity ~subst:[] [] ty in
  76  prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
  77  (*let args = List.rev_map (function name,_ -> mk_id name) args in
  78  prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
  79  let nparams = List.length args in
  80  prerr_endline ("nparams = " ^ string_of_int nparams);
  81
  82  let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
  83  prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
  84  let ls, rs = HExtlib.split_nth leftno xs in
  85  prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls));
  86  prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs));
  87  let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
  88
  89  let id_xs = List.map mk_id xs in
  90  let id_ls = List.map mk_id ls in
  91  let id_rs = List.map mk_id rs in
  92  let id_ys = List.map mk_id ys in
  93
  94  (* pseudocode  let t = Lambda y1 ... yr. xs_ = ys_ -> pred *)
  95
  96  (* check: assuming we have more than one right parameter *)
  97  (* pred := P yr- *)
  98  let pred = mk_appl ((mk_id "P")::id_ys) in
  99
 100  let selection = HExtlib.mk_list true (List.length ys) in
 101  let prods =
 102    let rec prodaux = function
 103        [],[],[] -> pred
 104      | false :: l,x::xs,y::ys -> prodaux (l,xs,ys)
 105      | true :: l,x::xs,y::ys  ->
 106         CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
 107                               prodaux (l,xs,ys))
 108      | _ -> assert false
 109    in prodaux (selection,id_rs,id_ys)
 110  in
 111
 112  let lambdas = mk_lambdas (ys@["p"]) prods in
 113
 114  let hyplist =
 115    let rec hypaux k = function
 116        0 -> []
 117      | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
 118    in (hypaux 1 ncons)
 119  in
 120  prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
 121  let theorem = mk_prods xs
 122                 (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort `Prop))),
 123                 mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
 124                                   Some (CicNotationPt.Implicit `JustOne)),
 125                                   mk_appl (mk_id "P"::id_rs)))))
 126  in
 127  let t = mk_appl ( [mk_id (ind_name ^ "_ind"); lambdas] @
 128                    List.map mk_id hyplist @
 129                    CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
 130
 131  prerr_endline ("NINVERTER 0");
 132  let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
 133                          (baseuri ^ name ^ ".def",
 134                            0,CicNotationPt.Theorem (`Theorem,name,theorem,Some (CicNotationPt.Implicit (`Tagged "inv")))) in
 135  prerr_endline ("NINVERTER 1");
 136  let uri,height,nmenv,nsubst,nobj = theorem in
 137  let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
 138  let status = status#set_obj theorem in
 139  let status = status#set_stack ninitial_stack in
 140  let status = subst_metasenv_and_fix_names status in
 141
 142  let cut_theorem =
 143    mk_arrows (List.map
 144      (fun x -> let x = mk_id x in mk_appl [mk_id "eq";
 145                                            CicNotationPt.Implicit `JustOne;
 146                                            x;x]) rs) (mk_appl (mk_id "P"::List.map mk_id rs)) in
 147  let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
 148                     CicNotationPt.Implicit (`Tagged "end"));
 149                     CicNotationPt.Implicit (`Tagged "cut")] in
 150
 151  let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
 152  (*let branches =
 153    let rec branch_aux k = function
 154        0 -> [NTactics.apply_tac ("",0,mk_id "H")]
 155      | n -> NTactics.apply_tac ("",0,mk_id ("H"^(string_of_int k)))::(branch_aux (k+1) (n-1))
 156    in branch_aux 1 ncons
 157  in*)
 158
 159  let status = NTactics.block_tac
 160                         (NTactics.branch_tac::
 161                          NTactics.case_tac "inv"::
 162                          (intros @
 163                           [NTactics.apply_tac ("",0,cut);
 164                            NTactics.branch_tac;
 165                            NTactics.case_tac "end";
 166                            (*NTactics.intro_tac "Hcut";*)
 167                            NTactics.apply_tac ("",0,mk_id "Hcut");
 168                            NTactics.apply_tac ("",0,mk_id "refl_eq");
 169                            NTactics.shift_tac;
 170                            NTactics.case_tac "cut";
 171                            NTactics.apply_tac ("",0,t);
 172                         (*   NTactics.branch_tac]
 173                           @ branches @
 174                           [NTactics.merge_tac; *)
 175                            NTactics.merge_tac;
 176                            NTactics.merge_tac;
 177                            NTactics.skip_tac])) status in
 178  status,status#obj
 179 ;;
 180
 181
 182 let ast_of_sort s =
 183   match s with
 184      NCic.Prop -> `Prop,"ind"
 185    | NCic.Type u ->
 186       let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
 187       (try
 188         if String.sub u 0 4 = "Type" then
 189          `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
 190         else if String.sub u 0 5 = "CProp" then
 191          `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
 192         else
 193          (prerr_endline u;
 194          assert false)
 195        with Failure _ -> assert false)
 196 ;;