cicDischarge: we still have some problems here. Some fixes

cicTypeChecker: added some debug prints (commented for now)
applyTransformation.ml: improved error detection

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 49d6da8904c8d033ea08a38c20d11c4aa8680ff4..f8ad074fb67081198cabf45c38d00d67c27b8e3a 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -70,6 +70,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 +108,11 @@ 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)                 ->
+(* FG: We do not discharge the nsubst here ?? *)   
       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)
+      (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *)
    | 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 +186,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 +230,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
+   prerr_endline ("Plain     : " ^ CicPp.ppobj obj); 
+   let obj' = discharge_object dn du obj in
+   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} 

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.mli b/helm/software/components/cic_proof_checking/cicDischarge.mli
index 447e2a344e6f6bee851f365b92efb1d26d71d27a..a6b097db2af01c22018662956dc5f5b56da6ae58 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.mli
+++ b/helm/software/components/cic_proof_checking/cicDischarge.mli
@@ -23,12 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(* discharges the explicit variables of the given object (with sharing)    *)
-(* the first argument is a map for relocating the uris of the dependencdes *)
+(* discharges the explicit variables of the given object (with sharing)     *)
+(* the first argument is a map for relacating the names of the objects      *)
+(* the second argument is a map for relocating the uris of the dependencdes *)
 val discharge_object:
-   (UriManager.uri -> UriManager.uri) -> Cic.obj -> Cic.obj
+   (string -> string) -> (UriManager.uri -> UriManager.uri) -> 
+   Cic.obj -> Cic.obj
 
 (* applies the previous function to the object at the given uri *)
 (* returns true if the object does not need discharging         *)
 val discharge_uri:
-   (UriManager.uri -> UriManager.uri) -> UriManager.uri -> Cic.obj * bool
+   (string -> string) -> (UriManager.uri -> UriManager.uri) ->
+   UriManager.uri -> Cic.obj * bool

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 00e40dfa6b237a63ac3a047f2c3dcbde3acd988f..30a886a2b47ad81acf62681117c04ce22e35b1c6 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1350,6 +1350,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
+(* FG: DEBUG ONLY   
+   prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
+   prerr_endline ("TC: term   :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
+*)   
    match t with
       C.Rel n ->
        (try

diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml
index 58fc1920813ae09291d52d7e4285ec0eb5b2552f..ca73e2baac10b2738622247327fec249fd903517 100644 (file)
--- a/helm/software/matita/applyTransformation.ml
+++ b/helm/software/matita/applyTransformation.ml
@@ -240,6 +240,8 @@ let discharge_uri style uri =
    let _, s = List.fold_left replacement (false, s) replacements in 
    UM.uri_of_string s
 
+let discharge_name s = s ^ "_discharged"
+
 let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    let print_exc = function
       | ProofEngineHelpers.Bad_pattern s as e ->
@@ -248,24 +250,34 @@ let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
    in
    let dbd = LibraryDb.instance () in   
    let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
+   let error uri e =
+      let msg  = 
+         Printf.sprintf 
+            "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
+            (UM.string_of_uri uri) e
+      in
+      Printf.eprintf "%s\n" msg;
+      GrafiteTypes.command_error msg
+   in
    let map uri =
       try
 (* FG: for now the explicit variables must be discharged *)
         let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
-        let obj, real = Ds.discharge_uri (discharge_uri style) uri in
+        let obj, real = 
+          Ds.discharge_uri discharge_name (discharge_uri style) uri
+       in
        if real then do_it obj else
        let newuri = discharge_uri style uri in
        let _lemmas = LS.add_obj GE.refinement_toolkit newuri obj in
        do_it obj
       with
-         | e -> 
-            let msg = 
-              Printf.sprintf 
-                 "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s" 
-                  (UM.string_of_uri uri) (print_exc e)
-           in
-           Printf.eprintf "%s\n" msg;
-           GrafiteTypes.command_error msg
+         | TC.TypeCheckerFailure s ->
+           error uri ("failure  : " ^ Lazy.force s)
+         | TC.AssertFailure s      ->
+           error uri ("assert   : " ^ Lazy.force s)
+         | E.Object_not_found u    ->
+           error uri ("not found: " ^ UM.string_of_uri u)
+        | e                       -> error uri (print_exc e)
    in
    String.concat "" (List.map map sorted_uris)