From da59a744767c799ad287489c55f2ff972f93d93c Mon Sep 17 00:00:00 2001 From: marangon Date: Wed, 11 Jan 2006 10:45:57 +0000 Subject: [PATCH] Code clean up. --- helm/ocaml/tactics/inversion.ml | 331 +++++++++++++------------------- 1 file changed, 131 insertions(+), 200 deletions(-) diff --git a/helm/ocaml/tactics/inversion.ml b/helm/ocaml/tactics/inversion.ml index ca175af94..6b563fe6a 100644 --- a/helm/ocaml/tactics/inversion.ml +++ b/helm/ocaml/tactics/inversion.ml @@ -28,10 +28,11 @@ exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple exception NotAnInductiveTypeToEliminate -let debug = false;; +let debug = false;; let debug_print = fun msg -> if debug then prerr_endline (Lazy.force msg) else () + let inside_obj = function | Cic.InductiveDefinition (l,params, nleft, _) -> (l,params,nleft) @@ -48,20 +49,19 @@ let rec baseuri_of_term = function | _ -> raise (Invalid_argument "baseuri_of_term") -(*prende il numero dei parametri sinistri, la lista dei parametri, la lista dei tipi dei parametri, -il tipo del GOAL e costruisce il termine per la cut ossia DX1 = DX1 -> ... DXn=DXn -> GOALTY *) -let rec foo_cut nleft l param_ty_l body uri_of_eq = +(* prende il numero dei parametri sinistri, la lista dei parametri, la lista +dei tipi dei parametri, il tipo del GOAL e costruisce il termine per la cut +ossia DX1 = DX1 -> ... DXn=DXn -> GOALTY *) - if nleft >0 then foo_cut (nleft-1) (List.tl l) (List.tl param_ty_l) body uri_of_eq - else match l with - | hd::tl -> Cic.Prod (Cic.Anonymous, - Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); - (List.hd param_ty_l) ; - hd; - hd], - foo_cut nleft (List.map (CicSubstitution.lift 1) tl) (List.tl param_ty_l) (CicSubstitution.lift 1 body) uri_of_eq - ) - | [] -> body +let rec foo_cut nleft l param_ty_l body uri_of_eq = + if nleft > 0 then foo_cut (nleft-1) (List.tl l) (List.tl param_ty_l) body + uri_of_eq + else match l with + | hd::tl -> Cic.Prod (Cic.Anonymous, Cic.Appl[Cic.MutInd (uri_of_eq ,0,[]); + (List.hd param_ty_l) ; hd; hd], foo_cut nleft + (List.map (CicSubstitution.lift 1) tl) (List.tl param_ty_l) + (CicSubstitution.lift 1 body) uri_of_eq ) + | [] -> body ;; (* da una catena di prod costruisce una lista dei termini che lo compongono.*) @@ -69,7 +69,6 @@ let rec list_of_prod term = match term with | Cic.Prod (Cic.Anonymous,src,tgt) -> [src] @ (list_of_prod tgt) | _ -> [term] - ;; @@ -92,13 +91,10 @@ match l with let foo_appl nleft nright_consno term uri = let l = [] in let a = ref l in - for n = 1 to nleft do a := !a @ [(Cic.Implicit None)] - done; a:= !a @ [term]; - for n = 1 to nright_consno do a := !a @ [(Cic.Implicit None)] done; @@ -106,217 +102,152 @@ let foo_appl nleft nright_consno term uri = ;; - -let rec foo_prod nright param_ty_l l l2 base_rel body uri_of_eq nleft termty isSetType term = - match param_ty_l with - | hd::tl -> Cic.Prod (Cic.Anonymous, - Cic.Appl[Cic.MutInd(uri_of_eq,0,[]); - hd; - (List.hd l); - Cic.Rel base_rel - ], - foo_prod (nright-1) tl (List.map (CicSubstitution.lift 1) (List.tl l)) - (List.map (CicSubstitution.lift 1) l2) - base_rel - (CicSubstitution.lift 1 body) - uri_of_eq nleft - (CicSubstitution.lift 1 termty) - isSetType - (CicSubstitution.lift 1 term)) - - - | [] -> ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) - ~what: (if isSetType then ((cut_first (1+nleft) (term_to_list termty) ) @ [term] ) - else (cut_first (1+nleft) (term_to_list termty) ) ) - ~with_what: (List.map (CicSubstitution.lift (-1)) l2) - ~where:body - (*TODO lo stesso sottotermine di body puo' essere sia sx che dx!*) +let rec foo_prod nright param_ty_l l l2 base_rel body uri_of_eq nleft termty + isSetType term = + match param_ty_l with + | hd::tl -> Cic.Prod ( + Cic.Anonymous, + Cic.Appl[Cic.MutInd(uri_of_eq,0,[]); hd; (List.hd l); Cic.Rel base_rel], + foo_prod (nright-1) tl (List.map (CicSubstitution.lift 1) (List.tl l)) + (List.map (CicSubstitution.lift 1) l2) + base_rel (CicSubstitution.lift 1 body) + uri_of_eq nleft (CicSubstitution.lift 1 termty) + isSetType (CicSubstitution.lift 1 term)) + | [] -> ProofEngineReduction.replace_lifting + ~equality:(ProofEngineReduction.alpha_equivalence) + ~what: (if isSetType + then ((cut_first (1+nleft) (term_to_list termty) ) @ [term] ) + else (cut_first (1+nleft) (term_to_list termty) ) ) + ~with_what: (List.map (CicSubstitution.lift (-1)) l2) + ~where:body +(*TODO lo stesso sottotermine di body puo' essere sia sx che dx!*) ;; - -let rec foo_lambda nright param_ty_l nright_ param_ty_l_ l l2 base_rel body uri_of_eq nleft termty isSetType ty_indty term = +let rec foo_lambda nright param_ty_l nright_ param_ty_l_ l l2 base_rel body + uri_of_eq nleft termty isSetType ty_indty term = (*assert nright >0 *) match param_ty_l with - | hd::tl ->Cic.Lambda ((Cic.Name ("lambda" ^ (string_of_int nright))), - hd, (* typ *) - foo_lambda (nright-1) tl - nright_ param_ty_l_ - (List.map (CicSubstitution.lift 1) l) - (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) - base_rel - (CicSubstitution.lift 1 body) - uri_of_eq nleft - (CicSubstitution.lift 1 termty) - isSetType ty_indty - (CicSubstitution.lift 1 term)) - | [] when isSetType -> Cic.Lambda ( - (Cic.Name ("lambda" ^ (string_of_int nright))), - (ProofEngineReduction.replace_lifting ~equality:(ProofEngineReduction.alpha_equivalence) - ~what: (cut_first (1+nleft) (term_to_list termty) ) - ~with_what: (List.map (CicSubstitution.lift (-1)) l2) - ~where:termty), (* tipo di H con i parametri destri sostituiti *) - foo_prod nright_ param_ty_l_ - (List.map (CicSubstitution.lift 1) l) - (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) - (base_rel+1) (CicSubstitution.lift 1 body) - uri_of_eq nleft - (CicSubstitution.lift 1 termty) isSetType - (CicSubstitution.lift 1 term)) - | [] -> foo_prod nright_ param_ty_l_ l l2 - base_rel body uri_of_eq - nleft termty isSetType term + | hd::tl ->Cic.Lambda ( + (Cic.Name ("lambda" ^ (string_of_int nright))), + hd, (* typ *) + foo_lambda (nright-1) tl nright_ param_ty_l_ + (List.map (CicSubstitution.lift 1) l) + (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) + base_rel (CicSubstitution.lift 1 body) + uri_of_eq nleft + (CicSubstitution.lift 1 termty) + isSetType ty_indty + (CicSubstitution.lift 1 term)) + | [] when isSetType -> Cic.Lambda ( + (Cic.Name ("lambda" ^ (string_of_int nright))), + (ProofEngineReduction.replace_lifting + ~equality:(ProofEngineReduction.alpha_equivalence) + ~what: (cut_first (1+nleft) (term_to_list termty) ) + ~with_what: (List.map (CicSubstitution.lift (-1)) l2) + ~where:termty), (* tipo di H con i parametri destri sostituiti *) + foo_prod nright_ param_ty_l_ (List.map (CicSubstitution.lift 1) l) + (List.map (CicSubstitution.lift 1) (l2 @ [Cic.Rel 1])) + (base_rel+1) (CicSubstitution.lift 1 body) + uri_of_eq nleft + (CicSubstitution.lift 1 termty) isSetType + (CicSubstitution.lift 1 term)) + | [] -> foo_prod nright_ param_ty_l_ l l2 base_rel body uri_of_eq nleft + termty isSetType term ;; - - let inversion_tac ~term = let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let module P = PrimitiveTactics in let module PET = ProofEngineTypes in + let module PEH = ProofEngineHelpers in let inversion_tac ~term (proof, goal) = let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let (newproof, metasenv') = ProofEngineHelpers.subst_meta_in_proof proof metano term [] in + let (newproof, metasenv') = PEH.subst_meta_in_proof proof metano term [] in let uri_of_eq = HelmLibraryObjects.Logic.eq_URI in -(* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che e' la terza componente -della relativa congettura *) -let (_,_,body) = CicUtil.lookup_meta goal metasenv in - -(* estrae il tipo del termine oggetto di inversion, di solito un Cic.Appl list, ma..*) - - let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + (* dall'indice che indentifica il goal nel metasenv, ritorna il suo tipo, che + e' la terza componente della relativa congettura *) + let (_,_,body) = CicUtil.lookup_meta goal metasenv in + (* estrae il tipo del termine(ipotesi) oggetto di inversion, + di solito un Cic.Appl *) + let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let uri = baseuri_of_term termty in let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in let l,params,nleft = inside_obj o in let (_,_,typeno,_) = - match termty with - C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) - | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> - (uri,exp_named_subst,typeno,args) - | _ -> raise NotAnInductiveTypeToEliminate + match termty with + C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) + | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> + (uri,exp_named_subst,typeno,args) + | _ -> raise NotAnInductiveTypeToEliminate in - let eliminator_uri = - - let buri = UriManager.buri_of_uri uri in - let name = - match o with - C.InductiveDefinition (tys,_,_,_) -> - let (name,_,_,_) = List.nth tys typeno in - name - |_ -> assert false - in - - -(* let ty_ty,_ = T.type_of_aux' metasenv context termty CicUniv.empty_ugraph in - let ext = - match ty_ty with - C.Sort C.Prop -> "_ind" - | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" - | C.Sort (C.Type _)-> "_rect" - | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple - | _ -> assert false - in -*) - - let ext = "_ind" in - UriManager.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") -in - - (* il tipo del tipo induttivo oggetto di inversione *) - + let buri = UriManager.buri_of_uri uri in + let name = + match o with + C.InductiveDefinition (tys,_,_,_) -> + let (name,_,_,_) = List.nth tys typeno in + name + |_ -> assert false + in + let ext = "_ind" in + UriManager.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") + in + (* il tipo del tipo induttivo da cui viene l'ipotesi oggetto di inversione *) let (_,_,ty_indty,cons_list) = (List.hd l) in - (*la lista ricavata dal tipo del tipo induttivo. *) + (*la lista di Cic.term ricavata dal tipo del tipo induttivo. *) let param_ty_l = list_of_prod ty_indty in let consno = List.length cons_list in let nright= (List.length param_ty_l)- (nleft+1) in - let isSetType = ((Pervasives.compare - (List.nth param_ty_l ((List.length param_ty_l)-1)) - (Cic.Sort Cic.Prop) - ) != 0) in - - - - -(* eliminiamo la testa di termty, in quanto e' il nome del predicato e non un parametro.*) -let cut_term = foo_cut nleft (List.tl (term_to_list termty)) (list_of_prod ty_indty) body uri_of_eq in - - - -(* cut DXn=DXn \to GOAL *) -let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in - -(* apply Hcut ; reflexivity (su tutti i goals aperti da apply_tac) *) -let proof2, gl2 = PET.apply_tactic - (Tacticals.then_ - ~start: (P.apply_tac (C.Rel 1) - ) (* apply Hcut *) - ~continuation: (EqualityTactics.reflexivity_tac - ) - ) - (proof1, (List.hd gl1)) - + (List.nth param_ty_l ((List.length param_ty_l)-1)) + (Cic.Sort Cic.Prop)) != 0) + in + (* eliminiamo la testa di termty, in quanto e' il nome del predicato e non un parametro.*) + let cut_term = foo_cut nleft (List.tl (term_to_list termty)) + (list_of_prod ty_indty) body uri_of_eq in + (* cut DXn=DXn \to GOAL *) + let proof1,gl1 = PET.apply_tactic (P.cut_tac cut_term) (proof,goal) in + (* apply Hcut ; reflexivity (su tutti i goals aperti da apply_tac) *) + let proof2, gl2 = PET.apply_tactic + (Tacticals.then_ + ~start: (P.apply_tac (C.Rel 1)) (* apply Hcut *) + ~continuation: (EqualityTactics.reflexivity_tac) + ) (proof1, (List.hd gl1)) in - - - -(* apply (ledx_ind( lambda x. lambda y, ...)) *) - -let (t1,metasenv,t3,t4) = proof2 in -let goal2 = List.hd (List.tl gl1) in -let (metano,context,_) = CicUtil.lookup_meta goal2 metasenv in - -let cut_param_ty_l = (cut_first nleft (cut_last param_ty_l)) in - -(* la lista dei soli parametri destri *) -let l= cut_first (1+nleft) (term_to_list termty) in - -let lambda_t = foo_lambda nright cut_param_ty_l nright cut_param_ty_l l [] nright body uri_of_eq nleft termty isSetType ty_indty term in -let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in - -debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t))); -prerr_endline ("Term: " ^ (CicPp.ppterm termty)); -prerr_endline ("Body: " ^ (CicPp.ppterm body)); -prerr_endline ("Right param: " ^ (CicPp.ppterm (Cic.Appl l))); - - - - - - -let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t CicUniv.empty_ugraph in - -let proof2 = (t1,metasenv'',t3,t4) in - -let proof3,gl3 = PET.apply_tactic (P.apply_tac ref_t) - (proof2, goal2) in - -let new_goals = - ProofEngineHelpers.compare_metasenvs - ~oldmetasenv:metasenv ~newmetasenv:metasenv'' - in - -let patched_new_goals = - let (_,metasenv''',_,_) = proof3 in - List.filter - (function i -> List.exists (function (j,_,_) -> j=i) metasenv''' - ) new_goals @ gl3 - in - - - - -(*prerr_endline ("METASENV: " ^ CicMetaSubst.ppmetasenv metasenv []); DEBUG*) - - -(proof3, patched_new_goals) - + (* apply (ledx_ind( lambda x. lambda y, ...)) *) + let (t1,metasenv,t3,t4) = proof2 in + let goal2 = List.hd (List.tl gl1) in + let (metano,context,_) = CicUtil.lookup_meta goal2 metasenv in + let cut_param_ty_l = (cut_first nleft (cut_last param_ty_l)) in + (* la lista dei soli parametri destri *) + let l= cut_first (1+nleft) (term_to_list termty) in + let lambda_t = foo_lambda nright cut_param_ty_l nright cut_param_ty_l l [] + nright body uri_of_eq nleft termty isSetType ty_indty term in + let t = foo_appl nleft (nright+consno) lambda_t eliminator_uri in + debug_print (lazy ("Lambda_t: " ^ (CicPp.ppterm t))); + debug_print (lazy ("Term: " ^ (CicPp.ppterm termty))); + debug_print (lazy ("Body: " ^ (CicPp.ppterm body))); + debug_print (lazy ("Right param: " ^ (CicPp.ppterm (Cic.Appl l)))); + + let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t + CicUniv.empty_ugraph + in + let proof2 = (t1,metasenv'',t3,t4) in + let proof3,gl3 = PET.apply_tactic (P.apply_tac ref_t) (proof2, goal2) in + let new_goals = ProofEngineHelpers.compare_metasenvs + ~oldmetasenv:metasenv ~newmetasenv:metasenv'' + in + let patched_new_goals = + let (_,metasenv''',_,_) = proof3 in + List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') + new_goals @ gl3 + in + (*prerr_endline ("METASENV: " ^ CicMetaSubst.ppmetasenv metasenv []); DEBUG*) + (proof3, patched_new_goals) in - ProofEngineTypes.mk_tactic (inversion_tac ~term) ;; -- 2.39.2