From aa791b78493b604792383cf6326877d0d53e0458 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 22 Jul 2007 18:33:38 +0000 Subject: [PATCH] Procedural: the statement body and it inner types must satisfy the Barendregt convenction on bound variables --- components/acic_procedural/acic2Procedural.ml | 4 +- .../acic_procedural/proceduralHelpers.ml | 104 ++++++++++++++++++ .../acic_procedural/proceduralHelpers.mli | 7 +- .../acic_procedural/proceduralOptimizer.ml | 1 + 4 files changed, 114 insertions(+), 2 deletions(-) diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml index cc4ec10a3..b4f6053c0 100644 --- a/components/acic_procedural/acic2Procedural.ml +++ b/components/acic_procedural/acic2Procedural.ml @@ -201,6 +201,7 @@ let mk_convert st ?name sty ety note = assert (Ut.is_sober csty); assert (Ut.is_sober cety); if Ut.alpha_equivalence 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, ""(*note*))] | Some (id, i) -> @@ -294,7 +295,8 @@ and proc_letin st what name v t = mk_fwd_rewrite st dtext intro tl false v | v -> let qs = [proc_proof (next st) v; [T.Id ""]] in - st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] + let ity = H.acic_bc st.context ity in + st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)] in st, C.Decl (H.cic ity), rqv | None -> diff --git a/components/acic_procedural/proceduralHelpers.ml b/components/acic_procedural/proceduralHelpers.ml index bfffb11ba..fb95a6d0c 100644 --- a/components/acic_procedural/proceduralHelpers.ml +++ b/components/acic_procedural/proceduralHelpers.ml @@ -158,3 +158,107 @@ let get_ind_parameters c t = ps, disp let cic = D.deannotate_term + +(* 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, t) -> + let name = mk_fresh_name c name in + let entry = Some (name, C.Def (v, None)) in + let v, t = bc c v, bc (entry :: c) t in + C.LetIn (name, v, 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, t) -> + let name = mk_fresh_name c name in + let entry = Some (name, C.Def (cic v, None)) in + let v, t = bc c v, bc (entry :: c) t in + C.ALetIn (id, name, v, 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 diff --git a/components/acic_procedural/proceduralHelpers.mli b/components/acic_procedural/proceduralHelpers.mli index a7dfcc957..c374a1866 100644 --- a/components/acic_procedural/proceduralHelpers.mli +++ b/components/acic_procedural/proceduralHelpers.mli @@ -53,4 +53,9 @@ 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 cic: + Cic.annterm -> Cic.term +val cic_bc: + Cic.context -> Cic.term -> Cic.term +val acic_bc: + Cic.context -> Cic.annterm -> Cic.annterm diff --git a/components/acic_procedural/proceduralOptimizer.ml b/components/acic_procedural/proceduralOptimizer.ml index 9d04c2f91..1953ae7f1 100644 --- a/components/acic_procedural/proceduralOptimizer.ml +++ b/components/acic_procedural/proceduralOptimizer.ml @@ -263,6 +263,7 @@ and opt2_term g c t = let optimize_obj = function | C.Constant (name, Some bo, ty, pars, attrs) -> + let bo, ty = H.cic_bc [] bo, H.cic_bc [] ty in let g bo = Printf.eprintf "Optimized : %s\nPost Nodes: %u\n" (Pp.ppterm bo) (I.count_nodes 0 bo); -- 2.39.2