Commit 5ee3ef4d authored by POGODALLA Sylvain's avatar POGODALLA Sylvain
Browse files

No commit message

No commit message
parent 769e6ac5
load d ../data/comp.acg;
surface meaning analyse G_top (John_top) (lambda y.G_comp (THE_MOST y) (Lambda d' .lambda z. EARN z d')) : S;
surface meaning analyse G_top (John_top) (lambda y.G_comp (THE_MOST y) (Lambda d' .lambda z. LIKE Mary z d')) : S;
surface meaning analyse G_top (Mary_top) (lambda y.G_comp (THE_MOST y) (Lambda d' .lambda z. LIKE z John d')) : S;
......@@ -53,7 +53,7 @@ type type_error =
| Other
| Is_Used of string * string
| Two_occurrences_of_linear_variable of (Lexing.position * Lexing.position)
| Non_empty_context of (string*(Lexing.position * Lexing.position))
| Non_empty_context of (string*(Lexing.position * Lexing.position)*(Lexing.position * Lexing.position)*string)
| Not_normal
| Vacuous_abstraction of (string * (Lexing.position * Lexing.position))
......@@ -133,7 +133,7 @@ let type_error_to_string = function
| Other -> "Not yet implemented"
| Is_Used (s1,s2) -> Printf.sprintf "The type of this expression is \"%s\" but is used with type \"%s\"" s1 s2
| Two_occurrences_of_linear_variable (s,e) -> Printf.sprintf "This linear variable was already used: %s" (compute_comment_for_position s e)
| Non_empty_context (x,(s,e)) -> Printf.sprintf "This term has a non empty linear context (variable \"%s\" at %s)" x (compute_comment_for_position s e)
| Non_empty_context (x,(s,e),funct_pos,funct_type) -> Printf.sprintf "This term contains a free linear variable \"%s\" at %s and is argument the term of type %s at %s )" x (compute_comment_for_position s e) funct_type (compute_comment_for_position (fst funct_pos) (snd funct_pos))
| Not_normal -> "This term is not in normal form"
| Vacuous_abstraction (x,(s,e)) -> Printf.sprintf "This linear variable \"%s\" is abstracted over but not used in term %s" x (compute_comment_for_position s e)
......
......@@ -38,7 +38,7 @@ type type_error =
| Other
| Is_Used of string * string
| Two_occurrences_of_linear_variable of (Lexing.position * Lexing.position)
| Non_empty_context of (string*(Lexing.position * Lexing.position))
| Non_empty_context of (string*(Lexing.position * Lexing.position)*(Lexing.position * Lexing.position)*string)
| Not_normal
| Vacuous_abstraction of (string * (Lexing.position * Lexing.position))
......
......@@ -69,6 +69,8 @@ struct
let analyse ?names e ?offset data l =
try
let additional_offset = "\t" in
let actual_offset = Printf.sprintf "%s%s" (match offset with | None -> "" | Some s -> s) additional_offset in
let entries =
match names with
| None -> [E.focus e]
......@@ -83,16 +85,16 @@ struct
(match last_abs_sg with
| Some previous_sg when (E.Signature1.name sg) = (E.Signature1.name previous_sg) -> (false,last_abs_sg)
| _ ->
let () = if first then Format.printf "In %s:\n\t%!" (fst (E.Signature1.name sg)) else () in
(match Data_parser.parse_term ~output:true ?offset data sg with
let () = if first then Format.printf "In %s:\n%s%!" (fst (E.Signature1.name sg)) additional_offset else () in
(match Data_parser.parse_term ~output:true ~offset:actual_offset data sg with
| None -> let () = in_sg sg in false, Some sg
| Some _ -> false,None))
| E.Lexicon lex ->
let abs,obj=E.Lexicon.get_sig lex in
match last_abs_sg with
| Some previous_sg when (E.Signature1.name abs) = (E.Signature1.name previous_sg) -> (false,last_abs_sg)
| _ -> let () = if first then Format.printf "In %s:\n\t%!" (fst (E.Signature1.name abs)) else () in
match Data_parser.parse_term ~output:first ?offset data abs with
| _ -> let () = if first then Format.printf "In %s:\n%s%!" (fst (E.Signature1.name abs)) additional_offset else () in
match Data_parser.parse_term ~output:first ~offset:actual_offset data abs with
| None -> false,Some abs
| Some (t,ty) ->
let t',ty' = E.Lexicon.interpret t ty lex in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment