From fa143d13b855aa48a11f3230a139f39ce2df0984 Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Mon, 11 Jul 2005 13:54:09 +0000 Subject: [PATCH] * added backtracking in matching code (hairy code!) --- helm/ocaml/cic_notation/TODO | 8 ++++---- helm/ocaml/cic_notation/cicNotationMatcher.ml | 18 +++++++++++++----- helm/ocaml/cic_notation/cicNotationMatcher.mli | 6 +++--- 3 files changed, 20 insertions(+), 12 deletions(-) diff --git a/helm/ocaml/cic_notation/TODO b/helm/ocaml/cic_notation/TODO index 2ba0283ce..73a2a49a6 100644 --- a/helm/ocaml/cic_notation/TODO +++ b/helm/ocaml/cic_notation/TODO @@ -3,25 +3,25 @@ TODO * implementare trasformazione 1 => 0 * gestione priorita'/associativita' - - annotazioni nel livello 1 generato? - triplicare livelli nella grammatica? * implementare type-checker per le trasformazioni * prestazioni trasformazioni 3 => 2 e 2 => 1 -* problema con pattern overlapping per i magic al livello 2 * magic per gestione degli array? * gestione speciale dei numeri -* gestione greedyness dei magic in 2 => 1 * sintassi concreta / prelexing - studiare/implementare sintassi con ... per i magic fold * integrazione - porting della disambiguazione al nuovo ast - apportare all'ast le modifiche di CicAst (case, cast non come annotazione, tipi opzionali nel let rec e nelle definizioni) -* href multipli DONE * implementare istanziazione dei magic a livello 1 (2 => 1) * implementare compilazione dei default in 2 => 1 -> Tue, 07 Jun 2005 17:17:36 +0200 zack +* annotazioni nel livello 1 generato +* problema con pattern overlapping per i magic al livello 2 +* gestione greedyness dei magic in 2 => 1 +* href multipli diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml index 6b1266ec8..1a0c02410 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.ml +++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml @@ -139,7 +139,18 @@ struct k else if are_empty t then let res = match_cb (matched t) in - (fun matched_terms _ -> res matched_terms) + (fun matched_terms terms -> + match res matched_terms with + None -> + begin + (* the match has failed, we rollback the last matched term + * into the unmatched ones and call the failure continuation + *) + match matched_terms with + hd :: tl -> k tl (hd :: terms) + | _ -> assert false + end + | Some v -> Some v) else match horizontal_split t with | _, [], _ -> assert false @@ -331,12 +342,9 @@ struct (fun term env -> prerr_endline "GUARDIA?" ; match compiled_guard term with - | None -> - prerr_endline "SONO CAZZI H2SO4" ; - None + | None -> None | Some _ -> begin - prerr_endline "OKKKKKKKKKKKKKK" ; match compiled_p term with | None -> None | Some (env', _) -> diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.mli b/helm/ocaml/cic_notation/cicNotationMatcher.mli index 55de82999..4abb5b8bc 100644 --- a/helm/ocaml/cic_notation/cicNotationMatcher.mli +++ b/helm/ocaml/cic_notation/cicNotationMatcher.mli @@ -39,9 +39,9 @@ module Matcher (P: PATTERN) : sig val compiler: (P.pattern_t * int) list -> - ((P.pattern_t list * int) list -> P.term_t list -> 'a) -> - (unit -> 'a) -> - (P.term_t -> 'a) + ((P.pattern_t list * int) list -> P.term_t list -> 'a option) -> + (unit -> 'a option) -> + (P.term_t -> 'a option) end module Matcher21: -- 2.39.2