let mk_id id =
let id = if id = "_" then fresh_name () else id in
- CicNotationPt.Ident (id,None)
+ NotationPt.Ident (id,None)
;;
-let rec split_arity ~subst context te =
- match NCicReduction.whd ~subst context te with
+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
;;
function
[] -> assert false
| [x] -> x
- | l -> CicNotationPt.Appl l
+ | l -> NotationPt.Appl l
;;
let rec mk_prods l t =
match l with
[] -> t
- | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
+ | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
;;
let rec mk_arrows ?(pattern=false) xs ys selection target =
[],[],[] -> target
| false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
| true :: l,x::xs,y::ys ->
- CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then CicNotationPt.Implicit `JustOne else mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
+ 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)
| _ -> 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 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
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)))), mk_appl (mk_id "P"::id_rs)))))
+ (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)))))
in
let status, theorem =
GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
- CicNotationPt.Theorem
+ NotationPt.Theorem
(`Theorem,name,theorem,
- Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
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),
+ let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
-CicNotationPt.Implicit (`Tagged "end"));
- CicNotationPt.Implicit (`Tagged "cut")] in
+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 where =
"",0,(None,[],
Some (
mk_arrows ~pattern:true
- (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys))
- (HExtlib.mk_list CicNotationPt.UserInput (List.length ys))
- selection CicNotationPt.UserInput)) in
+ (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
let status =
NTactics.block_tac