X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=cf4711db51f25320bcd6664822399e307f0b8662;hb=638616469ffdd7ba446ed0466e60ccf81a7b42cd;hp=aebda4bce746e543ed9d0f102f3329fa22e1bcae;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index aebda4bce..cf4711db5 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -23,13 +23,13 @@ let fresh_name = 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 ;; @@ -37,13 +37,13 @@ let mk_appl = 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 = @@ -51,7 +51,7 @@ 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") ;; @@ -60,21 +60,21 @@ let subst_metasenv_and_fix_names status = 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 @@ -118,15 +118,15 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = 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 @@ -138,18 +138,18 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = 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