X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=3ccd5414139bbd8886d90fc7ba12bdfc4675461d;hb=eac90ccb93a94f03df9ba5ad853cbd5d8c60b4f2;hp=53c60820c78632bd58f3b8527d697897537c92ff;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 53c60820c..3ccd54141 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -43,6 +43,7 @@ type ('a,'b,'c,'d,'e) grammars = { term: 'b Grammar.Entry.e; ident: 'e Grammar.Entry.e; let_defs: 'c Grammar.Entry.e; + located: Stdpp.location Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; } @@ -84,7 +85,10 @@ let level_of precedence = raise (Level_not_found precedence); string_of_int precedence -let gram_symbol s = Gramext.Stoken ("SYMBOL", s) +let gram_symbol s = + Gramext.srules + [ [ Gramext.Stoken ("SYMBOL",s) ], Gramext.action (fun _ loc -> loc) ] + let gram_ident status = Gramext.Snterm (Grammar.Entry.obj (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e)) @@ -110,7 +114,9 @@ let make_action action bindings = let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) - | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) + | NoBinding :: tl -> Gramext.action + (fun (loc: Ast.location) -> + aux (("",(Env.NoType,Env.LocValue loc))::vl) tl) (* LUCA: DEFCON 3 BEGIN *) | Binding (name, Env.TermType l) :: tl -> Gramext.action @@ -134,6 +140,7 @@ let make_action action bindings = aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl) | Env _ :: tl -> Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl) + | _ (* Binding (_,NoType) *) -> assert false (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -338,7 +345,7 @@ 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 ]) + Ast.Appl [ Ast.Symbol ("exists", None); lambda ]) terms body let fold_binder binder pt_names body = @@ -568,16 +575,6 @@ EXTEND | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n ] ]; - explicit_subst: [ - [ SYMBOL "\\subst "; (* to avoid catching frequent "a [1]" cases *) - SYMBOL "["; - substs = LIST1 [ - i = IDENT; SYMBOL <:unicode> (* ≔ *); t = term -> (i, t) - ] SEP SYMBOL ";"; - SYMBOL "]" -> - substs - ] - ]; meta_subst: [ [ s = SYMBOL "_" -> None | p = term -> Some p ] @@ -589,12 +586,12 @@ 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 + | id = PIDENT -> Ast.Ident (id, `Ambiguous), None + | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN -> - Ast.Ident (id, None), Some typ + Ast.Ident (id, `Ambiguous), Some typ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN -> - Ast.Ident ("_", None), Some typ + Ast.Ident ("_", `Ambiguous), Some typ ] ]; match_pattern: [ @@ -612,27 +609,34 @@ EXTEND | SYMBOL <:unicode> (* λ *) -> `Lambda ] ]; + tident: [ + [ uri = HREF; + id = IDENT; + HREFEND -> (id, `Uri uri) ]]; + gident: [ + [ fullident = tident -> fullident; + | id = IDENT -> (id, `Ambiguous) ]]; arg: [ - [ LPAREN; names = LIST1 IDENT SEP SYMBOL ","; + [ LPAREN; names = LIST1 gident SEP SYMBOL ","; SYMBOL ":"; ty = term; RPAREN -> - List.map (fun n -> Ast.Ident (n, None)) names, Some ty - | name = IDENT -> [Ast.Ident (name, None)], None + List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty + | (name,uri) = gident -> [Ast.Ident (name,uri)], None | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) -> [meta], None - | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None + | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None | _ -> failwith "Invalid bound name." ] ]; single_arg: [ - [ name = IDENT -> Ast.Ident (name, None) + [ (name,uri) = gident -> Ast.Ident (name,uri) | blob = UNPARSED_META -> let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) | Ast.Variable (Ast.IdentVar _) -> meta - | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None) + | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous) | _ -> failwith "Invalid index name." ] ]; @@ -649,6 +653,9 @@ EXTEND | _ -> failwith ("Invalid index name: " ^ blob) ] ]; + located: [ + [ s = SYMBOL -> loc ] + ]; let_defs: [ [ defs = LIST1 [ name = single_arg; @@ -692,7 +699,7 @@ EXTEND [ vars = [ l = [ l = LIST1 single_arg SEP SYMBOL "," -> l | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> - List.map (fun x -> Ast.Ident(x,None)) l + List.map (fun x -> Ast.Ident(x,`Ambiguous)) l ] -> l ]; typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ) ] @@ -712,8 +719,8 @@ EXTEND 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 ]; + | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> + Ast.Ident (id,uri), ty ]; SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) @@ -745,13 +752,12 @@ EXTEND ]; term: LEVEL "90" [ - [ id = IDENT -> return_term loc (Ast.Ident (id, None)) - | id = IDENT; s = explicit_subst -> - 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)) + [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri)) + | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None)) + | u = URI -> return_term loc (Ast.Ident + (NUri.name_of_uri (NUri.uri_of_string u), `Uri u)) | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r)) - | n = NUMBER -> return_term loc (Ast.Num (n, 0)) + | n = NUMBER -> return_term loc (Ast.Num (n, None)) | IMPLICIT -> return_term loc (Ast.Implicit `JustOne) | SYMBOL <:unicode> -> return_term loc (Ast.Implicit `Vector) | PLACEHOLDER -> return_term loc Ast.UserInput @@ -796,6 +802,7 @@ let initial_grammars keywords = let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in let term = Grammar.Entry.create level2_ast_grammar "term" in let ident = Grammar.Entry.create level2_ast_grammar "ident" in + let located = Grammar.Entry.create level2_ast_grammar "located" in let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in @@ -805,6 +812,7 @@ let initial_grammars keywords = term=term; ident=ident; let_defs=let_defs; + located=located; protected_binder_vars=protected_binder_vars; level2_meta=level2_meta; level2_ast_grammar=level2_ast_grammar; @@ -843,7 +851,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action = Some (Gramext.Level level), [ None, Some (*Gramext.NonA*) Gramext.NonA, - [ p_atoms, + [ p_atoms, (* concrete l1 syntax *) (make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc))