Merge remote-tracking branch 'origin/matita-lablgtk3'

[helm.git] / matita / components / ng_tactics / nInversion.ml

diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml
index 397a443dbcf37a4a6970e618b6b95ffd888b9576..f1da10cb7a08c3ab60f22fbdd9381620cd5b6c04 100644 (file)
--- a/matita/components/ng_tactics/nInversion.ml
+++ b/matita/components/ng_tactics/nInversion.ml
@@ -71,7 +71,7 @@ let rec jmeqpatt = function
 let rec mk_arrows ~jmeq xs ys selection target = 
   match selection,xs,ys with
     [],[],[] -> target
-  | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target
+  | false :: l,_x::xs,_y::ys -> mk_arrows ~jmeq xs ys l target
   | true :: l,x::xs,y::ys when jmeq ->
      NotationPt.Binder (`Forall, (mk_id "_",
        Some (mk_appl [mk_sym "jmsimeq" ; 
@@ -95,7 +95,7 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
 ;;
 
-let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
+let mk_inverter ~jmeq name _is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
  pp (lazy ("leftno = " ^ string_of_int leftno));
  let _,ind_name,ty,cl = it in
  pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
@@ -109,8 +109,11 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
  pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
  let nparams = List.length args in
 
+ (* the default is a dependent inversion *)
+ let is_dependent = (selection = None && (jmeq || nparams = 0)) in
+
  pp (lazy ("nparams = " ^ string_of_int nparams));
- if nparams = 0 
+ if (nparams = 0 && not is_dependent)
    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 (leftno+nparams+1)) in
@@ -118,24 +121,19 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
      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) (leftno+nparams+1)) in
+
+     (* dependent -> add Hterm to rs *)
+     let rs = if is_dependent then (rs@["Hterm"]) else rs 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) 
+     let selection = 
+       match selection with 
+         None -> HExtlib.mk_list true (List.length rs) 
        | Some s -> s
      in
-     let prods = mk_arrows ~jmeq id_rs id_ys selection pred in
     
      let hyplist = 
        let rec hypaux k = function
@@ -143,22 +141,22 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
          | 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 outsort, _suffix = NCicElim.ast_of_sort outsort in
      let theorem =
       mk_prods xs
-       (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (NotationPt.Sort outsort))),
-       mk_prods hyplist (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs)))))
+       (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))),
+        (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length rs)) (NotationPt.Sort outsort))),
+        mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
      in
      let status, theorem =
-      GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+      let attrs = `Generated, `Theorem, `InversionPrinciple in 
+      GrafiteDisambiguate.disambiguate_nobj status ~baseuri
        (baseuri ^ name ^ ".def",0,
          NotationPt.Theorem
-          (`Theorem,name,theorem,
-            Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+          (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
      in 
-     let uri,height,nmenv,nsubst,nobj = theorem 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
@@ -172,12 +170,16 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
                         
 NotationPt.Implicit (`Tagged "end"));
                         NotationPt.Implicit (`Tagged "cut")] in
-     let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
+     let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["Hterm";"P"]@hyplist) in
      let where =
       "",0,(None,[],
         Some (if jmeq then jmeqpatt selection
                      else leibpatt selection)) in
-     let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+     (* let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in *)
+     let elim_tac ~what ~where s =
+       try NTactics.elim_tac ~what ~where s 
+       with NTacStatus.Error _ -> NTactics.cases_tac ~what ~where s
+     in
      let status =
       NTactics.block_tac 
        (NTactics.branch_tac ::
@@ -203,6 +205,6 @@ NotationPt.Implicit (`Tagged "end"));
 
 let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
  try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri
- with NTacStatus.Error _ -> 
+ with NTacStatus.Error (_s,_) -> 
    mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri
 ;;