X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineStructuralRules.ml;h=47921953742be893160a5c5751570af6923b1d87;hb=c78edd42f3ebc7c82bb319b876908bf17288ab04;hp=4677a33ac8221a1080d7d0f6953e9fe2b8a822ba;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index 4677a33ac..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 ~hyp = - let clear ~hyp (proof, goal) = - let module C = Cic in - let curi,metasenv,pbo,pty = proof in +let clear_one ~hyp = + 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 ~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,56 +143,58 @@ let clear ~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 ~hyp) + PET.mk_tactic clear_one + +let clear ~hyps = + let clear status = + let aux status hyp = + match PET.apply_tactic (clear_one ~hyp) status with + | proof, [g] -> proof, g + | _ -> raise (PET.Fail (lazy "clear: internal error")) + in + let proof, g = List.fold_left aux status hyps in + proof, [g] + in + 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