X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicDischarge.ml;h=066eb72c9a3a948297a127b092efb2fc46bb493a;hb=3323758b99384afb5c7a70aa31bc006a78af64dd;hp=49d6da8904c8d033ea08a38c20d11c4aa8680ff4;hpb=04f22df647f35080b499b720bca7bc0eb1794c64;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 49d6da890..066eb72c9 100644
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -27,14 +27,26 @@ module UM = UriManager
 module C  = Cic
 module Un = CicUniv
 module E  = CicEnvironment
+module Ut = CicUtil
+module TC = CicTypeChecker
 
 let hashtbl_size = 11
 
 let not_implemented =
    "discharge of current proofs is not implemented yet"
 
+let debug = ref false
+
+let out = prerr_string
+
 (* helper functions *********************************************************)
 
+let typecheck t =
+   if !debug then begin
+      let _ = TC.type_of_aux' [] [] t Un.default_ugraph in
+      out "Typecheck : OK\n"
+   end
+
 let list_pos found l =
    let rec aux n = function
       | []       -> raise Not_found
@@ -70,6 +82,7 @@ let mk_arg s u =
 (* main functions ***********************************************************)
 
 type status = {
+   dn: string -> string;                (* name discharge map              *)
    du: UM.uri -> UM.uri;                (* uri discharge map               *)
    c : C.context;                       (* var context of this object      *)
    ls: (UM.uri, UM.uri list) Hashtbl.t; (* var lists of subobjects         *)
@@ -107,10 +120,10 @@ let rec discharge_term st t = match t with
       let s = List.map (mk_arg s) args in
       C.Appl (C.MutConstruct (st.du u, m, n, []) :: discharge_nsubst st s)
    | C.Var (u, s)                 ->
-      let args = get_args st u in
-      if args = [] then C.Rel (discharge st u) else
-      let s = List.map (mk_arg s) args in
-      C.Appl (C.Rel (discharge st u) :: discharge_nsubst st s)
+(* We do not discharge the nsubst because variables are not closed *)
+(* thus only the identity nsubst should be allowed                 *)
+      if s <> [] then assert false else
+      C.Rel (discharge st u)
    | C.Meta (i, s)                ->
       let s' = list_map_sh (discharge_usubst st) s in
       if s' == s then t else C.Meta (i, s')
@@ -119,28 +132,30 @@ let rec discharge_term st t = match t with
       if vs' == vs then t else C.Appl (flatten vs')
    | C.Cast (v, w)                ->
       let v', w' = discharge_term st v, discharge_term st w in
-      if v' = v && w' = w then t else
+      if v' == v && w' == w then t else
       C.Cast (sh v v', sh w w')
    | C.MutCase (u, m, w, v, vs)   ->
+      let args = get_args st u in
+      let u' = if args = [] then u else st.du u in
       let w', v', vs' = 
          discharge_term st w, discharge_term st v,
 	 list_map_sh (discharge_term st) vs
       in
