(* $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 () ->
;;
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
| 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
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
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
;;