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

[helm.git] / components / acic_procedural / proceduralHelpers.ml

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