let command_of_obj obj =
G.Executable (floc, G.Command (floc, obj))
-let command_of_macro macro =
- G.Executable (floc, G.Macro (floc, macro))
-
let require moo value =
command_of_obj (G.Include (floc, moo, `OldAndNew, value ^ ".ma"))
-let coercion value =
- command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0, 0))
-
-let inline kind uri prefix flavour params =
- let params = match prefix with
- | "" -> params
- | prefix -> G.IPPrefix prefix :: params
- in
- let params = match flavour with
- | None -> params
- | Some flavour -> G.IPAs flavour :: params
- in
- let params = match kind with
- | T.Declarative -> params
- | T.Procedural -> G.IPProcedural :: params
- in
- command_of_macro (G.Inline (floc, uri, params))
-
let out_alias och name uri =
Printf.fprintf och "alias id \"%s\" = \"%s\".\n\n" name uri
if !O.comments then out_unexported och "NOTATION" (snd specs) (**)
| T.Inline (_, T.Var, src, _, _, _) ->
if !O.comments then out_unexported och "UNEXPORTED" src
-(* FG: we do not export variables because we cook the other objects
- * let name = UriManager.name_of_uri (UriManager.uri_of_string src) in
- * out_alias och name src
- *)
- | T.Inline (_, _, src, pre, fl, params) ->
- if !O.getter then check och src;
- out_command och (inline kind src pre fl params)
| T.Section specs ->
if !O.comments then out_unexported och "UNEXPORTED" (trd specs)
| T.Comment comment ->
-cicUniv.cmi:
-cicPp.cmi: cic.cmo
-cic.cmo: cicUniv.cmi
-cic.cmx: cicUniv.cmx
-cicUniv.cmo: cicUniv.cmi
-cicUniv.cmx: cicUniv.cmi
-cicPp.cmo: cic.cmo cicPp.cmi
-cicPp.cmx: cic.cmx cicPp.cmi
(* $Id$ *)
-(* STUFF TO MANAGE IDENTIFIERS *)
type id = string (* the abstract type of the (annotated) node identifiers *)
-type 'term explicit_named_substitution = (UriManager.uri * 'term) list
-
-type implicit_annotation = [ `Closed | `Type | `Hole ]
-
-(* INTERNAL REPRESENTATION OF CIC OBJECTS AND TERMS *)
-
-type sort =
- Prop
- | Set
type name =
| Name of string
| `Variant
| `Axiom
]
-
-type object_class =
- [ `Elim of sort (** elimination principle; if sort is Type, the universe is
- * not relevant *)
- | `Record of (string * bool * int) list (**
- inductive type that encodes a record; the arguments are
- the record fields names and if they are coercions and
- then the coercion arity *)
- | `Projection (** record projection *)
- | `InversionPrinciple (** inversion principle *)
- ]
-
-type attribute =
- [ `Class of object_class
- | `Flavour of object_flavour
- | `Generated
- ]
-
-type term =
- Rel of int (* DeBrujin index, 1 based*)
- | Var of UriManager.uri * (* uri, *)
- term explicit_named_substitution (* explicit named subst. *)
- | Meta of int * (term option) list (* numeric id, *)
- (* local context *)
- | Sort of sort (* sort *)
- | Implicit of implicit_annotation option (* *)
- | Cast of term * term (* value, type *)
- | Prod of name * term * term (* binder, source, target *)
- | Lambda of name * term * term (* binder, source, target *)
- | LetIn of name * term * term * term (* binder, term, type, target *)
- | Appl of term list (* arguments *)
- | Const of UriManager.uri * (* uri, *)
- term explicit_named_substitution (* explicit named subst. *)
- | MutInd of UriManager.uri * int * (* uri, typeno, *)
- term explicit_named_substitution (* explicit named subst. *)
- (* typeno is 0 based *)
- | MutConstruct of UriManager.uri * (* uri, *)
- int * int * (* typeno, consno *)
- term explicit_named_substitution (* explicit named subst. *)
- (* typeno is 0 based *)
- (* consno is 1 based *)
- | MutCase of UriManager.uri * (* ind. uri, *)
- int * (* ind. typeno, *)
- term * term * (* outtype, ind. term *)
- term list (* patterns *)
- | Fix of int * inductiveFun list (* funno (0 based), funs *)
- | CoFix of int * coInductiveFun list (* funno (0 based), funs *)
-and obj =
- Constant of string * term option * term * (* id, body, type, *)
- UriManager.uri list * attribute list (* parameters *)
- | Variable of string * term option * term * (* name, body, type *)
- UriManager.uri list * attribute list (* parameters *)
- | CurrentProof of string * metasenv * term * (* name, conjectures, body, *)
- term * UriManager.uri list * attribute list (* type, parameters *)
- | InductiveDefinition of inductiveType list * (* inductive types, *)
- UriManager.uri list * int * attribute list (* params, left params no *)
-and inductiveType =
- string * bool * term * (* typename, inductive, arity *)
- constructor list (* constructors *)
-and constructor =
- string * term (* id, type *)
-and inductiveFun =
- string * int * term * term (* name, ind. index, type, body *)
-and coInductiveFun =
- string * term * term (* name, type, body *)
-
-(* a metasenv is a list of declarations of metas in declarations *)
-(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
-(* depend on new ones. *)
-and conjecture = int * context * term
-and metasenv = conjecture list
-and substitution = (int * (context * term * term)) list
-
-
-
-(* a metasenv is a list of declarations of metas in declarations *)
-(* order (i.e. [oldest ; ... ; newest]). Older variables can not *)
-(* depend on new ones. *)
-and annconjecture = id * int * anncontext * annterm
-and annmetasenv = annconjecture list
-
-and annterm =
- ARel of id * id * int * (* idref, DeBrujin index, *)
- string (* binder *)
- | AVar of id * UriManager.uri * (* uri, *)
- annterm explicit_named_substitution (* explicit named subst. *)
- | AMeta of id * int * (annterm option) list (* numeric id, *)
- (* local context *)
- | ASort of id * sort (* sort *)
- | AImplicit of id * implicit_annotation option (* *)
- | ACast of id * annterm * annterm (* value, type *)
- | AProd of id * name * annterm * annterm (* binder, source, target *)
- | ALambda of id * name * annterm * annterm (* binder, source, target *)
- | ALetIn of id * name * annterm * annterm * annterm (* binder, term, type, target *)
- | AAppl of id * annterm list (* arguments *)
- | AConst of id * UriManager.uri * (* uri, *)
- annterm explicit_named_substitution (* explicit named subst. *)
- | AMutInd of id * UriManager.uri * int * (* uri, typeno *)
- annterm explicit_named_substitution (* explicit named subst. *)
- (* typeno is 0 based *)
- | AMutConstruct of id * UriManager.uri * (* uri, *)
- int * int * (* typeno, consno *)
- annterm explicit_named_substitution (* explicit named subst. *)
- (* typeno is 0 based *)
- (* consno is 1 based *)
- | AMutCase of id * UriManager.uri * (* ind. uri, *)
- int * (* ind. typeno, *)
- annterm * annterm * (* outtype, ind. term *)
- annterm list (* patterns *)
- | AFix of id * int * anninductiveFun list (* funno, functions *)
- | ACoFix of id * int * anncoInductiveFun list (* funno, functions *)
-and annobj =
- AConstant of id * id option * string * (* name, *)
- annterm option * annterm * (* body, type, *)
- UriManager.uri list * attribute list (* parameters *)
- | AVariable of id *
- string * annterm option * annterm * (* name, body, type *)
- UriManager.uri list * attribute list (* parameters *)
- | ACurrentProof of id * id *
- string * annmetasenv * (* name, conjectures, *)
- annterm * annterm * UriManager.uri list * (* body,type,parameters *)
- attribute list
- | AInductiveDefinition of id *
- anninductiveType list * (* inductive types , *)
- UriManager.uri list * int * attribute list (* parameters,n ind. pars*)
-and anninductiveType =
- id * string * bool * annterm * (* typename, inductive, arity *)
- annconstructor list (* constructors *)
-and annconstructor =
- string * annterm (* id, type *)
-and anninductiveFun =
- id * string * int * annterm * annterm (* name, ind. index, type, body *)
-and anncoInductiveFun =
- id * string * annterm * annterm (* name, type, body *)
-and annotation =
- string
-
-and context_entry = (* A declaration or definition *)
- Decl of term
- | Def of term * term (* body, type *)
-
-and hypothesis =
- (name * context_entry) option (* None means no more accessible *)
-
-and context = hypothesis list
-
-and anncontext_entry = (* A declaration or definition *)
- ADecl of annterm
- | ADef of annterm * annterm
-
-and annhypothesis =
- id * (name * anncontext_entry) option (* None means no more accessible *)
-
-and anncontext = annhypothesis list
-;;
-
-type anntarget =
- Object of annobj (* if annobj is a Constant, this is its type *)
- | ConstantBody of annobj
- | Term of annterm
- | Conjecture of annconjecture
- | Hypothesis of annhypothesis
-
-module CicHash =
- Hashtbl.Make
- (struct
- type t = term
- let equal = (==)
- let hash = Hashtbl.hash_param 100 1000
- end)
-;;
-
| IPComments (* show statistics *)
| IPCR (* detect convertible rewriting *)
-type ('term,'lazy_term) macro =
- (* real macros *)
- | Eval of loc * 'lazy_term reduction * 'term
- | Check of loc * 'term
- | Hint of loc * bool
- | AutoInteractive of loc * 'term auto_params
- | Inline of loc * string * inline_param list
- (* URI or base-uri, parameters *)
-
type nmacro =
| NCheck of loc * NotationPt.term
| Screenshot of loc * string
* marshalling *)
let magic = 34
-type ('term,'obj) command =
- | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
- | Select of loc * UriManager.uri
- | Pump of loc * int
- | Coercion of loc * 'term * bool (* add_obj *) *
- int (* arity *) * int (* saturations *)
- | PreferCoercion of loc * 'term
- | Inverter of loc * string * 'term * bool list
- | Default of loc * string * UriManager.uri list
+type command =
| Drop of loc
| Include of loc * bool (* normal? *) * [`New | `OldAndNew] * string
- | Obj of loc * 'obj
- | Relation of
- loc * string * 'term * 'term * 'term option * 'term option * 'term option
| Set of loc * string * string
| Print of loc * string
| Qed of loc
| Skip of loc
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
- | Command of loc * ('term, 'obj) command
+ | Command of loc * command
| NCommand of loc * ncommand
- | Macro of loc * ('term,'lazy_term) macro
| NMacro of loc * nmacro
| NTactic of loc * ntactic list
| Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
-let pp_macro ~term_pp ~lazy_term_pp =
- let term_pp = pp_arg ~term_pp in
- let flavour_pp = function
- | `Definition -> "definition"
- | `Fact -> "fact"
- | `Lemma -> "lemma"
- | `Remark -> "remark"
- | `Theorem -> "theorem"
- | `Variant -> "variant"
- | `Axiom -> "axiom"
- | `MutualDefinition -> assert false
- in
- let pp_inline_params l =
- let pp_param = function
- | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
- | IPAs flavour -> flavour_pp flavour
- | IPCoercions -> "coercions"
- | IPDebug debug -> "debug = " ^ string_of_int debug
- | IPProcedural -> "procedural"
- | IPNoDefaults -> "nodefaults"
- | IPDepth depth -> "depth = " ^ string_of_int depth
- | IPLevel level -> "level = " ^ string_of_int level
- | IPComments -> "comments"
- | IPCR -> "cr"
- in
- let s = String.concat " " (List.map pp_param l) in
- if s = "" then s else " " ^ s
- in
- let pp_reduction_kind = pp_reduction_kind ~term_pp:lazy_term_pp in
- function
- (* real macros *)
- | Eval (_, kind, term) ->
- Printf.sprintf "eval %s on %s" (pp_reduction_kind kind) (term_pp term)
- | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
- | Hint (_, true) -> "hint rewrite"
- | Hint (_, false) -> "hint"
- | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
- | Inline (_, suri, params) ->
- Printf.sprintf "inline \"%s\"%s" suri (pp_inline_params params)
-
let pp_associativity = function
| Gramext.LeftA -> "left associative"
| Gramext.RightA -> "right associative"
map)
;;
-let pp_command ~term_pp ~obj_pp = function
- | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
- | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri
- | Coercion (_, t, do_composites, i, j) ->
- pp_coercion ~term_pp t do_composites i j
- | PreferCoercion (_,t) ->
- "prefer coercion " ^ term_pp t
- | Inverter (_,n,ty,params) ->
- "inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
- | Default (_,what,uris) -> pp_default what uris
+let pp_command = function
| Drop _ -> "drop"
| Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\""
| Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\""
| Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path
- | Obj (_,obj) -> obj_pp obj
- | Qed _ -> "qed"
- | 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) -> Printf.sprintf "set \"%s\" \"%s\"" name value
- | Pump (_) -> "not supported"
let pp_punctuation_tactical =
function
let pp_executable ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =
function
| NMacro (_, macro) -> pp_nmacro macro ^ "."
- | Macro (_, macro) -> pp_macro ~term_pp ~lazy_term_pp macro ^ "."
| Tactic (_, Some tac, punct) ->
pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp tac
^ pp_punctuation_tactical punct
| NonPunctuationTactical (_, tac, punct) ->
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
- | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
+ | Command (_, cmd) -> pp_command cmd ^ "."
| NCommand (_, cmd) ->
let obj_pp = Obj.magic obj_pp in
pp_ncommand ~obj_pp cmd ^ "."
'a GrafiteAst.reduction ->
string
-val pp_command:
- term_pp:('term -> string) ->
- obj_pp:('obj -> string) ->
- ('term,'obj) GrafiteAst.command -> string
-val pp_macro:
- term_pp:('term -> string) ->
- lazy_term_pp:('lazy_term -> string) ->
- ('term,'lazy_term) GrafiteAst.macro -> string
+val pp_command: GrafiteAst.command -> string
val pp_comment:
map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
(* $Id$ *)
-type ast_command = (Cic.term,Cic.obj) GrafiteAst.command
+type ast_command = GrafiteAst.command
type moo = ast_command list
let format_name = "grafite"
let rehash_uri uri =
UriManager.uri_of_string (UriManager.string_of_uri uri) in
function
- | GrafiteAst.Default (loc, name, uris) ->
- let uris = List.map rehash_uri uris in
- GrafiteAst.Default (loc, name, uris)
| GrafiteAst.Include _ as cmd -> cmd
| 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 ~term_pp ~obj_pp cmd);
+ prerr_endline (GrafiteAstPp.pp_command 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.term,Cic.obj) GrafiteAst.command
+type ast_command = GrafiteAst.command
type moo = ast_command list
val save_moo: fname:string -> moo -> unit
exception Drop
(* mo file name, ma file name *)
exception IncludedFileNotCompiled of string * string
-exception Macro of
- GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
+ (GrafiteAst.command) disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
type 'a eval_command =
{ec_go: 'term 'obj.
disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
+ (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
options -> GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
+ GrafiteAst.command disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
}
type 'a eval_comment =
{ecm_go: 'term 'lazy_term 'reduction_kind 'obj 'ident.
disambiguate_command:
- (GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
+ (GrafiteTypes.status -> GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
options -> GrafiteTypes.status ->
(('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input ->
GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list]
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
+ GrafiteAst.command disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
options ->
GrafiteTypes.status ->
status,`New []
| GrafiteAst.Print (_,_) -> status,`New []
| GrafiteAst.Set (loc, name, value) -> status, `New []
-(* GrafiteTypes.set_option status name value,[] *)
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
in
status,uris
} and eval_executable = {ee_go = fun ~disambiguate_command
-~disambiguate_macro opts status (text,prefix_len,ex) ->
+ opts status (text,prefix_len,ex) ->
match ex with
| GrafiteAst.NTactic (_(*loc*), tacl) ->
if status#ng_mode <> `ProofMode then
eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
| GrafiteAst.NCommand (_, cmd) ->
eval_ncommand opts status (text,prefix_len,cmd)
- | GrafiteAst.Macro (loc, macro) ->
- raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
| GrafiteAst.NMacro (loc, macro) ->
raise (NMacro (loc,macro))
let status,lemmas =
eval_ast.ea_go
~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
- ~disambiguate_macro:(fun _ _ -> assert false)
status ast
in
assert (lemmas=`New []);
status)
status moo
} and eval_ast = {ea_go = fun ~disambiguate_command
-~disambiguate_macro ?(do_heavy_checks=false) status
+?(do_heavy_checks=false) status
(text,prefix_len,st)
->
let opts = { do_heavy_checks = do_heavy_checks ; } in
match st with
| GrafiteAst.Executable (_,ex) ->
eval_executable.ee_go ~disambiguate_command
- ~disambiguate_macro opts status (text,prefix_len,ex)
+ opts status (text,prefix_len,ex)
| GrafiteAst.Comment (_,c) ->
eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c)
} and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) ->
exception Drop
exception IncludedFileNotCompiled of string * string
-exception Macro of
- GrafiteAst.loc *
- (Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro)
exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
type 'a disambiguator_input = string * int * 'a
val eval_ast :
disambiguate_command:
(GrafiteTypes.status ->
- (('term,'obj) GrafiteAst.command) disambiguator_input ->
- GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
-
- disambiguate_macro:
- (GrafiteTypes.status ->
- (('term,'lazy_term) GrafiteAst.macro) disambiguator_input ->
- Cic.context -> GrafiteTypes.status * (Cic.term,unit) GrafiteAst.macro) ->
+ (GrafiteAst.command) disambiguator_input ->
+ GrafiteTypes.status * GrafiteAst.command) ->
?do_heavy_checks:bool ->
GrafiteTypes.status ->
open Printf
-let is_a_variant obj =
- match obj with
- | Cic.Constant(_,_,_,_,attrs) ->
- List.exists (fun x -> x = `Flavour `Variant) attrs
- | _ -> false
-
-let uris_for_inductive_type uri obj =
- match obj with
- | Cic.InductiveDefinition(types,_,_,_) ->
- let suri = UriManager.string_of_uri uri in
- let uris,_ =
- List.fold_left
- (fun (acc,i) (_,_,_,constructors)->
- let is = string_of_int i in
- let newacc,_ =
- List.fold_left
- (fun (acc,j) _ ->
- let js = string_of_int j in
- UriManager.uri_of_string
- (suri^"#xpointer(1/"^is^"/"^js^")")::acc,j+1)
- (acc,1) constructors
- in
- newacc,i+1)
- ([],1) types
- in uris
- | _ -> [uri]
-;;
-
(** @return l2 \ l1 *)
let uri_list_diff l2 l1 =
let module S = UriManager.UriSet in
let add_moo_content cmds status =
let content = status#moo_content_rev in
- let content' =
- List.fold_right
- (fun cmd acc ->
-(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
- match cmd with
- | GrafiteAst.Default _
- | GrafiteAst.Index _
- | GrafiteAst.Coercion _ ->
- if List.mem cmd content then acc
- else cmd :: acc
- | _ -> cmd :: acc)
- cmds content
- in
+ let content' = cmds@content in
(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
GrafiteAstPp.pp_command content')); *)
status#set_moo_content_rev content'
;;
let disambiguate_command estatus ?baseuri (text,prefix_len,cmd)=
match cmd with
- | GrafiteAst.Index(loc,key,uri) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Select (loc,uri) ->
- estatus, GrafiteAst.Select(loc,uri)
- | GrafiteAst.PreferCoercion (loc,t) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Coercion (loc,t,b,a,s) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Inverter (loc,n,indty,params) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _
| GrafiteAst.Print _
- | GrafiteAst.Qed _
| GrafiteAst.Set _ as cmd ->
estatus,cmd
- | GrafiteAst.Obj (loc,obj) -> (* MATITA 1.0 *) assert false
- | GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans) -> (* MATITA 1.0 *) assert false
val disambiguate_command:
LexiconEngine.status as 'status ->
?baseuri:string ->
- ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
- 'status * (Cic.term,Cic.obj) GrafiteAst.command
+ GrafiteAst.command Disambiguate.disambiguator_input ->
+ 'status * GrafiteAst.command
val disambiguate_nterm :
NCic.term option ->
let loc,t = mk_rec_corec ind_kind defs loc in
G.NObj (loc,t)
-let mk_rec_corec ind_kind defs loc =
- let loc,t = mk_rec_corec ind_kind defs loc in
- G.Obj (loc,t)
-
let npunct_of_punct = function
| G.Branch loc -> G.NBranch loc
| G.Shift loc -> G.NShift loc
(params,name,typ,fields)
] ];
- macro: [
- [ [ IDENT "check" ]; t = term ->
- G.Check (loc, t)
- | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
- G.Eval (loc, kind, t)
- | IDENT "inline"; suri = QSTRING; params = inline_params ->
- G.Inline (loc, suri, params)
- | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
- if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
- | IDENT "auto"; params = auto_params ->
- G.AutoInteractive (loc,params)
- ]
- ];
alias_spec: [
[ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
let alpha = "[a-zA-Z]" in
G.Set (loc, n, v)
| IDENT "drop" -> G.Drop loc
| IDENT "print"; s = IDENT -> G.Print (loc,s)
- | IDENT "qed" -> G.Qed loc
- | IDENT "variant" ; name = IDENT; SYMBOL ":";
- typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
- G.Obj (loc,
- N.Theorem
- (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
- | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
- body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
- G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
- | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
- body = term ->
- G.Obj (loc,
- N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
- | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
- G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
- | LETCOREC ; defs = let_defs ->
- mk_rec_corec `CoInductive defs loc
- | LETREC ; defs = let_defs ->
- mk_rec_corec `Inductive defs loc
- | IDENT "inductive"; spec = inductive_spec ->
- let (params, ind_types) = spec in
- G.Obj (loc, N.Inductive (params, ind_types))
- | IDENT "coinductive"; spec = inductive_spec ->
- let (params, ind_types) = spec in
- let ind_types = (* set inductive flags to false (coinductive) *)
- List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
- ind_types
- in
- G.Obj (loc, N.Inductive (params, ind_types))
- | IDENT "coercion" ;
- t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
- arity = OPT int ; saturations = OPT int;
- composites = OPT (IDENT "nocomposites") ->
- let arity = match arity with None -> 0 | Some x -> x in
- let saturations = match saturations with None -> 0 | Some x -> x in
- let composites = match composites with None -> true | Some _ -> false in
- G.Coercion
- (loc, t, composites, arity, saturations)
- | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
- G.PreferCoercion (loc, t)
- | IDENT "pump" ; steps = int ->
- G.Pump(loc,steps)
- | IDENT "inverter"; name = IDENT; IDENT "for";
- indty = tactic_term; paramspec = inverter_param_list ->
- G.Inverter
- (loc, name, indty, paramspec)
- | IDENT "record" ; (params,name,ty,fields) = record_spec ->
- G.Obj (loc, N.Record (params,name,ty,fields))
- | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
- let uris = List.map UriManager.uri_of_string uris in
- G.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 ->
- G.Relation (loc,id,a,aeq,refl,sym,trans)
]];
lexicon_command: [ [
IDENT "alias" ; spec = alias_spec ->
| SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
punct = punctuation_tactical ->
G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
- | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
]
];
comment: [
| Some id ->
prerr_endline "removing last notation rule ...";
NotationParser.delete id) *)
- | G.Executable (_, G.Macro (_, G.Check (_, t))) ->
- prerr_endline (sprintf "ast: %s" (NotationPp.pp_term t));
- let t' = TermContentPres.pp_ast t in
- prerr_endline (sprintf "rendered ast: %s"
- (NotationPp.pp_term t'));
- let tbl = Hashtbl.create 0 in
- dump_xml t' tbl "out.xml"
| statement ->
prerr_endline
("Unsupported statement: " ^
let new_env = build_aliases [(name,uri)] in
LexiconEngine.set_proof_aliases status new_env
-let add_aliases_for_object status uri =
- function
- Cic.InductiveDefinition (types,_,_,_) ->
- add_aliases_for_inductive_def status types uri
- | Cic.Constant _ -> add_alias_for_constant status uri
- | Cic.Variable _
- | Cic.CurrentProof _ -> assert false
-
let add_aliases_for_objs status =
function
`Old _ -> assert false (* MATITA 1.0 *)
exception Choice_not_found of string Lazy.t
-let num_choices = ref []
let nnum_choices = ref []
-let add_num_choice choice = num_choices := choice :: !num_choices
let nadd_num_choice choice = nnum_choices := choice :: !nnum_choices
let has_description dsc = (fun x -> fst x = dsc)
-let lookup_num_choices () = !num_choices
-
-let lookup_num_by_dsc dsc =
- try
- List.find (has_description dsc) !num_choices
- with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc)))
-
let nlookup_num_by_dsc dsc =
try
List.find (has_description dsc) !nnum_choices
(** raised by lookup_XXXX below *)
exception Choice_not_found of string Lazy.t
- (** register a new number choice *)
-val add_num_choice: Cic.term codomain_item -> unit
-
(** register a new number choice *)
val nadd_num_choice: NCic.term codomain_item -> unit
(** {2 Choices lookup}
* for user defined aliases *)
-val lookup_num_choices: unit -> Cic.term codomain_item list
-
- (** @param dsc description (1st component of codomain_item) *)
-val lookup_num_by_dsc: string -> Cic.term codomain_item
-
(** @param dsc description (1st component of codomain_item) *)
val nlookup_num_by_dsc: string -> NCic.term codomain_item
type db
-val set_convert_term:
- (UriManager.uri -> Cic.term -> NCic.term * NCic.obj list) -> unit
-
class type g_status =
object
inherit NCicUnifHint.g_status
| [ [], [], [], `NoTag ] -> true
| _ -> false
- let of_metasenv metasenv =
- let goals = List.map (fun (g, _, _) -> g) metasenv in
- [ zero_pos goals, [], [], `NoTag ]
-
let of_nmetasenv metasenv =
let goals = List.map (fun (g, _) -> g) metasenv in
[ zero_pos goals, [], [], `NoTag ]
val find_goal: t -> goal (** find "next" goal *)
val is_empty: t -> bool (** a singleton empty level *)
- val of_metasenv: Cic.metasenv -> t
val of_nmetasenv: (goal * 'a) list -> t
val head_switches: t -> switch list (** top level switches *)
val head_goals: t -> goal list (** top level goals *)
let lexicon_status_ref = ref (status :> LexiconEngine.status) in
let baseuri = status#baseuri in
let new_status,new_objs =
- match ast with
- | G.Executable (_, G.Command (_, G.Coercion _)) when dump ->
-(* FG: some commands can not be executed when mmas are parsed *************)
-(* To be removed when mmas will be executed *)
- status, `New []
- | ast ->
GrafiteEngine.eval_ast
~disambiguate_command:(disambiguate_command lexicon_status_ref)
- ~disambiguate_macro:((* MATITA 1.0*) fun _ -> assert false)
?do_heavy_checks status (text,prefix_len,ast)
in
let new_status =
self#misc#modify_font_by_name
(sprintf "%s %d" BuildTimeConf.script_font !current_font_size)
method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
- method private set_cic_info = (function _ -> () : (Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
+ method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.hypothesis) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option) option -> unit)
+ (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit)
(* dal widget di Luca *)
method load_root ~root =
self#buffer#delete ~start:(self#buffer#get_iter `START)
[s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
-let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
- (* no idea why ocaml wants this *)
- let parsed_text_length = String.length parsed_text in
- match mac with
- (* REAL macro *)
- | TA.Hint (loc, rewrite) -> (* MATITA 1.0 *) assert false
- | TA.Eval (_, kind, term) -> assert false (* MATITA 1.0
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context =
- match user_goal with
- None -> []
- | Some n -> GrafiteTypes.get_proof_context grafite_status n in
- let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let term =
- match kind with
- | `Normalize ->
- CicReduction.normalize ~delta:true ~subst:[] context term
- | `Simpl ->
- ProofEngineReduction.simpl context term
- | `Unfold None ->
- ProofEngineReduction.unfold ?what:None context term
- | `Unfold (Some lazy_term) ->
- let what, _, _ =
- lazy_term context metasenv CicUniv.empty_ugraph in
- ProofEngineReduction.unfold ~what context term
- | `Whd ->
- CicReduction.whd ~delta:true ~subst:[] context term
- in
- let t_and_ty = Cic.Cast (term,ty) in
- guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [(grafite_status#set_proof_status No_proof), parsed_text ],"",
- parsed_text_length *)
-
-and eval_executable include_paths (buffer : GText.buffer) guistuff
+let rec eval_executable include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
script ex loc
=
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
- | GrafiteEngine.Macro (_loc,lazy_macro) ->
- let context = [] in
- let grafite_status,macro = lazy_macro context in
- eval_macro include_paths buffer guistuff grafite_status
- user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
| GrafiteEngine.NMacro (_loc,macro) ->
eval_nmacro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
in
let grafite_status =
let rec aux_for_dump x grafite_status =
- try
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
grafite_status buf x
| (g,None)::_ -> g
| (g,Some _)::_ ->
raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
- with MatitaEngine.EnrichedWithStatus
- (GrafiteEngine.Macro (floc, f), grafite) as exn ->
- match f (get_macro_context (Some grafite)) with
- | _, GrafiteAst.Inline (_, _suri, _params) ->
-(*
- let str =
- ApplyTransformation.txt_of_inline_macro style prefix suri
- ?flavour
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- in
- !out str;
-*)
- aux_for_dump x grafite
- |_-> raise exn
in
aux_for_dump print_cb grafite_status
in
projects / helm.git / commitdiff