From bdf8492f9e68500178dccde1c6f8614296f7c7dc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 22 Dec 2002 19:05:38 +0000 Subject: [PATCH] New constructs \x.T and !x.T introduced. They require refinement. --- .../cic_textual_parser/cicTextualParser.mly | 36 ++++++++++++++++--- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly index bb9113403..1d4bd933d 100644 --- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly +++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly @@ -410,13 +410,39 @@ pihead: let dom,mk_expr = $2 in Anonymous, (dom, function interp -> mk_expr interp) } + | PROD ID DOT + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; + let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + CicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl) + ] @ !CicTextualParser0.metasenv ; + Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) + } ; lambdahead: - LAMBDA ID COLON expr DOT - { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ; - let dom,mk_expr = $4 in - Cic.Name $2, (dom, function interp -> mk_expr interp) - } + LAMBDA ID COLON expr DOT + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; + let dom,mk_expr = $4 in + Cic.Name $2, (dom, function interp -> mk_expr interp) + } + | LAMBDA ID DOT + { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders; + let newmeta = new_meta () in + let new_canonical_context = [] in + let irl = + identity_relocation_list_for_metavariable new_canonical_context + in + CicTextualParser0.metasenv := + [newmeta, new_canonical_context, Sort Type ; + newmeta+1, new_canonical_context, Meta (newmeta,irl) + ] @ !CicTextualParser0.metasenv ; + Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl)) + } ; letinhead: LAMBDA ID LETIN expr DOT -- 2.39.2