X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=c42fe753212b780c382f6b5d647e7048cd7c33db;hb=68dbcd02022874a025a9444aa1125b0458816fbb;hp=fb95a6d0c4cf4e842831398e5f7186ac99ae77ac;hpb=fdeb64c7f9e870d43a4eb87153bf72e6f5705f01;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index fb95a6d0c..c42fe7532 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,9 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
+module DTI  = DoubleTypeInference
 
 (* fresh name generator *****************************************************)
 
@@ -59,12 +62,27 @@ let mk_fresh_name context (name, k) =
    in
    join (aux k context)
 
-let mk_fresh_name context = function
-   | C.Anonymous -> C.Anonymous
+let mk_fresh_name does_not_occur context = function
    | C.Name s    -> mk_fresh_name context (split s)
+   | C.Anonymous -> 
+      if does_not_occur then C.Anonymous 
+      else mk_fresh_name context (split "LOCAL")
 
 (* helper functions *********************************************************)
 
+let rec list_fold_right_cps g map l a = 
+   match l with
+      | []       -> g a
+      | hd :: tl ->
+         let h a = map g hd a in
+         list_fold_right_cps h map tl a
+
+let rec list_fold_left_cps g map a = function
+   | []       -> g a
+   | hd :: tl ->
+      let h a = list_fold_left_cps g map a tl in
+      map h a hd
+
 let rec list_map_cps g map = function
    | []       -> g []
    | hd :: tl -> 
@@ -81,31 +99,46 @@ let compose f g x = f (g x)
 let fst3 (x, _, _) = x
 
 let refine c t =
-   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
-   with e -> 
-      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
+   let error e = 
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
       raise e
+   in
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t with 
+      | Rf.RefineFailure s as e -> 
+         Printf.eprintf "REFINE FAILURE: %s\n" (Lazy.force s);
+	 error e
+      | e                       ->
+         Printf.eprintf "REFINE ERROR: %s\n" (Printexc.to_string e);
+	 error e
 
-let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
-   with e -> 
-      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
-      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
-      raise e
+let get_type msg c t =
+   let log s =
+      prerr_endline ("TC: " ^ s); 
+      prerr_endline ("TC: context: " ^ Pp.ppcontext c);
+      prerr_string "TC: term   : "; Ut.pp_term prerr_string [] c t;
+      prerr_newline (); prerr_endline ("TC: location: " ^ msg)
+   in   
+   try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
+      | TC.TypeCheckerFailure s as e ->
+        log ("failure: " ^ Lazy.force s); raise e        
+      | TC.AssertFailure s as e      -> 
+        log ("assert : " ^ Lazy.force s); raise e
 
 let get_tail c t =
    match PEH.split_with_whd (c, t) with
       | (_, hd) :: _, _ -> hd
       | _               -> assert false
 
-let is_proof c t =
-   match get_tail c (get_type c (get_type c t)) with
+let is_prop c t =
+   match get_tail c (get_type "is_prop" c t) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
 
+let is_proof c t =
+   is_prop c (get_type "is_prop" c t)
+
 let is_sort = function
    | C.Sort _ -> true
    | _        -> false 
@@ -124,18 +157,28 @@ let is_not_atomic = function
 let is_atomic t = not (is_not_atomic t)
 
 let get_ind_type uri tyno =
-   match E.get_obj Un.empty_ugraph uri with
+   match E.get_obj Un.default_ugraph uri with
       | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
       | _                                           -> assert false
 
+let get_ind_names uri tno =
+try   
+   let ts = match E.get_obj Un.default_ugraph uri with
+      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
+      | _                                      -> assert false
+   in
+   match List.nth ts tno with
+      | (_, _, _, cs) -> List.map fst cs  
+with Invalid_argument _ -> failwith "get_ind_names"
+
 let get_default_eliminator context uri tyno ty =
    let _, (name, _, _, _) = get_ind_type uri tyno in
-   let ext = match get_tail context (get_type context ty) with
-      | C.Sort C.Prop     -> "_ind"
-      | C.Sort C.Set      -> "_rec"
-      | C.Sort C.CProp    -> "_rec"
-      | C.Sort (C.Type _) -> "_rect"
-      | t                 -> 
+   let ext = match get_tail context (get_type "get_def_elim" context ty) with
+      | C.Sort C.Prop      -> "_ind"
+      | C.Sort C.Set       -> "_rec"
+      | C.Sort (C.CProp _) -> "_rect"
+      | C.Sort (C.Type _)  -> "_rect"
+      | t                  -> 
          Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
          assert false
    in
@@ -144,13 +187,13 @@ let get_default_eliminator context uri tyno ty =
    C.Const (uri, [])
 
 let get_ind_parameters c t =
-   let ty = get_type c t in
+   let ty = get_type "get_ind_pars 1" c t in
    let ps = match get_tail c ty with
       | C.MutInd _                  -> []
       | C.Appl (C.MutInd _ :: args) -> args
       | _                           -> assert false
    in
-   let disp = match get_tail c (get_type c ty) with
+   let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
       | C.Sort C.Prop -> 0
       | C.Sort _      -> 1
       | _             -> assert false
@@ -159,18 +202,84 @@ 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_equivalence ?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 = alpha_equivalence ~flatten:true c t1 t2 in
+      result := !result || r; r
+   in
+   let context, what, with_what = c, [what], [C.Rel 0] in
+   let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
+   !result
+
+let name_of_uri uri tyno cno =
+   let get_ind_type tys tyno =
+      let s, _, _, cs = List.nth tys tyno in s, cs
+   in
+   match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
+      | C.Variable (s, _, _, _, _), _, _                     -> s
+      | C.Constant (s, _, _, _, _), _, _                     -> s
+      | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
+         let s, _ = get_ind_type tys i in s
+      | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
+         let _, cs = get_ind_type tys i in
+	 let s, _ = List.nth cs (pred j) in s
+      | _                                                    -> assert false
+
 (* 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
+      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
@@ -180,18 +289,21 @@ 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.LetIn (name, v, ty, t) ->
+         let dno = DTI.does_not_occur 1 t in
+	 let name = mk_fresh_name dno 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 dno = DTI.does_not_occur 1 t in
+         let name = mk_fresh_name dno 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 dno = DTI.does_not_occur 1 t in
+         let name = mk_fresh_name dno 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)
@@ -222,18 +334,21 @@ 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.ALetIn (id, name, v, ty, t) ->
+         let dno = DTI.does_not_occur 1 (cic t) in
+         let name = mk_fresh_name dno 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 dno = DTI.does_not_occur 1 (cic t) in      
+         let name = mk_fresh_name dno 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 dno = DTI.does_not_occur 1 (cic t) in
+         let name = mk_fresh_name dno 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)
@@ -262,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)
+