X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=31c7f4e8d5058a4e16e8cc40b3b16c4800f3de9a;hb=cc23f034c9419186602d9250456241f2eba90d7c;hp=39607fefd7186fa04552131f59fda270d84f408e;hpb=c465c17581bf606e0330cbd89b238279c184ad35;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 39607fefd..31c7f4e8d 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -31,6 +31,7 @@ module TC   = CicTypeChecker
 module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
+module D    = Deannotate
 
 (* fresh name generator *****************************************************)
 
@@ -48,7 +49,7 @@ let split name =
 let join (s, i) =
    C.Name (if i < 0 then s else s ^ string_of_int i)
 
-let mk_fresh_name context name = 
+let mk_fresh_name context (name, k) = 
    let rec aux i = function
       | []                            -> name, i
       | Some (C.Name s, _) :: entries ->
@@ -56,11 +57,11 @@ let mk_fresh_name context name =
 	 if m = name && j >= i then aux (succ j) entries else aux i entries
       | _ :: entries                  -> aux i entries
    in
-   join (aux (-1) context)
+   join (aux k context)
 
 let mk_fresh_name context = function
    | C.Anonymous -> C.Anonymous
-   | C.Name s    -> mk_fresh_name context s
+   | C.Name s    -> mk_fresh_name context (split s)
 
 (* helper functions *********************************************************)
 
@@ -105,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
@@ -116,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
@@ -149,3 +156,109 @@ let get_ind_parameters c t =
       | _             -> assert false
    in
    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, ty, t) ->
+         let name = mk_fresh_name c name in
+         let entry = Some (name, C.Def (v, ty)) in
+         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+	 C.LetIn (name, v, ty, 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, ty, t) ->
+         let name = mk_fresh_name c name in
+         let entry = Some (name, C.Def (cic v, cic ty)) in
+         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
+	 C.ALetIn (id, name, v, ty, 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