NotationPt.Ident (id,None)
;;
-let rec split_arity ~subst context te =
- match NCicReduction.whd ~subst context te with
+let mk_sym s = NotationPt.Symbol (s,0);;
+
+let rec split_arity status ~subst context te =
+ match NCicReduction.whd status ~subst context te with
| NCic.Prod (name,so,ta) ->
- split_arity ~subst ((name, (NCic.Decl so))::context) ta
+ split_arity status ~subst ((name, (NCic.Decl so))::context) ta
| t -> context, t
;;
| hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
-let rec mk_arrows ?(pattern=false) xs ys selection target =
+let rec leibpatt = function
+ | [] -> NotationPt.UserInput
+ | false::sel -> leibpatt sel
+ | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_appl [NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.UserInput])),
+ leibpatt sel);;
+let rec jmeqpatt = function
+ | [] -> NotationPt.UserInput
+ | false::sel -> jmeqpatt sel
+ | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_appl [NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.Implicit `JustOne
+ ;NotationPt.UserInput
+ ;NotationPt.UserInput])),
+ jmeqpatt sel);;
+
+let rec mk_arrows ~jmeq xs ys selection target =
match selection,xs,ys with
[],[],[] -> target
- | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
- | true :: l,x::xs,y::ys ->
- NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])),
- mk_arrows ~pattern 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" ;
+ NotationPt.Implicit `JustOne;x;
+ NotationPt.Implicit `JustOne;y])),
+ mk_arrows ~jmeq xs ys l target)
+ | true :: l,x::xs,y::ys ->
+ NotationPt.Binder (`Forall, (mk_id "_",
+ Some (mk_appl [mk_sym "eq" ;
+ NotationPt.Implicit `JustOne;x;y])),
+ mk_arrows ~jmeq xs ys l target)
| _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
;;
let u,h,metasenv, subst,o = status#obj in
let o =
NCicUntrusted.map_obj_kind ~skip_body:true
- (NCicUntrusted.apply_subst subst []) o
+ (NCicUntrusted.apply_subst status subst []) o
in
- status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
+ status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
;;
-let mk_inverter name is_ind it leftno ?selection outsort 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: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
+ pp (lazy ("arity: " ^ status#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 status ~subst:[] [] leftno ty in
let params = List.rev_map (function name,_ -> mk_id name) params in
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,sort= split_arity status ~subst:[] [] ty in
+ pp (lazy ("arity sort: " ^ status#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
+ (* 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
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 id_rs id_ys selection pred in
let hyplist =
let rec hypaux k = function
| 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
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
+ mk_arrows ~jmeq rs rs selection (mk_appl (mk_id "P"::rs)) in
let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
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 (
- mk_arrows ~pattern:true
- (HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length ys))
- (HExtlib.mk_list NotationPt.UserInput (List.length ys))
- selection NotationPt.UserInput)) in
- let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+ 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 ~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 ::
NTactics.branch_tac;
NTactics.case_tac "end";
NTactics.apply_tac ("",0,mk_id "Hcut");
- NTactics.apply_tac ("",0,mk_id "refl");
+ NTactics.apply_tac ("",0,mk_sym "refl");
NTactics.shift_tac;
elim_tac ~what:("",0,mk_id "Hterm") ~where;
NTactics.branch_tac ~force:true] @
status,status#obj
;;
+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 (_s,_) ->
+ mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri
+;;
projects / helm.git / blobdiff