let level_of precedence =
if precedence < min_precedence || precedence > max_precedence then
raise (Level_not_found precedence);
- string_of_int precedence ^ "N"
+ string_of_int precedence
let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
let gram_ident s = Gramext.Stoken ("IDENT", s)
let gram_number s = Gramext.Stoken ("NUMBER", s)
let gram_keyword s = Gramext.Stoken ("", s)
let gram_term = function
- | None -> Gramext.Sself
- | Some (precedence) ->
- Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence)
+ | Ast.Self _ -> Gramext.Sself
+ | Ast.Level precedence ->
+ Gramext.Snterml
+ (Grammar.Entry.obj (term: 'a Grammar.Entry.e), level_of precedence)
;;
let gram_of_literal =
| Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\below"] @ aux p2
| Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\above"] @ aux p2
| Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\frac"] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol "\\infrule"] @ aux p1 @ aux p2 @ aux p3
| Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\atop"] @ aux p2
| Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\over"] @ aux p2
| Ast.Root (p1, p2) ->
and aux_variable =
function
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar (s,level) ->
- [Binding (s, Env.TermType level), gram_term level]
+ | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) ->
+ [Binding (s, Env.TermType level), gram_term lv]
| Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
| Ast.Literal _ as l -> incr symbols; l
| Ast.Layout l -> Ast.Layout (aux_layout l)
| Ast.Magic m -> Ast.Magic (aux_magic m)
- | Ast.Variable v -> Ast.Variable (aux_variable v)
+ | Ast.Variable v -> (aux_variable v)
| t -> assert false
and aux_layout = function
| Ast.Sub (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sub (p1, p2)
| Ast.Below (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Below (p1, p2)
| Ast.Above (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Above (p1, p2)
| Ast.Frac (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Frac (p1, p2)
+ | Ast.InfRule (p1, p2, p3) -> let p1 = aux p1 in let p2 = aux p2 in let p3 = aux p3 in Ast.InfRule (p1, p2, p3)
| Ast.Atop (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Atop (p1, p2)
| Ast.Over (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Over (p1, p2)
| Ast.Root (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Root (p1, p2)
| _ -> assert false
and aux_variable =
function
- | Ast.NumVar _ as t -> t
- | Ast.TermVar (s,None) when associativity <> Gramext.NonA ->
+ | Ast.NumVar _ as t -> Ast.Variable t
+ | Ast.TermVar (s,Ast.Self _) when associativity <> Gramext.NonA ->
incr variables;
if !variables > 2 then
raise (Parse_error ("Exactly 2 variables must be specified in an "^
"associative notation"));
(match !variables, associativity with
- | 1,Gramext.LeftA -> Ast.TermVar (s, None) (*Ast.TermVar (s, Some
- (level-1)) *)
- | 1,Gramext.RightA -> Ast.TermVar (s, None)
- | 2,Gramext.LeftA ->Ast.TermVar (s, None)
- | 2,Gramext.RightA -> Ast.TermVar (s, Some (level-1))
+ | 1,Gramext.LeftA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self level))
+ | 1,Gramext.RightA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+ | 2,Gramext.LeftA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Self (level+1)))
+ | 2,Gramext.RightA ->
+ Ast.Variable (Ast.TermVar (s, Ast.Level (level-1)))
| _ -> assert false)
- | Ast.TermVar (s,Some _) when associativity <> Gramext.NonA ->
+ | Ast.TermVar (s,Ast.Level _) when associativity <> Gramext.NonA ->
raise (Parse_error ("Variables can not be declared with a " ^
"precedence in an associative notation"))
- (* avoid camlp5 divergence due to non-Sself recursion at the same level *)
- | Ast.TermVar (s,Some l) when l <= level && !variables=0 && !symbols=0 ->
- raise (Parse_error ("Left recursive rule with precedence not greater " ^
- "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
- | Ast.TermVar _ as t -> incr variables; t
- | Ast.IdentVar _ as t -> t
+ (*avoid camlp5 divergence due to non-Sself recursion at the same level *)
+ | Ast.TermVar (s,Ast.Level l) when l<=level && !variables=0 && !symbols=0->
+ raise(Parse_error("Left recursive rule with precedence not greater " ^
+ "than " ^ string_of_int level ^ " is not allowed to avoid divergence"))
+ | Ast.TermVar _ as t -> incr variables; Ast.Variable t
+ | Ast.IdentVar _ as t -> Ast.Variable t
| Ast.Ascription _ -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
in
if associativity <> Gramext.NonA && level = min_precedence then
raise (Parse_error ("You can not specify an associative notation " ^
"at level "^string_of_int min_precedence ^ "; increase it"));
- let cp = CL1P (aux level1_pattern, level) in
+ let cp = aux level1_pattern in
+(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *)
if !variables <> 2 && associativity <> Gramext.NonA then
raise (Parse_error ("Exactly 2 variables must be specified in an "^
"associative notation"));
- cp
+ CL1P (cp,level)
;;
let extend (CL1P (level1_pattern,precedence)) action =
(** {2 Grammar} *)
-let parse_level1_pattern_ref = ref (fun _ -> assert false)
+let parse_level1_pattern_ref = ref (fun _ _ -> assert false)
let parse_level2_ast_ref = ref (fun _ -> assert false)
let parse_level2_meta_ref = ref (fun _ -> assert false)
pt_names body
let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
+let return_term_of_level loc term l =
+ Ast.AttributedTerm (`Loc loc, term l)
(* create empty precedence level for "term" *)
let _ =
| i when i < first -> acc
| i ->
aux
- ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod)
+ ((Some (level_of i), Some Gramext.NonA, dummy_prod)
:: acc)
(i - 1)
in
EXTEND
GLOBAL: level1_pattern;
- level1_pattern: [ [ p = l1_pattern; EOI -> CicNotationUtil.boxify p ] ];
- l1_pattern: [ [ p = LIST1 l1_simple_pattern -> p ] ];
+ level1_pattern: [
+ [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ]
+ ];
+ l1_pattern: [
+ [ p = LIST1 l1_simple_pattern ->
+ fun l -> List.map (fun x -> x l) p ]
+ ];
literal: [
[ s = SYMBOL -> `Symbol s
| k = QKEYWORD -> `Keyword k
]
];
sep: [ [ "sep"; sep = literal -> sep ] ];
-(* row_sep: [ [ "rowsep"; sep = literal -> sep ] ];
- field_sep: [ [ "fieldsep"; sep = literal -> sep ] ]; *)
l1_magic_pattern: [
- [ "list0"; p = l1_simple_pattern; sep = OPT sep -> Ast.List0 (p, sep)
- | "list1"; p = l1_simple_pattern; sep = OPT sep -> Ast.List1 (p, sep)
- | "opt"; p = l1_simple_pattern -> Ast.Opt p
+ [ "list0"; p = l1_simple_pattern; sep = OPT sep ->
+ fun l -> Ast.List0 (p l, sep)
+ | "list1"; p = l1_simple_pattern; sep = OPT sep ->
+ fun l -> Ast.List1 (p l, sep)
+ | "opt"; p = l1_simple_pattern -> fun l -> Ast.Opt (p l)
]
];
l1_pattern_variable: [
[ "term"; precedence = NUMBER; id = IDENT ->
- Ast.TermVar (id, Some (int_of_string precedence))
+ Ast.TermVar (id, Ast.Level (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
l1_simple_pattern:
[ "layout" LEFTA
[ p1 = SELF; SYMBOL "\\sub"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Sub (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\sup"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Sup (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\below"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Below (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\above"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Above (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\over"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Over (p1, p2)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l)))
| p1 = SELF; SYMBOL "\\atop"; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Atop (p1, p2)))
-(* | "array"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
- return_term loc (Array (p, csep, rsep)) *)
- | SYMBOL "\\frac"; p1 = SELF; p2 = SELF ->
- return_term loc (Ast.Layout (Ast.Frac (p1, p2)))
- | SYMBOL "\\sqrt"; p = SELF -> return_term loc (Ast.Layout (Ast.Sqrt p))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l)))
+ | p1 = SELF; SYMBOL "\\frac"; p2 = SELF ->
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Frac (p1 l, p2 l)))
+ | SYMBOL "\\infrule"; p1 = SELF; p2 = SELF; p3 = SELF ->
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.InfRule (p1 l, p2 l, p3 l)))
+ | SYMBOL "\\sqrt"; p = SELF ->
+ return_term_of_level loc (fun l -> Ast.Layout (Ast.Sqrt p l))
| SYMBOL "\\root"; index = SELF; SYMBOL "\\of"; arg = SELF ->
- return_term loc (Ast.Layout (Ast.Root (arg, index)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Root (arg l, index l)))
| "hbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.H, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.H, false, false), p l)))
| "vbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.V, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.V, false, false), p l)))
| "hvbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.HV, false, false), p)))
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.HV, false, false), p l)))
| "hovbox"; LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (Ast.Layout (Ast.Box ((Ast.HOV, false, false), p)))
- | "break" -> return_term loc (Ast.Layout Ast.Break)
-(* | SYMBOL "\\SPACE" -> return_term loc (Layout Space) *)
+ return_term_of_level loc
+ (fun l -> Ast.Layout (Ast.Box ((Ast.HOV, false, false), p l)))
+ | "break" -> return_term_of_level loc (fun _ -> Ast.Layout Ast.Break)
| LPAREN; p = l1_pattern; RPAREN ->
- return_term loc (CicNotationUtil.group p)
+ return_term_of_level loc (fun l -> CicNotationUtil.group (p l))
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None)))
- | m = l1_magic_pattern -> return_term loc (Ast.Magic m)
- | v = l1_pattern_variable -> return_term loc (Ast.Variable v)
- | l = literal -> return_term loc (Ast.Literal l)
+ [ i = IDENT ->
+ return_term_of_level loc
+ (fun l -> Ast.Variable (Ast.TermVar (i,Ast.Self l)))
+ | m = l1_magic_pattern ->
+ return_term_of_level loc (fun l -> Ast.Magic (m l))
+ | v = l1_pattern_variable ->
+ return_term_of_level loc (fun _ -> Ast.Variable v)
+ | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
]
];
END
GLOBAL: level2_meta;
l2_variable: [
[ "term"; precedence = NUMBER; id = IDENT ->
- Ast.TermVar (id,Some (int_of_string precedence))
+ Ast.TermVar (id,Ast.Level (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
| "fresh"; id = IDENT -> Ast.FreshVar id
- | "anonymous" -> Ast.TermVar ("_",None)
- | id = IDENT -> Ast.TermVar (id,None)
+ | "anonymous" -> Ast.TermVar ("_",Ast.Self 0) (* is the level relevant?*)
+ | id = IDENT -> Ast.TermVar (id,Ast.Self 0)
]
];
l2_magic: [
];
binder: [
[ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
-(* | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
| SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
| vars = protected_binder_vars -> vars
]
];
- term: LEVEL "10N"
+ term: LEVEL "10"
[
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
- term: LEVEL "20N"
+ term: LEVEL "20"
[
- [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" ->
+ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19" ->
return_term loc (fold_cluster b vars typ body)
- | SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"->
- return_term loc (fold_exists vars typ body)
]
];
- term: LEVEL "70N"
+ term: LEVEL "70"
[
- [ p1 = term; p2 = term LEVEL "71N" ->
+ [ p1 = term; p2 = term LEVEL "71" ->
let rec aux = function
| Ast.Appl (hd :: tl)
| Ast.AttributedTerm (_, Ast.Appl (hd :: tl)) ->
return_term loc (Ast.Appl (aux p1 @ [p2]))
]
];
- term: LEVEL "90N"
+ term: LEVEL "90"
[
[ id = IDENT -> return_term loc (Ast.Ident (id, None))
| id = IDENT; s = explicit_subst ->
| Stdpp.Exc_located (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
-let parse_level1_pattern lexbuf =
+let parse_level1_pattern precedence lexbuf =
exc_located_wrapper
- (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+ (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf) precedence)
let parse_level2_ast lexbuf =
exc_located_wrapper
projects / helm.git / blobdiff