(******************************************************************************)
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
- let index_sharp = String.index uri '#' in
- let index_rest = index_sharp + 10 in
- let baseuri = String.sub uri 0 index_sharp in
- let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
- baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
(* GLOBAL CONSTANTS *)
let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
(* MISC FUNCTIONS *)
-exception IllFormedUri of string;;
-
-let cic_textual_parser_uri_of_string uri' =
- try
- (* Constant *)
- if String.sub uri' (String.length uri' - 4) 4 = ".con" then
- CicTextualParser0.ConUri (UriManager.uri_of_string uri')
- else
- if String.sub uri' (String.length uri' - 4) 4 = ".var" then
- CicTextualParser0.VarUri (UriManager.uri_of_string uri')
- else
- (try
- (* Inductive Type *)
- let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
- CicTextualParser0.IndTyUri (uri'',typeno)
- with
- _ ->
- (* Constructor of an Inductive Type *)
- let uri'',typeno,consno =
- CicTextualLexer.indconuri_of_uri uri'
- in
- CicTextualParser0.IndConUri (uri'',typeno,consno)
- )
- with
- _ -> raise (IllFormedUri uri')
-;;
-
let term_of_cic_textual_parser_uri uri =
let module C = Cic in
let module CTP = CicTextualParser0 in
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
- term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
+ term_of_cic_textual_parser_uri
+ (Disambiguate.cic_textual_parser_uri_of_string uri)
in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
exception NoChoice;;
let
- interactive_user_uri_choice ~selection_mode ?(ok="Ok")
+ interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
?(enable_button_for_non_vars=false) ~title ~msg uris
=
let choices = ref [] in
let expected_height = 18 * List.length uris in
let height = if expected_height > 400 then 400 else expected_height in
GList.clist ~columns:1 ~packing:scrolled_window#add
- ~height ~selection_mode () in
+ ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
let _ = List.map (function x -> clist#append [x]) uris in
let hbox2 =
GPack.hbox ~border_width:0
let n' = Str.search_forward regexpr inputtext n in
let id = Str.matched_group 2 inputtext in
let uri =
- cic_textual_parser_uri_of_string
+ Disambiguate.cic_textual_parser_uri_of_string
("cic:" ^ (Str.matched_group 5 inputtext))
in
let dom,resolve_id = aux (n' + 1) in
let result = MQueryGenerator.locate id in
let uris =
List.map
- (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ (function uri,_ ->
+ Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
let html =
(" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
| Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
;;
-let locate_one_id id =
- let result = MQueryGenerator.locate id in
- let uris =
- List.map
- (function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
- output_html (rendering_window ())#outputhtml html ;
- let uris' =
- match uris with
- [] ->
- [UriManager.string_of_uri
- (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
- | [uri] -> [uri]
- | _ ->
- interactive_user_uri_choice
- ~selection_mode:`EXTENDED
- ~ok:"Try every selection."
- ~enable_button_for_non_vars:true
- ~title:"Ambiguous input."
- ~msg:
- ("Ambiguous input \"" ^ id ^
- "\". Please, choose one or more interpretations:")
- uris
- in
- List.map cic_textual_parser_uri_of_string uris'
-;;
-
-
-exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
exception AmbiguousInput;;
-type test_result =
- Ok of Cic.term * Cic.metasenv
- | Ko
- | Uncertain
-
-let disambiguate_input context metasenv dom mk_metasenv_and_expr =
- let known_ids,resolve_id = !id_to_uris in
- let dom' =
- let rec filter =
- function
- [] -> []
- | he::tl ->
- if List.mem he known_ids then filter tl else he::(filter tl)
- in
- filter dom
- in
- (* for each id in dom' we get the list of uris associated to it *)
- let list_of_uris = List.map locate_one_id dom' in
- let tests_no =
- List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
- in
- if tests_no > 1 then
- output_html (outputhtml ())
- ("<h1>Disambiguation phase started: " ^
- string_of_int tests_no ^ " cases will be tried.") ;
- (* and now we compute the list of all possible assignments from *)
- (* id to uris that generate well-typed terms *)
- let resolve_ids =
- (* function to test if a partial interpretation is so far correct *)
- let test resolve_id residual_dom =
- (* We put implicits in place of every identifier that is not *)
- (* resolved by resolve_id *)
- let resolve_id'' =
- let resolve_id' =
- function id ->
- match resolve_id id with
- None -> None
- | Some uri -> Some (CicTextualParser0.Uri uri)
- in
- List.fold_left
- (fun f id ->
- function id' ->
- if id = id' then Some (CicTextualParser0.Implicit) else f id'
- ) resolve_id' residual_dom
- in
- (* and we try to refine the term *)
- let saved_status = !CicTextualParser0.metasenv in
- let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
-(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
- (* The parser is imperative ==> we must restore the old status ;-(( *)
- CicTextualParser0.metasenv := saved_status ;
- try
- let term,_,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
- in
- Ok (term,metasenv'')
- with
- CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
- (try
- let term = CicTypeChecker.type_of_aux' metasenv' context expr in
- Ok (term,metasenv')
- with _ -> Ko
- )
- | CicRefine.Uncertain _ ->
-prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
- Uncertain
- | _ ->
-prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
- Ko
- in
- let rec aux resolve_id ids list_of_uris =
- match ids,list_of_uris with
- [],[] ->
- (match test resolve_id [] with
- Ok (term,metasenv) -> [resolve_id,term,metasenv]
- | Ko | Uncertain -> [])
- | id::idtl,uris::uristl ->
- let rec filter =
- function
- [] -> []
- | uri::uritl ->
- let resolve_id' =
- function id' -> if id = id' then Some uri else resolve_id id'
- in
- (match test resolve_id' idtl with
- Ok (term,metasenv) ->
- (* the next three ``if''s are used to avoid the base *)
- (* case where the term would be refined a second time. *)
- (if uristl = [] then
- [resolve_id',term,metasenv]
- else
- (aux resolve_id' idtl uristl)
- ) @ (filter uritl)
- | Uncertain ->
- (if uristl = [] then []
- else
- (aux resolve_id' idtl uristl)
- ) @ (filter uritl)
- | Ko ->
- filter uritl
- )
- in
- filter uris
- | _,_ -> assert false
- in
- aux resolve_id dom' list_of_uris
- in
- List.iter
- (function (resolve,term,newmetasenv) ->
- (* If metasen <> newmetasenv is a normal condition, we should *)
- (* be prepared to apply the returned substitution to the *)
- (* whole current proof. *)
- if metasenv <> newmetasenv then
- begin
- prerr_endline
- ("+++++ ASSERTION FAILED: " ^
- "a refine operation should not modify the metasenv") ;
- (* an assert would raise an exception that could be caught *)
- exit 1
- end
- ) resolve_ids ;
- let resolve_id',term,metasenv' =
- match resolve_ids with
- [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
- | [resolve_id] -> resolve_id
- | _ ->
- let choices =
- List.map
- (function (resolve,_,_) ->
- List.map
- (function id ->
- id,
- match resolve id with
- None -> assert false
- | Some uri ->
- match uri with
- CicTextualParser0.ConUri uri
- | CicTextualParser0.VarUri uri ->
- UriManager.string_of_uri uri
- | CicTextualParser0.IndTyUri (uri,tyno) ->
- UriManager.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (tyno+1) ^ ")"
- | CicTextualParser0.IndConUri (uri,tyno,consno) ->
- UriManager.string_of_uri uri ^ "#xpointer(1/" ^
- string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
- ) dom
- ) resolve_ids
- in
- let index = interactive_interpretation_choice choices in
- List.nth resolve_ids index
- in
- id_to_uris := known_ids @ dom', resolve_id' ;
- metasenv',term
+(* A WIDGET TO ENTER CIC TERMS *)
+
+module Callbacks =
+ struct
+ let output_html msg = output_html (outputhtml ()) msg;;
+ let interactive_user_uri_choice =
+ fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
+ interactive_user_uri_choice ~selection_mode ?ok
+ ?enable_button_for_non_vars ~title ~msg;;
+ let interactive_interpretation_choice = interactive_interpretation_choice;;
+ let input_or_locate_uri = input_or_locate_uri;;
+ end
;;
-(* A WIDGET TO ENTER CIC TERMS *)
+module Disambiguate' = Disambiguate.Make(Callbacks);;
class term_editor ?packing ?width ?height ?isnotempty_callback () =
let input = GEdit.text ~editable:true ?width ?height ?packing () in
CicTextualParserContext.main
~context:name_context ~metasenv CicTextualLexer.token lexbuf
in
- disambiguate_input context metasenv dom mk_metasenv_and_expr
+ let id_to_uris',metasenv,expr =
+ Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
+ ~id_to_uris:!id_to_uris
+ in
+ id_to_uris := id_to_uris' ;
+ metasenv,expr
end
;;
(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)
+ Disambiguate.cic_textual_parser_uri_of_string
+ (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
+ uristr)
with
CicTextualParser0.ConUri uri
| CicTextualParser0.VarUri uri
let uris =
List.map
(function uri,_ ->
- wrong_xpointer_format_from_wrong_xpointer_format' uri
+ Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
) result in
let html =
" <h1>Backward Query: </h1>" ^
if
ProofEngine.can_apply
(term_of_cic_textual_parser_uri
- (cic_textual_parser_uri_of_string uri))
+ (Disambiguate.cic_textual_parser_uri_of_string uri))
then
uri::tl',exc
else
projects / helm.git / blobdiff