From d2d20cd33c42d0897765387042c3779109bbf4fd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 7 Sep 2008 17:09:19 +0000 Subject: [PATCH] cicDischarge: we still have some problems here. Some fixes cicTypeChecker: added some debug prints (commented for now) applyTransformation.ml: improved error detection --- .../cic_proof_checking/cicDischarge.ml | 49 ++++++++++--------- .../cic_proof_checking/cicDischarge.mli | 11 +++-- .../cic_proof_checking/cicTypeChecker.ml | 4 ++ helm/software/matita/applyTransformation.ml | 30 ++++++++---- 4 files changed, 59 insertions(+), 35 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml index 49d6da890..f8ad074fb 100644 --- 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 447e2a344..a6b097db2 100644 --- 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 00e40dfa6..30a886a2b 100644 --- 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 58fc19208..ca73e2baa 100644 --- 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) -- 2.39.2