X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=54e8ebe050fb5a59cad06150b1c4238daa9da784;hb=54522577365be23b788d66c851ae5c78aebe5ffb;hp=bfffb11ba21ab846bb26a51d46f891246d7ff0e6;hpb=468ee32f0fc7de271454ed94643b4dd7c9578e5f;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index bfffb11ba..54e8ebe05 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -32,6 +32,8 @@ module PEH = ProofEngineHelpers module E = CicEnvironment module UM = UriManager module D = Deannotate +module PER = ProofEngineReduction +module Ut = CicUtil (* fresh name generator *****************************************************) @@ -81,7 +83,7 @@ let compose f g x = f (g x) let fst3 (x, _, _) = x let refine c t = - try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t + try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t with e -> Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e); Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c); @@ -89,7 +91,7 @@ let refine c t = raise e let get_type c t = - try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty + try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty with e -> Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c); Printf.eprintf "TC: term : %s\n" (Pp.ppterm t); @@ -124,7 +126,7 @@ let is_not_atomic = function let is_atomic t = not (is_not_atomic t) let get_ind_type uri tyno = - match E.get_obj Un.empty_ugraph uri with + match E.get_obj Un.oblivion_ugraph uri with | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno | _ -> assert false @@ -133,7 +135,7 @@ let get_default_eliminator context uri tyno ty = let ext = match get_tail context (get_type context ty) with | C.Sort C.Prop -> "_ind" | C.Sort C.Set -> "_rec" - | C.Sort C.CProp -> "_rec" + | C.Sort (C.CProp _) -> "_rect" | C.Sort (C.Type _) -> "_rect" | t -> Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t); @@ -158,3 +160,117 @@ let get_ind_parameters c t = ps, disp let cic = D.deannotate_term + +let occurs c ~what ~where = + let result = ref false in + let equality c t1 t2 = + let r = Ut.alpha_equivalence t1 t2 in + result := !result || r; r + in + let context, what, with_what = c, [what], [C.Rel 0] in + let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in + !result + +(* Ensuring Barendregt convenction ******************************************) + +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 + add_entries map (entry :: c) tl + +let get_sname c i = + try match List.nth c (pred i) with + | Some (Cic.Name sname, _) -> sname + | _ -> assert false + with + | Failure _ -> assert false + | Invalid_argument _ -> assert false + +let cic_bc c t = + let get_fix_decl (sname, i, w, v) = sname, w in + 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 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 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 entry = Some (name, C.Decl w) in + let w, t = bc c w, bc (entry :: c) t in + C.Prod (name, w, t) + | C.Appl vs -> + let vs = List.map (bc c) vs in + C.Appl vs + | C.MutCase (uri, tyno, u, v, ts) -> + let u, v, ts = bc c u, bc c v, List.map (bc c) ts in + C.MutCase (uri, tyno, u, v, ts) + | C.Cast (t, u) -> + let t, u = bc c t, bc c u in + C.Cast (t, u) + | C.Fix (i, fixes) -> + let d = add_entries get_fix_decl c fixes in + let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in + let fixes = List.map bc_fix fixes in + C.Fix (i, fixes) + | C.CoFix (i, cofixes) -> + let d = add_entries get_cofix_decl c cofixes in + let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in + let cofixes = List.map bc_cofix cofixes in + C.CoFix (i, cofixes) + | t -> t + in + bc c t + +let acic_bc c t = + let get_fix_decl (id, sname, i, w, v) = sname, cic w in + 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 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 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 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) + | C.AAppl (id, vs) -> + let vs = List.map (bc c) vs in + C.AAppl (id, vs) + | C.AMutCase (id, uri, tyno, u, v, ts) -> + let u, v, ts = bc c u, bc c v, List.map (bc c) ts in + C.AMutCase (id, uri, tyno, u, v, ts) + | C.ACast (id, t, u) -> + let t, u = bc c t, bc c u in + C.ACast (id, t, u) + | C.AFix (id, i, fixes) -> + let d = add_entries get_fix_decl c fixes in + let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in + let fixes = List.map bc_fix fixes in + C.AFix (id, i, fixes) + | C.ACoFix (id, i, cofixes) -> + let d = add_entries get_cofix_decl c cofixes in + let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in + let cofixes = List.map bc_cofix cofixes in + C.ACoFix (id, i, cofixes) + | C.ARel (id1, id2, i, sname) -> + let sname = get_sname c i in + C.ARel (id1, id2, i, sname) + | t -> t + in + bc c t