From: Claudio Sacerdoti Coen Date: Tue, 3 Dec 2002 16:05:50 +0000 (+0000) Subject: First working version of the possibility to introduce new inductive type X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0612f5cdb29570e4cf61ef7f40aba91c07f48f62;p=helm.git First working version of the possibility to introduce new inductive type definitions. Many checks have not been implemented yet and the interface allows you to progress to further stages even if the input is incorrect. Nevertheless, if the input is correct it will be accepted by the kernel, saved to disk and notified to the getter. This is the dawn of a new set implementation era. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 9bab1ff9b..a6dfd3a7b 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,14 +60,43 @@ let htmlfooter = "" ;; +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; +(* SACERDOT +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; +*) + +(* TASSI +let prooffile = "//miohelm/tmp/currentproof";; +let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; +*) + +(* GALATA let prooffile = "/home/galata/miohelm/currentproof";; let prooffiletype = "/home/galata/miohelm/currentprooftype";; +*) (*CSC: the getter should handle the innertypes, not the FS *) +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; + +(* SACERDOT +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; +*) + +(* TASSI +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; +*) + +(* GALATA let innertypesfile = "/home/galata/miohelm/innertypes";; let constanttypefile = "/home/galata/miohelm/constanttype";; +*) let empty_id_to_uris = ([],function _ -> None);; @@ -742,6 +771,20 @@ let make_dirs dirpath = ignore (Unix.system ("mkdir -p " ^ dirpath)) ;; +let save_obj uri obj = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object obj + in + (* let's save the theorem and register it to the getter *) + let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types + pathname +;; + let qed () = match !ProofEngine.proof with None -> assert false @@ -1054,7 +1097,9 @@ let setgoal metano = ("

" ^ Printexc.to_string e ^ "

") ;; -let show_in_show_window, show_in_show_window_callback = +let + show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback += let window = GWindow.window ~width:800 ~border_width:2 () in let scrolled_window = @@ -1063,35 +1108,38 @@ let show_in_show_window, show_in_show_window_callback = GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in let href = Gdome.domString "href" in - let show_in_show_window uri = + let show_in_show_window_obj uri obj = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - CicTypeChecker.typecheck uri ; - let obj = CicEnvironment.get_cooked_obj uri in - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object obj + in + let mml = + mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts + ids_to_inner_types in - let mml = - mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts - ids_to_inner_types - in - window#set_title (UriManager.string_of_uri uri) ; - window#misc#hide () ; window#show () ; - mmlwidget#load_tree mml ; + window#set_title (UriManager.string_of_uri uri) ; + window#misc#hide () ; window#show () ; + mmlwidget#load_tree mml ; with e -> output_html outputhtml ("

" ^ Printexc.to_string e ^ "

") ; + in + let show_in_show_window_uri uri = + CicTypeChecker.typecheck uri ; + let obj = CicEnvironment.get_cooked_obj uri in + show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget (n : Gdome.element) = if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then let uri = (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string in - show_in_show_window (UriManager.uri_of_string uri) + show_in_show_window_uri (UriManager.uri_of_string uri) else if mmlwidget#get_action <> None then mmlwidget#action_toggle @@ -1099,7 +1147,8 @@ let show_in_show_window, show_in_show_window_callback = let _ = mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget) in - show_in_show_window, show_in_show_window_callback + show_in_show_window_obj, show_in_show_window_uri, + show_in_show_window_callback ;; exception NoObjectsLocated;; @@ -1381,6 +1430,342 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = exception UriAlreadyInUse;; exception NotAUriToAConstant;; +let new_inductive () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in + + let chosen = ref false in + let inductive = ref true in + let paramsno = ref 0 in + let get_uri = ref (function _ -> assert false) in + 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 window = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:"New Block of Mutual (Co)Inductive Definitions" + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the URI for the new block:" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let uri_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + let hbox0 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label + ~text: + "Enter the number of left parameters in every arity and constructor type:" + ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let paramsno_entry = + GEdit.entry ~editable:true ~text:"0" + ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in + let hbox1 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Are the definitions inductive or coinductive?" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let inductiveb = + GButton.radio_button ~label:"Inductive" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let coinductiveb = + GButton.radio_button ~label:"Coinductive" + ~group:inductiveb#group + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the list of the names of the types:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let names_entry = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + (* First phase *) + let rec phase1 () = + ignore + (okb#connect#clicked + (function () -> + try + let uristr = "cic:" ^ uri_entry#text in + let namesstr = names_entry#text in + let paramsno' = int_of_string (paramsno_entry#text) in + match Str.split (Str.regexp " +") namesstr with + [] -> assert false + | (he::tl) as names -> + let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in + begin + try + ignore (Getter.resolve uri) ; + raise UriAlreadyInUse + with + Getter.Unresolved -> + get_uri := (function () -> uri) ; + get_names := (function () -> names) ; + inductive := inductiveb#active ; + paramsno := paramsno' ; + phase2 () + end + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) + (* Second phase *) + and phase2 () = + let type_widgets = + List.map + (function name -> + let frame = + GBin.frame ~label:name + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let vbox = GPack.vbox ~packing:frame#add () in + let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in + let _ = + GMisc.label ~text:("Enter its type:") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + let newinputt = + new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add () + ~isnotempty_callback: + (function b -> + (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) + in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the list of its constructors:") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cons_names_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + (newinputt,cons_names_entry) + ) (!get_names ()) + in + vbox#remove hboxn#coerce ; + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + let names = !get_names () in + 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 + in + match metasenv with + [] -> expr,cons_names + | _ -> raise AmbiguousInput + ) names type_widgets + in + (* Let's see if so far the definition is well-typed *) + let uri = !get_uri () in + let params = [] in + let paramsno = 0 in + let tys = + let i = ref 0 in + List.map2 + (fun name (ty,cons) -> + let cons' = + List.map + (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in + let res = (name, !inductive, ty, cons') in + incr i ; + res + ) names types_and_cons + in +(*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi + anche quando paramsno > 0 ;-(((( + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,paramsno) ; +*) + get_name_context_context_and_subst := + (function () -> + let i = ref 0 in + List.fold_left2 + (fun (namecontext,context,subst) name (ty,_) -> + let res = + (Some (Cic.Name name))::namecontext, + (Some (Cic.Name name, Cic.Decl ty))::context, + (Cic.MutInd (uri,!i,[]))::subst + in + incr i ; res + ) ([],[],[]) names types_and_cons) ; + let types_and_cons' = + List.map2 + (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) + names types_and_cons + in + get_types_and_cons := (function () -> types_and_cons') ; + chosen := true ; + window#destroy () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) + (* Third phase *) + and phase3 name cons = + let get_cons_types = ref (function () -> assert false) in + let window2 = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:(name ^ " Constructors") + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window2#add () in + let cons_type_widgets = + List.map + (function consname -> + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the type of " ^ consname ^ ":") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + let newinputt = + new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add () + ~isnotempty_callback: + (function b -> + (* (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)()) + in + newinputt + ) cons in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window2#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window2#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + chosen := true ; + let namecontext,context,subst= !get_name_context_context_and_subst () in + let cons_types = + List.map2 + (fun name inputt -> + let dom,mk_metasenv_and_expr = + inputt#get_term ~context:namecontext ~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 + ) cons cons_type_widgets + in + get_cons_types := (function () -> cons_types) ; + window2#destroy () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) ; + window2#show () ; + GMain.Main.main () ; + let okb_pressed = !chosen in + chosen := false ; + if (not okb_pressed) then + begin + window#destroy () ; + assert false (* The control never reaches this point *) + end + else + (!get_cons_types ()) + in + phase1 () ; + (* No more phases left or Abort pressed *) + window#show () ; + GMain.Main.main () ; + window#destroy () ; + if !chosen then + try + let uri = !get_uri () in +(*CSC: Da finire *) + let params = [] in + let tys = !get_types_and_cons () in + let obj = Cic.InductiveDefinition tys params !paramsno in + begin + try + prerr_endline (CicPp.ppobj obj) ; + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) ; + with + e -> + prerr_endline "Offending mutual (co)inductive type declaration:" ; + prerr_endline (CicPp.ppobj obj) ; + end ; + (* We already know that obj is well-typed. We need to add it to the *) + (* environment in order to compute the inner-types without having to *) + (* debrujin it or having to modify lots of other functions to avoid *) + (* asking the environment for the MUTINDs we are defining now. *) + CicEnvironment.put_inductive_definition uri obj ; + save_obj uri obj ; + show_in_show_window_obj uri obj + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + let new_proof () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in @@ -1932,7 +2317,7 @@ let simpl_in_scratch scratch_window = let show () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - show_in_show_window (input_or_locate_uri ~title:"Show") + show_in_show_window_uri (input_or_locate_uri ~title:"Show") with e -> output_html outputhtml @@ -1976,6 +2361,19 @@ let open_ () = ;; +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 + ignore (MQueryLevels2.get_constraints expr) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + let searchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in @@ -2504,6 +2902,10 @@ class rendering_window output (notebook : notebook) = let factory1 = new GMenu.factory file_menu ~accel_group in let export_to_postscript_menu_item = begin + let _ = + factory1#add_item "New Block of (Co)Inductive Definitions..." + ~key:GdkKeysyms._B ~callback:new_inductive + in let _ = factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N ~callback:new_proof @@ -2567,6 +2969,10 @@ class rendering_window output (notebook : notebook) = let _ = factory4#add_item "Locate..." ~key:GdkKeysyms._T ~callback:locate in + let searchPattern_menu_item = + factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D + ~callback:completeSearchPattern in + let _ = searchPattern_menu_item#misc#set_sensitive false in let show_menu_item = factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show in @@ -2600,7 +3006,10 @@ class rendering_window output (notebook : notebook) = ~packing:frame#add () in let inputt = new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () - ~isnotempty_callback:check_menu_item#misc#set_sensitive in + ~isnotempty_callback: + (function b -> + check_menu_item#misc#set_sensitive b ; + searchPattern_menu_item#misc#set_sensitive b) in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = @@ -2657,17 +3066,12 @@ let initialize_everything () = let _ = if !usedb then -(*<<<<<<< gTopLevel.ml -(* Mqint.init "dbname=helm_mowgli" ; *) -Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; -=======*) begin Mqint.set_database Mqint.postgres_db ; (* Mqint.init "dbname=helm_mowgli" ; *) (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *) - Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ; + Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"; end ; -(*>>>>>>> 1.35.2.34*) ignore (GtkMain.Main.init ()) ; initialize_everything () ; if !usedb then Mqint.close ();