(** {2 Grammar extension} *)
+let level_of precedence =
+ if precedence < min_precedence || precedence > max_precedence then
+ raise (Level_not_found precedence);
+ string_of_int precedence ^ "N"
+
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 = Gramext.Sself
+let gram_term = function
+ | None -> Gramext.Sself
+ | Some (precedence) ->
+ Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence)
+;;
let gram_of_literal =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
(* LUCA: DEFCON 3 BEGIN *)
- | Binding (name, Env.TermType) :: tl ->
+ | Binding (name, Env.TermType l) :: tl ->
Gramext.action
(fun (v:Ast.term) ->
- aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+ aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
| Binding (name, Env.StringType) :: tl ->
Gramext.action
(fun (v:string) ->
| Ast.List0 (p, _)
| Ast.List1 (p, _) ->
let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-(* let env0 = List.map list_binding_of_name p_names in
- let grow_env_entry env n v =
- List.map
- (function
- | (n', (ty, ListValue vl)) as entry ->
- if n' = n then n', (ty, ListValue (v :: vl)) else entry
- | _ -> assert false)
- env
- in
- let grow_env env_i env =
- List.fold_left
- (fun env (n, (_, v)) -> grow_env_entry env n v)
- env env_i
- in *)
let action (env_list : CicNotationEnv.t list) (loc : Ast.location) =
CicNotationEnv.coalesce_env p_names env_list
in
and aux_variable =
function
| Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
- | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+ | Ast.TermVar (s,level) ->
+ [Binding (s, Env.TermType level), gram_term level]
| Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
| Ast.Ascription (p, s) -> assert false (* TODO *)
| Ast.FreshVar _ -> assert false
in
aux pattern
-let level_of precedence associativity =
- if precedence < min_precedence || precedence > max_precedence then
- raise (Level_not_found precedence);
- let assoc_string =
- match associativity with
- | Gramext.NonA -> "N"
- | Gramext.LeftA -> "L"
- | Gramext.RightA -> "R"
- in
- string_of_int precedence ^ assoc_string
-
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
let owned_keywords = Hashtbl.create 23
-let extend level1_pattern ~precedence ~associativity action =
+type checked_l1_pattern = CL1P of CicNotationPt.term * int
+
+let check_l1_pattern level1_pattern level associativity =
+ let variables = ref 0 in
+ let symbols = ref 0 in
+ let rec aux = function
+ | Ast.AttributedTerm (att, t) -> Ast.AttributedTerm (att,aux t)
+ | 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)
+ | 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.Sup (p1, p2) -> let p1 = aux p1 in let p2 = aux p2 in Ast.Sup (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.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)
+ | Ast.Sqrt p -> Ast.Sqrt (aux p)
+ | Ast.Break as t -> t
+ | Ast.Box (b, pl) -> Ast.Box(b, List.map aux pl)
+ | Ast.Group pl -> Ast.Group (List.map aux pl)
+ and aux_magic magic =
+ match magic with
+ | Ast.Opt p -> Ast.Opt (aux p)
+ | Ast.List0 (p, x) -> Ast.List0 (aux p, x)
+ | Ast.List1 (p, x) -> Ast.List1 (aux p, x)
+ | _ -> assert false
+ and aux_variable =
+ function
+ | Ast.NumVar _ as t -> t
+ | Ast.TermVar (s,None) 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))
+ | _ -> assert false)
+ | Ast.TermVar (s,Some _) 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
+ | 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
+ if !variables <> 2 && associativity <> Gramext.NonA then
+ raise (Parse_error ("Exactly 2 variables must be specified in an "^
+ "associative notation"));
+ cp
+;;
+
+let extend (CL1P (level1_pattern,precedence)) action =
let p_bindings, p_atoms =
List.split (extract_term_production level1_pattern)
in
- let level = level_of precedence associativity in
-(* let p_names = flatten_opt p_bindings in *)
+ let level = level_of precedence in
let _ =
Grammar.extend
[ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
Some (Gramext.Level level),
[ None,
- Some associativity,
+ Some (*Gramext.NonA*) Gramext.NonA,
[ p_atoms,
(make_action
(fun (env: CicNotationEnv.t) (loc: Ast.location) ->
| i when i < first -> acc
| i ->
aux
- ((Some (string_of_int i ^ "N"), Some Gramext.NonA, dummy_prod)
- :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, dummy_prod)
- :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, dummy_prod)
+ ((Some (string_of_int i ^ "N"), Some (*Gramext.NonA*)Gramext.NonA, dummy_prod)
:: acc)
(i - 1)
in
]
];
l1_pattern_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; id = IDENT ->
+ Ast.TermVar (id, Some (int_of_string precedence))
| "number"; id = IDENT -> Ast.NumVar id
| "ident"; id = IDENT -> Ast.IdentVar id
]
return_term loc (CicNotationUtil.group p)
]
| "simple" NONA
- [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+ [ 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)
EXTEND
GLOBAL: level2_meta;
l2_variable: [
- [ "term"; id = IDENT -> Ast.TermVar id
+ [ "term"; precedence = NUMBER; id = IDENT ->
+ Ast.TermVar (id,Some (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 "_"
- | id = IDENT -> Ast.TermVar id
+ | "anonymous" -> Ast.TermVar ("_",None)
+ | id = IDENT -> Ast.TermVar (id,None)
]
];
l2_magic: [
[ "Prop" -> `Prop
| "Set" -> `Set
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp" -> `CProp
+ | "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
id, Some typ
| arg = single_arg -> arg, None
| SYMBOL "_" -> Ast.Ident ("_", None), None
+ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+ Ast.Ident ("_", None), Some typ
]
];
match_pattern: [
- [ id = IDENT -> id, None, []
+ [ id = IDENT -> Ast.Pattern (id, None, [])
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
- id, None, vars
+ Ast.Pattern (id, None, vars)
+ | id = IDENT; vars = LIST1 possibly_typed_name ->
+ Ast.Pattern (id, None, vars)
+ | SYMBOL "_" -> Ast.Wildcard
]
];
binder: [
let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
match meta with
| Ast.Variable (Ast.FreshVar _) -> [meta], None
- | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
+ | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
| _ -> failwith "Invalid bound name."
]
];
match meta with
| Ast.Variable (Ast.FreshVar _)
| Ast.Variable (Ast.IdentVar _) -> meta
- | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+ | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
| _ -> failwith "Invalid index name."
]
];
- induction_kind: [
- [ "rec" -> `Inductive
- | "corec" -> `CoInductive
- ]
- ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
| vars = protected_binder_vars -> vars
]
];
- term: LEVEL "10N" [ (* let in *)
+ term: LEVEL "10N"
+ [
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
- | "let"; k = induction_kind; defs = let_defs; "in";
+ | LETCOREC; defs = let_defs; "in";
+ body = term ->
+ return_term loc (Ast.LetRec (`CoInductive, defs, body))
+ | LETREC; defs = let_defs; "in";
body = term ->
- return_term loc (Ast.LetRec (k, defs, body))
+ return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
- term: LEVEL "20R" (* binder *)
+ term: LEVEL "20N"
[
- [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
+ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N" ->
return_term loc (fold_cluster b vars typ body)
| SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
+ (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term LEVEL "19N"->
return_term loc (fold_exists vars typ body)
]
];
- term: LEVEL "70L" (* apply *)
+ term: LEVEL "70N"
[
- [ p1 = term; p2 = term ->
+ [ p1 = term; p2 = term LEVEL "71N" ->
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" (* simple *)
+ term: LEVEL "90N"
[
[ id = IDENT -> return_term loc (Ast.Ident (id, None))
| id = IDENT; s = explicit_subst ->
projects / helm.git / blobdiff