X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=32b6b0a9068312564dcc8c65648b12892a6f4bc3;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=13817e248e08b013c31c212cb92a5fdb8478f24d;hpb=1ca0ec89cfc2c3f85af95d5b1bdad07597d976bd;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 13817e248..32b6b0a90 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -46,8 +46,6 @@ let term = Grammar.Entry.create level2_ast_grammar "term" 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 @@ -78,7 +76,7 @@ let make_action action bindings = 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) -> @@ -101,7 +99,7 @@ let make_action action bindings = 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) @@ -271,6 +269,13 @@ let fold_cluster binder terms ty body = (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) @@ -278,15 +283,23 @@ let fold_binder binder pt_names 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 @@ -396,7 +409,8 @@ EXTEND 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 @@ -409,7 +423,7 @@ EXTEND sort: [ [ "Prop" -> `Prop | "Set" -> `Set - | "Type" -> `Type + | "Type" -> `Type (CicUniv.fresh ()) | "CProp" -> `CProp ] ]; @@ -437,14 +451,14 @@ EXTEND ] ]; 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 - | SYMBOL <:unicode> (* ∃ *) -> `Exists +(* | SYMBOL <:unicode> |+ ∃ +| -> `Exists *) | SYMBOL <:unicode> (* ∀ *) -> `Forall | SYMBOL <:unicode> (* λ *) -> `Lambda ] @@ -455,7 +469,7 @@ EXTEND 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 @@ -465,9 +479,10 @@ EXTEND 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." ] @@ -540,6 +555,9 @@ EXTEND [ [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term -> return_term loc (fold_cluster b vars typ body) + | SYMBOL <:unicode> (* ∃ *); + (vars, typ) = binder_vars; SYMBOL "."; body = term -> + return_term loc (fold_exists vars typ body) ] ]; term: LEVEL "70L" (* apply *) @@ -568,9 +586,9 @@ EXTEND | 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> (* ⇒ *); @@ -582,7 +600,8 @@ EXTEND | 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 @@ -599,12 +618,17 @@ let exc_located_wrapper f = | 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;