From 6627bb6bb1c3ae3ce70bcfe4d59997a94bec8b18 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 20 Sep 2005 15:30:17 +0000 Subject: [PATCH] changed ast representation of exists --- helm/ocaml/cic_notation/cicNotationParser.ml | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index 933397067..45ff3d233 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -78,7 +78,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 4 BEGIN *) | Binding (name, Env.TermType) :: tl -> Gramext.action (fun (v:Ast.term) -> @@ -101,7 +101,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 4 END *) in aux [] (List.rev bindings) @@ -271,6 +271,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) @@ -452,7 +459,7 @@ EXTEND ]; binder: [ [ SYMBOL <:unicode> (* Π *) -> `Pi - | SYMBOL <:unicode> (* ∃ *) -> `Exists +(* | SYMBOL <:unicode> |+ ∃ +| -> `Exists *) | SYMBOL <:unicode> (* ∀ *) -> `Forall | SYMBOL <:unicode> (* λ *) -> `Lambda ] @@ -475,7 +482,8 @@ EXTEND | blob = UNPARSED_META -> let meta = !parse_level2_meta_ref (Stream.of_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." ] @@ -548,6 +556,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 *) -- 2.39.2