Added initial support for inversion principles in Matita NG.

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

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 3628e5944b93a4708fd2e4fc6ae98bde8e5d6789..4305f915340941a414ccea26e4ce5a460d88b679 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -202,10 +202,52 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let flatten_appls =
+   let rec flatten_xns (uri, t) = uri, flatten_term t
+   and flatten_ms = function
+      | None   -> None
+      | Some t -> Some (flatten_term t)
+   and flatten_fix (name, i, ty, bo) =
+      name, i, flatten_term ty, flatten_term bo
+   and flatten_cofix (name, ty, bo) =
+      name, flatten_term ty, flatten_term bo
+   and flatten_term = function
+      | C.Sort _ as t -> t
+      | C.Implicit _ as t -> t
+      | C.Rel _ as t -> t 
+      | C.Const (uri, xnss) -> C.Const (uri, List.map flatten_xns xnss)
+      | C.Var (uri, xnss) -> C.Var (uri, List.map flatten_xns xnss)
+      | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, List.map flatten_xns xnss)
+      | C.MutConstruct (uri, tyno, consno, xnss) -> C.MutConstruct (uri, tyno, consno, List.map flatten_xns xnss)
+      | C.Meta (i, mss) -> C.Meta(i, List.map flatten_ms mss)
+(* begin flattening *)      
+      | C.Appl [t] -> flatten_term t
+      | C.Appl (C.Appl ts1 :: ts2) -> flatten_term (C.Appl (ts1 @ ts2))
+      | C.Appl [] -> assert false
+(* end flattening *)
+      | C.Appl ts -> C.Appl (List.map flatten_term ts)
+      | C.Cast (te, ty) -> C.Cast (flatten_term te, flatten_term ty)
+      | C.MutCase (sp, i, outty, t, pl) -> C.MutCase (sp, i, flatten_term outty, flatten_term t, List.map flatten_term pl)
+      | C.Prod (n, s, t) -> C.Prod (n, flatten_term s, flatten_term t)
+      | C.Lambda (n, s, t) -> C.Lambda (n, flatten_term s, flatten_term t)
+      | C.LetIn (n, ty, s, t) -> C.LetIn (n, flatten_term ty, flatten_term s, flatten_term t)
+      | C.Fix (i, fl) -> C.Fix (i, List.map flatten_fix fl)
+      | C.CoFix (i, fl) -> C.CoFix (i, List.map flatten_cofix fl)
+   in
+   flatten_term
+
+let sober ?(flatten=false) c t =
+   if flatten then flatten_appls t else (assert (Ut.is_sober c t); t)
+
+let alpha ?flatten c t1 t2 =
+   let t1 = sober ?flatten c t1 in
+   let t2 = sober ?flatten c t2 in
+   Ut.alpha_equivalence t1 t2
+
 let occurs c ~what ~where =
    let result = ref false in
    let equality c t1 t2 =
-      let r = Ut.alpha_equivalence t1 t2 in
+      let r = alpha ~flatten:true c t1 t2 in
       result := !result || r; r
    in
    let context, what, with_what = c, [what], [C.Rel 0] in
@@ -232,12 +274,12 @@ 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
+      let entry = Some (C.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
+      | Some (C.Name sname, _) -> sname
       | _                        -> assert false
    with 
       | Failure _          -> assert false
@@ -335,3 +377,11 @@ let acic_bc c t =
       | t -> t
    in 
    bc c t
+
+let is_acic_proof sorts context v =
+   let id = Ut.id_of_annterm v in
+   try match Hashtbl.find sorts id with
+      | `Prop -> true
+      | _     -> false
+   with Not_found -> is_proof context (cic v)
+