X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=4305f915340941a414ccea26e4ce5a460d88b679;hb=57c7d6ef239b4c2b070721715887684adf41159c;hp=a9fa6473f280ac7e12fc50422181b99cf0a248cf;hpb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index a9fa6473f..4305f9153 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -34,6 +34,7 @@ module UM = UriManager module D = Deannotate module PER = ProofEngineReduction module Ut = CicUtil +module DTI = DoubleTypeInference (* fresh name generator *****************************************************) @@ -61,9 +62,11 @@ let mk_fresh_name context (name, k) = in join (aux k context) -let mk_fresh_name context = function - | C.Anonymous -> C.Anonymous +let mk_fresh_name does_not_occur context = function | C.Name s -> mk_fresh_name context (split s) + | C.Anonymous -> + if does_not_occur then C.Anonymous + else mk_fresh_name context (split "LOCAL") (* helper functions *********************************************************) @@ -199,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 ?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 ~flatten:true c t1 t2 in result := !result || r; r in let context, what, with_what = c, [what], [C.Rel 0] in @@ -229,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 @@ -245,17 +290,20 @@ let cic_bc c t = let get_cofix_decl (sname, w, v) = sname, w in let rec bc c = function | C.LetIn (name, v, ty, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Def (v, ty)) in let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in C.LetIn (name, v, ty, t) | C.Lambda (name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl w) in let w, t = bc c w, bc (entry :: c) t in C.Lambda (name, w, t) | C.Prod (name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 t in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl w) in let w, t = bc c w, bc (entry :: c) t in C.Prod (name, w, t) @@ -287,17 +335,20 @@ let acic_bc c t = let get_cofix_decl (id, sname, w, v) = sname, cic w in let rec bc c = function | C.ALetIn (id, name, v, ty, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Def (cic v, cic ty)) in let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in C.ALetIn (id, name, v, ty, t) | C.ALambda (id, name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl (cic w)) in let w, t = bc c w, bc (entry :: c) t in C.ALambda (id, name, w, t) | C.AProd (id, name, w, t) -> - let name = mk_fresh_name c name in + let dno = DTI.does_not_occur 1 (cic t) in + let name = mk_fresh_name dno c name in let entry = Some (name, C.Decl (cic w)) in let w, t = bc c w, bc (entry :: c) t in C.AProd (id, name, w, t) @@ -326,3 +377,11 @@ let acic_bc c t = | t -> t in bc c t + +let is_acic_proof sorts context v = + let id = Ut.id_of_annterm v in + try match Hashtbl.find sorts id with + | `Prop -> true + | _ -> false + with Not_found -> is_proof context (cic v) +