X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_procedural%2FproceduralHelpers.ml;h=fb95a6d0c4cf4e842831398e5f7186ac99ae77ac;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=0925289e250111e1921fd9d7daeadff63c6c9eb0;hpb=6bd485b5c69ab84ff70afc377a18456bb7860ffc;p=helm.git

diff --git a/components/acic_procedural/proceduralHelpers.ml b/components/acic_procedural/proceduralHelpers.ml
index 0925289e2..fb95a6d0c 100644
--- a/components/acic_procedural/proceduralHelpers.ml
+++ b/components/acic_procedural/proceduralHelpers.ml
@@ -106,6 +106,10 @@ let is_proof c t =
       | C.Sort _      -> false
       | _             -> assert false 
 
+let is_sort = function
+   | C.Sort _ -> true
+   | _        -> false 
+
 let is_unsafe h (c, t) = true
 
 let is_not_atomic = function
@@ -117,6 +121,8 @@ let is_not_atomic = function
    | C.MutConstruct _ -> false
    | _                -> true
 
+let is_atomic t = not (is_not_atomic t)
+
 let get_ind_type uri tyno =
    match E.get_obj Un.empty_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
@@ -152,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