(* $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 () ->
| 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 =
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)
-;;
projects / helm.git / blobdiff