From: Ferruccio Guidi Date: Thu, 10 May 2007 12:59:52 +0000 (+0000) Subject: Procedural: clear tactics added X-Git-Tag: make_still_working~6339 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3d4ea54cb895a1adc6cb327df42e1394b3f2bea;p=helm.git Procedural: clear tactics added --- diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 95c4c1a9a..18e1ecc5b 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -43,6 +43,7 @@ module DTI = DoubleTypeInference module Cl = ProceduralClassify module T = ProceduralTypes module Cn = ProceduralConversion +module H = ProceduralHelpers type status = { sorts : (C.id, A.sort_kind) Hashtbl.t; @@ -178,6 +179,8 @@ with Invalid_argument _ -> failwith "A2P.get_ind_names" (* proof construction *******************************************************) +let used_premise = C.Name "USED" + let mk_exp_args hd tl classes synth = let meta id = C.AImplicit (id, None) in let map v (cl, b) = @@ -250,12 +253,16 @@ let mk_rewrite st dtext what qs tl direction = let rec proc_lambda st name v t = let dno = DTI.does_not_occur 1 (cic t) in - let dno = dno && match get_inner_types st v with + let dno = dno && match get_inner_types st t with | None -> true | Some (it, et) -> DTI.does_not_occur 1 (cic it) && DTI.does_not_occur 1 (cic et) in - let name = if dno then C.Anonymous else name in + let name = match dno, name with + | true, _ -> C.Anonymous + | false, C.Anonymous -> H.mk_fresh_name st.context used_premise + | false, name -> name + in let entry = Some (name, C.Decl (cic v)) in let intro = get_intro name in proc_proof (add st entry intro) t @@ -350,12 +357,14 @@ and proc_other st what = and proc_proof st t = let f st = - let xet = match get_inner_types st t with - | Some (_, et) -> Some (cic et) - | None -> None + let xtypes, note = match get_inner_types st t with + | Some (it, et) -> Some (cic it, cic et), + (Printf.sprintf "\nInferred: %s\nExpected: %s" + (Pp.ppterm (cic it)) (Pp.ppterm (cic et))) + | None -> None, "\nNo types" in - let context, clears = Cn.get_clears st.context (cic t) xet in - let note = Pp.ppcontext st.context in + let context, clears = Cn.get_clears st.context (cic t) xtypes in + let note = Pp.ppcontext st.context ^ note in {st with context = context; clears = clears; clears_note = note} in match t with diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 68b47341c..b8cdc08ea 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -145,44 +145,48 @@ let mk_pattern psno predicate = let body = generalize psno predicate in clear_absts 0 psno body -let get_clears c p xet = +let get_clears c p xtypes = let meta = C.Implicit None in - let rec aux c names p et = function + let rec aux c names p it et = function | [] -> List.rev c, List.rev names | Some (C.Name name as n, C.Decl v) as hd :: tl -> let hd, names, v = - if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then + if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then Some (C.Anonymous, C.Decl v), name :: names, meta else hd, names, v in let p = C.Lambda (n, v, p) in + let it = C.Prod (n, v, it) in let et = C.Prod (n, v, et) in - aux (hd :: c) names p et tl + aux (hd :: c) names p it et tl | Some (C.Name name as n, C.Def (v, x)) as hd :: tl -> let hd, names, v = - if DTI.does_not_occur 1 p && DTI.does_not_occur 1 et then + if DTI.does_not_occur 1 p && DTI.does_not_occur 1 it && DTI.does_not_occur 1 et then Some (C.Anonymous, C.Def (v, x)), name :: names, meta else hd, names, v in let p = C.LetIn (n, v, p) in + let it = C.LetIn (n, v, it) in let et = C.LetIn (n, v, et) in - aux (hd :: c) names p et tl + aux (hd :: c) names p it et tl | Some (C.Anonymous as n, C.Decl v) as hd :: tl -> let p = C.Lambda (n, meta, p) in + let it = C.Lambda (n, meta, it) in let et = C.Lambda (n, meta, et) in - aux (hd :: c) names p et tl + aux (hd :: c) names p it et tl | Some (C.Anonymous as n, C.Def (v, _)) as hd :: tl -> let p = C.LetIn (n, meta, p) in + let it = C.LetIn (n, meta, it) in let et = C.LetIn (n, meta, et) in - aux (hd :: c) names p et tl + aux (hd :: c) names p it et tl | None :: tl -> assert false in - match xet with - | Some et -> aux [] [] p et c - | None -> c, [] + match xtypes with + | Some (it, et) -> aux [] [] p it et c + | None -> c, [] let clear c hyp = let rec aux c = function diff --git a/helm/software/components/acic_procedural/proceduralConversion.mli b/helm/software/components/acic_procedural/proceduralConversion.mli index f41f8e56c..e5b2dcdcf 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.mli +++ b/helm/software/components/acic_procedural/proceduralConversion.mli @@ -32,6 +32,7 @@ val lift: int -> int -> Cic.annterm -> Cic.annterm val mk_pattern: int -> Cic.annterm -> Cic.annterm val get_clears: - Cic.context -> Cic.term -> Cic.term option -> Cic.context * string list + Cic.context -> Cic.term -> (Cic.term * Cic.term) option -> + Cic.context * string list val clear: Cic.context -> string -> Cic.context