X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=7d95d86775de199f8e83ee7a1798bf6556b9ef4e;hb=04c05cf08605156ba8c6fa7225b4a90496c03698;hp=d599bdeb2b8420c11ce83573535d11603e3e2b38;hpb=2e2648a9ed26d9b813de8e6a10e2776162565f09;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index d599bdeb2..7d95d8677 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -32,6 +32,104 @@ module PEH  = ProofEngineHelpers
 module E    = CicEnvironment
 module UM   = UriManager
 module D    = Deannotate
+module PER  = ProofEngineReduction
+module Ut   = CicUtil
+
+(* raw cic prettyprinter ****************************************************)
+
+let xiter out so ss sc map l =
+   let rec aux = function
+      | hd :: tl when tl <> [] -> map hd; out ss; aux tl
+      | hd :: tl               -> map hd; aux tl
+      | []                     -> ()
+   in
+   out so; aux l; out sc
+
+let abst s w = Some (s, C.Decl w)
+
+let abbr s v w = Some (s, C.Def (v, w))
+
+let pp_sort out = function
+   | C.Type _  -> out "*Type"
+   | C.Prop    -> out "*Prop"
+   | C.CProp _ -> out "*CProp"
+   | C.Set     -> out "*Set"
+
+let pp_name out = function
+   | C.Name s    -> out s
+   | C.Anonymous -> out "_"
+
+let pp_rel out c i =
+   try match List.nth c (pred i) with
+      | None           -> out (Printf.sprintf "%u[?]" i)
+      | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
+   with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))
+
+let pp_implict out = function
+   | None         -> out "?"
+   | Some `Closed -> out "?[Closed]" 
+   | Some `Type   -> out "?[Type]"
+   | Some `Hole   -> out "?[Hole]"
+
+let pp_uri out a =
+   out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
+
+let rec pp_term out e c = function
+   | C.Sort h                      -> pp_sort out h
+   | C.Rel i                       -> pp_rel out c i
+   | C.Implicit x                  -> pp_implict out x
+   | C.Meta (i, iss)               ->
+      let map = function None   -> out "_" | Some v -> pp_term out e c v in
+      out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
+   | C.Var (a, xss)              ->
+      pp_uri out a; pp_xss out e c xss
+   | C.Const (a, xss)              ->
+      pp_uri out a; pp_xss out e c xss
+   | C.MutInd (a, m, xss)          ->
+      pp_uri out a; out (Printf.sprintf "/%u" m);
+      pp_xss out e c xss
+   | C.MutConstruct (a, m, n, xss) ->
+      pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
+      pp_xss out e c xss
+   | C.Cast (v, w)                 ->
+      out "type "; pp_term out e c w; out " contains "; pp_term out e c v
+   | C.Appl vs                     ->
+      xiter out "(" " @ " ")" (pp_term out e c) vs
+   | C.MutCase (a, m, w, v, vs)    ->
+      out "match "; pp_term out e c v;
+      out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
+      out " to "; pp_term out e c w;
+      xiter out " cases " " | " "" (pp_term out e c) vs
+   | C.Prod (s, w, t)             ->
+      out "forall "; pp_name out s; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abst s w :: c) t
+   | C.Lambda (s, w, t)            ->
+      out "fun "; pp_name out s; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abst s w :: c) t
+   | C.LetIn (s, v, w, t)          ->
+      out "let "; pp_name out s; 
+      out " def "; pp_term out e c v; out " of "; pp_term out e c w;
+      out " in "; pp_term out e (abbr s v w :: c) t
+   | C.Fix (i, fs)                 ->
+      let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
+      let c' = List.fold_left map c fs in
+      let map (s, i, w, v) =
+         out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v; 
+	 out " of "; pp_term out e c w;
+      in
+      xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
+   | C.CoFix (i, fs)                 ->
+      let map c (s, w, v) = abbr (C.Name s) v w :: c in
+      let c' = List.fold_left map c fs in
+      let map (s, w, v) =
+         out s; pp_term out e c' v; 
+	 out " of "; pp_term out e c w;
+      in
+      xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)
+
+and pp_xss out e c xss = 
+   let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
+   xiter out "[" "; " "]" map xss 
 
 (* fresh name generator *****************************************************)
 
@@ -65,6 +163,19 @@ let mk_fresh_name context = function
 
 (* 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,19 +192,25 @@ 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.oblivion_ugraph in t
+   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
    with e -> 
       Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
       Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
       Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
       raise e
 
-let get_type c t =
-   try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_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   : "; 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
@@ -101,7 +218,7 @@ let get_tail c t =
       | _               -> assert false
 
 let is_proof c t =
-   match get_tail c (get_type c (get_type c t)) with
+   match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" c t)) with
       | C.Sort C.Prop -> true
       | C.Sort _      -> false
       | _             -> assert false 
@@ -124,18 +241,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.oblivion_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 +271,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,6 +286,30 @@ let get_ind_parameters c t =
 
 let cic = D.deannotate_term
 
+let occurs c ~what ~where =
+   let result = ref false in
+   let equality c t1 t2 =
+      let r = Ut.alpha_equivalence 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