From: Ferruccio Guidi Date: Wed, 6 May 2009 18:26:56 +0000 (+0000) Subject: - cicUtil: is_sober now detects folded applications X-Git-Tag: make_still_working~4016 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdd3fc617825db73ce08a0cb700e2a8e115b4fb3;p=helm.git - cicUtil: is_sober now detects folded applications - Procedural: bugfix in pattern generation for elim/rewrite, better debug output, applications are flattened before alpha-conversion to hide a bug of the double type inference :( (it generates folded applications) - applyTransformation: coercions are shown when rendering a tactic because Procedural is not aware of coercions :( --- diff --git a/helm/software/components/acic_procedural/.depend b/helm/software/components/acic_procedural/.depend index fde9f7d63..8d0128744 100644 --- a/helm/software/components/acic_procedural/.depend +++ b/helm/software/components/acic_procedural/.depend @@ -15,8 +15,8 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi -procedural1.cmo: procedural1.cmi -procedural1.cmx: procedural1.cmi +procedural1.cmo: proceduralTypes.cmi procedural1.cmi +procedural1.cmx: proceduralTypes.cmx procedural1.cmi procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt index fde9f7d63..8d0128744 100644 --- a/helm/software/components/acic_procedural/.depend.opt +++ b/helm/software/components/acic_procedural/.depend.opt @@ -15,8 +15,8 @@ proceduralMode.cmo: proceduralClassify.cmi proceduralMode.cmi proceduralMode.cmx: proceduralClassify.cmx proceduralMode.cmi proceduralConversion.cmo: proceduralHelpers.cmi proceduralConversion.cmi proceduralConversion.cmx: proceduralHelpers.cmx proceduralConversion.cmi -procedural1.cmo: procedural1.cmi -procedural1.cmx: procedural1.cmi +procedural1.cmo: proceduralTypes.cmi procedural1.cmi +procedural1.cmx: proceduralTypes.cmx procedural1.cmi procedural2.cmo: proceduralTypes.cmi proceduralHelpers.cmi \ proceduralConversion.cmi proceduralClassify.cmi procedural2.cmi procedural2.cmx: proceduralTypes.cmx proceduralHelpers.cmx \ diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index ed30f767b..dbd70428c 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -186,28 +186,27 @@ let mk_exp_args hd tl classes synth = if args = [] then b, hd else b, C.AAppl ("", hd :: args) let mk_convert st ?name sty ety note = + let ppterm t = + let a = ref "" in Ut.pp_term (fun s -> a := !a ^ s) [] st.context t; !a + in let e = Cn.hole "" in let csty, cety = H.cic sty, H.cic ety in - let script = + let note = if !debug then let sname = match name with None -> "" | Some (id, _) -> id in - let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s" - note sname (Pp.ppterm csty) (Pp.ppterm cety) - in - [T.Note note] - else [] + Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s" + note sname (ppterm csty) (ppterm cety) + else "" in - assert (Ut.is_sober st.context csty); - assert (Ut.is_sober st.context cety); - if Ut.alpha_equivalence csty cety then script else + if H.alpha_equivalence ~flatten:true st.context csty cety then [T.Note note] else let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in match name with - | None -> T.Change (sty, ety, None, e, "") :: script + | None -> [T.Change (sty, ety, None, e, note)] | Some (id, i) -> begin match get_entry st id with | C.Def _ -> assert false (* T.ClearBody (id, "") :: script *) | C.Decl _ -> - T.Change (ety, sty, Some (id, Some id), e, "") :: script + [T.Change (ety, sty, Some (id, Some id), e, note)] end let convert st ?name v = diff --git a/helm/software/components/acic_procedural/proceduralConversion.ml b/helm/software/components/acic_procedural/proceduralConversion.ml index 67b293393..8c9a1ddc6 100644 --- a/helm/software/components/acic_procedural/proceduralConversion.ml +++ b/helm/software/components/acic_procedural/proceduralConversion.ml @@ -119,19 +119,19 @@ let lift k n = in ann_term c -let clear_absts m = - let rec aux k n = function - | C.AImplicit (_, None) as t -> t - | C.ALambda (id, s, v, t) when k > 0 -> - C.ALambda (id, s, v, aux (pred k) n t) - | C.ALambda (_, _, _, t) when n > 0 -> - aux 0 (pred n) (lift 1 (-1) t) - | t when n > 0 -> - Printf.eprintf "CLEAR: %u %s\n" n (CicPp.ppterm (H.cic t)); - assert false - | t -> t - in - aux m +let mk_arel k = C.ARel ("", "", k, "") + +let mk_aappl ts = C.AAppl ("", ts) + +let rec clear_absts f n k = function + | t when n = 0 -> f k t + | C.ALambda (_, _, _, t) -> clear_absts f (pred n) (succ k) t + | t -> + let u = match mk_aappl [lift (succ k) 1 t; mk_arel (succ k)] with + | C.AAppl (_, [ C.AAppl (id, ts); t]) -> C.AAppl (id, ts @ [t]) + | t -> t + in + clear_absts f (pred n) (succ k) u let hole id = C.AImplicit (id, Some `Hole) @@ -182,11 +182,10 @@ let generalize n = | C.AFix (id, i, fl) -> C.AFix (id, i, List.map (gen_fix (List.length fl) k) fl) | C.ACoFix (id, i, fl) -> C.ACoFix (id, i, List.map (gen_cofix (List.length fl) k) fl) in - gen_term 0 + gen_term let mk_pattern psno predicate = - let body = generalize psno predicate in - clear_absts 0 psno body + clear_absts (generalize psno) psno 0 predicate let get_clears c p xtypes = let meta = C.Implicit None in diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index b2f73f311..c42fe7532 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -202,10 +202,52 @@ let get_ind_parameters c t = let cic = D.deannotate_term +let flatten_appls = + let rec flatten_xns (uri, t) = uri, flatten_term t + and flatten_ms = function + | None -> None + | Some t -> Some (flatten_term t) + and flatten_fix (name, i, ty, bo) = + name, i, flatten_term ty, flatten_term bo + and flatten_cofix (name, ty, bo) = + name, flatten_term ty, flatten_term bo + and flatten_term = function + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Rel _ as t -> t + | C.Const (uri, xnss) -> C.Const (uri, List.map flatten_xns xnss) + | C.Var (uri, xnss) -> C.Var (uri, List.map flatten_xns xnss) + | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, List.map flatten_xns xnss) + | C.MutConstruct (uri, tyno, consno, xnss) -> C.MutConstruct (uri, tyno, consno, List.map flatten_xns xnss) + | C.Meta (i, mss) -> C.Meta(i, List.map flatten_ms mss) +(* begin flattening *) + | C.Appl [t] -> flatten_term t + | C.Appl (C.Appl ts1 :: ts2) -> flatten_term (C.Appl (ts1 @ ts2)) + | C.Appl [] -> assert false +(* end flattening *) + | C.Appl ts -> C.Appl (List.map flatten_term ts) + | C.Cast (te, ty) -> C.Cast (flatten_term te, flatten_term ty) + | C.MutCase (sp, i, outty, t, pl) -> C.MutCase (sp, i, flatten_term outty, flatten_term t, List.map flatten_term pl) + | C.Prod (n, s, t) -> C.Prod (n, flatten_term s, flatten_term t) + | C.Lambda (n, s, t) -> C.Lambda (n, flatten_term s, flatten_term t) + | C.LetIn (n, ty, s, t) -> C.LetIn (n, flatten_term ty, flatten_term s, flatten_term t) + | C.Fix (i, fl) -> C.Fix (i, List.map flatten_fix fl) + | C.CoFix (i, fl) -> C.CoFix (i, List.map flatten_cofix fl) + in + flatten_term + +let sober ?(flatten=false) c t = + if flatten then flatten_appls t else (assert (Ut.is_sober c t); t) + +let alpha_equivalence ?flatten c t1 t2 = + let t1 = sober ?flatten c t1 in + let t2 = sober ?flatten c t2 in + Ut.alpha_equivalence t1 t2 + let occurs c ~what ~where = let result = ref false in let equality c t1 t2 = - let r = Ut.alpha_equivalence t1 t2 in + let r = alpha_equivalence ~flatten:true c t1 t2 in result := !result || r; r in let context, what, with_what = c, [what], [C.Rel 0] in @@ -232,12 +274,12 @@ let rec add_entries map c = function | [] -> c | hd :: tl -> let sname, w = map hd in - let entry = Some (Cic.Name sname, C.Decl w) in + let entry = Some (C.Name sname, C.Decl w) in add_entries map (entry :: c) tl let get_sname c i = try match List.nth c (pred i) with - | Some (Cic.Name sname, _) -> sname + | Some (C.Name sname, _) -> sname | _ -> assert false with | Failure _ -> assert false @@ -342,3 +384,4 @@ let is_acic_proof sorts context v = | `Prop -> true | _ -> false with Not_found -> is_proof context (cic v) + diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 203224371..03faf269b 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -25,52 +25,79 @@ val mk_fresh_name: bool -> Cic.context -> Cic.name -> Cic.name + val list_fold_right_cps: ('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c + val list_fold_left_cps: ('b -> 'c) -> (('b -> 'c) -> 'b -> 'a -> 'c) -> 'b -> 'a list -> 'c + val list_map_cps: ('b list -> 'c) -> (('b -> 'c) -> 'a -> 'c) -> 'a list -> 'c + val identity: 'a -> 'a + val compose: ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + val fst3: 'a * 'b * 'c -> 'a + val refine: Cic.context -> Cic.term -> Cic.term + val get_type: string -> Cic.context -> Cic.term -> Cic.term + val is_prop: Cic.context -> Cic.term -> bool + val is_proof: Cic.context -> Cic.term -> bool + val is_sort: Cic.term -> bool + val is_unsafe: int -> Cic.context * Cic.term -> bool + val is_not_atomic: Cic.term -> bool + val is_atomic: Cic.term -> bool + val get_ind_type: UriManager.uri -> int -> int * Cic.inductiveType + val get_ind_names: UriManager.uri -> int -> string list + val get_default_eliminator: Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term + val get_ind_parameters: Cic.context -> Cic.term -> Cic.term list * int + val cic: Cic.annterm -> Cic.term + val occurs: Cic.context -> what:Cic.term -> where:Cic.term -> bool + val name_of_uri: UriManager.uri -> int option -> int option -> string + val cic_bc: Cic.context -> Cic.term -> Cic.term + val acic_bc: Cic.context -> Cic.annterm -> Cic.annterm + val is_acic_proof: (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm -> bool + +val alpha_equivalence: + ?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 8fa982859..deb8f1e68 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -565,7 +565,8 @@ let is_sober c t = | C.LetIn (_, v, ty, t) -> sober_term c (sober_term c (sober_term c g t) ty) v | C.Appl [] - | C.Appl [_] -> fun b -> false + | C.Appl [_] + | C.Appl (C.Appl _ :: _) -> fun b -> false | C.Appl ts -> sober_terms c g ts | C.MutCase (_, _, t, v, ts) -> sober_terms c (sober_term c (sober_term c g t) v) ts diff --git a/helm/software/components/cic/cicUtil.mli b/helm/software/components/cic/cicUtil.mli index 66fbebe47..237aa19a4 100644 --- a/helm/software/components/cic/cicUtil.mli +++ b/helm/software/components/cic/cicUtil.mli @@ -67,7 +67,7 @@ val rehash_obj: Cic.obj -> Cic.obj val alpha_equivalence: Cic.term -> Cic.term -> bool (* FG: Consistency Check - * detects applications without arguments + * detects applications without arguments and folded applications *) val is_sober: Cic.context -> Cic.term -> bool diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 2988af421..d572a78d9 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -222,11 +222,20 @@ let txt_of_cic_object in let aux = function | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm - -> + -> enable_notations false; - let str = stm_pp stm in enable_notations true; str + let str = stm_pp stm in + enable_notations true; + str (* FG: we disable notation for Inductive to avoid recursive notation *) - | stm -> stm_pp stm + | G.Executable (_, G.Tactic _) as stm -> + let hc = !Acic2content.hide_coercions in + Acic2content.hide_coercions := false; + let str = stm_pp stm in + Acic2content.hide_coercions := hc; + str +(* FG: we show coercion because the reconstruction is not aware of them *) + | stm -> stm_pp stm in let script = Acic2Procedural.procedural_of_acic_object diff --git a/helm/software/matita/contribs/procedural/library/library.conf.xml b/helm/software/matita/contribs/procedural/library/library.conf.xml index d20adfe2d..2f7264fc7 100644 --- a/helm/software/matita/contribs/procedural/library/library.conf.xml +++ b/helm/software/matita/contribs/procedural/library/library.conf.xml @@ -13,5 +13,8 @@ logic/equality/symmetric_eq nodefaults logic/equality/transitive_eq nodefaults + logic/equality/eq_elim_r nodefaults + logic/equality/eq_f nodefaults + logic/equality/eq_f' nodefaults