X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=8995fbbeb8443ebed4cac5fd963b4b304483c7a7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=20b0f21c9f307f0c8f9f05042f3f6aa4147f3f8d;hpb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 20b0f21c9..8995fbbeb 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -25,128 +25,169 @@ open ProofEngineTypes -let clearbody ~hyp (proof, goal) = - let module C = Cic in - match hyp with - None -> assert false - | Some (_, C.Def (_, Some _)) -> assert false - | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") - | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body -> - let curi,metasenv,pbo,pty = proof in - let metano,_,_ = CicUtil.lookup_meta goal metasenv in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear_body -> - let cleared_entry = - let ty = - CicTypeChecker.type_of_aux' metasenv context term +let clearbody ~hyp = + let clearbody ~hyp (proof, goal) = + let module C = Cic in + let curi,metasenv,pbo,pty = proof in + let metano,_,_ = CicUtil.lookup_meta goal metasenv in + let string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let canonical_context' = + List.fold_right + (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 + cleared_entry::context + | None -> None::context + | Some (n,C.Decl t) + | Some (n,C.Def (t,None)) -> + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.empty_ugraph (* TASSI: FIXME *) + with + _ -> + raise + (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 + ) canonical_context [] + in + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + CicUniv.empty_ugraph (* TASSI: FIXME *) + with + _ -> + raise + (Fail + (lazy ("The correctness of the goal relies on the body of " ^ + hyp))) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + in + mk_tactic (clearbody ~hyp) + +let clear ~hyp = + let clear ~hyp (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 string_of_name = + function + C.Name n -> n + | C.Anonymous -> "_" + in + let metasenv' = + List.map + (function + (m,canonical_context,ty) when m = metano -> + let context_changed, canonical_context' = + List.fold_right + (fun entry (b, context) -> + match entry with + Some (Cic.Name hyp',_) when hyp' = 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)) -> + if b then + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv context t + CicUniv.empty_ugraph + with _ -> + raise + (Fail + (lazy ("Hypothesis " ^ string_of_name n ^ + " uses hypothesis " ^ hyp))) in - Some (n_to_clear_body, Cic.Decl ty) - in - cleared_entry::context - | None -> None::context - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("The correctness of hypothesis " ^ - string_of_name n ^ - " relies on the body of " ^ - string_of_name n_to_clear_body) - ) - in - entry::context - | Some (_,Cic.Def (_,Some _)) -> assert false - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("The correctness of the goal relies on the body of " ^ - string_of_name n_to_clear_body)) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] + (b, entry::context) + else + (b, entry::context) + ) canonical_context (false, []) + in + if not context_changed then + raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); + let _,_ = + try + CicTypeChecker.type_of_aux' metasenv canonical_context' ty + CicUniv.empty_ugraph + with _ -> + raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) + in + m,canonical_context',ty + | t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [goal] + in + mk_tactic (clear ~hyp) -let clear ~hyp:hyp_to_clear (proof, goal) = - let module C = Cic in - match hyp_to_clear with - None -> assert false - | Some (n_to_clear, _) -> - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = - CicUtil.lookup_meta goal metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" - in - let metasenv' = - List.map - (function - (m,canonical_context,ty) when m = metano -> - let canonical_context' = - List.fold_right - (fun entry context -> - match entry with - t when t == hyp_to_clear -> None::context - | None -> None::context - | Some (_,Cic.Def (_,Some _)) -> assert false - | Some (n,C.Decl t) - | Some (n,C.Def (t,None)) -> - let _ = - try - CicTypeChecker.type_of_aux' metasenv context t - with - _ -> - raise - (Fail - ("Hypothesis " ^ - string_of_name n ^ - " uses hypothesis " ^ - string_of_name n_to_clear) - ) - in - entry::context - ) canonical_context [] - in - let _ = - try - CicTypeChecker.type_of_aux' metasenv canonical_context' ty - with - _ -> - raise - (Fail - ("Hypothesis " ^ string_of_name n_to_clear ^ - " occurs in the goal")) - in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] +(* 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))))