From 2dde94202f728a388eabd91018d71c0bce0708cb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 10 Jun 2005 16:57:33 +0000 Subject: [PATCH] added records --- helm/matita/matitaEngine.ml | 110 ++++++++---------- helm/matita/matitaGui.ml | 5 +- helm/matita/matitaSync.ml | 92 ++++++++++++++- helm/matita/matitaSync.mli | 4 + helm/matita/tests/test_abort.ma | 16 --- .../cic_disambiguation/cicTextualParser2.ml | 19 ++- 6 files changed, 165 insertions(+), 81 deletions(-) delete mode 100644 helm/matita/tests/test_abort.ma diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index f16b02266..2c946199b 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -79,7 +79,9 @@ let tactic_of_ast = function | _ -> false) context with - Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis")) + Not_found -> + raise (ProofEngineTypes.Fail + (ident ^ " is not an hypothesis")) in (match hyp with | Some (_, Cic.Decl term) -> term @@ -160,31 +162,6 @@ let eval_tactical status tac = in apply_tactic (tactical_of_ast tac) -(** given a uri and a type list (the contructors types) builds a list of pairs - * (name,uri) that is used to generate authomatic aliases **) -let extract_alias types uri = - fst(List.fold_left ( - fun (acc,i) (name, _, _, cl) -> - ((name, UriManager.string_of_uriref (uri,[i])) - :: - (fst(List.fold_left ( - fun (acc,j) (name,_) -> - (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) - ) (acc,1) cl))),i+1 - ) ([],0) types) - -(** adds a (name,uri) list l to a disambiguation environment e **) -let env_of_list l e = - let module DT = DisambiguateTypes in - let module DTE = DisambiguateTypes.Environment in - List.fold_left ( - fun e (name,uri) -> - DTE.add - (DT.Id name) - (uri,fun _ _ _ -> CicUtil.term_of_uri uri) - e - ) e l - let eval_coercion status coercion = let coer_uri,coer_ty = match coercion with @@ -279,16 +256,16 @@ let eval_command status cmd = "type you've declared!"); MatitaLog.message (sprintf "%s defined" suri); let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in - let status = - let name = UriManager.name_of_uri uri in - let new_env = env_of_list [(name,suri)] status.aliases in - {status with aliases = new_env } - in + {status with proof_status = No_proof } + | TacticAst.Record (loc, params, name, ty, fields) -> + let suri = MatitaMisc.qualify status name ^ ".ind" in + let record_spec = (suri, params, ty, fields) in + let status = MatitaSync.add_record_def record_spec status in {status with proof_status = No_proof } | TacticAst.Inductive (loc, dummy_params, types) -> (* dummy_params are not real params, it is a list of nothing, and the only - * semantic content is the len, that is leftno (note: leftno and pamaters - * have nothing in common). + * semantic content is the len, that is leftno (note: leftno and + * paramaters have nothing in common). *) let suri = match types with @@ -303,28 +280,9 @@ let eval_command status cmd = (types, [], leftno) CicUniv.empty_ugraph in let status = - MatitaSync.add_inductive_def - ~uri ~types ~params:[] ~leftno ~ugraph status + MatitaSync.add_inductive_def ~uri ~types ~leftno ~ugraph status in - (* aliases for the constructors and types *) - let aliases = env_of_list (extract_alias types uri) status.aliases in - (* aliases for the eliminations principles *) - let aliases = - let base = String.sub suri 0 (String.length suri - 4) in - env_of_list - (List.fold_left ( - fun acc suffix -> - if List.exists ( - fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix - ) status.objects then - let u = base ^ suffix in - (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc - else - acc - ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases - in - let status = {status with proof_status = No_proof } in - { status with aliases = aliases} + {status with proof_status = No_proof } | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) -> let uri = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") @@ -356,11 +314,6 @@ let eval_command status cmd = let body = CicMetaSubst.apply_subst subst body in let ty = CicMetaSubst.apply_subst subst ty in let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in - let status = - let suri = UriManager.string_of_uri uri in - let new_env = env_of_list [(name,suri)] status.aliases in - {status with aliases = new_env } - in {status with proof_status = No_proof} | TacticAst.Theorem (_, _, None, _, _) -> command_error "The grammar should avoid having unnamed theorems!" @@ -426,7 +379,7 @@ let disambiguate_term status term = in status, cic -let disambiguate_terms status terms = +let disambiguate_closedtypes status terms = let term = CicAst.pack terms in let status, term = disambiguate_term status term in status, CicUtil.unpack term @@ -575,7 +528,7 @@ let disambiguate_inddef status params indTypes = add_ast (add_pi params typ); List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors) indTypes; - let status, terms = disambiguate_terms status !asts in + let status, terms = disambiguate_closedtypes status !asts in let terms = ref (List.rev terms) in let get_term () = match !terms with [] -> assert false | hd :: tl -> terms := tl; hd @@ -613,7 +566,41 @@ let disambiguate_inddef status params indTypes = let cicIndTypes = List.rev cicIndTypes in status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno)) +let disambiguate_record status params ty fields = + let packed = + List.fold_right + (fun (name,ast) acc -> + CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc)) + (params @ ["",ty] @ fields) (CicAst.Sort `Type) + in + prerr_endline (CicAstPp.pp_term packed); + let status, packed = disambiguate_term status packed in + let rec split t = function + | [] -> [],t + | (n,_)::tl -> + match t with + | Cic.Prod (_, src, tgt) -> + let l, t = split tgt tl in + (n, src) :: l, t + | _-> assert false + in + let params, t = split packed params in + let ty, t = + match t with + | Cic.Prod (_ , ty, t) -> ty, t + | _ -> assert false + in + let fields, _ = + split (let t,_,_ = CicMetaSubst.delift_rels [] [] 1 t in t) fields + in + params, ty, fields + let disambiguate_command status = function + | TacticAst.Record(loc, params,name,ty,fields) -> + let params, ty, fields = + disambiguate_record status params ty fields + in + status, TacticAst.Record(loc, params, name, ty, fields) | TacticAst.Inductive (loc, params, types) -> let (status, (uri, (ind_types, vars, paramsno))) = disambiguate_inddef status params types @@ -709,3 +696,4 @@ let initial_status = objects = []; } + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 34238f80d..abab0f793 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -174,7 +174,7 @@ class gui () = | Some f -> script#reset (); script#loadFrom f; - console#message ("'"^f^"' loaded."); + console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f | None -> () in @@ -289,7 +289,8 @@ class gui () = initializer self#check_widgets (); let combo_widget = combo#coerce in - uriHBox#add combo_widget + uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; + combo#entry#misc#grab_focus () method browserUri = combo end diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 9a44742b7..850c23ddd 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -27,6 +27,58 @@ open Printf open MatitaTypes +(** given a uri and a type list (the contructors types) builds a list of pairs + * (name,uri) that is used to generate authomatic aliases **) +let extract_alias types uri = + fst(List.fold_left ( + fun (acc,i) (name, _, _, cl) -> + ((name, UriManager.string_of_uriref (uri,[i])) + :: + (fst(List.fold_left ( + fun (acc,j) (name,_) -> + (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1) + ) (acc,1) cl))),i+1 + ) ([],0) types) + +(** adds a (name,uri) list l to a disambiguation environment e **) +let env_of_list l e = + let module DT = DisambiguateTypes in + let module DTE = DisambiguateTypes.Environment in + List.fold_left ( + fun e (name,uri) -> + DTE.add + (DT.Id name) + (uri,fun _ _ _ -> CicUtil.term_of_uri uri) + e + ) e l + +let add_aliases_for_object status suri = + let uri = UriManager.uri_of_string suri in + let name = UriManager.name_of_uri uri in + let new_env = env_of_list [(name,suri)] status.aliases in + {status with aliases = new_env } + +let add_aliases_for_inductive_def status types suri = + let uri = UriManager.uri_of_string suri in + (* aliases for the constructors and types *) + let aliases = env_of_list (extract_alias types uri) status.aliases in + (* aliases for the eliminations principles *) + let base = String.sub suri 0 (String.length suri - 4) in + let alisases = + env_of_list + (List.fold_left ( + fun acc suffix -> + if List.exists ( + fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix + ) status.objects then + let u = base ^ suffix in + (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc + else + acc + ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases + in + {status with aliases = aliases } + let paths_and_uris_of_obj uri status = let basedir = get_string_option status "basedir" in let innertypesuri = UriManager.innertypesuri_of_uri uri in @@ -106,6 +158,7 @@ let add_constant ~uri ?body ~ty ~ugraph ?(params = []) ?(attrs = []) status = MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s constant defined" suri); + let status = add_aliases_for_object status suri in { status with objects = new_stuff @ status.objects } end @@ -129,6 +182,7 @@ let add_inductive_def MetadataDb.index_obj ~dbd ~uri; (* must be in the env *) let new_stuff = save_object_to_disk status uri obj in MatitaLog.message (sprintf "%s inductive type defined" suri); + let status = add_aliases_for_inductive_def status types suri in let status = { status with objects = new_stuff @ status.objects } in let elim sort status = try @@ -146,7 +200,43 @@ let add_inductive_def status [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; end - + +let add_record_def (suri, params, ty, fields) status = + let module CTC = CicTypeChecker in + let uri = UriManager.uri_of_string suri in + let buri = UriManager.buri_of_uri uri in + let record_spec = suri, params, ty, fields in + let types, leftno, obj, ugraph = CicRecord.inductive_of_record record_spec in + let status = add_inductive_def ~uri ~types ~leftno ~ugraph status in + let projections = CicRecord.projections_of record_spec in + let status = + List.fold_left ( + fun status (suri, name, t) -> + try + let ty, ugraph = + CTC.type_of_aux' [] [] t CicUniv.empty_ugraph + in + (* THIS MUST BE IN SYNC WITH CicRecord *) + let uri = UriManager.uri_of_string suri in + let t = Unshare.unshare t in + let ty = Unshare.unshare ty in + let status = add_constant ~uri ~body:t ~ty ~ugraph status in + add_aliases_for_object status suri + with + | CTC.TypeCheckerFailure s -> + MatitaLog.message + ("Unable to create projection " ^ name ^ " cause: " ^ s); + status + | Http_getter_types.Key_not_found s -> + let depend = UriManager.uri_of_string s in + let depend = UriManager.name_of_uri depend in + MatitaLog.message + ("Unable to create projection " ^ name ^ " cause uses " ^ depend); + status + ) status projections + in + status + module OrderedUri = struct type t = UriManager.uri * string diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index 8e85c4186..ee0c9b6e7 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -36,6 +36,10 @@ val add_inductive_def: ?params:UriManager.uri list -> ?leftno:int -> ?attrs:Cic.attribute list -> ugraph:CicUniv.universe_graph -> MatitaTypes.status -> MatitaTypes.status + +val add_record_def: + CicRecord.record_spec -> + MatitaTypes.status -> MatitaTypes.status val time_travel: present:MatitaTypes.status -> past:MatitaTypes.status -> unit diff --git a/helm/matita/tests/test_abort.ma b/helm/matita/tests/test_abort.ma deleted file mode 100644 index e589c5aaa..000000000 --- a/helm/matita/tests/test_abort.ma +++ /dev/null @@ -1,16 +0,0 @@ -alias symbol "eq" (instance 0) = "leibnitz's equality". -theorem a:\forall x.x=x. -alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -goal 5. -exact nat. -intro. -reflexivity. -qed. -alias num (instance 0) = "natural number". -alias symbol "times" (instance 0) = "natural times". - -theorem b:\forall p:nat. p * 0=0. -intro. -auto. -abort. -qed. \ No newline at end of file diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 951028745..a7d43bb45 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -472,7 +472,22 @@ EXTEND let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; - + + record_spec: [ [ + name = IDENT; params = LIST0 [ arg = arg -> arg ] ; + SYMBOL ":"; typ = term; SYMBOL <:unicode>; PAREN "{" ; + fields = LIST0 [ + name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) + ] SEP SYMBOL ";"; PAREN "}" -> + let params = + List.fold_right + (fun (names, typ) acc -> + (List.map (fun name -> (name, typ)) names) @ acc) + params [] + in + (params,name,typ,fields) + ] ]; + macro: [ [ [ IDENT "quit" ] -> TacticAst.Quit loc (* | [ IDENT "abort" ] -> TacticAst.Abort loc *) @@ -572,6 +587,8 @@ EXTEND TacticAst.Coercion (loc, CicAst.Uri (name,Some [])) | [ IDENT "alias" ]; spec = alias_spec -> TacticAst.Alias (loc, spec) + | [ IDENT "record" ]; (params,name,ty,fields) = record_spec -> + TacticAst.Record (loc, params,name,ty,fields) ]]; executable: [ -- 2.39.2