let pp_fields fields =
(if fields <> [] then "\n" else "") ^
String.concat ";\n"
- (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term ty) fields)
+ (List.map
+ (fun (name,ty,coercion) ->
+ " " ^ name ^ if coercion then ":>" else ": " ^ pp_term ty) fields)
let pp_obj = function
| Ast.Inductive (params, types) ->
* - body is present when its given along with the command, otherwise it
* will be given in proof editing mode using the tactical language
*)
- | Record of (string * term) list * string * term * (string * term) list
+ | Record of (string * term) list * string * term * (string * term * bool) list
(** left parameters, name, type, fields *)
(** {2 Standard precedences} *)
let index = ref 0 in
let freshen_term = freshen_term ~index in
let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
+ let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
match obj with
| CicNotationPt.Inductive (params, indtypes) ->
let indtypes =
CicNotationPt.Theorem (flav, n, freshen_term t, ty_opt)
| CicNotationPt.Record (params, n, ty, fields) ->
CicNotationPt.Record (freshen_name_ty params, n, freshen_term ty,
- freshen_name_ty fields)
+ freshen_name_ty_b fields)
let freshen_term = freshen_term ?index:None
deannotate.cmx: cic.cmx deannotate.cmi
cicParser.cmo: deannotate.cmi cicUniv.cmi cic.cmo cicParser.cmi
cicParser.cmx: deannotate.cmx cicUniv.cmx cic.cmx cicParser.cmi
-cicUtil.cmo: cic.cmo cicUtil.cmi
-cicUtil.cmx: cic.cmx cicUtil.cmi
+cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi
+cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi
helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi
helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi
libraryObjects.cmo: helmLibraryObjects.cmi libraryObjects.cmi
[ `Coercion
| `Elim of sort (** elimination principle; if sort is Type, the universe is
* not relevant *)
- | `Record of string list (** inductive type that encodes a record;
- the arguments are the record fields *)
+ | `Record of (string * bool) list (**
+ inductive type that encodes a record; the arguments are
+ the record fields names and if they are coercions *)
| `Projection (** record projection *)
]
let fields =
List.map
(function
- | Obj_field name -> name
+ | Obj_field name ->
+ (match Str.split (Str.regexp " ") name with
+ | [name] -> name, false
+ | [name;"coercion"] -> name,true
+ | _ ->
+ parse_error
+ "wrong \"field\"'s name attribute")
| _ ->
parse_error
"unexpected extra content for \"record\" object class")
| Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest
| Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest
| Cic.Appl l ->
- List.fold_right (fun x i -> i && is_meta_closed x) l true
+ not (List.exists (fun x -> not (is_meta_closed x)) l)
| Cic.Var (_,exp_named_subst)
| Cic.Const (_,exp_named_subst)
| Cic.MutInd (_,_,exp_named_subst)
| Cic.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right (fun (_,x) i -> i && is_meta_closed x)
- exp_named_subst true
+ not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst)
| Cic.MutCase (_,_,out,te,pl) ->
is_meta_closed out && is_meta_closed te &&
- List.fold_right (fun x i -> i && is_meta_closed x) pl true
+ not (List.exists (fun x -> not (is_meta_closed x)) pl)
| Cic.Fix (_,fl) ->
- List.fold_right
- (fun (_,_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo
- ) fl true
+ not (List.exists
+ (fun (_,_,ty,bo) ->
+ not (is_meta_closed ty) || not (is_meta_closed bo))
+ fl)
| Cic.CoFix (_,fl) ->
- List.fold_right
- (fun (_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo
- ) fl true
+ not (List.exists
+ (fun (_,ty,bo) ->
+ not (is_meta_closed ty) || not (is_meta_closed bo))
+ fl)
;;
let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
(**** TABLES ****)
+let default_eq_URIs =
+ [HelmLibraryObjects.Logic.eq_URI,
+ HelmLibraryObjects.Logic.sym_eq_URI,
+ HelmLibraryObjects.Logic.trans_eq_URI,
+ HelmLibraryObjects.Logic.eq_ind_URI,
+ HelmLibraryObjects.Logic.eq_ind_r_URI];;
+
+let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
+let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
+let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
+
(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
let eq_URIs_ref =
ref [HelmLibraryObjects.Logic.eq_URI,
absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
| _,_ -> raise NotRecognized
+let reset_defaults () =
+ eq_URIs_ref := default_eq_URIs;
+ true_URIs_ref := default_true_URIs;
+ false_URIs_ref := default_false_URIs;
+ absurd_URIs_ref := default_absurd_URIs
+
(**** LOOKUP FUNCTIONS ****)
let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
*)
val set_default : string -> UriManager.uri list -> unit
+val reset_defaults : unit -> unit
val eq_URI : unit -> UriManager.uri
val false_URI : unit -> UriManager.uri
val true_URI : unit -> UriManager.uri
val absurd_URI : unit -> UriManager.uri
+
| `Record field_names ->
Xml.xml_nempty "class" [None,"value","record"]
(List.fold_right
- (fun name res ->
- [< Xml.xml_empty "field" [None,"name",name]; res >]
+ (fun (name,coercion) res ->
+ [< Xml.xml_empty "field"
+ [None,"name",if coercion then name ^ " coercion" else name];
+ res >]
) field_names [<>])
| `Projection -> Xml.xml_empty "class" [None,"value","projection"]
in
let fields' =
snd (
List.fold_left
- (fun (context,res) (name,ty) ->
+ (fun (context,res) (name,ty,_coercion) ->
let context' = Cic.Name name :: context in
context',(name,interpretate_term context env None false ty)::res
) (context,[]) fields) in
concl fields' in
let con' = add_params con in
let tyl = [name,true,ty',["mk_" ^ name,con']] in
- let field_names = List.map fst fields in
+ let field_names = List.map (fun (x,_,y) -> x,y) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
| CicNotationPt.Record (params,_,ty,fields) ->
let dom =
List.flatten
- (List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
+ (List.rev_map (fun (_,ty,_) -> domain_rev_of_term [] ty) fields) in
let dom =
List.filter
(fun name->
not ( List.exists (fun (name',_) -> name = Id name') params
- || List.exists (fun (name',_) -> name = Id name') fields)
+ || List.exists (fun (name',_,_) -> name = Id name') fields)
) dom
in
List.fold_left
exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;
+let insert_coercions = ref true
+
let debug_print = fun _ -> ()
let profiler = HExtlib.profile "CicRefine.fo_unif"
| _ -> assert false
;;
+
let rec type_of_constant uri ugraph =
let module C = Cic in
let module R = CicReduction in
let coerce_to_sort in_source tgt_sort t type_to_coerce
subst context metasenv uragph
=
- let coercion_src = carr type_to_coerce subst context in
- match coercion_src with
- | Cic.Sort _ ->
- t,type_to_coerce,subst,metasenv,ugraph
- | Cic.Meta _ as meta ->
- t, meta, subst, metasenv, ugraph
- | Cic.Cast _ as cast ->
- t, cast, subst, metasenv, ugraph
- | term ->
- let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
- (match boh with
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl t
- (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl t
- (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst t context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph)
+ if not !insert_coercions then
+ t,type_to_coerce,subst,metasenv,ugraph
+ else
+ let coercion_src = carr type_to_coerce subst context in
+ match coercion_src with
+ | Cic.Sort _ ->
+ t,type_to_coerce,subst,metasenv,ugraph
+ | Cic.Meta _ as meta ->
+ t, meta, subst, metasenv, ugraph
+ | Cic.Cast _ as cast ->
+ t, cast, subst, metasenv, ugraph
+ | term ->
+ let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ (match boh with
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl t
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl t
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst t context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.SomeCoercion c ->
+ let newt, tty, subst, metasenv, ugraph =
+ avoid_double_coercion
+ subst metasenv ugraph
+ (Cic.Appl[c;t]) coercion_tgt
+ in
+ newt, tty, subst, metasenv, ugraph)
in
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph
let s',sort1,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context s ugraph in
- let s',sort1 =
- match CicReduction.whd ~subst:subst' context sort1 with
- C.Meta _
- | C.Sort _ -> s',sort1
- | coercion_src ->
- let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh ())) in
- let search = CoercGraph.look_for_coercion in
- let boh = search coercion_src coercion_tgt in
- match boh with
- | CoercGraph.SomeCoercion c ->
- Cic.Appl [c;s'], coercion_tgt
- | CoercGraph.NoCoercion
- | CoercGraph.NotHandled _ ->
- enrich localization_tbl s'
- (RefineFailure (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
- | CoercGraph.NotMetaClosed ->
- enrich localization_tbl s'
- (Uncertain (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst s' context ^ " is not a type since it has type " ^ CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort")))
+ let s',sort1,subst',metasenv',ugraph1 =
+ if not !insert_coercions then
+ s',sort1, subst', metasenv', ugraph1
+ else
+ match CicReduction.whd ~subst:subst' context sort1 with
+ | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1
+ | coercion_src ->
+ let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in
+ let search = CoercGraph.look_for_coercion in
+ let boh = search coercion_src coercion_tgt in
+ match boh with
+ | CoercGraph.SomeCoercion c ->
+ let newt, tty, subst', metasenv', ugraph1 =
+ avoid_double_coercion
+ subst' metasenv' ugraph1
+ (Cic.Appl[c;s']) coercion_tgt
+ in
+ newt, tty, subst', metasenv', ugraph1
+ | CoercGraph.NoCoercion
+ | CoercGraph.NotHandled _ ->
+ enrich localization_tbl s'
+ (RefineFailure
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
+ | CoercGraph.NotMetaClosed ->
+ enrich localization_tbl s'
+ (Uncertain
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst s' context ^
+ " is not a type since it has type " ^
+ CicMetaSubst.ppterm_in_context
+ subst coercion_src context ^ " that is not a sort")))
in
let context_for_t = ((Some (n,(C.Decl s')))::context) in
let t',type2,subst'',metasenv'',ugraph2 =
eat_prods true subst'' metasenv'' context
hetype tlbody_and_type ugraph2
in
- C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
+ avoid_double_coercion
+ subst''' metasenv''' ugraph3 (C.Appl (he'::tl')) applty
| C.Appl _ -> assert false
| C.Const (uri,exp_named_subst) ->
let exp_named_subst',subst',metasenv',ugraph1 =
relocalize localization_tbl t t';
res
+ and avoid_double_coercion subst metasenv ugraph t ty =
+ match t with
+ | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
+ CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CicMetaSubst.apply_subst subst ty in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c ->
+ Cic.Appl [ c ; head ], ty, subst,metasenv,ugraph
+ | _ -> assert false) (* the composite coercion must exist *)
+ | _ -> t, ty, subst, metasenv, ugraph
+
(* check_metasenv_consistency checks that the "canonical" context of a
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
fo_unif_subst subst context metasenv hety s ugraph
in
hete,subst,metasenv,ugraph1
- with exn when allow_coercions ->
+ with exn when allow_coercions && !insert_coercions ->
(* we search a coercion from hety to s *)
- let coer =
+ let coer, tgt_carr =
let carr t subst context =
CicMetaSubst.apply_subst subst t
in
let c_hety = carr hety subst context in
let c_s = carr s subst context in
- CoercGraph.look_for_coercion c_hety c_s
+ CoercGraph.look_for_coercion c_hety c_s, c_s
in
match coer with
| CoercGraph.NoCoercion
CicMetaSubst.ppterm_in_context subst s context
(* "\nReason: " ^ Lazy.force e*))))
| CoercGraph.SomeCoercion c ->
- (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph
+ let newt, _, subst, metasenv, ugraph =
+ avoid_double_coercion
+ subst metasenv ugraph
+ (Cic.Appl[c;hete]) tgt_carr
+ in
+ newt, subst, metasenv, ugraph
in
let coerced_args,metasenv',subst',t',ugraph2 =
eat_prods metasenv subst context
localization_tbl:Token.flocation Cic.CicHash.t ->
Cic.metasenv -> UriManager.uri option -> Cic.obj ->
Cic.obj * Cic.metasenv * CicUniv.universe_graph
+
+val insert_coercions: bool ref (* initially true *)
+
boxPp.cmi
boxPp.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
boxPp.cmi
-content2pres.cmo: renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi \
- box.cmi content2pres.cmi
-content2pres.cmx: renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx \
- box.cmx content2pres.cmi
-sequent2pres.cmo: mpresentation.cmi cicNotationPres.cmi box.cmi \
- sequent2pres.cmi
-sequent2pres.cmx: mpresentation.cmx cicNotationPres.cmx box.cmx \
- sequent2pres.cmi
+content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \
+ cicNotationPres.cmi box.cmi content2pres.cmi
+content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
+ cicNotationPres.cmx box.cmx content2pres.cmi
+sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \
+ box.cmi sequent2pres.cmi
+sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \
+ box.cmx sequent2pres.cmi
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
+let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
+ sprintf "interpretation \"%s\" '%s %s = %s"
+ dsc symbol
+ (String.concat " " (List.map pp_argument_pattern arg_patterns))
+ (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
+
+let pp_default what uris =
+ sprintf "default \"%s\" %s" what
+ (String.concat " " (List.map UriManager.string_of_uri uris))
+
+let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
+ sprintf "notation %s\"%s\" %s %s for %s"
+ (pp_dir_opt dir_opt)
+ (pp_l1_pattern l1_pattern)
+ (pp_associativity assoc)
+ (pp_precedence prec)
+ (pp_l2_pattern l2_pattern)
+
+let pp_coercion_ast term do_composites =
+ sprintf "coercion %s (* %s *)" (pp_term_ast term)
+ (if do_composites then "compounds" else "no compounds")
+
+let pp_coercion_cic term do_composites =
+ sprintf "coercion %s (* %s *)" (pp_term_cic term)
+ (if do_composites then "compounds" else "no compounds")
+
let pp_command = function
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
| Drop _ -> "drop"
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
- | Coercion (_,term, _do_composites) ->
- sprintf "coercion %s" (pp_term_ast term)
+ | Coercion (_,term, do_composites) ->
+ pp_coercion_ast term do_composites
| Alias (_,s) -> pp_alias s
| Obj (_,obj) -> CicNotationPp.pp_obj obj
| Default (_,what,uris) ->
- sprintf "default \"%s\" %s" what
- (String.concat " " (List.map UriManager.string_of_uri uris))
+ pp_default what uris
| Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
- sprintf "interpretation \"%s\" '%s %s = %s"
- dsc symbol
- (String.concat " " (List.map pp_argument_pattern arg_patterns))
- (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
+ pp_interpretation dsc symbol arg_patterns cic_appl_pattern
| Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
- sprintf "notation %s\"%s\" %s %s for %s"
- (pp_dir_opt dir_opt)
- (pp_l1_pattern l1_pattern)
- (pp_associativity assoc)
- (pp_precedence prec)
- (pp_l2_pattern l2_pattern)
+ pp_notation dir_opt l1_pattern assoc prec l2_pattern
| Render _
| Dump _ -> assert false (* ZACK: debugging *)
| Executable (_, ex) -> pp_executable ex
| Comment (_, c) -> pp_comment c
+
+
let pp_cic_command = function
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
| Drop _ -> "drop"
- | Coercion (_,term,_add_composites) ->
- sprintf "coercion %s" (CicPp.ppterm term)
- | Set _
- | Alias _
- | Default _
- | Render _
- | Dump _
- | Interpretation _
- | Notation _
- | Obj _ -> assert false (* not implemented *)
+ | Coercion (_,term, do_composites) ->
+ pp_coercion_cic term do_composites
+ | Obj (_,obj) -> CicPp.ppobj obj
+ | Set _-> assert false (* not implemented *)
+ | Alias (_, alias) -> pp_alias alias
+ | Default (_,what,uris) ->
+ pp_default what uris
+ | Render _ -> assert false (* not implemented *)
+ | Dump _ -> assert false (* not implemented *)
+ | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
+ pp_interpretation dsc symbol arg_patterns cic_appl_pattern
+ | Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
+ pp_notation dir_opt l1_pattern assoc prec l2_pattern
let pp_dependency = function
| IncludeDep str -> "include \"" ^ str ^ "\""
let add_coercion status ~add_composites uri =
let basedir = Helm_registry.get "matita.basedir" in
- let lemmas = CoercGraph.add_coercion ~basedir ~add_composites uri in
- let status = {status with coercions = uri :: status.coercions} in
+ let compounds = CoercGraph.add_coercion uri in
+ let status =
+ if add_composites then
+ (List.iter (fun (u,_) ->
+ prerr_endline (UriManager.string_of_uri u)) compounds;
+ List.fold_left (fun s (uri,o) -> add_obj uri o s) status compounds )
+ else
+ status
+ in
+ let status =
+ {status with coercions = uri :: List.map fst compounds @ status.coercions}
+ in
let statement_of name =
- GrafiteAst.Coercion
- (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in
+ GrafiteAst.Coercion
+ (DisambiguateTypes.dummy_floc, CicUtil.term_of_uri uri, false) in
let moo_content = [statement_of (UriManager.name_of_uri uri)] in
let status = GrafiteTypes.add_moo_content moo_content status in
- List.fold_left add_alias_for_constant status lemmas
+ List.fold_left add_alias_for_constant status (List.map fst compounds)
module OrderedUri =
struct
in
let debug_list = ref [] in
List.iter
- (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri))
+ (fun uri -> CoercGraph.remove_coercion uri)
coercions_to_remove;
List.iter LibrarySync.remove_obj objs_to_remove;
List.iter CicNotation.remove_notation notation_to_remove
+
+let init () =
+ CoercGraph.remove_all ();
+ LibraryObjects.reset_defaults ();
+ {
+ aliases = DisambiguateTypes.Environment.empty;
+ multi_aliases = DisambiguateTypes.Environment.empty;
+ moo_content_rev = [];
+ metadata = [];
+ proof_status = No_proof;
+ options = no_options;
+ objects = [];
+ coercions = [];
+ notation_ids = [];
+ }
+
+
GrafiteTypes.status ->
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
GrafiteTypes.status
+
+ (* also resets the imperative part of the status *)
+val init: unit -> GrafiteTypes.status
+
+
matitaDisambiguator.cmx: matitaDisambiguator.cmi
grafiteDisambiguate.cmo: matitaDisambiguator.cmi grafiteDisambiguate.cmi
grafiteDisambiguate.cmx: matitaDisambiguator.cmx grafiteDisambiguate.cmi
-grafiteParserMisc.cmo: grafiteParserMisc.cmi
-grafiteParserMisc.cmx: grafiteParserMisc.cmi
+grafiteParserMisc.cmo: grafiteParser.cmi grafiteParserMisc.cmi
+grafiteParserMisc.cmx: grafiteParser.cmx grafiteParserMisc.cmi
name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
fields = LIST0 [
- name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty)
+ name = IDENT ;
+ coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ;
+ ty = term -> (name,ty,coercion)
] SEP SYMBOL ";"; SYMBOL "}" ->
let params =
List.fold_right
(true, library, true);
]
in
- let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
- CoercDb.use_coercions := use_coercions;
+ let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
+ CicRefine.insert_coercions := insert_coercions;
f ~fresh_instances ~aliases ~universe thing
in
let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
aux (errors @ [newerrors]) tl)
| [] -> assert false
in
- let saved_use_coercions = !CoercDb.use_coercions in
+ let saved_insert_coercions = !CicRefine.insert_coercions in
try
let res = aux [] passes in
- CoercDb.use_coercions := saved_use_coercions;
+ CicRefine.insert_coercions := saved_insert_coercions;
res
with exn ->
- CoercDb.use_coercions := saved_use_coercions;
+ CicRefine.insert_coercions := saved_insert_coercions;
raise exn
type disambiguator_thing =
libraryDb.cmx: libraryDb.cmi
coercDb.cmo: coercDb.cmi
coercDb.cmx: coercDb.cmi
-librarySync.cmo: libraryDb.cmi coercDb.cmi cicRecord.cmi cicElim.cmi \
+coercGraph.cmo: coercDb.cmi coercGraph.cmi
+coercGraph.cmx: coercDb.cmx coercGraph.cmi
+librarySync.cmo: libraryDb.cmi coercGraph.cmi cicRecord.cmi cicElim.cmi \
librarySync.cmi
-librarySync.cmx: libraryDb.cmx coercDb.cmx cicRecord.cmx cicElim.cmx \
+librarySync.cmx: libraryDb.cmx coercGraph.cmx cicRecord.cmx cicElim.cmx \
librarySync.cmi
-coercGraph.cmo: librarySync.cmi coercDb.cmi coercGraph.cmi
-coercGraph.cmx: librarySync.cmx coercDb.cmx coercGraph.cmi
libraryNoDb.cmo: libraryNoDb.cmi
libraryNoDb.cmx: libraryNoDb.cmi
libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
libraryMisc.mli \
libraryDb.mli \
coercDb.mli \
- librarySync.mli \
coercGraph.mli \
+ librarySync.mli \
libraryNoDb.mli \
libraryClean.mli \
$(NULL)
Cic.Lambda (Cic.Name name,ty,acc)) l start in
let recty = rec_ty uri paramsno in
let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in
- Some
(mk_lambdas params
(Cic.Lambda (Cic.Name "w", recty,
Cic.MutCase (uri,0,outtype, Cic.Rel 1,
Cic.MutInd _, []
| Cic.Appl _, [] -> []
| Cic.Prod (_,s,t), name::tl ->
- (match generate_one_proj uri leftparams paramsno fields s i with
- Some p ->
- let puri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- (puri,name,p) ::
- aux (i - 1)
- (CicSubstitution.subst
- (Cic.Appl
- (Cic.Const (puri,[]) ::
- CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
- ) t, tl)
- | None -> assert false)
+ let p = generate_one_proj uri leftparams paramsno fields s i in
+ let puri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
+ (puri,name,p) ::
+ aux (i - 1)
+ (CicSubstitution.subst
+ (Cic.Appl
+ (Cic.Const (puri,[]) ::
+ CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
+ ) t, tl)
| _,_ -> assert false
in
aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
exception EqCarrOnNonMetaClosed
let db = ref []
-let use_coercions = ref true
let coerc_carr_of_term t =
try
db := List.filter (fun u -> not(p u)) !db
let find_coercion f =
- if !use_coercions then
- List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
- else []
+ List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+
+let is_a_coercion u =
+ List.exists (fun (_,_,x) -> UriManager.eq x u) !db
+
+let get_carr uri =
+ try
+ let src, tgt, _ = List.find (fun (_,_,x) -> UriManager.eq x uri) !db in
+ src, tgt
+ with Not_found -> assert false (* uri must be a coercion *)
* http://cs.unibo.it/helm/.
*)
+
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph **)
+
+
(** XXX WARNING: non-reentrant *)
type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
exception EqCarrNotImplemented of string Lazy.t
val coerc_carr_of_term: Cic.term -> coerc_carr
val name_of_carr: coerc_carr -> string
-val use_coercions: bool ref (** initial status is true *)
-
val to_list:
unit ->
(coerc_carr * coerc_carr * UriManager.uri) list
val remove_coercion:
(coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
-val find_coercion:
+val find_coercion:
(coerc_carr * coerc_carr -> bool) -> UriManager.uri list
+val is_a_coercion: UriManager.uri -> bool
+val get_carr: UriManager.uri -> coerc_carr * coerc_carr
+
+
let term_of_carr = function
| CoercDb.Uri u -> CicUtil.term_of_uri u
- | CoercDb.Sort _ -> assert false
+ | CoercDb.Sort s -> Cic.Sort s
| CoercDb.Term _ -> assert false
(* given a new coercion uri from src to tgt returns
let coercions = CoercDb.to_list () in
let todo_list = get_closure_coercions src tgt uri coercions in
let todo_list = filter_duplicates todo_list coercions in
- let new_coercions, new_coercions_obj =
- List.split (
- List.map (
- fun (src, l , tgt) ->
- match l with
- | [] -> assert false
- | he :: tl ->
- let first_step =
- Cic.Constant ("",
- Some (term_of_carr (CoercDb.Uri he)), Cic.Sort Cic.Prop, [], obj_attrs)
- in
- let o,u =
- List.fold_left (fun (o,univ) coer ->
- match o with
- | Cic.Constant (_,Some c,_,[],_) ->
- generate_composite_closure c (term_of_carr (CoercDb.Uri
- coer)) univ
- | _ -> assert false
- ) (first_step, CicUniv.empty_ugraph) tl
- in
- let name_src = CoercDb.name_of_carr src in
- let name_tgt = CoercDb.name_of_carr tgt in
- let name = name_tgt ^ "_of_" ^ name_src in
- let buri = UriManager.buri_of_uri uri in
- let c_uri =
- UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
- in
- let named_obj =
- match o with
- | Cic.Constant (_,bo,ty,vl,attrs) ->
- Cic.Constant (name,bo,ty,vl,attrs)
+ let new_coercions =
+ List.map (
+ fun (src, l , tgt) ->
+ match l with
+ | [] -> assert false
+ | he :: tl ->
+ let first_step =
+ Cic.Constant ("",
+ Some (term_of_carr (CoercDb.Uri he)),
+ Cic.Sort Cic.Prop, [], obj_attrs)
+ in
+ let o,_ =
+ List.fold_left (fun (o,univ) coer ->
+ match o with
+ | Cic.Constant (_,Some c,_,[],_) ->
+ generate_composite_closure c (term_of_carr (CoercDb.Uri
+ coer)) univ
| _ -> assert false
- in
- ((src,tgt,c_uri),(c_uri,named_obj,u))
- ) todo_list)
+ ) (first_step, CicUniv.empty_ugraph) tl
+ in
+ let name_src = CoercDb.name_of_carr src in
+ let name_tgt = CoercDb.name_of_carr tgt in
+ let name = name_tgt ^ "_of_" ^ name_src in
+ let buri = UriManager.buri_of_uri uri in
+ let c_uri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+ in
+ let named_obj =
+ match o with
+ | Cic.Constant (_,bo,ty,vl,attrs) ->
+ Cic.Constant (name,bo,ty,vl,attrs)
+ | _ -> assert false
+ in
+ ((src,tgt,c_uri,named_obj))
+ ) todo_list
in
- List.iter CoercDb.add_coercion (new_coercions @ [src,tgt,uri]);
- new_coercions_obj
+ new_coercions
;;
let coercion_hashtbl = UriManager.UriHashtbl.create 3
-let add_coercion ~basedir ~add_composites uri =
+let add_coercion uri =
let coer_ty,_ =
CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri uri)
CicUniv.empty_ugraph
let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
let new_coercions = close_coercion_graph src_uri tgt_uri uri in
- let uris = ref [] in
- if add_composites then
- try
- let lemmas =
- List.fold_left
- (fun lemmas (uri,o,_) ->
- let lemmas' = LibrarySync.add_obj ~basedir uri o in
- uris := uri :: !uris;
- uri::lemmas'@lemmas
- ) [] new_coercions;
- in
- UriManager.UriHashtbl.add coercion_hashtbl uri !uris;
- lemmas
- with
- exn ->
- List.iter LibrarySync.remove_obj !uris;
- raise exn
- else
- []
+ UriManager.UriHashtbl.add coercion_hashtbl uri
+ (List.map (fun (_,_,uri,_) -> uri) new_coercions);
+ CoercDb.add_coercion (src_uri,tgt_uri,uri);
+ List.iter
+ (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri))
+ new_coercions;
+ List.map (fun (_,_,uri,o) -> uri,o) new_coercions
+
let remove_coercion uri =
- let uris =
try
let res = UriManager.UriHashtbl.find coercion_hashtbl uri in
UriManager.UriHashtbl.remove coercion_hashtbl uri;
- res
+ CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq uri u);
+ List.iter
+ (fun u ->
+ CoercDb.remove_coercion
+ (fun (_,_,u1) -> UriManager.eq u u1))
+ res;
with
- Not_found -> assert false
- in
- List.iter LibrarySync.remove_obj uris
+ Not_found -> ()
+
+let remove_all () =
+ CoercDb.remove_coercion (fun (_,_,u1) -> true)
+let is_a_coercion t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ CoercDb.is_a_coercion uri
+ with Invalid_argument _ -> false
+
+let source_of t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ term_of_carr (fst (CoercDb.get_carr uri))
+ with Invalid_argument _ -> assert false (* t must be a coercion *)
+
+let target_of t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ term_of_carr (snd (CoercDb.get_carr uri))
+ with Invalid_argument _ -> assert false (* t must be a coercion *)
+
(* EOF *)
val look_for_coercion :
Cic.term -> Cic.term -> coercion_search_result
-(* it returns the list of composite coercions and their auxiliary lemmas *)
+(* it returns the list of composite coercions *)
(* composite coercions are always declared as such; they are added to the *)
-(* library only on demand (i.e. not when processing a .moo) *)
+(* CoercDb adding them to the library is left to the caller *)
val add_coercion:
- basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list
+ UriManager.uri ->
+ (UriManager.uri * Cic.obj) list
val remove_coercion: UriManager.uri -> unit
+
+val is_a_coercion: Cic.term -> bool
+val source_of: Cic.term -> Cic.term
+val target_of: Cic.term -> Cic.term
+
+val remove_all: unit -> unit
exception AlreadyDefined of UriManager.uri
+let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
+
+let merge_coercions obj =
+ let module C = Cic in
+ let rec aux2 = (fun (u,t) -> u,aux t)
+ and aux = function
+ | C.Rel _ | C.Sort _ as t -> t
+ | C.Meta _ | C.Implicit _ -> assert false
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (name,so,dest) ->
+ C.Prod (name, aux so, aux dest)
+ | C.Lambda (name,so,dest) ->
+ C.Lambda (name, aux so, aux dest)
+ | C.LetIn (name,so,dest) ->
+ C.LetIn (name, aux so, aux dest)
+ | (Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ]) as t when
+ CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
+ let source_carr = CoercGraph.source_of c2 in
+ let tgt_carr = CoercGraph.target_of c1 in
+ (match CoercGraph.look_for_coercion source_carr tgt_carr
+ with
+ | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
+ | _ -> assert false) (* the composite coercion must exist *)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux2 exp_named_subst in
+ C.Var (uri, exp_named_subst)
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst = List.map aux2 exp_named_subst in
+ C.Const (uri, exp_named_subst)
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let exp_named_subst = List.map aux2 exp_named_subst in
+ C.MutInd (uri,tyno,exp_named_subst)
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let exp_named_subst = List.map aux2 exp_named_subst in
+ C.MutConstruct (uri,tyno,consno,exp_named_subst)
+ | C.MutCase (uri,tyno,out,te,pl) ->
+ let pl = List.map aux pl in
+ C.MutCase (uri,tyno,aux out,aux te,pl)
+ | C.Fix (fno, fl) ->
+ let fl = List.map (fun (name,idx,ty,bo)->(name,idx,aux ty,aux bo)) fl in
+ C.Fix (fno, fl)
+ | C.CoFix (fno, fl) ->
+ let fl = List.map (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl in
+ C.CoFix (fno, fl)
+ in
+ match obj with
+ | C.Constant (id, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (aux body)
+ in
+ let ty = aux ty in
+ C.Constant (id, body, ty, params, attrs)
+ | C.Variable (name, body, ty, params, attrs) ->
+ let body =
+ match body with
+ | None -> None
+ | Some body -> Some (aux body)
+ in
+ let ty = aux ty in
+ C.Variable (name, body, ty, params, attrs)
+ | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
+ assert false
+ | C.InductiveDefinition (indtys, params, leftno, attrs) ->
+ let indtys =
+ List.map
+ (fun (name, ind, arity, cl) ->
+ let arity = aux arity in
+ let cl = List.map (fun (name, ty) -> (name,aux ty)) cl in
+ (name, ind, arity, cl))
+ indtys
+ in
+ C.InductiveDefinition (indtys, params, leftno, attrs)
+
let uris_of_obj uri =
let innertypesuri = UriManager.innertypesuri_of_uri uri in
let bodyuri = UriManager.bodyuri_of_uri uri in
profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
let add_single_obj uri obj ~basedir =
+ let obj =
+ if List.mem `Generated (CicUtil.attributes_of_obj obj) &&
+ not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+ then
+ merge_coercions obj
+ else
+ obj
+ in
let dbd = LibraryDb.instance () in
if CicEnvironment.in_library uri then
raise (AlreadyDefined uri)
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
ignore (LibraryDb.remove_uri uri);
- CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri);
+ CoercGraph.remove_coercion uri;
CicEnvironment.remove_obj uri)
to_remove
let generate_projections ~basedir uri fields =
let uris = ref [] in
- let projections = CicRecord.projections_of uri fields in
+ let projections = CicRecord.projections_of uri (List.map fst fields) in
try
- List.iter
- (fun (uri, name, bo) ->
+ List.iter2
+ (fun (uri, name, bo) (_name, coercion) ->
try
let ty, ugraph =
CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+
add_single_obj ~basedir uri obj;
- uris := uri :: !uris
+ let composites =
+ if coercion then
+ (* this is _NOT_ the place for THIS!!! *)
+ (* MOO HANDLING IS MISSING *)
+ let toadd = CoercGraph.add_coercion uri in
+ List.iter (fun (uri,o) -> add_single_obj ~basedir uri o) toadd;
+ List.map fst toadd
+ else
+ []
+ in
+ uris := uri :: composites @ !uris
with
CicTypeChecker.TypeCheckerFailure s ->
HLog.message
HLog.message
("Unable to create projection " ^ name ^ " because it requires " ^
depend)
- ) projections;
+ ) projections fields;
!uris
with exn ->
List.iter remove_single_obj !uris;
raise exn
-let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29
let add_obj uri obj ~basedir =
add_single_obj uri obj ~basedir;
* http://helm.cs.unibo.it/
*)
+exception AlreadyDefined of UriManager.uri
+
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
introductionTactics.cmi
eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
- primitiveTactics.cmi metadataQuery.cmi eliminationTactics.cmi
+ primitiveTactics.cmi eliminationTactics.cmi
eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
- primitiveTactics.cmx metadataQuery.cmx eliminationTactics.cmi
+ primitiveTactics.cmx eliminationTactics.cmi
negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \
primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi
negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \
fourier.cmx equalityTactics.cmx fourierR.cmi
fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
- primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi
+ primitiveTactics.cmi fwdSimplTactic.cmi
fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
- primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi
+ primitiveTactics.cmx fwdSimplTactic.cmi
history.cmo: history.cmi
history.cmx: history.cmi
statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \
but share the same design, understanding it and they way such GUIs are operated
is relevant to our discussion.
-\begin{figure}[ht]
- \begin{center}
- \resizebox{\textwidth}{!}{\includegraphics{pics/pg-coq-screenshot}}
- \caption{Proof General: a generic interface for proof assistants}
- \label{fig:proofgeneral}
- \end{center}
-\end{figure}
+%\begin{figure}[ht]
+% \begin{center}
+% \includegraphic{pics/pg-coq-screenshot}
+% \caption{Proof General: a generic interface for proof assistants}
+% \label{fig:proofgeneral}
+% \end{center}
+%\end{figure}
% - modo di lavorare
the sake of presentation) as it can be found in the standard library of the
\MATITA{} proof assistant:
-\begin{example}
-\begin{Verbatim}
-theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
- intros.
- cut (m+p \le n \or m+p \nleq n).
- elim Hcut.
- symmetry.
- apply plus_to_minus.
- rewrite > assoc_plus.
- rewrite > (sym_plus p).
- rewrite < plus_minus_m_m.
- rewrite > sym_plus.
- rewrite < plus_minus_m_m.
- reflexivity.
- apply (trans_le ? (m+p)).
- rewrite < sym_plus.
- apply le_plus_n.
- assumption.
- apply le_plus_to_minus_r.
- rewrite > sym_plus.
- assumption.
- rewrite > (eq_minus_n_m_O n (m+p)).
- rewrite > (eq_minus_n_m_O (n-m) p).
- reflexivity.
- apply le_plus_to_minus.
- apply lt_to_le.
- rewrite < sym_plus.
- apply not_le_to_lt.
- assumption.
- apply lt_to_le.
- apply not_le_to_lt.
- assumption.
- apply (decidable_le (m+p) n).
-qed.
-\end{Verbatim}
-\end{example}
+%\begin{example}
+%\begin{Verbatim}
+%theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
+% intros.
+% cut (m+p \le n \or m+p \nleq n).
+% elim Hcut.
+% symmetry.
+% apply plus_to_minus.
+% rewrite > assoc_plus.
+% rewrite > (sym_plus p).
+% rewrite < plus_minus_m_m.
+% rewrite > sym_plus.
+% rewrite < plus_minus_m_m.
+% reflexivity.
+% apply (trans_le ? (m+p)).
+% rewrite < sym_plus.
+% apply le_plus_n.
+% assumption.
+% apply le_plus_to_minus_r.
+% rewrite > sym_plus.
+% assumption.
+% rewrite > (eq_minus_n_m_O n (m+p)).
+% rewrite > (eq_minus_n_m_O (n-m) p).
+% reflexivity.
+% apply le_plus_to_minus.
+% apply lt_to_le.
+% rewrite < sym_plus.
+% apply not_le_to_lt.
+% assumption.
+% apply lt_to_le.
+% apply not_le_to_lt.
+% assumption.
+% apply (decidable_le (m+p) n).
+%qed.
+%\end{Verbatim}
+%\end{example}
The script snippet is made of 32 statements, one per line (but this is not a
requirement of the \MATITA{} script language, namely \emph{Grafite}). The first
having feedback about the status of the proof in that point. See for example
Fig.~\ref{fig:matita} where an intermediate proof status is shown.
-\begin{figure}[ht]
- \begin{center}
- \resizebox{\textwidth}{!}{\includegraphics{matita_screenshot}}
- \caption{Matita: ongoing proof}
- \label{fig:matita}
- \end{center}
-\end{figure}
+%\begin{figure}[ht]
+% \begin{center}
+% \includegraphic{matita_screenshot}
+% \caption{Matita: ongoing proof}
+% \label{fig:matita}
+% \end{center}
+%\end{figure}
% - script: sorgenti di un linguaggio imperativo, oggetti la loro semantica
% - script = sequenza di comandi
proof structuring. Consider for example an alternative, branching based, version
of the example above:
-\begin{example}
-\begin{Verbatim}
-...
-\end{Verbatim}
-\end{example}
+%\begin{example}
+%\begin{Verbatim}
+%...
+%\end{Verbatim}
+%\end{example}
Tactic applications are the same of the previous version of the script, but
branching tacticals are used. The above version is highly more readable and
\usepackage{pifont}
\usepackage{semantic}
\usepackage{stmaryrd}
+\usepackage{graphicx}
\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
projects / helm.git / commitdiff