let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
-let return_term loc term = ()
-
let int_of_string s =
try
Pervasives.int_of_string s
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
| NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
- (* LUCA: DEFCON 5 BEGIN *)
+ (* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType) :: tl ->
Gramext.action
(fun (v:Ast.term) ->
aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
| Env _ :: tl ->
Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
- (* LUCA: DEFCON 5 END *)
+ (* LUCA: DEFCON 3 END *)
in
aux [] (List.rev bindings)
(fun term body -> Ast.Binder (binder, (term, ty), body))
terms body (* terms are names: either Ident or FreshVar *)
+let fold_exists terms ty body =
+ List.fold_right
+ (fun term body ->
+ let lambda = Ast.Binder (`Lambda, (term, ty), body) in
+ Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+ terms body
+
let fold_binder binder pt_names body =
List.fold_right
(fun (names, ty) body -> fold_cluster binder names ty body)
let return_term loc term = Ast.AttributedTerm (`Loc loc, term)
-let _ = (* create empty precedence level for "term" *)
+ (* create empty precedence level for "term" *)
+let _ =
+ let dummy_action =
+ Gramext.action (fun _ ->
+ failwith "internal error, lexer generated a dummy token")
+ in
+ (* Needed since campl4 on "delete_rule" remove the precedence level if it gets
+ * empty after the deletion. The lexer never generate the Stoken below. *)
+ let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
let mk_level_list first last =
let rec aux acc = function
| i when i < first -> acc
| i ->
aux
- ((Some (string_of_int i ^ "N"), Some Gramext.NonA, [])
- :: (Some (string_of_int i ^ "L"), Some Gramext.LeftA, [])
- :: (Some (string_of_int i ^ "R"), Some Gramext.RightA, [])
+ ((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)
:: acc)
(i - 1)
in
level2_meta: [
[ magic = l2_magic -> Ast.Magic magic
| var = l2_variable -> Ast.Variable var
- | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
+ | blob = UNPARSED_AST ->
+ !parse_level2_ast_ref (Ulexing.from_utf8_string blob)
]
];
END
sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
- | "Type" -> `Type
+ | "Type" -> `Type (CicUniv.fresh ())
| "CProp" -> `CProp
]
];
]
];
match_pattern: [
- [ id = IDENT -> id, []
+ [ id = IDENT -> id, None, []
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
- id, vars
+ id, None, vars
]
];
binder: [
[ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
- | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+(* | SYMBOL <:unicode<exists>> |+ ∃ +| -> `Exists *)
| SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
| SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
]
List.map (fun n -> Ast.Ident (n, None)) names, Some ty
| name = IDENT -> [Ast.Ident (name, None)], None
| blob = UNPARSED_META ->
- let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+ 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
single_arg: [
[ name = IDENT -> Ast.Ident (name, None)
| blob = UNPARSED_META ->
- let meta = !parse_level2_meta_ref (Stream.of_string blob) in
+ let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
match meta with
- | Ast.Variable (Ast.FreshVar _) -> meta
+ | Ast.Variable (Ast.FreshVar _)
+ | Ast.Variable (Ast.IdentVar _) -> meta
| Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
| _ -> failwith "Invalid index name."
]
[
[ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
return_term loc (fold_cluster b vars typ body)
+ | SYMBOL <:unicode<exists>> (* ∃ *);
+ (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ return_term loc (fold_exists vars typ body)
]
];
term: LEVEL "70L" (* apply *)
| m = META; s = meta_substs ->
return_term loc (Ast.Meta (int_of_string m, s))
| s = sort -> return_term loc (Ast.Sort s)
- | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
- "match"; t = term;
- indty_ident = OPT [ "in"; id = IDENT -> id ];
+ | "match"; t = term;
+ indty_ident = OPT [ "in"; id = IDENT -> id, None ];
+ outtyp = OPT [ "return"; ty = term -> ty ];
"with"; SYMBOL "[";
patterns = LIST0 [
lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
| LPAREN; p1 = term; SYMBOL ":"; p2 = term; RPAREN ->
return_term loc (Ast.Cast (p1, p2))
| LPAREN; p = term; RPAREN -> p
- | blob = UNPARSED_META -> !parse_level2_meta_ref (Stream.of_string blob)
+ | blob = UNPARSED_META ->
+ !parse_level2_meta_ref (Ulexing.from_utf8_string blob)
]
];
END
| Stdpp.Exc_located (floc, exn) ->
raise (Parse_error (floc, (Printexc.to_string exn)))
-let parse_level1_pattern stream =
- exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
-let parse_level2_ast stream =
- exc_located_wrapper (fun () -> Grammar.Entry.parse level2_ast stream)
-let parse_level2_meta stream =
- exc_located_wrapper (fun () -> Grammar.Entry.parse level2_meta stream)
+let parse_level1_pattern lexbuf =
+ exc_located_wrapper
+ (fun () -> Grammar.Entry.parse level1_pattern (Obj.magic lexbuf))
+
+let parse_level2_ast lexbuf =
+ exc_located_wrapper
+ (fun () -> Grammar.Entry.parse level2_ast (Obj.magic lexbuf))
+
+let parse_level2_meta lexbuf =
+ exc_located_wrapper
+ (fun () -> Grammar.Entry.parse level2_meta (Obj.magic lexbuf))
let _ =
parse_level1_pattern_ref := parse_level1_pattern;
projects / helm.git / blobdiff