X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.ml;h=b2f73f311a9d932374fb4694432c6be0a2469469;hb=70660e05baa914569c52555230901d5a8dd92f0b;hp=91f7016cd83de6f5baaa916d72efb3fc7769fb94;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml
index 91f7016cd..b2f73f311 100644
--- a/helm/software/components/acic_procedural/proceduralHelpers.ml
+++ b/helm/software/components/acic_procedural/proceduralHelpers.ml
@@ -34,102 +34,7 @@ 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 
+module DTI  = DoubleTypeInference
 
 (* fresh name generator *****************************************************)
 
@@ -157,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 -> 
@@ -179,18 +99,24 @@ 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.default_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 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_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
@@ -204,12 +130,15 @@ let get_tail c t =
       | (_, hd) :: _, _ -> hd
       | _               -> assert false
 
-let is_proof c t =
-   match get_tail c (get_type "is_proof 1" c (get_type "is_proof 2" 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 
@@ -319,17 +248,20 @@ let cic_bc c t =
    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 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)
@@ -361,17 +293,20 @@ let acic_bc c t =
    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 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)
@@ -400,3 +335,10 @@ 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)