X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineStructuralRules.ml;h=47921953742be893160a5c5751570af6923b1d87;hb=82d4772ee9ac860f0a99b774612d2cf19838bb4b;hp=b1e23751f413afb1b7280bc56a2b1879ca943f73;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index b1e23751f..479219537 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -25,12 +25,12 @@ (* $Id$ *) -open ProofEngineTypes +module PET = ProofEngineTypes +module C = Cic let clearbody ~hyp = - let clearbody ~hyp (proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in + let clearbody (proof, goal) = + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,_,_ = CicUtil.lookup_meta goal metasenv in let string_of_name = function @@ -46,46 +46,51 @@ let clearbody ~hyp = (fun entry context -> match entry with Some (C.Name hyp',C.Def (term,ty)) when hyp = hyp' -> - let cleared_entry = - let ty = - match ty with - Some ty -> ty - | None -> - fst - (CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph) (* TASSI: FIXME *) - in - Some (C.Name hyp, Cic.Decl ty) - in + let cleared_entry = Some (C.Name hyp, Cic.Decl ty) in cleared_entry::context | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> + | Some (n,C.Decl t) -> let _,_ = try CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph (* TASSI: FIXME *) + CicUniv.oblivion_ugraph (* TASSI: FIXME *) with _ -> raise - (Fail + (PET.Fail (lazy ("The correctness of hypothesis " ^ string_of_name n ^ " relies on the body of " ^ hyp) )) in entry::context - | Some (_,Cic.Def (_,Some _)) -> assert false + | Some (n,Cic.Def (te,ty)) -> + (try + ignore + (CicTypeChecker.type_of_aux' metasenv context te + CicUniv.oblivion_ugraph (* TASSI: FIXME *)); + ignore + (CicTypeChecker.type_of_aux' metasenv context ty + CicUniv.oblivion_ugraph (* TASSI: FIXME *)); + with + _ -> + raise + (PET.Fail + (lazy ("The correctness of hypothesis " ^ + string_of_name n ^ + " relies on the body of " ^ hyp) + ))); + entry::context ) canonical_context [] in let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph (* TASSI: FIXME *) + CicUniv.oblivion_ugraph (* TASSI: FIXME *) with _ -> raise - (Fail + (PET.Fail (lazy ("The correctness of the goal relies on the body of " ^ hyp))) in @@ -93,14 +98,13 @@ let clearbody ~hyp = | t -> t ) metasenv in - (curi,metasenv',pbo,pty), [goal] + (curi,metasenv',_subst,pbo,pty, attrs), [goal] in - mk_tactic (clearbody ~hyp) + PET.mk_tactic clearbody let clear_one ~hyp = - let clear_one ~hyp (proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in + let clear_one (proof, goal) = + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in @@ -121,16 +125,15 @@ let clear_one ~hyp = (true, None::context) | None -> (b, None::context) | Some (n,C.Decl t) - | Some (n,Cic.Def (t,Some _)) - | Some (n,C.Def (t,None)) -> + | Some (n,Cic.Def (t,_)) -> if b then let _,_ = try CicTypeChecker.type_of_aux' metasenv context t - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph with _ -> raise - (Fail + (PET.Fail (lazy ("Hypothesis " ^ string_of_name n ^ " uses hypothesis " ^ hyp))) in @@ -140,68 +143,58 @@ let clear_one ~hyp = ) canonical_context (false, []) in if not context_changed then - raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); + raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty - CicUniv.empty_ugraph + CicUniv.oblivion_ugraph with _ -> - raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) + raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) in m,canonical_context',ty | t -> t ) metasenv in - (curi,metasenv',pbo,pty), [goal] + (curi,metasenv',_subst,pbo,pty, attrs), [goal] in - mk_tactic (clear_one ~hyp) + PET.mk_tactic clear_one let clear ~hyps = - let clear hyps status = + let clear status = let aux status hyp = - match apply_tactic (clear_one ~hyp) status with + match PET.apply_tactic (clear_one ~hyp) status with | proof, [g] -> proof, g - | _ -> raise (Fail (lazy "clear: internal error")) + | _ -> raise (PET.Fail (lazy "clear: internal error")) in let proof, g = List.fold_left aux status hyps in proof, [g] in - mk_tactic (clear hyps) + PET.mk_tactic clear (* Warning: this tactic has no effect on the proof term. It just changes the name of an hypothesis in the current sequent *) -let rename ~from ~to_ = - let rename ~from ~to_ (proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - CicUtil.lookup_meta goal metasenv - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.map - (function - Some (Cic.Name hyp,decl_or_def) when hyp = from -> - Some (Cic.Name to_,decl_or_def) - | item -> item - ) canonical_context - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] - in - mk_tactic (rename ~from ~to_) - -let set_goal n = - ProofEngineTypes.mk_tactic - (fun (proof, goal) -> - let (_, metasenv, _, _) = proof in - if CicUtil.exists_meta n metasenv then - (proof, [n]) - else - raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n)))) +let rename ~froms ~tos = + let rename (proof, goal) = + let error = "rename: lists of different length" in + let assocs = + try List.combine froms tos + with Invalid_argument _ -> raise (PET.Fail (lazy error)) + in + let curi, metasenv, _subst, pbo, pty, attrs = proof in + let metano, _, _ = CicUtil.lookup_meta goal metasenv in + let rename_map = function + | Some (Cic.Name hyp, decl_or_def) as entry -> + begin try Some (Cic.Name (List.assoc hyp assocs), decl_or_def) + with Not_found -> entry end + | entry -> entry + in + let map = function + | m, canonical_context, ty when m = metano -> + let canonical_context = List.map rename_map canonical_context in + m, canonical_context, ty + | conjecture -> conjecture + in + let metasenv = List.map map metasenv in + (curi, metasenv, _subst, pbo, pty, attrs), [goal] + in + PET.mk_tactic rename