X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineStructuralRules.ml;h=e8956944528197c456992eb72d1dae5e777701a3;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=07ddf3a9ea4c77c430f3fe5c00d163e6abda76ee;hpb=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 07ddf3a9e..e89569445 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -25,128 +25,133 @@ open ProofEngineTypes -let clearbody ~hyp ~status:(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,_,_ = List.find (function (m,_,_) -> m=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 + 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 + 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 - 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)) + entry::context + | Some (_,Cic.Def (_,Some _)) -> assert false + ) canonical_context [] in - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] + 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] + in + mk_tactic (clearbody ~hyp) -let clear ~hyp:hyp_to_clear ~status:(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 = - List.find (function (m,_,_) -> m=goal) metasenv - in - let string_of_name = - function - C.Name n -> n - | C.Anonymous -> "_" +let 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 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")) + 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 - m,canonical_context',ty - | t -> t - ) metasenv - in - (curi,metasenv',pbo,pty), [goal] - + 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] + in + mk_tactic (clear ~hyp)