* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 18/02/2003 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 18/02/2003 *)
+(* *)
+(* *)
+(*****************************************************************************)
module MQI = MQueryInterpreter
module MQIC = MQIConn
match mqi_handle.MQIConn.pgc with
MQIConn.MySQL_C conn -> conn
| _ -> assert false in
- let result = Match_concl.cmatch conn ty in
- (* Stampa il risultato della query
- List.iter
- (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;
- *)
- let uris =
- List.map
- (fun (n,u) ->
- (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
- result in
+ let uris = Match_concl.cmatch conn ty in
+ (* List.iter
+ (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
(* delete all .var uris *)
let isvar (_,s) =
let len = String.length s in
(* concl_cost are the costants in the conclusion of the proof
while hyp_const are the constants in the hypothesis *)
let (main_concl,concl_const) = NewConstraints.mainandcons ty in
- prerr_endline ("Ne sono rimasti 1 " ^ string_of_int (List.length uris));
+ prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris));
let hyp t set =
match t with
Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
in
prerr_endline "HO FILTRATO2";
*)
+ let uris =
+ List.map
+ (fun (n,u) ->
+ (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
+ uris in
let uris' =
let rec filter_out =
function
let tl' = filter_out tl in
try
prerr_endline ("STO APPLICANDO " ^ uri);
- (m,
+ let res = (m,
(ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac
~term:(MQueryMisc.term_of_cic_textual_parser_uri
(MQueryMisc.cic_textual_parser_uri_of_string uri)))
- status))::tl'
+ status))::tl' in
+ prerr_endline ("OK");res
(* with ProofEngineTypes.Fail _ -> tl' *)
(* patch to cover CSC's exportation bug *)
- with _ -> tl'
+ with _ -> prerr_endline ("FAIL");tl'
in
prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris));
filter_out uris
(*
prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
*)
- let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+ let ty_sort1,u = (*TASSI: FIXME *)
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
(*
prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
*)
- let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+ let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
(*
prerr_endline "DOPO LA SECONDA TYPE OF " ;
*)
- let prop1 = if CicReduction.are_convertible
- ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
- else 1 in
- let prop2 = if CicReduction.are_convertible
- ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
- else 1 in
- prop1 - prop2 in
- List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res
+ let b,u2 =
+ CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
+ let prop1 = if b then 0 else 1 in
+ let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
+ let prop2 = if b then 0 else 1 in
+ prop1 - prop2 in
+ List.map (
+ fun (level,(proof,goallist)) ->
+ (proof, (List.stable_sort (order_goal_list proof) goallist))
+ ) res
;;