Syntax error

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

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 7c58ae87e5fca689fd807990ab6a45cdc0395055..8df07952f65eea99e4feed26987c41ecc0677180 100644 (file)
--- 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,30 @@ 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 = 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);
+ 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);
+ 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
-     prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
+     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));
+     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_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 +120,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
@@ -127,9 +130,8 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
                                       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
-    
+                       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
@@ -147,24 +149,23 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
      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 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
 ;;