parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic / cicUtil.ml

diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml
index 48481440929dacc40a88f68bb740a712e30884d8..9b6ece214f4d1d251c28f85b25e82c3613c058fb 100644 (file)
--- a/helm/software/components/cic/cicUtil.ml
+++ b/helm/software/components/cic/cicUtil.ml
@@ -216,16 +216,6 @@ let attributes_of_obj = function
 
 let is_generated obj = List.exists ((=) `Generated) (attributes_of_obj obj)
 
-let arity_of_composed_coercion obj =
-  let attrs = attributes_of_obj obj in
-  try
-    let tag=List.find (function `Class (`Coercion _) -> true|_->false) attrs in
-    match tag with
-    |  `Class (`Coercion n) -> n
-    | _-> assert false 
-  with Not_found -> 0
-;;
-
 let projections_of_record obj uri =
   let attrs = attributes_of_obj obj in
   try
@@ -560,7 +550,8 @@ let alpha_equivalence =
 
 let is_sober c t =
    let rec sober_term c g = function
-      | C.Rel _ 
+      | C.Rel i                         ->
+         if i <= 0 then fun b -> false else g
       | C.Sort _  
       | C.Implicit _                    -> g      
       | C.Const (_, xnss) 
@@ -575,7 +566,8 @@ let is_sober c t =
       | C.LetIn (_, v, ty, t)           ->
          sober_term c (sober_term c (sober_term c g t) ty) v
       | C.Appl []                       
-      | C.Appl [_]                      -> fun b -> false
+      | C.Appl [_]                      
+      | C.Appl (C.Appl _ :: _)          -> fun b -> false
       | C.Appl ts                       -> sober_terms c g ts
       | C.MutCase (_, _, t, v, ts)      -> 
          sober_terms c (sober_term c (sober_term c g t) v) ts
@@ -628,13 +620,14 @@ 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))
+   with Failure "nth" -> out (Printf.sprintf "%u[%i]" i (List.length c - i))
 
-let pp_implict out = function
+let pp_implicit out = function
    | None         -> out "?"
    | Some `Closed -> out "?[Closed]" 
    | Some `Type   -> out "?[Type]"
    | Some `Hole   -> out "?[Hole]"
+   | Some `Vector -> out "?[...]"
 
 let pp_uri out a =
    out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 
@@ -642,7 +635,7 @@ let pp_uri out 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.Implicit x                  -> pp_implicit 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
@@ -696,7 +689,10 @@ 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 
 
-and pp_attrs out attrs = 
+let pp_int out i =
+   out (Printf.sprintf "%u" i)
+
+let pp_attrs out attrs = 
    let map = function
       | _ -> ()
    in
@@ -705,19 +701,32 @@ and pp_attrs out attrs =
 let pp_pars out pars = 
    xiter out " (" ", " ")\n" (pp_uri out) pars 
 
+let pp_point out point =
+   if point then out "ind " else out "coind "
+
+let pp_constructor out (s, w) =
+   out s; out " of "; pp_term out [] [] w
+
+let pp_definition out (s, point, w, ts) =
+   out "let "; pp_point out point; out s; out " of "; pp_term out [] [] w;  
+   xiter out "\ndef " "\nor " "" (pp_constructor out) ts
+
 let pp_obj out = function
-   | C.Constant (s, None, u, pars, attrs)          ->
+   | C.Constant (s, None, u, pars, attrs)           ->
       out "fun "; pp_attrs out attrs; out s; pp_pars out pars;
       out " of "; pp_term out [] [] u
-   | C.Constant (s, Some t, u, pars, attrs)        ->
+   | C.Constant (s, Some t, u, pars, attrs)         ->
       out "let "; pp_attrs out attrs; out s; pp_pars out pars;
       out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
-   | C.Variable (s, None, u, pars, attrs)          ->
-      out "Local declaration"
-   | C.Variable (s, Some t, u, pars, attrs)        ->
-      out "Local definition"
-   | C.CurrentProof (s, e, t, u, pars, attrs)      ->
+   | C.Variable (s, None, u, pars, attrs)           ->
+      out "local fun "; pp_attrs out attrs; out s; pp_pars out pars;
+      out " of "; pp_term out [] [] u
+   | C.Variable (s, Some t, u, pars, attrs)         ->
+      out "local let "; pp_attrs out attrs; out s; pp_pars out pars;
+      out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
+   | C.InductiveDefinition (us, pars, lpsno, attrs) ->
+      out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars;
+      xiter out "" "\n" "" (pp_definition out) us
+   | C.CurrentProof (s, e, t, u, pars, attrs)       ->
       out "Current Proof" 
-   | C.InductiveDefinition (us, pars, lpno, attrs) ->
-      out "Inductive Definition"
-   
+