From: Claudio Sacerdoti Coen Date: Wed, 27 Sep 2006 09:49:48 +0000 (+0000) Subject: Initial work on setoids: X-Git-Tag: 0.4.95@7852~990 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e53c9d7cf1a5d3d33c41cad5b046b018a62a9d2d;p=helm.git Initial work on setoids: - AST changed to make it more parametric on terms (for the Relation command) - functions that work on ASTs consider the constructors in alphabetical order - --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 6bde8baee..c7d644e60 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -117,17 +117,19 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 9 +let magic = 10 -type 'obj command = +type ('term,'obj) command = + | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *) | Default of loc * string * UriManager.uri list + | Drop of loc | Include of loc * string + | Obj of loc * 'obj + | Relation of + loc * string * 'term * 'term * 'term option * 'term option * 'term option | Set of loc * string * string - | Drop of loc | Print of loc * string | Qed of loc - | Coercion of loc * UriManager.uri * bool (* add_obj *) * int (* arity *) - | Obj of loc * 'obj type ('term, 'lazy_term, 'reduction, 'ident) tactical = | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic @@ -161,7 +163,7 @@ let is_punctuation = | _ -> false type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = - | Command of loc * 'obj command + | Command of loc * ('term, 'obj) command | Macro of loc * 'term macro | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *) diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 365bc9375..569b68399 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -221,16 +221,26 @@ let pp_coercion uri do_composites arity = sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity (if do_composites then "compounds" else "no compounds") -let pp_command ~obj_pp = function +let pp_command ~term_pp ~obj_pp = function + | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i + | Default (_,what,uris) -> pp_default what uris + | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\"" + | Obj (_,obj) -> obj_pp obj | Qed _ -> "qed" - | Drop _ -> "drop" + | Relation (_,id,a,aeq,refl,sym,trans) -> + "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^ + (match refl with + Some r -> " reflexivity proved by " ^ term_pp r + | None -> "") ^ + (match sym with + Some r -> " symmetry proved by " ^ term_pp r + | None -> "") ^ + (match trans with + Some r -> " transitivity proved by " ^ term_pp r + | None -> "") | Print (_,s) -> "print " ^ s | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value - | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i - | Obj (_,obj) -> obj_pp obj - | Default (_,what,uris) -> - pp_default what uris let rec pp_tactical ~term_pp ~lazy_term_pp = let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in @@ -271,7 +281,7 @@ let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = pp_tactical ~lazy_term_pp ~term_pp tac ^ pp_tactical ~lazy_term_pp ~term_pp punct | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac - | Command (_, cmd) -> pp_command ~obj_pp cmd ^ "." + | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "." let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = function diff --git a/components/grafite/grafiteAstPp.mli b/components/grafite/grafiteAstPp.mli index f9b3b37cc..7478883aa 100644 --- a/components/grafite/grafiteAstPp.mli +++ b/components/grafite/grafiteAstPp.mli @@ -41,7 +41,10 @@ val pp_reduction_kind: 'a GrafiteAst.reduction -> string -val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string +val pp_command: + term_pp:('term -> string) -> + obj_pp:('obj -> string) -> + ('term,'obj) GrafiteAst.command -> string val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string val pp_comment: term_pp:('term -> string) -> diff --git a/components/grafite/grafiteMarshal.ml b/components/grafite/grafiteMarshal.ml index 2b1ed9dba..cc4423b96 100644 --- a/components/grafite/grafiteMarshal.ml +++ b/components/grafite/grafiteMarshal.ml @@ -25,7 +25,7 @@ (* $Id$ *) -type ast_command = Cic.obj GrafiteAst.command +type ast_command = (Cic.term,Cic.obj) GrafiteAst.command type moo = ast_command list let format_name = "grafite" @@ -48,8 +48,9 @@ let rehash_cmd_uris = GrafiteAst.Coercion (loc, rehash_uri uri, close, arity) | cmd -> prerr_endline "Found a command not expected in a .moo:"; + let term_pp _ = assert false in let obj_pp _ = assert false in - prerr_endline (GrafiteAstPp.pp_command ~obj_pp cmd); + prerr_endline (GrafiteAstPp.pp_command ~term_pp ~obj_pp cmd); assert false let save_moo ~fname moo = save_moo_to_file ~fname (List.rev moo) diff --git a/components/grafite/grafiteMarshal.mli b/components/grafite/grafiteMarshal.mli index e60ad39d8..cad7b1187 100644 --- a/components/grafite/grafiteMarshal.mli +++ b/components/grafite/grafiteMarshal.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -type ast_command = Cic.obj GrafiteAst.command +type ast_command = (Cic.term,Cic.obj) GrafiteAst.command type moo = ast_command list val save_moo: fname:string -> moo -> unit diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 7f342b392..2d0d691f1 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -25,8 +25,6 @@ (* $Id$ *) -module GT = GrafiteTypes - open Printf exception Drop @@ -34,7 +32,7 @@ exception Drop exception IncludedFileNotCompiled of string * string exception Macro of GrafiteAst.loc * - (Cic.context -> GT.status * Cic.term GrafiteAst.macro) + (Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) exception ReadOnlyUri of string type 'a disambiguator_input = string * int * 'a @@ -297,13 +295,13 @@ let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = (* prerr_endline "apply_tactic"; *) -(* prerr_endline (Continuationals.Stack.pp (GT.get_stack status)); *) - let starting_metasenv = GT.get_proof_metasenv status in +(* prerr_endline (Continuationals.Stack.pp (GrafiteTypes.get_stack status)); *) + let starting_metasenv = GrafiteTypes.get_proof_metasenv status in let before = List.map (fun g, _, _ -> g) starting_metasenv in (* prerr_endline "disambiguate"; *) let status, tactic = disambiguate_tactic status goal (text,prefix_len,tactic) in - let metasenv_after_refinement = GT.get_proof_metasenv status in - let proof = GT.get_current_proof status in + let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in + let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, goal in let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in @@ -335,82 +333,82 @@ prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int clos proof, opened_goals in let incomplete_proof = - match status.GT.proof_status with - | GT.Incomplete_proof p -> p + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof p -> p | _ -> assert false in - { status with GT.proof_status = - GT.Incomplete_proof - { incomplete_proof with GT.proof = proof } }, + { status with GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { incomplete_proof with GrafiteTypes.proof = proof } }, opened_goals, closed_goals type eval_ast = {ea_go: 'term 'lazy_term 'reduction 'obj 'ident. disambiguate_tactic: - (GT.status -> + (GrafiteTypes.status -> ProofEngineTypes.goal -> (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic) disambiguator_input -> - GT.status * + GrafiteTypes.status * (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: - (GT.status -> - ('obj GrafiteAst.command) disambiguator_input -> - GT.status * Cic.obj GrafiteAst.command) -> + (GrafiteTypes.status -> + (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> disambiguate_macro: - (GT.status -> + (GrafiteTypes.status -> ('term GrafiteAst.macro) disambiguator_input -> - Cic.context -> GT.status * Cic.term GrafiteAst.macro) -> + Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> ?do_heavy_checks:bool -> ?clean_baseuri:bool -> - GT.status -> + GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> - GT.status * UriManager.uri list + GrafiteTypes.status * UriManager.uri list } type 'a eval_command = {ec_go: 'term 'obj. disambiguate_command: - (GT.status -> ('obj GrafiteAst.command) disambiguator_input -> - GT.status * Cic.obj GrafiteAst.command) -> - options -> GT.status -> - ('obj GrafiteAst.command) disambiguator_input -> - GT.status * UriManager.uri list + (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> + options -> GrafiteTypes.status -> + (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * UriManager.uri list } type 'a eval_executable = {ee_go: 'term 'lazy_term 'reduction 'obj 'ident. disambiguate_tactic: - (GT.status -> + (GrafiteTypes.status -> ProofEngineTypes.goal -> (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic) disambiguator_input -> - GT.status * + GrafiteTypes.status * (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) -> disambiguate_command: - (GT.status -> - ('obj GrafiteAst.command) disambiguator_input -> - GT.status * Cic.obj GrafiteAst.command) -> + (GrafiteTypes.status -> + (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> disambiguate_macro: - (GT.status -> + (GrafiteTypes.status -> ('term GrafiteAst.macro) disambiguator_input -> - Cic.context -> GT.status * Cic.term GrafiteAst.macro) -> + Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro) -> options -> - GT.status -> + GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input -> - GT.status * UriManager.uri list + GrafiteTypes.status * UriManager.uri list } type 'a eval_from_moo = - { efm_go: GT.status -> string -> GT.status } + { efm_go: GrafiteTypes.status -> string -> GrafiteTypes.status } let coercion_moo_statement_of arity uri = GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity) @@ -445,18 +443,18 @@ let eval_coercion status ~add_composites uri arity = let moo_content = List.map (coercion_moo_statement_of arity) (uri::compounds) in - let status = GT.add_moo_content moo_content status in - {status with GT.proof_status = GT.No_proof}, + let status = GrafiteTypes.add_moo_content moo_content status in + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, compounds let eval_tactical ~disambiguate_tactic status tac = let apply_tactic = apply_tactic ~disambiguate_tactic in let module MatitaStatus = struct - type input_status = GT.status * ProofEngineTypes.goal + type input_status = GrafiteTypes.status * ProofEngineTypes.goal type output_status = - GT.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list + GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list type tactic = input_status -> output_status @@ -465,20 +463,20 @@ let eval_tactical ~disambiguate_tactic status tac = let apply_tactic tac = tac let goals (_, opened, closed) = opened, closed let set_goals (opened, closed) (status, _, _) = (status, opened, closed) - let get_stack (status, _) = GT.get_stack status + let get_stack (status, _) = GrafiteTypes.get_stack status let get_status (status, goal) = - match status.GT.proof_status with - | GT.Incomplete_proof incomplete -> incomplete.GT.proof, goal + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof, goal | _ -> assert false let get_proof (status, _, _) = - match status.GT.proof_status with - | GT.Incomplete_proof incomplete -> incomplete.GT.proof + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof incomplete -> incomplete.GrafiteTypes.proof | _ -> assert false let set_stack stack (status, opened, closed) = - GT.set_stack stack status, opened, closed + GrafiteTypes.set_stack stack status, opened, closed let inject (status, _) = (status, [], []) let focus goal (status, _, _) = (status, goal) @@ -526,11 +524,11 @@ let eval_tactical ~disambiguate_tactic status tac = in let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in let status = (* is proof completed? *) - match status.GT.proof_status with - | GT.Incomplete_proof - { GT.stack = stack; proof = proof } + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Incomplete_proof + { GrafiteTypes.stack = stack; proof = proof } when Continuationals.Stack.is_empty stack -> - { status with GT.proof_status = GT.Proof proof } + { status with GrafiteTypes.proof_status = GrafiteTypes.Proof proof } | _ -> status in status @@ -567,7 +565,7 @@ let add_coercions_of_record_to_moo obj lemmas status = | (name,true,arity) -> Some (arity, UriManager.uri_of_string - (GT.qualify status name ^ ".con")) + (GrafiteTypes.qualify status name ^ ".con")) | _ -> None) fields in @@ -605,9 +603,9 @@ let add_coercions_of_record_to_moo obj lemmas status = List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) lemmas; *) - let status = GT.add_moo_content moo_content status in + let status = GrafiteTypes.add_moo_content moo_content status in {status with - GT.coercions = coercions @ status.GT.coercions}, + GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions}, lemmas let add_obj uri obj status = @@ -619,14 +617,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with - | GrafiteAst.Print (_,"proofterm") -> - let _,_,p,_ = GT.get_current_proof status in - print_endline (AutoTactic.pp_proofterm p); - status,[] - | GrafiteAst.Print (_,_) -> status,[] + | GrafiteAst.Coercion (loc, uri, add_composites, arity) -> + eval_coercion status ~add_composites uri arity | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; - GT.add_moo_content [cmd] status,[] + GrafiteTypes.add_moo_content [cmd] status,[] + | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Include (loc, baseuri) -> let moopath_rw, moopath_r = LibraryMisc.obj_file_of_baseuri @@ -641,13 +637,43 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in let status = eval_from_moo.efm_go status moopath in status,[] + | GrafiteAst.Print (_,"proofterm") -> + let _,_,p,_ = GrafiteTypes.get_current_proof status in + print_endline (AutoTactic.pp_proofterm p); + status,[] + | GrafiteAst.Print (_,_) -> status,[] + | GrafiteAst.Qed loc -> + let uri, metasenv, bo, ty = + match status.GrafiteTypes.proof_status with + | GrafiteTypes.Proof (Some uri, metasenv, body, ty) -> + uri, metasenv, body, ty + | GrafiteTypes.Proof (None, metasenv, body, ty) -> + raise (GrafiteTypes.Command_error + ("Someone allows to start a theorem without giving the "^ + "name/uri. This should be fixed!")) + | _-> + raise + (GrafiteTypes.Command_error "You can't Qed an incomplete theorem") + in + if metasenv <> [] then + raise + (GrafiteTypes.Command_error + "Proof not completed! metasenv is not empty!"); + let name = UriManager.name_of_uri uri in + let obj = Cic.Constant (name,Some bo,ty,[],[]) in + let status, lemmas = add_obj uri obj status in + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, + uri::lemmas + | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> + Setoids.add_relation id a aeq refl sym trans; + status, [] (*CSC: TO BE FIXED *) | GrafiteAst.Set (loc, name, value) -> if name = "baseuri" then begin let value = let v = Http_getter_misc.strip_trailing_slash value in try ignore (String.index v ' '); - GT.command_error "baseuri can't contain spaces" + GrafiteTypes.command_error "baseuri can't contain spaces" with Not_found -> v in if Http_getter_storage.is_read_only value then begin @@ -669,32 +695,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (Filename.dirname (Http_getter.filename ~writable:true (value ^ "/foo.con"))); end; - GT.set_option status name value,[] - | GrafiteAst.Drop loc -> raise Drop - | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = - match status.GT.proof_status with - | GT.Proof (Some uri, metasenv, body, ty) -> - uri, metasenv, body, ty - | GT.Proof (None, metasenv, body, ty) -> - raise (GT.Command_error - ("Someone allows to start a theorem without giving the "^ - "name/uri. This should be fixed!")) - | _-> - raise - (GT.Command_error "You can't Qed an incomplete theorem") - in - if metasenv <> [] then - raise - (GT.Command_error - "Proof not completed! metasenv is not empty!"); - let name = UriManager.name_of_uri uri in - let obj = Cic.Constant (name,Some bo,ty,[],[]) in - let status, lemmas = add_obj uri obj status in - {status with GT.proof_status = GT.No_proof}, - uri::lemmas - | GrafiteAst.Coercion (loc, uri, add_composites, arity) -> - eval_coercion status ~add_composites uri arity + GrafiteTypes.set_option status name value,[] | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -705,9 +706,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status (match types with (name,_,_,_)::_ -> name | _ -> assert false) | _ -> assert false in let uri = - UriManager.uri_of_string (GT.qualify status name ^ ext) in + UriManager.uri_of_string (GrafiteTypes.qualify status name ^ ext) in let obj = CicRefine.pack_coercion_obj obj in - let metasenv = GT.get_proof_metasenv status in + let metasenv = GrafiteTypes.get_proof_metasenv status in match obj with | Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> let name = UriManager.name_of_uri uri in @@ -743,25 +744,25 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status end; let initial_proof = (Some uri, metasenv', bo, ty) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in - { status with GT.proof_status = - GT.Incomplete_proof - { GT.proof = initial_proof; stack = initial_stack } }, + { status with GrafiteTypes.proof_status = + GrafiteTypes.Incomplete_proof + { GrafiteTypes.proof = initial_proof; stack = initial_stack } }, [] | _ -> if metasenv <> [] then - raise (GT.Command_error ( + raise (GrafiteTypes.Command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv)); let status, lemmas = add_obj uri obj status in let status,new_lemmas = add_coercions_of_record_to_moo obj lemmas status in - {status with GT.proof_status = GT.No_proof}, + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, uri::new_lemmas@lemmas in - match status.GT.proof_status with - GT.Intermediate _ -> - {status with GT.proof_status = GT.No_proof},uris + match status.GrafiteTypes.proof_status with + GrafiteTypes.Intermediate _ -> + {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris | _ -> status,uris } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command diff --git a/components/grafite_engine/grafiteEngine.mli b/components/grafite_engine/grafiteEngine.mli index 8363971ae..63580ad2e 100644 --- a/components/grafite_engine/grafiteEngine.mli +++ b/components/grafite_engine/grafiteEngine.mli @@ -42,8 +42,8 @@ val eval_ast : disambiguate_command: (GrafiteTypes.status -> - ('obj GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * Cic.obj GrafiteAst.command) -> + (('term,'obj) GrafiteAst.command) disambiguator_input -> + GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) -> disambiguate_macro: (GrafiteTypes.status -> diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 6df39bfc4..4baac499f 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -362,19 +362,37 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = lexicon_status, metasenv, cic let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)= - match cmd with - | GrafiteAst.Coercion _ - | GrafiteAst.Default _ - | GrafiteAst.Drop _ - | GrafiteAst.Print _ - | GrafiteAst.Include _ - | GrafiteAst.Qed _ - | GrafiteAst.Set _ as cmd -> - lexicon_status,metasenv,cmd - | GrafiteAst.Obj (loc,obj) -> - let lexicon_status,metasenv,obj = - disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in - lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + match cmd with + | GrafiteAst.Coercion _ + | GrafiteAst.Default _ + | GrafiteAst.Drop _ + | GrafiteAst.Include _ + | GrafiteAst.Print _ + | GrafiteAst.Qed _ + | GrafiteAst.Set _ as cmd -> + lexicon_status,metasenv,cmd + | GrafiteAst.Obj (loc,obj) -> + let lexicon_status,metasenv,obj = + disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj)in + lexicon_status, metasenv, GrafiteAst.Obj (loc,obj) + | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> + let lexicon_status_ref = ref lexicon_status in + let disambiguate_term = + disambiguate_term text prefix_len lexicon_status_ref [] in + let disambiguate_term_option metasenv = + function + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term metasenv t in + metasenv, Some t + in + let metasenv,a = disambiguate_term metasenv a in + let metasenv,aeq = disambiguate_term metasenv aeq in + let metasenv,refl = disambiguate_term_option metasenv refl in + let metasenv,sym = disambiguate_term_option metasenv sym in + let metasenv,trans = disambiguate_term_option metasenv trans in + !lexicon_status_ref, metasenv, + GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) let disambiguate_macro lexicon_status_ref metasenv context (text,prefix_len, macro) diff --git a/components/grafite_parser/grafiteDisambiguate.mli b/components/grafite_parser/grafiteDisambiguate.mli index 582ab11ec..f78507042 100644 --- a/components/grafite_parser/grafiteDisambiguate.mli +++ b/components/grafite_parser/grafiteDisambiguate.mli @@ -45,8 +45,8 @@ val disambiguate_command: LexiconEngine.status -> baseuri:string option -> Cic.metasenv -> - (CicNotationPt.obj GrafiteAst.command) Disambiguate.disambiguator_input -> - LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command + ((CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input -> + LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command val disambiguate_macro: LexiconEngine.status ref -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index ab15311df..19f9e359e 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -573,6 +573,15 @@ EXTEND | IDENT "default" ; what = QSTRING ; uris = LIST1 URI -> let uris = List.map UriManager.uri_of_string uris in GrafiteAst.Default (loc,what,uris) + | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ; + refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ; + refl = tactic_term -> refl ] ; + sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ; + sym = tactic_term -> sym ] ; + trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ; + trans = tactic_term -> trans ] ; + "as" ; id = IDENT -> + GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) ]]; lexicon_command: [ [ IDENT "alias" ; spec = alias_spec -> diff --git a/components/tactics/.depend b/components/tactics/.depend index ea22a46d7..380c50f51 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -163,8 +163,10 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \ primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \ primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi -setoids.cmo: proofEngineTypes.cmi setoids.cmi -setoids.cmx: proofEngineTypes.cmx setoids.cmi +setoids.cmo: proofEngineTypes.cmi primitiveTactics.cmi equalityTactics.cmi \ + setoids.cmi +setoids.cmx: proofEngineTypes.cmx primitiveTactics.cmx equalityTactics.cmx \ + setoids.cmi fourier.cmo: fourier.cmi fourier.cmx: fourier.cmi fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ @@ -185,16 +187,16 @@ statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ statefulProofEngine.cmi statefulProofEngine.cmx: proofEngineTypes.cmx history.cmx \ statefulProofEngine.cmi -tactics.cmo: variousTactics.cmi tacticals.cmi paramodulation/saturation.cmi \ - ring.cmi reductionTactics.cmi proofEngineStructuralRules.cmi \ - primitiveTactics.cmi negationTactics.cmi inversion.cmi \ - introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ +tactics.cmo: variousTactics.cmi tacticals.cmi setoids.cmi \ + paramodulation/saturation.cmi ring.cmi reductionTactics.cmi \ + proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \ + inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \ autoTactic.cmi tactics.cmi -tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \ - ring.cmx reductionTactics.cmx proofEngineStructuralRules.cmx \ - primitiveTactics.cmx negationTactics.cmx inversion.cmx \ - introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ +tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx \ + paramodulation/saturation.cmx ring.cmx reductionTactics.cmx \ + proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \ + inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \ diff --git a/components/tactics/setoids.ml b/components/tactics/setoids.ml index 5729b3ace..f81fe99ef 100644 --- a/components/tactics/setoids.ml +++ b/components/tactics/setoids.ml @@ -74,14 +74,14 @@ let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c (*COQ let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s -*) let constant dir s = assert false +*) let constant dir s = Cic.Implicit None (*COQ let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s -*) let gen_constant dir s = assert false +*) let gen_constant dir s = Cic.Implicit None (*COQ let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s let eval_reference dir s = EvalConstRef (destConst (constant dir s)) -*) let eval_reference dir s = assert false +*) let eval_reference dir s = Cic.Implicit None (*COQ let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s)) *) @@ -91,7 +91,7 @@ let current_constant id = try global_reference id with Not_found -> - anomaly ("Setoid: cannot find " ^ (string_of_id id)) + anomaly ("Setoid: cannot find " ^ id) *) let current_constant id = assert false (* From Setoid.v *) @@ -265,7 +265,7 @@ let find_relation_class rel = (*COQ let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff)) let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl)) -*) let coq_iff_relation = assert false let coq_impl_relation = assert false +*) let coq_iff_relation = Obj.magic 0 let coq_impl_relation = Obj.magic 0 let relation_morphism_of_constr_morphism = let relation_relation_class_of_constr_relation_class = @@ -288,9 +288,7 @@ let equiv_list () = (* Declare a new type of object in the environment : "relation-theory". *) -(*COQ -let (relation_to_obj, obj_to_relation)= - let cache_set (_,(s, th)) = +let relation_to_obj (s, th) = let th' = if relation_table_mem s then begin @@ -299,8 +297,8 @@ let (relation_to_obj, obj_to_relation)= {th with rel_sym = match th.rel_sym with None -> old_relation.rel_sym - | Some t -> Some t} in -(*COQ + | Some t -> Some t} + in prerr_endline ("Warning: The relation " ^ prrelation th' ^ " is redeclared. The new declaration" ^ @@ -327,22 +325,12 @@ let (relation_to_obj, obj_to_relation)= (if old_relation.rel_refl <> None && old_relation.rel_sym <> None then ")" else "") ^ "."); -*) th' end else th in relation_table_add (s,th') - and export_set x = Some x - in - declare_object {(default_object "relation-theory") with - cache_function = cache_set; - load_function = (fun i o -> cache_set o); - subst_function = subst_set; - classify_function = (fun (_,x) -> Substitute x); - export_function = export_set} -*) (******************************* Table of declared morphisms ********************) @@ -901,13 +889,15 @@ let new_named_morphism id m sign = (************************** Adding a relation to the database *********************) +let check_a a = (*COQ -let check_a env a = let typ = Typing.type_of env Evd.empty a in let a_quantifiers_rev,_ = Reduction.dest_arity env typ in a_quantifiers_rev +*) assert false -let check_eq env a_quantifiers_rev a aeq = +let check_eq a_quantifiers_rev a aeq = +(*COQ let typ = Sign.it_mkProd_or_LetIn (Cic.Appl [coq_relation ; apply_to_rels a a_quantifiers_rev]) @@ -918,8 +908,10 @@ let check_eq env a_quantifiers_rev a aeq = then raise (ProofEngineTypes.Fail (lazy (CicPp.ppterm aeq ^ " should have type (" ^ CicPp.ppterm typ ^ ")"))) +*) (assert false : unit) -let check_property env a_quantifiers_rev a aeq strprop coq_prop t = +let check_property a_quantifiers_rev a aeq strprop coq_prop t = +(*COQ if not (is_conv env Evd.empty (Typing.type_of env Evd.empty t) @@ -931,23 +923,27 @@ let check_property env a_quantifiers_rev a aeq strprop coq_prop t = then raise (ProofEngineTypes.Fail (lazy ("Not a valid proof of " ^ strprop ^ "."))) +*) assert false -let check_refl env a_quantifiers_rev a aeq refl = - check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl +let check_refl a_quantifiers_rev a aeq refl = + check_property a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl -let check_sym env a_quantifiers_rev a aeq sym = - check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetric sym +let check_sym a_quantifiers_rev a aeq sym = + check_property a_quantifiers_rev a aeq "symmetry" coq_symmetric sym -let check_trans env a_quantifiers_rev a aeq trans = - check_property env a_quantifiers_rev a aeq "transitivity" coq_transitive trans +let check_trans a_quantifiers_rev a aeq trans = + check_property a_quantifiers_rev a aeq "transitivity" coq_transitive trans +;; let int_add_relation id a aeq refl sym trans = +(*COQ let env = Global.env () in - let a_quantifiers_rev = check_a env a in - check_eq env a_quantifiers_rev a aeq ; - option_iter (check_refl env a_quantifiers_rev a aeq) refl ; - option_iter (check_sym env a_quantifiers_rev a aeq) sym ; - option_iter (check_trans env a_quantifiers_rev a aeq) trans ; +*) + let a_quantifiers_rev = check_a a in + check_eq a_quantifiers_rev a aeq ; + HExtlib.iter_option (check_refl a_quantifiers_rev a aeq) refl ; + HExtlib.iter_option (check_sym a_quantifiers_rev a aeq) sym ; + HExtlib.iter_option (check_trans a_quantifiers_rev a aeq) trans ; let quantifiers_no = List.length a_quantifiers_rev in let aeq_rel = { rel_a = a; @@ -966,18 +962,20 @@ let int_add_relation id a aeq refl sym trans = cic_relation_class_of_X_relation (Cic.Rel 2) (Cic.Rel 1) (apply_to_relation subst aeq_rel) in let _ = +(*COQ Declare.declare_internal_constant id (DefinitionEntry {const_entry_body = Sign.it_mkLambda_or_LetIn x_relation_class - ([ Name (id_of_string "v"),None,Cic.Rel 1; - Name (id_of_string "X"),None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @ + ([ Name "v",None,Cic.Rel 1; + Name "X",None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @ a_quantifiers_rev); const_entry_type = None; const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, IsDefinition Definition) in - let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in +*) () in + let id_precise = id ^ "_precise_relation_class" in let xreflexive_relation_class = let subst = let len = List.length a_quantifiers_rev in @@ -985,6 +983,7 @@ let int_add_relation id a aeq refl sym trans = in cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in let _ = +(*COQ Declare.declare_internal_constant id_precise (DefinitionEntry {const_entry_body = @@ -993,16 +992,17 @@ let int_add_relation id a aeq refl sym trans = const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions() }, IsDefinition Definition) in +*) () in let aeq_rel = { aeq_rel with rel_X_relation_class = current_constant id; rel_Xreflexive_relation_class = current_constant id_precise } in - Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; - Options.if_verbose prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation"); + relation_to_obj (aeq, aeq_rel) ; + prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation"); match trans with None -> () | Some trans -> - let mor_name = id_of_string (string_of_id id ^ "_morphism") in + let mor_name = id ^ "_morphism" in let a_instance = apply_to_rels a a_quantifiers_rev in let aeq_instance = apply_to_rels aeq a_quantifiers_rev in let sym_instance = @@ -1042,6 +1042,7 @@ let int_add_relation id a aeq refl sym trans = trans_instance], coq_iff_relation in let _ = +(*COQ Declare.declare_internal_constant mor_name (DefinitionEntry {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; @@ -1049,20 +1050,17 @@ let int_add_relation id a aeq refl sym trans = const_entry_opaque = false; const_entry_boxed = Options.boxed_definitions()}, IsDefinition Definition) +*) () in let a_quantifiers_rev = List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in add_morphism None mor_name (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2], output) -*) (* The vernac command "Add Relation ..." *) let add_relation id a aeq refl sym trans = -(*COQ - int_add_relation id (constr_of a) (constr_of aeq) (HExtlib.map_option constr_of refl) - (HExtlib.map_option constr_of sym) (HExtlib.map_option constr_of trans) -*) assert false + int_add_relation id a aeq refl sym trans (****************************** The tactic itself *******************************) @@ -1816,37 +1814,47 @@ let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) = (* [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let setoid_reflexivity (*COQgl*) = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_reflexivity" - [] ((*COQ pf_concl gl*) assert false) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_refl with - None -> - raise (ProofEngineTypes.Fail (lazy - ("The relation " ^ prrelation rel ^ " is not reflexive."))) - | Some refl -> (*COQ apply refl gl*) assert false - with - Optimize -> (*COQ reflexivity gl*) assert false +let setoid_reflexivity_tac = + let tac ((proof,goal) as status) = + let (_,metasenv,_,_) = proof in + let metano,context,ty = CicUtil.lookup_meta goal metasenv in + try + let relation_class = + relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in + match relation_class with + Leibniz _ -> assert false (* since [] is empty *) + | Relation rel -> + match rel.rel_refl with + None -> + raise (ProofEngineTypes.Fail (lazy + ("The relation " ^ prrelation rel ^ " is not reflexive."))) + | Some refl -> + ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl) + status + with + Optimize -> + ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status + in + ProofEngineTypes.mk_tactic tac -let setoid_symmetry (*COQgl*) = - try - let relation_class = - relation_class_that_matches_a_constr "Setoid_symmetry" - [] ((*COQ pf_concl gl*) assert false) in - match relation_class with - Leibniz _ -> assert false (* since [] is empty *) - | Relation rel -> - match rel.rel_sym with - None -> - raise (ProofEngineTypes.Fail (lazy - ("The relation " ^ prrelation rel ^ " is not symmetric."))) - | Some sym -> (*COQ apply sym gl*) assert false - with - Optimize -> (*COQ symmetry gl*) assert false +let setoid_symmetry = + let tac status = + try + let relation_class = + relation_class_that_matches_a_constr "Setoid_symmetry" + [] ((*COQ pf_concl gl*) assert false) in + match relation_class with + Leibniz _ -> assert false (* since [] is empty *) + | Relation rel -> + match rel.rel_sym with + None -> + raise (ProofEngineTypes.Fail (lazy + ("The relation " ^ prrelation rel ^ " is not symmetric."))) + | Some sym -> (*COQ apply sym gl*) assert false + with + Optimize -> (*COQ symmetry gl*) assert false + in + ProofEngineTypes.mk_tactic tac let setoid_symmetry_in id (*COQgl*) = (*COQ diff --git a/components/tactics/setoids.mli b/components/tactics/setoids.mli index 4c5d655cb..abe71f4eb 100644 --- a/components/tactics/setoids.mli +++ b/components/tactics/setoids.mli @@ -54,7 +54,7 @@ val general_s_rewrite : bool -> Cic.term -> new_goals:Cic.term list -> ProofEngi val general_s_rewrite_in : string -> bool -> Cic.term -> new_goals:Cic.term list -> ProofEngineTypes.tactic -val setoid_reflexivity : ProofEngineTypes.tactic +val setoid_reflexivity_tac : ProofEngineTypes.tactic val setoid_symmetry : ProofEngineTypes.tactic val setoid_symmetry_in : string -> ProofEngineTypes.tactic val setoid_transitivity : Cic.term -> ProofEngineTypes.tactic diff --git a/components/tactics/tactics.ml b/components/tactics/tactics.ml index 5a2cc0e16..dfca1c908 100644 --- a/components/tactics/tactics.ml +++ b/components/tactics/tactics.ml @@ -57,7 +57,7 @@ let left = IntroductionTactics.left_tac let letin = PrimitiveTactics.letin_tac let normalize = ReductionTactics.normalize_tac let reduce = ReductionTactics.reduce_tac -let reflexivity = EqualityTactics.reflexivity_tac +let reflexivity = Setoids.setoid_reflexivity_tac let replace = EqualityTactics.replace_tac let rewrite = EqualityTactics.rewrite_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac diff --git a/matita/dump_moo.ml b/matita/dump_moo.ml index 05c21d40d..54eaea4ba 100644 --- a/matita/dump_moo.ml +++ b/matita/dump_moo.ml @@ -51,7 +51,9 @@ let _ = List.iter (fun cmd -> printf " %s\n%!" - (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) cmd)) + (GrafiteAstPp.pp_command + ~term_pp:(fun _ -> assert false) + ~obj_pp:(fun _ -> assert false) cmd)) commands; end) (List.rev !moos) diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma index 3567dd915..b91a59e17 100644 --- a/matita/library/datatypes/constructors.ma +++ b/matita/library/datatypes/constructors.ma @@ -17,6 +17,8 @@ include "logic/equality.ma". inductive void : Set \def. +inductive unit : Set ≝ something: unit. + inductive Prod (A,B:Set) : Set \def pair : A \to B \to Prod A B. diff --git a/matita/library/logic/equality.ma b/matita/library/logic/equality.ma index c26449c42..0561fb993 100644 --- a/matita/library/logic/equality.ma +++ b/matita/library/logic/equality.ma @@ -62,7 +62,7 @@ qed. theorem eq_f: \forall A,B:Type.\forall f:A\to B. \forall x,y:A. x=y \to f x = f y. -intros.elim H.reflexivity. +intros.elim H.apply refl_eq. qed. coercion cic:/matita/logic/equality/sym_eq.con. diff --git a/matita/library/nat/exp.ma b/matita/library/nat/exp.ma index 11d84f74c..e40844e3f 100644 --- a/matita/library/nat/exp.ma +++ b/matita/library/nat/exp.ma @@ -54,7 +54,7 @@ apply le_times.assumption.assumption. qed. theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m. -intros.elim m.simplify.unfold lt.reflexivity. +intros.elim m.simplify.unfold lt.apply le_n. simplify.unfold lt. apply (trans_le ? ((S(S O))*(S n1))). simplify. diff --git a/matita/library/nat/gcd.ma b/matita/library/nat/gcd.ma index 2bb22081f..6ce4f538e 100644 --- a/matita/library/nat/gcd.ma +++ b/matita/library/nat/gcd.ma @@ -413,7 +413,7 @@ symmetric_gcd. theorem le_gcd_times: \forall m,n,p:nat. O< p \to gcd m n \le gcd m (n*p). intros. -apply (nat_case n).reflexivity. +apply (nat_case n).apply le_n. intro. apply divides_to_le. apply lt_O_gcd. diff --git a/matita/library/nat/primes.ma b/matita/library/nat/primes.ma index 30339d654..c5fe7bd29 100644 --- a/matita/library/nat/primes.ma +++ b/matita/library/nat/primes.ma @@ -416,8 +416,8 @@ qed. theorem le_smallest_factor_n : \forall n:nat. smallest_factor n \le n. -intro.apply (nat_case n).simplify.reflexivity. -intro.apply (nat_case m).simplify.reflexivity. +intro.apply (nat_case n).simplify.apply le_n. +intro.apply (nat_case m).simplify.apply le_n. intro.apply divides_to_le. unfold lt.apply le_S_S.apply le_O_n. apply divides_smallest_factor_n. diff --git a/matita/matita.ml b/matita/matita.ml index 6e9fa5f23..609a014d0 100644 --- a/matita/matita.ml +++ b/matita/matita.ml @@ -146,8 +146,11 @@ let _ = let moo = grafite_status.moo_content_rev in List.iter (fun cmd -> - prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false) - cmd)) + prerr_endline + (GrafiteAstPp.pp_command + ~term_pp:(fun _ -> assert false) + ~obj_pp:(fun _ -> assert false) + cmd)) (List.rev moo)); addDebugItem "print metasenv goals and stack to stderr" (fun _ ->