From cfb41205e930ede65c1d19ec7ec6f252e0803d55 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 27 May 2009 17:16:31 +0000 Subject: [PATCH] - Procedural: we specify more unifiers for apply to help higher-order unification - cicNotationPp: bugfix in the notation for Meta and ImplicitPattern - transcript: grafite lexer/parser updated --- .../components/acic_content/cicNotationPp.ml | 4 +-- .../components/acic_procedural/procedural2.ml | 31 +++++++++++++------ .../binaries/transcript/grafiteLexer.mll | 2 ++ .../binaries/transcript/grafiteParser.mly | 9 +++--- 4 files changed, 30 insertions(+), 16 deletions(-) diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index a835e074f..b2cb12f92 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -147,7 +147,7 @@ let rec pp_term ?(pp_parens = true) t = | Ast.Meta (index, substs) -> sprintf "%d[%s]" index (String.concat "; " - (List.map (function None -> "_" | Some t -> pp_term t) substs)) + (List.map (function None -> "?" | Some t -> pp_term t) substs)) | Ast.Num (num, _) -> num | Ast.Sort `Set -> "Set" | Ast.Sort `Prop -> "Prop" @@ -358,7 +358,7 @@ let pp_env env = let rec pp_cic_appl_pattern = function | Ast.UriPattern uri -> UriManager.string_of_uri uri | Ast.VarPattern name -> name - | Ast.ImplicitPattern -> "_" + | Ast.ImplicitPattern -> "?" | Ast.ApplPattern aps -> sprintf "(%s)" (String.concat " " (List.map pp_cic_appl_pattern aps)) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 46d4431bd..45444f4fc 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -171,19 +171,31 @@ let get_type msg st t = H.get_type msg st.context (H.cic t) let anonymous_premise = C.Name "UNNAMED" -let mk_exp_args hd tl classes synth = +let mk_exp_args hd tl classes synth qs = + let exp = ref 0 in let meta id = C.AImplicit (id, None) in let map v (cl, b) = - if I.overlaps synth cl && b then v else meta "" + if I.overlaps synth cl then + let w = if H.is_atomic (H.cic v) then v else meta "" in + if b then v, v else meta "", w + else + meta "", meta "" in - let rec aux b = function - | [] -> b, [] + let rec rev a = function + | [] -> a | hd :: tl -> - if hd = meta "" then aux true tl else b, List.rev (hd :: tl) + if snd hd <> meta "" then incr exp; + rev (snd hd :: a) tl + in + let rec aux = function + | [] -> [] + | hd :: tl -> + if fst hd = meta "" then aux tl else rev [] (hd :: tl) in let args = T.list_rev_map2 map tl classes in - let b, args = aux false args in - if args = [] then b, hd else b, C.AAppl ("", hd :: args) + let args = aux args in + let part = !exp < List.length tl in + if args = [] then part, hd, qs else part, C.AAppl ("", hd :: args), qs let mk_convert st ?name sty ety note = let ppterm t = @@ -342,6 +354,7 @@ and proc_appl st what hd tl = let diff = goal_arity - decurry in if diff < 0 then let text = Printf.sprintf "partial application: %i" diff in + prerr_endline ("Procedural 2: " ^ text); [T.Exact (what, dtext ^ text)] else let classes = Cl.adjust st.context tl ?goal classes in @@ -366,7 +379,7 @@ and proc_appl st what hd tl = in if List.length qs <> List.length names then let qs = proc_bkd_proofs (next st) synth [] classes tl in - let b, hd = mk_exp_args hd tl classes synth in + let b, hd, qs = mk_exp_args hd tl classes synth qs in script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else if is_rewrite_right st hd then script2 @ mk_rewrite st dtext where qs tl2 false what ety @@ -381,7 +394,7 @@ and proc_appl st what hd tl = | _ -> let names = get_sub_names hd tl in let qs = proc_bkd_proofs (next st) synth names classes tl in - let b, hd = mk_exp_args hd tl classes synth in + let b, hd, qs = mk_exp_args hd tl classes synth qs in script @ [tactic b hd (dtext ^ text); T.Branch (qs, "")] else [T.Exact (what, dtext)] diff --git a/helm/software/components/binaries/transcript/grafiteLexer.mll b/helm/software/components/binaries/transcript/grafiteLexer.mll index bfa818e30..ac3055bc5 100644 --- a/helm/software/components/binaries/transcript/grafiteLexer.mll +++ b/helm/software/components/binaries/transcript/grafiteLexer.mll @@ -62,12 +62,14 @@ rule token = parse | "default" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } | "include" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } | "inline" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } + | "pump" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s } | "qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s } | "elim" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } | "apply" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } | "intros" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } | "assume" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } | "the" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } + | "rewrite" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s } | IDENT { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s } | "." SPC { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } | "." { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s } diff --git a/helm/software/components/binaries/transcript/grafiteParser.mly b/helm/software/components/binaries/transcript/grafiteParser.mly index 03ca0cdf4..82295c69b 100644 --- a/helm/software/components/binaries/transcript/grafiteParser.mly +++ b/helm/software/components/binaries/transcript/grafiteParser.mly @@ -129,13 +129,12 @@ { out "TH" $3; let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b, [])] } - | UNX line drops - { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } - | PS steps - { [] } + | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] } + | PS steps { out "PS" $2; [] } + | QED FS { [] } ; items: | EOF { [] } | item items { $1 @ $2 } /* | error { out "ERROR" ""; failwith ("item id " ^ "") } */ - ; + ; -- 2.39.2