X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=829e78b6d0d16476e4e73a968436c2774ec523b5;hb=806ecbdd749ecf2a1cabff52b41cf748fe022401;hp=8ddb78781a1f74214bb7ad4cdebc8de8241693fc;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 8ddb78781..829e78b6d 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -170,18 +170,18 @@ let extract_term_production pattern = [NoBinding, gram_keyword s] | `Number s -> [NoBinding, gram_number s] and aux_layout = function - | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub"] @ aux p2 - | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup"] @ aux p2 - | 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.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sub "] @ aux p2 + | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol "\\sup "] @ aux p2 + | 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) -> - [NoBinding, gram_symbol "\\root"] @ aux p2 - @ [NoBinding, gram_symbol "\\of"] @ aux p1 - | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt"] @ aux p + [NoBinding, gram_symbol "\\root "] @ aux p2 + @ [NoBinding, gram_symbol "\\of "] @ aux p1 + | Ast.Sqrt p -> [NoBinding, gram_symbol "\\sqrt "] @ aux p | Ast.Break -> [] | Ast.Box (_, pl) -> List.flatten (List.map aux pl) | Ast.Group pl -> List.flatten (List.map aux pl) @@ -460,33 +460,33 @@ EXTEND v = [ PERCENTAGE ] -> id, v]]; l1_simple_pattern: [ "layout" LEFTA - [ p1 = SELF; SYMBOL "\\sub"; p2 = SELF -> + [ p1 = SELF; SYMBOL "\\sub "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Sub (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\sup"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\sup "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Sup (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\below"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\below "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Below (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\above"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\above "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Above (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\over"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\over "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Over (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\atop"; p2 = SELF -> + | p1 = SELF; SYMBOL "\\atop "; p2 = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Atop (p1 l, p2 l))) - | p1 = SELF; SYMBOL "\\frac"; p2 = SELF -> + | 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 -> + | 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 -> + | 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 -> + | SYMBOL "\\root "; index = SELF; SYMBOL "\\of "; arg = SELF -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Root (arg l, index l))) | "hbox"; LPAREN; p = l1_pattern; RPAREN -> @@ -581,13 +581,14 @@ EXTEND sort: [ [ "Prop" -> `Prop | "Set" -> `Set - | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n + | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n | "Type" -> `Type (CicUniv.fresh ()) + | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n | "CProp" -> `CProp (CicUniv.fresh ()) ] ]; explicit_subst: [ - [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *) + [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *) SYMBOL "["; substs = LIST1 [ i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) @@ -607,18 +608,21 @@ EXTEND [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> id, Some typ | arg = single_arg -> arg, None + | id = PIDENT -> Ast.Ident (id, None), None | SYMBOL "_" -> Ast.Ident ("_", None), None + | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN -> + Ast.Ident (id, None), Some typ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN -> Ast.Ident ("_", None), Some typ ] ]; match_pattern: [ - [ id = IDENT -> Ast.Pattern (id, None, []) + [ SYMBOL "_" -> Ast.Wildcard + | id = IDENT -> Ast.Pattern (id, None, []) | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> Ast.Pattern (id, None, vars) | id = IDENT; vars = LIST1 possibly_typed_name -> Ast.Pattern (id, None, vars) - | SYMBOL "_" -> Ast.Wildcard ] ]; binder: [ @@ -689,9 +693,11 @@ EXTEND ] ]; binder_vars: [ - [ vars = [ - l = LIST1 single_arg SEP SYMBOL "," -> l - | SYMBOL "_" -> [Ast.Ident ("_", None)] ]; + [ vars = [ l = + [ l = LIST1 single_arg SEP SYMBOL "," -> l + | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> + List.map (fun x -> Ast.Ident(x,None)) l + ] -> l ]; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) ] ]; @@ -706,7 +712,13 @@ EXTEND ]; term: LEVEL "10" [ - [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); + [ "let"; + var = + [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> + id, Some typ + | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> + Ast.Ident(id,None), ty ]; + SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) | LETCOREC; defs = let_defs; "in"; @@ -742,8 +754,10 @@ EXTEND return_term loc (Ast.Ident (id, Some s)) | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0)) | u = URI -> return_term loc (Ast.Uri (u, None)) + | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r)) | n = NUMBER -> return_term loc (Ast.Num (n, 0)) - | IMPLICIT -> return_term loc (Ast.Implicit) + | IMPLICIT -> return_term loc (Ast.Implicit `JustOne) + | SYMBOL <:unicode> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput | m = META -> return_term loc (Ast.Meta (int_of_string m, [])) | m = META; s = meta_substs -> @@ -802,6 +816,8 @@ let exc_located_wrapper f = with | Stdpp.Exc_located (floc, Stream.Error msg) -> raise (HExtlib.Localized (floc, Parse_error msg)) + | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) -> + raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) | Stdpp.Exc_located (floc, exn) -> raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))