From 3fcde61beded58d18775c13906b9741ba4735864 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 22 Dec 2002 19:06:27 +0000 Subject: [PATCH] New: refinement is now used to disambiguate parsing. --- helm/gTopLevel/.depend | 4 +- helm/gTopLevel/gTopLevel.ml | 289 ++++++++++++++++++------------------ 2 files changed, 143 insertions(+), 150 deletions(-) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 03c071b5c..58de61eda 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -22,9 +22,9 @@ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi primitiveTactics.cmi: proofEngineTypes.cmo -variousTactics.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \ +variousTactics.cmo: primitiveTactics.cmi proofEngineReduction.cmi \ proofEngineTypes.cmo tacticals.cmi variousTactics.cmi -variousTactics.cmx: primitiveTactics.cmx proofEngineHelpers.cmx \ +variousTactics.cmx: primitiveTactics.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx tacticals.cmx variousTactics.cmi variousTactics.cmi: proofEngineTypes.cmo introductionTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo \ diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index eac6fad1b..f81dffc85 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -170,33 +170,6 @@ let argspec = in Arg.parse argspec ignore "" -(* A WIDGET TO ENTER CIC TERMS *) - -class term_editor ?packing ?width ?height ?isnotempty_callback () = - let input = GEdit.text ~editable:true ?width ?height ?packing () in - let _ = - match isnotempty_callback with - None -> () - | Some callback -> - ignore(input#connect#changed (function () -> callback (input#length > 0))) - in -object(self) - method coerce = input#coerce - method reset = - input#delete_text 0 input#length - (* CSC: txt is now a string, but should be of type Cic.term *) - method set_term txt = - self#reset ; - ignore ((input#insert_text txt) ~pos:0) - (* CSC: this method should disappear *) - method get_as_string = - input#get_chars 0 input#length - method get_term ~context ~metasenv = - let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in - CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf -end -;; - (* MISC FUNCTIONS *) exception IllFormedUri of string;; @@ -291,7 +264,6 @@ let check_window outputhtml uris = in try let mml = !mml_of_cic_term_ref 111 expr in -prerr_endline ("### " ^ CicPp.ppterm expr) ; mmlwidget#load_tree ~dom:mml with e -> @@ -1205,22 +1177,6 @@ let locate_callback id = uris ;; -let locate () = - let inputt = ((rendering_window ())#inputt : term_editor) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - try - match - GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" - with - None -> raise NoChoice - | Some input -> - let uri = locate_callback input in - inputt#set_term uri - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; let input_or_locate_uri ~title = let uri = ref None in @@ -1355,6 +1311,7 @@ let locate_one_id id = List.map cic_textual_parser_uri_of_string uris' ;; + exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;; exception AmbiguousInput;; @@ -1405,22 +1362,40 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = let metasenv',expr = mk_metasenv_and_expr resolve in try (*CSC: Bug here: we do not try to typecheck also the metasenv' *) - ignore - (CicTypeChecker.type_of_aux' metasenv context expr) ; - resolve::(filter tl) + let term,_,_,metasenv'' = + CicRefine.type_of_aux' metasenv' context expr + in + (* If metasen <> metasenv'' is a normal condition, we should *) + (* be prepared to apply the returned substitution to the *) + (* whole current proof. *) + if metasenv <> metasenv'' 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,term,metasenv'')::(filter tl) with - _ -> filter tl + CicRefine.MutCaseFixAndCofixRefineNotImplemented -> + (try + let term = CicTypeChecker.type_of_aux' metasenv' context expr in + (resolve,term,metasenv')::(filter tl) + with _ -> filter tl + ) + | _ -> filter tl in filter resolve_ids in - let resolve_id' = + let resolve_id',term,metasenv' = match resolve_ids' with [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput | [resolve_id] -> resolve_id | _ -> let choices = List.map - (function resolve -> + (function (resolve,_,_) -> List.map (function id -> id, @@ -1444,9 +1419,67 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = List.nth resolve_ids' index in id_to_uris := known_ids @ dom', resolve_id' ; - mk_metasenv_and_expr resolve_id' + metasenv',term +;; + +(* A WIDGET TO ENTER CIC TERMS *) + +class term_editor ?packing ?width ?height ?isnotempty_callback () = + let input = GEdit.text ~editable:true ?width ?height ?packing () in + let _ = + match isnotempty_callback with + None -> () + | Some callback -> + ignore(input#connect#changed (function () -> callback (input#length > 0))) + in +object(self) + method coerce = input#coerce + method reset = + input#delete_text 0 input#length + (* CSC: txt is now a string, but should be of type Cic.term *) + method set_term txt = + self#reset ; + ignore ((input#insert_text txt) ~pos:0) + (* CSC: this method should disappear *) + method get_as_string = + input#get_chars 0 input#length + method get_metasenv_and_term ~context ~metasenv = + let name_context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in + let dom,mk_metasenv_and_expr = + CicTextualParserContext.main + ~context:name_context ~metasenv CicTextualLexer.token lexbuf + in + disambiguate_input context metasenv dom mk_metasenv_and_expr +end +;; + +(* OTHER FUNCTIONS *) + +let locate () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + match + GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" + with + None -> raise NoChoice + | Some input -> + let uri = locate_callback input in + inputt#set_term uri + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ;; + exception UriAlreadyInUse;; exception NotAUriToAConstant;; @@ -1462,7 +1495,7 @@ let new_inductive () = let get_base_uri = ref (function _ -> assert false) in let get_names = ref (function _ -> assert false) in let get_types_and_cons = ref (function _ -> assert false) in - let get_name_context_context_and_subst = ref (function _ -> assert false) in + let get_context_and_subst = ref (function _ -> assert false) in let window = GWindow.window ~width:600 ~modal:true ~position:`CENTER @@ -1607,12 +1640,10 @@ let new_inductive () = let types_and_cons = List.map2 (fun name (newinputt,cons_names_entry) -> - let dom,mk_metasenv_and_expr = - newinputt#get_term ~context:[] ~metasenv:[] in let consnamesstr = cons_names_entry#text in let cons_names = Str.split (Str.regexp " +") consnamesstr in let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr + newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with [] -> expr,cons_names @@ -1635,18 +1666,17 @@ let new_inductive () = CicTypeChecker.typecheck_mutual_inductive_defs uri (tys,params,paramsno) in - get_name_context_context_and_subst := + get_context_and_subst := (function () -> let i = ref 0 in List.fold_left2 - (fun (namecontext,context,subst) name (ty,_) -> + (fun (context,subst) name (ty,_) -> let res = - (Some (Cic.Name name))::namecontext, - (Some (Cic.Name name, Cic.Decl ty))::context, + (Some (Cic.Name name, Cic.Decl ty))::context, (Cic.MutInd (uri,!i,[]))::subst in incr i ; res - ) ([],[],[]) names types_and_cons) ; + ) ([],[]) names types_and_cons) ; let types_and_cons' = List.map2 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) @@ -1707,24 +1737,21 @@ let new_inductive () = (function () -> try chosen := true ; - let namecontext,context,subst= !get_name_context_context_and_subst () in + let context,subst= !get_context_and_subst () in let cons_types = List.map2 (fun name inputt -> - let dom,mk_metasenv_and_expr = - inputt#get_term ~context:namecontext ~metasenv:[] + let metasenv,expr = + inputt#get_metasenv_and_term ~context ~metasenv:[] in - let metasenv,expr = - disambiguate_input context [] dom mk_metasenv_and_expr - in - match metasenv with - [] -> - let undebrujined_expr = - List.fold_left - (fun expr t -> CicSubstitution.subst t expr) expr subst - in - name, undebrujined_expr - | _ -> raise AmbiguousInput + match metasenv with + [] -> + let undebrujined_expr = + List.fold_left + (fun expr t -> CicSubstitution.subst t expr) expr subst + in + name, undebrujined_expr + | _ -> raise AmbiguousInput ) cons cons_type_widgets in get_cons_types := (function () -> cons_types) ; @@ -1788,7 +1815,7 @@ let new_proof () = let notebook = (rendering_window ())#notebook in let chosen = ref false in - let get_parsed = ref (function _ -> assert false) in + let get_metasenv_and_term = ref (function _ -> assert false) in let get_uri = ref (function _ -> assert false) in let non_empty_type = ref false in let window = @@ -1848,7 +1875,7 @@ let new_proof () = (function () -> chosen := true ; try - let parsed = newinputt#get_term [] [] in + let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in let uristr = "cic:" ^ uri_entry#text in let uri = UriManager.uri_of_string uristr in if String.sub uristr (String.length uristr - 4) 4 <> ".con" then @@ -1860,7 +1887,7 @@ let new_proof () = raise UriAlreadyInUse with Getter.Unresolved -> - get_parsed := (function () -> parsed) ; + get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end @@ -1873,18 +1900,15 @@ let new_proof () = GMain.Main.main () ; if !chosen then try - let dom,mk_metasenv_and_expr = !get_parsed () in - let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr - in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.proof := - Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent notebook ; - refresh_proof output ; - !save_set_sensitive true ; - inputt#reset + let metasenv,expr = !get_metasenv_and_term () in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent notebook ; + refresh_proof output ; + !save_set_sensitive true ; + inputt#reset with RefreshSequentException e -> output_html outputhtml @@ -1901,9 +1925,8 @@ let new_proof () = let check_term_in_scratch scratch_window metasenv context expr = try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in + let ty = CicTypeChecker.type_of_aux' metasenv context expr in let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in -prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; scratch_window#show () ; scratch_window#mmlwidget#load_tree ~dom:mml with @@ -1920,29 +1943,18 @@ let check scratch_window () = None -> [] | Some (_,metasenv,_,_) -> metasenv in - let context,names_context = - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - context, - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context in try - let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in - let (metasenv',expr) = - disambiguate_input context metasenv dom mk_metasenv_and_expr - in - check_term_in_scratch scratch_window metasenv' context expr + let metasenv',expr = inputt#get_metasenv_and_term context metasenv in + check_term_in_scratch scratch_window metasenv' context expr with e -> output_html outputhtml @@ -2009,24 +2021,16 @@ let call_tactic_with_input tactic () = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context - in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) canonical_context in try - let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in - let (metasenv',expr) = - disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset + let metasenv',expr = + inputt#get_metasenv_and_term canonical_context metasenv + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic expr ; + refresh_sequent notebook ; + refresh_proof output ; + inputt#reset with RefreshSequentException e -> output_html outputhtml @@ -2139,25 +2143,15 @@ let call_tactic_with_input_and_goal_input tactic () = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None - ) canonical_context + let (metasenv',expr) = + inputt#get_metasenv_and_term canonical_context metasenv in - let dom,mk_metasenv_and_expr = inputt#get_term context metasenv - in - let (metasenv',expr) = - disambiguate_input canonical_context metasenv dom - mk_metasenv_and_expr - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic ~goal_input:(Hashtbl.find ids_to_terms id) + ~input:expr ; + refresh_sequent notebook ; + refresh_proof output ; + inputt#reset | None -> assert false (* "ERROR: No current term!!!" *) with RefreshSequentException e -> @@ -2630,8 +2624,7 @@ let completeSearchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in - let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in + let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = MQueryLevels2.get_constraints expr in let must',only = refine_constraints must in let results = MQueryGenerator.searchPattern must' only in -- 2.39.2