-      if w' = w && v' = v && vs' == vs then t else
-      C.MutCase (st.du u, m, sh w w', sh v v', sh vs vs')
+      if UM.eq u u' && w' == w && v' == v && vs' == vs then t else
+      C.MutCase (u', m, sh w w', sh v v', sh vs vs')
    | C.Prod (b, w, v)             ->
       let w', v' = discharge_term st w, discharge_term (add st 1) v in
-      if w' = w && v' = v then t else
+      if w' == w && v' == v then t else
       C.Prod (b, sh w w', sh v v')
    | C.Lambda (b, w, v)           ->
       let w', v' = discharge_term st w, discharge_term (add st 1) v in
-      if w' = w && v' = v then t else
+      if w' == w && v' == v then t else
       C.Lambda (b, sh w w', sh v v')
    | C.LetIn (b, y, w, v)   ->
       let y', w', v' = 
          discharge_term st y, discharge_term st w, discharge_term (add st 1) v
       in
-      if y' = y && w' = w && v' == v then t else
+      if y' == y && w' == w && v' == v then t else
       C.LetIn (b, sh y y', sh w w', sh v v')
    | C.CoFix (i, s)         ->
       let no = List.length s in
@@ -163,13 +178,13 @@ and discharge_usubst st s = match s with
 and discharge_cofun st no f =
    let b, w, v = f in
    let w', v' = discharge_term st w, discharge_term (add st no) v in
-   if w' = w && v' = v then f else
+   if w' == w && v' == v then f else
    b, sh w w', sh v v'
 
 and discharge_fun st no f =
    let b, i, w, v = f in
    let w', v' = discharge_term st w, discharge_term (add st no) v in
-   if w' = w && v' = v then f else
+   if w' == w && v' == v then f else
    b, i, sh w w', sh v v'
 
 let close is_type st t = 
@@ -184,43 +199,47 @@ let close is_type st t =
 let discharge_con st con =
    let b, v = con in
    let v' = discharge_term st v in
-   if v' == v && st.rl = [] then con else b, close true st (sh v v')
+   if v' == v && st.rl = [] then con else st.dn b, close true st (sh v v')
 
 let discharge_type st ind_type =
    let b, ind, w, cons = ind_type in
    let w', cons' = discharge_term st w, list_map_sh (discharge_con st) cons in
    if w' == w && cons' == cons && st.rl = [] then ind_type else
    let w'' = close true st (sh w w') in
-   b, ind, w'', sh cons cons'
+   st.dn b, ind, w'', sh cons cons'
 
-let rec discharge_object du obj = 
+let rec discharge_object dn du obj = 
    let ls = Hashtbl.create hashtbl_size in match obj with
    | C.Variable (b, None, w, vars, attrs)              ->
-      let st = init_status du ls vars in
+      let st = init_status dn du ls vars in
       let w' = discharge_term st w in
-      if w' = w && vars = [] then obj else
-      let w'' = close true st (sh w w') in
-      C.Variable (b, None, w'', [], attrs)
+      if w' == w && vars = [] then obj else
+      let w'' = sh w w' in
+      let _ = typecheck w'' in
+      C.Variable (dn b, None, w'', [], attrs)
    | C.Variable (b, Some v, w, vars, attrs)            ->
-      let st = init_status du ls vars in
+      let st = init_status dn du ls vars in
       let w', v' = discharge_term st w, discharge_term st v in
-      if w' = w && v' = v && vars = [] then obj else
-      let w'', v'' = close true st (sh w w'), close false st (sh v v') in
-      C.Variable (b, Some v'', w'', [], attrs)
+      if w' == w && v' == v && vars = [] then obj else
+      let w'', v'' = sh w w', sh v v' in
+      let _ = typecheck (C.Cast (v'', w'')) in
+      C.Variable (dn b, Some v'', w'', [], attrs)
    | C.Constant (b, None, w, vars, attrs)              ->
-      let st = init_status du ls vars in
+      let st = init_status dn du ls vars in
       let w' = discharge_term st w in
-      if w' = w && vars = [] then obj else
+      if w' == w && vars = [] then obj else
       let w'' = close true st (sh w w') in
-      C.Constant (b, None, w'', [], attrs)
+      let _ = typecheck w'' in
+      C.Constant (dn b, None, w'', [], attrs)
    | C.Constant (b, Some v, w, vars, attrs)            ->
-      let st = init_status du ls vars in
+      let st = init_status dn du ls vars in
       let w', v' = discharge_term st w, discharge_term st v in
-      if w' = w && v' = v && vars = [] then obj else
+      if w' == w && v' == v && vars = [] then obj else
       let w'', v'' = close true st (sh w w'), close false st (sh v v') in
-      C.Constant (b, Some v'', w'', [], attrs)
+      let _ = typecheck (C.Cast (v'', w'')) in
+      C.Constant (dn b, Some v'', w'', [], attrs)
    | C.InductiveDefinition (types, vars, lpsno, attrs) ->
-      let st = init_status du ls vars in
+      let st = init_status dn du ls vars in
       let types' = list_map_sh (discharge_type st) types in
       if types' == types && vars = [] then obj else
       let lpsno' = lpsno + List.length vars in
@@ -228,20 +247,28 @@ let rec discharge_object du obj =
    | C.CurrentProof _                                  ->
       HLog.warn not_implemented; obj
 
-and discharge_uri du uri =
+and discharge_uri dn du uri =
+   let prerr msg obj =
+      if !debug then begin
+         out msg; Ut.pp_obj out obj; out "\n"
+      end
+   in
    let obj, _ = E.get_obj Un.default_ugraph uri in
-   let obj' = discharge_object du obj in
+   prerr "Plain     : " obj;
+   let obj' = discharge_object dn du obj in
+   prerr "Discharged: " obj';
    obj', obj' == obj
 
-and discharge_vars du vars =
+and discharge_vars dn du vars =
+(* We should check that the dependences are ordered telesopically *)   
    let map u =
-      match discharge_uri du u with
+      match discharge_uri dn du u with
          | C.Variable (b, None, w, _, _), _   -> Some (C.Name b, C.Decl w)
          | C.Variable (b, Some v, w, _, _), _ -> Some (C.Name b, C.Def (v, w))
 	 | _                                  -> None
    in
    List.rev_map map vars
 
-and init_status du ls vars =
-   let c, rl = discharge_vars du vars, List.rev vars in
-   {du = du; c = c; ls = ls; rl = rl; h = 1} 
+and init_status dn du ls vars =
+   let c, rl = discharge_vars dn du vars, List.rev vars in
+   {dn = dn; du = du; c = c; ls = ls; rl = rl; h = 1}