From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 22 Jul 2007 18:33:38 +0000 (+0000)
Subject: Procedural: the statement body and it inner types must satisfy the Barendregt
X-Git-Tag: 0.4.95@7852~292
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa791b78493b604792383cf6326877d0d53e0458;p=helm.git

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 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);