Procedural: the statement body and it inner types must satisfy the Barendregt

            convenction on bound variables

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index cc4ec10a340e9793999d5b09bbd3d12b4dcd40c8..b4f6053c04e493f2dcd5271ee74ebf0f3589e0c9 100644 (file)
--- 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 bfffb11ba21ab846bb26a51d46f891246d7ff0e6..fb95a6d0c4cf4e842831398e5f7186ac99ae77ac 100644 (file)
--- 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 a7dfcc957dc8a04ef54beb88a9425acd085f9f50..c374a1866c9b266659513bd107e8b8f8ba8dd71b 100644 (file)
--- 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 9d04c2f91f89d0c78667c50f1c5076c56e333065..1953ae7f1b6a5c385fcdbb6aad65b76740a15a28 100644 (file)
--- 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);