From: Stefano Zacchiroli Date: Wed, 4 Feb 2004 09:41:35 +0000 (+0000) Subject: - added support for implicit in concrete syntax X-Git-Tag: V_0_2_3~81 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7aee283a4fee4fca3fc1d53619c366f793f1e694;p=helm.git - added support for implicit in concrete syntax - ported to new Ast --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index b339b8dc4..bcc8fda28 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -40,6 +40,7 @@ let regexp ident_cont' = ident_cont | tex_token let regexp ident = (alpha ident_cont*) | ('_' ident_cont+) let regexp ident' = ((alpha | tex_token) ident_cont'*) | ('_' ident_cont'+) let regexp paren = [ '(' '[' '{' ')' ']' '}' ] +let regexp implicit = '?' let regexp meta = '?' num let regexp qstring = '"' [^ '"']* '"' let regexp uri = @@ -99,6 +100,7 @@ let rec token = lexer | num -> return lexbuf ("NUM", Ulexing.utf8_lexeme lexbuf) | paren -> return lexbuf ("PAREN", Ulexing.utf8_lexeme lexbuf) | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) + | implicit -> return lexbuf ("IMPLICIT", Ulexing.utf8_lexeme lexbuf) | qstring -> let lexeme = Ulexing.utf8_lexeme lexbuf in let s = String.sub lexeme 1 (String.length lexeme - 2) in diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 2806becc1..397d03867 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -46,8 +46,7 @@ let term0 = Grammar.Entry.create grammar "term0" (* let tactic = Grammar.Entry.create grammar "tactic" *) (* let tactical = Grammar.Entry.create grammar "tactical" *) -let return_term loc term = - CicTextualParser2Ast.AttributedTerm (`Loc loc, term) +let return_term loc term = CicAst.AttributedTerm (`Loc loc, term) (* let return_term loc term = term *) let fail (x, y) msg = @@ -88,8 +87,8 @@ EXTEND substs ] -> (match subst with - | Some l -> CicTextualParser2Ast.Ident (s, l) - | None -> CicTextualParser2Ast.Ident (s, [])) + | Some l -> CicAst.Ident (s, l) + | None -> CicAst.Ident (s, [])) ] ]; name: [ (* as substituted_name with no explicit substitution *) @@ -106,7 +105,7 @@ EXTEND [ "arrow" RIGHTA [ t1 = term; SYMBOL <:unicode>; t2 = term -> return_term loc - (CicTextualParser2Ast.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) + (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2)) ] | "binder" RIGHTA [ @@ -117,14 +116,14 @@ EXTEND List.fold_right (fun var body -> let name = name_of_string var in - CicTextualParser2Ast.Binder (b, (name, typ), body)) + CicAst.Binder (b, (name, typ), body)) vars body in return_term loc binder ] | "eq" LEFTA [ t1 = term; SYMBOL "="; t2 = term -> - return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2])) + return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2]) ] | "add" LEFTA [ (* nothing here by default *) ] | "mult" LEFTA [ (* nothing here by default *) ] @@ -134,11 +133,12 @@ EXTEND sort_kind = [ "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp ] -> - CicTextualParser2Ast.Sort sort_kind + CicAst.Sort sort_kind | n = substituted_name -> return_term loc n | PAREN "("; head = term; args = LIST1 term; PAREN ")" -> - return_term loc (CicTextualParser2Ast.Appl (head :: args)) - | i = NUM -> return_term loc (CicTextualParser2Ast.Num (i, 0)) + return_term loc (CicAst.Appl (head :: args)) + | i = NUM -> return_term loc (CicAst.Num (i, 0)) + | IMPLICIT -> return_term loc CicAst.Implicit | m = META; substs = [ PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" -> @@ -150,7 +150,7 @@ EXTEND with Failure "int_of_string" -> fail loc ("Invalid meta variable number: " ^ m) in - return_term loc (CicTextualParser2Ast.Meta (index, substs)) + return_term loc (CicAst.Meta (index, substs)) (* actually "in" and "and" are _not_ keywords. Parsing works anyway * since applications are required to be bound by parens *) | "let"; var = typed_name; @@ -158,7 +158,7 @@ EXTEND SYMBOL "="; t1 = term; IDENT "in"; t2 = term -> - return_term loc (CicTextualParser2Ast.LetIn (var, t1, t2)) + return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; defs = LIST1 [ var = typed_name; @@ -171,7 +171,7 @@ EXTEND (var, t1, (match index with None -> 0 | Some i -> i)) ] SEP (IDENT "and"); IDENT "in"; body = term -> - return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body)) + return_term loc (CicAst.LetRec (ind_kind, defs, body)) | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ]; "match"; t = term; SYMBOL ":"; indty = IDENT; @@ -179,11 +179,11 @@ EXTEND PAREN "["; patterns = LIST0 [ lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> - ((lhs: CicTextualParser2Ast.case_pattern), rhs) + ((lhs: CicAst.case_pattern), rhs) ] SEP SYMBOL "|"; PAREN "]" -> return_term loc - (CicTextualParser2Ast.Case (t, indty, outtyp, patterns)) + (CicAst.Case (t, indty, outtyp, patterns)) | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli index 0f13d116a..aec7c8f1d 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli @@ -27,19 +27,17 @@ exception Parse_error of string (** {2 Parsing functions} *) -val parse_term: char Stream.t -> CicTextualParser2Ast.term +val parse_term: char Stream.t -> CicAst.term (** {2 Grammar extensions} *) -val term: CicTextualParser2Ast.term Grammar.Entry.e (** recursive rule *) -val term0: CicTextualParser2Ast.term Grammar.Entry.e (** top level rule *) +val term: CicAst.term Grammar.Entry.e (** recursive rule *) +val term0: CicAst.term Grammar.Entry.e (** top level rule *) -val return_term: - CicTextualParser2Ast.location -> CicTextualParser2Ast.term -> - CicTextualParser2Ast.term +val return_term: CicAst.location -> CicAst.term -> CicAst.term (** raise a parse error *) -val fail: CicTextualParser2Ast.location -> string -> 'a +val fail: CicAst.location -> string -> 'a (**/**)