(** 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
| _ -> 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 *)
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
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
'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) ->
(* $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"
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)
* 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
(* $Id$ *)
-module GT = GrafiteTypes
-
open Printf
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
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
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)
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
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)
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
| (name,true,arity) ->
Some
(arity, UriManager.uri_of_string
- (GT.qualify status name ^ ".con"))
+ (GrafiteTypes.qualify status name ^ ".con"))
| _ -> None)
fields
in
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 =
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
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
(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
(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
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
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 ->
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)
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 ->
| 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 ->
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 \
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 \
(*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))
*)
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 *)
(*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 =
(* 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
{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" ^
(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 ********************)
(************************** 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])
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)
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;
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
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 =
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 =
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;
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 *******************************)
(* [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
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
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
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)
inductive void : Set \def.
+inductive unit : Set ≝ something: unit.
+
inductive Prod (A,B:Set) : Set \def
pair : A \to B \to Prod A B.
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.
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.
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.
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.
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 _ ->
projects / helm.git / commitdiff