module Ast = CicNotationPt
+exception NoInclusionPerformed of string (* full path *)
+
type 'a localized_option =
LSome of 'a
| LNone of GrafiteAst.loc
GrafiteAst.statement
type statement =
+ ?never_include:bool ->
include_paths:string list ->
LexiconEngine.status ->
LexiconEngine.status * ast_statement localized_option
];
reduction_kind: [
[ IDENT "normalize" -> `Normalize
- | IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
| IDENT "unfold"; t = OPT tactic_term -> `Unfold t
| IDENT "whd" -> `Whd ]
GrafiteAst.Absurd (loc, t)
| IDENT "apply"; t = tactic_term ->
GrafiteAst.Apply (loc, t)
- | IDENT "applyS"; t = tactic_term ; params =
- LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
- string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ | IDENT "applyS"; t = tactic_term ; params = auto_params ->
GrafiteAst.ApplyS (loc, t, params)
| IDENT "assumption" ->
GrafiteAst.Assumption loc
| IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
- | IDENT "demodulate" -> GrafiteAst.Demodulate loc
+ | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
| IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
GrafiteAst.Destruct (loc, xts)
| IDENT "elim"; what = tactic_term; using = using;
GrafiteAst.Assume (loc, id, t)
| IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
GrafiteAst.Suppose (loc, t, id, t1)
- | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
+ | "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
cont=by_continuation ->
let t' = match t with LNone _ -> None | LSome t -> Some t in
(match cont with
| LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
| IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
GrafiteAst.We_need_to_prove (loc, t, id, t1)
- | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
- | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
+ | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
- | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+ | "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
GrafiteAst.Byinduction(loc, t, id)
| IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
GrafiteAst.Thesisbecomes(loc, t)
| IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
GrafiteAst.Case(loc,id,params)
- | start =
- [ IDENT "conclude" -> None
- | IDENT "obtain" ; name = IDENT -> Some name ] ;
- termine = tactic_term ;
+ | start = OPT [
+ start =
+ [ IDENT "conclude" -> None
+ | IDENT "obtain" ; name = IDENT -> Some name ] ;
+ termine = tactic_term -> start, termine];
SYMBOL "=" ;
t1=tactic_term ;
- IDENT "by" ;
t2 =
- [ t=tactic_term -> `Term t
- | SYMBOL "_" ; params = auto_params' -> `Auto params
- | IDENT "proof" -> `Proof] ;
+ [ IDENT "exact"; t=tactic_term -> `Term t
+ | IDENT "using"; term=tactic_term -> `SolveWith term
+ | IDENT "proof" -> `Proof
+ | params = auto_params -> `Auto params];
cont = rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
- | SYMBOL "=" ;
- t1=tactic_term ;
- IDENT "by" ;
- t2=
- [ t=tactic_term -> `Term t
- | SYMBOL "_" ; params = auto_params' -> `Auto params
- | IDENT "proof" -> `Proof] ;
- cont=rewriting_step_continuation ->
- GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+ GrafiteAst.RewritingStep(loc, start, t1, t2, cont)
]
];
auto_params: [
[ params =
LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
- string_of_int v | v = IDENT -> v ] -> i,v ] ->
+ string_of_int v | v = IDENT -> v ] -> i,v ];
+ tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] ->
+ (match tl with Some l -> l | None -> []),
params
]
-];
- auto_params': [
- [ LPAREN; params = auto_params; RPAREN -> params
- | -> []
- ]
];
by_continuation: [
[ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
| IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
- IDENT "done" -> BYC_weproved (ty,None,t1)
- | IDENT "done" -> BYC_done
+ "done" -> BYC_weproved (ty,None,t1)
+ | "done" -> BYC_done
| "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
| IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
]
];
rewriting_step_continuation : [
- [ IDENT "done" -> true
+ [ "done" -> true
| -> false
]
];
ind_types
in
GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
- | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
+ | IDENT "coercion" ; suri = URI ; 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
GrafiteAst.Coercion
- (loc, UriManager.uri_of_string suri, true, arity, saturations)
+ (loc, UriManager.uri_of_string suri, composites, arity, saturations)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
| 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 = OPT [ IDENT "reflexivity" ; IDENT "proved" ; "by" ;
refl = tactic_term -> refl ] ;
- sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+ sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ;
sym = tactic_term -> sym ] ;
- trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+ trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ;
trans = tactic_term -> trans ] ;
"as" ; id = IDENT ->
GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
];
statement: [
[ ex = executable ->
- fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
+ fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
| com = comment ->
- fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
+ fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
| (iloc,fname,mode) = include_command ; SYMBOL "." ->
- fun ~include_paths status ->
- let buri, fullpath =
- DependenciesParser.baseuri_of_script ~include_paths fname
+ fun ?(never_include=false) ~include_paths status ->
+ let _root, buri, fullpath, _rrelpath =
+ Librarian.baseuri_of_script ~include_paths fname
in
let status =
- LexiconEngine.eval_command status
- (LexiconAst.Include (iloc,buri,mode,fullpath))
+ if never_include then raise (NoInclusionPerformed fullpath)
+ else LexiconEngine.eval_command status
+ (LexiconAst.Include (iloc,buri,mode,fullpath))
in
!out fname;
status,
(loc,GrafiteAst.Command
(loc,GrafiteAst.Include (iloc,buri))))
| scom = lexicon_command ; SYMBOL "." ->
- fun ~include_paths status ->
+ fun ?(never_include=false) ~include_paths status ->
let status = LexiconEngine.eval_command status scom in
status,LNone loc
| EOI -> raise End_of_file
let parse_statement lexbuf =
exc_located_wrapper
(fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
+