X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=42ee2c1609b9ab6d18a0f8bf30326c5cd326d930;hb=b7e39b3d2f611c716669fb8b36c0eba3cb66cc29;hp=f5f4e42adf0b6b06ca1387754ca4924045025a92;hpb=9b23e4b3a2862c73d0b61c96cd68562dac3bf7f6;p=helm.git diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index f5f4e42ad..42ee2c160 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -665,22 +665,34 @@ let reduction_tactic reduction_function term = None -> assert false | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv in - let term' = reduction_function context term in - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) - (*CSC: che si guadagni nulla in fatto di efficienza. *) - let replace = - ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: Il vero problema e' che non sapendo dove sia il term non *) + (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) + (*CSC: e' meglio prima cercare il termine e scoprirne il *) + (*CSC: contesto, poi ridurre e infine rimpiazzare. *) + let replace context where= +(*CSC: Per il momento se la riduzione fallisce significa solamente che *) +(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) +(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) + try + let term' = reduction_function context term in + ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' + ~where:where + with + _ -> where in - let ty' = replace ty in + let ty' = replace context ty in let context' = - List.map - (function - Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) - | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) - | None -> None - ) context + List.fold_right + (fun entry context -> + match entry with + Some (name,Cic.Def t) -> + (Some (name,Cic.Def (replace context t)))::context + | Some (name,Cic.Decl t) -> + (Some (name,Cic.Decl (replace context t)))::context + | None -> None::context + ) context [] in let metasenv' = List.map @@ -863,3 +875,141 @@ let change ~goal_input ~input = else raise NotConvertible ;; + +let clearbody = + let module C = Cic in + function + None -> assert false + | Some (_, C.Decl _) -> raise (Fail "No Body To Clear") + | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body -> + let curi,metasenv,pbo,pty = + match !proof with + None -> assert false + | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty + in + let metano,_,_ = + match !goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + let string_of_name = + function + C.Name n -> n + | C.Anonimous -> "_" + 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) -> + 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 + ) 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 + proof := Some (curi,metasenv',pbo,pty) +;; + +let clear hyp_to_clear = + let module C = Cic in + match hyp_to_clear with + None -> assert false + | Some (n_to_clear, _) -> + let curi,metasenv,pbo,pty = + match !proof with + None -> assert false + | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty + in + let metano,context,ty = + match !goal with + None -> assert false + | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + in + let string_of_name = + function + C.Name n -> n + | C.Anonimous -> "_" + 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 (n,C.Decl t) + | Some (n,C.Def t) -> + 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 + proof := Some (curi,metasenv',pbo,pty) +;;