iremoved call to auto

[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.ml

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 49d6da8904c8d033ea08a38c20d11c4aa8680ff4..52b841952a2158e47784108e62ea5f740ece3ca0 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -33,6 +33,8 @@ let hashtbl_size = 11
 let not_implemented =
    "discharge of current proofs is not implemented yet"
 
+let debug = ref false
+
 (* helper functions *********************************************************)
 
 let list_pos found l =
@@ -70,6 +72,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 +110,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')
@@ -184,43 +187,43 @@ 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)
+      let w'' = sh w 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)
+      let w'', v'' = sh w w', sh v v' 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
       let w'' = close true st (sh w w') in
-      C.Constant (b, None, w'', [], attrs)
+      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
       let w'', v'' = close true st (sh w w'), close false st (sh v v') in
-      C.Constant (b, Some v'', w'', [], attrs)
+      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 +231,23 @@ 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 obj, _ = E.get_obj Un.default_ugraph uri in
-   let obj' = discharge_object du obj in
+   if !debug then prerr_endline ("Plain     : " ^ CicPp.ppobj obj); 
+   let obj' = discharge_object dn du obj in
+   if !debug then prerr_endline ("Discharged: " ^ CicPp.ppobj 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}