X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=890f5d75fd4071f5482c5fd00dfec2e530ef669c;hb=a772e377c1ca7c43c3e1e25eb47479fc3c5ceb9e;hp=afbbc143919ccf8fd96bd68974779eae76a3802b;hpb=d7d05aa09759ebf31f2df81b33051d6b3e463f52;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index afbbc1439..890f5d75f 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -27,7 +27,7 @@ (* *) (* PROJECT HELM *) (* *) -(* Claudio Sacerdoti Coen *) +(* Claudio Sacerdoti Coen *) (* 06/01/2002 *) (* *) (* *) @@ -68,6 +68,11 @@ let prooffile = "/public/sacerdot/currentproof";; let prooffiletype = "/public/sacerdot/currentprooftype";; *) +(* NATILE +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; +*) + (* TASSI let prooffile = "//miohelm/tmp/currentproof";; let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; @@ -88,6 +93,11 @@ let innertypesfile = "/public/sacerdot/innertypes";; let constanttypefile = "/public/sacerdot/constanttype";; *) +(* NATILE +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; +*) + (* TASSI let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; @@ -1130,8 +1140,7 @@ let ("

" ^ Printexc.to_string e ^ "

") ; in let show_in_show_window_uri uri = - CicTypeChecker.typecheck uri ; - let obj = CicEnvironment.get_cooked_obj uri in + let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget (n : Gdome.element) = @@ -2362,6 +2371,145 @@ let open_ () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let show_query_results results = + let window = + GWindow.window + ~modal:false ~title:"Query results." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Click on a URI to show that object" + ~packing:hbox#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in + ignore + (List.map + (function (uri,_) -> + let n = + clist#append [uri] + in + clist#set_row ~selectable:false n + ) results + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + let (uristr,_) = List.nth results row in + match + cic_textual_parser_uri_of_string + (wrong_xpointer_format_from_wrong_xpointer_format' uristr) + with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri + | CicTextualParser0.IndTyUri (uri,_) + | CicTextualParser0.IndConUri (uri,_,_) -> + show_in_show_window_uri uri + ) + ) ; + window#show () +;; + +let + refine_constraints (must_obj,must_rel,must_sort) (only_obj,only_rel,only_sort) += + let chosen = ref false in + let use_only = ref false in + let window = + GWindow.window + ~modal:true ~title:"Constraints refinement." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "\"Only\" constraints can be enforced or not." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let onlyb = + GButton.toggle_button ~label:"Enforce \"only\" constraints" + ~active:false ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) + () + in + ignore + (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Rels." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* Rel constraints *) + let expected_height = 25 * (List.length must_rel + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let rel_constraints = + List.map + (function (position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:position + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:(string_of_int depth') + ~active:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) + () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref + ) must_rel in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + if !chosen then + let chosen_must_rel = + List.map +(* + (function (position,ref_depth) -> position,!ref_depth) rel_constraints +*) +(function (position,ref_depth) -> prerr_endline ("### " ^ position ^ " " ^ match !ref_depth with None -> "NULL" | Some d -> string_of_int d) ; position,!ref_depth) rel_constraints + in + (must_obj,chosen_must_rel,must_sort), + (if !use_only then +(*CSC: ???????????????????????? I assume that must and only are the same... *) + only_obj,Some chosen_must_rel,only_sort + else + None,None,None + ) + else + raise NoChoice +;; let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in @@ -2369,35 +2517,145 @@ let completeSearchPattern () = try let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in - ignore (MQueryLevels2.get_constraints expr) + let must,only = MQueryLevels2.get_constraints expr in + let must',only' = refine_constraints must only in + let results = MQueryGenerator.searchPattern must' only' in + show_query_results results with e -> output_html outputhtml ("

" ^ Printexc.to_string e ^ "

") ; ;; +let choose_must list_of_must only = + let chosen = ref None in + let user_constraints = ref [] in + let window = + GWindow.window + ~modal:true ~title:"Query refinement." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + ("You can now specify the genericity of the query. " ^ + "The more generic the slower.") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + "Suggestion: start with faster queries before moving to more generic ones." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + let page = ref 0 in + let last = List.length list_of_must in + List.map + (function must -> + incr page ; + let label = + GMisc.label ~text: + (if !page = 1 then "More generic" else + if !page = last then "More precise" else " ") () in + let expected_height = 25 * (List.length must + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (uri,position) -> + let n = + clist#append + [uri; if position then "MainConclusion" else "Conclusion"] + in + clist#set_row ~selectable:false n + ) must + ) ; + clist#columns_autosize () + ) list_of_must in + let _ = + let label = GMisc.label ~text:"User provided" () in + let vbox = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Select the constraints that must be satisfied and press OK." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length only + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~selection_mode:`EXTENDED + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (uri,position) -> + let n = + clist#append + [uri; if position then "MainConclusion" else "Conclusion"] + in + clist#set_row ~selectable:true n + ) only + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + user_constraints := (List.nth only row)::!user_constraints)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + user_constraints := + List.filter + (function uri -> uri != (List.nth only row)) !user_constraints)) ; + in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + match !chosen with + None -> raise NoChoice + | Some n -> + if n = List.length list_of_must then + (* user provided constraints *) + !user_constraints + else + List.nth list_of_must n +;; + let searchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - let rec get_level ?(last_invalid=false) () = - match - GToolbox.input_string - ~title:"Insert the strictness parameter for the query:" - ((if last_invalid then - "Invalid input (must be a non-negative natural number). Insert again " - else - "Insert " - ) ^ "the strictness parameter for the query:") - with - None -> raise NoChoice - | Some n -> - try - int_of_string n - with - _ -> get_level ~last_invalid:true () - in - let level = get_level () in let metasenv = match !ProofEngine.proof with None -> assert false @@ -2407,10 +2665,22 @@ let searchPattern () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in - let len = List.length list_of_must in - let must = if level < len then List.nth list_of_must level else can in - let result = MQueryGenerator.searchPattern metasenv ey ty must can in + let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in + let must = choose_must list_of_must only in + let torigth_restriction (u,b) = + let p = + if b then + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else + "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u,p,None) + in + let rigth_must = List.map torigth_restriction must in + let rigth_only = Some (List.map torigth_restriction only) in + let result = + MQueryGenerator.searchPattern + (rigth_must,[],[]) (rigth_only,None,None) in let uris = List.map (function uri,_ -> @@ -2418,9 +2688,6 @@ let searchPattern () = ) result in let html = "

Backward Query:

" ^ - "

Levels:

" ^ - MQueryLevels.string_of_levels - (MQueryLevels.levels_of_term metasenv ey ty) "
" ^ " 
" ^ get_last_query result ^ "
" in output_html outputhtml html ;