X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=829e78b6d0d16476e4e73a968436c2774ec523b5;hb=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;hp=695db149e3f0c2bc722629d589b8bfc39f61adb9;hpb=e78cf74f8976cf0ca554f64baa9979d0423ee927;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 695db149e..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,14 +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; SYMBOL "]" -> `NCProp n + | "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) @@ -712,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"; @@ -748,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 -> @@ -808,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))))